Blockchain.v 30 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
33
34
    compute_block_reward : nat -> Amount;
  }.

Global Opaque Address address_eqb address_eqb_spec
       address_eqdec address_countable
35
       address_ote compute_block_reward.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
36

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

41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
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.

58
59
60
Global Ltac destruct_address_eq :=
  repeat
    match goal with
61
62
63
64
    | [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)
65
    end.
66

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

70
71
Record BlockHeader :=
  build_block_header {
72
73
74
    block_height : nat;
    slot_number : nat;
    finalized_height : nat;
75
76
  }.

77
78
79
80
(* This represents the view of the blockchain that a contract
can access and interact with. *)
Record Chain :=
  build_chain {
81
    block_header : BlockHeader;
82
    account_balance : Address -> Amount;
83
    contract_state : Address -> option OakValue;
84
85
  }.

86
87
(* Two chains are said to be equivalent if they are extensionally equal.
We will later require that all deployed contracts respect this relation.
88
This equivalence is equality if funext is assumed. *)
89
90
91
Record ChainEquiv (c1 c2 : Chain) : Prop :=
  build_chain_equiv {
    header_eq : block_header c1 = block_header c2;
92
    account_balance_eq : forall addr, account_balance c1 addr = account_balance c2 addr;
93
    contract_state_eq : forall addr, contract_state c1 addr = contract_state c2 addr;
94
95
  }.

96
Global Program Instance chain_equiv_equivalence : Equivalence ChainEquiv.
97
98
99
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.
100
101
102
103

Global Instance chain_equiv_header_proper :
  Proper (ChainEquiv ==> eq) block_header.
Proof. repeat intro; auto using header_eq. Qed.
104
105
106
Global Instance chain_equiv_account_balance_proper :
  Proper (ChainEquiv ==> eq ==> eq) account_balance.
Proof. repeat intro; subst; auto using account_balance_eq. Qed.
107
108
109
110
Global Instance chain_equiv_contract_state_proper :
  Proper (ChainEquiv ==> eq ==> eq) contract_state.
Proof. repeat intro; subst; auto using contract_state_eq. Qed.

111
112
Record ContractCallContext :=
  build_ctx {
113
114
115
116
117
118
    (* 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;
119
  }.
120

121
122
123
(* Operations that a contract can return or that a user can use
to interact with a chain. *)
Inductive ActionBody :=
124
125
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
126
127
  | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
with WeakContract :=
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
     | 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).
146
147

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

150
151
152
153
154
155
156
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
157
      | build_weak_contract _ ip _ _ => ip
158
159
      end).
Qed.
160
161

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

164
165
166
167
168
169
170
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
171
      | build_weak_contract _ _ _ rp => rp
172
173
      end).
Qed.
174
175
176
177
178
179

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

181
(* Represents a strongly-typed contract. This is what user's will primarily
182
183
184
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 *)
185
Record Contract
186
187
188
189
      (Setup Msg State : Type)
      `{OakTypeEquivalence Setup}
      `{OakTypeEquivalence Msg}
      `{OakTypeEquivalence State} :=
190
  build_contract {
191
192
193
    init :
      Chain ->
      ContractCallContext ->
194
195
      Setup ->
      option State;
196
197
    init_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq) init;
198
    receive :
199
200
      Chain ->
      ContractCallContext ->
201
202
203
      State ->
      option Msg ->
      option (State * list ActionBody);
204
205
    receive_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive;
206
207
  }.

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

212
Program Definition contract_to_weak_contract
213
214
215
216
217
          {Setup Msg State : Type}
          `{OakTypeEquivalence Setup}
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
          (c : Contract Setup Msg State) : WeakContract :=
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
      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
233
      build_weak_contract weak_init _ weak_recv _.
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
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.
255

256
257
Coercion contract_to_weak_contract : Contract >-> WeakContract.

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

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

282
Arguments ContractInterface _ _ : clear implicits.
283

284
Definition get_contract_interface
285
286
          (chain : Chain)
          (addr : Address)
287
          (Msg State : Type)
288
289
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
290
  : option (ContractInterface Msg State) :=
291
  let ifc_get_state chain := contract_state chain addr >>= deserialize in
292
293
294
295
296
297
  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; |}.
298

299
300
Section Semantics.
Instance chain_settable : Settable _ :=
301
302
303
304
305
306
  settable! build_chain <block_header; account_balance; contract_state>.

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

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

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

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

329
330
331
332
333
334
335
336
337
338
339
340
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.

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

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

349
350
351
352
353
354
355
356
357
Instance env_settable : Settable _ :=
  settable! build_env <env_chain; env_contracts>.

