Blockchain.v 42.7 KB
Newer Older
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
(* This file defines blockchains, both a contract's view (which is
more computational) and the semantics of executing smart contracts
in a blockchain.

The most important types are:

* The ChainBase type, describing basic assumptions made of any blockchain.
In most cases we will abstract over this type.

* The Chain type, describing a smart contract's view of the blockchain.
This is the the data that can be accessed by smart contracts.

* The Action type, describing how smart contracts (and external users)
interact with the blockchain. We allow transfers, calls and deployment
of contracts.

* The WeakContract type, describing a "weak" or "stringly" typed
version of smart contracts. Contracts are just two functions init and
receive to respectively initialize state on deployment and to update
state when receiving messages. The weak version of contracts means that
the state/message/setup types, which would normally vary with contracts,
are stored in a serialized format.

* The Contract type, describing a more strongly typed version of a contract.
This is the same as the above except we abstract over the appropriate types.
Users of the framework will mostly need to deal with this.

The next types deal with semantics.

* The Environment type. This augments the Chain type with more information.
Environment can be thought of as the information that a realistic blockchain
implementation would need to keep track of to implement operations. For instance,
it is reasonable to assume that an implementation needs to access the state of
contracts, but not to assume that it needs to store the full transaction history
of all addresses.

* The ActionEvaluation type. This specifies how to evaluate actions returned by
contracts or input in blocks. This related an environment and action to a new
environment and list of new actions to execute.

* The ChainState type. This augments the Environment type with a queue of
"outstanding" actions that need to be executed. For instance, when a block is
added, its actions are put into this queue.

* The ChainStep type. This specifies how the blockchain should execute smart
contracts, and how new blocks are added. It relates a ChainState to a new ChainState.
There are steps to allow adding blocks, evaluating actions in the queue and to
permute the queue (allowing to model any execution order).

* The ChainTrace type. This just represents a sequence of steps. If a trace ends
in a state it means that state is reachable and there is a "semantically correct"
way of executing to get to this state. This type records the full history of a
blockchain's execution and it would thus be unrealistic to extract.

* The ChainBuilderType type. This is a typeclass for implementations of blockchains,
where these implementations need to prove that they satisfy our semantics.

*)


61
From Coq Require Import Arith ZArith.
62
From Coq Require Import List.
63
64
65
66
From Coq Require Import Psatz.
From Coq Require Import Permutation.
From Coq Require Import Morphisms.
From Coq Require Import Setoid.
67
From SmartContracts Require Import Serializable.
68
From SmartContracts Require Import Monads.
69
From SmartContracts Require Import Extras.
70
From SmartContracts Require Import Automation.
71
From SmartContracts Require Import ChainedList.
72
73
74
75
76
77
78
79
From RecordUpdate Require Import RecordUpdate.
From stdpp Require countable.

Import ListNotations.

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

80
81
Class ChainBase :=
  build_chain_base {
82
83
    Address : Type;
    address_eqb : Address -> Address -> bool;
84
85
    address_eqb_spec :
      forall (a b : Address), Bool.reflect (a = b) (address_eqb a b);
86
87
    address_eqdec :> stdpp.base.EqDecision Address;
    address_countable :> countable.Countable Address;
88
    address_serializable :> Serializable Address;
89
    address_is_contract : Address -> bool;
90
91
92
  }.

Global Opaque Address address_eqb address_eqb_spec
93
       address_eqdec address_countable address_serializable.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
94

95
Delimit Scope address_scope with address.
96
Bind Scope address_scope with Address.
97
Infix "=?" := address_eqb (at level 70) : address_scope.
98

99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
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.

116
117
118
Global Ltac destruct_address_eq :=
  repeat
    match goal with
119
120
121
122
    | [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)
123
    end.
124

125
Section Blockchain.
126
Context {BaseTypes : ChainBase}.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
127

128
129
130
131
(* This represents the view of the blockchain that a contract
can access and interact with. *)
Record Chain :=
  build_chain {
132
133
134
    chain_height : nat;
    current_slot : nat;
    finalized_height : nat;
135
    account_balance : Address -> Amount;
136
137
  }.

