Blockchain.v 29.2 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
20
21
22
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.

Import ListNotations.

Definition Version := nat.

Definition Amount := Z.

Bind Scope Z_scope with Amount.

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

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

40
Delimit Scope address_scope with address.
41
Bind Scope address_scope with Address.
42
Infix "=?" := address_eqb (at level 70) : address_scope.
43

44
45
46
Global Ltac destruct_address_eq :=
  repeat
    match goal with
47
48
    | [H: context[address_eqb ?a ?b] |- _] => destruct (address_eqb_spec a b)
    | [|- context[address_eqb ?a ?b]] => destruct (address_eqb_spec a b)
49
    end.
50

51
Section Blockchain.
52
Context {BaseTypes : ChainBase}.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
53

54
55
56
57
58
59
60
61
62
63
64
65
66
Lemma address_eq_refl x :
  address_eqb x x = true.
Proof. destruct_address_eq; auto; congruence. Qed.

Lemma address_eq_sym x y :
  address_eqb x y = address_eqb y x.
Proof. destruct_address_eq; auto; congruence. Qed.

Lemma address_eq_ne x y :
  x <> y ->
  address_eqb x y = false.
Proof. destruct_address_eq; auto; congruence. Qed.

67
68
Record BlockHeader :=
  build_block_header {
69
70
71
    block_height : nat;
    slot_number : nat;
    finalized_height : nat;
72
73
  }.

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

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

93
Global Program Instance chain_equiv_equivalence : Equivalence ChainEquiv.
94
95
96
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.
97
98
99
100

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

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

118
119
120
(* Operations that a contract can return or that a user can use
to interact with a chain. *)
Inductive ActionBody :=
121
122
  | act_transfer (to : Address) (amount : Amount)
  | act_call (to : Address) (amount : Amount) (msg : OakValue)
123
  | act_deploy (amount : Amount) (c : WeakContract) (setup : OakValue)
124

125
(* Since one operation is the possibility to deploy a new contract,
126
127
128
129
130
131
132
133
134
135
136
this represents an instance of a contract. Note that the act of deploying
a contract has to be a separate thing to the contract deployment a contract
can access during its execution due to positivity constraints. That is,
we would like to allow contracts to obtain information about what another
contract was deployed with (its setup, version and amount transferred). An obvious
way to model this would be to simply store a WeakContract in the chain.
But this is already a non-strict positive occurence, since we dumbed down then
end up with
Record WeakContract := { receive : (Address -> WeakContract) -> State -> State }.
where Address -> WeakContract would be some operation that the chain provides
to allow access to contracts in deployments.
137
*)
138
with WeakContract :=
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
     | build_weak_contract
         (version : Version)
         (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).
158
159
160
161
162
163
164

Definition wc_version (wc : WeakContract) : Version :=
  let (v, _, _, _, _) := wc in v.

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

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

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

179
180
181
182
183
184
185
186
187
188
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
      | build_weak_contract _ _ _ _ rp => rp
      end).
Qed.
189
190
191
192
193
194

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

196
(* Represents a strongly-typed contract. This is what user's will primarily
197
198
199
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 *)
200
Record Contract
201
202
203
204
      (Setup Msg State : Type)
      `{OakTypeEquivalence Setup}
      `{OakTypeEquivalence Msg}
      `{OakTypeEquivalence State} :=
205
206
  build_contract {
    version : Version;
207
208
209
    init :
      Chain ->
      ContractCallContext ->
210
211
      Setup ->
      option State;
212
213
    init_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq) init;
214
    receive :
215
216
      Chain ->
      ContractCallContext ->
217
218
219
      State ->
      option Msg ->
      option (State * list ActionBody);
220
221
    receive_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive;
222
223
  }.

224
225
226
Arguments version {_ _ _ _ _ _}.
Arguments init {_ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _}.
227
228
Arguments build_contract {_ _ _ _ _ _}.

229
Program Definition contract_to_weak_contract
230
231
232
233
234
          {Setup Msg State : Type}
          `{OakTypeEquivalence Setup}
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
          (c : Contract Setup Msg State) : WeakContract :=
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
      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
      build_weak_contract c.(version) weak_init _ weak_recv _.
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.
272

273
274
Coercion contract_to_weak_contract : Contract >-> WeakContract.

