Commit 71ea5d00 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Specify and prove an initial blockchain semantics

This specifies an initial version of blockchain semantics. The semantics
are specified as several relations:

ChainStep :
  Environment -> Action -> Tx ->
  Environment -> list Action ->

This relation captures the semantics of a single step/action in the
chain. Such an action can either be a transfer, contract deployment or
contract call. It specifies that when an action is executed in some
starting environment, then the blockchain records a transaction (Tx) on
the chain and performs certain updates to the environment. Finally, the
step also results in possible new actions to be executed due to contract

An environment is for now simply a Chain (which contracts can interact
with) and a collection of contracts that have been deployed to some
addresses. The Chain contains various useful operations for contracts
such as the current block number or ability to query transactions and
user balances.

For example, for a simple transfer action we may have ChainStep pre act
tx post []. Then the ChainStep relation will capture that the only thing
that has changed in the post environment is that tx has been added to
the chain (so that the appropriate account balances have been updated),
but for instance also that no new contracts have appeared. Since this is
just a transfer, there also cannot be any new actions to execute.

The semantics of the environment updates are captured in an abstract
manner to allow for different implementations of blockchains.
Specifically, we use an equivalence relation
EnvironmentEquiv : Environment -> Environment -> Prop and just require
that the environment is equivalent (under this relation) to an obvious
implementation of an environment. We implement an obvious blockchain,
LocalBlockchain, which uses finite maps with log n access times rather
than the linear maps used in the default semantics.

A single block, when added to a blockchain, consists of a list of these
actions to execute. In each block this list of actions must then be
executed (in a correct manner) until no more actions are left. This is
captured in
BlockTrace :
  Environment -> list Action ->
  Environment -> list Action -> Prop.
For all intents and purposes this can be seen as just a transitive
reflexive closure of the ChainStep relation above. Right now it only
allows blocks to reduce steps in a depth-first order, but this relation
should be simple to update to other or more general orders of reduction.
Note that ChainStep and BlockTrace say nothing about new blocks, but
only about execution within blocks. The semantics of how blocks are
added to the chain is captured in
ChainTrace : Environment -> Environment -> Prop.

This is a collection of block traces and representing additions of
blocks. At each block added, ChainTrace also captures that the
environment must be updated accordingly so that contracts can access
information about block numbers correctly.

Finally, a blockchain must always be able to prove that there is a
ChainTrace from its initial environment (the genesis blockchain) to its
current environment.

There are several TODOs left in the semantics:
1. We need to account for gas and allow execution failures
2. We need to put restrictions on when contracts can appear as the
source of actions
3. We need to capture soundness of the add_block function in blockchain

We also provide to sanity checks for these semantics:
1. We prove them for a simple block chain (LocalBlockchain.v).
2. We prove a "circulation" theorem for any blockchain satisfying the
semantics. That is, we show the following theorem:

Theorem chain_trace_circulation
      {env_start env_end : Environment}
      (trace : ChainTrace env_start env_end)
  : circulation env_end =
    (circulation env_start +
       (block_height (block_header env_start))
       (block_height (block_header env_end)))%Z.