138
139
(* Two chains are said to be equivalent if they are extensionally equal.
We will later require that all deployed contracts respect this relation.
140
This equivalence is equality if funext is assumed. *)
141
142
Record ChainEquiv (c1 c2 : Chain) : Prop :=
  build_chain_equiv {
143
144
145
    chain_height_eq : chain_height c1 = chain_height c2;
    current_slot_eq : current_slot c1 = current_slot c2;
    finalized_height_eq : finalized_height c1 = finalized_height c2;
146
    account_balance_eq : forall addr, account_balance c1 addr = account_balance c2 addr;
147
148
  }.

149
Global Program Instance chain_equiv_equivalence : Equivalence ChainEquiv.
150
151
152
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.
153

154
155
156
157
158
159
160
161
162
Global Instance chain_equiv_chain_height :
  Proper (ChainEquiv ==> eq) chain_height.
Proof. repeat intro; auto using chain_height_eq. Qed.
Global Instance chain_equiv_current_slot :
  Proper (ChainEquiv ==> eq) current_slot.
Proof. repeat intro; auto using current_slot_eq. Qed.
Global Instance chain_equiv_finalized_height :
  Proper (ChainEquiv ==> eq) finalized_height.
Proof. repeat intro; auto using finalized_height_eq. Qed.
163
164
165
Global Instance chain_equiv_account_balance_proper :
  Proper (ChainEquiv ==> eq ==> eq) account_balance.
Proof. repeat intro; subst; auto using account_balance_eq. Qed.
166

167
168
Record ContractCallContext :=
  build_ctx {
169
170
171
172
    (* Address sending the funds *)
    ctx_from : Address;
    (* Address of the contract being called *)
    ctx_contract_address : Address;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
173
    (* Amount of currency passed in call *)
174
    ctx_amount : Amount;
175
  }.
176

177
178
179
(* Operations that a contract can return or that a user can use
to interact with a chain. *)
Inductive ActionBody :=
180
  | act_transfer (to : Address) (amount : Amount)
181
182
  | act_call (to : Address) (amount : Amount) (msg : SerializedValue)
  | act_deploy (amount : Amount) (c : WeakContract) (setup : SerializedValue)
183
with WeakContract :=
184
185
186
187
     | build_weak_contract
         (init :
            Chain ->
            ContractCallContext ->
188
189
            SerializedValue (* setup *) ->
            option SerializedValue)
190
191
192
193
194
195
         (* Init respects chain equivalence *)
         (init_proper :
            Proper (ChainEquiv ==> eq ==> eq ==> eq) init)
         (receive :
            Chain ->
            ContractCallContext ->
196
197
198
            SerializedValue (* state *) ->
            option SerializedValue (* message *) ->
            option (SerializedValue * list ActionBody))
199
200
201
         (* And so does receive *)
         (receive_proper :
            Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive).
202
203

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

206
207
208
209
210
211
212
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
213
      | build_weak_contract _ ip _ _ => ip
214
215
      end).
Qed.
216
217

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

220
221
222
223
224
225
226
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
227
      | build_weak_contract _ _ _ rp => rp
228
229
      end).
Qed.
230
231
232
233
234
235

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

237
(* Represents a strongly-typed contract. This is what user's will primarily
238
239
240
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 *)
241
Record Contract
242
      (Setup Msg State : Type)
243
244
245
      `{Serializable Setup}
      `{Serializable Msg}
      `{Serializable State} :=
246
  build_contract {
247
248
249
    init :
      Chain ->
      ContractCallContext ->
250
251
      Setup ->
      option State;
252
253
    init_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq) init;
254
    receive :
255
256
      Chain ->
      ContractCallContext ->
257
258
259
      State ->
      option Msg ->
      option (State * list ActionBody);
260
261
    receive_proper :
      Proper (ChainEquiv ==> eq ==> eq ==> eq ==> eq) receive;
262
263
  }.

264
265
266
Global Arguments init {_ _ _ _ _ _}.
Global Arguments receive {_ _ _ _ _ _}.
Global Arguments build_contract {_ _ _ _ _ _}.
267

268
Program Definition contract_to_weak_contract
269
          {Setup Msg State : Type}
270
271
272
          `{Serializable Setup}
          `{Serializable Msg}
          `{Serializable State}
273
          (c : Contract Setup Msg State) : WeakContract :=