Definition update_chain (upd : Chain -> Chain) (e : Environment)
  : Environment :=
  let chain := env_chain e in
  let chain := upd chain in
  e <|env_chain := chain|>.

358
359
360
Definition transfer_balance (from to : Address) (amount : Amount) :=
  update_chain (fun c => c<|account_balance ::= add_balance to amount|>
                          <|account_balance ::= add_balance from (-amount)|>).
361
362
363
364
365

Definition add_contract (addr : Address) (contract : WeakContract) (e : Environment)
  : Environment :=
  e <| env_contracts ::=
    fun f a =>
366
      if (a =? addr)%address
367
368
369
370
371
372
373
      then Some contract
      else f a |>.

Definition set_contract_state (addr : Address) (state : OakValue) :=
  update_chain
    (fun c => c <|contract_state ::= set_chain_contract_state addr state|>).

374
375
376
377
378
Ltac rewrite_environment_equiv :=
  match goal with
  | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
  end.

379
380
381
382
383
Ltac solve_proper :=
  apply build_env_equiv;
  [apply build_chain_equiv|];
  cbn;
  repeat intro;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
384
  repeat rewrite_environment_equiv;
385
386
  auto.

387
388
Global Instance transfer_balance_proper :
  Proper (eq ==> eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) transfer_balance.
389
390
Proof.
  repeat intro; subst.
391
  unfold transfer_balance, add_balance.
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
  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.
  unfold set_contract_state, update_chain, set_chain_contract_state.
  solve_proper.
Qed.

