Commit 4e862e5a authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Prove an auxiliary lemma and clean up circulation proof

parent b09772ad
Pipeline #12147 passed with stage
in 5 minutes and 16 seconds
......@@ -42,7 +42,8 @@ Infix "=?" := address_eqb (at level 70) : address_scope.
Global Ltac destruct_address_eq :=
repeat
match goal with
| [|- context[(?a =? ?b)%address]] => destruct (address_eqb_spec a b)
| [H: context[address_eqb ?a ?b] |- _] => destruct (address_eqb_spec a b)
| [|- context[address_eqb ?a ?b]] => destruct (address_eqb_spec a b)
end.
Section Blockchain.
......@@ -819,6 +820,33 @@ Proof.
| [IH: _ |- _] => now rewrite IH
end.
Qed.
Ltac rewrite_environment_equiv :=
match goal with
| [H: EnvironmentEquiv _ _ |- _] => rewrite H in *
end.
Ltac destruct_step :=
match goal with
| [H: ChainStep _ _ _ _ _ |- _] => destruct H
end.
Lemma contract_addr_format
{to to_queue}
(trace : ChainTrace empty_env [] to to_queue)
(addr : Address) (wc : WeakContract) :
env_contracts to addr = Some wc ->
address_is_contract addr = true.
Proof.
intros contract_at_addr.
remember empty_env eqn:eq.
induction trace; rewrite eq in *; clear eq;
try rewrite_environment_equiv; cbn in *; auto.
- congruence.
- destruct_step; rewrite_environment_equiv; cbn in *; auto.
destruct_address_eq; subst; auto.
Qed.
End Theories.
End Trace.
End Semantics.
......
......@@ -42,7 +42,7 @@ Proof.
unfold circulation.
induction (elements Address) as [| x xs IH].
- reflexivity.
- simpl in *.
- cbn in *.
rewrite IH, (account_balance_post step), from_eq_to.
lia.
Qed.
......@@ -100,21 +100,20 @@ Proof.
pose proof (Permutation_NoDup perm (elements_set Address)) as perm_set.
unfold circulation.
rewrite perm.
simpl.
cbn.
unfold constructor, set, account_balance.
simpl.
cbn.
destruct (address_eqb_spec baker baker); try congruence.
simpl.
pose proof (in_NoDup_app baker [baker] suf ltac:(prove) perm_set) as not_in_suf.
repeat rewrite <- Z.add_assoc.
f_equal.
rewrite <- Z.add_comm.
repeat rewrite <- Z.add_assoc.
f_equal.
cbn.
match goal with
| [|- ((?a - ?b + (?c + ?d)) + ?e = (?a - ?b + ?d + ?f + ?c))%Z] =>
enough (e = f) by lia
end.
pose proof (in_NoDup_app baker [baker] suf ltac:(prove) perm_set) as not_in_suf.
clear perm perm_set e.
induction suf as [| x xs IH]; auto.
simpl in *.
cbn in *.
apply Decidable.not_or in not_in_suf.
destruct (address_eqb_spec x baker); try tauto.
specialize (IH (proj2 not_in_suf)).
......
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