274
275
      let weak_init chain ctx ser_setup :=
          do setup <- deserialize ser_setup;
276
277
          do state <- c.(init) chain ctx setup;
          Some (serialize state) in
278
279
280
281
282
      let weak_recv chain ctx ser_state ser_msg_opt :=
          do state <- deserialize ser_state;
          match ser_msg_opt with
          | Some ser_msg =>
            do msg <- deserialize ser_msg;
283
284
285
286
287
288
            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
289
      build_weak_contract weak_init _ weak_recv _.
290
Next Obligation.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
291
292
  repeat intro.
  subst.
293
  subst weak_init.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
294
295
296
  cbn.
  destruct (deserialize _); auto.
  cbn.
297
298
299
  now rewrite init_proper.
Qed.
Next Obligation.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
300
301
  repeat intro.
  subst.
302
  subst weak_recv.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
303
304
305
306
307
308
  cbn.
  destruct (deserialize _); auto.
  cbn.
  destruct_match.
  - destruct (deserialize _); auto.
    cbn.
309
    now rewrite receive_proper.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
310
  - now rewrite receive_proper.
311
Qed.
312

313
314
Coercion contract_to_weak_contract : Contract >-> WeakContract.

315
(* Deploy a strongly typed contract with some amount and setup *)
316
Definition create_deployment
317
          {Setup Msg State : Type}
318
319
320
          `{Serializable Setup}
          `{Serializable Msg}
          `{Serializable State}
321
          (amount : Amount)
322
323
          (contract : Contract Setup Msg State)
          (setup : Setup) : ActionBody :=
324
325
  act_deploy amount contract (serialize setup).

326
(* The contract interface is the main mechanism allowing a deployed
327
contract to interact with another deployed contract. This hides
328
the ugly details of everything being SerializedValue away from contracts. *)
329
Record ContractInterface {Msg : Type} :=
330
  build_contract_interface {
331
    (* The address of the contract being interfaced with *)
332
    contract_address : Address;
333
334
    (* Make an action sending money and optionally a message to the contract *)
    send : Amount -> option Msg -> ActionBody;
335
336
  }.

337
Global Arguments ContractInterface _ : clear implicits.
338

339
Definition get_contract_interface
340
341
342
          (chain : Chain) (addr : Address)
          (Msg : Type) `{Serializable Msg}
  : option (ContractInterface Msg) :=
343
344
345
346
347
  let ifc_send amount msg :=
      match msg with
      | None => act_transfer addr amount
      | Some msg => act_call addr amount (serialize msg)
      end in
348
  Some {| contract_address := addr; send := ifc_send; |}.
349

350
Section Semantics.
351
Global Instance chain_settable : Settable _ :=
352
353
  settable! build_chain
  <chain_height; current_slot; finalized_height; account_balance>.
354
355
356
357
358

Definition add_balance (addr : Address) (amount : Amount) (map : Address -> Amount) :
  Address -> Amount :=
  fun a => if (a =? addr)%address
           then (amount + map a)%Z
359
360
361
           else map a.

Definition set_chain_contract_state
362
363
364
           (addr : Address) (state : SerializedValue)
           (map : Address -> option SerializedValue)
  : Address -> option SerializedValue :=
365
  fun a => if (a =? addr)%address
366
367
368
369
370
371
372
           then Some state
           else map a.

Record Environment :=
  build_env {
    env_chain :> Chain;
    env_contracts : Address -> option WeakContract;
373
    env_contract_states : Address -> option SerializedValue;
374
375
  }.

376
(* Furthermore we define extensional equality for such environments. *)
377
378
Record EnvironmentEquiv (e1 e2 : Environment) : Prop :=
  build_env_equiv {
379
    chain_equiv : ChainEquiv e1 e2;
380
    contracts_eq : forall a, env_contracts e1 a = env_contracts e2 a;
381
    contract_states_eq : forall addr, env_contract_states e1 addr = env_contract_states e2 addr;
382
383
  }.

