Commit 92325c90 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Introduce reachable proposition

A state being reachable means there is an execution starting from the
empty state, that ends up in the state.
parent 3eaadae9
......@@ -769,6 +769,10 @@ starting from one environment and queue of actions, we end up in a
different environment and queue of actions. *)
Definition ChainTrace := ChainedList ChainState ChainEvent.
(* Additionally, a state is reachable if there is a trace ending in this trace. *)
Definition reachable (state : ChainState) : Prop :=
inhabited (ChainTrace empty_state state).
Section Theories.
Ltac destruct_chain_event :=
match goal with
......@@ -812,7 +816,7 @@ Local Open Scope address.
the ending state will not have any queued actions from
undeployed contracts. *)
Lemma undeployed_contract_no_out_queue contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
reachable state ->
address_is_contract contract = true ->
env_contracts state contract = None ->
Forall (fun act => (act_from act =? contract) = false) (chain_state_queue state).
......@@ -855,7 +859,7 @@ Qed.
(* With this lemma proven, we can show that the (perhaps seemingly stronger)
fact, that an undeployed contract has no outgoing txs, holds. *)
Lemma undeployed_contract_no_out_txs contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
reachable state ->
address_is_contract contract = true ->
env_contracts state contract = None ->
outgoing_txs state contract = [].
......@@ -869,10 +873,9 @@ Proof.
rewrite_environment_equiv; auto.
- (* In these steps we will use that the queue did not contain txs to the contract. *)
Hint Resolve contracts_post_pre_none : core.
Hint Unfold reachable : core.
pose proof
(undeployed_contract_no_out_queue
contract prev
ltac:(auto) ltac:(auto) ltac:(eauto)) as Hqueue.
repeat
......@@ -893,7 +896,7 @@ Proof.
Qed.
Lemma undeployed_contract_no_in_txs contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
reachable state ->
address_is_contract contract = true ->
env_contracts state contract = None ->
incoming_txs state contract = [].
......@@ -934,7 +937,7 @@ Class ChainBuilderType :=
option builder_type;
builder_trace (b : builder_type) :
inhabited (ChainTrace empty_state (build_chain_state (builder_env b) []));
reachable (build_chain_state (builder_env b) []);
}.
Global Coercion builder_type : ChainBuilderType >-> Sortclass.
......
......@@ -152,11 +152,12 @@ Proof.
Qed.
Theorem chain_trace_circulation
{state : ChainState}
(trace : ChainTrace empty_state state)
: circulation state =
sumZ compute_block_reward (seq 1 (block_height (block_header state))).
{state : ChainState} :
reachable state ->
circulation state =
sumZ compute_block_reward (seq 1 (block_height (block_header state))).
Proof.
intros [trace].
remember empty_state as from eqn:eq.
induction trace as [| from mid to xs IH x]; rewrite eq in *; clear eq.
- unfold circulation.
......
......@@ -668,13 +668,14 @@ Proof.
Qed.
Lemma undeployed_contract_no_out_queue_count contract (state : ChainState) :
inhabited (ChainTrace empty_state state) ->
reachable state ->
address_is_contract contract = true ->
env_contracts state contract = None ->
num_outgoing_acts (chain_state_queue state) contract = 0.
Proof.
intros [trace] is_contract undeployed.
pose proof undeployed_contract_no_out_queue as all; specialize_hypotheses.
Hint Unfold reachable : core.
induction all; auto.
cbn.
match goal with
......@@ -683,7 +684,7 @@ Proof.
Qed.
Lemma undeployed_contract_not_from_self contract (state : ChainState) act acts :
inhabited (ChainTrace empty_state state) ->
reachable state ->
address_is_contract contract = true ->
env_contracts state contract = None ->
chain_state_queue state = act :: acts ->
......@@ -776,7 +777,7 @@ Local Ltac simpl_hyp_invariant :=
end.
Theorem congress_txs_well_behaved to contract :
inhabited (ChainTrace empty_state to) ->
reachable to ->
env_contracts to contract = Some (Congress.contract : WeakContract) ->
num_cacts_in_state to contract +
length (outgoing_txs to contract) +
......
......@@ -371,7 +371,7 @@ Definition lc_initial : LocalChain :=
Record LocalChainBuilder :=
build_local_chain_builder {
lcb_lc : LocalChain;
lcb_trace : inhabited (ChainTrace empty_state (build_chain_state lcb_lc []));
lcb_trace : reachable (build_chain_state lcb_lc []);
}.
Definition lcb_initial : LocalChainBuilder.
......
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