Blockchain.v 31 KB
Newer Older
1
From Coq Require Import Arith ZArith.
2
From Coq Require Import List.
3
4
5
6
From Coq Require Import Psatz.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
7
8
From SmartContracts Require Import Oak.
From SmartContracts Require Import Monads.
9
From SmartContracts Require Import Extras.
10
From SmartContracts Require Import Automation.
11
From SmartContracts Require Import ChainedList.
12
13
14
15
16
17
18
19
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.

Import ListNotations.

Definition Amount := Z.
Bind Scope Z_scope with Amount.

20
21
Class ChainBase :=
  build_chain_base {
22
23
    Address : Type;
    address_eqb : Address -> Address -> bool;
24
25
    address_eqb_spec :
      forall (a b : Address), Bool.reflect (a = b) (address_eqb a b);
26
27
28
    address_eqdec :> stdpp.base.EqDecision Address;
    address_countable :> countable.Countable Address;
    address_ote :> OakTypeEquivalence Address;
29
    address_is_contract : Address -> bool;
30
31
32
  }.

Global Opaque Address address_eqb address_eqb_spec
33
       address_eqdec address_countable address_ote.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
34

35
Delimit Scope address_scope with address.
36
Bind Scope address_scope with Address.
37
Infix "=?" := address_eqb (at level 70) : address_scope.
38

39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
Lemma address_eq_refl `{ChainBase} x :
  address_eqb x x = true.
Proof. destruct (address_eqb_spec x x); auto; congruence. Qed.

Lemma address_eq_ne `{ChainBase} x y :
  x <> y ->
  address_eqb x y = false.
Proof. destruct (address_eqb_spec x y) as [->|]; tauto. Qed.

