Congress.v 12.3 KB
Newer Older
1
2
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
3
4
From Coq Require Import Morphisms.

5
From SmartContracts Require Import Blockchain.
6
7
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
8
From SmartContracts Require Import Containers.
9
From SmartContracts Require Import Automation.
10
From RecordUpdate Require Import RecordUpdate.
11
From Coq Require Import List.
12

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
13
14
15
Import ListNotations.
Import RecordSetNotations.

16
17
18
19
Section Congress.
Context {BaseTypes : ChainBaseTypes}.

Local Open Scope Z.
20
Set Primitive Projections.
21

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
    votes : FMap Address Z;
32
    vote_result : Z;
33
    proposed_in : nat;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
34
35
  }.

36
37
Instance proposal_settable : Settable _ :=
  settable! build_proposal <actions; votes; vote_result; proposed_in>.
38

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

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

Inductive Msg :=
52
53
54
55
56
57
58
59
60
  | 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
61
62

Record State :=
63
64
65
  build_state {
    owner : Address;
    state_rules : Rules;
66
    proposals : FMap nat Proposal;
67
    next_proposal_id : ProposalId;
68
    members : FMap Address unit;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
69
70
  }.

71
72
Instance state_settable : Settable _ :=
  settable! build_state <owner; state_rules; proposals; next_proposal_id; members>.
73

74
75
76
77
78
79
80
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)
81
        && (0 <=? rules.(debating_period_in_blocks))%nat.
82

83
84
85
86
Definition init
           (chain : Chain)
           (ctx : ContractCallContext)
           (setup : Setup) : option State :=
87
88
  if validate_rules setup.(setup_rules) then
    Some {| owner := ctx.(ctx_from);
89
            state_rules := setup.(setup_rules);
90
            proposals := FMap.empty;
91
            next_proposal_id := 1%nat;
92
            members := FMap.empty |}
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
93
94
95
  else
    None.

96
Definition add_proposal (actions : list CongressAction) (chain : Chain) (state : State) : State :=
97
  let id := state.(next_proposal_id) in
98
  let slot_num := chain.(block_header).(slot_number) in
99
  let proposal := {| actions := actions;
100
                     votes := FMap.empty;
101
                     vote_result := 0;
102
                     proposed_in := slot_num |} in
103
  let new_proposals := FMap.add id proposal state.(proposals) in
104
  state<|proposals := new_proposals|><|next_proposal_id := (id + 1)%nat|>.
105
106
107

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

123
Definition do_retract_vote
124
           (voter : Address)
125
126
127
           (pid : ProposalId)
           (state : State)
  : option State :=
128
129
130
  do proposal <- FMap.find pid state.(proposals);
  do old_vote <- FMap.find voter proposal.(votes);
  let new_votes := FMap.remove voter proposal.(votes) in
131
  let new_vote_result := proposal.(vote_result) - old_vote in
132
133
134
  let new_proposal :=
      proposal<|votes := new_votes|><|vote_result := new_vote_result|> in
  Some (state<|proposals ::= FMap.add pid new_proposal|>).
135

136
Definition congress_action_to_chain_action (act : CongressAction) : ActionBody :=
137
138
139
140
141
  match act with
  | cact_transfer to amt => act_transfer to amt
  | cact_call to amt msg => act_call to amt msg
  end.

142
Definition do_finish_proposal
143
144
           (pid : ProposalId)
           (state : State)
145
           (chain : Chain)
146
  : option (State * list ActionBody) :=
147
  do proposal <- FMap.find pid state.(proposals);
148
  let rules := state.(state_rules) in
149
150
151
  let debate_end := (proposal.(proposed_in) + rules.(debating_period_in_blocks))%nat in
  let cur_slot := chain.(block_header).(slot_number) in
  if (cur_slot <? debate_end)%nat then
152
153
    None
  else
154
    let new_state := state<|proposals ::= FMap.remove pid|> in
155
    let total_votes_for_proposal := Z.of_nat (FMap.size proposal.(votes)) in
156
    let total_members := Z.of_nat (FMap.size state.(members)) in
157
158
159
160
161
162
163
164
    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)
165
        else [] in
166
167
    let response_chain_acts := map congress_action_to_chain_action response_acts in
    Some (new_state, response_chain_acts).
168

169
Definition receive
170
           (chain : Chain)
171
           (ctx : ContractCallContext)
172
           (state : State)
173
           (maybe_msg : option Msg)
174
  : option (State * list ActionBody) :=
175
176
  let sender := ctx.(ctx_from) in
  let is_from_owner := (sender =? state.(owner))%address in
177
  let is_from_member := FMap.mem sender state.(members) in
178
  let without_actions := option_map (fun new_state => (new_state, [])) in
179
  match is_from_owner, is_from_member, maybe_msg with
180
  | true, _, Some (transfer_ownership new_owner) =>
181
        Some (state<|owner := new_owner|>, [])
182

183
  | true, _, Some (change_rules new_rules) =>
