LocalBlockchain.v 15.8 KB
Newer Older
1
From Coq Require Import Arith ZArith.
2
3
4
From SmartContracts Require Import Blockchain.
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
5
6
From SmartContracts Require Import Containers.
From SmartContracts Require Import Extras.
7
From SmartContracts Require Import Automation.
8
From SmartContracts Require Import BoundedN.
9
From RecordUpdate Require Import RecordUpdate.
10
From Coq Require Import List.
11
From Coq Require Import Psatz.
12
From stdpp Require countable.
13

14
Import RecordSetNotations.
15
16
Import ListNotations.

17
Section LocalBlockchain.
18
Local Open Scope bool.
19

20
Definition AddrSize : N := 2^128.
21

22
Global Instance LocalChainBaseTypes : ChainBaseTypes :=
23
24
25
  {| Address := BoundedN AddrSize;
     address_eqb := BoundedN.eqb;
     address_eqb_spec := BoundedN.eqb_spec;
26
     compute_block_reward n := 50%Z;
27
  |}.
28

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
29
30
Compute LocalChainBaseTypes.

31
32
Record LocalChain :=
  build_local_chain {
33
    lc_header : BlockHeader;
34
35
    lc_incoming_txs : FMap Address (list Tx);
    lc_outgoing_txs : FMap Address (list Tx);
36
37
38
    lc_contract_state : FMap Address OakValue;
    lc_blocks_baked : FMap Address (list nat);
    lc_contracts : FMap Address WeakContract;
39
40
  }.

41
42
Instance local_chain_settable : Settable _ :=
  settable! build_local_chain
43
44
  < lc_header; lc_incoming_txs; lc_outgoing_txs;
    lc_contract_state; lc_blocks_baked; lc_contracts >.
45

46
47
48
49
50
51
52
53
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); |}.
54

55
Global Coercion lc_to_env : LocalChain >-> Environment.
56

57
Section ExecuteActions.
58
59
60
61
62
63
64
  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.
65

66
  Arguments add_tx : simpl never.
67

68
69
  Definition count_contract_deployments (lc : LocalChain) : nat :=
    FMap.size (lc_contracts lc).
70

71
72
73
  Definition add_contract
             (addr : Address)
             (wc : WeakContract)
74
75
             (lc : LocalChain) : LocalChain :=
    lc<|lc_contracts ::= FMap.add addr wc|>.
76

77
78
79
  Definition set_contract_state
             (addr : Address)
             (state : OakValue)
80
81
             (lc : LocalChain) : LocalChain :=
    lc<|lc_contract_state ::= FMap.add addr state|>.
82
83
84
85
86

  Definition send_or_call
             (from to : Address)
             (amount : Amount)
             (msg : option OakValue)
87
88
89
90
91
92
93
94
95
             (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 *)
      match msg with
        | None => Some ([], add_tx (build_tx from to amount tx_empty) lc)
        | Some msg => None
      end
96
97
98
99
100
101
    | Some wc =>
      let tx_body :=
          match msg with
          | None => tx_empty
          | Some msg => tx_call msg
          end in
102
103
      do state <- contract_state lc to;
      let lc := add_tx (build_tx from to amount tx_body) lc in
104
      let ctx := build_ctx from to amount in
105
106
107
      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)
108
109
110
111
112
113
114
    end.

  Definition deploy_contract
             (from : Address)
             (amount : Amount)
             (wc : WeakContract)
             (setup : OakValue)
115
116
117
118
             (lc : LocalChain)
    : option (list Action * LocalChain) :=
    do if amount >? account_balance lc from then None else Some tt;
    let num := (1 + count_contract_deployments lc)%nat in
119
    do contract_addr <- BoundedN.of_nat num;
120
    do match incoming_txs lc contract_addr with
121
122
123
       | _ :: _ => None
       | [] => Some tt
       end;
124
    do match FMap.find contract_addr (lc_contracts lc) with
125
126
127
128
       | Some _ => None
       | None => Some tt
       end;
    let body := tx_deploy (build_contract_deployment (wc_version wc) setup) in
129
    let lc := add_tx (build_tx from contract_addr amount body) lc in
130
    let ctx := build_ctx from contract_addr amount in
131
132
133
134
    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).
135
136
137

  Local Open Scope nat.

