Congress.v 11.2 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
(* This is included last to default things to list rather than map/set *)
14
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
Open Scope Z.
21
Set Primitive Projections.
22

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

25
26
27
28
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
29
Record Proposal :=
30
  build_proposal {
31
    actions : list CongressAction;
32
33
34
    votes : Map[Address, Z];
    vote_result : Z;
    proposed_in : BlockId;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
35
36
  }.

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

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

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

Inductive Msg :=
57
58
59
60
61
62
63
64
65
  | transfer_ownership : Address -> Msg
  | change_rules : Rules -> Msg
  | add_member : Address -> Msg
  | remove_member : Address -> Msg
  | create_proposal : list CongressAction -> Msg
  | vote_for_proposal : ProposalId -> Msg
  | vote_against_proposal : ProposalId -> Msg
  | retract_vote : ProposalId -> Msg
  | finish_proposal : ProposalId -> Msg.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
66
67

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

76
Instance eta_state : Settable _ :=
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
77
  mkSettable
78
79
    ((constructor build_state) <*> owner
                               <*> state_rules
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
80
                               <*> proposals
81
82
                               <*> next_proposal_id
                               <*> members)%settable.
83

84
85
86
87
88
89
90
91
92
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).

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

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

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

141
142
143
144
145
146
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.

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

174
Definition receive
175
           (ctx : ContractCallContext)
176
           (state : State)
177
178
           (maybe_msg : option Msg)
  : option (State * list ChainAction) :=
179
  let chain := ctx.(ctx_chain) in
180
181
182
183
184
  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
185
  | true, _, Some (transfer_ownership new_owner) =>
186
187
        Some (state[[owner := new_owner]], [ ])

188
  | true, _, Some (change_rules new_rules) =>
189
190
        if validate_rules new_rules then
            Some (state[[state_rules := new_rules]], [ ])
191
        else
192
            None
193

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

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

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

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

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

209
210
211
212
213
  | _, true, Some (retract_vote pid) =>
        without_actions (do_retract_vote sender pid state)

  | _, _, Some (finish_proposal pid) =>
        do_finish_proposal pid state chain
214

215
216
  | _, _, _ =>
        None
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328

  end.

Definition deserialize_rules (v : OakValue) : option Rules :=
  do '((a, b), c) <- deserialize v;
  Some (build_rules a b c).

Program Instance rules_equivalence : OakTypeEquivalence Rules :=
  {| serialize r := let (a, b, c) := r in serialize (a, b, c);
     (* Why does
     deserialize v :=
       do '((a, b), c) <- deserialize v;
       Some (build_rules a b c); |}.
       not work here? *)
     deserialize := deserialize_rules; |}.

Program Instance setup_equivalence : OakTypeEquivalence Setup :=
  {| serialize s := serialize s.(setup_rules);
     deserialize or :=
       do rules <- deserialize or;
       Some (build_setup rules); |}.

Definition deserialize_congress_action (v : OakValue) : option CongressAction :=
  do val <- deserialize v;
  Some (match val with
  | inl (to, amount) => cact_transfer to amount
  | inr (to, amount, msg) => cact_call to amount msg
  end).

Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
  {| serialize ca :=
       serialize
         match ca with
         | cact_transfer to amount => inl (to, amount)
         | cact_call to amount msg => inr (to, amount, msg)
         end;
     deserialize := deserialize_congress_action; |}.
Next Obligation.
  unfold deserialize_congress_action.
  rewrite ote_equivalence.
  destruct x; reflexivity.
Qed.

Definition deserialize_proposal (v : OakValue) : option Proposal :=
  do '(a, b, c, d) <- deserialize v;
  Some (build_proposal a b c d).

Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
  {| serialize p :=
       let (a, b, c, d) := p in
       serialize (a, b, c, d);
     deserialize := deserialize_proposal;
  |}.
Next Obligation.
  unfold deserialize_proposal.
  rewrite ote_equivalence.
  destruct x; reflexivity.
Qed.

Definition serialize_msg (m : Msg) : OakValue :=
  serialize
    match m with
    | transfer_ownership a => (0, serialize a)
    | change_rules r => (1, serialize r)
    | add_member a => (2, serialize a)
    | remove_member a => (3, serialize a)
    | create_proposal l => (4, serialize l)
    | vote_for_proposal pid => (5, serialize pid)
    | vote_against_proposal pid => (6, serialize pid)
    | retract_vote pid => (7, serialize pid)
    | finish_proposal pid => (8, serialize pid)
    end.

Definition deserialize_msg (v : OakValue) : option Msg :=
  do '(tag, v) <- deserialize v;
  match tag with
  | 0 => option_map transfer_ownership (deserialize v)
  | 1 => option_map change_rules (deserialize v)
  | 2 => option_map add_member (deserialize v)
  | 3 => option_map remove_member (deserialize v)
  | 4 => option_map create_proposal (deserialize v)
  | 5 => option_map vote_for_proposal (deserialize v)
  | 6 => option_map vote_against_proposal (deserialize v)
  | 7 => option_map retract_vote (deserialize v)
  | 8 => option_map finish_proposal (deserialize v)
  | _ => None
  end.

Program Instance msg_equivalence : OakTypeEquivalence Msg :=
  {| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
  unfold serialize_msg, deserialize_msg.
  destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
Qed.

Definition serialize_state (s : State) : OakValue :=
  let (a, b, c, d, e) := s in
  serialize (a, b, c, d, e).

Definition deserialize_state (v : OakValue) : option State :=
  do '(a, b, c, d, e) <- deserialize v;
  Some (build_state a b c d e).

Program Instance state_equivalence : OakTypeEquivalence State :=
  {| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
  unfold serialize_state, deserialize_state.
  destruct x; repeat (simpl; rewrite ote_equivalence); reflexivity.
Qed.

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