411
Local Open Scope Z.
412
413
414
415
416
417
(* 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 :
418
419
  Environment -> Action ->
  Environment -> list Action -> Type :=
420
  | eval_transfer :
421
422
423
424
425
426
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             (from to : Address)
             (amount : Amount),
        amount <= account_balance pre from ->
427
        address_is_contract to = false ->
428
        act = build_act from (act_transfer to amount) ->
429
        EnvironmentEquiv new_env (transfer_balance from to amount pre) ->
430
431
        ActionEvaluation pre act new_env []
  | eval_deploy :
432
433
434
435
436
437
438
439
440
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             (from to : Address)
             (amount : Amount)
             (wc : WeakContract)
             (setup : OakValue)
             (state : OakValue),
      amount <= account_balance pre from ->
441
      address_is_contract to = true ->
442
      env_contracts pre to = None ->
443
      act = build_act from (act_deploy amount wc setup) ->
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
444
445
      wc_init
        wc
446
        (transfer_balance from to amount pre)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
447
448
        (build_ctx from to amount)
        setup = Some state ->
449
450
      EnvironmentEquiv
        new_env
451
        (set_contract_state to state (add_contract to wc (transfer_balance from to amount pre))) ->
452
453
      ActionEvaluation pre act new_env []
  | eval_call :
454
455
456
457
458
459
460
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             {new_acts : list Action}
             (from to : Address)
             (amount : Amount)
             (wc : WeakContract)
461
             (msg : option OakValue)
462
463
464
465
466
467
             (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 ->
468
469
470
471
      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
472
473
      wc_receive
        wc
474
        (transfer_balance from to amount pre)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
475
476
        (build_ctx from to amount)
        prev_state
477
        msg = Some (new_state, resp_acts) ->
478
479
480
      new_acts = map (build_act to) resp_acts ->
      EnvironmentEquiv
        new_env
481
        (set_contract_state to new_state (transfer_balance from to amount pre)) ->
482
      ActionEvaluation pre act new_env new_acts.
483
484
485
486

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

489
490
491
492
493
Definition eval_from : Address :=
  match eval with
  | eval_transfer from _ _ _ _ _ _
  | eval_deploy from _ _ _ _ _ _ _ _ _ _ _
  | eval_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
494
495
  end.

496
497
498
499
500
Definition eval_to : Address :=
  match eval with
  | eval_transfer _ to _ _ _ _ _
  | eval_deploy _ to _ _ _ _ _ _ _ _ _ _
  | eval_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ => to
501
502
  end.

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

511
Section Theories.
512
Context {pre : Environment} {act : Action}
513
        {post : Environment} {new_acts : list Action}
514
        (eval : ActionEvaluation pre act post new_acts).
515
516

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

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

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

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

559
560
Lemma block_header_post_action : block_header post = block_header pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.
561
562
563
564
565
566

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

573
Section Trace.
574
Definition add_new_block
575
576
577
          (header : BlockHeader)
          (baker : Address)
          (env : Environment) : Environment :=
578
579
580
581
582
  let chain := env_chain env in
  let chain := chain<|block_header := header|> in
  let reward := compute_block_reward (block_height header) in
  let chain := chain<|account_balance ::= add_balance baker reward|> in
  env<|env_chain := chain|>.
583

584
585
(* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *)
586
Local Open Scope nat.
587
588
589
590
591
592
Definition IsValidNextBlock (new old : BlockHeader) : Prop :=
  block_height new = S (block_height old) /\
  slot_number new > slot_number old /\
  finalized_height new >= finalized_height old /\
  finalized_height new < block_height new.

593
594
595
Definition ActIsFromAccount (act : Action) : Prop :=
  address_is_contract (act_from act) = false.

596
597
598
599
600
Record ChainState :=
  build_chain_state {
    chain_state_env :> Environment;
    chain_state_queue : list Action;
  }.
601

602
603
Inductive ChainStep : ChainState -> ChainState -> Type :=
| step_block :
604
605
606
607
608
609
610
611
612
    forall {prev : ChainState}
           {header : BlockHeader}
           {baker : Address}
           {next : ChainState},
      chain_state_queue prev = [] ->
      IsValidNextBlock header (block_header prev) ->
      Forall ActIsFromAccount (chain_state_queue next) ->
      EnvironmentEquiv
        next
613
        (add_new_block header baker prev) ->
614
615
      ChainStep prev next
| step_action :
616
617
618
619
620
621
    forall {prev : ChainState}
           {act : Action}
           {acts : list Action}
           {next : ChainState}
           {new_acts : list Action},
      chain_state_queue prev = act :: acts ->
622
      ActionEvaluation prev act next new_acts ->
623
      chain_state_queue next = new_acts ++ acts ->
624
625
626
627
628
629
      ChainStep prev next
| step_permute :
    forall {prev new : ChainState},
      chain_state_env prev = chain_state_env new ->
      Permutation (chain_state_queue prev) (chain_state_queue new) ->
      ChainStep prev new.
630
631
632
633
634
635
636
637

Definition empty_state : ChainState :=
  {| chain_state_env :=
       {| env_chain :=
            {| block_header :=
                 {| block_height := 0;
                    slot_number := 0;
                    finalized_height := 0; |};
638
               account_balance a := 0%Z;
639
640
641
               contract_state a := None; |};
          env_contracts a := None; |};
     chain_state_queue := [] |}.
642

643
644
645
(* 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. *)
646
Definition ChainTrace := ChainedList ChainState ChainStep.
647

648
649
650
651
(* Additionally, a state is reachable if there is a trace ending in this trace. *)
Definition reachable (state : ChainState) : Prop :=
  inhabited (ChainTrace empty_state state).

652
653
654
(* 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
655
656
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. *)
657
658
659
660
661
662
663
664
665
666
667
668
669
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;
  }.

670
Definition eval_tx {pre : Environment} {act : Action}
671
                   {post : Environment} {new_acts : list Action}
672
                   (step : ActionEvaluation pre act post new_acts) : Tx :=
673
  match step with
674
  | eval_transfer from to amount _ _ _ _ =>
675
    build_tx from to amount tx_empty
676
  | eval_deploy from to amount wc setup _ _ _ _ _ _ _ =>
677
    build_tx from to amount (tx_deploy wc setup)
678
  | eval_call from to amount _ msg _ _ _ _ _ _ _ _ _ _ =>
679
680
681
682
683
    build_tx from to amount (tx_call msg)
  end.

Fixpoint trace_txs {from to : ChainState} (trace : ChainTrace from to) : list Tx :=
  match trace with
684
685
686
  | snoc trace' step =>
    match step with
    | step_action _ eval _ => eval_tx eval :: trace_txs trace'
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
    | _ => 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).

704
705
706
Fixpoint blocks_baked {from to : ChainState}
         (trace : ChainTrace from to) (addr : Address) : list nat :=
  match trace with
707
708
709
  | snoc trace' step =>
    match step with
    | @step_block _ header baker _ _ _ _ _ =>
710
711
712
713
714
715
716
717
      if (baker =? addr)%address
      then block_height header :: blocks_baked trace' addr
      else blocks_baked trace' addr
    | _ => blocks_baked trace' addr
    end
  | clnil => []
  end.

718
Section Theories.
719
Ltac destruct_chain_step :=
720
  match goal with
721
722
  | [step: ChainStep _ _ |- _] =>
    destruct step as
723
724
725
        [prev header baker next queue_prev valid_header acts_from_accs env_eq|
         prev act acts next new_acts queue_prev step queue_new|
         prev new prev_new perm]
726
727
  end.

728
Ltac destruct_action_eval :=
729
  match goal with
730
  | [eval: ActionEvaluation _ _ _ _ |- _] => destruct eval
731
732
  end.

733
734
Lemma contract_addr_format {to} (addr : Address) (wc : WeakContract) :
  reachable to ->
735
736
737
  env_contracts to addr = Some wc ->
  address_is_contract addr = true.
