Blockchain.v 30.1 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
Global Instance block_header_settable : Settable _ :=
  settable! build_block_header <block_height; slot_number; finalized_height>.

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

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

99
Global Program Instance chain_equiv_equivalence : Equivalence ChainEquiv.
100
101
102
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.
103
104
105
106

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

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

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

Definition wc_init (wc : WeakContract) :=
151
  let (i, _, _, _) := wc in i.
152

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

Definition wc_receive (wc : WeakContract) :=
165
  let (_, _, r, _) := wc in r.
166

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

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

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

211
212
Arguments init {_ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _}.
213
214
Arguments build_contract {_ _ _ _ _ _}.

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

259
260
Coercion contract_to_weak_contract : Contract >-> WeakContract.

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

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

285
Arguments ContractInterface _ _ : clear implicits.
286

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

302
303
Section Semantics.
Instance chain_settable : Settable _ :=
304
305
306
307
308
309
  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
310
311
312
313
314
           else map a.

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

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

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

332
333
334
335
336
337
338
339
340
341
342
343
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.

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

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

352
353
354
355
356
357
358
359
360
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|>.

361
362
363
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)|>).
364
365
366
367
368

Definition add_contract (addr : Address) (contract : WeakContract) (e : Environment)
  : Environment :=
  e <| env_contracts ::=
    fun f a =>
369
      if (a =? addr)%address
370
371
372
373
374
375
376
      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|>).

377
378
379
380
381
Ltac rewrite_environment_equiv :=
  match goal with
  | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
  end.

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

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

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

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

492
493
494
495
496
Definition eval_from : Address :=
  match eval with
  | eval_transfer from _ _ _ _ _ _
  | eval_deploy from _ _ _ _ _ _ _ _ _ _ _
  | eval_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
497
498
  end.

499
500
501
502
503
Definition eval_to : Address :=
  match eval with
  | eval_transfer _ to _ _ _ _ _
  | eval_deploy _ to _ _ _ _ _ _ _ _ _ _
  | eval_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ => to
504
505
  end.

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

514
Section Theories.
515
Context {pre : Environment} {act : Action}
516
        {post : Environment} {new_acts : list Action}
517
        (eval : ActionEvaluation pre act post new_acts).
518
519

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

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

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

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

562
563
Lemma block_header_post_action : block_header post = block_header pre.
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
Definition add_new_block
578
579
580
          (header : BlockHeader)
          (baker : Address)
          (env : Environment) : Environment :=
581
582
583
584
585
  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|>.
586

587
588
(* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *)
589
Local Open Scope nat.
590
591
592
593
594
595
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.

596
597
598
Definition ActIsFromAccount (act : Action) : Prop :=
  address_is_contract (act_from act) = false.

599
600
601
602
603
Record ChainState :=
  build_chain_state {
    chain_state_env :> Environment;
    chain_state_queue : list Action;
  }.
604

605
606
Inductive ChainStep : ChainState -> ChainState -> Type :=
| step_block :
607
608
609
610
611
612
613
614
615
    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
616
        (add_new_block header baker prev) ->
617
618
      ChainStep prev next
| step_action :
619
620
621
622
623
624
    forall {prev : ChainState}
           {act : Action}
           {acts : list Action}
           {next : ChainState}
           {new_acts : list Action},
      chain_state_queue prev = act :: acts ->
625
      ActionEvaluation prev act next new_acts ->
626
      chain_state_queue next = new_acts ++ acts ->
627
628
629
630
631
632
      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.
633
634
635
636
637
638
639
640

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

646
647
648
(* 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. *)
649
Definition ChainTrace := ChainedList ChainState ChainStep.
650

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

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

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

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

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

721
Section Theories.
722
Ltac destruct_chain_step :=
723
  match goal with
724
725
  | [step: ChainStep _ _ |- _] =>
    destruct step as
726
727
728
        [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]
729
730
  end.

731
Ltac destruct_action_eval :=
732
  match goal with
733
  | [eval: ActionEvaluation _ _ _ _ |- _] => destruct eval
734
735
  end.

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

751
752
753
754
755
756
757
758
759
760
761
762
763
764
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. *)
765
Lemma undeployed_contract_no_out_queue contract state :
766
  reachable state ->
767
768
769
770
771
772
773
774
  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.
775
  destruct_chain_step; [|destruct_action_eval|];
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
805
806
807
    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. *)
808
809
Lemma undeployed_contract_no_out_txs
      contract state (trace : ChainTrace empty_state state) :
810
811
  address_is_contract contract = true ->
  env_contracts state contract = None ->
812
  outgoing_txs trace contract = [].
813
Proof.
814
  intros is_contract undeployed.
815
  remember empty_state eqn:eq.
816
  induction trace; cbn; auto.
817
  destruct_chain_step.
818
819
820
821
  - (* 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.
822
    Hint Unfold reachable : core.
823
824
    subst.
    cbn.
825
826
827
828
    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
829
830
831
832
833
    repeat
      match goal with
      | [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
      end.
    inversion_clear Hqueue.
834
    destruct_action_eval; rewrite_environment_equiv;
835
836
837
838
839
840
841
842
843
      subst;
      cbn in *;
      destruct_address_eq;
      subst; try tauto; congruence.
  - match goal with
    | [H: _ = _ |- _] => rewrite H in *; auto
    end.
Qed.

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

864
865
866
867
868
869
870
871
872
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.
873
  induction trace; [|destruct_chain_step].
874
875
876
877
878
879
880
881
882
  - subst. cbn. lia.
  - (* Block *)
    rewrite_environment_equiv.
    cbn.
    unfold add_balance.
    rewrite IHtrace by auto.
    destruct_address_eq; subst; cbn; lia.
  - (* Step *)
    cbn.
883
    destruct_action_eval; cbn; rewrite_environment_equiv; cbn.
884
885
886
887
888
889
890
    all: unfold add_balance; rewrite IHtrace by auto.
    all: destruct_address_eq; cbn; lia.
  - cbn.
    rewrite <- prev_new.
    auto.
Qed.

891
End Theories.
892
End Trace.
893
894
895
896
897
898
899
900
901
902
903
End Semantics.

Class ChainBuilderType :=
  build_builder {
    builder_type : Type;

    builder_initial : builder_type;

    builder_env : builder_type -> Environment;

    builder_add_block
904
      (builder : builder_type)
905
      (baker : Address)
906
907
      (header : BlockHeader)
      (actions : list Action) :
908
909
      option builder_type;

910
911
    builder_trace (builder : builder_type) :
      ChainTrace empty_state (build_chain_state (builder_env builder) []);
912
913
  }.

914
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
915
Global Coercion builder_env : builder_type >-> Environment.
916
End Blockchain.
917

918
919
920
Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}.
921
Arguments ContractInterface {_} _ _.
922
Arguments build_contract_interface {_ _ _ _}.
923

924
Ltac destruct_chain_step :=
925
  match goal with
926
927
  | [step: ChainStep _ _ |- _] =>
    destruct step as
928
929
930
        [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]
931
932
  end.

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

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