384
385
386
387
388
389
(* Strongly typed version of contract state *)
Definition contract_state
           {A : Type} `{Serializable A}
           (env : Environment) (addr : Address) : option A :=
  env_contract_states env addr >>= deserialize.

390
391
392
393
394
395
396
397
398
399
400
401
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.

402
Global Instance environment_equiv_env_contracts_proper :
403
404
405
  Proper (EnvironmentEquiv ==> eq ==> eq) env_contracts.
Proof. repeat intro; subst; apply contracts_eq; assumption. Qed.

406
Global Instance environment_equiv_env_contract_states_proper :
407
408
409
  Proper (EnvironmentEquiv ==> eq ==> eq) env_contract_states.
Proof. repeat intro; subst; apply contract_states_eq; assumption. Qed.

410
Global Instance environment_equiv_env_chain_equiv_proper :
411
412
413
  Proper (EnvironmentEquiv ==> ChainEquiv) env_chain.
Proof. repeat intro; apply chain_equiv; assumption. Qed.

414
415
416
417
418
419
420
421
422
423
Global Instance environment_equiv_contract_state_proper
  {A : Type} `{Serializable A} :
  Proper (EnvironmentEquiv ==> eq ==> (@eq (option A))) contract_state.
Proof.
  intros ? ? env_eq ? ? ?.
  subst.
  unfold contract_state.
  now rewrite env_eq.
Qed.

424
Instance env_settable : Settable _ :=
425
  settable! build_env <env_chain; env_contracts; env_contract_states>.
426

427
428
429
Definition transfer_balance (from to : Address) (amount : Amount) (env : Environment) :=
  env<|env_chain; account_balance ::= add_balance to amount|>
     <|env_chain; account_balance ::= add_balance from (-amount)|>.
430

431
Definition add_contract (addr : Address) (contract : WeakContract) (env : Environment)
432
  : Environment :=
433
  env<|env_contracts ::=
434
    fun f a =>
435
      if (a =? addr)%address
436
      then Some contract
437
      else f a|>.
438

439
440
Definition set_contract_state
           (addr : Address) (state : SerializedValue) (env : Environment) :=
441
  env<|env_contract_states ::= set_chain_contract_state addr state|>.
442

443
444
445
446
447
(* set_chain_contract_state updates a map (function) by returning a
   new map (function).  If this function is immediately applied to a
   key, then unfold it. *)
Global Arguments set_chain_contract_state _ _ _ /.