Proof.
738
  intros [trace] contract_at_addr.
739
740
741
  remember empty_state eqn:eq.
  induction trace; rewrite eq in *; clear eq.
  - cbn in *; congruence.
742
  - destruct_chain_step.
743
    + rewrite_environment_equiv; cbn in *; auto.
744
    + destruct_action_eval; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
745
    + intuition.
746
Qed.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
747

748
749
750
751
752
753
754
755
756
757
758
759
760
761
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. *)
762
Lemma undeployed_contract_no_out_queue contract state :
763
  reachable state ->
764
765
766
767
768
769
770
771
  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.
772
  destruct_chain_step; [|destruct_action_eval|];
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
    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. *)
805
806
Lemma undeployed_contract_no_out_txs
      contract state (trace : ChainTrace empty_state state) :
807
808
  address_is_contract contract = true ->
  env_contracts state contract = None ->
809
  outgoing_txs trace contract = [].
810
Proof.
811
  intros is_contract undeployed.
812
  remember empty_state eqn:eq.
813
  induction trace; cbn; auto.
814
  destruct_chain_step.
815
816
817
818
  - (* 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.
819
    Hint Unfold reachable : core.
820
821
    subst.
    cbn.
822
823
824
825
    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
826
827
828
829
830
    repeat
      match goal with
      | [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
      end.
    inversion_clear Hqueue.
831
    destruct_action_eval; rewrite_environment_equiv;
832
833
834
835
836
837
838
839
840
      subst;
      cbn in *;
      destruct_address_eq;
      subst; try tauto; congruence.
  - match goal with
    | [H: _ = _ |- _] => rewrite H in *; auto
    end.
Qed.

841
842
Lemma undeployed_contract_no_in_txs
      contract state (trace : ChainTrace empty_state state) :
843
844
  address_is_contract contract = true ->
  env_contracts state contract = None ->
845
  incoming_txs trace contract = [].
846
Proof.
847
  intros is_contract undeployed.
848
  remember empty_state eqn:eq.
849
  induction trace; cbn; auto.
850
  destruct_chain_step.
851
852
  - (* New block *)
    rewrite_environment_equiv; auto.
853
  - destruct_action_eval; rewrite_environment_equiv;
854
855
856
857
858
859
      cbn in *;
      destruct_address_eq; auto; subst; congruence.
  - match goal with
    | [H: _ = _ |- _] => rewrite H in *; auto
    end.
Qed.
860

861
862
863
864
865
866
867
868
869
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) +
  sumZ compute_block_reward (blocks_baked trace addr) -
  sumZ tx_amount (outgoing_txs trace addr).
Proof.
  unfold incoming_txs, outgoing_txs.
  remember empty_state as from_state.
870
  induction trace; [|destruct_chain_step].
871
872
873
874
875
876
877
878
879
  - subst. cbn. lia.
  - (* Block *)
    rewrite_environment_equiv.
    cbn.
    unfold add_balance.
    rewrite IHtrace by auto.
    destruct_address_eq; subst; cbn; lia.
  - (* Step *)
    cbn.
880
    destruct_action_eval; cbn; rewrite_environment_equiv; cbn.
881
882
883
884
885
886
887
    all: unfold add_balance; rewrite IHtrace by auto.
    all: destruct_address_eq; cbn; lia.
  - cbn.
    rewrite <- prev_new.
    auto.
Qed.

888
End Theories.
889
End Trace.
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
End Semantics.

Class ChainBuilderType :=
  build_builder {
    builder_type : Type;

    builder_initial : builder_type;

    builder_env : builder_type -> Environment;

    builder_add_block
      (b : builder_type)
      (baker : Address)
      (actions : list Action)
      (slot_number : nat)
      (finalized_height : nat) :
      option builder_type;

908
909
    builder_trace (b : builder_type) :
      ChainTrace empty_state (build_chain_state (builder_env b) []);
910
911
  }.

912
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
913
Global Coercion builder_env : builder_type >-> Environment.
914
End Blockchain.
915

916
917
918
Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}.
919
Arguments ContractInterface {_} _ _.
920
Arguments build_contract_interface {_ _ _ _}.
921

922
Ltac destruct_chain_step :=
923
  match goal with
924
925
  | [step: ChainStep _ _ |- _] =>
    destruct step as
926
927
928
        [prev header baker next queue_prev valid_header acts_from_accs env_eq|
         prev act acts next new_acts queue_prev step queue_new|
         prev new prev_new perm]
929
930
  end.

931
Ltac destruct_action_eval :=
932
  match goal with
933
  | [eval: ActionEvaluation _ _ _ _ |- _] => destruct eval
934
935
936
937
938
939
  end.

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