138
139
  Definition execute_action (act : Action) (lc : LocalChain) :
    option (list Action * LocalChain) :=
140
141
    match act with
    | build_act from (act_transfer to amount) =>
142
      send_or_call from to amount None lc
143
    | build_act from (act_deploy amount wc setup) =>
144
      deploy_contract from amount wc setup lc
145
    | build_act from (act_call to amount msg) =>
146
      send_or_call from to amount (Some msg) lc
147
148
    end.

149
150
  Fixpoint execute_steps (gas : nat) (stack : list Action) (lc : LocalChain)
    : option LocalChain :=
151
    match gas, stack with
152
    | _, [] => Some lc
153
154
    | 0, _ => None
    | S gas, act :: acts =>
155
156
      do '(next_acts, lc) <- execute_action act lc;
      execute_steps gas (next_acts ++ acts) lc
157
158
    end.

159
160
161
162
  Ltac remember_tx :=
    match goal with
    | [H: context[add_tx ?a _] |- _] => remember a as tx
    end.
163

164
165
166
  Lemma add_tx_equiv tx (lc : LocalChain) (env : Environment) :
    EnvironmentEquiv lc env ->
    EnvironmentEquiv (add_tx tx lc) (Blockchain.add_tx tx env).
167
  Proof.
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
    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.
185
186
  Qed.

187
188
189
190
191
  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).
192
  Proof.
193
194
195
196
197
198
199
200
    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].
201
202
  Qed.

203
204
205
206
207
  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).
208
  Proof.
209
210
211
212
213
214
    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].
215
216
  Qed.

217
218
219
220
221
222
223
  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) ->
    exists tx, ChainStep lc_before act tx lc_after new_acts.
224
  Proof.
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
    intros sent act_eq.
    unfold send_or_call in sent.
    destruct (Z.gtb_spec amount (account_balance lc_before from)); [simpl in *; congruence|].
    destruct (FMap.find to (lc_contracts lc_before)) as [wc|] eqn:to_contract.
    - (* there is a contract at destination, so do call *)
      remember_tx.
      exists tx.
      destruct (contract_state _ _) as [prev_state|] eqn:prev_state_eq;
        cbn in *; try congruence.
      destruct (wc_receive _ _ _ _ _) eqn:receive; cbn in *; try congruence.
      match goal with
      | [p: OakValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
      end.
      (* We record the steps different depending on whether this *)
      (* is a call with a message or without a message *)
      destruct msg as [msg|].
      1: apply (step_call_msg from to amount wc msg prev_state new_state resp_acts);
        try solve [simpl in *; congruence].
      3: apply (step_call_empty from to amount wc prev_state new_state resp_acts);
        try solve [simpl in *; congruence].
      1, 3:
        rewrite <- receive; unfold constructor;
        apply wc_receive_proper; auto;
          symmetry; now apply add_tx_equiv.
      1, 2:
        inversion sent; subst;
        now apply set_contract_state_equiv, add_tx_equiv.
    - (* no contract at destination, so msg should be empty *)
      destruct msg; simpl in *; try congruence.
      assert (new_acts = []) by congruence; subst new_acts.
      remember_tx.
      exists tx.
      apply (step_empty from to amount); auto.
      inversion sent; subst; now apply add_tx_equiv.
259
260
  Qed.

261
262
263
264
  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) ->
    exists tx, ChainStep lc_before act tx lc_after new_acts.
265
  Proof.
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
    intros dep act_eq.
    unfold deploy_contract in dep.
    destruct (Z.gtb_spec amount (account_balance lc_before from)); [cbn in *; congruence|].
    destruct (BoundedN.of_nat _) as [contract_addr|]; [|cbn in *; congruence].
    change (BoundedN AddrSize) with Address in *.
    cbn -[incoming_txs] in dep.
    remember_tx.
    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.
    exists tx.
    assert (new_acts = []) by congruence; subst new_acts.
    apply (step_deploy from contract_addr amount wc setup state);
      try solve [cbn in *; congruence].
    - 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.
286
287
  Qed.

288
289
290
291
292
293
294
  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) ->
    exists tx, ChainStep lc_before act tx lc_after new_acts.
295
  Proof.