Lemma address_eq_sym `{ChainBase} x y :
  address_eqb x y = address_eqb y x.
Proof.
  destruct (address_eqb_spec x y) as [->|].
  - now rewrite address_eq_refl.
  - rewrite address_eq_ne; auto.
Qed.

56
57
58
Global Ltac destruct_address_eq :=
  repeat
    match goal with
59
60
61
62
    | [H: context[address_eqb ?a ?b] |- _] =>
      try rewrite (address_eq_sym b a) in *; destruct (address_eqb_spec a b)
    | [|- context[address_eqb ?a ?b]] =>
      try rewrite (address_eq_sym b a) in *; destruct (address_eqb_spec a b)
63
    end.
64

65
Section Blockchain.
66
Context {BaseTypes : ChainBase}.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
67

68
69
70
71
(* This represents the view of the blockchain that a contract
can access and interact with. *)
Record Chain :=
  build_chain {
72
73
74
    chain_height : nat;
    current_slot : nat;
    finalized_height : nat;
75
    account_balance : Address -> Amount;
76
    contract_state : Address -> option OakValue;
77
78
  }.

79
80
(* Two chains are said to be equivalent if they are extensionally equal.
We will later require that all deployed contracts respect this relation.
81
This equivalence is equality if funext is assumed. *)
82
83
Record ChainEquiv (c1 c2 : Chain) : Prop :=
  build_chain_equiv {
84
85
86
    chain_height_eq : chain_height c1 = chain_height c2;
    current_slot_eq : current_slot c1 = current_slot c2;
    finalized_height_eq : finalized_height c1 = finalized_height c2;
87
    account_balance_eq : forall addr, account_balance c1 addr = account_balance c2 addr;
88
    contract_state_eq : forall addr, contract_state c1 addr = contract_state c2 addr;
89
90
  }.

91
Global Program Instance chain_equiv_equivalence : Equivalence ChainEquiv.
92
93
94
Next Obligation. repeat intro; apply build_chain_equiv; reflexivity. Qed.
Next Obligation. intros x y []; apply build_chain_equiv; congruence. Qed.
Next Obligation. intros x y z [] []; apply build_chain_equiv; congruence. Qed.
95

96
97
98
99
100
101
102
103
104
Global Instance chain_equiv_chain_height :
  Proper (ChainEquiv ==> eq) chain_height.
Proof. repeat intro; auto using chain_height_eq. Qed.
Global Instance chain_equiv_current_slot :
  Proper (ChainEquiv ==> eq) current_slot.
Proof. repeat intro; auto using current_slot_eq. Qed.
Global Instance chain_equiv_finalized_height :
  Proper (ChainEquiv ==> eq) finalized_height.
Proof. repeat intro; auto using finalized_height_eq. Qed.
105
106
107
Global Instance chain_equiv_account_balance_proper :
  Proper (ChainEquiv ==> eq ==> eq) account_balance.
Proof. repeat intro; subst; auto using account_balance_eq. Qed.
108
109
110
111
Global Instance chain_equiv_contract_state_proper :
  Proper (ChainEquiv ==> eq ==> eq) contract_state.
Proof. repeat intro; subst; auto using contract_state_eq. Qed.

112
113
Record ContractCallContext :=
  build_ctx {
114
115
116
117
118
119
    (* Address sending the funds *)
    ctx_from : Address;
    (* Address of the contract being called *)
    ctx_contract_address : Address;
    (* Amount of GTU passed in call *)
    ctx_amount : Amount;
120
  }.
121

122
123
124
(* Operations that a contract can return or that a user can use
to interact with a chain. *)
Inductive ActionBody :=
125
126
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
127
128
  | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
with WeakContract :=
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
     | build_weak_contract
         (init :
            Chain ->
            ContractCallContext ->
            OakValue (* setup *) ->
            option OakValue)
         (* Init respects chain equivalence *)
         (init_proper :
            Proper (ChainEquiv ==> eq ==> eq ==> eq) init)
         (receive :
            Chain ->
            ContractCallContext ->
            OakValue (* state *) ->
            option OakValue (* message *) ->
            option (OakValue * list ActionBody))
         (* And so does receive *)
         (receive_proper :
            Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive).
147
148

Definition wc_init (wc : WeakContract) :=
149
  let (i, _, _, _) := wc in i.
150

151
152
153
154
155
156
157
Global Instance wc_init_proper :
  Proper (eq ==> ChainEquiv ==> eq ==> eq ==> eq) wc_init.
Proof.
  intros wc wc' eq; subst wc'.
  exact (
      match wc return
            Proper (ChainEquiv ==> eq ==> eq ==> eq) (wc_init wc) with
158
      | build_weak_contract _ ip _ _ => ip
159
160
      end).
Qed.
161
162

Definition wc_receive (wc : WeakContract) :=
163
  let (_, _, r, _) := wc in r.
164

165
166
167
168
169
170
171
Global Instance wc_receive_proper :
  Proper (eq ==> ChainEquiv ==> eq ==> eq ==> eq ==> eq) wc_receive.
Proof.
  intros wc wc' eq; subst wc'.
  exact (
      match wc return
            Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) (wc_receive wc) with
172
      | build_weak_contract _ _ _ rp => rp
173
174
      end).
Qed.
175
176
177
178
179
180

Record Action :=
  build_act {
    act_from : Address;
    act_body : ActionBody;
  }.
181

182
(* Represents a strongly-typed contract. This is what user's will primarily
183
184
185
use and interact with when they want deployment. We keep the weak contract
only "internally" for blockchains, while any strongly-typed contract can
be converted to and from *)
186
Record Contract
187
188
189
190
      (Setup Msg State : Type)
      `{OakTypeEquivalence Setup}
      `{OakTypeEquivalence Msg}
      `{OakTypeEquivalence State} :=
191
  build_contract {
192
193
194
    init :
      Chain ->
      ContractCallContext ->
195
196
      Setup ->
      option State;
197
198
    init_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq) init;
199
    receive :
200
201
      Chain ->
      ContractCallContext ->
202
203
204
      State ->
      option Msg ->
      option (State * list ActionBody);
205
206
    receive_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive;
207
208
  }.

209
210
Arguments init {_ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _}.
211
212
Arguments build_contract {_ _ _ _ _ _}.