448
449
450
451
452
Ltac rewrite_environment_equiv :=
  match goal with
  | [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
  end.

453
454
Ltac solve_proper :=
  apply build_env_equiv;
455
  [apply build_chain_equiv| |];
456
457
  cbn;
  repeat intro;
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
458
  repeat rewrite_environment_equiv;
459
460
  auto.

461
462
Global Instance transfer_balance_proper :
  Proper (eq ==> eq ==> eq ==> EnvironmentEquiv ==> EnvironmentEquiv) transfer_balance.
463
464
Proof.
  repeat intro; subst.
465
  unfold transfer_balance, add_balance.
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
  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.
481
  unfold set_contract_state, set_chain_contract_state.
482
483
484
  solve_proper.
Qed.

485
Local Open Scope Z.
486
487
488
489
490
(* 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. *)
491
492
493
Inductive ActionEvaluation
          (prev_env : Environment) (act : Action)
          (new_env : Environment) (new_acts : list Action) : Type :=
494
  | eval_transfer :
495
      forall (from to : Address)
496
             (amount : Amount),
497
        amount >= 0 ->
498
        amount <= account_balance prev_env from ->
499
        address_is_contract to = false ->
500
        act = build_act from (act_transfer to amount) ->
501
502
        EnvironmentEquiv
          new_env
503
504
505
          (transfer_balance from to amount prev_env) ->
        new_acts = [] ->
        ActionEvaluation prev_env act new_env new_acts
506
  | eval_deploy :
507
      forall (from to : Address)
508
509
             (amount : Amount)
             (wc : WeakContract)
510
511
             (setup : SerializedValue)
             (state : SerializedValue),
512
      amount >= 0 ->
513
      amount <= account_balance prev_env from ->
514
      address_is_contract to = true ->
515
      env_contracts prev_env to = None ->
516
      act = build_act from (act_deploy amount wc setup) ->
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
517
518
      wc_init
        wc
519
        (transfer_balance from to amount prev_env)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
520
521
        (build_ctx from to amount)
        setup = Some state ->
522
523
      EnvironmentEquiv
        new_env
524
525
526
        (set_contract_state to state (add_contract to wc (transfer_balance from to amount prev_env))) ->
      new_acts = [] ->
      ActionEvaluation prev_env act new_env new_acts
527
  | eval_call :
528
      forall (from to : Address)
529
530
             (amount : Amount)
             (wc : WeakContract)
531
532
533
             (msg : option SerializedValue)
             (prev_state : SerializedValue)
             (new_state : SerializedValue)
534
             (resp_acts : list ActionBody),
535
      amount >= 0 ->
536
537
538
      amount <= account_balance prev_env from ->
      env_contracts prev_env to = Some wc ->
      env_contract_states prev_env to = Some prev_state ->
539
540
541
542
      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
543
544
      wc_receive
        wc
545
        (transfer_balance from to amount prev_env)
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
546
547
        (build_ctx from to amount)
        prev_state
548
        msg = Some (new_state, resp_acts) ->
549
550
551
      new_acts = map (build_act to) resp_acts ->
      EnvironmentEquiv
        new_env
552
553
554
555
556
557
        (set_contract_state to new_state (transfer_balance from to amount prev_env)) ->
      ActionEvaluation prev_env act new_env new_acts.

Global Arguments eval_transfer {_ _ _ _}.
Global Arguments eval_deploy {_ _ _ _}.
Global Arguments eval_call {_ _ _ _}.
558
559
560
561

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

564
565
Definition eval_from : Address :=
  match eval with
566
567
  | eval_transfer from _ _ _ _ _ _ _ _
  | eval_deploy from _ _ _ _ _ _ _ _ _ _ _ _ _
568
  | eval_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
569
570
  end.

571
572
Definition eval_to : Address :=
  match eval with
573
574
  | eval_transfer _ to _ _ _ _ _ _ _
  | eval_deploy _ to _ _ _ _ _ _ _ _ _ _ _ _
575
  | eval_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ _ => to
576
577
  end.

578
579
Definition eval_amount : Amount :=
  match eval with
580
581
  | eval_transfer _ _ amount _ _ _ _ _ _
  | eval_deploy _ _ amount _ _ _ _ _ _ _ _ _ _ _
582
  | eval_call _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ _ => amount
583
584
  end.
End Accessors.
585

586
Section Theories.
587
Context {pre : Environment} {act : Action}
588
        {post : Environment} {new_acts : list Action}
589
        (eval : ActionEvaluation pre act post new_acts).
590
591

Lemma account_balance_post (addr : Address) :
592
  account_balance post addr =
593
  account_balance pre addr
594
595
  + (if (addr =? eval_to eval)%address then eval_amount eval else 0)
  - (if (addr =? eval_from eval)%address then eval_amount eval else 0).
596
Proof.
597
  destruct eval; cbn; rewrite_environment_equiv; cbn;
598
    unfold add_balance; destruct_address_eq; lia.
599
600
601
Qed.

Lemma account_balance_post_to :
602
603
604
  eval_from eval <> eval_to eval ->
  account_balance post (eval_to eval) =
  account_balance pre (eval_to eval) + eval_amount eval.
605
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
606
  intros neq.
607
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
608
609
  rewrite address_eq_refl, address_eq_ne by auto.
  lia.
610
611
612
Qed.

Lemma account_balance_post_from :
613
614
615
  eval_from eval <> eval_to eval ->
  account_balance post (eval_from eval) =
  account_balance pre (eval_from eval) - eval_amount eval.
616
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
617
  intros neq.
618
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
619
620
  rewrite address_eq_refl, address_eq_ne by auto.
  lia.
621
622
623
Qed.

Lemma account_balance_post_irrelevant (addr : Address) :
624
625
  addr <> eval_from eval ->
  addr <> eval_to eval ->
626
627
  account_balance post addr = account_balance pre addr.
Proof.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
628
  intros neq_from neq_to.
629
  rewrite account_balance_post.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
630
631
  repeat rewrite address_eq_ne by auto.
  lia.
632
633
Qed.

634
635
636
637
638
639
640
Lemma chain_height_post_action : chain_height post = chain_height pre.
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.

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

Lemma finalized_height_post_action : finalized_height post = finalized_height pre.
641
Proof. destruct eval; rewrite_environment_equiv; auto. Qed.
642
643
644
645
646
647

Lemma contracts_post_pre_none contract :
  env_contracts post contract = None ->
  env_contracts pre contract = None.
Proof.
  intros H.
648
  destruct eval; rewrite_environment_equiv; auto.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
649
  cbn in *.
650
651
  destruct_address_eq; congruence.
Qed.
652
653
654
655
656
657
658
659

Lemma eval_amount_nonnegative : eval_amount eval >= 0.
Proof. now destruct eval. Qed.

Lemma eval_amount_le_account_balance :
  eval_amount eval <= account_balance pre (eval_from eval).
Proof. now destruct eval. Qed.

660
End Theories.
661

662
Section Trace.
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679

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

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

681
682
(* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *)
683
Local Open Scope nat.
684
Definition act_is_from_account (act : Action) : Prop :=
685
686
  address_is_contract (act_from act) = false.

687
688
689
690
691
692
693
694
695
696
697
Record IsValidNextBlock (header : BlockHeader) (chain : Chain) : Prop :=
  build_is_valid_next_block {
    valid_height : block_height header = S (chain_height chain);
    valid_slot : block_slot header > current_slot chain;
    valid_finalized_height :
      block_finalized_height header >= finalized_height chain /\
      block_finalized_height header < block_height header;
    valid_creator : address_is_contract (block_creator header) = false;
    valid_reward : (block_reward header >= 0)%Z;
  }.

698
699
700
701
702
Record ChainState :=
  build_chain_state {
    chain_state_env :> Environment;
    chain_state_queue : list Action;
  }.
703

704
705
706
Global Instance chain_state_settable : Settable _ :=
  settable! build_chain_state <chain_state_env; chain_state_queue>.

707
708
Inductive ChainStep : ChainState -> ChainState -> Type :=
| step_block :
709
710
    forall {prev next : ChainState}
           (header : BlockHeader),
711
      chain_state_queue prev = [] ->
712
713
      IsValidNextBlock header prev ->
      Forall act_is_from_account (chain_state_queue next) ->
714
715
      EnvironmentEquiv
        next
716
        (add_new_block_to_env header prev) ->
717
718
      ChainStep prev next
| step_action :
719
720
721
722
    forall {prev next : ChainState}
           (act : Action)
           (acts : list Action)
           (new_acts : list Action),
723
      chain_state_queue prev = act :: acts ->
724
      ActionEvaluation prev act next new_acts ->
725
      chain_state_queue next = new_acts ++ acts ->
726
727
      ChainStep prev next
| step_permute :
728
729
730
731
    forall {prev next : ChainState},
      chain_state_env prev = chain_state_env next ->
      Permutation (chain_state_queue prev) (chain_state_queue next) ->
      ChainStep prev next.
732
733
734
735

Definition empty_state : ChainState :=
  {| chain_state_env :=
       {| env_chain :=
736
737
738
            {| chain_height := 0;
               current_slot := 0;
               finalized_height := 0;
739
740
               account_balance a := 0%Z; |};
          env_contract_states a := None;
741
742
          env_contracts a := None; |};
     chain_state_queue := [] |}.
743

744
745
746
(* 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. *)
747
Definition ChainTrace := ChainedList ChainState ChainStep.
748

749
750
751
752
(* Additionally, a state is reachable if there is a trace ending in this trace. *)
Definition reachable (state : ChainState) : Prop :=
  inhabited (ChainTrace empty_state state).

753
754
755
(* 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
756
757
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. *)
758
759
Inductive TxBody :=
  | tx_empty
760
761
  | tx_deploy (wc : WeakContract) (setup : SerializedValue)
  | tx_call (msg : option SerializedValue).
762
763
764
765
766
767
768
769
770

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

771
Definition eval_tx {pre : Environment} {act : Action}
772
                   {post : Environment} {new_acts : list Action}
773
                   (step : ActionEvaluation pre act post new_acts) : Tx :=
774
  match step with
775
  | eval_transfer from to amount _ _ _ _ _ _ =>
776
    build_tx from to amount tx_empty
777
  | eval_deploy from to amount wc setup _ _ _ _ _ _ _ _ _ =>
778
    build_tx from to amount (tx_deploy wc setup)
779
  | eval_call from to amount _ msg _ _ _ _ _ _ _ _ _ _ _ =>
780
781
782
783
784
    build_tx from to amount (tx_call msg)
  end.

Fixpoint trace_txs {from to : ChainState} (trace : ChainTrace from to) : list Tx :=
  match trace with
785
786
  | snoc trace' step =>
    match step with
787
    | step_action _ _ _ _ eval _ => eval_tx eval :: trace_txs trace'
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
    | _ => 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).