296
297
298
299
300
301
    intros exec.
    unfold execute_action in exec.
    destruct act as [from body].
    Hint Resolve send_or_call_step.
    Hint Resolve deploy_contract_step.
    destruct body as [to amount|to amount msg|amount wc setup]; eauto.
302
303
  Qed.

304
305
306
  Lemma execute_steps_trace gas acts lc lc_after :
    execute_steps gas acts lc = Some lc_after ->
    BlockTrace lc acts lc_after [].
307
  Proof.
308
309
310
311
312
313
314
315
316
317
318
319
320
    revert acts lc lc_after.
    induction gas as [|gas IH]; intros acts lc lc_after exec.
    - unfold execute_steps in exec.
      destruct acts as [|x xs]; [|congruence].
      Hint Constructors BlockTrace.
      replace lc_after with lc by congruence; auto.
    - destruct acts as [|x xs]; simpl in *.
      + replace lc_after with lc by congruence; auto.
      + destruct (execute_action x lc) as [[acts lc_after_act]|] eqn:exec_once;
          simpl in *; [|congruence].
        specialize (IH _ _ _ exec); clear exec.
        destruct (execute_action_step _ _ _ _ exec_once) as [tx step]; clear exec_once.
        eauto.
321
  Qed.
322
End ExecuteActions.
323

324
325
326
327
328
329
330
331
332
333
334
Definition lc_initial : LocalChain :=
  {| lc_header :=
       {| block_height := 1;
          slot_number := 1;
          finalized_height := 0; |};
     lc_incoming_txs := FMap.empty;
     lc_outgoing_txs := FMap.empty;
     lc_contract_state := FMap.empty;
     (* zero address has mined two blocks *)
     lc_blocks_baked := FMap.add (BoundedN.of_Z_const AddrSize 0) [0; 1] FMap.empty;
     lc_contracts := FMap.empty; |}.
335

336
337
338
339
340
Record LocalChainBuilder :=
  build_local_chain_builder {
    lcb_lc : LocalChain;
    lcb_trace : ChainTrace lc_initial lcb_lc;
  }.
341

342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
Definition lcb_initial : LocalChainBuilder :=
  {| lcb_lc := lc_initial;
     lcb_trace := ctrace_refl _ |}.

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

373
374
375
Axiom b : False.
Notation todo := (False_rect _ b).

376
377
378
379
(* 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
380
           (lcb : LocalChainBuilder)
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
           (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);
         let lc := lc<|lc_header := new_header|> in
         let add_block o :=
             Some ((block_height new_header) :: (with_default [] o)) in
         let lc := lc<|lc_blocks_baked ::= FMap.partial_alter add_block baker|> in
         execute_steps 10 actions lc in
      _).

  destruct lcopt as [lc|] eqn:exec; [|exact None].
  subst lcopt.
  cbn -[execute_steps] in exec.
  destruct (validate_header _) eqn:validate; [|simpl in *; congruence].
  destruct_units.
  match goal with
  | [H: context[validate_header ?new _] |- _] => remember new as new_header
  end.
  unfold constructor in *.
  cbn -[execute_steps] in exec.

  destruct lcb as [prev_lc_end prev_lcb_trace].
  refine (Some {| lcb_lc := lc; lcb_trace := _ |}).
  match goal with
  | [H: context[execute_steps _ _ ?a] |- _] => remember a as lc_block_start
  end.
  Hint Resolve validate_header_valid execute_steps_trace.
  apply (ctrace_block lc_initial prev_lc_end new_header baker actions lc_block_start lc);
    eauto; clear validate.

  subst lc_block_start.
  simpl.
  apply build_env_equiv; auto.
  apply build_chain_equiv; auto.
  intros addr.
  simpl.
  destruct (address_eqb_spec addr baker) as [addrs_eq|addrs_neq].
  - subst.
    now rewrite FMap.find_partial_alter.
  - now rewrite FMap.find_partial_alter_ne; auto.
432
Defined.
433
434
435
436
437
438
439

Global Instance lcb_chain_builder_type : ChainBuilderType :=
  {| builder_type := LocalChainBuilder;
     builder_initial := lcb_initial;
     builder_env lcb := lcb_lc lcb;
     builder_add_block := add_block;
     builder_trace := lcb_trace; |}.
440
441

End LocalBlockchain.