Commit 59b60edd authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Large refactoring and work on formalizing ChainTrace

parent 16722906
......@@ -9,24 +9,23 @@ From SmartContracts Require Import Extras.
From SmartContracts Require Import Automation.
Import ListNotations.
Definition Address := nat.
Definition Address := positive.
Delimit Scope address_scope with address.
Bind Scope address_scope with Address.
Module Address.
Definition eqb := Nat.eqb.
Definition eq_dec := Nat.eq_dec.
Definition eqb := Pos.eqb.
Definition eq_dec := Pos.eq_dec.
End Address.
Infix "=?" := Address.eqb (at level 70) : address_scope.
Section Blockchain.
Definition Amount := Z.
Definition BlockId := nat.
Definition Version := nat.
Open Scope Z.
Record ContractDeployment :=
build_contract_deployment {
deployment_version : Version;
......@@ -56,6 +55,7 @@ Record Tx :=
Record BlockHeader :=
build_block_header {
block_number : BlockId;
block_coinbase : Address;
}.
Record Block :=
......@@ -64,103 +64,51 @@ Record Block :=
block_txs : list Tx;
}.
Module Chain.
(* The ChainInterface is an interface that allows different implementations
of chains. This represents the view of the blockchain that a contract
can access and interact with. This does not contain all information of
the chain (and it can't for positivity reasons).
*)
Record ChainInterface :=
build_chain_interface {
type : Type;
chain_at : type -> BlockId -> option type;
(* Last finished block. During contract execution, this is the previous
block, i.e. this block does _not_ contain the transaction that caused
the contract to be called *)
head_block : type -> Block;
incoming_txs : type -> Address -> list Tx;
outgoing_txs : type -> Address -> list Tx;
contract_state : type -> Address -> option OakValue;
valid_address : type -> Address -> Prop;
no_incoming_txs
(t : type) (a : Address) : ~valid_address t a -> incoming_txs t a = [];
no_outgoing_txs
(t : type) (a : Address) : ~valid_address t a -> outgoing_txs t a = [];
no_contract_state
(t : type) (a : Address) : ~valid_address t a -> contract_state t a = None;
}.
(* The ChainType is an interface that allows different implementations
of chains. This represents the view of the blockchain that a contract
can access and interact with. This does not contain all information of
the chain (and it can't for positivity reasons).
*)
Class ChainType :=
build_chain_type {
chain_type : Type;
chain_at : chain_type -> BlockId -> option chain_type;
(* Last finished block. During contract execution, this is the previous
block, i.e. this block does _not_ contain the transaction that caused
the contract to be called *)
head_block : chain_type -> Block;
incoming_txs : chain_type -> Address -> list Tx;
outgoing_txs : chain_type -> Address -> list Tx;
contract_state : chain_type -> Address -> option OakValue;
valid_address : Address -> Prop;
no_incoming_txs
(t : chain_type) (a : Address) : ~valid_address a -> incoming_txs t a = [];
no_outgoing_txs
(t : chain_type) (a : Address) : ~valid_address a -> outgoing_txs t a = [];
no_contract_state
(t : chain_type) (a : Address) : ~valid_address a -> contract_state t a = None;
}.
(* An actual chain interface together with a value of the chain.
For example, one obvious chain implementation could be as a list
of blocks and some operations on such a list. Then, the value is
simply the list of blocks.
This avoids having to either
1. Import an actual instance of ChainInterface when taking a chain, or
2. Abstracting over any implementation of ChainInterface when taking
a chain. *)
Record Chain :=
build_chain {
ifc : ChainInterface;
val : ifc.(type);
}.
Coercion chain_type : ChainType >-> Sortclass.
(* In the rest of this file we quantify over some implementation of chain. *)
Context {Chain : ChainType}.
Local Open Scope Z.
Definition account_balance (chain : Chain) (addr : Address)
: Amount :=
let sum_amounts txs := sumZ tx_amount txs in
sum_amounts (incoming_txs chain addr) - sum_amounts (outgoing_txs chain addr).
Module Exports.
Notation Chain := Chain.
Section Accessors.
Context (chain : Chain).
Let g {A : Type} (p : forall chain : ChainInterface, type chain -> A)
:= p chain.(ifc) chain.(val).
Definition chain_at (bid : BlockId) : option Chain :=
do x <- chain.(ifc).(chain_at) chain.(val) bid;
Some {| val := x |}.
Definition head_block := g head_block.
Definition incoming_txs := g incoming_txs.
Definition outgoing_txs := g outgoing_txs.
Definition contract_state := g contract_state.
Definition valid_address := g valid_address.
Lemma no_incoming_txs (a : Address) :
~valid_address a -> incoming_txs a = [].
Proof.
unfold valid_address, incoming_txs, g;
destruct chain as [ifc val];
destruct ifc; prove.
Qed.
Lemma no_outgoing_txs (a : Address) :
~valid_address a -> outgoing_txs a = [].
Proof.
unfold valid_address, outgoing_txs, g;
destruct chain as [ifc val];
destruct ifc; prove.
Qed.
Lemma no_contract_state (a : Address) :
~valid_address a -> contract_state a = None.
Proof.
unfold valid_address, contract_state, g;
destruct chain as [ifc val];
destruct ifc; prove.
Qed.
Definition account_balance (addr : Address) : Amount :=
let sum_amounts txs := sumZ tx_amount txs in
sum_amounts (incoming_txs addr) - sum_amounts (outgoing_txs addr).
Definition contract_deployment (addr : Address) : option ContractDeployment :=
let to_dep tx := match tx.(tx_body) with
| tx_deploy dep => Some dep
| _ => None
end in
find_first to_dep (incoming_txs addr).
End Accessors.
End Exports.
End Chain.
Export Chain.Exports.
Definition contract_deployment (chain : Chain) (addr : Address)
: option ContractDeployment :=
let to_dep tx := match tx.(tx_body) with
| tx_deploy dep => Some dep
| _ => None
end in
find_first to_dep (incoming_txs chain addr).
Inductive ContractCallContext :=
build_ctx {
......@@ -195,10 +143,10 @@ where Address -> WeakContract would be some operation that the chain provides
to allow access to contracts in deployments.
*)
with WeakContract :=
| build_weak_contract
(version : Version)
(init : ContractCallContext -> OakValue -> option OakValue)
(receive : ContractCallContext -> OakValue (* state *) ->
| build_weak_contract
(version : Version)
(init : ContractCallContext -> OakValue -> option OakValue)
(receive : ContractCallContext -> OakValue (* state *) ->
option OakValue (* message *) ->
option (OakValue * list ChainAction)).
......@@ -216,10 +164,10 @@ 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 *)
Record Contract
(setup_ty msg_ty state_ty : Type)
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty} :=
(setup_ty msg_ty state_ty : Type)
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty} :=
build_contract {
version : Version;
init : ContractCallContext -> setup_ty -> option state_ty;
......@@ -234,11 +182,11 @@ Arguments receive {_ _ _ _ _ _} contract ctx state msg : rename.
Arguments build_contract {_ _ _ _ _ _}.
Definition contract_to_weak_contract
{setup_ty msg_ty state_ty : Type}
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty}
(c : Contract setup_ty msg_ty state_ty) : WeakContract :=
{setup_ty msg_ty state_ty : Type}
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty}
(c : Contract setup_ty msg_ty state_ty) : WeakContract :=
let weak_init ctx oak_setup :=
do setup <- deserialize oak_setup;
do state <- c.(init) ctx setup;
......@@ -260,13 +208,13 @@ Coercion contract_to_weak_contract : Contract >-> WeakContract.
(* Deploy a strongly typed contract with some amount and setup *)
Definition create_deployment
{setup_ty msg_ty state_ty : Type}
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty}
(amount : Amount)
(contract : Contract setup_ty msg_ty state_ty)
(setup : setup_ty)
{setup_ty msg_ty state_ty : Type}
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty}
(amount : Amount)
(contract : Contract setup_ty msg_ty state_ty)
(setup : setup_ty)
: ChainAction :=
act_deploy amount contract (serialize setup).
......@@ -284,7 +232,7 @@ Record ContractInterface {setup_ty msg_ty state_ty : Type} :=
(* Obtain the state at some point of time *)
get_state : Chain -> option state_ty;
(* Make an action transferring money to the contract without
a message *)
a message *)
transfer : Amount -> ChainAction;
(* Make an action calling the contract *)
call : Amount -> msg_ty -> ChainAction;
......@@ -294,12 +242,12 @@ Arguments ContractInterface _ _ _ : clear implicits.
Arguments build_contract_interface {_ _ _}.
Definition get_contract_interface
(chain : Chain)
(addr : Address)
(setup_ty msg_ty state_ty : Type)
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty}
(chain : Chain)
(addr : Address)
(setup_ty msg_ty state_ty : Type)
`{OakTypeEquivalence setup_ty}
`{OakTypeEquivalence msg_ty}
`{OakTypeEquivalence state_ty}
: option (ContractInterface setup_ty msg_ty state_ty) :=
do 'build_contract_deployment ver ov_setup <- contract_deployment chain addr;
do setup <- deserialize ov_setup;
......@@ -333,7 +281,7 @@ Record InternalAction :=
}.
Record Environment :=
build_environment {
build_env {
env_chain : Chain;
env_contracts : Address -> option WeakContract;
}.
......@@ -350,9 +298,10 @@ Definition iact_to_tx (act : InternalAction) : Tx :=
end in
build_tx from to amount tx_body.
Local Coercion iact_to_tx : InternalAction >-> Tx.
Local Coercion env_chain : Environment >-> Chain.
Coercion iact_to_tx : InternalAction >-> Tx.
Coercion env_chain : Environment >-> chain_type.
(* Define how single actions affect the chain *)
Section Transfer.
Context {action : InternalAction} {pre post : Environment}.
......@@ -404,10 +353,9 @@ Section Transfer.
Record Transfer : Prop :=
build_transfer {
from_neq_to : from <> to;
valid_address_from : valid_address pre from;
valid_address_to : valid_address pre to;
valid_address_from : valid_address from;
valid_address_to : valid_address to;
amount_nonnegative : amount >= 0;
valid_address_post : valid_address post = valid_address pre;
head_block_post : head_block post = head_block pre;
account_balance_pre_from : account_balance pre from >= amount;
account_balance_post_to : account_balance post to >= amount;
......@@ -433,24 +381,6 @@ Arguments EmptyTransfer : clear implicits.
Arguments CallTransfer : clear implicits.
Arguments DeployTransfer : clear implicits.
(* Proposition for whether an internal action actually reflects an external action. *)
Definition action_properly_reflected
(ext_from : Address)
(ext : ChainAction)
(iact : InternalAction) : Prop :=
let (iact_from, iact_to, iact_amount, iact_body) := iact in
iact_from = ext_from /\
match iact_body, ext with
| iact_empty, act_transfer ext_to ext_amount
| iact_call None, act_transfer ext_to ext_amount =>
iact_to = ext_to /\ iact_amount = ext_amount
| iact_deploy iact_wc iact_setup, act_deploy ext_amount ext_wc ext_setup =>
iact_amount = ext_amount /\ iact_wc = ext_wc /\ iact_setup = ext_setup
| iact_call (Some iact_msg), act_call ext_to ext_amount ext_msg =>
ext_to = iact_to /\ ext_amount = iact_amount /\ ext_msg = iact_msg
| _, _ => False
end.
Section TransferTheories.
Context {action : InternalAction} {pre post : Environment}
(transfer : Transfer action pre post).
......@@ -486,6 +416,26 @@ Section TransferTheories.
Proof. solve_transfer. Qed.
End TransferTheories.
(* Proposition for whether an internal action actually reflects an external action.
This ensures that the block is actually recording the external actions that a contract
returns and not making up its own. *)
Definition IntActReflectsExtAct
(iact : InternalAction)
(ext : ChainAction)
(ext_from : Address) : Prop :=
let (iact_from, iact_to, iact_amount, iact_body) := iact in
iact_from = ext_from /\
match iact_body, ext with
| iact_empty, act_transfer ext_to ext_amount
| iact_call None, act_transfer ext_to ext_amount =>
iact_to = ext_to /\ iact_amount = ext_amount
| iact_deploy iact_wc iact_setup, act_deploy ext_amount ext_wc ext_setup =>
iact_amount = ext_amount /\ iact_wc = ext_wc /\ iact_setup = ext_setup
| iact_call (Some iact_msg), act_call ext_to ext_amount ext_msg =>
ext_to = iact_to /\ ext_amount = iact_amount /\ ext_msg = iact_msg
| _, _ => False
end.
(* Finally we can define the stepping relation. It captures how a single
action is reduced. *)
Inductive ChainStep (pre post : Environment)
......@@ -505,112 +455,73 @@ Inductive ChainStep (pre post : Environment)
Transfer act pre post ->
env_contracts pre to = Some wc ->
wc.(wc_receive) ctx prev_state msg = Some (new_state, ext_acts) ->
Forall2 (action_properly_reflected to) ext_acts int_acts ->
Forall2 (fun e i => IntActReflectsExtAct i e to) ext_acts int_acts ->
ChainStep pre post (pref ++ [act] ++ suf) (pref ++ int_acts ++ suf).
(* A block trace is just the reflexive transitive closure of this. It captures
execution within a single block. *)
Inductive BlockTrace :
Environment -> Environment -> list InternalAction -> list InternalAction -> Prop :=
| trace_refl : forall acts env,
| btrace_refl : forall acts env,
BlockTrace env env acts acts
| trace_step : forall pre mid post x y z,
ChainStep pre mid x y -> BlockTrace mid post y z -> BlockTrace pre post x z.
(* We would expect that the circulation of coins does not change during block execution.
Indeed, this is the case, as we now set out to prove. *)
Definition total_balance (chain : Chain) (addrs : list Address) :=
sumZ (account_balance chain) addrs.
(* First, we must define the circulation. We will define it as a finite
sum of the balance over all valid addresses. An unfortunate side effects is that
this results only holds when the address space is finite, though this restriction
could potentially be removed.
This first predicate specifies whether a list contains all valid addresses in
two chains. *)
Definition IsAllAddrs (addrs : list Address) (pre post : Chain) : Prop :=
forall a, valid_address pre a \/ valid_address post a -> In a addrs.
(* We then prove that over any single step, the circulation is preserved.
The idea behind this proof is that all_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. *)
Section StepCirculation.
Context {pre post : Environment}
(addrs : list Address)
{addrs_set : NoDup addrs}
{all_addrs : IsAllAddrs addrs pre post}.
Lemma transfer_reorganize
{act : InternalAction}
(transfer : Transfer act pre post)
: exists suf, Permutation ([iact_from act; iact_to act] ++ suf) addrs.
Proof.
pose proof (valid_address_from transfer).
pose proof (valid_address_to transfer).
pose proof (from_neq_to transfer).
apply (NoDup_incl_reorganize _ ([iact_from act; iact_to act]));
repeat constructor; unfold incl; prove.
Qed.
Lemma act_circulation_unchanged
{act : InternalAction}
(transfer : Transfer act pre post) :
total_balance pre addrs = total_balance post addrs.
Proof.
unfold total_balance.
destruct (transfer_reorganize transfer) as [suf perm].
apply Permutation_sym in perm.
rewrite 2!(sumZ_permutation perm); prove.
rewrite (account_balance_from_pre_post transfer).
rewrite (account_balance_to_pre_post transfer).
rewrite account_balance_from_pre_post.
enough (sumZ (account_balance pre) suf = sumZ (account_balance post) suf) by prove.
pose proof (Permutation_NoDup perm addrs_set) as perm_set.
assert (from_not_in_suf: ~In (iact_from act) suf).
{ apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
assert (to_not_in_suf: ~In (iact_to act) suf).
{ apply (in_NoDup_app _ [iact_from act; iact_to act] _); prove. }
clear perm perm_set.
pose proof (account_balance_unrelated_pre_post transfer).
induction suf as [| x xs IH]; prove.
Qed.
Hint Resolve act_circulation_unchanged.
Lemma step_circulation_unchanged
{x y : list InternalAction}
(step : ChainStep pre post x y) :
total_balance pre addrs = total_balance post addrs.
Proof. destruct step; eauto. Qed.
End StepCirculation.
(* Finally, we get the result over block traces by a simple induction. *)
Lemma block_trace_circulation_unchanged
{pre post : Environment}
{x y : list InternalAction}
(trace : BlockTrace pre post x y)
(addrs : list Address)
(addrs_set : NoDup addrs)
(all_addrs : IsAllAddrs addrs pre post)
: total_balance pre addrs = total_balance post addrs.
Proof.
induction trace; prove.
unfold IsAllAddrs in *.
assert (mid_in: forall a, valid_address mid a -> In a addrs).
{
destruct H;
match goal with
| [H: Transfer ?a ?pre ?post |- _] => rewrite (valid_address_post H); prove
end.
}
assert (post_in: forall a, valid_address post a -> In a addrs) by prove.
rewrite <- IHtrace; [|prove].
refine (step_circulation_unchanged addrs H); unfold IsAllAddrs; prove.
Qed.
| btrace_step : forall pre mid post x y z,
ChainStep pre mid x y ->
BlockTrace mid post y z ->
BlockTrace pre post x z.
(*
Record ChainEq (l r : Chain) : Prop :=
build_chain_eq {
head_block_eq : head_block l = head_block r;
incoming_txs_eq : incoming_txs l = incoming_txs r;
outgoing_txs_eq : outgoing_txs l = outgoing_txs r;
contract_state_eq : contract_state l = contract_state r;
}.
*)
(* Define how adding a block affects the chain. *)
Section BlockTransfer.
Context {acts : list InternalAction}
{pre post : Environment}.
Let coinbase := block_coinbase (block_header (head_block post)).
Let pre_num := block_number (block_header (head_block pre)).
Let post_num := block_number (block_header (head_block post)).
Let block_txs := block_txs (head_block post).
Local Open Scope nat.
Record BlockTransfer : Prop :=
builder_block_transfer {
post_num_S : post_num = S pre_num;
coinbase_valid : valid_address coinbase;
chain_at_head : chain_at post post_num = Some (env_chain post);
chain_at_above_none : forall n, n > post_num -> chain_at post n = None;
chain_at_below_eq : forall n, n < post_num ->
chain_at pre n = chain_at post n /\
chain_at post n <> None;
block_txs_reflect : Permutation block_txs (map iact_to_tx acts);
}.
End BlockTransfer.
Arguments BlockTransfer : clear implicits.
Inductive ChainTrace : Environment -> Environment -> Prop :=
| ctrace_refl : forall env, ChainTrace env env
| ctrace_block : forall {pre block_executed acts block_added post},
BlockTrace pre block_executed acts [] ->
BlockTransfer acts block_executed block_added ->
ChainTrace block_added post ->
ChainTrace pre post.
(* todo: soundness *)
Inductive IsTraceExtension
{pre mid post : Environment}
(extension : ChainTrace pre post)
(prefix : ChainTrace pre mid)
(coinbase : Address)
(acts : list (Address * ChainAction)) : Prop :=
full.
(* A ChainBuilder represents the additional state, operations and specifications
that a concrete implementation of a block chain needs to support. In contrast
......@@ -619,59 +530,42 @@ Thus, a ChainBuilder should be convertible into a Chain but not vice-versa.
As an example, the builder needs to contain information about all contracts
(including their receive functions) to be able to properly call into contracts
when receiving messages. The ChainBuilder is what supports the actual
"progression of time" induced by new blocks being added. Such a ChainBuilder is
what contracts will reason over when proving interesting temporal properties
of their behavior. *)
(* TODO: Naming of this is kind of bad. It is somewhat descriptive, but not really.
Maybe something like ChainEnvironment or ChainContext could be better. *)
Record ChainBuilderInterface :=
build_chain_builder_interface {
cbi_type : Type;
cbi_chain : cbi_type -> Chain;
cbi_initial : cbi_type;
cbi_add_block : cbi_type -> (* cur *)
Address (* coinbase *) ->
list (Address * ChainAction) (* actions *) ->
option cbi_type;
cbi_block_actions : cbi_type -> list InternalAction;
cbi_deployed_contracts : cbi_type -> Address -> option WeakContract;
cbi_trace :
forall (cb : cbi_type),
BlockTrace
(cbi_block_actions cb)
(ChainTrace.build_environment
(cbi_chain cbi_initial)
(cbi_deployed_contracts cbi_initial))
[]
(ChainTrace.build_environment
(cbi_chain cb)
(cbi_deployed_contracts cb));
"progression of time" induced by new blocks being added. *)
Class ChainBuilderType :=
build_builder {
builder_type : Type;
builder_chain : builder_type -> Chain;
builder_contracts : builder_type -> Address -> option WeakContract;
builder_initial : builder_type;
builder_trace (b : builder_type) :
ChainTrace
(build_env (builder_chain builder_initial) (builder_contracts builder_initial))
(build_env (builder_chain b) (builder_contracts b));
builder_add_block
(b : builder_type)
(coinbase : Address)
(actions : list (Address * ChainAction)) :
option builder_type;
builder_add_block_sound
(b : builder_type)
(coinbase : Address)
(actions : list (Address * ChainAction)) :
match builder_add_block b coinbase actions with
| Some built =>
IsTraceExtension (builder_trace built) (builder_trace b) coinbase actions
| None => True