213
Program Definition contract_to_weak_contract
214
215
216
217
218
          {Setup Msg State : Type}
          `{OakTypeEquivalence Setup}
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
          (c : Contract Setup Msg State) : WeakContract :=
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
      let weak_init chain ctx oak_setup :=
          do setup <- deserialize oak_setup;
          do state <- c.(init) chain ctx setup;
          Some (serialize state) in
      let weak_recv chain ctx oak_state oak_msg_opt :=
          do state <- deserialize oak_state;
          match oak_msg_opt with
          | Some oak_msg =>
            do msg <- deserialize oak_msg;
            do '(new_state, acts) <- c.(receive) chain ctx state (Some msg);
            Some (serialize new_state, acts)
          | None =>
            do '(new_state, acts) <- c.(receive) chain ctx state None;
            Some (serialize new_state, acts)
          end in
234
      build_weak_contract weak_init _ weak_recv _.
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
Next Obligation.
  intros.
  intros c1 c2 eq_chains ctx1 ctx2 eq_ctx setup1 setup2 eq_setups.
  subst ctx2 setup2.
  subst weak_init.
  simpl.
  destruct (deserialize setup1); auto; simpl.
  now rewrite init_proper.
Qed.
Next Obligation.
  intros.
  intros c1 c2 eq_chains ctx1 ctx2 eq_ctx state1 state2 eq_states msg1 msg2 eq_msgs.
  subst ctx2 state2 msg2.
  subst weak_recv.
  simpl.
  destruct (deserialize state1); auto; simpl.
  destruct msg1.
  + destruct (deserialize o); auto; simpl.
    now rewrite receive_proper.
  + now rewrite receive_proper.
Qed.
256

257
258
Coercion contract_to_weak_contract : Contract >-> WeakContract.

259
(* Deploy a strongly typed contract with some amount and setup *)
260
Definition create_deployment
261
262
263
264
          {Setup Msg State : Type}
          `{OakTypeEquivalence Setup}
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
265
          (amount : Amount)
266
267
          (contract : Contract Setup Msg State)
          (setup : Setup) : ActionBody :=
268
269
  act_deploy amount contract (serialize setup).

270
(* The contract interface is the main mechanism allowing a deployed
271
contract to interact with another deployed contract. This hides
272
the ugly details of everything being OakValue away from contracts. *)
273
Record ContractInterface {Msg State : Type} :=
274
  build_contract_interface {
275
    (* The address of the contract being interfaced with *)
276
    contract_address : Address;
277
    (* Obtain the state at some point of time *)
278
    get_state : Chain -> option State;
279
280
    (* Make an action sending money and optionally a message to the contract *)
    send : Amount -> option Msg -> ActionBody;
281
282
  }.

283
Arguments ContractInterface _ _ : clear implicits.
284

285
Definition get_contract_interface
286
287
          (chain : Chain)
          (addr : Address)
288
          (Msg State : Type)
289
290
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
291
  : option (ContractInterface Msg State) :=
292
  let ifc_get_state chain := contract_state chain addr >>= deserialize in
293
294
295
296
297
298
  let ifc_send amount msg :=
      match msg with
      | None => act_transfer addr amount
      | Some msg => act_call addr amount (serialize msg)
      end in
  Some {| contract_address := addr; get_state := ifc_get_state; send := ifc_send; |}.
299

300
301
Section Semantics.
Instance chain_settable : Settable _ :=
302
303
  settable! build_chain <chain_height; current_slot; finalized_height;
                         account_balance; contract_state>.
304
305
306
307
308

Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amount) :
  Address -> Amount :=
  fun a => if (a =? addr)%address
           then (amount + map a)%Z
309
310
311
312
313
           else map a.

Definition set_chain_contract_state
           (addr : Address) (state : OakValue) (map : Address -> option OakValue)
  : Address -> option OakValue :=
314
  fun a => if (a =? addr)%address
315
316
317
318
319
320
321
           then Some state
           else map a.

Record Environment :=
  build_env {
    env_chain :> Chain;
    env_contracts : Address -> option WeakContract;
322
323
  }.

324
(* Furthermore we define extensional equality for such environments. *)
325
326
Record EnvironmentEquiv (e1 e2 : Environment) : Prop :=
  build_env_equiv {
327
    chain_equiv : ChainEquiv e1 e2;
328
    contracts_eq : forall a, env_contracts e1 a = env_contracts e2 a;
329
330
  }.

331
332
333
334
335
336
337
338
339
340
341
342
Global Program Instance environment_equiv_equivalence : Equivalence EnvironmentEquiv.
Next Obligation.
  intros x; apply build_env_equiv; reflexivity.
Qed.
Next Obligation.
  intros x y []; apply build_env_equiv; now symmetry.
Qed.
Next Obligation.
  intros x y z [] []; apply build_env_equiv; try congruence.
  apply (@transitivity Chain _ _ _ y _); auto.
Qed.

343
Global Instance environment_equiv_contracts_proper :
344
345
346
  Proper (EnvironmentEquiv ==> eq ==> eq) env_contracts.
Proof. repeat intro; subst; apply contracts_eq; assumption. Qed.

347
348
349
350
Global Instance environment_equiv_chain_equiv_proper :
  Proper (EnvironmentEquiv ==> ChainEquiv) env_chain.
