LocalBlockchain.v 18.6 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
From Coq Require Import ZArith.
2
From Coq Require Import Permutation.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
3
From Coq Require Import Morphisms.
4
5
6
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
7
8
From SmartContracts Require Import Containers.
From SmartContracts Require Import Extras.
9
10
From SmartContracts Require Import Automation.
From SmartContracts Require Import BoundedN.
11
From SmartContracts Require Import Circulation.
12
From SmartContracts Require Import ChainedList.
13
From RecordUpdate Require Import RecordUpdate.
14
From Coq Require Import List.
15
16
From Coq Require Import Psatz.
From stdpp Require countable.
17

18
Import RecordSetNotations.
19
20
Import ListNotations.

21
22
Section LocalBlockchain.
Local Open Scope bool.
23

24
Definition AddrSize : N := 2^128.
25
Definition ContractAddrBase : N := AddrSize / 2.
26

27
Global Instance LocalChainBase : ChainBase :=
28
29
30
31
  {| Address := BoundedN AddrSize;
     address_eqb := BoundedN.eqb;
     address_eqb_spec := BoundedN.eqb_spec;
     compute_block_reward n := 50%Z;
32
     address_is_contract a := (ContractAddrBase <=? BoundedN.to_N a)%N
33
34
  |}.

35
36
37
38
39
40
41
42
43
Record LocalChain :=
  build_local_chain {
    lc_header : BlockHeader;
    lc_incoming_txs : FMap Address (list Tx);
    lc_outgoing_txs : FMap Address (list Tx);
    lc_contract_state : FMap Address OakValue;
    lc_blocks_baked : FMap Address (list nat);
    lc_contracts : FMap Address WeakContract;
  }.
44

45
46
47
48
Instance local_chain_settable : Settable _ :=
  settable! build_local_chain
  < lc_header; lc_incoming_txs; lc_outgoing_txs;
    lc_contract_state; lc_blocks_baked; lc_contracts >.
49

50
51
52
53
54
55
56
57
Definition lc_to_env (lc : LocalChain) : Environment :=
  {| env_chain :=
        {| block_header := lc_header lc;
          incoming_txs a := with_default [] (FMap.find a (lc_incoming_txs lc));
          outgoing_txs a := with_default [] (FMap.find a (lc_outgoing_txs lc));
          contract_state a := FMap.find a (lc_contract_state lc);
          blocks_baked a := with_default [] (FMap.find a (lc_blocks_baked lc)); |};
      env_contracts a := FMap.find a (lc_contracts lc); |}.
58

59
Global Coercion lc_to_env : LocalChain >-> Environment.
60
61

Section ExecuteActions.
62
63
64
65
66
67
68
69
70
71
  Local Open Scope Z.

  Definition add_tx (tx : Tx) (lc : LocalChain) : LocalChain :=
    let add_tx opt := Some (cons tx (with_default [] opt)) in
    let lc := lc<|lc_incoming_txs ::= FMap.partial_alter add_tx (tx_to tx) |> in
    let lc := lc<|lc_outgoing_txs ::= FMap.partial_alter add_tx (tx_from tx) |> in
    lc.

  Arguments add_tx : simpl never.

72
73
  Definition get_new_contract_addr (lc : LocalChain) : option Address :=
    BoundedN.of_N (ContractAddrBase + N.of_nat (FMap.size (lc_contracts lc))).
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95

  Definition add_contract
             (addr : Address)
             (wc : WeakContract)
             (lc : LocalChain) : LocalChain :=
    lc<|lc_contracts ::= FMap.add addr wc|>.

  Definition set_contract_state
             (addr : Address)
             (state : OakValue)
             (lc : LocalChain) : LocalChain :=
    lc<|lc_contract_state ::= FMap.add addr state|>.

  Definition send_or_call
             (from to : Address)
             (amount : Amount)
             (msg : option OakValue)
             (lc : LocalChain) : option (list Action * LocalChain) :=
    do if amount >? account_balance lc from then None else Some tt;
    match FMap.find to lc.(lc_contracts) with
    | None =>
      (* Fail if sending a message to address without contract *)