275
(* Deploy a strongly typed contract with some amount and setup *)
276
Definition create_deployment
277
278
279
280
          {Setup Msg State : Type}
          `{OakTypeEquivalence Setup}
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
281
          (amount : Amount)
282
283
          (contract : Contract Setup Msg State)
          (setup : Setup) : ActionBody :=
284
285
  act_deploy amount contract (serialize setup).

286
(* The contract interface is the main mechanism allowing a deployed
287
contract to interact with another deployed contract. This hides
288
the ugly details of everything being OakValue away from contracts. *)
289
Record ContractInterface {Msg State : Type} :=
290
  build_contract_interface {
291
    (* The address of the contract being interfaced with *)
292
    contract_address : Address;
293
    (* Obtain the state at some point of time *)
294
    get_state : Chain -> option State;
295
296
    (* Make an action sending money and optionally a message to the contract *)
    send : Amount -> option Msg -> ActionBody;
297
298
  }.

299
Arguments ContractInterface _ _ : clear implicits.
300

301
Definition get_contract_interface
302
303
          (chain : Chain)
          (addr : Address)
304
          (Msg State : Type)
305
306
          `{OakTypeEquivalence Msg}
          `{OakTypeEquivalence State}
307
  : option (ContractInterface Msg State) :=
308
  let ifc_get_state chain := contract_state chain addr >>= deserialize in
309
310
311
312
313
314
  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; |}.
315

316
317
Section Semantics.
Instance chain_settable : Settable _ :=
318
319
320
321
322
323
  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
324
325
326
327
328
329
330
331
332
333
334
335
336
           else map a.

Definition set_chain_contract_state
           (addr : Address) (state : OakValue) (map : Address -> option OakValue)
  : Address -> option OakValue :=
  fun a => if address_eqb a addr
           then Some state
           else map a.

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

339
(* Furthermore we define extensional equality for such environments. *)
340
341
Record EnvironmentEquiv (e1 e2 : Environment) : Prop :=
  build_env_equiv {
342
    chain_equiv : ChainEquiv e1 e2;
343
    contracts_eq : forall a, env_contracts e1 a = env_contracts e2 a;
344
345
  }.

346
347
348
349
350
351
352
353
354
355
356
357
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.

358
Global Instance environment_equiv_contracts_proper :
359
360
361
  Proper (EnvironmentEquiv ==> eq ==> eq) env_contracts.
Proof. repeat intro; subst; apply contracts_eq; assumption. Qed.

362
363
364
365
Global Instance environment_equiv_chain_equiv_proper :
  Proper (EnvironmentEquiv ==> ChainEquiv) env_chain.
Proof. repeat intro; apply chain_equiv; assumption. Qed.

366
367
368
369
370
371
372
373
374
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|>.

375
376
377
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)|>).
378
379
380
381
382

Definition add_contract (addr : Address) (contract : WeakContract) (e : Environment)
  : Environment :=
  e <| env_contracts ::=
    fun f a =>
383
      if (a =? addr)%address
384
385
386
387
388
389
390
      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|>).

391
392
393
394
395
Ltac rewrite_environment_equiv :=
  match goal with
  | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
  end.

396
397
398
399
400
Ltac solve_proper :=
  apply build_env_equiv;
  [apply build_chain_equiv|];
  cbn;
  repeat intro;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
401
  repeat rewrite_environment_equiv;
402
403
  auto.

404
405
Global Instance transfer_balance_proper :
  Proper (eq ==> eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) transfer_balance.
406
407
Proof.
  repeat intro; subst.
408
  unfold transfer_balance, add_balance.
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
  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.

428
429
430
431
432
433
434
Section Step.
Local Open Scope Z.
(* Next we define a single step. It specifies how an external action
changes an environment and which external actions to execute after it. *)
(* todo: handle deploy/call failures. We should still transfer gas and allow this
to be recorded. *)
Inductive ChainStep :
435
436
  Environment -> Action ->
  Environment -> list Action -> Type :=
437
  | step_transfer :
438
439
440
441
442
443
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             (from to : Address)
             (amount : Amount),
        amount <= account_balance pre from ->
444
        address_is_contract to = false ->
445
        act = build_act from (act_transfer to amount) ->
446
        EnvironmentEquiv new_env (transfer_balance from to amount pre) ->
447
        ChainStep pre act new_env []
448
449
450
451
452
453
454
455
456
457
  | step_deploy :
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             (from to : Address)
             (amount : Amount)
             (wc : WeakContract)
             (setup : OakValue)
             (state : OakValue),
      amount <= account_balance pre from ->
458
      address_is_contract to = true ->
459
      env_contracts pre to = None ->
460
      act = build_act from (act_deploy amount wc setup) ->
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
461
462
      wc_init
        wc
463
        (transfer_balance from to amount pre)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
464
465
        (build_ctx from to amount)
        setup = Some state ->
466
467
      EnvironmentEquiv
        new_env
468
        (set_contract_state to state (add_contract to wc (transfer_balance from to amount pre))) ->
469
      ChainStep pre act new_env []
470
  | step_call :
471
472
473
474
475
476
477
      forall {pre : Environment}
             {act : Action}
             {new_env : Environment}
             {new_acts : list Action}
             (from to : Address)
             (amount : Amount)
             (wc : WeakContract)
478
             (msg : option OakValue)
479
480
481
482
483
484
             (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 ->
485
486
487
488
      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
489
490
      wc_receive
        wc
491
        (transfer_balance from to amount pre)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
492
493
        (build_ctx from to amount)
        prev_state
494
        msg = Some (new_state, resp_acts) ->
495
496
497
      new_acts = map (build_act to) resp_acts ->
      EnvironmentEquiv
        new_env
498
        (set_contract_state to new_state (transfer_balance from to amount pre)) ->
499
500
501
502
503
504
505
506
507
      ChainStep pre act new_env new_acts.

Section Accessors.
Context {pre : Environment} {act : Action}
        {post : Environment} {new_acts : list Action}
        (step : ChainStep pre act post new_acts).

Definition step_from : Address :=
  match step with
508
509
510
  | step_transfer from _ _ _ _ _ _
  | step_deploy from _ _ _ _ _ _ _ _ _ _ _
  | step_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
511
512
513
514
  end.

Definition step_to : Address :=
  match step with
515
516
517
  | step_transfer _ to _ _ _ _ _
  | step_deploy _ to _ _ _ _ _ _ _ _ _ _
  | step_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ => to
518
519
520
521
  end.

Definition step_amount : Amount :=
  match step with
522
523
524
  | step_transfer _ _ amount _ _ _ _
  | step_deploy _ _ amount _ _ _ _ _ _ _ _ _
  | step_call _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ => amount
525
526
  end.
End Accessors.
527

528
Section Theories.
529
Context {pre : Environment} {act : Action}
530
        {post : Environment} {new_acts : list Action}
531
        (step : ChainStep pre act post new_acts).
532
533

Lemma account_balance_post (addr : Address) :
534
  account_balance post addr =
535
  account_balance pre addr
536
537
  + (if (addr =? step_to step)%address then step_amount step else 0)
  - (if (addr =? step_from step)%address then step_amount step else 0).
538
Proof.
539
540
  destruct step; cbn; rewrite_environment_equiv; cbn;
    unfold add_balance; destruct_address_eq; lia.
541
542
543
Qed.

Lemma account_balance_post_to :
544
545
546
  step_from step <> step_to step ->
  account_balance post (step_to step) =
  account_balance pre (step_to step) + step_amount step.
547
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
548
  intros neq.
549
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
550
551
  rewrite address_eq_refl, address_eq_ne by auto.
  lia.
552
553
554
Qed.

Lemma account_balance_post_from :
555
556
557
  step_from step <> step_to step ->
  account_balance post (step_from step) =
  account_balance pre (step_from step) - step_amount step.
558
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
559
  intros neq.
560
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
561
562
  rewrite address_eq_refl, address_eq_ne by auto.
  lia.
563
564
565
Qed.

Lemma account_balance_post_irrelevant (addr : Address) :
566
567
  addr <> step_from step ->
  addr <> step_to step ->
568
569
  account_balance post addr = account_balance pre addr.
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
570
  intros neq_from neq_to.
571
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
572
573
  repeat rewrite address_eq_ne by auto.
  lia.
574
575
576
Qed.

Lemma block_header_post_step : block_header post = block_header pre.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
577
Proof. destruct step; rewrite_environment_equiv; auto. Qed.
578
579
580
581
582
583

Lemma contracts_post_pre_none contract :
  env_contracts post contract = None ->
  env_contracts pre contract = None.
Proof.
  intros H.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
584
585
  destruct step; rewrite_environment_equiv; auto.
  cbn in *.
586
587
  destruct_address_eq; congruence.
Qed.
588
589
End Theories.
End Step.
590

591
Section Trace.
592
Definition add_new_block
593
594
595
          (header : BlockHeader)
          (baker : Address)
          (env : Environment) : Environment :=
596
597
598
599
600
  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|>.
601

602
603
(* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *)
604
605
606
607
608
609
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.

610
611
612
Definition ActIsFromAccount (act : Action) : Prop :=
  address_is_contract (act_from act) = false.

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

619
Inductive ChainEvent : ChainState -> ChainState -> Type :=
620
621
622
623
624
625
626
627
628
629
| evt_block :
    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
630
        (add_new_block header baker prev) ->
631
632
633
634
635
636
637
638
639
640
641
      ChainEvent prev next
| evt_step :
    forall {prev : ChainState}
           {act : Action}
           {acts : list Action}
           {next : ChainState}
           {new_acts : list Action},
      chain_state_queue prev = act :: acts ->
      ChainStep prev act next new_acts ->
      chain_state_queue next = new_acts ++ acts ->
      ChainEvent prev next
642
643
644
645
646
647
648
649
650
651
652
653
654
  | evt_permute :
      forall {prev new : ChainState},
        chain_state_env prev = chain_state_env new ->
        Permutation (chain_state_queue prev) (chain_state_queue new) ->
        ChainEvent prev new.

Definition empty_state : ChainState :=
  {| chain_state_env :=
       {| env_chain :=
            {| block_header :=
                 {| block_height := 0;
                    slot_number := 0;
                    finalized_height := 0; |};
655
               account_balance a := 0%Z;
656
657
658
               contract_state a := None; |};
          env_contracts a := None; |};
     chain_state_queue := [] |}.
659

660
661
662
(* 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. *)
663
Definition ChainTrace := ChainedList ChainState ChainEvent.
664

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

669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
(* 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
a normal blockchain is. Each step corresponds to a transaction and we can go from a
trace to a list of transactions. *)
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;
  }.

Definition step_tx {pre : Environment} {act : Action}
                   {post : Environment} {new_acts : list Action}
                   (step : ChainStep pre act post new_acts) : Tx :=
  match step with
  | step_transfer from to amount _ _ _ _ =>
    build_tx from to amount tx_empty
  | step_deploy from to amount wc setup _ _ _ _ _ _ _ =>
    build_tx from to amount (tx_deploy wc setup)
  | step_call from to amount _ msg _ _ _ _ _ _ _ _ _ _ =>
    build_tx from to amount (tx_call msg)
  end.

Fixpoint trace_txs {from to : ChainState} (trace : ChainTrace from to) : list Tx :=
  match trace with
  | snoc trace' evt =>
    match evt with
    | evt_step _ step _ => step_tx step :: trace_txs trace'
    | _ => 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).

721
Section Theories.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
722
Ltac destruct_chain_event :=
723
  match goal with
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
724
  | [evt: ChainEvent _ _ |- _] => destruct evt
725
726
  end.

Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
727
Ltac destruct_chain_step :=
728
  match goal with
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
729
  | [step: ChainStep _ _ _ _ |- _] => destruct step
730
731
  end.

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

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

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

860
End Theories.
861
End Trace.
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
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;

880
881
    builder_trace (b : builder_type) :
      ChainTrace empty_state (build_chain_state (builder_env b) []);
882
883
  }.

884
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
885
Global Coercion builder_env : builder_type >-> Environment.
886
End Blockchain.
887

888
889
890
891
Arguments version {_ _ _ _ _ _ _}.
Arguments init {_ _ _ _ _ _ _}.
Arguments receive {_ _ _ _ _ _ _}.
Arguments build_contract {_ _ _ _ _ _ _}.
892
Arguments ContractInterface {_} _ _.
893
Arguments build_contract_interface {_ _ _ _}.
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913

Ltac destruct_chain_event :=
  match goal with
  | [evt: ChainEvent _ _ |- _] => destruct evt
  end.

Ltac destruct_chain_step :=
  match goal with
  | [step: ChainStep _ _ _ _ |- _] => destruct step
  end.

Ltac invert_chain_step :=
  match goal with
  | [step: ChainStep _ _ _ _ |- _] => inversion step
  end.

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