Proof. repeat intro; apply chain_equiv; assumption. Qed.

351
352
353
Instance env_settable : Settable _ :=
  settable! build_env <env_chain; env_contracts>.

354
355
356
Definition transfer_balance (from to : Address) (amount : Amount) (env : Environment) :=
  env<|env_chain; account_balance ::= add_balance to amount|>
     <|env_chain; account_balance ::= add_balance from (-amount)|>.
357

358
Definition add_contract (addr : Address) (contract : WeakContract) (env : Environment)
359
  : Environment :=
360
  env<|env_contracts ::=
361
    fun f a =>
362
      if (a =? addr)%address
363
      then Some contract
364
      else f a|>.
365

366
367
Definition set_contract_state (addr : Address) (state : OakValue) (env : Environment) :=
  env<|env_chain; contract_state ::= set_chain_contract_state addr state|>.
368

369
370
371
372
373
Ltac rewrite_environment_equiv :=
  match goal with
  | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
  end.

374
375
376
377
378
Ltac solve_proper :=
  apply build_env_equiv;
  [apply build_chain_equiv|];
  cbn;
  repeat intro;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
379
  repeat rewrite_environment_equiv;
380
381
  auto.

382
383
Global Instance transfer_balance_proper :
  Proper (eq ==> eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) transfer_balance.
384
385
Proof.
  repeat intro; subst.
386
  unfold transfer_balance, add_balance.
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
  solve_proper.
Qed.

Global Instance add_contract_proper :
  Proper (eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) add_contract.
Proof.
  repeat intro; subst.
  unfold add_contract.
  solve_proper.
Qed.

Global Instance set_contract_state_proper :
  Proper (eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) set_contract_state.
Proof.
  repeat intro; subst.
402
  unfold set_contract_state, set_chain_contract_state.
403
404
405
  solve_proper.
Qed.

406
Local Open Scope Z.
407
408
409
410
411
412
(* Next we define how actions are executed. It specifies how an action
changes an environment and which external actions to execute after it.
Note that there can be multiple ways to execute an action. For example, if
the action says to deploy a contract, the implementation is responsible for
selecting which address the new contract should get. *)
Inductive ActionEvaluation :
413
414
  Environment -> Action ->
  Environment -> list Action -> Type :=
415
  | eval_transfer :
416
417
418
419
420
421
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             (from to : Address)
             (amount : Amount),
        amount <= account_balance pre from ->
422
        address_is_contract to = false ->
423
        act = build_act from (act_transfer to amount) ->
424
425
426
        EnvironmentEquiv
          new_env
          (transfer_balance from to amount pre) ->
427
428
        ActionEvaluation pre act new_env []
  | eval_deploy :
429
430
431
432
433
434
435
436
437
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             (from to : Address)
             (amount : Amount)
             (wc : WeakContract)
             (setup : OakValue)
             (state : OakValue),
      amount <= account_balance pre from ->
438
      address_is_contract to = true ->
439
      env_contracts pre to = None ->
440
      act = build_act from (act_deploy amount wc setup) ->
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
441
442
      wc_init
        wc
443
        (transfer_balance from to amount pre)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
444
445
        (build_ctx from to amount)
        setup = Some state ->
446
447
      EnvironmentEquiv
        new_env
448
        (set_contract_state to state (add_contract to wc (transfer_balance from to amount pre))) ->
449
450
      ActionEvaluation pre act new_env []
  | eval_call :
451
452
453
454
455
456
457
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             {new_acts : list Action}
             (from to : Address)
             (amount : Amount)
             (wc : WeakContract)
458
             (msg : option OakValue)
459
460
461
462
463
464
             (prev_state : OakValue)
             (new_state : OakValue)
             (resp_acts : list ActionBody),
      amount <= account_balance pre from ->
      env_contracts pre to = Some wc ->
      contract_state pre to = Some prev_state ->
465
466
467
468
      act = build_act from (match msg with
                            | None => act_transfer to amount
                            | Some msg => act_call to amount msg
                            end) ->
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
469
470
      wc_receive
        wc
471
        (transfer_balance from to amount pre)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
472
473
        (build_ctx from to amount)
        prev_state
474
        msg = Some (new_state, resp_acts) ->
475
476
477
      new_acts = map (build_act to) resp_acts ->
      EnvironmentEquiv
        new_env
478
        (set_contract_state to new_state (transfer_balance from to amount pre)) ->
