Congress.v 7.1 KB
Newer Older
1
2
3
4
From Coq Require Import String.
From Coq Require Import List.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
5
6
7
From Containers Require Import OrderedTypeEx.
From Containers Require Import MapInterface.
From Containers Require Import SetInterface.
8
9
From Containers Require MapAVL.
From Containers Require SetAVL.
10
From SmartContracts Require Import Blockchain.
11
12
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
13
14
From RecordUpdate Require Import RecordUpdate.

15
Import MapNotations.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
16
17
18
Import ListNotations.
Import RecordSetNotations.

19
20
Open Scope Z.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
21
22
23
Definition ProposalId := nat.

Record Proposal :=
24
25
26
27
28
  build_proposal {
    actions : list ChainAction;
    votes : Map[Address, Z];
    vote_result : Z;
    proposed_in : BlockId;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
29
30
  }.

31
Instance eta_proposal : Settable _ :=
32
  mkSettable
33
    ((constructor build_proposal) <*> actions
34
                                  <*> votes
35
36
                                  <*> vote_result
                                  <*> proposed_in)%settable.
37

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
38
Record Rules :=
39
40
41
42
  build_rules {
    min_vote_count_permille : Z;
    margin_needed_permille : Z;
    debating_period_in_blocks : Z;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
43
44
45
  }.

Record Setup :=
46
47
  build_setup {
    setup_rules : Rules;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
48
49
50
  }.

Inductive Msg :=
51
| TransferOwnership : Address -> Msg
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
52
| ChangeRules : Rules -> Msg
53
54
55
| AddMember : Address -> Msg
| RemoveMember : Address -> Msg
| CreateProposal : list ChainAction -> Msg
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
56
57
58
59
60
61
| VoteForProposal : ProposalId -> Msg
| VoteAgainstProposal : ProposalId -> Msg
| RetractVote : ProposalId -> Msg
| FinishProposal : ProposalId -> Msg.

Record State :=
62
63
64
65
66
67
  build_state {
    owner : Address;
    state_rules : Rules;
    proposals : Map[nat, Proposal];
    next_proposal_id : ProposalId;
    members : SetInterface.set Address;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
68
69
  }.

70
Instance eta_state : Settable _ :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
71
  mkSettable
72
73
    ((constructor build_state) <*> owner
                               <*> state_rules
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
74
                               <*> proposals
75
76
                               <*> next_proposal_id
                               <*> members)%settable.
77
  
78
79
80
81
82
83
84
85
86
Definition version : Version := 1%nat.

Definition validate_rules (rules : Rules) : bool :=
    (rules.(min_vote_count_permille) >=? 0)
        && (rules.(min_vote_count_permille) <=? 1000)
        && (rules.(margin_needed_permille) >=? 0)
        && (rules.(margin_needed_permille) <=? 1000)
        && (rules.(debating_period_in_blocks) >=? 0).

87
Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
88
89
90
91
92
93
  if validate_rules setup.(setup_rules) then
    Some {| owner := ctx.(ctx_from);
            state_rules := setup.(setup_rules); 
            proposals := []%map;
            next_proposal_id := 1%nat;
            members := {}%set |}
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
94
95
96
  else
    None.

97
98
99
100
101
102
103
104
105
106
107
108
Definition add_proposal (actions : list ChainAction) (chain : Chain) (state : State) : State :=
  let id := state.(next_proposal_id) in
  let head_block := chain.(head_block) in
  let proposal := {| actions := actions;
                     votes := []%map;
                     vote_result := 0;
                     proposed_in := head_block.(block_header).(block_number) |} in
  let new_proposals := state.(proposals)[id <- proposal]%map in
  state[[proposals := new_proposals]][[next_proposal_id := (id + 1)%nat]].

Definition vote_on_proposal
           (voter : Address)
109
110
111
112
           (pid : ProposalId)
           (vote : Z)
           (state : State)
  : option State :=
113
114
115
  do proposal <- state.(proposals)[pid]%map;
  let old_vote := match proposal.(votes)[voter]%map with
                 | Some old => old
116
                 | None => 0
117
                 end in
