Commit f8adfa8c authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Various refactorings and cleanups

* Remove BlockTrace and bake everything into ChainTrace
* Simplify ChainTrace. Its signature is now
ChainTrace : Environment -> list Action -> Prop.

These changes will make it easier to reason over traces when proving
properties about contracts. For one, we can now talk about prefixes of
the entire chain without the weird distinction between block traces and
chain traces.
parent f8824cf5
Pipeline #12099 passed with stage
in 6 minutes and 18 seconds
......@@ -593,38 +593,7 @@ Proof.
Qed.
End Step.
(* A block trace is essentially just the reflexive transitive closure of the steps.
It captures execution within a single block. *)
Inductive BlockTrace :
Environment -> list Action ->
Environment -> list Action -> Prop :=
| btrace_refl : forall {acts} {env : Environment},
BlockTrace env acts env acts
| btrace_step : forall {pre post} act tx mid new_acts suf final,
ChainStep pre act tx mid new_acts ->
BlockTrace mid (new_acts ++ suf) post final ->
BlockTrace pre (act :: suf) post final
| btrace_permute : forall pre post acts acts' final_acts,
Permutation acts acts' ->
BlockTrace pre acts post final_acts ->
BlockTrace pre acts' post final_acts.
Section BlockTraceTheories.
Context {pre : Environment} {acts : list Action}
{post : Environment} {post_acts : list Action}
(trace : BlockTrace pre acts post post_acts).
Lemma block_header_post_steps : block_header post = block_header pre.
Proof.
induction trace; auto.
match goal with
| [H: ChainStep _ _ _ _ _ |- _] => rewrite <- (block_header_post_step H)
end.
auto.
Qed.
End BlockTraceTheories.
Definition add_new_block
Definition add_new_block_header
(header : BlockHeader)
(baker : Address)
(env : Environment) : Environment :=
......@@ -640,6 +609,8 @@ let chain :=
else blocks_baked chain a; |} in
env <|env_chain := chain|>.
(* Todo: this should just be a computation. But I still do not *)
(* know exactly what the best way of working with reflect is *)
Definition IsValidNextBlock (new old : BlockHeader) : Prop :=
block_height new = S (block_height old) /\
slot_number new > slot_number old /\
......@@ -658,42 +629,44 @@ Definition initial_env :=
contract_state a := None; |};
env_contracts a := None; |}.
Inductive ChainTrace : Environment -> Environment -> Prop :=
| ctrace_initial :
forall (env : Environment),
EnvironmentEquiv env initial_env ->
ChainTrace env env
(* The chain captures that an environment can be reached with some current actions. *)
Inductive ChainTrace : Environment -> list Action -> Prop :=
| ctrace_initial :
forall (env : Environment),
EnvironmentEquiv env initial_env ->
ChainTrace env []
(* Add a new block to the trace *)
| ctrace_block :
forall (prev_start prev_end : Environment)
forall (prev : Environment)
(header : BlockHeader)
(baker : Address)
(acts : list Action)
(block_start new_end : Environment),
ChainTrace prev_start prev_end ->
IsValidNextBlock header (block_header prev_end) ->
(new : Environment),
ChainTrace prev [] ->
IsValidNextBlock header (block_header prev) ->
Forall (fun act => address_is_contract (act_from act) = false) acts ->
BlockTrace block_start acts new_end [] ->
EnvironmentEquiv
block_start
(add_new_block header baker prev_end) ->
ChainTrace prev_start new_end.
Section ChainTraceTheories.
Context {pre post : Environment} (trace : ChainTrace pre post).
Lemma block_height_post_trace :
block_height (block_header pre) <= block_height (block_header post).
Proof.
induction trace; auto.
match goal with
| [H: BlockTrace _ _ _ _, H': EnvironmentEquiv _ _ |- _]
=> rewrite (block_header_post_steps H), H'
end.
unfold IsValidNextBlock in *.
simpl.
intuition.
Qed.
End ChainTraceTheories.
new
(add_new_block_header header baker prev) ->
ChainTrace new acts
(* Execute an action *)
| ctrace_step :
forall (prev : Environment)
(act : Action)
(acts : list Action)
(tx : Tx)
(new : Environment)
(new_acts : list Action),
ChainTrace prev (act :: acts) ->
ChainStep prev act tx new new_acts ->
ChainTrace new (new_acts ++ acts)
(* Reorder action order *)
| ctrace_permute :
forall (env : Environment)
(acts acts' : list Action),
ChainTrace env acts ->
Permutation acts acts' ->
ChainTrace env acts'.
End Semantics.
Class ChainBuilderType :=
......@@ -713,7 +686,7 @@ Class ChainBuilderType :=
option builder_type;
builder_trace (b : builder_type) :
ChainTrace (builder_env builder_initial) (builder_env b);
ChainTrace (builder_env b) [];
}.
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
......
......@@ -81,22 +81,6 @@ Qed.
Hint Resolve step_circulation_unchanged : core.
(* Finally, we get the result over block traces by a simple induction. *)
Lemma block_trace_circulation_unchanged
{bef : list Action}
{after : list Action}
{post pre : Environment}
(trace : BlockTrace pre bef post after)
: circulation post = circulation pre.
Proof.
induction trace;
match goal with
| [IH: _ |- _] => try rewrite IH; eauto
end.
Qed.
Hint Resolve block_trace_circulation_unchanged : core.
Instance circulation_proper :
Proper (ChainEquiv ==> eq) circulation.
Proof.
......@@ -106,7 +90,7 @@ Proof.
Qed.
Lemma circulation_add_new_block header baker env :
circulation (add_new_block header baker env) =
circulation (add_new_block_header header baker env) =
(circulation env + compute_block_reward (block_height header))%Z.
Proof.
assert (Hperm: exists suf, Permutation ([baker] ++ suf) (elements Address)).
......@@ -137,28 +121,26 @@ Proof.
lia.
Qed.
Theorem chain_trace_circulation
{env_start env_end : Environment}
(trace : ChainTrace env_start env_end)
: circulation env_end =
sumZ compute_block_reward (seq 1 (block_height (block_header env_end))).
Theorem chain_trace_circulation {env : Environment} (trace : ChainTrace env [])
: circulation env =
sumZ compute_block_reward (seq 1 (block_height (block_header env))).
Proof.
induction trace as
[env eq|
prev_start prev_end
header baker acts
block_start new_end
prev_trace IH valid
from_accounts block_trace eq].
- rewrite eq.
prev header baker acts new prev_trace IH valid from_accounts eq|
prev act acts tx new new_acts prev_trace IH|
env acts acts' prev_trace IH perm].
- (* Initial chain *)
rewrite eq.
unfold circulation.
induction (elements Address); auto.
- unfold IsValidNextBlock in *.
rewrite (block_header_post_steps block_trace).
rewrite eq.
simpl.
rewrite (proj1 valid), sumZ_seq_S, <- IH.
rewrite (block_trace_circulation_unchanged block_trace), eq, circulation_add_new_block.
now rewrite (proj1 valid).
- (* New block header. Generates new coins, so idea is to just split the sumZ. *)
rewrite eq, circulation_add_new_block.
cbn.
now rewrite (proj1 valid), sumZ_seq_S, IH.
- (* execute step *)
erewrite step_circulation_unchanged, block_header_post_step; eassumption.
- (* permute *)
auto.
Qed.
End Circulation.
......@@ -324,26 +324,21 @@ Section ExecuteActions.
destruct body as [to amount|to amount msg|amount wc setup]; eauto.
Qed.
Lemma execute_steps_trace gas acts lc df lc_after :
execute_steps gas acts lc df = Some lc_after ->
BlockTrace lc acts lc_after [].
Lemma execute_steps_trace gas acts (lc lc_final : LocalChain) df :
ChainTrace lc acts ->
execute_steps gas acts lc df = Some lc_final ->
ChainTrace lc_final [].
Proof.
revert acts lc lc_after.
induction gas as [|gas IH]; intros acts lc lc_after exec.
- unfold execute_steps in exec.
destruct acts as [|x xs]; [|congruence].
Hint Constructors BlockTrace : core.
replace lc_after with lc by congruence; auto.
- destruct acts as [|x xs]; simpl in *.
+ replace lc_after with lc by congruence; auto.
+ destruct (execute_action x lc) as [[acts lc_after_act]|] eqn:exec_once;
simpl in *; [|congruence].
specialize (IH _ _ _ exec); clear exec.
destruct (execute_action_step _ _ _ _ exec_once) as [tx step]; clear exec_once.
(* For breadth first case our IH is xs ++ acts ->* [] and we need to show *)
(* x :: xs ->* [], so we will need to permute it first. *)
assert (Permutation (xs ++ acts) (acts ++ xs)) by perm_simplify.
destruct df; eauto.
revert acts lc lc_final.
induction gas as [| gas IH]; intros acts lc lc_final trace exec; cbn in *.
- destruct acts; congruence.
- 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].
Hint Constructors ChainTrace : core.
assert (Permutation (new_acts ++ xs) (xs ++ new_acts)) by perm_simplify.
destruct df; eauto.
Qed.
End ExecuteActions.
......@@ -361,7 +356,7 @@ Definition lc_initial : LocalChain :=
Record LocalChainBuilder :=
build_local_chain_builder {
lcb_lc : LocalChain;
lcb_trace : ChainTrace lc_initial lcb_lc;
lcb_trace : ChainTrace lcb_lc [];
}.
Definition lcb_initial : LocalChainBuilder.
......@@ -469,8 +464,8 @@ Proof.
| [H: context[execute_steps _ _ ?a] |- _] => remember a as lc_block_start
end.
Hint Resolve validate_header_valid validate_actions_valid execute_steps_trace : core.
apply (ctrace_block lc_initial prev_lc_end new_header baker actions lc_block_start lc);
eauto; clear validate.
enough (ChainTrace lc_block_start actions) by eauto.
eapply ctrace_block with (baker0 := baker); eauto.
subst lc_block_start.
simpl.
......@@ -497,5 +492,4 @@ Definition lcb_chain_builder_type_breadth_first : ChainBuilderType :=
builder_env lcb := lcb_lc lcb;
builder_add_block := add_block false;
builder_trace := lcb_trace; |}.
End LocalBlockchain.
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