479
      ActionEvaluation pre act new_env new_acts.
480
481
482
483

Section Accessors.
Context {pre : Environment} {act : Action}
        {post : Environment} {new_acts : list Action}
484
        (eval : ActionEvaluation pre act post new_acts).
485

486
487
488
489
490
Definition eval_from : Address :=
  match eval with
  | eval_transfer from _ _ _ _ _ _
  | eval_deploy from _ _ _ _ _ _ _ _ _ _ _
  | eval_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
491
492
  end.

493
494
495
496
497
Definition eval_to : Address :=
  match eval with
  | eval_transfer _ to _ _ _ _ _
  | eval_deploy _ to _ _ _ _ _ _ _ _ _ _
  | eval_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ => to
498
499
  end.

500
501
502
503
504
Definition eval_amount : Amount :=
  match eval with
  | eval_transfer _ _ amount _ _ _ _
  | eval_deploy _ _ amount _ _ _ _ _ _ _ _ _
  | eval_call _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ => amount
505
506
  end.
End Accessors.
507

508
Section Theories.
509
Context {pre : Environment} {act : Action}
510
        {post : Environment} {new_acts : list Action}
511
        (eval : ActionEvaluation pre act post new_acts).
512
513

Lemma account_balance_post (addr : Address) :
514
  account_balance post addr =
515
  account_balance pre addr
516
517
  + (if (addr =? eval_to eval)%address then eval_amount eval else 0)
  - (if (addr =? eval_from eval)%address then eval_amount eval else 0).
518
Proof.
519
  destruct eval; cbn; rewrite_environment_equiv; cbn;
520
    unfold add_balance; destruct_address_eq; lia.
521
522
523
Qed.

Lemma account_balance_post_to :
524
525
526
  eval_from eval <> eval_to eval ->
  account_balance post (eval_to eval) =
  account_balance pre (eval_to eval) + eval_amount eval.
527
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
528
  intros neq.
529
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
530
531
  rewrite address_eq_refl, address_eq_ne by auto.
  lia.
532
533
534
Qed.

Lemma account_balance_post_from :
535
536
537
  eval_from eval <> eval_to eval ->
  account_balance post (eval_from eval) =
  account_balance pre (eval_from eval) - eval_amount eval.
538
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
539
  intros neq.
540
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
541
542
  rewrite address_eq_refl, address_eq_ne by auto.
  lia.
543
544
545
Qed.

Lemma account_balance_post_irrelevant (addr : Address) :
546
547
  addr <> eval_from eval ->
  addr <> eval_to eval ->
548
549
  account_balance post addr = account_balance pre addr.
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
550
  intros neq_from neq_to.
551
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
552
553
  repeat rewrite address_eq_ne by auto.
  lia.
554
555
Qed.

556
557
558
559
560
561
562
Lemma chain_height_post_action : chain_height post = chain_height pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.

Lemma current_slot_post_action : current_slot post = current_slot pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.

Lemma finalized_height_post_action : finalized_height post = finalized_height pre.
563
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.
564
565
566
567
568
569

Lemma contracts_post_pre_none contract :
  env_contracts post contract = None ->
  env_contracts pre contract = None.
Proof.
  intros H.
570
  destruct eval; rewrite_environment_equiv; auto.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
571
  cbn in *.
572
573
  destruct_address_eq; congruence.
Qed.
574
End Theories.
575

576
Section Trace.
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593

Record BlockHeader :=
  build_block_Header {
    block_height : nat;
    block_slot : nat;
    block_finalized_height : nat;
    block_reward : Amount;
    block_creator : Address;
  }.

Definition add_new_block_to_env
           (header : BlockHeader) (env : Environment) : Environment :=
  env<|env_chain; chain_height := block_height header|>
     <|env_chain; current_slot := block_slot header|>
     <|env_chain; finalized_height := block_finalized_height header|>
     <|env_chain; account_balance ::=
         add_balance (block_creator header) (block_reward header)|>.
594

595
596
(* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *)
597
Local Open Scope nat.
598
Definition act_is_from_account (act : Action) : Prop :=
599
600
  address_is_contract (act_from act) = false.

601
602
603
604
605
606
607
608
609
610
611
Record IsValidNextBlock (header : BlockHeader) (chain : Chain) : Prop :=
  build_is_valid_next_block {
    valid_height : block_height header = S (chain_height chain);
    valid_slot : block_slot header > current_slot chain;
    valid_finalized_height :
      block_finalized_height header >= finalized_height chain /\
      block_finalized_height header < block_height header;
    valid_creator : address_is_contract (block_creator header) = false;
    valid_reward : (block_reward header >= 0)%Z;
  }.

