Commit 5221931a authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Move ChainStep and ChainTrace to Type

This moves ChainStep and ChainTrace to type. The reason being that our
proofs will depend on prefixes of traces and it will be very useful (if
not required) to be able to match on the trace and the steps.
ChainBuilderType is changed appropriately: now, an implementation just
needs to prove that ChainTrace empty_env [] cur_env [] is inhabited.
Thus, ChainTrace can basically be seen as one particular way to order
the execution so that we reach a state. When it is inhabited, it thus
means that there exists a proper way to order actions so that we reach
the state we are in.
parent 62aff812
Pipeline #12155 failed with stage
in 1 minute and 26 seconds
......@@ -505,25 +505,23 @@ changes an environment and which external actions to execute after it. *)
(* todo: handle deploy/call failures. We should still transfer gas and allow this
to be recorded. *)
Inductive ChainStep :
Environment -> Action -> Tx ->
Environment -> list Action -> Prop :=
Environment -> Action ->
Environment -> list Action -> Type :=
| step_empty :
forall {pre : Environment}
{act : Action}
{tx : Tx}
{new_env : Environment}
(from to : Address)
(amount : Amount),
amount <= account_balance pre from ->
address_is_contract to = false ->
act = build_act from (act_transfer to amount) ->
tx = build_tx from to amount tx_empty ->
let tx := build_tx from to amount tx_empty in
EnvironmentEquiv new_env (add_tx tx pre) ->
ChainStep pre act tx new_env []
ChainStep pre act new_env []
| step_deploy :
forall {pre : Environment}
{act : Action}
{tx : Tx}
{new_env : Environment}
(from to : Address)
(amount : Amount)
......@@ -535,7 +533,9 @@ Inductive ChainStep :
incoming_txs pre to = [] ->
address_is_contract to = true ->
act = build_act from (act_deploy amount wc setup) ->
tx = build_tx from to amount (tx_deploy (build_contract_deployment (wc_version wc) setup)) ->
let tx := build_tx
from to amount
(tx_deploy (build_contract_deployment (wc_version wc) setup)) in
wc_init
wc
(add_tx tx pre)
......@@ -544,11 +544,10 @@ Inductive ChainStep :
EnvironmentEquiv
new_env
(set_contract_state to state (add_contract to wc (add_tx tx pre))) ->
ChainStep pre act tx new_env []
ChainStep pre act new_env []
| step_call_empty :
forall {pre : Environment}
{act : Action}
{tx : Tx}
{new_env : Environment}
{new_acts : list Action}
(from to : Address)
......@@ -561,7 +560,7 @@ Inductive ChainStep :
env_contracts pre to = Some wc ->
contract_state pre to = Some prev_state ->
act = build_act from (act_transfer to amount) ->
tx = build_tx from to amount tx_empty ->
let tx := build_tx from to amount tx_empty in
wc_receive
wc
(add_tx tx pre)
......@@ -572,11 +571,10 @@ Inductive ChainStep :
EnvironmentEquiv
new_env
(set_contract_state to new_state (add_tx tx pre)) ->
ChainStep pre act tx new_env new_acts
ChainStep pre act new_env new_acts
| step_call_msg :
forall {pre : Environment}
{act : Action}
{tx : Tx}
{new_env : Environment}
{new_acts : list Action}
(from to : Address)
......@@ -590,7 +588,7 @@ Inductive ChainStep :
env_contracts pre to = Some wc ->
contract_state pre to = Some prev_state ->
act = build_act from (act_call to amount msg) ->
tx = build_tx from to amount (tx_call msg) ->
let tx := build_tx from to amount (tx_call msg) in
wc_receive
wc
(add_tx tx pre)
......@@ -601,49 +599,78 @@ Inductive ChainStep :
EnvironmentEquiv
new_env
(set_contract_state to new_state (add_tx tx pre)) ->
ChainStep pre act tx new_env new_acts.
ChainStep pre act new_env new_acts.
Section Accessors.
Context {pre : Environment} {act : Action}
{post : Environment} {new_acts : list Action}
(step : ChainStep pre act post new_acts).
Definition step_from : Address :=
match step with
| step_empty from _ _ _ _ _ _ _
| step_deploy from _ _ _ _ _ _ _ _ _ _ _ _ _
| step_call_empty from _ _ _ _ _ _ _ _ _ _ _ _ _ _
| step_call_msg from _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
end.
Definition step_to : Address :=
match step with
| step_empty _ to _ _ _ _ _ _
| step_deploy _ to _ _ _ _ _ _ _ _ _ _ _ _
| step_call_empty _ to _ _ _ _ _ _ _ _ _ _ _ _ _
| step_call_msg _ to _ _ _ _ _ _ _ _ _ _ _ _ _ _ => to
end.
Definition step_amount : Amount :=
match step with
| step_empty _ _ amount _ _ _ _ _
| step_deploy _ _ amount _ _ _ _ _ _ _ _ _ _ _
| step_call_empty _ _ amount _ _ _ _ _ _ _ _ _ _ _ _
| step_call_msg _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ _ => amount
end.
End Accessors.
Section Theories.
Section Single.
Context {pre : Environment} {act : Action} {tx : Tx}
Context {pre : Environment} {act : Action}
{post : Environment} {new_acts : list Action}
(step : ChainStep pre act tx post new_acts).
(step : ChainStep pre act post new_acts).
Lemma account_balance_post (addr : Address) :
(account_balance post addr =
account_balance post addr =
account_balance pre addr
+ (if (addr =? tx_to tx)%address then tx_amount tx else 0)
- (if (addr =? tx_from tx)%address then tx_amount tx else 0)).
+ (if (addr =? step_to step)%address then step_amount step else 0)
- (if (addr =? step_from step)%address then step_amount step else 0).
Proof.
unfold account_balance.
destruct step;
destruct step; subst; cbn;
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H
end;
simpl; unfold add_tx_to_map; destruct_address_eq; simpl; lia.
cbn; unfold add_tx_to_map; destruct_address_eq; cbn; lia.
Qed.
Lemma account_balance_post_to :
tx_from tx <> tx_to tx ->
account_balance post (tx_to tx) =
account_balance pre (tx_to tx) + tx_amount tx.
step_from step <> step_to step ->
account_balance post (step_to step) =
account_balance pre (step_to step) + step_amount step.
Proof.
rewrite account_balance_post.
destruct_address_eq; prove.
Qed.
Lemma account_balance_post_from :
tx_from tx <> tx_to tx ->
account_balance post (tx_from tx) =
account_balance pre (tx_from tx) - tx_amount tx.
step_from step <> step_to step ->
account_balance post (step_from step) =
account_balance pre (step_from step) - step_amount step.
Proof.
rewrite account_balance_post.
destruct_address_eq; prove.
Qed.
Lemma account_balance_post_irrelevant (addr : Address) :
addr <> tx_from tx ->
addr <> tx_to tx ->
addr <> step_from step ->
addr <> step_to step ->
account_balance post addr = account_balance pre addr.
Proof.
rewrite account_balance_post.
......@@ -657,7 +684,6 @@ Proof.
| [H: EnvironmentEquiv _ _ |- _] => now rewrite H
end.
Qed.
End Single.
End Theories.
End Step.
......@@ -701,10 +727,9 @@ Definition empty_env : Environment :=
(* The ChainTrace captures that there is a valid execution where,
starting from one environment and queue of actions, we end up in a
different environment and queue of actions. *)
Unset Elimination Schemes.
Inductive ChainTrace :
Environment -> list Action ->
Environment -> list Action -> Prop :=
Environment -> list Action -> Type :=
| ctrace_refl :
forall {env l}, ChainTrace env l env l
(* Add a new block to the trace *)
......@@ -730,11 +755,10 @@ Inductive ChainTrace :
{prev_to : Environment}
{act : Action}
{acts : list Action}
{tx : Tx}
{new : Environment}
{new_acts : list Action},
ChainTrace from from_queue prev_to (act :: acts) ->
ChainStep prev_to act tx new new_acts ->
ChainStep prev_to act new new_acts ->
ChainTrace from from_queue new (new_acts ++ acts)
(* Reorder action order *)
| ctrace_permute :
......@@ -746,17 +770,6 @@ Inductive ChainTrace :
Permutation to_queue to_queue' ->
ChainTrace from from_queue to to_queue'.
(* The normal induction principle generated for propositions does not
allow the picked proposition to depend on the inhabitant of the
proposition. However, for our traces, we will often want to prove
properties that rely on the specific inhabitant. For instance when we
need to reason about prefixes or suffixes. Thus we derive a normal
principle instead. As an example, rhis is necessary for the proofs
about trace_app below. This difference between inductives in Prop and
Type, and the solution was highlighted to me by Danil Annenkov. *)
Scheme ChainTrace_ind := Induction for ChainTrace Sort Prop.
Set Elimination Schemes.
Fixpoint trace_app
{from mid to : Environment}
{from_queue mid_queue to_queue : list Action}
......@@ -822,7 +835,7 @@ Ltac rewrite_environment_equiv :=
Ltac destruct_step :=
match goal with
| [H: ChainStep _ _ _ _ _ |- _] => destruct H
| [H: ChainStep _ _ _ _ |- _] => destruct H
end.
Lemma contract_addr_format
......@@ -862,7 +875,7 @@ Class ChainBuilderType :=
option builder_type;
builder_trace (b : builder_type) :
ChainTrace empty_env [] (builder_env b) [];
inhabited (ChainTrace empty_env [] (builder_env b) []);
}.
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
......
......@@ -31,11 +31,10 @@ Qed.
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 ->
(step : ChainStep pre act post new_acts) :
step_from step = step_to step ->
circulation post = circulation pre.
Proof.
intros from_eq_to.
......@@ -52,13 +51,12 @@ Hint Resolve step_from_to_same : core.
Lemma step_circulation_unchanged
{pre : Environment}
{act : Action}
{tx : Tx}
{post : Environment}
{new_acts : list Action}
(step : ChainStep pre act tx post new_acts) :
(step : ChainStep pre act post new_acts) :
circulation post = circulation pre.
Proof.
destruct (address_eqb_spec (tx_from tx) (tx_to tx))
destruct (address_eqb_spec (step_from step) (step_to step))
as [from_eq_to | from_neq_to]; eauto.
destruct (address_reorganize from_neq_to) as [suf perm].
apply Permutation_sym in perm.
......@@ -69,10 +67,10 @@ Proof.
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. }
assert (from_not_in_suf: ~In (step_from step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
assert (to_not_in_suf: ~In (step_to step) suf).
{ apply (in_NoDup_app _ [step_from step; step_to step] _); prove. }
clear perm perm_set.
pose proof (account_balance_post_irrelevant step).
......
......@@ -230,15 +230,13 @@ Section ExecuteActions.
| None => act_transfer to amount
| Some msg => act_call to amount msg
end) ->
exists tx, ChainStep lc_before act tx lc_after new_acts.
inhabited (ChainStep lc_before act lc_after new_acts).
Proof.
intros sent act_eq.
unfold send_or_call in sent.
destruct (Z.gtb_spec amount (account_balance lc_before from)); [simpl in *; congruence|].
destruct (FMap.find to (lc_contracts lc_before)) as [wc|] eqn:to_contract.
- (* there is a contract at destination, so do call *)
remember_tx.
exists tx.
destruct (contract_state _ _) as [prev_state|] eqn:prev_state_eq;
cbn in *; try congruence.
destruct (wc_receive _ _ _ _ _) eqn:receive; cbn in *; try congruence.
......@@ -247,6 +245,7 @@ Section ExecuteActions.
end.
(* We record the steps different depending on whether this *)
(* is a call with a message or without a message *)
constructor.
destruct msg as [msg|].
1: apply (step_call_msg from to amount wc msg prev_state new_state resp_acts);
try solve [simpl in *; congruence].
......@@ -263,8 +262,7 @@ Section ExecuteActions.
destruct (address_is_contract to) eqn:addr_format; simpl in *; try congruence.
destruct msg; simpl in *; try congruence.
assert (new_acts = []) by congruence; subst new_acts.
remember_tx.
exists tx.
constructor.
apply (step_empty from to amount); auto.
inversion sent; subst; now apply add_tx_equiv.
Qed.
......@@ -286,7 +284,7 @@ Section ExecuteActions.
Lemma deploy_contract_step from amount wc setup act lc_before new_acts lc_after :
deploy_contract from amount wc setup lc_before = Some (new_acts, lc_after) ->
act = build_act from (act_deploy amount wc setup) ->
exists tx, ChainStep lc_before act tx lc_after new_acts.
inhabited (ChainStep lc_before act lc_after new_acts).
Proof.
intros dep act_eq.
unfold deploy_contract in dep.
......@@ -294,14 +292,13 @@ Section ExecuteActions.
destruct (get_new_contract_addr lc_before) as [contract_addr|] eqn:new_contract_addr;
[|cbn in *; congruence].
cbn -[incoming_txs] in dep.
remember_tx.
destruct (incoming_txs _ _) eqn:no_txs; [|cbn in *; congruence].
destruct (FMap.find _ _) eqn:no_contracts; [cbn in *; congruence|].
destruct (wc_init _ _ _ _) as [state|] eqn:recv; [|cbn in *; congruence].
cbn in dep.
exists tx.
assert (new_acts = []) by congruence; subst new_acts.
Hint Resolve get_new_contract_addr_is_contract_addr : core.
constructor.
apply (step_deploy from contract_addr amount wc setup state); eauto.
- rewrite <- recv.
apply wc_init_proper; auto.
......@@ -316,7 +313,7 @@ Section ExecuteActions.
(lc_before : LocalChain)
(lc_after : LocalChain) :
execute_action act lc_before = Some (new_acts, lc_after) ->
exists tx, ChainStep lc_before act tx lc_after new_acts.
inhabited (ChainStep lc_before act lc_after new_acts).
Proof.
intros exec.
unfold execute_action in exec.
......@@ -326,9 +323,9 @@ Section ExecuteActions.
Qed.
Lemma execute_steps_trace gas acts (lc lc_final : LocalChain) df :
ChainTrace empty_env [] lc acts ->
inhabited (ChainTrace empty_env [] lc acts) ->
execute_steps gas acts lc df = Some lc_final ->
ChainTrace empty_env [] lc_final [].
inhabited (ChainTrace empty_env [] lc_final []).
Proof.
revert acts lc lc_final.
induction gas as [| gas IH]; intros acts lc lc_final trace exec; cbn in *.
......@@ -336,7 +333,8 @@ Section ExecuteActions.
- destruct acts as [|x xs]; try congruence.
destruct (execute_action x lc) as [[new_acts lc_after]|] eqn:exec_once;
cbn in *; try congruence.
destruct (execute_action_step _ _ _ _ exec_once) as [tx step].
destruct (execute_action_step _ _ _ _ exec_once) as [step].
destruct trace as [trace].
Hint Constructors ChainTrace : core.
assert (Permutation (new_acts ++ xs) (xs ++ new_acts)) by perm_simplify.
destruct df; eauto.
......@@ -357,7 +355,7 @@ Definition lc_initial : LocalChain :=
Record LocalChainBuilder :=
build_local_chain_builder {
lcb_lc : LocalChain;
lcb_trace : ChainTrace empty_env [] lcb_lc [];
lcb_trace : inhabited (ChainTrace empty_env [] lcb_lc []);
}.
Definition lcb_initial : LocalChainBuilder.
......@@ -486,7 +484,8 @@ Proof.
ctrace_block : core.
(* auto does not pick up reflexivity for reflexive relations. *)
Hint Extern 1 (EnvironmentEquiv _ _) => reflexivity : core.
eauto 6.
destruct prev_lcb_trace as [prev_lcb_trace].
eauto 7.
Defined.
Global Instance lcb_chain_builder_type : ChainBuilderType :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment