Contents:
Library ConCert.Execution.BlockchainBuilder
From Stdlib Require Import ZArith.
From Stdlib Require Import List.
From Stdlib Require Import Psatz.
From Stdlib Require Import Permutation.
From Stdlib Require Import Morphisms.
From Stdlib Require Import String.
From Stdlib Require Import Logic.Decidable.
From ConCert.Execution Require Import ChainedList.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import BlockchainBase.
From ConCert.Execution Require Import BlockchainTheories.
From ConCert.Utils Require Import Automation.
From ConCert.Utils Require Import Extras.
From ConCert.Utils Require Import RecordUpdate.
Import ListNotations.
Section Builder.
Context {Base : ChainBase}.
Inductive ActionEvaluationError :=
| amount_negative (amount : Amount) (* amount is negative *)
| amount_too_high (amount : Amount) (* sender does not have enough money *)
| no_such_contract (addr : Address) (* there is no contract at that address *)
| too_many_contracts (* cannot generate fresh address for new contract *)
| init_failed (err : SerializedValue) (* contract init function failed *)
| receive_failed (err : SerializedValue) (* contract receive function failed *)
| deserialization_failed (val : SerializedValue) (* failed deserializing value *)
| internal_error. (* unexpected internal error *)
Inductive AddBlockError :=
| invalid_header (header : BlockHeader) (* header for next block is invalid *)
| invalid_root_action (act : Action) (* a specified root action is invalid *)
| origin_from_mismatch (act : Action) (* origin and from addresses do not match for an action in a new block *)
| action_evaluation_depth_exceeded (* out of fuel while evaluating actions recursively *)
| action_evaluation_error (* error when evaluating single action *)
(act : Action)
(err : ActionEvaluationError).
Class ChainBuilderType :=
build_builder {
builder_type : Type;
builder_initial : builder_type;
builder_env : builder_type -> Environment;
builder_add_block
(builder : builder_type)
(header : BlockHeader)
(actions : list Action) :
result builder_type AddBlockError;
builder_trace (builder : builder_type) :
ChainTrace empty_state (build_chain_state (builder_env builder) []);
}.
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
Global Coercion builder_env : builder_type >-> Environment.
End Builder.
Module BuildUtils.
Definition receiver_can_receive_transfer `{ChainBase} (bstate : ChainState) act_body :=
match act_body with
| act_transfer to _ => address_is_contract to = false \/
(exists wc state,
env_contracts bstate to = Some wc /\
env_contract_states bstate to = Some state /\
forall (bstate_new : ChainState) ctx, exists new_state, wc_receive wc bstate_new ctx state None = Ok (new_state, []))
| _ => True
end.
(* This axiom states that for any reachable state and any contract it is
decidable whether or not there is an address where the contract can be deployed to.
This is not provable in general with the assumption ChainBase makes about
addresses and the function address_is_contract. However, this should be
provable in any sensible instance of ChainBase *)
Axiom deployable_address_decidable : forall `{ChainBase} bstate wc setup act_origin act_from amount,
reachable bstate ->
decidable (exists addr state, address_is_contract addr = true
/\ env_contracts bstate addr = None
/\ wc_init wc
(transfer_balance act_from addr amount bstate)
(build_ctx act_origin act_from addr amount amount)
setup = Ok state).
Ltac action_not_decidable :=
right; intro;
match goal with
| H : exists bstate new_acts, inhabited (ActionEvaluation _ _ bstate new_acts) |- False =>
destruct H as [bstate_new [new_acts [action_evaluation]]];
destruct_action_eval; try congruence
end; repeat
match goal with
| H : {| act_origin := _; act_from := _; act_body := _ |} = {| act_origin := _; act_from := _; act_body := match ?msg with | Some _ => _ | None =>_ end |} |- False =>
destruct msg
| H : {| act_origin := _; act_from := _; act_body := _ |} = {| act_origin := _; act_from := _; act_body := _ |} |- False =>
inversion H; subst; clear H
end.
Ltac action_decidable :=
left; do 2 eexists; constructor;
match goal with
| H : wc_receive _ _ _ _ ?m = Ok _ |- _ => eapply (eval_call _ _ _ _ _ m)
| H : wc_init _ _ _ _ = Ok _ |- _ => eapply eval_deploy
| H : context [act_transfer _ _] |- _ => eapply eval_transfer
end;
eauto; try now constructor.
Ltac rewrite_balance :=
match goal with
| H := context [if (_ =? ?to)%address then _ else _],
H2 : Environment |- _ =>
assert (new_to_balance_eq : env_account_balances H2 to = H);
[ try rewrite_environment_equiv in *; cbn; unfold H; destruct_address_eq; try congruence; lia |
now rewrite <- new_to_balance_eq in *]
end.
(* For any reachable state and an action it is decidable if it is
possible to evaluate the action in the state *)
Open Scope Z_scope.
Lemma action_evaluation_decidable `{ChainBase} : forall bstate act,
reachable bstate ->
decidable (exists bstate' new_acts, inhabited (ActionEvaluation bstate act bstate' new_acts)).
Proof.
intros * reach.
destruct act eqn:Hact.
destruct act_body;
(destruct (amount >=? 0) eqn:amount_positive;
[destruct (amount <=? env_account_balances bstate act_from) eqn:balance |
action_not_decidable; now rewrite Z.geb_leb, Z.leb_gt in amount_positive (* Eliminate cases where amount is negative *)];
[| action_not_decidable; now rewrite Z.leb_gt in balance ]); (* Eliminate cases where sender does not have enough balance *)
try (destruct (address_is_contract to) eqn:to_is_contract;
[destruct (env_contracts bstate to) eqn:to_contract;
[destruct (env_contract_states bstate to) eqn:contract_state |] |]);
try now action_not_decidable. (* Eliminate cases with obvious contradictions *)
all : rewrite Z.geb_leb, <- Zge_is_le_bool in amount_positive.
all : rewrite Z.leb_le in balance.
- (* act_body = act_transfer to amount *)
pose (new_to_balance := if (address_eqb act_from to)
then (env_account_balances bstate to)
else (env_account_balances bstate to) + amount).
destruct (wc_receive w
(transfer_balance act_from to amount bstate)
(build_ctx act_origin act_from to new_to_balance amount)
s None) eqn:receive.
+ (* Case: act_transfer is evaluable by eval_call *)
destruct t.
pose (bstate' := (set_contract_state to s0
(transfer_balance act_from to amount bstate))).
action_decidable.
rewrite_balance.
+ (* Case: act_transfer is not evaluable by eval_call
because wc_receive returned None *)
action_not_decidable.
rewrite_balance.
- (* act_body = act_transfer to amount *)
(* Case: act_transfer is evaluable by eval_transfer *)
pose (bstate' := (transfer_balance act_from to amount bstate)).
action_decidable.
- (* act_body = act_call to amount msg *)
pose (new_to_balance := if (address_eqb act_from to)
then (env_account_balances bstate to)
else (env_account_balances bstate to) + amount).
destruct (wc_receive w
(transfer_balance act_from to amount bstate)
(build_ctx act_origin act_from to new_to_balance amount)
s (Some msg)) eqn:receive.
+ (* Case: act_call is evaluable by eval_call *)
destruct t.
pose (bstate' := (set_contract_state to s0
(transfer_balance act_from to amount bstate))).
action_decidable.
rewrite_balance.
+ (* Case: act_call is not evaluable by eval_call
because wc_receive returned None *)
action_not_decidable.
rewrite_balance.
- (* act_body = act_call to amount msg *)
(* Case: contradiction *)
action_not_decidable.
now apply contract_addr_format in deployed; auto.
- (* act_body = act_deploy amount c setup *)
apply deployable_address_decidable
with (wc := c) (setup := setup) (act_origin := act_origin)
(act_from := act_from) (amount := amount)
in reach.
destruct reach as [[to [state [to_is_contract_addr [to_not_deployed init]]]] | no_deployable_addr].
+ (* Case: act_deploy is evaluable by eval_deploy *)
pose (bstate' := (set_contract_state to state
(add_contract to c
(transfer_balance act_from to amount bstate)))).
action_decidable.
+ (* Case: act_deploy is not evaluable by eval_deploy
because no there is no available contract address
that this contract can be deployed to *)
action_not_decidable.
apply no_deployable_addr.
eauto.
Qed.
Close Scope Z_scope.
(* Property stating that an action does not produce any new action when evaluated *)
Definition produces_no_new_acts `{ChainBase} act : Prop :=
forall bstate bstate' new_acts, ActionEvaluation bstate act bstate' new_acts -> new_acts = [].
(* Property on a ChainState queue stating all actions are from accounts and produces
no new actions when evaluated. This ensures that the queue can be emptied successfully *)
Definition emptyable `{ChainBase} queue : Prop :=
Forall act_is_from_account queue /\
Forall produces_no_new_acts queue.
(* An empty queue is always emptyable *)
Lemma empty_queue_is_emptyable `{ChainBase} : emptyable [].
Proof.
now constructor.
Qed.
(* A subset of an emptyable queue is also emptyable *)
Lemma emptyable_cons `{ChainBase} : forall x l,
emptyable (x :: l) -> emptyable l.
Proof.
intros * [acts_from_account no_new_acts].
apply Forall_inv_tail in acts_from_account.
now apply Forall_inv_tail in no_new_acts.
Qed.
(* For any reachable state it is possible to empty the chain_state_queue
if the queue only contains action that satisfy the following
1) the action is from a user and not a contract
2) the action does not produce any actions when evaluated
For any property that holds on the starting state this also hold on
the state with an empty queue if it can be proven that the property
holds after evaluating any action.
*)
Lemma empty_queue `{ChainBase} : forall bstate (P : ChainState -> Prop),
reachable bstate ->
emptyable (chain_state_queue bstate) ->
P bstate ->
(forall (bstate bstate' : ChainState) act acts, reachable bstate -> reachable bstate' -> P bstate ->
chain_state_queue bstate = act :: acts -> chain_state_queue bstate' = acts ->
(inhabited (ActionEvaluation bstate act bstate' []) \/ EnvironmentEquiv bstate bstate') -> P bstate') ->
exists bstate', reachable_through bstate bstate' /\ P bstate' /\ (chain_state_queue bstate') = [].
Proof.
intros * reach [acts_from_account no_new_acts].
remember (chain_state_queue bstate) as queue.
generalize dependent bstate.
induction queue; intros bstate reach Hqueue_eq HP HP_preserved.
- (* Case: queue is already empty, thus we are already done *)
now eexists.
- (* Case: queue contains at least one action,
thus we need to either discard or evaluate it *)
apply list_relations.list.Forall_cons_1 in acts_from_account as [act_from_a acts_from_account].
apply list_relations.list.Forall_cons_1 in no_new_acts as [no_new_acts_from_a no_new_acts].
edestruct action_evaluation_decidable as
[[mid_env [new_acts [action_evaluation]]] | no_action_evaluation]; eauto.
+ (* Case: the action is evaluable *)
pose (build_chain_state mid_env (new_acts ++ queue)) as mid.
assert (step : ChainStep bstate mid) by (now eapply step_action).
apply no_new_acts_from_a in action_evaluation as new_acts_eq; subst.
eapply HP_preserved with (bstate' := mid) in HP; eauto.
apply IHqueue in HP as [to [reachable_through [P_to queue_to]]]; subst; eauto.
now exists to.
+ (* Case: the action not is evaluable *)
pose (bstate<| chain_state_queue := queue |>) as mid.
assert (step : ChainStep bstate mid).
{ eapply step_action_invalid; try easy.
intros. apply no_action_evaluation.
now do 2 eexists.
}
apply reachable_step in step as reachable_mid; eauto.
apply IHqueue in reachable_mid as [to [reachable_through [P_to queue_to]]]; eauto.
exists to.
destruct_and_split; auto.
eauto.
eapply (HP_preserved bstate mid); eauto.
now right.
Qed.
Open Scope Z_scope.
(* Lemma showing that there exists a future ChainState with an added block *)
Lemma add_block `{ChainBase} : forall bstate reward creator acts slot_incr,
reachable bstate ->
chain_state_queue bstate = [] ->
address_is_contract creator = false ->
reward >= 0->
(slot_incr > 0)%nat ->
Forall act_is_from_account acts ->
Forall act_origin_is_eq_from acts ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
(add_new_block_to_env {| block_height := S (chain_height bstate);
block_slot := current_slot bstate + slot_incr;
block_finalized_height := finalized_height bstate;
block_creator := creator;
block_reward := reward; |} bstate)).
Proof.
intros * reach queue creator_not_contract
reward_positive slot_incr_positive
acts_from_accounts origins_from_accounts.
pose (header :=
{| block_height := S (chain_height bstate);
block_slot := current_slot bstate + slot_incr;
block_finalized_height := finalized_height bstate;
block_creator := creator;
block_reward := reward; |}).
pose (bstate_with_acts := (bstate<|chain_state_queue := acts|>
<|chain_state_env := add_new_block_to_env header bstate|>)).
assert (step_with_acts : ChainStep bstate bstate_with_acts).
{ eapply step_block; try easy.
- constructor; try easy.
+ cbn. lia.
+ split; try (cbn; lia). cbn.
now apply finalized_heigh_chain_height.
}
exists bstate_with_acts.
split; eauto.
split; eauto.
constructor; try reflexivity.
Qed.
(* Lemma showing that there exists a future ChainState with the
same contract states where the current slot is <slot> *)
Lemma forward_time_exact `{ChainBase} : forall bstate reward creator slot,
reachable bstate ->
chain_state_queue bstate = [] ->
address_is_contract creator = false ->
reward >= 0 ->
(current_slot bstate < slot)%nat ->
(exists bstate' header,
reachable_through bstate bstate'
/\ IsValidNextBlock header bstate
/\ (slot = current_slot bstate')%nat
/\ chain_state_queue bstate' = []
/\ EnvironmentEquiv
bstate'
(add_new_block_to_env header bstate)).
Proof.
intros bstate reward creator slot reach queue
creator_not_contract reward_positive slot_not_hit.
eapply add_block with (slot_incr := (slot - current_slot bstate)%nat) in reach as new_block; try easy.
destruct new_block as [bstate_with_act [reach' [queue' env_eq]]].
do 2 eexists.
split; eauto.
do 3 try split; only 9: apply env_eq; eauto; cbn; try lia.
- now apply finalized_heigh_chain_height.
- rewrite_environment_equiv in *. cbn. lia.
Qed.
(* Lemma showing that there exists a future ChainState with the
same contract states where the current slot is at least <slot> *)
Lemma forward_time `{ChainBase} : forall bstate reward creator slot,
reachable bstate ->
chain_state_queue bstate = [] ->
address_is_contract creator = false ->
reward >= 0 ->
(exists bstate' header,
reachable_through bstate bstate'
/\ IsValidNextBlock header bstate
/\ (slot <= current_slot bstate')%nat
/\ chain_state_queue bstate' = []
/\ EnvironmentEquiv
bstate'
(add_new_block_to_env header bstate)).
Proof.
intros * reach queue creator_not_contract reward_positive.
destruct (slot - current_slot bstate)%nat eqn:slot_hit.
- eapply add_block with (slot_incr := 1%nat) in reach as new_block; try easy.
destruct new_block as [bstate_with_act [reach' [queue' env_eq]]].
do 2 eexists.
split; eauto.
do 3 try split; only 9: apply env_eq; eauto; cbn; try lia.
+ now apply finalized_heigh_chain_height.
+ apply Nat.sub_0_le in slot_hit.
rewrite_environment_equiv in *. cbn. lia.
- specialize (forward_time_exact bstate reward creator slot) as
(bstate' & header & reach' & header_valid & slot_hit' & queue' & env_eq); eauto.
lia.
do 2 eexists.
destruct_and_split; eauto.
lia.
Qed.
(* Lemma showing that there exists a future ChainState
where the contract call is evaluated *)
Lemma evaluate_action `{ChainBase} : forall {Setup Msg State Error : Type}
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State}
`{Serializable Error}
(contract : Contract Setup Msg State Error)
bstate origin from caddr amount msg acts new_acts
cstate new_cstate,
reachable bstate ->
chain_state_queue bstate = {| act_from := from;
act_origin := origin;
act_body := act_call caddr amount ((@serialize Msg _) msg) |} :: acts ->
amount >= 0 ->
env_account_balances bstate from >= amount ->
env_contracts bstate caddr = Some (contract : WeakContract) ->
env_contract_states bstate caddr = Some ((@serialize State _) cstate) ->
BlockchainBase.receive contract (transfer_balance from caddr amount bstate)
(build_ctx origin from caddr (if (address_eqb from caddr)
then (env_account_balances bstate caddr)
else (env_account_balances bstate caddr) + amount) amount)
cstate (Some msg) = Ok (new_cstate, new_acts) ->
(exists bstate',
reachable_through bstate bstate'
/\ env_contract_states bstate' caddr = Some ((@serialize State _) new_cstate)
/\ chain_state_queue bstate' = (map (build_act origin caddr) new_acts) ++ acts
/\ EnvironmentEquiv
bstate'
(set_contract_state caddr ((@serialize State _) new_cstate) (transfer_balance from caddr amount bstate))).
Proof.
intros * reach queue amount_nonnegative enough_balance%Z.ge_le
deployed deployed_state receive_some.
pose (new_to_balance := if (address_eqb from caddr)
then (env_account_balances bstate caddr)
else (env_account_balances bstate caddr) + amount).
pose (bstate' := (bstate<|chain_state_queue := (map (build_act origin caddr) new_acts) ++ acts|>
<|chain_state_env := set_contract_state caddr ((@serialize State _) new_cstate)
(transfer_balance from caddr amount bstate)|>)).
assert (new_to_balance_eq : env_account_balances bstate' caddr = new_to_balance) by
(cbn; destruct_address_eq; easy).
assert (step : ChainStep bstate bstate').
- eapply step_action; eauto.
eapply eval_call with (msg := Some ((@serialize Msg _) msg)); eauto.
+ rewrite new_to_balance_eq.
now apply wc_receive_to_receive in receive_some.
+ constructor; reflexivity.
- exists bstate'.
split; eauto.
repeat split; eauto.
cbn.
now destruct_address_eq.
Qed.
(* Lemma showing that there exists a future ChainState
where the transfer action is evaluated *)
Lemma evaluate_transfer `{ChainBase} : forall bstate origin from to amount acts,
reachable bstate ->
chain_state_queue bstate = {| act_from := from;
act_origin := origin;
act_body := act_transfer to amount |} :: acts ->
amount >= 0 ->
env_account_balances bstate from >= amount ->
address_is_contract to = false ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
(transfer_balance from to amount bstate)).
Proof.
intros * reach queue amount_nonnegative enough_balance%Z.ge_le to_not_contract.
pose (bstate' := (bstate<|chain_state_queue := acts|>
<|chain_state_env := (transfer_balance from to amount bstate)|>)).
assert (step : ChainStep bstate bstate').
- eapply step_action with (new_acts := []); eauto.
eapply eval_transfer; eauto.
constructor; reflexivity.
- eexists bstate'.
split; eauto.
repeat split; eauto.
Qed.
(* Lemma showing that if an action in the queue is invalid then
there exists a future ChainState with the same environment
where that action is discarded *)
Lemma discard_invalid_action `{ChainBase} : forall bstate act acts,
reachable bstate ->
chain_state_queue bstate = act :: acts ->
act_is_from_account act ->
(forall (bstate0 : Environment) (new_acts : list Action), ActionEvaluation bstate act bstate0 new_acts -> False) ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
bstate).
Proof.
intros * reach queue act_from_account no_action_evaluation.
pose (bstate' := (bstate<|chain_state_queue := acts|>)).
assert (step : ChainStep bstate bstate').
- eapply step_action_invalid; eauto.
constructor; reflexivity.
- eexists bstate'.
split; eauto.
repeat split; eauto.
Qed.
(* Lemma showing that for any permutation of the queue there
exists a future ChainState with the same environment
end the queue permuted *)
Lemma permute_queue `{ChainBase} : forall bstate acts acts_permuted,
reachable bstate ->
chain_state_queue bstate = acts ->
Permutation.Permutation acts acts_permuted ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts_permuted
/\ EnvironmentEquiv
bstate'
bstate).
Proof.
intros * reach queue perm.
pose (bstate' := (bstate<|chain_state_queue := acts_permuted|>)).
assert (step : ChainStep bstate bstate').
- eapply step_permute.
+ econstructor; eauto.
+ now rewrite queue.
- eexists bstate'.
split; eauto.
repeat split; eauto.
Qed.
(* Lemma showing that there exists a future ChainState
where the contract is deployed *)
Lemma deploy_contract `{ChainBase} : forall {Setup Msg State Error : Type}
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State}
`{Serializable Error}
(contract : Contract Setup Msg State Error)
bstate origin from caddr amount acts setup cstate,
reachable bstate ->
chain_state_queue bstate = {| act_from := from;
act_origin := origin;
act_body := act_deploy amount contract ((@serialize Setup _) setup) |} :: acts ->
amount >= 0 ->
env_account_balances bstate from >= amount ->
address_is_contract caddr = true ->
env_contracts bstate caddr = None ->
BlockchainBase.init contract
(transfer_balance from caddr amount bstate)
(build_ctx origin from caddr amount amount)
setup = Ok cstate ->
(exists bstate' (trace : ChainTrace empty_state bstate'),
reachable_through bstate bstate'
/\ env_contracts bstate' caddr = Some (contract : WeakContract)
/\ env_contract_states bstate' caddr = Some ((@serialize State _) cstate)
/\ deployment_info Setup trace caddr = Some (build_deployment_info origin from amount setup)
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
(set_contract_state caddr ((@serialize State _) cstate)
(add_contract caddr contract
(transfer_balance from caddr amount bstate)))).
Proof.
intros * reach queue amount_nonnegative enough_balance%Z.ge_le
caddr_is_contract not_deployed init_some.
pose (bstate' := (bstate<|chain_state_queue := acts|>
<|chain_state_env :=
(set_contract_state caddr ((@serialize State _) cstate)
(add_contract caddr contract
(transfer_balance from caddr amount bstate)))|>)).
assert (step : ChainStep bstate bstate').
- eapply step_action with (new_acts := []); eauto.
eapply eval_deploy; eauto.
+ now apply wc_init_to_init in init_some.
+ constructor; reflexivity.
- exists bstate'.
destruct reach as [trace].
exists (ChainedList.snoc trace step).
split; eauto.
repeat split; eauto;
try (cbn; now destruct_address_eq).
cbn. destruct_chain_step; try congruence.
+ destruct_action_eval;
try congruence; cbn in *; subst; rewrite queue in queue_prev; inversion queue_prev; subst.
* destruct_address_eq.
-- now rewrite deserialize_serialize.
-- inversion env_eq.
cbn in contracts_eq.
specialize (contracts_eq caddr).
now rewrite address_eq_refl, address_eq_ne in contracts_eq.
* now destruct msg.
+ exfalso. eapply no_eval.
rewrite queue in queue_prev.
inversion queue_prev.
eapply eval_deploy; eauto.
* now apply wc_init_to_init in init_some.
* now constructor.
+ rewrite <- env_eq in not_deployed.
cbn in not_deployed.
now destruct_address_eq.
Qed.
Close Scope Z_scope.
Global Hint Resolve reachable_through_refl
reachable_through_trans'
reachable_through_trans
reachable_through_step
reachable_through_reachable : core.
Global Hint Resolve reachable_through_refl
reachable_through_trans'
reachable_through_trans
reachable_through_step
reachable_through_reachable : core.
Local Ltac update_fix term1 term2 H H_orig H' :=
match H with
| context G [ term1 ] =>
let x := context G [ term2 ] in
update_fix term1 term2 x H_orig H'
| _ =>
let h := fresh "H" in
assert H; [H' | clear H_orig; rename h into H_orig]
end.
(* Replaces all occurrences of <term1> with <term2> in hypothesis <H>
using tactic <H'> to prove the old hypothesis implies the updated *)
Local Ltac update_ term1 term2 H H' :=
match type of H with
| context G [ term1 ] =>
let x := context G [ term2 ] in
update_fix term1 term2 x H H'
end.
Tactic Notation "update" constr(t1) "with" constr(t2) "in" hyp(H) := update_ t1 t2 H ltac:(try (cbn; easy)).
Tactic Notation "update" constr(t1) "with" constr(t2) "in" hyp(H) "by" tactic(G) := update_ t1 t2 H G.
Tactic Notation "update" constr(t2) "in" hyp(H) := let t1 := type of H in update_ t1 t2 H ltac:(try (cbn; easy)).
Tactic Notation "update" constr(t2) "in" hyp(H) "by" tactic(G) := let t1 := type of H in update_ t1 t2 H G.
Local Ltac only_on_match tac :=
match goal with
| |- exists bstate', reachable_through ?bstate bstate' /\ _ => tac
| |- _ => idtac
end.
Local Ltac update_chainstate bstate1 bstate2 :=
match goal with
| H : reachable bstate1 |- _ => clear H
| H : chain_state_queue bstate1 = _ |- _ => clear H
| H : IsValidNextBlock _ bstate1.(chain_state_env).(env_chain) |- _ => clear H
| H : reachable_through bstate1 bstate2 |- _ =>
update (reachable bstate2) in H
| H : env_contracts bstate1.(chain_state_env) _ = Some _ |- _ =>
update bstate1 with bstate2 in H by (now rewrite_environment_equiv in *)
| H : env_contract_states bstate1.(chain_state_env) _ = Some _ |- _ =>
update bstate1 with bstate2 in H by (now rewrite_environment_equiv in *)
| H : context [ bstate1 ] |- _ =>
match type of H with
| EnvironmentEquiv _ _ => fail 1
| _ => update bstate1 with bstate2 in H by (try (rewrite_environment_equiv in *; cbn; easy))
end
end;
only_on_match ltac:(progress update_chainstate bstate1 bstate2).
(* Tactic for updating goal and all occurrences of an old ChainState
after adding a future ChainState to the environment. *)
Ltac update_all :=
match goal with
| Hreach : reachable_through ?bstate1 ?bstate2,
Henv_eq : EnvironmentEquiv ?bstate2.(chain_state_env) (add_new_block_to_env ?header ?bstate1.(chain_state_env)) |-
exists bstate3, reachable_through ?bstate1 bstate3 /\ _ =>
apply (step_reachable_through_exists bstate1 bstate2); auto;
update_chainstate bstate1 bstate2;
only_on_match ltac:(
clear Henv_eq;
(try clear dependent header);
clear dependent bstate1)
| Hreach : reachable_through ?bstate1 ?bstate2,
Henv_eq : EnvironmentEquiv ?bstate2.(chain_state_env) _ |-
exists bstate3, reachable_through ?bstate1 bstate3 /\ _ =>
apply (step_reachable_through_exists bstate1 bstate2); auto;
update_chainstate bstate1 bstate2;
only_on_match ltac:(
clear Henv_eq;
clear dependent bstate1)
| Hreach : reachable_through ?bstate1 ?bstate2 |-
exists bstate3, reachable_through ?bstate1 bstate3 /\ _ =>
apply (step_reachable_through_exists bstate1 bstate2); auto;
update (reachable bstate2) in Hreach;
only_on_match ltac:(clear dependent bstate1)
end.
Ltac forward_time slot_ :=
let new_bstate := fresh "bstate" in
let new_header := fresh "header" in
let new_header_valid := fresh "header_valid" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
let new_slot_hit := fresh "slot_hit" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = [],
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (forward_time bstate) with (slot := slot_)
as [new_bstate [new_header [new_reach [new_header_valid [new_slot_hit [new_queue new_env_eq]]]]]]
end.
Ltac forward_time_exact slot_ :=
let new_bstate := fresh "bstate" in
let new_header := fresh "header" in
let new_header_valid := fresh "header_valid" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
let new_slot_hit := fresh "slot_hit" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = [],
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (forward_time_exact bstate) with (slot := slot_)
as [new_bstate [new_header [new_reach [new_header_valid [new_slot_hit [new_queue new_env_eq]]]]]]
end.
Ltac add_block acts_ slot_ :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = [],
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct add_block with (acts := acts_) (slot_incr := slot_)
as [new_bstate [new_reach [new_queue new_env_eq]]];
[apply Hreach | apply Hqueue| | | | | |]
end.
Ltac evaluate_action contract_ :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_deployed_state := fresh "deployed_state" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (evaluate_action contract_) as
[new_bstate [new_reach [new_deployed_state [new_queue new_env_eq]]]];
[apply Hreach | rewrite Hqueue | | | | | | ]
end.
Ltac evaluate_transfer :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct evaluate_transfer as
[new_bstate [new_reach [new_queue new_env_eq]]];
[apply Hreach | rewrite Hqueue | | | | ]
end.
Ltac discard_invalid_action :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct discard_invalid_action as
[new_bstate [new_reach [new_queue new_env_eq]]];
[apply Hreach | rewrite Hqueue | | | ]
end.
Ltac empty_queue H :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let temp_H := fresh "H" in
let temp_eval := fresh "eval" in
match goal with
| Hempty : emptyable (chain_state_queue ?bstate),
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
pattern (bstate) in H;
match type of H with
| ?f bstate =>
edestruct (empty_queue bstate f) as
[new_bstate [new_reach [temp_H new_queue]]];
[apply Hreach | apply Hempty | apply H |
clear H;
intros ?bstate_from ?bstate_to ?act ?acts ?reach_from ?reach_to
H ?queue_from ?queue_to [[temp_eval] | ?env_eq];
only 1: destruct_action_eval |
clear H; rename temp_H into H]
end
end.
Ltac deploy_contract contract_ :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_deployed_state := fresh "deployed_state" in
let new_contract_deployed := fresh "contract_deployed" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
let new_cstate := fresh "cstate" in
let contract_not_deployed := fresh "trace" in
let deploy_info := fresh "deploy_info" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate,
Haddress : address_is_contract ?caddr = true,
Hdeployed : env_contracts ?bstate.(chain_state_env) ?caddr = None |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (deploy_contract contract_) as
(new_bstate & trace & new_reach & new_contract_deployed &
new_deployed_state & deploy_info & new_queue & new_env_eq);
[apply Hreach | rewrite Hqueue | | |
apply Haddress | apply Hdeployed | |
clear Haddress Hdeployed;
match type of new_deployed_state with
| env_contract_states _ _ = Some ((@serialize _ _) ?state) => remember state as new_cstate
end
]
end.
End BuildUtils.
From Stdlib Require Import List.
From Stdlib Require Import Psatz.
From Stdlib Require Import Permutation.
From Stdlib Require Import Morphisms.
From Stdlib Require Import String.
From Stdlib Require Import Logic.Decidable.
From ConCert.Execution Require Import ChainedList.
From ConCert.Execution Require Import Monad.
From ConCert.Execution Require Import ResultMonad.
From ConCert.Execution Require Import Serializable.
From ConCert.Execution Require Import BlockchainBase.
From ConCert.Execution Require Import BlockchainTheories.
From ConCert.Utils Require Import Automation.
From ConCert.Utils Require Import Extras.
From ConCert.Utils Require Import RecordUpdate.
Import ListNotations.
Section Builder.
Context {Base : ChainBase}.
Inductive ActionEvaluationError :=
| amount_negative (amount : Amount) (* amount is negative *)
| amount_too_high (amount : Amount) (* sender does not have enough money *)
| no_such_contract (addr : Address) (* there is no contract at that address *)
| too_many_contracts (* cannot generate fresh address for new contract *)
| init_failed (err : SerializedValue) (* contract init function failed *)
| receive_failed (err : SerializedValue) (* contract receive function failed *)
| deserialization_failed (val : SerializedValue) (* failed deserializing value *)
| internal_error. (* unexpected internal error *)
Inductive AddBlockError :=
| invalid_header (header : BlockHeader) (* header for next block is invalid *)
| invalid_root_action (act : Action) (* a specified root action is invalid *)
| origin_from_mismatch (act : Action) (* origin and from addresses do not match for an action in a new block *)
| action_evaluation_depth_exceeded (* out of fuel while evaluating actions recursively *)
| action_evaluation_error (* error when evaluating single action *)
(act : Action)
(err : ActionEvaluationError).
Class ChainBuilderType :=
build_builder {
builder_type : Type;
builder_initial : builder_type;
builder_env : builder_type -> Environment;
builder_add_block
(builder : builder_type)
(header : BlockHeader)
(actions : list Action) :
result builder_type AddBlockError;
builder_trace (builder : builder_type) :
ChainTrace empty_state (build_chain_state (builder_env builder) []);
}.
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
Global Coercion builder_env : builder_type >-> Environment.
End Builder.
Module BuildUtils.
Definition receiver_can_receive_transfer `{ChainBase} (bstate : ChainState) act_body :=
match act_body with
| act_transfer to _ => address_is_contract to = false \/
(exists wc state,
env_contracts bstate to = Some wc /\
env_contract_states bstate to = Some state /\
forall (bstate_new : ChainState) ctx, exists new_state, wc_receive wc bstate_new ctx state None = Ok (new_state, []))
| _ => True
end.
(* This axiom states that for any reachable state and any contract it is
decidable whether or not there is an address where the contract can be deployed to.
This is not provable in general with the assumption ChainBase makes about
addresses and the function address_is_contract. However, this should be
provable in any sensible instance of ChainBase *)
Axiom deployable_address_decidable : forall `{ChainBase} bstate wc setup act_origin act_from amount,
reachable bstate ->
decidable (exists addr state, address_is_contract addr = true
/\ env_contracts bstate addr = None
/\ wc_init wc
(transfer_balance act_from addr amount bstate)
(build_ctx act_origin act_from addr amount amount)
setup = Ok state).
Ltac action_not_decidable :=
right; intro;
match goal with
| H : exists bstate new_acts, inhabited (ActionEvaluation _ _ bstate new_acts) |- False =>
destruct H as [bstate_new [new_acts [action_evaluation]]];
destruct_action_eval; try congruence
end; repeat
match goal with
| H : {| act_origin := _; act_from := _; act_body := _ |} = {| act_origin := _; act_from := _; act_body := match ?msg with | Some _ => _ | None =>_ end |} |- False =>
destruct msg
| H : {| act_origin := _; act_from := _; act_body := _ |} = {| act_origin := _; act_from := _; act_body := _ |} |- False =>
inversion H; subst; clear H
end.
Ltac action_decidable :=
left; do 2 eexists; constructor;
match goal with
| H : wc_receive _ _ _ _ ?m = Ok _ |- _ => eapply (eval_call _ _ _ _ _ m)
| H : wc_init _ _ _ _ = Ok _ |- _ => eapply eval_deploy
| H : context [act_transfer _ _] |- _ => eapply eval_transfer
end;
eauto; try now constructor.
Ltac rewrite_balance :=
match goal with
| H := context [if (_ =? ?to)%address then _ else _],
H2 : Environment |- _ =>
assert (new_to_balance_eq : env_account_balances H2 to = H);
[ try rewrite_environment_equiv in *; cbn; unfold H; destruct_address_eq; try congruence; lia |
now rewrite <- new_to_balance_eq in *]
end.
(* For any reachable state and an action it is decidable if it is
possible to evaluate the action in the state *)
Open Scope Z_scope.
Lemma action_evaluation_decidable `{ChainBase} : forall bstate act,
reachable bstate ->
decidable (exists bstate' new_acts, inhabited (ActionEvaluation bstate act bstate' new_acts)).
Proof.
intros * reach.
destruct act eqn:Hact.
destruct act_body;
(destruct (amount >=? 0) eqn:amount_positive;
[destruct (amount <=? env_account_balances bstate act_from) eqn:balance |
action_not_decidable; now rewrite Z.geb_leb, Z.leb_gt in amount_positive (* Eliminate cases where amount is negative *)];
[| action_not_decidable; now rewrite Z.leb_gt in balance ]); (* Eliminate cases where sender does not have enough balance *)
try (destruct (address_is_contract to) eqn:to_is_contract;
[destruct (env_contracts bstate to) eqn:to_contract;
[destruct (env_contract_states bstate to) eqn:contract_state |] |]);
try now action_not_decidable. (* Eliminate cases with obvious contradictions *)
all : rewrite Z.geb_leb, <- Zge_is_le_bool in amount_positive.
all : rewrite Z.leb_le in balance.
- (* act_body = act_transfer to amount *)
pose (new_to_balance := if (address_eqb act_from to)
then (env_account_balances bstate to)
else (env_account_balances bstate to) + amount).
destruct (wc_receive w
(transfer_balance act_from to amount bstate)
(build_ctx act_origin act_from to new_to_balance amount)
s None) eqn:receive.
+ (* Case: act_transfer is evaluable by eval_call *)
destruct t.
pose (bstate' := (set_contract_state to s0
(transfer_balance act_from to amount bstate))).
action_decidable.
rewrite_balance.
+ (* Case: act_transfer is not evaluable by eval_call
because wc_receive returned None *)
action_not_decidable.
rewrite_balance.
- (* act_body = act_transfer to amount *)
(* Case: act_transfer is evaluable by eval_transfer *)
pose (bstate' := (transfer_balance act_from to amount bstate)).
action_decidable.
- (* act_body = act_call to amount msg *)
pose (new_to_balance := if (address_eqb act_from to)
then (env_account_balances bstate to)
else (env_account_balances bstate to) + amount).
destruct (wc_receive w
(transfer_balance act_from to amount bstate)
(build_ctx act_origin act_from to new_to_balance amount)
s (Some msg)) eqn:receive.
+ (* Case: act_call is evaluable by eval_call *)
destruct t.
pose (bstate' := (set_contract_state to s0
(transfer_balance act_from to amount bstate))).
action_decidable.
rewrite_balance.
+ (* Case: act_call is not evaluable by eval_call
because wc_receive returned None *)
action_not_decidable.
rewrite_balance.
- (* act_body = act_call to amount msg *)
(* Case: contradiction *)
action_not_decidable.
now apply contract_addr_format in deployed; auto.
- (* act_body = act_deploy amount c setup *)
apply deployable_address_decidable
with (wc := c) (setup := setup) (act_origin := act_origin)
(act_from := act_from) (amount := amount)
in reach.
destruct reach as [[to [state [to_is_contract_addr [to_not_deployed init]]]] | no_deployable_addr].
+ (* Case: act_deploy is evaluable by eval_deploy *)
pose (bstate' := (set_contract_state to state
(add_contract to c
(transfer_balance act_from to amount bstate)))).
action_decidable.
+ (* Case: act_deploy is not evaluable by eval_deploy
because no there is no available contract address
that this contract can be deployed to *)
action_not_decidable.
apply no_deployable_addr.
eauto.
Qed.
Close Scope Z_scope.
(* Property stating that an action does not produce any new action when evaluated *)
Definition produces_no_new_acts `{ChainBase} act : Prop :=
forall bstate bstate' new_acts, ActionEvaluation bstate act bstate' new_acts -> new_acts = [].
(* Property on a ChainState queue stating all actions are from accounts and produces
no new actions when evaluated. This ensures that the queue can be emptied successfully *)
Definition emptyable `{ChainBase} queue : Prop :=
Forall act_is_from_account queue /\
Forall produces_no_new_acts queue.
(* An empty queue is always emptyable *)
Lemma empty_queue_is_emptyable `{ChainBase} : emptyable [].
Proof.
now constructor.
Qed.
(* A subset of an emptyable queue is also emptyable *)
Lemma emptyable_cons `{ChainBase} : forall x l,
emptyable (x :: l) -> emptyable l.
Proof.
intros * [acts_from_account no_new_acts].
apply Forall_inv_tail in acts_from_account.
now apply Forall_inv_tail in no_new_acts.
Qed.
(* For any reachable state it is possible to empty the chain_state_queue
if the queue only contains action that satisfy the following
1) the action is from a user and not a contract
2) the action does not produce any actions when evaluated
For any property that holds on the starting state this also hold on
the state with an empty queue if it can be proven that the property
holds after evaluating any action.
*)
Lemma empty_queue `{ChainBase} : forall bstate (P : ChainState -> Prop),
reachable bstate ->
emptyable (chain_state_queue bstate) ->
P bstate ->
(forall (bstate bstate' : ChainState) act acts, reachable bstate -> reachable bstate' -> P bstate ->
chain_state_queue bstate = act :: acts -> chain_state_queue bstate' = acts ->
(inhabited (ActionEvaluation bstate act bstate' []) \/ EnvironmentEquiv bstate bstate') -> P bstate') ->
exists bstate', reachable_through bstate bstate' /\ P bstate' /\ (chain_state_queue bstate') = [].
Proof.
intros * reach [acts_from_account no_new_acts].
remember (chain_state_queue bstate) as queue.
generalize dependent bstate.
induction queue; intros bstate reach Hqueue_eq HP HP_preserved.
- (* Case: queue is already empty, thus we are already done *)
now eexists.
- (* Case: queue contains at least one action,
thus we need to either discard or evaluate it *)
apply list_relations.list.Forall_cons_1 in acts_from_account as [act_from_a acts_from_account].
apply list_relations.list.Forall_cons_1 in no_new_acts as [no_new_acts_from_a no_new_acts].
edestruct action_evaluation_decidable as
[[mid_env [new_acts [action_evaluation]]] | no_action_evaluation]; eauto.
+ (* Case: the action is evaluable *)
pose (build_chain_state mid_env (new_acts ++ queue)) as mid.
assert (step : ChainStep bstate mid) by (now eapply step_action).
apply no_new_acts_from_a in action_evaluation as new_acts_eq; subst.
eapply HP_preserved with (bstate' := mid) in HP; eauto.
apply IHqueue in HP as [to [reachable_through [P_to queue_to]]]; subst; eauto.
now exists to.
+ (* Case: the action not is evaluable *)
pose (bstate<| chain_state_queue := queue |>) as mid.
assert (step : ChainStep bstate mid).
{ eapply step_action_invalid; try easy.
intros. apply no_action_evaluation.
now do 2 eexists.
}
apply reachable_step in step as reachable_mid; eauto.
apply IHqueue in reachable_mid as [to [reachable_through [P_to queue_to]]]; eauto.
exists to.
destruct_and_split; auto.
eauto.
eapply (HP_preserved bstate mid); eauto.
now right.
Qed.
Open Scope Z_scope.
(* Lemma showing that there exists a future ChainState with an added block *)
Lemma add_block `{ChainBase} : forall bstate reward creator acts slot_incr,
reachable bstate ->
chain_state_queue bstate = [] ->
address_is_contract creator = false ->
reward >= 0->
(slot_incr > 0)%nat ->
Forall act_is_from_account acts ->
Forall act_origin_is_eq_from acts ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
(add_new_block_to_env {| block_height := S (chain_height bstate);
block_slot := current_slot bstate + slot_incr;
block_finalized_height := finalized_height bstate;
block_creator := creator;
block_reward := reward; |} bstate)).
Proof.
intros * reach queue creator_not_contract
reward_positive slot_incr_positive
acts_from_accounts origins_from_accounts.
pose (header :=
{| block_height := S (chain_height bstate);
block_slot := current_slot bstate + slot_incr;
block_finalized_height := finalized_height bstate;
block_creator := creator;
block_reward := reward; |}).
pose (bstate_with_acts := (bstate<|chain_state_queue := acts|>
<|chain_state_env := add_new_block_to_env header bstate|>)).
assert (step_with_acts : ChainStep bstate bstate_with_acts).
{ eapply step_block; try easy.
- constructor; try easy.
+ cbn. lia.
+ split; try (cbn; lia). cbn.
now apply finalized_heigh_chain_height.
}
exists bstate_with_acts.
split; eauto.
split; eauto.
constructor; try reflexivity.
Qed.
(* Lemma showing that there exists a future ChainState with the
same contract states where the current slot is <slot> *)
Lemma forward_time_exact `{ChainBase} : forall bstate reward creator slot,
reachable bstate ->
chain_state_queue bstate = [] ->
address_is_contract creator = false ->
reward >= 0 ->
(current_slot bstate < slot)%nat ->
(exists bstate' header,
reachable_through bstate bstate'
/\ IsValidNextBlock header bstate
/\ (slot = current_slot bstate')%nat
/\ chain_state_queue bstate' = []
/\ EnvironmentEquiv
bstate'
(add_new_block_to_env header bstate)).
Proof.
intros bstate reward creator slot reach queue
creator_not_contract reward_positive slot_not_hit.
eapply add_block with (slot_incr := (slot - current_slot bstate)%nat) in reach as new_block; try easy.
destruct new_block as [bstate_with_act [reach' [queue' env_eq]]].
do 2 eexists.
split; eauto.
do 3 try split; only 9: apply env_eq; eauto; cbn; try lia.
- now apply finalized_heigh_chain_height.
- rewrite_environment_equiv in *. cbn. lia.
Qed.
(* Lemma showing that there exists a future ChainState with the
same contract states where the current slot is at least <slot> *)
Lemma forward_time `{ChainBase} : forall bstate reward creator slot,
reachable bstate ->
chain_state_queue bstate = [] ->
address_is_contract creator = false ->
reward >= 0 ->
(exists bstate' header,
reachable_through bstate bstate'
/\ IsValidNextBlock header bstate
/\ (slot <= current_slot bstate')%nat
/\ chain_state_queue bstate' = []
/\ EnvironmentEquiv
bstate'
(add_new_block_to_env header bstate)).
Proof.
intros * reach queue creator_not_contract reward_positive.
destruct (slot - current_slot bstate)%nat eqn:slot_hit.
- eapply add_block with (slot_incr := 1%nat) in reach as new_block; try easy.
destruct new_block as [bstate_with_act [reach' [queue' env_eq]]].
do 2 eexists.
split; eauto.
do 3 try split; only 9: apply env_eq; eauto; cbn; try lia.
+ now apply finalized_heigh_chain_height.
+ apply Nat.sub_0_le in slot_hit.
rewrite_environment_equiv in *. cbn. lia.
- specialize (forward_time_exact bstate reward creator slot) as
(bstate' & header & reach' & header_valid & slot_hit' & queue' & env_eq); eauto.
lia.
do 2 eexists.
destruct_and_split; eauto.
lia.
Qed.
(* Lemma showing that there exists a future ChainState
where the contract call is evaluated *)
Lemma evaluate_action `{ChainBase} : forall {Setup Msg State Error : Type}
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State}
`{Serializable Error}
(contract : Contract Setup Msg State Error)
bstate origin from caddr amount msg acts new_acts
cstate new_cstate,
reachable bstate ->
chain_state_queue bstate = {| act_from := from;
act_origin := origin;
act_body := act_call caddr amount ((@serialize Msg _) msg) |} :: acts ->
amount >= 0 ->
env_account_balances bstate from >= amount ->
env_contracts bstate caddr = Some (contract : WeakContract) ->
env_contract_states bstate caddr = Some ((@serialize State _) cstate) ->
BlockchainBase.receive contract (transfer_balance from caddr amount bstate)
(build_ctx origin from caddr (if (address_eqb from caddr)
then (env_account_balances bstate caddr)
else (env_account_balances bstate caddr) + amount) amount)
cstate (Some msg) = Ok (new_cstate, new_acts) ->
(exists bstate',
reachable_through bstate bstate'
/\ env_contract_states bstate' caddr = Some ((@serialize State _) new_cstate)
/\ chain_state_queue bstate' = (map (build_act origin caddr) new_acts) ++ acts
/\ EnvironmentEquiv
bstate'
(set_contract_state caddr ((@serialize State _) new_cstate) (transfer_balance from caddr amount bstate))).
Proof.
intros * reach queue amount_nonnegative enough_balance%Z.ge_le
deployed deployed_state receive_some.
pose (new_to_balance := if (address_eqb from caddr)
then (env_account_balances bstate caddr)
else (env_account_balances bstate caddr) + amount).
pose (bstate' := (bstate<|chain_state_queue := (map (build_act origin caddr) new_acts) ++ acts|>
<|chain_state_env := set_contract_state caddr ((@serialize State _) new_cstate)
(transfer_balance from caddr amount bstate)|>)).
assert (new_to_balance_eq : env_account_balances bstate' caddr = new_to_balance) by
(cbn; destruct_address_eq; easy).
assert (step : ChainStep bstate bstate').
- eapply step_action; eauto.
eapply eval_call with (msg := Some ((@serialize Msg _) msg)); eauto.
+ rewrite new_to_balance_eq.
now apply wc_receive_to_receive in receive_some.
+ constructor; reflexivity.
- exists bstate'.
split; eauto.
repeat split; eauto.
cbn.
now destruct_address_eq.
Qed.
(* Lemma showing that there exists a future ChainState
where the transfer action is evaluated *)
Lemma evaluate_transfer `{ChainBase} : forall bstate origin from to amount acts,
reachable bstate ->
chain_state_queue bstate = {| act_from := from;
act_origin := origin;
act_body := act_transfer to amount |} :: acts ->
amount >= 0 ->
env_account_balances bstate from >= amount ->
address_is_contract to = false ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
(transfer_balance from to amount bstate)).
Proof.
intros * reach queue amount_nonnegative enough_balance%Z.ge_le to_not_contract.
pose (bstate' := (bstate<|chain_state_queue := acts|>
<|chain_state_env := (transfer_balance from to amount bstate)|>)).
assert (step : ChainStep bstate bstate').
- eapply step_action with (new_acts := []); eauto.
eapply eval_transfer; eauto.
constructor; reflexivity.
- eexists bstate'.
split; eauto.
repeat split; eauto.
Qed.
(* Lemma showing that if an action in the queue is invalid then
there exists a future ChainState with the same environment
where that action is discarded *)
Lemma discard_invalid_action `{ChainBase} : forall bstate act acts,
reachable bstate ->
chain_state_queue bstate = act :: acts ->
act_is_from_account act ->
(forall (bstate0 : Environment) (new_acts : list Action), ActionEvaluation bstate act bstate0 new_acts -> False) ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
bstate).
Proof.
intros * reach queue act_from_account no_action_evaluation.
pose (bstate' := (bstate<|chain_state_queue := acts|>)).
assert (step : ChainStep bstate bstate').
- eapply step_action_invalid; eauto.
constructor; reflexivity.
- eexists bstate'.
split; eauto.
repeat split; eauto.
Qed.
(* Lemma showing that for any permutation of the queue there
exists a future ChainState with the same environment
end the queue permuted *)
Lemma permute_queue `{ChainBase} : forall bstate acts acts_permuted,
reachable bstate ->
chain_state_queue bstate = acts ->
Permutation.Permutation acts acts_permuted ->
(exists bstate',
reachable_through bstate bstate'
/\ chain_state_queue bstate' = acts_permuted
/\ EnvironmentEquiv
bstate'
bstate).
Proof.
intros * reach queue perm.
pose (bstate' := (bstate<|chain_state_queue := acts_permuted|>)).
assert (step : ChainStep bstate bstate').
- eapply step_permute.
+ econstructor; eauto.
+ now rewrite queue.
- eexists bstate'.
split; eauto.
repeat split; eauto.
Qed.
(* Lemma showing that there exists a future ChainState
where the contract is deployed *)
Lemma deploy_contract `{ChainBase} : forall {Setup Msg State Error : Type}
`{Serializable Setup}
`{Serializable Msg}
`{Serializable State}
`{Serializable Error}
(contract : Contract Setup Msg State Error)
bstate origin from caddr amount acts setup cstate,
reachable bstate ->
chain_state_queue bstate = {| act_from := from;
act_origin := origin;
act_body := act_deploy amount contract ((@serialize Setup _) setup) |} :: acts ->
amount >= 0 ->
env_account_balances bstate from >= amount ->
address_is_contract caddr = true ->
env_contracts bstate caddr = None ->
BlockchainBase.init contract
(transfer_balance from caddr amount bstate)
(build_ctx origin from caddr amount amount)
setup = Ok cstate ->
(exists bstate' (trace : ChainTrace empty_state bstate'),
reachable_through bstate bstate'
/\ env_contracts bstate' caddr = Some (contract : WeakContract)
/\ env_contract_states bstate' caddr = Some ((@serialize State _) cstate)
/\ deployment_info Setup trace caddr = Some (build_deployment_info origin from amount setup)
/\ chain_state_queue bstate' = acts
/\ EnvironmentEquiv
bstate'
(set_contract_state caddr ((@serialize State _) cstate)
(add_contract caddr contract
(transfer_balance from caddr amount bstate)))).
Proof.
intros * reach queue amount_nonnegative enough_balance%Z.ge_le
caddr_is_contract not_deployed init_some.
pose (bstate' := (bstate<|chain_state_queue := acts|>
<|chain_state_env :=
(set_contract_state caddr ((@serialize State _) cstate)
(add_contract caddr contract
(transfer_balance from caddr amount bstate)))|>)).
assert (step : ChainStep bstate bstate').
- eapply step_action with (new_acts := []); eauto.
eapply eval_deploy; eauto.
+ now apply wc_init_to_init in init_some.
+ constructor; reflexivity.
- exists bstate'.
destruct reach as [trace].
exists (ChainedList.snoc trace step).
split; eauto.
repeat split; eauto;
try (cbn; now destruct_address_eq).
cbn. destruct_chain_step; try congruence.
+ destruct_action_eval;
try congruence; cbn in *; subst; rewrite queue in queue_prev; inversion queue_prev; subst.
* destruct_address_eq.
-- now rewrite deserialize_serialize.
-- inversion env_eq.
cbn in contracts_eq.
specialize (contracts_eq caddr).
now rewrite address_eq_refl, address_eq_ne in contracts_eq.
* now destruct msg.
+ exfalso. eapply no_eval.
rewrite queue in queue_prev.
inversion queue_prev.
eapply eval_deploy; eauto.
* now apply wc_init_to_init in init_some.
* now constructor.
+ rewrite <- env_eq in not_deployed.
cbn in not_deployed.
now destruct_address_eq.
Qed.
Close Scope Z_scope.
Global Hint Resolve reachable_through_refl
reachable_through_trans'
reachable_through_trans
reachable_through_step
reachable_through_reachable : core.
Global Hint Resolve reachable_through_refl
reachable_through_trans'
reachable_through_trans
reachable_through_step
reachable_through_reachable : core.
Local Ltac update_fix term1 term2 H H_orig H' :=
match H with
| context G [ term1 ] =>
let x := context G [ term2 ] in
update_fix term1 term2 x H_orig H'
| _ =>
let h := fresh "H" in
assert H; [H' | clear H_orig; rename h into H_orig]
end.
(* Replaces all occurrences of <term1> with <term2> in hypothesis <H>
using tactic <H'> to prove the old hypothesis implies the updated *)
Local Ltac update_ term1 term2 H H' :=
match type of H with
| context G [ term1 ] =>
let x := context G [ term2 ] in
update_fix term1 term2 x H H'
end.
Tactic Notation "update" constr(t1) "with" constr(t2) "in" hyp(H) := update_ t1 t2 H ltac:(try (cbn; easy)).
Tactic Notation "update" constr(t1) "with" constr(t2) "in" hyp(H) "by" tactic(G) := update_ t1 t2 H G.
Tactic Notation "update" constr(t2) "in" hyp(H) := let t1 := type of H in update_ t1 t2 H ltac:(try (cbn; easy)).
Tactic Notation "update" constr(t2) "in" hyp(H) "by" tactic(G) := let t1 := type of H in update_ t1 t2 H G.
Local Ltac only_on_match tac :=
match goal with
| |- exists bstate', reachable_through ?bstate bstate' /\ _ => tac
| |- _ => idtac
end.
Local Ltac update_chainstate bstate1 bstate2 :=
match goal with
| H : reachable bstate1 |- _ => clear H
| H : chain_state_queue bstate1 = _ |- _ => clear H
| H : IsValidNextBlock _ bstate1.(chain_state_env).(env_chain) |- _ => clear H
| H : reachable_through bstate1 bstate2 |- _ =>
update (reachable bstate2) in H
| H : env_contracts bstate1.(chain_state_env) _ = Some _ |- _ =>
update bstate1 with bstate2 in H by (now rewrite_environment_equiv in *)
| H : env_contract_states bstate1.(chain_state_env) _ = Some _ |- _ =>
update bstate1 with bstate2 in H by (now rewrite_environment_equiv in *)
| H : context [ bstate1 ] |- _ =>
match type of H with
| EnvironmentEquiv _ _ => fail 1
| _ => update bstate1 with bstate2 in H by (try (rewrite_environment_equiv in *; cbn; easy))
end
end;
only_on_match ltac:(progress update_chainstate bstate1 bstate2).
(* Tactic for updating goal and all occurrences of an old ChainState
after adding a future ChainState to the environment. *)
Ltac update_all :=
match goal with
| Hreach : reachable_through ?bstate1 ?bstate2,
Henv_eq : EnvironmentEquiv ?bstate2.(chain_state_env) (add_new_block_to_env ?header ?bstate1.(chain_state_env)) |-
exists bstate3, reachable_through ?bstate1 bstate3 /\ _ =>
apply (step_reachable_through_exists bstate1 bstate2); auto;
update_chainstate bstate1 bstate2;
only_on_match ltac:(
clear Henv_eq;
(try clear dependent header);
clear dependent bstate1)
| Hreach : reachable_through ?bstate1 ?bstate2,
Henv_eq : EnvironmentEquiv ?bstate2.(chain_state_env) _ |-
exists bstate3, reachable_through ?bstate1 bstate3 /\ _ =>
apply (step_reachable_through_exists bstate1 bstate2); auto;
update_chainstate bstate1 bstate2;
only_on_match ltac:(
clear Henv_eq;
clear dependent bstate1)
| Hreach : reachable_through ?bstate1 ?bstate2 |-
exists bstate3, reachable_through ?bstate1 bstate3 /\ _ =>
apply (step_reachable_through_exists bstate1 bstate2); auto;
update (reachable bstate2) in Hreach;
only_on_match ltac:(clear dependent bstate1)
end.
Ltac forward_time slot_ :=
let new_bstate := fresh "bstate" in
let new_header := fresh "header" in
let new_header_valid := fresh "header_valid" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
let new_slot_hit := fresh "slot_hit" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = [],
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (forward_time bstate) with (slot := slot_)
as [new_bstate [new_header [new_reach [new_header_valid [new_slot_hit [new_queue new_env_eq]]]]]]
end.
Ltac forward_time_exact slot_ :=
let new_bstate := fresh "bstate" in
let new_header := fresh "header" in
let new_header_valid := fresh "header_valid" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
let new_slot_hit := fresh "slot_hit" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = [],
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (forward_time_exact bstate) with (slot := slot_)
as [new_bstate [new_header [new_reach [new_header_valid [new_slot_hit [new_queue new_env_eq]]]]]]
end.
Ltac add_block acts_ slot_ :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = [],
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct add_block with (acts := acts_) (slot_incr := slot_)
as [new_bstate [new_reach [new_queue new_env_eq]]];
[apply Hreach | apply Hqueue| | | | | |]
end.
Ltac evaluate_action contract_ :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_deployed_state := fresh "deployed_state" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (evaluate_action contract_) as
[new_bstate [new_reach [new_deployed_state [new_queue new_env_eq]]]];
[apply Hreach | rewrite Hqueue | | | | | | ]
end.
Ltac evaluate_transfer :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct evaluate_transfer as
[new_bstate [new_reach [new_queue new_env_eq]]];
[apply Hreach | rewrite Hqueue | | | | ]
end.
Ltac discard_invalid_action :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct discard_invalid_action as
[new_bstate [new_reach [new_queue new_env_eq]]];
[apply Hreach | rewrite Hqueue | | | ]
end.
Ltac empty_queue H :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_queue := fresh "queue" in
let temp_H := fresh "H" in
let temp_eval := fresh "eval" in
match goal with
| Hempty : emptyable (chain_state_queue ?bstate),
Hreach : reachable ?bstate |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
pattern (bstate) in H;
match type of H with
| ?f bstate =>
edestruct (empty_queue bstate f) as
[new_bstate [new_reach [temp_H new_queue]]];
[apply Hreach | apply Hempty | apply H |
clear H;
intros ?bstate_from ?bstate_to ?act ?acts ?reach_from ?reach_to
H ?queue_from ?queue_to [[temp_eval] | ?env_eq];
only 1: destruct_action_eval |
clear H; rename temp_H into H]
end
end.
Ltac deploy_contract contract_ :=
let new_bstate := fresh "bstate" in
let new_reach := fresh "reach" in
let new_deployed_state := fresh "deployed_state" in
let new_contract_deployed := fresh "contract_deployed" in
let new_queue := fresh "queue" in
let new_env_eq := fresh "env_eq" in
let new_cstate := fresh "cstate" in
let contract_not_deployed := fresh "trace" in
let deploy_info := fresh "deploy_info" in
match goal with
| Hqueue : (chain_state_queue ?bstate) = _,
Hreach : reachable ?bstate,
Haddress : address_is_contract ?caddr = true,
Hdeployed : env_contracts ?bstate.(chain_state_env) ?caddr = None |-
exists bstate', reachable_through ?bstate bstate' /\ _ =>
edestruct (deploy_contract contract_) as
(new_bstate & trace & new_reach & new_contract_deployed &
new_deployed_state & deploy_info & new_queue & new_env_eq);
[apply Hreach | rewrite Hqueue | | |
apply Haddress | apply Hdeployed | |
clear Haddress Hdeployed;
match type of new_deployed_state with
| env_contract_states _ _ = Some ((@serialize _ _) ?state) => remember state as new_cstate
end
]
end.
End BuildUtils.