612
613
614
615
616
Record ChainState :=
  build_chain_state {
    chain_state_env :> Environment;
    chain_state_queue : list Action;
  }.
617

618
619
620
Global Instance chain_state_settable : Settable _ :=
  settable! build_chain_state <chain_state_env; chain_state_queue>.

621
622
Inductive ChainStep : ChainState -> ChainState -> Type :=
| step_block :
623
624
    forall {prev next : ChainState}
           (header : BlockHeader),
625
      chain_state_queue prev = [] ->
626
627
      IsValidNextBlock header prev ->
      Forall act_is_from_account (chain_state_queue next) ->
628
629
      EnvironmentEquiv
        next
630
        (add_new_block_to_env header prev) ->
631
632
      ChainStep prev next
| step_action :
633
634
635
636
    forall {prev next : ChainState}
           (act : Action)
           (acts : list Action)
           (new_acts : list Action),
637
      chain_state_queue prev = act :: acts ->
638
      ActionEvaluation prev act next new_acts ->
639
      chain_state_queue next = new_acts ++ acts ->
640
641
      ChainStep prev next
| step_permute :
642
643
644
645
    forall {prev next : ChainState},
      chain_state_env prev = chain_state_env next ->
      Permutation (chain_state_queue prev) (chain_state_queue next) ->
      ChainStep prev next.
646
647
648
649

Definition empty_state : ChainState :=
  {| chain_state_env :=
       {| env_chain :=
650
651
652
            {| chain_height := 0;
               current_slot := 0;
               finalized_height := 0;
653
               account_balance a := 0%Z;
654
655
656
               contract_state a := None; |};
          env_contracts a := None; |};
     chain_state_queue := [] |}.
657

658
659
660
(* The ChainTrace captures that there is a valid execution where,
starting from one environment and queue of actions, we end up in a
different environment and queue of actions. *)
661
Definition ChainTrace := ChainedList ChainState ChainStep.
662

663
664
665
666
(* Additionally, a state is reachable if there is a trace ending in this trace. *)
Definition reachable (state : ChainState) : Prop :=
  inhabited (ChainTrace empty_state state).

667
668
669
(* We define a transaction as a "fully specified" action, recording all info. For
example, a transaction contains the contract address that was created when a contract
is deployed. This is more about bridging the gap between our definitions and what
670
671
a normal blockchain is. Each evaluation of an action in the blockchain corresponds to
a transaction, so we can go from a trace to a list of transactions. *)
672
673
674
675
676
677
678
679
680
681
682
683
684
Inductive TxBody :=
  | tx_empty
  | tx_deploy (wc : WeakContract) (setup : OakValue)
  | tx_call (msg : option OakValue).

Record Tx :=
  build_tx {
      tx_from : Address;
      tx_to : Address;
      tx_amount : Amount;
      tx_body : TxBody;
  }.

685
Definition eval_tx {pre : Environment} {act : Action}
686
                   {post : Environment} {new_acts : list Action}
687
                   (step : ActionEvaluation pre act post new_acts) : Tx :=
688
  match step with
689
  | eval_transfer from to amount _ _ _ _ =>
690
    build_tx from to amount tx_empty
691
  | eval_deploy from to amount wc setup _ _ _ _ _ _ _ =>
692
    build_tx from to amount (tx_deploy wc setup)
693
  | eval_call from to amount _ msg _ _ _ _ _ _ _ _ _ _ =>
694
695
696
697
698
    build_tx from to amount (tx_call msg)
  end.

Fixpoint trace_txs {from to : ChainState} (trace : ChainTrace from to) : list Tx :=
  match trace with
699
700
  | snoc trace' step =>
    match step with
701
    | step_action _ _ _ _ eval _ => eval_tx eval :: trace_txs trace'
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
    | _ => trace_txs trace'
    end
  | _ => []
  end.

Definition incoming_txs
           {from to : ChainState}
           (trace : ChainTrace from to)
           (addr : Address) : list Tx :=
  filter (fun tx => (tx_to tx =? addr)%address) (trace_txs trace).

Definition outgoing_txs
           {from to : ChainState}
           (trace : ChainTrace from to)
           (addr : Address) : list Tx :=
  filter (fun tx => (tx_from tx =? addr)%address) (trace_txs trace).