805
806
Fixpoint trace_blocks {from to : ChainState}
         (trace : ChainTrace from to) : list BlockHeader :=
807
  match trace with
808
809
  | snoc trace' step =>
    match step with
810
811
812
    | step_block header _ _ _ _ =>
      header :: trace_blocks trace'
    | _ => trace_blocks trace'
813
814
815
816
    end
  | clnil => []
  end.

817
818
819
820
821
822
Definition created_blocks
           {from to : ChainState} (trace : ChainTrace from to)
           (creator : Address) : list BlockHeader :=
  filter (fun b => (block_creator b =? creator)%address)
         (trace_blocks trace).

823
Section Theories.
824
Ltac destruct_chain_step :=
825
  match goal with
826
827
  | [step: ChainStep _ _ |- _] =>
    destruct step as
828
829
830
        [prev next header queue_prev valid_header acts_from_accs env_eq|
         prev next act acts new_acts queue_prev eval queue_new|
         prev next prev_next perm]
831
832
  end.

833
Ltac destruct_action_eval :=
834
  match goal with
835
  | [eval: ActionEvaluation _ _ _ _ |- _] => destruct eval
836
837
  end.

838
839
Lemma contract_addr_format {to} (addr : Address) (wc : WeakContract) :
  reachable to ->
840
841
842
  env_contracts to addr = Some wc ->
  address_is_contract addr = true.