parent 99b27297
Pipeline #12077 failed with stage
in 5 minutes and 54 seconds
......@@ -3,5 +3,6 @@
-R src SmartContracts
From Coq Require Import Eqdep List Omega Permutation.
Import ListNotations.
Set Implicit Arguments.
Ltac inject H := injection H; clear H; intros; try subst.
Ltac appHyps f :=
match goal with
| [ H : _ |- _ ] => f H
Ltac inList x ls :=
match ls with
| x => idtac
| (_, x) => idtac
| (?LS, _) => inList x LS
Ltac app f ls :=
match ls with
| (?LS, ?X) => f X || app f LS || fail 1
| _ => f ls
Ltac all f ls :=
match ls with
| (?LS, ?X) => f X; all f LS
| (_, _) => fail 1
| _ => f ls
(** Workhorse tactic to simplify hypotheses for a variety of proofs.
* Argument [invOne] is a tuple-list of predicates for which we always do inversion automatically. *)
Ltac simplHyp invOne :=
(** Helper function to do inversion on certain hypotheses, where [H] is the hypothesis and [F] its head symbol *)
let invert H F :=
(** We only proceed for those predicates in [invOne]. *)
inList F invOne;
(** This case covers an inversion that succeeds immediately, meaning no constructors of [F] applied. *)
(inversion H; fail)
(** Otherwise, we only proceed if inversion eliminates all but one constructor case. *)
|| (inversion H; [idtac]; clear H; try subst) in
match goal with
(** Eliminate all existential hypotheses. *)
| [ H : ex _ |- _ ] => destruct H
(** Find opportunities to take advantage of injectivity of data constructors, for several different arities. *)
| [ H : ?F ?X = ?F ?Y |- ?G ] =>
(** This first branch of the [||] fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal. *)
(assert (X = Y); [ assumption | fail 1 ])
(** If we pass that filter, then we use injection on [H] and do some simplification as in [inject].
* The odd-looking check of the goal form is to avoid cases where [injection] gives a more complex result because of dependent typing, which we aren't equipped to handle here. *)
|| (injection H;
match goal with
| [ |- X = Y -> G ] =>
try clear H; intros; try subst
| [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
(assert (X = Y); [ assumption
| assert (U = V); [ assumption | fail 1 ] ])
|| (injection H;
match goal with
| [ |- U = V -> X = Y -> G ] =>
try clear H; intros; try subst
(** Consider some different arities of a predicate [F] in a hypothesis that we might want to invert. *)
| [ H : ?F _ |- _ ] => invert H F
| [ H : ?F _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ _ |- _ ] => invert H F
| [ H : Some _ = Some _ |- _ ] => injection H; clear H
(** Find some hypothesis to rewrite with, ensuring that [auto] proves all of the extra subgoals added by [rewrite]. *)
Ltac rewriteHyp :=
match goal with
| [ H : _ |- _ ] => rewrite H by solve [ auto ]
(** Combine [autorewrite] with automatic hypothesis rewrites. *)
Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
Ltac rewriter := autorewrite with core in *; rewriterP.
Hint Rewrite app_ass.
Hint Rewrite app_comm_cons.
Ltac prove' invOne :=
let sintuition :=
simpl in *; intuition auto; try subst;
repeat (simplHyp invOne; intuition auto; try subst); try congruence in
let rewriter := autorewrite with core in *;
repeat (match goal with
| [ H : ?P |- _ ] => rewrite H by prove' invOne
end; autorewrite with core in *) in
do 3 (sintuition; autounfold; rewriter); try omega; try (elimtype False; omega).
Ltac prove := prove' fail.
Lemma Permutation_app_middle {A : Type} (xs l1 l2 l3 l4 : list A) :
Permutation (l1 ++ l2) (l3 ++ l4) ->
Permutation (l1 ++ xs ++ l2) (l3 ++ xs ++ l4).
Hint Rewrite <- Permutation_middle.
intros perm.
induction xs; prove.
(* Change all x :: l into [x] ++ l *)
Ltac appify :=
match goal with
| [|- context[?e :: ?l]] =>
match l with
| nil => fail 1
| _ => change (e :: l) with ([e] ++ l)
Local Ltac reassoc_right :=
match goal with
| [|- Permutation _ (?l1 ++ ?l2 ++ ?l3)] => rewrite (app_assoc l1 l2 l3)
Local Ltac reassoc_left :=
match goal with
| [|- Permutation (?l1 ++ ?l2 ++ ?l3) _] => rewrite (app_assoc l1 l2 l3)
Local Ltac unassoc_right :=
match goal with
| [|- Permutation _ ((?l1 ++ ?l2) ++ ?l3)] => rewrite <- (app_assoc l1 l2 l3)
Local Ltac simplify_perm_once :=
let rec aux :=
apply Permutation_app_middle ||
tryif reassoc_right
then aux
else (unassoc_right; reassoc_left; aux) in
repeat rewrite <- app_assoc;
Local Ltac simplify_perm_round :=
repeat appify;
(* Change into [] ++ l ++ [] *)
match goal with
| [|- Permutation ?l1 ?l2] => change l1 with ([] ++ l1);
change l2 with ([] ++ l2);
rewrite <- (app_nil_r l1), <- (app_nil_r l2)
repeat simplify_perm_once;
repeat rewrite <- app_assoc;
repeat rewrite app_nil_r;
match goal with
| [H: Permutation ?l1 ?l2|-_] => rewrite H
Ltac simplify_perm :=
repeat simplify_perm_round;
try apply Permutation_refl.
Ltac case_match :=
match goal with
| [H: context [ match ?x with _ => _ end ] |- _] => destruct x eqn:?
| [|- context [ match ?x with _ => _ end ]] => destruct x eqn:?
Ltac destruct_units :=
match goal with
| [u: unit |- _] => destruct u
This diff is collapsed.
From Coq Require Import NArith ZArith.
From SmartContracts Require Import Monads.
From SmartContracts Require Import Finite.
From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
From Coq Require Import Eqdep_dec.
From Coq Require Import List.
From Coq Require Import Psatz.
From Coq Require Import JMeq.
From stdpp Require countable.
Import ListNotations.
Local Open Scope N.
Inductive BoundedN (bound : N) :=
| bounded (n : N) (_ : (bound ?= n) = Gt).
Arguments bounded {_}.
Module BoundedN.
Definition to_N {bound : N} (n : BoundedN bound) : N :=
let (val, _) := n in val.
Definition eqb {bound : N} (a b : BoundedN bound) : bool :=
N.eqb (to_N a) (to_N b).
Definition of_N_compare {bound : N} (n : N) : option ((bound ?= n) = Gt) :=
match bound ?= n as comp return (option (comp = Gt)) with
| Gt => Some eq_refl
| _ => None
Definition of_N {bound : N} (n : N) : option (BoundedN bound) :=
match of_N_compare n with
| Some prf => Some (bounded n prf)
| None => None
Definition to_nat {bound : N} (n : BoundedN bound) : nat :=
N.to_nat (to_N n).
Definition of_nat {bound : N} (n : nat) : option (BoundedN bound) :=
of_N (N.of_nat n).
Definition to_Z {bound : N} (n : BoundedN bound) : Z :=
Z.of_N (to_N n).
Definition of_Z {bound : N} (z : Z) : option (BoundedN bound) :=
if (z <? 0)%Z then None else of_N (Z.to_N z).
Definition of_Z_const (bound : N) (z : Z) :=
let ofz := @of_Z bound z in
match ofz return (match ofz with
| Some _ => BoundedN bound
| None => unit
end) with
| Some x => x
| None => tt
Lemma to_N_inj {bound : N} {a b : BoundedN bound} :
to_N a = to_N b -> a = b.
intros eq.
destruct a, b.
simpl in *.
apply UIP_dec.
decide equality.
Hint Resolve to_N_inj.
Lemma eqb_spec {bound : N} (a b : BoundedN bound) :
Bool.reflect (a = b) (eqb a b).
unfold eqb.
destruct (N.eqb_spec (to_N a) (to_N b)) as [eq | neq].
- constructor.
- constructor.
intros H; rewrite H in neq; tauto.
Lemma eqb_refl {bound : N} (n : BoundedN bound) :
eqb n n = true.
Proof. destruct (eqb_spec n n); tauto. Qed.
Lemma to_nat_inj {bound : N} (a b : BoundedN bound) :
to_nat a = to_nat b -> a = b.
intros eq.
apply to_N_inj.
unfold to_nat in eq.
now apply N2Nat.inj.
Lemma to_Z_inj {bound : N} (a b : BoundedN bound) :
to_Z a = to_Z b -> a = b.
intros eq.
apply to_N_inj.
unfold to_Z in eq.
now apply N2Z.inj.
Lemma of_to_N {bound : N} (n : BoundedN bound) :
of_N (to_N n) = Some n.
destruct n as [n prf]; simpl.
unfold of_N.
replace (of_N_compare n) with (Some prf); auto.
unfold of_N_compare.
now rewrite prf.
Lemma of_to_nat {bound : N} (n : BoundedN bound) :
of_nat (to_nat n) = Some n.
unfold to_nat, of_nat.
apply of_to_N.
Lemma of_n_not_lt_0 (n : N) :
(Z.of_N n <? 0)%Z = false.
destruct (Z.ltb_spec (Z.of_N n) 0).
- apply Zlt_not_le in H.
destruct (H (N2Z.is_nonneg n)).
- reflexivity.
Lemma of_to_Z {bound : N} (n : BoundedN bound) :
of_Z (to_Z n) = Some n.
unfold to_Z, of_Z.
rewrite of_n_not_lt_0.
apply of_to_N.
Lemma of_N_some {bound : N} {m : N} {n : BoundedN bound} :
of_N m = Some n -> to_N n = m.
intros H.
unfold of_N in H.
destruct (of_N_compare m); try congruence.
now inversion H.
Lemma of_N_none {bound : N} {m : N} :
@of_N bound m = None -> bound <= m.
intros H.
unfold of_N in H.
destruct (of_N_compare m) eqn:comp; try congruence.
unfold of_N_compare in comp.
destruct (bound ?= m) eqn:comp'; congruence.
Lemma of_nat_some {bound : N} {m : nat} {n : BoundedN bound} :
of_nat m = Some n -> to_nat n = m.
intros H.
unfold to_nat.
rewrite (of_N_some H).
Lemma of_nat_none {bound : N} {m : nat} :
@of_nat bound m = None -> bound <= N.of_nat m.
Proof. apply of_N_none. Qed.
Lemma in_map_of_nat (bound : N) (n : BoundedN bound) (xs : list nat) :
In n (map_option (@of_nat bound) xs) <-> In (to_nat n) xs.
induction xs as [|x xs IH].
- split; intros H; inversion H.
- simpl.
destruct (of_nat x) eqn:of_nat_x; split; intros H.
+ destruct H.
* subst.
now apply of_nat_some.
* tauto.
+ destruct H as [eq | Hin].
* left.
rewrite eq in of_nat_x.
rewrite of_to_nat in of_nat_x; prove.
* prove.
+ tauto.
+ destruct H as [eq | Hin].
* rewrite eq, of_to_nat in of_nat_x; inversion of_nat_x.
* prove.
Module Stdpp.
Import countable.
Lemma eq_dec {bound : N} : EqDecision (BoundedN bound).
intros x y.
destruct (BoundedN.eqb_spec x y); [left|right]; assumption.
Global Instance BoundedNEqDec {bound : N} : EqDecision (BoundedN bound) :=
Definition encode_bounded {bound : N} (n : BoundedN bound) : positive :=
encode (to_N n).
Definition decode_bounded {bound : N} (n : positive) : option (BoundedN bound) :=
decode n >>= of_N.
Lemma decode_encode_bounded {bound : N} (n : BoundedN bound) :
decode_bounded (encode_bounded n) = Some n.
unfold decode_bounded, encode_bounded.
rewrite decode_encode.
apply of_to_N.
Global Instance BoundedNCountable {bound : N} : Countable (BoundedN bound) :=
{| encode := encode_bounded;
decode := decode_bounded;
decode_encode := decode_encode_bounded; |}.
End Stdpp.
Global Instance BoundedN_finite {bound : N} : Finite (BoundedN bound) :=
{| elements := map_option of_nat (List.seq 0 (N.to_nat bound)) |}.
- pose proof (seq_NoDup (N.to_nat bound) 0) as nodup.
pose proof (in_seq (N.to_nat bound) 0) as in_seq'.
pose proof (fun n => proj1 (in_seq' n)) as in_seq; clear in_seq'.
induction nodup; try constructor.
pose proof (in_seq x) as x_bound.
specialize (x_bound (or_introl eq_refl)).
destruct x_bound as [useless x_bound]; clear useless.
simpl in x_bound.
destruct (of_nat x) eqn:ofnatx. all: cycle 1.
apply of_nat_none in ofnatx.
+ intros Hin.
apply in_map_of_nat in Hin.
apply of_nat_some in ofnatx.
rewrite <- ofnatx in H.
+ apply IHnodup.
intros n in_n_l.
apply (in_seq n (or_intror in_n_l)).
- intros t.
apply in_map_of_nat.
apply in_seq.
unfold to_nat.
destruct t as [t lt].
change ((bound ?= t) = Gt) with (bound > t) in lt.
End BoundedN.
Delimit Scope BoundedN_scope with BoundedN.
Bind Scope BoundedN_scope with BoundedN.
(* In this file we prove various results about the circulation of coins in any
chain implementing a chain type. More specifically, we show that the circulation
does not change during execution of blocks. This is proven under the (implicit)
assumption that the address space is finite. *)
From Coq Require Import List Permutation ZArith Psatz.
From SmartContracts Require Import Automation Blockchain Extras Finite.
From RecordUpdate Require Import RecordSet.
Import ListNotations.
Section Circulation.
Context {ChainBaseTypes : ChainBaseTypes}.
Context `{Finite Address}.
Definition circulation (chain : Chain) :=
sumZ (account_balance chain) (elements Address).
Definition coins_created (start_height end_height : nat) : Amount :=
sumZ compute_block_reward (seq (S start_height) (end_height - start_height)).
(* We then prove that over any single step, the circulation is preserved.
The idea behind this proof is that addrs contain from and to so
we can move them to the beginning of the sum and it easily follows that
the sum of their balances is the same as before. For the rest of the
list the total balance will then not be affected which follows by induction. *)
Lemma address_reorganize {a b : Address} :
a <> b ->
exists suf, Permutation ([a; b] ++ suf) (elements Address).
intros a_neq_b.
apply (NoDup_incl_reorganize _ [a; b]);
repeat constructor; unfold incl; prove.
Lemma step_from_to_same
{pre : Environment}
{act : Action}
{tx : Tx}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act tx post new_acts) :
tx_from tx = tx_to tx ->
circulation post = circulation pre.
intros from_eq_to.
unfold circulation.
induction (elements Address) as [| x xs IH].
- reflexivity.
- simpl in *.
rewrite IH, (account_balance_post step), from_eq_to.
Hint Resolve step_from_to_same.
Lemma step_circulation_unchanged
{pre : Environment}
{act : Action}
{tx : Tx}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act tx post new_acts) :
circulation post = circulation pre.
destruct (address_eqb_spec (tx_from tx) (tx_to tx))
as [from_eq_to | from_neq_to]; eauto.
destruct (address_reorganize from_neq_to) as [suf perm].
apply Permutation_sym in perm.
unfold circulation.
rewrite 2!(sumZ_permutation perm); prove.
rewrite (account_balance_post_to step from_neq_to).
rewrite (account_balance_post_from step from_neq_to).
enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
pose proof (Permutation_NoDup perm) as perm_set.
assert (from_not_in_suf: ~In (tx_from tx) suf).
{ apply (in_NoDup_app _ [tx_from tx; tx_to tx] _); prove. }
assert (to_not_in_suf: ~In (tx_to tx) suf).
{ apply (in_NoDup_app _ [tx_from tx; tx_to tx] _); prove. }
clear perm perm_set.
pose proof (account_balance_post_irrelevant step).
induction suf as [| x xs IH]; prove.
Hint Resolve step_circulation_unchanged.
(* Finally, we get the result over block traces by a simple induction. *)
Lemma block_trace_circulation_unchanged
{bef : list Action}
{after : list Action}
{post pre : Environment}
(trace : BlockTrace pre bef post after)
: circulation post = circulation pre.
induction trace;
match goal with
| [IH: _ |- _] => try rewrite IH; eauto
Hint Resolve block_trace_circulation_unchanged.
Lemma circulation_equal (c1 c2 : Chain) :
ChainEquiv c1 c2 -> circulation c1 = circulation c2.
intros [].
unfold circulation, account_balance.
induction (elements Address); prove.
Lemma circulation_add_new_block header baker env :
circulation (add_new_block header baker env) =
(circulation env + compute_block_reward (block_height header))%Z.
assert (Hperm: exists suf, Permutation ([baker] ++ suf) (elements Address)).
{ apply NoDup_incl_reorganize; repeat constructor; unfold incl; prove. }
destruct Hperm as [suf perm].
symmetry in perm.
pose proof (Permutation_NoDup perm (elements_set Address)) as perm_set.
unfold circulation.
rewrite perm.
unfold constructor, set, account_balance.
destruct (address_eqb_spec baker baker); try congruence.
pose proof (in_NoDup_app baker [baker] suf ltac:(prove) perm_set) as not_in_suf.
repeat rewrite <- Z.add_assoc.
rewrite <- Z.add_comm.
repeat rewrite <- Z.add_assoc.
clear perm perm_set e.
induction suf as [| x xs IH]; auto.
simpl in *.
apply Decidable.not_or in not_in_suf.
destruct (address_eqb_spec x baker); try tauto.
specialize (IH (proj2 not_in_suf)).
Theorem chain_trace_circulation
{env_start env_end : Environment}
(trace : ChainTrace env_start env_end)
: circulation env_end =
(circulation env_start +
(block_height (block_header env_start))