719
720
Fixpoint trace_blocks {from to : ChainState}
         (trace : ChainTrace from to) : list BlockHeader :=
721
  match trace with
722
723
  | snoc trace' step =>
    match step with
724
725
726
    | step_block header _ _ _ _ =>
      header :: trace_blocks trace'
    | _ => trace_blocks trace'
727
728
729
730
    end
  | clnil => []
  end.

731
732
733
734
735
736
Definition created_blocks
           {from to : ChainState} (trace : ChainTrace from to)
           (creator : Address) : list BlockHeader :=
  filter (fun b => (block_creator b =? creator)%address)
         (trace_blocks trace).

737
Section Theories.
738
Ltac destruct_chain_step :=
739
  match goal with
740
741
  | [step: ChainStep _ _ |- _] =>
    destruct step as
742
743
744
        [prev next header queue_prev valid_header acts_from_accs env_eq|
         prev next act acts new_acts queue_prev eval queue_new|
         prev next prev_next perm]
745
746
  end.

747
Ltac destruct_action_eval :=
748
  match goal with
749
  | [eval: ActionEvaluation _ _ _ _ |- _] => destruct eval
750
751
  end.

752
753
Lemma contract_addr_format {to} (addr : Address) (wc : WeakContract) :
  reachable to ->
754
755
756
  env_contracts to addr = Some wc ->
  address_is_contract addr = true.
Proof.
757
  intros [trace] contract_at_addr.
758
759
760
  remember empty_state eqn:eq.
  induction trace; rewrite eq in *; clear eq.
  - cbn in *; congruence.
761
  - destruct_chain_step.
762
    + rewrite_environment_equiv; cbn in *; auto.
763
    + destruct_action_eval; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
764
    + intuition.
765
Qed.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
766

767
768
769
770
771
772
773
774
775
776
777
778
779
780
Lemma new_acts_no_out_queue addr1 addr2 new_acts resp_acts :
  addr1 <> addr2 ->
  new_acts = map (build_act addr2) resp_acts ->
  Forall (fun a => (act_from a =? addr1)%address = false) new_acts.
Proof.
  intros neq ?; subst.
  induction resp_acts; cbn; auto.
  constructor; destruct_address_eq; cbn in *; congruence.
Qed.

Local Open Scope address.
(* This next lemma shows that any for a full chain trace,
the ending state will not have any queued actions from
undeployed contracts. *)
781
Lemma undeployed_contract_no_out_queue contract state :
782
  reachable state ->
783
784
785
786
787
788
789
790
  address_is_contract contract = true ->
  env_contracts state contract = None ->
  Forall (fun act => (act_from act =? contract) = false) (chain_state_queue state).
Proof.
  intros [trace] is_contract.
  remember empty_state eqn:eq.
  induction trace;
    intros undeployed; rewrite eq in *; clear eq; cbn; auto.
