Commit 778c39f1 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Add definition for when an action comes from an account

parent 973dfc92
......@@ -689,6 +689,9 @@ Definition IsValidNextBlock (new old : BlockHeader) : Prop :=
finalized_height new >= finalized_height old /\
finalized_height new < block_height new.
Definition ActIsFromAccount (act : Action) : Prop :=
address_is_contract (act_from act) = false.
Record ChainState :=
build_chain_state {
chain_state_env :> Environment;
......@@ -703,9 +706,7 @@ Inductive ChainEvent : ChainState -> ChainState -> Type :=
{next : ChainState},
chain_state_queue prev = [] ->
IsValidNextBlock header (block_header prev) ->
Forall
(fun act => address_is_contract (act_from act) = false)
(chain_state_queue next) ->
Forall ActIsFromAccount (chain_state_queue next) ->
EnvironmentEquiv
next
(add_new_block_header header baker prev) ->
......
......@@ -416,14 +416,14 @@ Definition validate_actions (actions : list Action) : option unit :=
Lemma validate_actions_valid actions :
validate_actions actions = Some tt ->
Forall (fun act => address_is_contract (act_from act) = false) actions.
Forall ActIsFromAccount actions.
Proof.
intros valid.
induction actions as [|x xs IH]; auto.
unfold validate_actions in valid.
cbn -[address_is_contract] in valid.
destruct (address_is_contract _) eqn:eq1; try (simpl in *; congruence).
destruct (existsb _) eqn:eq2; try (simpl in *; congruence).
destruct (address_is_contract _) eqn:eq1; try (cbn in *; congruence).
destruct (existsb _) eqn:eq2; try (cbn in *; congruence).
clear valid.
unfold validate_actions in IH.
rewrite eq2 in IH.
......
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