Commit 973dfc92 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Rename step_empty -> step_transfer and merge step_call ctors

This split between cases only makes things harder.
parent 391ccde6
......@@ -508,7 +508,7 @@ to be recorded. *)
Inductive ChainStep :
Environment -> Action ->
Environment -> list Action -> Type :=
| step_empty :
| step_transfer :
forall {pre : Environment}
{act : Action}
{new_env : Environment}
......@@ -546,7 +546,7 @@ Inductive ChainStep :
new_env
(set_contract_state to state (add_contract to wc (add_tx tx pre))) ->
ChainStep pre act new_env []
| step_call_empty :
| step_call :
forall {pre : Environment}
{act : Action}
{new_env : Environment}
......@@ -554,48 +554,27 @@ Inductive ChainStep :
(from to : Address)
(amount : Amount)
(wc : WeakContract)
(msg : option OakValue)
(prev_state : OakValue)
(new_state : OakValue)
(resp_acts : list ActionBody),
amount <= account_balance pre from ->
env_contracts pre to = Some wc ->
contract_state pre to = Some prev_state ->
act = build_act from (act_transfer to amount) ->
let tx := build_tx from to amount tx_empty in
act = build_act from (match msg with
| None => act_transfer to amount
| Some msg => act_call to amount msg
end) ->
let tx := build_tx from to amount (match msg with
| None => tx_empty
| Some msg => tx_call msg
end) in
wc_receive
wc
(add_tx tx pre)
(build_ctx from to amount)
prev_state
None = Some (new_state, resp_acts) ->
new_acts = map (build_act to) resp_acts ->
EnvironmentEquiv
new_env
(set_contract_state to new_state (add_tx tx pre)) ->
ChainStep pre act new_env new_acts
| step_call_msg :
forall {pre : Environment}
{act : Action}
{new_env : Environment}
{new_acts : list Action}
(from to : Address)
(amount : Amount)
(wc : WeakContract)
(msg : OakValue)
(prev_state : OakValue)
(new_state : OakValue)
(resp_acts : list ActionBody),
amount <= account_balance pre from ->
env_contracts pre to = Some wc ->
contract_state pre to = Some prev_state ->
act = build_act from (act_call to amount msg) ->
let tx := build_tx from to amount (tx_call msg) in
wc_receive
wc
(add_tx tx pre)
(build_ctx from to amount)
prev_state
(Some msg) = Some (new_state, resp_acts) ->
msg = Some (new_state, resp_acts) ->
new_acts = map (build_act to) resp_acts ->
EnvironmentEquiv
new_env
......@@ -609,26 +588,23 @@ Context {pre : Environment} {act : Action}
Definition step_from : Address :=
match step with
| step_empty from _ _ _ _ _ _ _
| step_transfer from _ _ _ _ _ _ _
| step_deploy from _ _ _ _ _ _ _ _ _ _ _ _ _
| step_call_empty from _ _ _ _ _ _ _ _ _ _ _ _ _ _
| step_call_msg from _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
| step_call from _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ => from
end.
Definition step_to : Address :=
match step with
| step_empty _ to _ _ _ _ _ _
| step_transfer _ to _ _ _ _ _ _
| step_deploy _ to _ _ _ _ _ _ _ _ _ _ _ _
| step_call_empty _ to _ _ _ _ _ _ _ _ _ _ _ _ _
| step_call_msg _ to _ _ _ _ _ _ _ _ _ _ _ _ _ _ => to
| step_call _ to _ _ _ _ _ _ _ _ _ _ _ _ _ _ => to
end.
Definition step_amount : Amount :=
match step with
| step_empty _ _ amount _ _ _ _ _
| step_transfer _ _ amount _ _ _ _ _
| step_deploy _ _ amount _ _ _ _ _ _ _ _ _ _ _
| step_call_empty _ _ amount _ _ _ _ _ _ _ _ _ _ _ _
| step_call_msg _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ _ => amount
| step_call _ _ amount _ _ _ _ _ _ _ _ _ _ _ _ _ => amount
end.
End Accessors.
......
......@@ -235,36 +235,45 @@ Section ExecuteActions.
Proof.
intros sent act_eq.
unfold send_or_call in sent.
destruct (Z.gtb_spec amount (account_balance lc_before from)); [simpl in *; congruence|].
(* Make goals a little more manageable by factoring intermediate envs *)
repeat
match goal with
| [H: context[add_tx ?tx ?env] |- _] =>
match type of H with
| _ = add_tx tx env => fail 1
| _ =>
let name := fresh "with_tx" in
remember (add_tx tx env) as name
end
end.
destruct (Z.gtb_spec amount (account_balance lc_before from));
[cbn in *; congruence|].
destruct (FMap.find to (lc_contracts lc_before)) as [wc|] eqn:to_contract.
- (* there is a contract at destination, so do call *)
destruct (contract_state _ _) as [prev_state|] eqn:prev_state_eq;
cbn in *; try congruence.
destruct (wc_receive _ _ _ _ _) eqn:receive; cbn in *; try congruence.
[|cbn in *; congruence].
cbn -[lc_to_env] in *.
destruct (wc_receive wc _ _ _ _) eqn:receive;
[|cbn in *; congruence].
match goal with
| [p: OakValue * list ActionBody |- _] => destruct p as [new_state resp_acts]
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].
3: apply (step_call_empty from to amount wc prev_state new_state resp_acts);
try solve [simpl in *; congruence].
1, 3:
rewrite <- receive; unfold constructor;
apply wc_receive_proper; auto;
symmetry; now apply add_tx_equiv.
1, 2:
inversion sent; subst;
now apply set_contract_state_equiv, add_tx_equiv.
apply (step_call from to amount wc msg prev_state new_state resp_acts);
try solve [cbn in *; congruence].
+ rewrite <- receive.
apply wc_receive_proper; auto.
subst with_tx.
symmetry.
now apply add_tx_equiv.
+ inversion sent; subst;
now apply set_contract_state_equiv, add_tx_equiv.
- (* no contract at destination, so msg should be empty *)
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.
constructor.
apply (step_empty from to amount); auto.
apply (step_transfer from to amount); auto.
inversion sent; subst; now apply add_tx_equiv.
Qed.
......
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