Congress.v 16.8 KB
Newer Older
1
2
From Coq Require Import ZArith.
From Coq Require Import Program.Basics.
3
From Coq Require Import Morphisms.
4
From Coq Require Import Program.
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 SmartContracts Require Import Extras.
11
From RecordUpdate Require Import RecordUpdate.
12
From Coq Require Import List.
13

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  end.

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

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

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

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

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

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

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

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

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

337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
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.

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

(*
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
Section Theories.
Local Open Scope nat.
Definition num_proposed_congress_actions chain address :=
  let extract tx :=
      match tx_body tx with
      | tx_call msg =>
        match deserialize msg with
        | Some (create_proposal acts) => length acts
        | _ => 0
        end
      | _ => 0
      end in
  fold_right (fun tx n => n + extract tx) 0 (incoming_txs chain address).

Definition num_proposed_congress_actions_in_state chain address :=
  match contract_state chain address >>= deserialize with
  | Some state =>
    fold_right (fun proposal n => n + length (actions proposal)) 0 (FMap.values (proposals state))
  | None => 0
  end.

Instance num_proposed_congress_actions_proper :
  Proper (ChainEquiv ==> eq ==> eq) num_proposed_congress_actions.
Proof.
  now repeat intro; subst; unfold num_proposed_congress_actions;
    match goal with
    | [H: ChainEquiv _ _ |- _] => rewrite H
    end.
Qed.

Instance num_proposed_congress_actions_in_state_proper :
  Proper (ChainEquiv ==> eq ==> eq) num_proposed_congress_actions_in_state.
Proof.
  now repeat intro; subst; unfold num_proposed_congress_actions_in_state;
    match goal with
    | [H: ChainEquiv _ _ |- _] => rewrite H
    end.
Qed.

Lemma num_proposed_congress_actions_unchanged c1 c2 address :
  incoming_txs c1 address = incoming_txs c2 address ->
  num_proposed_congress_actions c1 address = num_proposed_congress_actions c2 address.
Proof.
  Admitted.

Lemma num_proposed_congress_actions_in_state_unchanged c1 c2 address :
  incoming_txs c1 address = incoming_txs c2 address ->
  num_proposed_congress_actions_in_state c1 address =
  num_proposed_congress_actions_in_state c2 address.
Proof.
  Admitted.

Local Open Scope trace.
Lemma trace_prefix_refl {e1 q1 e2 q2} {trace : ChainTrace e1 q1 e2 q2} :
  trace `prefix_of` ctrace_refl -> trace ~= @ctrace_refl _ e1 q1.
Proof.
  intros [suffix app_eq].
  dependent destruction suffix; cbn in *; inversion app_eq; auto.
Qed.

Definition ends_with_tx_from
           (address : Address)
           {from from_queue to to_queue}
           (trace : ChainTrace from from_queue to to_queue) : Prop :=
  match trace with
  | ctrace_step _ step => step_from step = address
  | _ => False
  end.

Definition ends_with_tx_to
           (address : Address)
           {from from_queue to to_queue}
           (trace : ChainTrace from from_queue to to_queue) : Prop :=
  match trace with
  | ctrace_step _ step => step_to step = address
  | _ => False
  end.

Lemma matching_proposals env l address (trace : ChainTrace empty_env [] env l) :
  forall out_env out_q (out_t : ChainTrace empty_env [] out_env out_q),
    out_t `prefix_of` trace /\ ends_with_tx_from address out_t ->
    exists in_env in_q (in_t : ChainTrace empty_env [] in_env in_q),
      in_t `prefix_of` out_t /\ ends_with_tx_to address in_t.
Proof.
  remember empty_env eqn:eq.
  induction trace; intros out_env out_q out_t [out_prefix out_is_out].
  - destruct out_prefix as [suffix suffix_eq].
    destruct out_t; try inversion out_is_out.
    dependent destruction suffix; inversion suffix_eq.
  -
specialize (IHtrace eq).


    dependent destruction out_t;
      dependent destruction suffix; try inversion suffix_eq.
    inversion out_is_out.
  - Show Proof.
dependent destruction out_t; unfold EndsWithTxFrom in *;
      try solve [inversion out_is_out].
    destruct out_prefix.
    +
pose proof (trace_prefix_refl out_prefix).
    inversion H.
    rewrite H in out_is_out.
    { dependent destruction out_t; auto.


rewrite (trace_prefix_refl out_prefix) in out_is_out.

 inversion contract_out_prefix.

  ChainTrace env l ->
  env_contracts env address = Some (Congress.contract : WeakContract) ->
  num_proposed_congress_actions_in_state env address +
  length (outgoing_txs env address) <= num_proposed_congress_actions env address.
Proof.
  intros trace congress_deployed.
  Hint Resolve contract_addr_format.
  assert (address_is_contract address = true) as addr_format
      by eauto.
  induction trace.
  - now rewrite H.
  - rewrite H1 in *; auto.
  - destruct H.
    + rewrite H3 in *.
      assert (incoming_txs (add_tx tx pre) address = incoming_txs pre address).
      {
        cbn.
        unfold add_tx_to_map; destruct_address_eq; subst; cbn in *; congruence.
      }
      erewrite num_proposed_congress_actions_unchanged,
      num_proposed_congress_actions_in_state_unchanged; try eassumption.

      unfold num_proposed_congress_actions.
      assert (incoming_txs (add_tx tx pre
      unfold num_proposed_congress_actions, num_proposed_congress_actions_in_state.
      unfold contract_state.
      cbn.
      unfold add_tx_to_map.
      subst tx; cbn.
      assert (address <> to) by (destruct (address_eqb_spec address to); congruence).

      subst tx.
      cbn in *.

      subst tx.
      cbn in *.
      apply IHc.
  - auto.
End Theories.
515
*)
516
517

End Congress.