96
      do if address_is_contract to then None else Some tt;
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
      match msg with
        | None => Some ([], add_tx (build_tx from to amount tx_empty) lc)
        | Some msg => None
      end
    | Some wc =>
      let tx_body :=
          match msg with
          | None => tx_empty
          | Some msg => tx_call msg
          end in
      do state <- contract_state lc to;
      let lc := add_tx (build_tx from to amount tx_body) lc in
      let ctx := build_ctx from to amount in
      do '(new_state, new_actions) <- wc_receive wc  lc ctx state msg;
      let lc := set_contract_state to new_state lc in
      Some (map (build_act to) new_actions, lc)
    end.

  Definition deploy_contract
             (from : Address)
             (amount : Amount)
             (wc : WeakContract)
             (setup : OakValue)
             (lc : LocalChain)
    : option (list Action * LocalChain) :=
    do if amount >? account_balance lc from then None else Some tt;
123
    do contract_addr <- get_new_contract_addr lc;
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
    do match incoming_txs lc contract_addr with
       | _ :: _ => None
       | [] => Some tt
       end;
    do match FMap.find contract_addr (lc_contracts lc) with
       | Some _ => None
       | None => Some tt
       end;
    let body := tx_deploy (build_contract_deployment (wc_version wc) setup) in
    let lc := add_tx (build_tx from contract_addr amount body) lc in
    let ctx := build_ctx from contract_addr amount in
    do state <- wc_init wc lc ctx setup;
    let lc := add_contract contract_addr wc lc in
    let lc := set_contract_state contract_addr state lc in
    Some ([], lc).

  Local Open Scope nat.

  Definition execute_action (act : Action) (lc : LocalChain) :
    option (list Action * LocalChain) :=
    match act with
    | build_act from (act_transfer to amount) =>
      send_or_call from to amount None lc
    | build_act from (act_deploy amount wc setup) =>
      deploy_contract from amount wc setup lc
    | build_act from (act_call to amount msg) =>
      send_or_call from to amount (Some msg) lc
151
152
    end.

153
154
  Fixpoint execute_actions
           (count : nat)
155
156
157
           (acts : list Action)
           (lc : LocalChain)
           (depth_first : bool)
158
    : option LocalChain :=
159
    match count, acts with
160
    | _, [] => Some lc
161
    | 0, _ => None
162
    | S count, act :: acts =>
163
      do '(next_acts, lc) <- execute_action act lc;
164
165
166
      let acts := if depth_first
                  then next_acts ++ acts
                  else acts ++ next_acts in
167
      execute_actions count acts lc depth_first
168
    end.
169

170
171
172
  Ltac remember_tx :=
    match goal with
    | [H: context[add_tx ?a _] |- _] => remember a as tx
173
174
    end.