184
        if validate_rules new_rules then
185
            Some (state<|state_rules := new_rules|>, [])
186
        else
187
            None
188

189
  | true, _, Some (add_member new_member) =>
190
        Some (state<|members ::= FMap.add new_member tt|>, [])
191

192
  | true, _, Some (remove_member old_member) =>
193
        Some (state<|members ::= FMap.remove old_member|>, [])
194

195
  | _, true, Some (create_proposal actions) =>
196
        Some (add_proposal actions chain state, [])
197

198
  | _, true, Some (vote_for_proposal pid) =>
199
        without_actions (vote_on_proposal sender pid 1 state)
200

201
  | _, true, Some (vote_against_proposal pid) =>
202
        without_actions (vote_on_proposal sender pid (-1) state)
203

204
205
206
207
208
  | _, true, Some (retract_vote pid) =>
        without_actions (do_retract_vote sender pid state)

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

210
211
  | _, _, _ =>
        None
212
213
214
215
216
217
218

  end.

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

219
Global Program Instance rules_equivalence : OakTypeEquivalence Rules :=
220
221
222
223
224
225
226
  {| 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; |}.
227
228
229
230
231
Next Obligation.
  intros x. unfold deserialize_rules.
  rewrite deserialize_serialize.
  reflexivity.
Qed.
232

233
Global Program Instance setup_equivalence : OakTypeEquivalence Setup :=
234
235
236
237
  {| serialize s := serialize s.(setup_rules);
     deserialize or :=
       do rules <- deserialize or;
       Some (build_setup rules); |}.
238
239
240
241
242
243
Next Obligation.
  intros x.
  simpl.
  rewrite deserialize_serialize.
  reflexivity.
Qed.
244
245
246
247
248
249
250
251

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).

252
Global Program Instance congress_action_equivalence : OakTypeEquivalence CongressAction :=
253
254
255
256
257
258
259
260
  {| 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.
261
  intros ca.
262
  unfold deserialize_congress_action.
263
264
  rewrite deserialize_serialize.
  destruct ca; reflexivity.
265
266
267
268
269
270
Qed.

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

271
Global Program Instance proposal_equivalence : OakTypeEquivalence Proposal :=
272
273
274
275
276
277
  {| serialize p :=
       let (a, b, c, d) := p in
       serialize (a, b, c, d);
     deserialize := deserialize_proposal;
  |}.
Next Obligation.
278
  intros p.
279
  unfold deserialize_proposal.
280
281
  rewrite deserialize_serialize.
  destruct p; reflexivity.
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
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.

313
Global Program Instance msg_equivalence : OakTypeEquivalence Msg :=
314
315
  {| serialize := serialize_msg; deserialize := deserialize_msg; |}.
Next Obligation.
316
  intros msg.
317
  unfold serialize_msg, deserialize_msg.
318
  destruct msg; repeat (simpl; rewrite deserialize_serialize); reflexivity.
319
320
321
322
323
324
325
326
327
328
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).

329
Global Program Instance state_equivalence : OakTypeEquivalence State :=
330
331
332
  {| serialize := serialize_state; deserialize := deserialize_state; |}.
Next Obligation.
  unfold serialize_state, deserialize_state.
333
  destruct x; repeat (simpl; rewrite deserialize_serialize); reflexivity.
334
335
Qed.

336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
Ltac solve_contract_proper :=
  repeat
    match goal with
    | [|- ?x _  = ?x _] => unfold x
    | [|- ?x _ _ = ?x _ _] => unfold x
    | [|- ?x _ _ _ = ?x _ _ _] => unfold x
    | [|- ?x _ _ _ _ = ?x _ _ _ _] => unfold x
    | [|- ?x _ _ _ _ = ?x _ _ _ _] => unfold x
    | [|- ?x _ _ _ _ _ = ?x _ _ _ _ _] => unfold x
    | [|- Some _ = Some _] => f_equal
    | [|- pair _ _ = pair _ _] => f_equal
    | [|- (if ?x then _ else _) = (if ?x then _ else _)] => destruct x
    | [|- match ?x with | _ => _ end = match ?x with | _ => _ end ] => destruct x
    | _ => prove
    end.

Lemma init_proper :
  Proper (ChainEquiv ==> eq ==> eq ==> eq) init.
Proof. repeat intro; solve_contract_proper. Qed.

Lemma receive_proper :
  Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive.
Proof. repeat intro; solve_contract_proper. Qed.

360
Definition contract : Contract Setup Msg State :=
361
  build_contract version init init_proper receive receive_proper.
362

363
End Congress.
364

365
366
367
368
369
370
371
372
373
(*
(* This first property states that the Congress will only send out actions
   to be performed if there is a matching CreateProposal somewhere in the
   past. That is, no CreateProposal can lead to two batches of actions being
   sent out, and the actions correspond to the ones passed in CreateProposal. *)
Theorem congress_no_unmatched_actions
        (chain : Chain)
        (
*)