Proof.
843
  intros [trace] contract_at_addr.
844
845
846
  remember empty_state eqn:eq.
  induction trace; rewrite eq in *; clear eq.
  - cbn in *; congruence.
847
  - destruct_chain_step.
848
    + rewrite_environment_equiv; cbn in *; auto.
849
    + destruct_action_eval; rewrite_environment_equiv; cbn in *; destruct_address_eq; subst; auto.
850
    + intuition.
851
Qed.
Jakob Botsch Nielsen's avatar
Jakob Botsch Nielsen committed
852

853
854
855
856
857
858
859
860
861
862
863
864
865
866
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. *)
867
Lemma undeployed_contract_no_out_queue contract state :
868
  reachable state ->
869
870
871
872
873
874
875
876
  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.
877
  destruct_chain_step; [|destruct_action_eval|];
878
879
880
881
882
    try rewrite_environment_equiv;
    repeat
      match goal with
      | [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
      end;
883
    subst;
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
    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 *)
    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. *)
910
911
Lemma undeployed_contract_no_out_txs
      contract state (trace : ChainTrace empty_state state) :
912
913
  address_is_contract contract = true ->
  env_contracts state contract = None ->
914
  outgoing_txs trace contract = [].
915
Proof.
916
  intros is_contract undeployed.
917
  remember empty_state eqn:eq.
918
  induction trace; cbn; auto.
919
  destruct_chain_step.
920
921
922
923
  - (* 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.
924
    Hint Unfold reachable : core.
925
926
    subst.
    cbn.
927
928
929
930
    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
931
932
933
934
935
    repeat
      match goal with
      | [H: chain_state_queue _ = _ |- _] => rewrite H in *; clear H
      end.
    inversion_clear Hqueue.
936
    destruct_action_eval; rewrite_environment_equiv;
937
938
939
940
941
942
943
944
945
      subst;
      cbn in *;
      destruct_address_eq;
      subst; try tauto; congruence.
  - match goal with
    | [H: _ = _ |- _] => rewrite H in *; auto
    end.
Qed.

946
947
Lemma undeployed_contract_no_in_txs
      contract state (trace : ChainTrace empty_state state) :
948
949
  address_is_contract contract = true ->
  env_contracts state contract = None ->
950
  incoming_txs trace contract = [].
951
Proof.
952
  intros is_contract undeployed.
953
  remember empty_state eqn:eq.
954
  induction trace; cbn; auto.