175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
  Lemma add_tx_equiv tx (lc : LocalChain) (env : Environment) :
    EnvironmentEquiv lc env ->
    EnvironmentEquiv (add_tx tx lc) (Blockchain.add_tx tx env).
  Proof.
    intros eq.
    apply build_env_equiv; simpl in *; try apply eq.
    apply build_chain_equiv; simpl in *; try apply eq.
    - intros addr.
      unfold add_tx_to_map.
      destruct (address_eqb_spec addr (tx_to tx)) as [eq_to|neq_to].
      + subst; rewrite FMap.find_partial_alter; simpl.
        f_equal; apply eq.
      + rewrite (FMap.find_partial_alter_ne _ _ _ _ (not_eq_sym neq_to)).
        apply eq.
    - intros addr.
      unfold add_tx_to_map.
      destruct (address_eqb_spec addr (tx_from tx)) as [eq_from|neq_from].
      + subst; rewrite FMap.find_partial_alter; simpl.
        f_equal; apply eq.
      + rewrite (FMap.find_partial_alter_ne _ _ _ _ (not_eq_sym neq_from)).
        apply eq.
  Qed.

  Lemma set_contract_state_equiv addr state (lc : LocalChain) (env : Environment) :
    EnvironmentEquiv lc env ->
    EnvironmentEquiv
      (set_contract_state addr state lc)
      (Blockchain.set_contract_state addr state env).
  Proof.
    intros eq.
    apply build_env_equiv; simpl in *; try apply eq.
    apply build_chain_equiv; simpl in *; try apply eq.
    intros addr'.
    unfold set_chain_contract_state.
    destruct (address_eqb_spec addr' addr) as [eq_addrs|neq_addrs].
    - subst; now rewrite FMap.find_add.
    - rewrite FMap.find_add_ne; [apply eq|auto].
  Qed.

  Lemma add_contract_equiv addr wc (lc : LocalChain) (env : Environment) :
    EnvironmentEquiv lc env ->
    EnvironmentEquiv
      (add_contract addr wc lc)
      (Blockchain.add_contract addr wc env).
  Proof.
    intros eq.
    apply build_env_equiv; simpl in *; try apply eq.
    intros addr'.
    destruct (address_eqb_spec addr' addr) as [eq_addrs|neq_addrs].
    - subst; now rewrite FMap.find_add.
    - rewrite FMap.find_add_ne; [apply eq|auto].
  Qed.

  Lemma send_or_call_step from to amount msg act lc_before new_acts lc_after :
    send_or_call from to amount msg lc_before = Some (new_acts, lc_after) ->
    act = build_act from (match msg with
                          | None => act_transfer to amount
                          | Some msg => act_call to amount msg
                          end) ->
234
    inhabited (ChainStep lc_before act lc_after new_acts).
235
236
237
  Proof.
    intros sent act_eq.
    unfold send_or_call in sent.
238
239
240
241
242
243
244
245
246
247
248
249
250
    (* Make goals a little more manageable by factoring intermediate envs *)
    repeat
    match goal with
    | [H: context[add_tx ?tx ?env] |- _] =>
      match type of H with
      | _ = add_tx tx env => fail 1
      | _ =>
        let name := fresh "with_tx" in
        remember (add_tx tx env) as name
      end
    end.
    destruct (Z.gtb_spec amount (account_balance lc_before from));
      [cbn in *; congruence|].
251
252
253
    destruct (FMap.find to (lc_contracts lc_before)) as [wc|] eqn:to_contract.
    - (* there is a contract at destination, so do call *)
      destruct (contract_state _ _) as [prev_state|] eqn:prev_state_eq;
254
255
256
257
        [|cbn in *; congruence].
      cbn -[lc_to_env] in *.
      destruct (wc_receive wc _ _ _ _) eqn:receive;
        [|cbn in *; congruence].
258
259
260
      match goal with
      | [p: OakValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
      end.
261
      constructor.
262
263
264
265
266
267
268
269
270
      apply (step_call from to amount wc msg prev_state new_state resp_acts);
        try solve [cbn in *; congruence].
      + rewrite <- receive.
        apply wc_receive_proper; auto.
        subst with_tx.
        symmetry.
        now apply add_tx_equiv.
      + inversion sent; subst;
          now apply set_contract_state_equiv, add_tx_equiv.
271
    - (* no contract at destination, so msg should be empty *)
272
      destruct (address_is_contract to) eqn:addr_format; simpl in *; try congruence.
273
274
      destruct msg; simpl in *; try congruence.
      assert (new_acts = []) by congruence; subst new_acts.
275
      constructor.
276
      apply (step_transfer from to amount); auto.
277
278
279
      inversion sent; subst; now apply add_tx_equiv.
  Qed.

280
281
282
283
284
285
286
287
288
289
290
291
292
293
  Lemma get_new_contract_addr_is_contract_addr lc addr :
    get_new_contract_addr lc = Some addr ->
    address_is_contract addr = true.
  Proof.
    intros get.
    unfold get_new_contract_addr in get.
    pose proof (BoundedN.of_N_some get) as eq.
    destruct addr as [addr prf].
    simpl in *; rewrite eq.
    match goal with
    | [|- context[N.leb ?a ?b = true]] => destruct (N.leb_spec a b); auto; lia
    end.
  Qed.

294
295
296
  Lemma deploy_contract_step from amount wc setup act lc_before new_acts lc_after :
    deploy_contract from amount wc setup lc_before = Some (new_acts, lc_after) ->
    act = build_act from (act_deploy amount wc setup) ->
297
    inhabited (ChainStep lc_before act lc_after new_acts).
298
299
300
301
  Proof.
    intros dep act_eq.
    unfold deploy_contract in dep.
    destruct (Z.gtb_spec amount (account_balance lc_before from)); [cbn in *; congruence|].
302
303
    destruct (get_new_contract_addr lc_before) as [contract_addr|] eqn:new_contract_addr;
      [|cbn in *; congruence].
304
305
306
307
308
309
    cbn -[incoming_txs] in dep.
    destruct (incoming_txs _ _) eqn:no_txs; [|cbn in *; congruence].
    destruct (FMap.find _ _) eqn:no_contracts; [cbn in *; congruence|].
    destruct (wc_init _ _ _ _) as [state|] eqn:recv; [|cbn in *; congruence].
    cbn in dep.
    assert (new_acts = []) by congruence; subst new_acts.
310
    Hint Resolve get_new_contract_addr_is_contract_addr : core.
311
    constructor.
312
    apply (step_deploy from contract_addr amount wc setup state); eauto.
313
314
315
316
317
318
319
320
321
322
323
324
325
    - rewrite <- recv.
      apply wc_init_proper; auto.
      now symmetry; apply add_tx_equiv.
    - inversion dep; subst lc_after.
      now apply set_contract_state_equiv, add_contract_equiv, add_tx_equiv.
  Qed.

  Lemma execute_action_step
        (act : Action)
        (new_acts : list Action)
        (lc_before : LocalChain)
        (lc_after : LocalChain) :
    execute_action act lc_before = Some (new_acts, lc_after) ->
326
    inhabited (ChainStep lc_before act lc_after new_acts).
327
328
329
330
  Proof.
    intros exec.
    unfold execute_action in exec.
    destruct act as [from body].
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
331
    Hint Resolve send_or_call_step deploy_contract_step : core.
332
333
334
    destruct body as [to amount|to amount msg|amount wc setup]; eauto.
  Qed.

335
336
337
338
  Lemma execute_actions_reachable count acts (lc lc_final : LocalChain) df :
    reachable (build_chain_state lc acts) ->
    execute_actions count acts lc df = Some lc_final ->
    reachable (build_chain_state lc_final []).
339
  Proof.
340
    unfold reachable.
341
    revert acts lc lc_final.
342
    induction count as [| count IH]; intros acts lc lc_final trace exec; cbn in *.
343
344
345
346
    - destruct acts; congruence.
    - destruct acts as [|x xs]; try congruence.
      destruct (execute_action x lc) as [[new_acts lc_after]|] eqn:exec_once;
        cbn in *; try congruence.
347
348
      destruct (execute_action_step _ _ _ _ exec_once) as [step].
      destruct trace as [trace].
349
      Hint Constructors ChainEvent : core.
350
      Hint Constructors ChainedList : core.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
351
      Hint Unfold ChainTrace : core.
352
353
354
355
356
357
358
359
360
      destruct df.
      + (* depth-first case *)
        eapply IH; try eassumption; eauto.
      + (* breadth-first case. Insert permute event. *)
        eapply IH; try eassumption.
        assert (Permutation (new_acts ++ xs) (xs ++ new_acts)) by perm_simplify.
        cut (ChainTrace
              empty_state
              (build_chain_state lc_after (new_acts ++ xs))); eauto.
361
  Qed.
362
363
End ExecuteActions.

364
365
Definition lc_initial : LocalChain :=
  {| lc_header :=
366
367
       {| block_height := 0;
          slot_number := 0;
368
369
370
371
          finalized_height := 0; |};
     lc_incoming_txs := FMap.empty;
     lc_outgoing_txs := FMap.empty;
     lc_contract_state := FMap.empty;
372
     lc_blocks_baked := FMap.empty;
373
374
375
376
377
     lc_contracts := FMap.empty; |}.

Record LocalChainBuilder :=
  build_local_chain_builder {
    lcb_lc : LocalChain;
378
    lcb_reachable : reachable (build_chain_state lcb_lc []);
379
380
  }.

381
382
383
Definition lcb_initial : LocalChainBuilder.
Proof.
  refine
384
    {| lcb_lc := lc_initial; lcb_reachable := _ |}.
385
  constructor.
386
  exact clnil.
387
Defined.
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

Definition validate_header (new old : BlockHeader) : option unit :=
  let (prev_block_height, prev_slot_number, prev_finalized_height) := old in
  let (block_height, slot_number, finalized_height) := new in
  if (block_height =? S prev_block_height)
       && (prev_slot_number <? slot_number)
       && (finalized_height <=? prev_block_height)
       && (prev_finalized_height <=? finalized_height)
  then Some tt
  else None.

Lemma validate_header_valid (new old : BlockHeader) :
  validate_header new old = Some tt ->
  IsValidNextBlock new old.
Proof.
  intros valid.
  destruct new as [block_height slot_number fin_height];
  destruct old as [prev_block_height prev_slot_number prev_fin_height].
  unfold IsValidNextBlock.
  simpl in *.
  repeat
    match goal with
    | [H: context[Nat.eqb ?a ?b] |- _] => destruct (Nat.eqb_spec a b)
    | [H: context[Nat.ltb ?a ?b] |- _] => destruct (Nat.ltb_spec a b)
    | [H: context[Nat.leb ?a ?b] |- _] => destruct (Nat.leb_spec a b)
    end; simpl in *; intuition.
Qed.

416
417
418
419
420
421
422
Definition validate_actions (actions : list Action) : option unit :=
  if existsb (fun act => address_is_contract (act_from act)) actions
  then None
  else Some tt.

Lemma validate_actions_valid actions :
  validate_actions actions = Some tt ->
423
  Forall ActIsFromAccount actions.
424
425
426
427
428
Proof.
  intros valid.
  induction actions as [|x xs IH]; auto.
  unfold validate_actions in valid.
  cbn -[address_is_contract] in valid.
429
430
  destruct (address_is_contract _) eqn:eq1; try (cbn in *; congruence).
  destruct (existsb _) eqn:eq2; try (cbn in *; congruence).
431
432
433
434
435
436
  clear valid.
  unfold validate_actions in IH.
  rewrite eq2 in IH.
  auto.
Qed.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
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
Definition add_new_block_header
           (header : BlockHeader)
           (baker : Address)
           (lc : LocalChain) : LocalChain :=
  let add_block o :=
      Some ((block_height header) :: (with_default [] o)) in
  let lc := lc<|lc_blocks_baked ::= FMap.partial_alter add_block baker|> in
  let lc := lc<|lc_header := header|> in
  lc.

Lemma add_new_block_header_equiv header baker (lc : LocalChain) (env : Environment) :
  EnvironmentEquiv lc env ->
  EnvironmentEquiv
    (add_new_block_header header baker lc)
    (Blockchain.add_new_block_header header baker env).
Proof.
  intros eq.
  apply build_env_equiv; try apply eq.
  apply build_chain_equiv; try apply eq; auto.
  intros addr.
  cbn.
  destruct (address_eqb_spec addr baker) as [addrs_eq|addrs_neq].
  - subst.
    rewrite FMap.find_partial_alter.
    cbn.
    f_equal.
    apply eq.
  - rewrite FMap.find_partial_alter_ne; auto.
    apply eq.
Qed.
467

468
469
470
471
(* Adds a block to the chain by executing the specified chain actions.
   Returns the new chain if the execution succeeded (for instance,
   transactions need enough funds, contracts should not reject, etc. *)
Definition add_block
472
           (depth_first : bool)
473
           (lcb : LocalChainBuilder)
474
475
476
477
478
479
480
481
482
483
484
485
486
487
           (baker : Address)
           (actions : list Action)
           (slot_number : nat)
           (finalized_height : nat)
  : option LocalChainBuilder.
Proof.
  refine (
      let lcopt :=
         let lc := lcb_lc lcb in
         let new_header :=
             {| block_height := S (block_height (lc_header lc));
                slot_number := slot_number;
                finalized_height := finalized_height; |} in
         do validate_header new_header (lc_header lc);
488
         do validate_actions actions;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
489
         let lc := add_new_block_header new_header baker lc in
490
         execute_actions 1000 actions lc depth_first in
491
492
493
494
      _).

  destruct lcopt as [lc|] eqn:exec; [|exact None].
  subst lcopt.
495
  cbn -[execute_actions address_is_contract] in exec.
496
  destruct (validate_header _) eqn:validate; [|simpl in *; congruence].
497
  destruct (validate_actions _) eqn:validate_actions; [|simpl in *; congruence].
498
499
  destruct_units.
  destruct lcb as [prev_lc_end prev_lcb_trace].
500
501
  refine (Some {| lcb_lc := lc; lcb_reachable := _ |}).
  cbn -[execute_actions] in exec.
502
  destruct prev_lcb_trace as [prev_lcb_trace].
503

504
  refine (execute_actions_reachable _ _ _ _ _ _ exec).
505
506
  constructor.
  refine (snoc prev_lcb_trace _).
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
507
  Hint Resolve validate_header_valid validate_actions_valid : core.
508
509
510
  eapply evt_block; eauto.
  apply add_new_block_header_equiv.
  reflexivity.
511
512
Defined.

513
Global Instance LocalChainBuilderDepthFirst : ChainBuilderType :=
514
515
516
  {| builder_type := LocalChainBuilder;
     builder_initial := lcb_initial;
     builder_env lcb := lcb_lc lcb;
517
     builder_add_block := add_block true;
518
     builder_reachable := lcb_reachable; |}.
519

520
Definition LocalChainBuilderBreadthFirst : ChainBuilderType :=
521
522
523
524
  {| builder_type := LocalChainBuilder;
     builder_initial := lcb_initial;
     builder_env lcb := lcb_lc lcb;
     builder_add_block := add_block false;
525
     builder_reachable := lcb_reachable; |}.
526
End LocalBlockchain.