Commit 40a3ee2d authored by zhenlei's avatar zhenlei

[coq|spend]add proof

parent cc83c912
Pipeline #71292697 failed with stage
in 5 minutes and 7 seconds
......@@ -69,6 +69,35 @@ Module manager(C:ContractContext)(E:Env ST C).
let (destination, amount) := param in
new_storage = storage /\ returned_operations = (transfer_tokens env unit tt amount (implicit_account env destination) :: nil)%list.
Lemma eqb_eq a c1 c2 :
BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = true <->
c1 = c2.
Proof.
rewrite BinInt.Z.eqb_eq.
rewrite comparison_to_int_Eq.
apply comparable.compare_eq_iff.
Qed.
Lemma eqb_neq a c1 c2 :
BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = false <->
c1 <> c2.
Proof.
split.
- intros H He.
apply eqb_eq in He.
congruence.
- intro Hneq.
rewrite <- eqb_eq in Hneq.
generalize (BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0) Hneq.
intros []; congruence.
Qed.
Lemma and_right {P Q R : Prop} : P -> (Q <-> R) -> (Q <-> (P /\ R)).
Proof.
intuition.
Qed.
Lemma spend_correct
(storage : data storage_ty)
(param : data parameter_ty)
......@@ -85,10 +114,11 @@ Module manager(C:ContractContext)(E:Env ST C).
rewrite return_precond.
rewrite eval_precond_correct.
unfold spend_spec.
do 5 (more_fuel; simplify_instruction).
destruct param as [param|].
- do 4 (more_fuel; simplify_instruction).
case_eq (BinInt.Z.eqb (comparison_to_int (address_compare (sender env) (address_ env unit (implicit_account env storage)))) Z0).
do 9 (more_fuel; simplify_instruction).
(* proof: sender env = address_ env unit (implicit_account env storage) *)
case_eq (BinInt.Z.eqb (comparison_to_int (address_compare (sender env) (address_ env unit (implicit_account env storage)))) Z0).
(* proof if sender is manager *)
+ intro Htrue.
apply (eqb_eq address) in Htrue.
apply and_right.
......@@ -96,17 +126,18 @@ Module manager(C:ContractContext)(E:Env ST C).
* assumption.
* simpl.
do 3 (more_fuel; simplify_instruction).
destruct param as [(destination, amount)|[new_delegate|[()|new_spend]]];
repeat (more_fuel; simplify_instruction); intuition congruence.
destruct param as (destination, amount).
repeat (more_fuel; simplify_instruction). intuition congruence.
(* proof if sender no is manager *)
+ intro Hfalse.
apply (eqb_neq address) in Hfalse.
simpl.
repeat (more_fuel; simplify_instruction).
repeat (more_fuel; simplify_instruction).
split.
* intros Hf; inversion Hf.
* intros (H, _).
contradiction.
- intuition congruence.
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