Congress.v 7.51 KB
Newer Older
1
2
3
From Coq Require Import String.
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
4
5
6
From Containers Require Import OrderedTypeEx.
From Containers Require Import MapInterface.
From Containers Require Import SetInterface.
7
8
From Containers Require MapAVL.
From Containers Require SetAVL.
9
From SmartContracts Require Import Blockchain.
10
11
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
12
From RecordUpdate Require Import RecordUpdate.
13
14
(* This is included last to default things to list rather than map/set *)
From Coq Require Import List. 
15

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

20
21
Open Scope Z.

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

24
25
26
27
Inductive CongressAction :=
  | cact_transfer (to : Address) (amount : Amount)
  | cact_call (to : Address) (amount : Amount) (msg : OakValue).

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
28
Record Proposal :=
29
  build_proposal {
30
    actions : list CongressAction;
31
32
33
    votes : Map[Address, Z];
    vote_result : Z;
    proposed_in : BlockId;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
34
35
  }.

36
Instance eta_proposal : Settable _ :=
37
  mkSettable
38
    ((constructor build_proposal) <*> actions
39
                                  <*> votes
40
41
                                  <*> vote_result
                                  <*> proposed_in)%settable.
42

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
43
Record Rules :=
44
45
46
47
  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
48
49
50
  }.

Record Setup :=
51
52
  build_setup {
    setup_rules : Rules;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
53
54
55
  }.

Inductive Msg :=
56
| TransferOwnership : Address -> Msg
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
57
| ChangeRules : Rules -> Msg
58
59
| AddMember : Address -> Msg
| RemoveMember : Address -> Msg
60
| CreateProposal : list CongressAction -> Msg
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
61
62
63
64
65
66
| VoteForProposal : ProposalId -> Msg
| VoteAgainstProposal : ProposalId -> Msg
| RetractVote : ProposalId -> Msg
| FinishProposal : ProposalId -> Msg.

Record State :=
67
68
69
70
71
72
  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
73
74
  }.

75
Instance eta_state : Settable _ :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
76
  mkSettable
77
78
    ((constructor build_state) <*> owner
                               <*> state_rules
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
79
                               <*> proposals
80
81
                               <*> next_proposal_id
                               <*> members)%settable.
82
  
83
84
85
86
87
88
89
90
91
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).

92
Definition init (ctx : ContractCallContext) (setup : Setup) : option State :=
93
94
95
96
97
98
  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
99
100
101
  else
    None.

102
Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
103
104
105
106
107
108
109
110
111
112
113
  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)
114
115
116
117
           (pid : ProposalId)
           (vote : Z)
           (state : State)
  : option State :=
118
119
120
  do proposal <- state.(proposals)[pid]%map;
  let old_vote := match proposal.(votes)[voter]%map with
                 | Some old => old
121
                 | None => 0
122
                 end in
123
124
125
126
  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]]).
127

128
129
Definition retract_vote
           (voter : Address)
130
131
132
           (pid : ProposalId)
           (state : State)
  : option State :=
133
134
135
136
137
138
139
  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]]).

140
141
142
143
144
145
Definition congress_action_to_chain_action (act : CongressAction) : ChainAction :=
  match act with
  | cact_transfer to amt => act_transfer to amt
  | cact_call to amt msg => act_call to amt msg
  end.

146
Definition finish_proposal
147
148
           (pid : ProposalId)
           (state : State)
149
150
151
152
153
154
155
           (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
156
157
    None
  else
158
159
160
161
162
163
164
165
166
167
168
169
    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
170
171
    let response_chain_acts := map congress_action_to_chain_action response_acts in
    Some (new_state, response_chain_acts).
172

173
Definition receive
174
           (ctx : ContractCallContext)
175
           (state : State)
176
177
           (maybe_msg : option Msg)
  : option (State * list ChainAction) :=
178
  let chain := ctx.(ctx_chain) in
179
180
181
182
183
184
185
186
187
188
189
  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]], [ ])
190
        else
191
            None
192

193
194
  | true, _, Some (AddMember new_member) =>
        Some (state[[members ::= SetInterface.add new_member]], [ ])
195

196
197
  | true, _, Some (RemoveMember old_member) =>
        Some (state[[members ::= SetInterface.remove old_member]], [ ])
198

199
200
  | _, true, Some (CreateProposal actions) =>
        Some (add_proposal actions chain state, [ ])
201

202
  | _, true, Some (VoteForProposal pid) =>
203
        without_actions (vote_on_proposal sender pid 1 state)
204
205

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

208
  | _, true, Some (RetractVote pid) =>
209
        without_actions (retract_vote sender pid state)
210

211
  | _, _, Some (FinishProposal pid) =>
212
        finish_proposal pid state chain
213
 
214
215
216
  | _, _, _ =>
        None
    
217
  end.