791
  destruct_chain_step; [|destruct_action_eval|];
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
    try rewrite_environment_equiv;
    repeat
      match goal with
      | [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
      end;
    cbn in *.
  - (* New block *)
    match goal with
    | [H: Forall _ _ |- _] => induction H
    end; constructor; auto.
    destruct_address_eq; congruence.
  - (* Transfer step, just use IH *)
    eapply list.Forall_cons; eauto.
  - (* Deploy step. First show that it is not to contract and then use IH. *)
    destruct_address_eq; try congruence.
    eapply list.Forall_cons; eauto.
  - (* Call. Show that it holds for new actions as it is from *)
    (* another contract, and use IH for remaining. *)
    apply list.Forall_app.
    assert (contract <> to) by congruence.
    split; [eapply new_acts_no_out_queue|eapply list.Forall_cons]; eauto.
  - (* Permutation *)
    subst.
    specialize_hypotheses.
    match goal with
    | [prev_eq_new: _ = _, perm: Permutation _ _ |- _] =>
      now rewrite prev_eq_new in *; rewrite <- perm; auto
    end.
Qed.

(* With this lemma proven, we can show that the (perhaps seemingly stronger)
fact, that an undeployed contract has no outgoing txs, holds. *)
824
825
Lemma undeployed_contract_no_out_txs
      contract state (trace : ChainTrace empty_state state) :
826
827
  address_is_contract contract = true ->
  env_contracts state contract = None ->
828
  outgoing_txs trace contract = [].
829
Proof.
830
  intros is_contract undeployed.
831
  remember empty_state eqn:eq.
832
  induction trace; cbn; auto.
833
  destruct_chain_step.
834
835
836
837
  - (* New block *)
    rewrite_environment_equiv; auto.
  - (* In these steps we will use that the queue did not contain txs to the contract. *)
    Hint Resolve contracts_post_pre_none : core.
838
    Hint Unfold reachable : core.
839
840
    subst.
    cbn.
841
842
843
844
    pose proof
         (undeployed_contract_no_out_queue
            contract prev
            ltac:(auto) ltac:(auto) ltac:(eauto)) as Hqueue.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
845
846
847
848
849
    repeat
      match goal with
      | [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
      end.
    inversion_clear Hqueue.
850
    destruct_action_eval; rewrite_environment_equiv;
851
852
853
854
855
856
857
858
859
      subst;
      cbn in *;
      destruct_address_eq;
      subst; try tauto; congruence.
  - match goal with
    | [H: _ = _ |- _] => rewrite H in *; auto
    end.
Qed.

860
861
Lemma undeployed_contract_no_in_txs
      contract state (trace : ChainTrace empty_state state) :
862
863
  address_is_contract contract = true ->
  env_contracts state contract = None ->
864
  incoming_txs trace contract = [].
865
Proof.
866
  intros is_contract undeployed.
867
  remember empty_state eqn:eq.
868
  induction trace; cbn; auto.
869
  destruct_chain_step.
870
871
  - (* New block *)
    rewrite_environment_equiv; auto.
872
  - destruct_action_eval; rewrite_environment_equiv;
873
874
875
876
877
878
      cbn in *;
      destruct_address_eq; auto; subst; congruence.
  - match goal with
    | [H: _ = _ |- _] => rewrite H in *; auto
    end.
Qed.
879

880
881
882
883
Local Open Scope Z.
Lemma account_balance_trace state (trace : ChainTrace empty_state state) addr :
  account_balance state addr =
  sumZ tx_amount (incoming_txs trace addr) +
884
  sumZ block_reward (created_blocks trace addr) -
885
886
887
888
  sumZ tx_amount (outgoing_txs trace addr).
Proof.
  unfold incoming_txs, outgoing_txs.
  remember empty_state as from_state.
889
  induction trace; [|destruct_chain_step].
890
891
892
893
  - subst. cbn. lia.
  - (* Block *)
    rewrite_environment_equiv.
    cbn.
894
    fold (created_blocks trace addr).
895
896
897
898
899
    unfold add_balance.
    rewrite IHtrace by auto.
    destruct_address_eq; subst; cbn; lia.
  - (* Step *)
    cbn.
900
    destruct_action_eval; cbn; rewrite_environment_equiv; cbn.
901
    all: fold (created_blocks trace addr); unfold add_balance; rewrite IHtrace by auto.
902
903
    all: destruct_address_eq; cbn; lia.
  - cbn.
904
    rewrite <- prev_next.
905
906
907
    auto.
Qed.

908
End Theories.
909
End Trace.
910
911
912
913
914
915
916
917
918
919
920
End Semantics.

Class ChainBuilderType :=
  build_builder {
    builder_type : Type;

    builder_initial : builder_type;

    builder_env : builder_type -> Environment;

    builder_add_block
921
922
923
      (builder : builder_type)
      (header : BlockHeader)
      (actions : list Action) :
924
925
      option builder_type;

926
927
    builder_trace (builder : builder_type) :
      ChainTrace empty_state (build_chain_state (builder_env builder) []);
928
929
  }.

930
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
931
Global Coercion builder_env : builder_type >-> Environment.
932
End Blockchain.
933

934
935
936
Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}.
937
Arguments ContractInterface {_} _ _.
938
Arguments build_contract_interface {_ _ _ _}.
939

940
Ltac destruct_chain_step :=
941
  match goal with
942
943
  | [step: ChainStep _ _ |- _] =>
    destruct step as
944
945
946
        [prev next header queue_prev valid_header acts_from_accs env_eq|
         prev next act acts new_acts queue_prev eval queue_new|
         prev next prev_next perm]
947
948
  end.

949
Ltac destruct_action_eval :=
950
  match goal with
951
  | [eval: ActionEvaluation _ _ _ _ |- _] => destruct eval
952
953
954
955
956
957
  end.

Ltac rewrite_environment_equiv :=
  match goal with
  | [eq: EnvironmentEquiv _ _ |- _] => rewrite eq in *
  end.