118
119
120
121
  let new_votes := proposal.(votes)[voter <- vote]%map in
  let new_vote_result := proposal.(vote_result) - old_vote + vote in
  let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
  Some (state[[proposals ::= MapInterface.add pid new_proposal]]).
122

123
124
Definition retract_vote
           (voter : Address)
125
126
127
           (pid : ProposalId)
           (state : State)
  : option State :=
128
129
130
131
132
133
134
135
  do proposal <- state.(proposals)[pid]%map;
  do old_vote <- proposal.(votes)[voter]%map;
  let new_votes := MapInterface.remove voter proposal.(votes) in
  let new_vote_result := proposal.(vote_result) - old_vote in
  let new_proposal := proposal[[votes := new_votes]][[vote_result := new_vote_result]] in
  Some (state[[proposals ::= MapInterface.add pid new_proposal]]).

Definition finish_proposal
136
137
           (pid : ProposalId)
           (state : State)
138
139
140
141
142
143
144
           (chain : Chain)
  : option (State * list ChainAction) :=
  do proposal <- state.(proposals)[pid]%map;
  let rules := state.(state_rules) in
  let debate_end := (Z.of_nat proposal.(proposed_in)) + rules.(debating_period_in_blocks) in
  let cur_block := chain.(head_block) in
  if (Z.of_nat cur_block.(block_header).(block_number)) <? debate_end then
145
146
    None
  else
147
148
149
150
151
152
153
154
155
156
157
158
159
    let new_state := state[[proposals ::= MapInterface.remove pid]] in
    let total_votes_for_proposal := Z.of_nat (MapInterface.cardinal proposal.(votes)) in
    let total_members := Z.of_nat (SetInterface.cardinal state.(members)) in
    let aye_votes := (proposal.(vote_result) + total_votes_for_proposal) / 2 in
    let vote_count_permille := total_votes_for_proposal * 1000 / total_members in
    let aye_permille := aye_votes * 1000 / total_votes_for_proposal in
    let enough_voters := vote_count_permille >=? rules.(min_vote_count_permille) in
    let enough_ayes := aye_permille >=? rules.(margin_needed_permille) in
    let response_acts :=
        if (enough_voters && enough_ayes)%bool
        then proposal.(actions)
        else [ ] in
    Some (new_state, response_acts).
160

161
Definition receive
162
           (ctx : ContractCallContext)
163
           (state : State)
164
165
           (maybe_msg : option Msg)
  : option (State * list ChainAction) :=
166
  let chain := ctx.(ctx_chain) in
167
168
169
170
171
172
173
174
175
176
177
  let sender := ctx.(ctx_from) in
  let is_from_owner := (sender =? state.(owner))%address in
  let is_from_member := (sender \in state.(members))%set in
  let without_actions := option_map (fun new_state => (new_state, [ ])) in
  match is_from_owner, is_from_member, maybe_msg with
  | true, _, Some (TransferOwnership new_owner) =>
        Some (state[[owner := new_owner]], [ ])

  | true, _, Some (ChangeRules new_rules) =>
        if validate_rules new_rules then
            Some (state[[state_rules := new_rules]], [ ])
178
        else
179
            None
180

181
182
  | true, _, Some (AddMember new_member) =>
        Some (state[[members ::= SetInterface.add new_member]], [ ])
183

184
185
  | true, _, Some (RemoveMember old_member) =>
        Some (state[[members ::= SetInterface.remove old_member]], [ ])
186

187
188
  | _, true, Some (CreateProposal actions) =>
        Some (add_proposal actions chain state, [ ])
189

190
  | _, true, Some (VoteForProposal pid) =>
191
        without_actions (vote_on_proposal sender pid 1 state)
192
193

  | _, true, Some (VoteAgainstProposal pid) =>
194
        without_actions (vote_on_proposal sender pid (-1) state)
195

196
  | _, true, Some (RetractVote pid) =>
197
        without_actions (retract_vote sender pid state)
198

199
  | _, _, Some (FinishProposal pid) =>
200
        finish_proposal pid state chain
201
 
202
203
204
205
  | _, _, _ =>
        None
    
  end.
206
207
208

Definition congress_contract : Contract Setup Msg State :=
  build_contract version init receive.