https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 08edb74856d05a9ecdbc5dc5e40903aee308bd1b authored by Arvid Jakobsson on 28 September 2020, 21:46:43 UTC
[dexter] update proof for exchange entrypoints
[dexter] update proof for exchange entrypoints
Tip revision: 08edb74
dexter_verification.v
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import NArith.
Require Import ZArith.
Require Import semantics.
Require Import util.
Import error.
Require List.
Require Import Coq.Setoids.Setoid.
Require Import Coq.micromega.Lia.
Require dexter_definition.
Require dexter_spec.
Require dexter_addlqt_definition.
Module Dexter_verification (C : ContractContext).
Module Def := dexter_definition.
Module DefAddLqt := dexter_addlqt_definition.
Module Spec := dexter_spec.Dexter_spec C.
Import Spec.semantics.
Module Tactics.
Ltac destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool :=
destruct sto as
(accounts, ((self_is_updating_token_pool, (freeze_baker, lq_total)), ((manager, token_address), (token_pool, xtz_pool)))).
Ltac auto_fuel :=
repeat match goal with
| [ |- context G[eval_precond] ]
=> more_fuel; simpl
end.
(* TODO: Arvid: This tactic, and its usage could be omitted if the
appropriate mutez definitions and operations are rendered
Opaque *)
Ltac fold_mutez_goal :=
match goal with
| [ |- context[(exist (A := Vector.t _ _) ?P ?bv ?Hpbv)] ] =>
match bv with
(Vector.cons ?T ?f ?len ?l) =>
let z := eval cbn in (int64bv.to_Z bv) in
replace (exist P bv Hpbv)
with (exist P (int64bv.of_Z_safe z eq_refl) Hpbv)
by reflexivity
end
end.
End Tactics.
Import Tactics.
Lemma eqb_neq a c1 c2 :
BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = false <->
c1 <> c2.
Proof.
split.
- intros Hf He.
rewrite <- eqb_eq in He.
congruence.
- intro Hneq.
rewrite <- eqb_eq in Hneq.
destruct ((comparison_to_int (compare a c1 c2) =? 0)%Z); congruence.
Qed.
Lemma negb_is_true:
forall b : Datatypes.bool, negb b = true <-> ~ is_true b.
Proof.
intros. destruct b.
- intuition. elimtype False. apply H. reflexivity.
- simpl. split; intuition.
Qed.
Lemma is_false:
forall b : Datatypes.bool, b = false <-> (b -> False).
Proof.
intros.
rewrite bool_not_false.
apply not_iff_compat.
split; [apply Bool.Is_true_eq_left | apply Bool.Is_true_eq_true].
Qed.
Section entrypoints.
Variable (env : @proto_env dexter_definition.self_type).
Lemma comparison_to_int_ltb:
forall z1 z2 : Z, (comparison_to_int (z1 ?= z2) <? 0)%Z = (z1 <? z2)%Z.
Proof.
intros z1 z2.
destruct (Z.compare_spec z1 z2); simpl.
- rewrite H.
now repeat rewrite Z.ltb_irrefl.
- apply Z.ltb_lt in H.
rewrite H.
reflexivity.
- apply Z.lt_asymm in H.
apply Z.ltb_nlt in H.
rewrite H.
reflexivity.
Qed.
Lemma cmp_mutez_lt_zero:
forall t,
(comparison_to_int (tez.compare (0 ~Mutez) t) <? 0)%Z = true <->
(t <> (0 ~Mutez)).
Proof.
intros t.
unfold tez.compare.
unfold int64bv.int64_compare.
unfold int64bv.compare.
rewrite comparison_to_int_ltb.
rewrite Z.ltb_lt.
split.
- intro Heq.
apply Z.lt_neq in Heq.
congruence.
- intro Hneq.
destruct (Zle_lt_or_eq _ _ (tez.to_Z_lower_bound t)) as [Hlt | Heq].
+ apply Hlt.
+ change 0%Z with (tez.to_Z (0 ~Mutez)) in Heq.
apply tez.to_Z_inj in Heq.
congruence.
Qed.
Lemma N_le_neq2:
forall m : N, (0 < m)%N <-> m <> 0%N.
Proof.
(* solved direcrlty by lia in later versions of coq. *)
destruct m; lia.
Qed.
Lemma N_comparison_to_int_lt:
forall n1 n2,
(comparison_to_int (compare nat n1 n2) <? 0)%Z = true <-> (n1 < n2)%N.
Proof.
intros n1 n2. simpl. rewrite Z.ltb_lt. destruct (N.compare_spec n1 n2); simpl; lia.
Qed.
Lemma cmp_nat_lt_zero n :
(comparison_to_int (compare nat 0 n)%N <? 0)%Z = true <->
(n <> 0)%N.
Proof.
rewrite N_comparison_to_int_lt.
apply N_le_neq2.
Qed.
Lemma some_equal_inv :
forall A (x y : A),
Some x = Some y <->
y = x.
intuition (f_equal; congruence).
Qed.
Lemma mutez_to_nat :
forall t,
match tez.of_Z (Z.of_N (Z.to_N (tez.to_Z t mod tez.to_Z (1 ~Mutez)))) with
| Failed _ _ => None
| Return rem => Some (Z.to_N (tez.to_Z t / tez.to_Z (1 ~Mutez)), rem)
end = Some (Z.to_N (tez.to_Z t), (0 ~Mutez)).
Proof. intro t. now rewrite Z.mod_1_r, Z.div_1_r. Qed.
Lemma mutez_add_correct:
forall (x y z : data (Comparable_type mutez)),
tez.of_Z (tez.to_Z y + tez.to_Z x) = Return z <->
Spec.mutez_add x y z.
Proof. intros x y. now rewrite Z.add_comm. Qed.
Lemma tez_compare_mutez_to_nat :
forall t t',
(comparison_to_int (tez.compare t t') <=? 0)%Z = true <->
(Spec.mutez_to_nat t <= Spec.mutez_to_nat t')%N.
Proof.
intros t t'.
unfold tez.compare, int64bv.int64_compare, int64bv.compare.
rewrite comparison_to_int_leb.
rewrite Z.leb_le.
rewrite Z2N.inj_le; try apply tez.to_Z_lower_bound.
reflexivity.
Qed.
Lemma ex2_comm2 :
forall (T : Set) Q P R,
(((exists (y : T), Q y) /\ P) /\ R)
<-> (exists (y : T), Q y /\ P /\ R).
Proof.
intros T Q P R.
rewrite and_comm.
rewrite and_comm.
rewrite and_assoc.
rewrite and_comm.
rewrite ex_and_comm.
apply forall_ex. intuition.
Qed.
Lemma and_both_0_inv { P R S Q } :
Q <-> S -> P <-> R -> P /\ Q <-> R /\ S.
intuition.
Qed.
(* Shim for pair_equal_spec which is not in Coq 8.08 *)
Lemma shim_pair_equal_spec (A B : Type) (a1 a2 : A) (b1 b2 : B) :
(a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
Proof with auto.
split; intro H.
- split.
+ replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
rewrite H...
+ replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
rewrite H...
- destruct H; subst...
Qed.
Lemma comparison_to_int_pos :
forall n,
(comparison_to_int
match n with
| 0%N => Eq
| N.pos _ => Lt
end <? 0)%Z = true <-> (n > 0)%N.
Proof.
intro n. destruct n. simpl. cbv. intuition congruence.
simpl. intuition. lia.
Qed.
Lemma and_refl : forall P Q, P /\ P /\ Q <-> P /\ Q. intuition. Qed.
Lemma N_comparison_to_int_le:
forall x y,
(comparison_to_int (x ?= y)%N <=? 0)%Z = true <->
(x <= y)%N.
Proof.
intros x y.
destruct (N.compare_spec x y); unfold Z.leb; simpl.
- rewrite H. intuition.
- apply N.lt_le_incl in H. intuition.
- split; intro H1. discriminate. lia.
Qed.
Lemma N_comparison_to_int_opp:
forall (n1 n2 : N),
(comparison_to_int (n2 ?= n1)%N >=? 0)%Z =
(comparison_to_int (n1 ?= n2)%N <=? 0)%Z.
Proof.
intros n1 n2.
rewrite N.compare_antisym.
destruct (n1 ?= n2)%N; simpl; tauto.
Qed.
Lemma ediv_N_some :
forall x y,
y <> 0%N <->
ediv_N x y = Some ((x / y)%N, (x mod y)%N).
Proof.
unfold ediv_N.
intros x y.
rewrite <- N.eqb_eq. rewrite <- bool_not_false.
split; intro H.
- now rewrite H.
- destruct (_ =? _)%N; [discriminate| reflexivity].
Qed.
Lemma ediv_N_some_iff :
forall (x y : N) P Q,
y <> 0%N /\ P <-> y <> 0%N /\ Q ((x / y)%N, (x mod y)%N) ->
y <> 0%N /\ P <-> (exists z, ediv_N x y = Some z /\ Q z).
Proof.
intros x y P Q H.
split; intros Hn0.
- eexists. split. apply ediv_N_some. apply Hn0. apply H. apply Hn0.
- rewrite <- N.eqb_eq. rewrite <- bool_not_false.
destruct Hn0 as [z [Hdiv Hq]].
unfold ediv_N in Hdiv.
destruct (_ =? _)%N eqn:Hy0.
discriminate.
split. reflexivity.
apply H.
split.
+ rewrite <- N.eqb_eq. rewrite <- bool_not_false. assumption.
+ congruence.
Qed.
Lemma Z_mod_to_N_mod :
forall x y, (Z.of_N (x mod y) =? 0)%Z = true <-> (x mod y)%N = 0%N.
intros x y.
destruct (_ =? _)%Z eqn:Heq.
rewrite Z.eqb_eq in Heq.
rewrite <- N2Z.inj_iff.
now intuition.
intuition. inversion H.
rewrite <- Heq. rewrite H. reflexivity.
Qed.
Lemma Spec_Nceiling_mod :
forall (x y : N),
(Z.of_N (x mod y) =? 0)%Z = true ->
Spec.Nceiling x y = (x / y)%N.
Proof.
intros x y H.
apply Z_mod_to_N_mod in H.
unfold Spec.Nceiling.
rewrite surjective_pairing with (p := N.div_eucl _ _).
unfold N.modulo in H.
now rewrite H.
Qed.
Lemma Spec_Nceiling_rem :
forall (x y : N),
(Z.of_N (x mod y) =? 0)%Z = false ->
Spec.Nceiling x y = (x / y + 1)%N.
Proof.
intros x y H.
generalize (Z_mod_to_N_mod x y); intro Hconv.
apply not_iff_compat in Hconv.
unfold Spec.Nceiling.
rewrite surjective_pairing with (p := N.div_eucl _ _).
unfold N.modulo in H.
destruct (snd _) eqn:Heqn; intuition.
Qed.
Lemma ediv_N_some_iff' :
forall (x y : N) Q,
y <> 0%N /\ Q ((x / y)%N, (x mod y)%N) <->
(exists z, ediv_N x y = Some z /\ Q z).
Proof.
intros.
split.
- intros [H1 H2].
exists ((x / y)%N, (x mod y)%N).
split. apply ediv_N_some. assumption. assumption.
- unfold ediv_N.
intros [z [Hdiv Hq]].
rewrite <- N.eqb_eq. rewrite <- bool_not_false.
destruct (y =? 0)%N.
+ discriminate.
+ intuition congruence.
Qed.
Ltac N_add_comm y :=
match goal with
[ |- context[(?x + y)%N]] =>
replace (x + y)%N with (y + x)%N
by apply N.add_comm
end.
Lemma tez_to_Z_bij :
forall t1 t2 : tez.mutez, tez.to_Z t1 = tez.to_Z t2 <-> t1 = t2.
Proof.
split. apply tez.to_Z_inj. intro. now f_equal.
Qed.
Lemma cmp_mutez_eq_zero:
(comparison_to_int (tez.compare (amount env) (0 ~Mutez)) =? 0)%Z = true <->
amount env = (0 ~Mutez).
Proof.
change tez.compare with (compare mutez).
now rewrite util.eqb_eq.
Qed.
Lemma Bool_is_true_false_iff_not :
forall b,
b = false <-> ~ b.
Proof.
intro b.
rewrite bool_not_false.
apply not_iff_compat.
split; [apply Bool.Is_true_eq_left | apply Bool.Is_true_eq_true].
Qed.
Lemma self_is_updating_token_pool_correct:
forall accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool,
self_is_updating_token_pool = false <->
~
Spec.Storage.sto_selfIsUpdatingTokenPool
(accounts,
(self_is_updating_token_pool, (freeze_baker, lq_total),
(manager, token_address, (token_pool, xtz_pool)))).
Proof.
destruct self_is_updating_token_pool; cbv; intuition.
Qed.
Lemma comparison_to_int_nat_match_0:
forall (a : data (Comparable_type nat)),
(comparison_to_int match a with | 0%N => Eq | N.pos _ => Lt end <? 0)%Z = true <->
(0 < a)%N.
Proof.
intros []; cbv; intuition congruence.
Qed.
Lemma iff_both_false :
forall A B : Prop,
(A -> False) ->
(B -> False) ->
A <-> B.
Proof. intuition. Qed.
Lemma ex_match :
forall A (m : M A) P,
match m with
| Failed _ _ => False
| Return x => P x
end <-> (exists x, m = Return x /\ P x).
Proof.
intros A m P.
destruct m.
- apply iff_both_false; intuition.
destruct H as [ x [H1 H2] ].
discriminate.
- intuition.
+ exists a. intuition.
+ destruct H as [ x [H1 H2] ]. congruence.
Qed.
Lemma some_match :
forall A (m : Datatypes.option A) P,
match m with
| None => False
| Some x => P x
end <-> (exists x, m = Some x /\ P x).
intros A m P.
destruct m.
- intuition.
+ exists a. intuition.
+ destruct H as [ x [H1 H2] ]. congruence.
- apply iff_both_false; intuition.
destruct H as [ x [H1 H2] ].
discriminate.
Qed.
(* TODO: Arvid: I've copied this from somewhere, should be moved to the correct place *)
Ltac fold_eval_precond :=
change (@eval_precond_body (@eval_precond ?fuel)) with (@eval_precond (S fuel)).
Ltac ex_and_comm_intro x :=
repeat rewrite ex_and_comm;
apply forall_ex; intro x.
Lemma bool_false_not b : b = false <-> ~ b.
Proof.
rewrite (iff_sym (Bool.not_true_iff_false _)).
destruct b; simpl; split; auto.
Qed.
Local Lemma ediv a b d r :
ediv_N a b = Some (d, r) <-> (d = (a / b)%N /\ r = (a mod b)%N) /\ (0 < b)%N.
Proof.
unfold ediv_N; destruct b; simpl; split.
- discriminate.
- lia.
- intro H; injection H; intros Hr Hd; rewrite Hr, Hd; unfold N.lt; simpl; auto.
- intros [[Hd Hr] _]; rewrite Hd, Hr; auto.
Qed.
Lemma comp_to_int_Eq c : (comparison_to_int c =? 0)%Z = true <-> c = Eq.
Proof.
destruct c; simpl; split; auto; discriminate.
Qed.
Lemma comp_to_int_Lt c : (comparison_to_int c <? 0)%Z = true <-> c = Lt.
Proof.
destruct c; simpl; split; auto; discriminate.
Qed.
Lemma comp_to_int_Gt c : (comparison_to_int c >? 0)%Z = true <-> c = Gt.
Proof.
destruct c; simpl; split; auto; discriminate.
Qed.
Local Lemma comp_nat_to_int_leb x y : (comparison_to_int (x ?= y)%N >=? 0)%Z = true <-> (x >= y)%N.
Proof.
unfold N.ge; destruct (x ?= y)%N; simpl; unfold Z.geb; simpl; split; auto.
2: discriminate.
all: intros _ H; discriminate.
Qed.
Lemma compare_gt_lt t a b : compare t a b = Lt <-> compare t b a = Gt.
Proof.
split.
- intro Hlt.
case_eq (compare t b a).
+ rewrite compare_eq_iff.
intros He.
symmetry in He.
rewrite <- compare_eq_iff in He.
congruence.
+ intro Hba.
assert (compare t a a = Lt) by (exact (comparable.lt_trans _ _ _ _ Hlt Hba)).
assert (compare t a a = Eq) by (rewrite compare_eq_iff; reflexivity).
congruence.
+ intro; reflexivity.
- intro Hgt.
case_eq (compare t a b).
+ rewrite compare_eq_iff.
intros He.
symmetry in He.
rewrite <- compare_eq_iff in He.
congruence.
+ intro; reflexivity.
+ intro Hab.
assert (compare t a a = Gt) by (exact (comparable.gt_trans _ _ _ _ Hab Hgt)).
assert (compare t a a = Eq) by (rewrite compare_eq_iff; reflexivity).
congruence.
Qed.
Lemma comp_tez_Lt_Gt a b :
tez.compare a b = Gt <-> tez.compare b a = Lt.
Proof.
change tez.compare with (compare mutez).
symmetry.
apply compare_gt_lt.
Qed.
Lemma mutez_nonneg t : tez.compare (0 ~Mutez) t <> Gt.
Proof.
simpl.
unfold tez.compare. unfold tez.to_int64.
unfold int64bv.int64_compare.
unfold int64bv.compare.
rewrite Z.compare_le_iff.
apply tez.to_Z_lower_bound.
Qed.
Lemma compare_eq_comm : forall t a b,
compare t a b = Eq <-> compare t b a = Eq.
Proof.
intros t a b.
transitivity (a = b).
apply compare_eq_iff.
transitivity (b = a). intuition.
symmetry. apply compare_eq_iff.
Qed.
Lemma comparison_to_int_compare_gt_lt:
forall (t : comparable_type) (a b : comparable_data t),
(comparison_to_int (compare t a b) <? 0)%Z = true <->
(comparison_to_int (compare t b a) >? 0)%Z = true.
Proof.
intros t a b.
rewrite comp_to_int_Lt, comp_to_int_Gt.
apply compare_gt_lt.
Qed.
Lemma check_deadline_correct :
forall deadline,
(comparison_to_int (now env ?= deadline) <? 0)%Z = true <->
Spec.check_deadline env deadline.
Proof.
intros deadline.
unfold Spec.check_deadline, Spec.cmp_ltb. simpl.
destruct (_ ?= _)%Z; cbv; intuition.
Qed.
Lemma Z_comparison_to_int_lt :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) <? 0)%Z = true <-> (z1 < z2)%Z.
Proof.
intros z1 z2. simpl. rewrite Z.ltb_lt. destruct (Z.compare_spec z1 z2); simpl; lia.
Qed.
Lemma Z_comparison_to_int_le :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) <=? 0)%Z = true <-> (z1 <= z2)%Z.
Proof.
intros z1 z2. simpl. rewrite Z.leb_le. destruct (Z.compare_spec z1 z2); simpl; lia.
Qed.
Lemma Z_comparison_to_int_gt :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) >? 0)%Z = true <-> (z1 > z2)%Z.
Proof.
intros z1 z2. simpl. rewrite <- Zgt_is_gt_bool. destruct (Z.compare_spec z1 z2); simpl; lia.
Qed.
Lemma Z_comparison_to_int_ge :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) >=? 0)%Z = true <-> (z1 >= z2)%Z.
Proof.
intros z1 z2. simpl.
rewrite Z.geb_leb.
rewrite Z.leb_le.
destruct (Z.compare_spec z1 z2); simpl; lia.
Qed.
Lemma N_comparison_to_int_gt :
forall (n1 n2 : N),
(comparison_to_int (compare nat n1 n2) >? 0)%Z = true <-> (n1 > n2)%N.
Proof.
intros n1 n2. simpl. rewrite <- Zgt_is_gt_bool. destruct (N.compare_spec n1 n2); simpl; lia.
Qed.
Lemma N_comparison_to_int_ge :
forall (n1 n2 : N),
(comparison_to_int (compare nat n1 n2) >=? 0)%Z = true <-> (n1 >= n2)%N.
Proof.
intros n1 n2. simpl.
rewrite Z.geb_leb.
rewrite Z.leb_le.
destruct (N.compare_spec n1 n2); simpl; lia.
Qed.
Lemma comp_tez_Eq a b :
tez.compare a b = Eq <-> tez.compare b a = Eq.
Proof.
change tez.compare with (compare mutez); apply compare_eq_comm.
Qed.
Lemma cmp_mutez_gt_lt t :
(comparison_to_int (tez.compare t (0 ~Mutez)) >? 0)%Z = true <->
(comparison_to_int (tez.compare (0 ~Mutez) t) <? 0)%Z = true.
Proof.
rewrite comp_to_int_Lt, comp_to_int_Gt.
apply comp_tez_Lt_Gt.
Qed.
Lemma match_z_eq :
forall (z : Z),
(match z with
| 0 => 0
| Z.pos y' => Z.pos y'
| Z.neg y' => Z.neg y'
end)%Z = z.
Proof. destruct z; reflexivity. Qed.
Lemma Spec_cmp_eqb_comparison_to_int :
forall a x y,
Spec.cmp_eqb x y =
(comparison_to_int (compare a x y) =? 0)%Z.
Proof.
intros a x y. unfold Spec.cmp_eqb. now destruct (compare _ _ _).
Qed.
Lemma mutez_N_comparison_to_int_le :
forall t1 t2,
(comparison_to_int (compare mutez t1 t2) <=? 0)%Z = true <->
((Z.to_N (tez.to_Z t1)) <= (Z.to_N (tez.to_Z t2)))%N.
Proof.
intros t1 t2.
rewrite tez_compare_mutez_to_nat.
reflexivity.
Qed.
Lemma Z_abs_N_sub :
forall (n1 n2 : N),
(0 <= Z.of_N n1 - Z.of_N n2)%Z ->
Z.abs_N (Z.of_N n1 - Z.of_N n2)%Z =
(n1 - n2)%N.
Proof.
intros n1 n2 H.
rewrite Zabs2N.inj_sub.
now do 2 rewrite Zabs2N.id.
lia.
Qed.
Lemma comparison_to_int_eq_comm : forall t a b,
(comparison_to_int (compare t a b) =? 0)%Z =
(comparison_to_int (compare t b a) =? 0)%Z.
Proof.
intros t a b.
case_eq (compare t a b); intro Hcomp; simpl.
- apply compare_eq_comm in Hcomp. now rewrite Hcomp.
- case_eq (compare t b a); intro Hcomp'; try reflexivity.
assert (a <> b). apply compare_diff. intuition.
apply compare_eq_iff in Hcomp'. congruence.
- case_eq (compare t b a); intro Hcomp'; try reflexivity.
assert (a <> b). apply compare_diff. intuition.
apply compare_eq_iff in Hcomp'. congruence.
Qed.
Lemma compare_int_compare_spec :
forall a b, CompareSpec (a = b) (a < b)%Z (b < a)%Z (compare int a b).
Proof. apply Z.compare_spec. Qed.
Lemma compare_nat_compare_spec :
forall a b, CompareSpec (a = b) (a < b)%N (b < a)%N (compare nat a b).
Proof. apply N.compare_spec. Qed.
Lemma N_compare_lt: forall n1 n2 : N, ((compare nat n1 n2) = Lt)%Z <-> (n1 < n2)%N.
Proof.
intros n1 n2.
pose proof (compare_nat_compare_spec n1 n2).
inversion H; intuition.
Qed.
Lemma N_compare_gt: forall n1 n2 : N, ((compare nat n1 n2) = Gt)%Z <-> (n1 > n2)%N.
Proof.
intros n1 n2.
pose proof (compare_nat_compare_spec n1 n2).
inversion H; intuition.
Qed.
Lemma Z_comparison_to_int_geb :
forall (z1 z2 : Z),
(comparison_to_int (compare int z1 z2) >=? 0)%Z = (z1 >=? z2)%Z.
Proof.
intros z1 z2.
destruct (compare_int_compare_spec z1 z2); simpl.
- rewrite H.
repeat rewrite Z.geb_leb.
repeat rewrite Z.leb_refl.
reflexivity.
- repeat rewrite Z.geb_leb.
apply Z.leb_gt in H. rewrite H. reflexivity.
- repeat rewrite Z.geb_leb.
apply Z.lt_le_incl in H.
rewrite <- Z.ge_le_iff in H.
rewrite Zge_is_le_bool in H.
rewrite H. reflexivity.
Qed.
Lemma comp_tez_comp_to_int x y :
(comparison_to_int (tez.compare y x) >=? 0)%Z = true <-> @Spec.cmp_leb mutez x y.
Proof.
unfold Spec.cmp_leb, compare, simple_compare.
destruct (tez.compare x y) eqn:eq.
1: change tez.compare with (compare mutez) in eq; rewrite compare_eq_comm in eq;
change (compare mutez) with tez.compare in eq.
2: rewrite (iff_sym (comp_tez_Lt_Gt _ _)) in eq.
3: rewrite comp_tez_Lt_Gt in eq.
all: rewrite eq; simpl; unfold Z.geb; simpl; intuition; auto.
Qed.
Local Definition get_amount_bought_rem x y z
:= ((x * 997 * z) mod (y * 1000 + x * 997))%N.
Lemma tez_neq_zero t :
t <> (0 ~Mutez) <-> (0 < Spec.mutez_to_nat t)%N.
Proof.
unfold Spec.mutez_to_nat.
change 0%N with (Z.to_N (tez.to_Z (0 ~Mutez))).
rewrite <- tez_to_Z_bij.
rewrite <- Z2N.inj_iff by apply tez.to_Z_lower_bound.
split; simpl; intro H; lia.
Qed.
Section ep_xtzToToken.
Opaque N.mul.
Opaque compare.
Lemma ep_xtzToToken_correct
(p : data dexter_definition.parameter_ep_xtzToToken_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
8 <= fuel ->
eval_precond fuel env Def.ep_xtzToToken
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_xtzToToken env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct p as [to [min_tokens_bought deadline]].
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
do 8 more_fuel; simpl; fold_mutez_goal; clear fuel Hfuel.
change (compare mutez) with tez.compare.
rewrite bool_false_not, check_deadline_correct, !cmp_nat_lt_zero, cmp_mutez_gt_lt, !cmp_mutez_lt_zero.
fold_mutez_goal.
do 4 apply and_both.
rewrite !mutez_to_nat; split.
- intros [H_xtz_pool [H_token_pool [[xtz_pool_nat tez] [H_xtz_pool_nat [[amount rem] H]]]]].
injection H_xtz_pool_nat; clear H_xtz_pool_nat; intros _ H_xtz_pool_nat; clear tez.
destruct H as [H_amount [[tokens_bought tez] H]].
injection H_amount; clear H_amount; intros _ H_amount; clear rem.
rewrite ediv in H; destruct H as [[[H_tokens_bought _] H_non_zero] H]; clear tez.
unfold Spec.mutez_to_nat, Spec.nat_to_mutez.
assert (H_tokens_bought_spec :
Spec.get_amount_bought amount xtz_pool_nat token_pool = tokens_bought).
{ unfold Spec.get_amount_bought; rewrite H_tokens_bought.
rewrite N.add_comm, N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N).
destruct amount; destruct xtz_pool_nat; auto. }
unfold dexter_definition.self_type, dexter_definition.parameter_ty, annotation.
rewrite H_amount, H_xtz_pool_nat.
rewrite H_tokens_bought_spec; clear H_tokens_bought H_tokens_bought_spec.
destruct H as [H_tokens_bought_min [H_tokens_bought_max H]]; revert H.
unfold Spec.mutez_add; simpl; rewrite Z.add_comm.
destruct (tez.of_Z _ ) as [e | xtz_pool' ]; simpl.
1: intuition.
intros [transfer_contract [H_transfer_contract H]].
injection H; intros H_ret_sto H_ret_ops; clear H.
rewrite comp_nat_to_int_leb in H_tokens_bought_min.
split; auto; split; auto; split; auto.
split. {
apply Z_comparison_to_int_le in H_tokens_bought_max; lia. }
split with xtz_pool'; split with transfer_contract.
split; auto; split; auto; split; auto.
rewrite (eq_sym H_ret_sto); do 4 f_equal.
destruct (_ - _)%Z eqn:eq in H_tokens_bought_max.
3: discriminate.
all: lia.
- intros [H_xtz_pool [H_token_pool [H_tokens_bought_min [H_tokens_bought_max [xtz_pool' [transfer_contract [H_xtz_pool' [H_transfer_contract [H_ret_sto H_ret_ops]]]]]]]]].
split; auto; split; auto.
split with (Spec.mutez_to_nat xtz_pool, 0 ~Mutez); split; auto.
split with (Spec.mutez_to_nat (amount env), 0 ~Mutez); split; auto.
split with (Spec.get_amount_bought (Spec.mutez_to_nat (amount env)) (Spec.mutez_to_nat xtz_pool) token_pool,
get_amount_bought_rem (Spec.mutez_to_nat (amount env)) (Spec.mutez_to_nat xtz_pool) token_pool).
rewrite ediv; split.
1:{ unfold Spec.get_amount_bought, get_amount_bought_rem; split.
split.
rewrite N.add_comm, N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N). reflexivity.
rewrite N.add_comm, N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N). reflexivity.
rewrite tez_neq_zero in H_xtz_pool; lia. }
rewrite comp_nat_to_int_leb; split; auto.
unfold Spec.mutez_add, add in H_xtz_pool'.
unfold dexter_definition.self_type, dexter_definition.parameter_ty, annotation in H_xtz_pool'.
rewrite Z.add_comm, H_xtz_pool'; simpl; clear H_xtz_pool'.
split.
apply Z_comparison_to_int_le. lia.
destruct (_ - _)%Z eqn:eq.
3: lia.
all: split with transfer_contract; split; auto.
all: rewrite H_ret_ops, H_ret_sto; do 6 f_equal; lia.
Qed.
End ep_xtzToToken.
Lemma ep_addLiquidity_no_lqt_correct
(p : data dexter_definition.parameter_ep_addLiquidity_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
300 <= fuel ->
eval_seq_precond fuel env DefAddLqt.ep_addLiquidity2_no_lqt
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_addLiquidity_no_lqt env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
do 4 more_fuel.
simpl. (* 8s *)
repeat fold_mutez_goal. (* 1s *)
destruct p as ((owner, min_lqt_minted), (max_tokens_deposited, deadline)).
unfold Spec.ep_addLiquidity_no_lqt.
rewrite ex_and_comm.
rewrite mutez_to_nat.
rewrite underex_and_comm.
setoid_rewrite some_equal_inv.
setoid_rewrite and_assoc.
rewrite ex_eq_simpl.
rewrite iff_comm.
rewrite ex_order.
match goal with
| [ |- (exists (x : ?T1) (y : ?T2), ?P /\ ?Q /\ ?R /\ ?S)
<-> _ ] =>
setoid_replace (exists (x : T1) (y : T2), P /\ Q /\ R /\ S) with
((exists (x : T1), (exists (y : T2), P /\ S) /\ Q) /\ R)
end.
rewrite iff_comm.
unfold Spec.set_account_balance.
unfold Spec.map_get_def.
unfold Spec.map_get.
destruct (map.get) as [(balance, allowances)|] eqn:Hmapget; simpl.
- rewrite precond_exists.
unfold precond_ex.
rewrite underex_and_comm.
simpl. apply and_both_0_inv.
+ apply tez_compare_mutez_to_nat.
+ apply forall_ex. intro x.
simpl. apply and_both_0_inv.
* apply mutez_add_correct.
* apply forall_ex. intro t.
rewrite N.add_comm.
rewrite !shim_pair_equal_spec.
intuition.
- (* Arvid-TODO: this is copy-pasted from the previous goal *)
rewrite precond_exists.
unfold precond_ex.
rewrite underex_and_comm.
simpl. apply and_both_0_inv.
+ apply tez_compare_mutez_to_nat.
+ apply forall_ex. intro x.
simpl. apply and_both_0_inv.
* apply mutez_add_correct.
* apply forall_ex. intro t.
rewrite N.add_comm.
rewrite !shim_pair_equal_spec.
intuition.
- (* attempts put existential binders in iff in head, then apply forall_ex. *)
Ltac and_comm' := match goal with
| [ |- context[?P /\ ?Q] ] =>
match P with
| (exists (x : ?T), _) =>
setoid_replace (P /\ Q) with (Q /\ P) by intuition;
rewrite ex_and_comm
end
| [ |- context[?P /\ ?Q] ] =>
match Q with
| (exists (x : ?T), _) =>
rewrite ex_and_comm
end
end.
(* put existential binders in iff in head, then apply intuition *)
Ltac ex_intuition :=
repeat
(repeat (and_comm'; try rewrite ex_and_comm);
apply forall_ex; intro);
intuition.
ex_intuition.
Qed.
Lemma ep_addLiquidity_some_lqt_correct
(p : data dexter_definition.parameter_ep_addLiquidity_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
300 <= fuel ->
eval_seq_precond fuel env DefAddLqt.ep_addLiquidity3_some_lqt
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_addLiquidity_some_lqt env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
Opaque N.add.
do 3 more_fuel.
simpl. (* 28s *)
repeat fold_mutez_goal. (* 0.9s *)
destruct p as ((owner, min_lqt_minted), (max_tokens_deposited, deadline)).
unfold Spec.ep_addLiquidity_some_lqt. simpl.
do 2 rewrite mutez_to_nat.
do 2 (setoid_rewrite some_equal_inv; rewrite ex_eq_simpl).
rewrite iff_comm.
rewrite <- ediv_N_some_iff'.
unfold Spec.set_account_balance.
unfold Spec.get_account_balance.
unfold Spec.map_get_def.
unfold Spec.map_get.
rewrite <- tez_to_Z_bij.
rewrite <- Z2N.inj_iff by apply tez.to_Z_lower_bound.
Ltac rewrite_spec :=
match goal with
| [ |- _ <->
?PpoolNz' /\
?Ptoken_dep_lb /\
?PpoolNz /\
?Plqt_minted_lb /\
?Ptoken_dep_ub /\
(exists (x : ?Tx),
?Ppool /\
(exists (c : ?Tc),
?Ptransfer /\ ?Pret))
]
=>
setoid_replace
(PpoolNz' /\
Ptoken_dep_lb /\
PpoolNz /\
Plqt_minted_lb /\
Ptoken_dep_ub /\
(exists (x : Tx),
Ppool /\
(exists (c : Tc),
Ptransfer /\ Pret))) with
(PpoolNz /\
(exists (c : Tc) (x : Tx),
Ptransfer /\
Ppool /\
Plqt_minted_lb /\
Ptoken_dep_lb /\
Ptoken_dep_ub /\
Pret))
end.
(* The following four cases are very similar, but I had a hard time
* refactorising the proof. *)
destruct (Z.of_N (_ mod _) =? 0)%Z eqn:Hmod;
repeat rewrite comparison_to_int_pos;
rewrite <- ediv_N_some_iff';
destruct (map.get) as [(balance, allowances)|] eqn:Hmapget;
simpl;
rewrite precond_exists;
unfold precond_ex.
- rewrite_spec.
rewrite Spec_Nceiling_mod by apply Hmod.
+ apply and_both.
apply forall_ex; intro c.
apply forall_ex; intro x.
repeat rewrite N_comparison_to_int_opp.
repeat rewrite N_comparison_to_int_le.
rewrite mutez_add_correct.
N_add_comm lq_total.
N_add_comm token_pool.
N_add_comm balance.
destruct ret_sto.
rewrite !shim_pair_equal_spec.
intuition.
+ repeat rewrite ex_and_comm.
setoid_rewrite ex_and_comm.
rewrite ex_order.
apply forall_ex; intro x.
repeat rewrite ex_and_comm.
apply forall_ex; intro c.
intuition.
- rewrite_spec.
rewrite Spec_Nceiling_mod by apply Hmod.
+ apply and_both.
apply forall_ex; intro c.
apply forall_ex; intro x.
repeat rewrite N_comparison_to_int_opp.
repeat rewrite N_comparison_to_int_le.
rewrite mutez_add_correct.
N_add_comm lq_total.
N_add_comm token_pool.
N_add_comm 0%N.
destruct ret_sto.
unfold Spec.map_update.
rewrite !shim_pair_equal_spec.
intuition.
+ repeat rewrite ex_and_comm.
setoid_rewrite ex_and_comm.
rewrite ex_order.
apply forall_ex; intro x.
repeat rewrite ex_and_comm.
apply forall_ex; intro c.
intuition.
- rewrite_spec.
rewrite Spec_Nceiling_rem by apply Hmod.
+ apply and_both.
apply forall_ex; intro c.
apply forall_ex; intro x.
repeat rewrite N_comparison_to_int_opp.
repeat rewrite N_comparison_to_int_le.
rewrite mutez_add_correct.
N_add_comm lq_total.
N_add_comm token_pool.
N_add_comm balance.
repeat N_add_comm 1%N.
destruct ret_sto.
unfold Spec.map_update.
rewrite !shim_pair_equal_spec.
intuition.
+ repeat rewrite ex_and_comm.
setoid_rewrite ex_and_comm.
rewrite ex_order.
apply forall_ex; intro x.
repeat rewrite ex_and_comm.
apply forall_ex; intro c.
intuition.
- rewrite_spec.
rewrite Spec_Nceiling_rem by apply Hmod.
+ apply and_both.
apply forall_ex; intro c.
apply forall_ex; intro x.
repeat rewrite N_comparison_to_int_opp.
repeat rewrite N_comparison_to_int_le.
rewrite mutez_add_correct.
N_add_comm lq_total.
N_add_comm token_pool.
N_add_comm 0%N.
repeat N_add_comm 1%N.
destruct ret_sto.
unfold Spec.map_update.
rewrite !shim_pair_equal_spec.
intuition.
+ repeat rewrite ex_and_comm.
setoid_rewrite ex_and_comm.
rewrite ex_order.
apply forall_ex; intro x.
repeat rewrite ex_and_comm.
apply forall_ex; intro c.
intuition.
Qed.
Section ep_addLiquidity.
Opaque compare.
Lemma ep_addLiquidity_correct
(p : data dexter_definition.parameter_ep_addLiquidity_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
400 <= fuel ->
eval_precond fuel env DefAddLqt.ep_addLiquidity_alt
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_addLiquidity env p sto ret_ops ret_sto.
Proof.
(* TODO: Arvid: This proof is a mess and should be cleaned up *)
intros Hfuel.
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
unfold DefAddLqt.ep_addLiquidity_alt, DefAddLqt.ep_addLiquidity1_header.
Opaque DefAddLqt.ep_addLiquidity2_no_lqt DefAddLqt.ep_addLiquidity3_some_lqt.
do 3 (more_fuel; simpl).
repeat fold_mutez_goal.
unfold Spec.ep_addLiquidity.
unfold Spec.ep_addLiquidity_header.
destruct p as ((owner, min_lqt_minted), (max_tokens_deposited, deadline)).
(*
* re-order conjuncts to match spec.
*)
repeat rewrite and_assoc.
repeat apply and_both_0_inv.
simpl (Spec.Storage.sto_lqtTotal _).
destruct lq_total; simpl;
repeat fold_eval_precond;
rewrite fold_eval_seq_precond_aux.
- rewrite ep_addLiquidity_no_lqt_correct; [| lia].
unfold Spec.ep_addLiquidity_no_lqt.
ex_and_comm_intro c.
ex_and_comm_intro x.
intuition.
- rewrite ep_addLiquidity_some_lqt_correct; [| lia].
unfold Spec.ep_addLiquidity_some_lqt.
ex_and_comm_intro c.
ex_and_comm_intro x.
intuition.
- rewrite <- comparison_to_int_compare_gt_lt.
apply cmp_mutez_lt_zero.
- now rewrite N_comparison_to_int_lt.
- now rewrite N_comparison_to_int_lt.
- apply check_deadline_correct.
- apply self_is_updating_token_pool_correct.
Qed.
End ep_addLiquidity.
Section ep_approve.
(* It's better not to unfold compare in this prove,
* this makes it easier to use util.eqb_eq.
* I open a section to avoid disturbing other proofs.
*)
Opaque compare.
Lemma ep_approve_correct
(p : data dexter_definition.parameter_ep_approve_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
400 <= fuel ->
eval_precond fuel env Def.ep_approve
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_approve env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
time (do 4 more_fuel; simpl; repeat fold_mutez_goal). (* 1s *)
destruct p as (spender, (new_allowance, current_allowance)).
unfold Spec.ep_approve.
rewrite and_comm.
rewrite and_assoc.
apply (and_both_0 cmp_mutez_eq_zero).
rewrite and_comm.
apply (and_both_0 (Bool_is_true_false_iff_not _)).
unfold Spec.Storage.sto_set_accounts.
unfold Spec.map_get_def.
unfold Spec.map_get.
destruct (map.get _ _ _ (sender env)) as [(sender_balance, sender_allowances)|] eqn:Hmapget; simpl.
- destruct (map.get _ _ _ spender) as [spender_allowance|] eqn:Hmapget';
repeat rewrite util.eqb_eq; rewrite !shim_pair_equal_spec; intuition.
- repeat rewrite util.eqb_eq; rewrite !shim_pair_equal_spec; intuition.
Qed.
End ep_approve.
Lemma ep_default_correct
(p : data dexter_definition.parameter_ep_default_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
400 <= fuel ->
eval_precond fuel env Def.ep_default
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_default env p sto ret_ops ret_sto.
Proof.
intro Hfuel.
auto_fuel.
destruct_sto sto
accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
rewrite precond_exists.
unfold precond_ex.
apply and_both_0.
unfold Spec.Storage.sto_selfIsUpdatingTokenPool.
- (* Check self_updating_token_pool is false *)
apply is_false.
- (* Check xtz_pool is set to xtz_pool + amount *)
unfold Spec.ep_default, Spec.mutez_add, add.
unfold Spec.Storage.sto_xtzPool.
unfold Spec.Storage.sto_set_xtzPool.
simpl.
intuition.
+ destruct H.
destruct H.
exists x.
rewrite <- H.
rewrite Zplus_comm.
injection H0.
clear H0.
intros.
rewrite H0, H1.
intuition reflexivity.
+ destruct H.
destruct H.
exists x.
rewrite <- H.
rewrite Zplus_comm.
destruct H0.
subst.
intuition reflexivity.
Qed.
Lemma Spec_cmp_geb_comparison_to_int_0 :
forall a b,
(@Spec.cmp_geb nat a b) =
(comparison_to_int (compare int (Z.of_N a - Z.of_N b) 0) >=? 0)%Z.
intros a b.
unfold Spec.cmp_geb.
rewrite Z_comparison_to_int_geb.
rewrite Z.geb_leb.
destruct (compare_nat_compare_spec a b); symmetry;
destruct (Z.leb_spec0 0%Z (Z.of_N a - Z.of_N b)); try congruence; try lia.
Qed.
Hint Unfold
Spec.Storage.sto_accounts
Spec.Storage.sto_set_accounts
Spec.Storage.sto_accounts
Spec.set_allowance
Spec.check_allowance_update
Spec.get_account_balance
Spec.set_account_balance : spec_storage.
Hint Unfold
Spec.map_get_def
Spec.map_update
Spec.map_get : spec_map.
Hint Unfold Spec.nat_to_mutez Spec.mutez_to_nat Spec.mutez_sub Spec.env_sender : spec.
Ltac unfold_spec :=
autounfold with spec_storage;
autounfold with spec_map;
autounfold with spec.
Section ep_removeLiquidity.
Opaque compare.
Opaque Z.modulo.
Lemma tez_fact_l:
forall (min_x : data (Comparable_type mutez))
(x' : data (Comparable_type nat))
(x : tez.mutez),
tez.to_Z x = Z.of_N x' ->
(Z.to_N (tez.to_Z min_x) <= Z.to_N (tez.to_Z x))%N ->
(x' >= Z.to_N (tez.to_Z min_x))%N.
Proof.
intros min_x x' x H.
intuition; rewrite H in *; rewrite N2Z.id in *; lia.
Qed.
Lemma tez_fact_r:
forall (min_x : data (Comparable_type mutez))
(x' : data (Comparable_type nat))
(x : tez.mutez),
tez.to_Z x = Z.of_N x' ->
(x' >= Z.to_N (tez.to_Z min_x))%N ->
(Z.to_N (tez.to_Z min_x) <= Z.to_N (tez.to_Z x))%N.
Proof.
intros min_x x' x H.
intuition; rewrite H in *; rewrite N2Z.id in *; lia.
Qed.
Lemma ep_removeLiquidity_correct
(p : data dexter_definition.parameter_ep_removeLiquidity_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
400 <= fuel ->
eval_precond fuel env Def.ep_removeLiquidity
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_removeLiquidity env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
time (do 7 more_fuel; simpl; repeat fold_mutez_goal). (* 52s *)
destruct p as ((owner, (to, lqt_burned)),
(min_xtz_withdrawn,
(min_tokens_withdrawn, deadline))).
unfold Spec.ep_removeLiquidity.
apply and_both_0. apply Bool_is_true_false_iff_not.
match goal with
| [ |- _ <-> ?Pamount /\ ?Pdeadline /\ ?Pmin_xtz_wd /\ ?Pmin_tok_wd /\ ?Plqt_total /\ ?P_lqt_burned /\ ?P ] =>
setoid_replace (Pamount /\ Pdeadline /\ Pmin_xtz_wd /\ Pmin_tok_wd /\ Plqt_total /\ P_lqt_burned /\ P) with
(Pdeadline /\ Pamount /\ Pmin_xtz_wd /\ Pmin_tok_wd /\ P_lqt_burned /\ Plqt_total /\ P)
by intuition
end.
apply and_both_0. apply check_deadline_correct.
apply and_both_0. apply cmp_mutez_eq_zero.
rewrite cmp_mutez_lt_zero. apply and_both.
rewrite !N_comparison_to_int_lt, !N_le_neq2.
repeat apply and_both.
Ltac N_mul_comm_with x :=
match goal with
| [ |- context[(?P * x)%N] ] =>
replace (P * x)%N
with (x * P)%N by apply N.mul_comm
end.
unfold_spec; simpl.
destruct (map.get _ _ _ owner) as [(balance, allowances)|] eqn:Hmapget; simpl.
- setoid_rewrite some_equal_inv.
rewrite ex_eq_simpl.
rewrite Spec_cmp_eqb_comparison_to_int.
rewrite mutez_to_nat.
rewrite comparison_to_int_eq_comm.
destruct (_ =? _)%Z eqn:Hsender_is_owner.
+ setoid_rewrite some_equal_inv.
rewrite ex_eq_simpl.
rewrite <- ediv_N_some_iff'.
rewrite precond_exists.
unfold precond_ex.
rewrite match_z_eq.
setoid_rewrite <- ediv_N_some_iff'.
repeat setoid_rewrite ex_match.
setoid_rewrite some_match.
ex_and_comm_intro xtz_withdrawn.
ex_and_comm_intro xtz_pool'.
ex_and_comm_intro to_contract.
ex_and_comm_intro fa12_contract.
rewrite !N_comparison_to_int_ge.
rewrite !N_comparison_to_int_le.
rewrite !Z_comparison_to_int_le.
rewrite !mutez_N_comparison_to_int_le.
simpl.
simpl in Hmapget.
rewrite Hmapget.
rewrite !shim_pair_equal_spec.
repeat (N_mul_comm_with lqt_burned).
repeat rewrite <- tez.of_Z_to_Z_eqv.
intuition (
subst;
repeat rewrite Z_abs_N_sub by lia;
try reflexivity;
try congruence;
try lia;
eauto using tez_fact_l, tez_fact_r).
+ destruct (map.get _ _ _ _ allowances) as [current_allowance|] eqn:Hmapget_allowances; simpl.
* setoid_rewrite some_equal_inv.
rewrite ex_eq_simpl.
rewrite ex_eq_simpl.
rewrite <- ediv_N_some_iff'.
rewrite precond_exists.
unfold precond_ex.
rewrite match_z_eq.
setoid_rewrite <- ediv_N_some_iff'.
rewrite Spec_cmp_geb_comparison_to_int_0.
rewrite Z_comparison_to_int_geb.
destruct (Z.of_N current_allowance - Z.of_N lqt_burned >=? 0)%Z
eqn:Hhas_allowance; [| intuition congruence].
apply Z.geb_le in Hhas_allowance.
repeat setoid_rewrite ex_match.
ex_and_comm_intro xtz_withdrawn.
rewrite map.map_updateeq.
rewrite precond_exists.
unfold precond_ex.
ex_and_comm_intro xtz_pool'.
repeat setoid_rewrite some_match.
ex_and_comm_intro to_contract.
ex_and_comm_intro fa12_contract.
repeat rewrite N_comparison_to_int_ge.
repeat rewrite N_comparison_to_int_le.
repeat rewrite Z_comparison_to_int_le.
repeat rewrite mutez_N_comparison_to_int_le.
unfold_spec; simpl.
simpl in Hmapget.
rewrite Hmapget; simpl.
rewrite map.map_updateeq.
rewrite !shim_pair_equal_spec.
repeat (N_mul_comm_with lqt_burned).
simpl.
repeat rewrite <- tez.of_Z_to_Z_eqv.
intuition (
subst;
repeat rewrite Z_abs_N_sub by lia;
try reflexivity;
try congruence;
try lia;
eauto using tez_fact_l, tez_fact_r).
* apply iff_both_false.
-- intros [H1 [H2 [x [H3 _]]]]. congruence.
-- intuition.
- (* both sides imply false *)
apply iff_both_false.
+ intros [x [H2 _]]. discriminate.
+ lia.
Qed.
End ep_removeLiquidity.
Lemma ep_setBaker_correct
(p : data dexter_definition.parameter_ep_setBaker_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
400 <= fuel ->
eval_precond fuel env Def.ep_setBaker
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_setBaker env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
auto_fuel.
destruct_sto sto
accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
rewrite (eqb_eq address).
rewrite (eqb_eq mutez).
rewrite negb_is_true.
destruct p as (param_baker, param_freeze_baker).
apply and_both_0.
- apply is_false.
- apply and_both_2.
intros.
simpl.
intuition.
+ injection H3.
intros.
clear H3.
rewrite <- H4.
reflexivity.
+ congruence.
+ rewrite H2.
rewrite H4.
reflexivity.
Qed.
Lemma ep_updateTokenPool_correct
(p : data dexter_definition.parameter_ep_updateTokenPool_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
400 <= fuel ->
eval_precond fuel env Def.ep_updateTokenPool
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_updateTokenPool env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
auto_fuel.
destruct_sto sto
accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
rewrite (eqb_eq mutez).
rewrite (eqb_eq address).
intuition.
simpl.
subst.
- destruct H3.
intuition.
exists x.
simpl.
injection H3.
intros.
clear H3.
rewrite <- H4.
rewrite <- H1.
intuition reflexivity.
- destruct H.
apply H.
- destruct H.
apply H.
- destruct H.
intuition.
subst.
destruct self_is_updating_token_pool.
+ elimtype False. apply H. constructor.
+ reflexivity.
- destruct H.
intuition.
exists x.
subst.
intuition reflexivity.
Qed.
Lemma ep_updateTokenPoolInternal_correct
(p : data dexter_definition.parameter_ep_updateTokenPoolInternal_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
(* TODO: fuel may have to be adapted to suit the entrypoint *)
400 <= fuel ->
eval_precond fuel env Def.ep_updateTokenPoolInternal
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_updateTokenPoolInternal env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
auto_fuel.
destruct_sto sto
accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
rewrite (eqb_eq mutez).
rewrite (eqb_eq address).
apply and_both_0.
- reflexivity.
- intuition.
+ subst.
unfold Spec.Storage.sto_selfIsUpdatingTokenPool.
constructor.
+ intuition congruence.
+ simpl.
injection H2.
clear H2.
intros.
rewrite H1.
reflexivity.
+ destruct self_is_updating_token_pool.
* reflexivity.
* contradiction.
+ rewrite H3.
rewrite H1.
reflexivity.
Qed.
Section ep_tokenToXtz.
Opaque N.mul.
Opaque compare.
Lemma ep_tokenToXtz_correct
(p : data dexter_definition.parameter_ep_tokenToXtz_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
8 <= fuel ->
eval_precond fuel env Def.ep_tokenToXtz
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_tokenToXtz env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct p as [[owner to] [tokens_sold [min_xtz_bought deadline]]].
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
do 8 more_fuel; simpl; fold_mutez_goal; clear fuel Hfuel.
rewrite bool_false_not, check_deadline_correct, comp_to_int_Eq, tez.compare_eq_iff, !cmp_nat_lt_zero, !cmp_mutez_lt_zero.
fold_mutez_goal; do 3 apply and_both.
rewrite mutez_to_nat; split.
- intros [H_xtz_pool [H_token_pool [H_tokens_sold [H_min_xtz_bought [[xtz_pool_nat tez] [H_xtz_pool_nat [[xtz_bought rem] H]]]]]]].
injection H_xtz_pool_nat; clear H_xtz_pool_nat; intros _ H_xtz_pool_nat; clear tez.
rewrite ediv in H; destruct H as [[[H_xtz_bought _] _] H]; clear rem.
unfold Spec.mutez_to_nat, Spec.nat_to_mutez.
assert (H_xtz_bought_spec :
Spec.get_amount_bought tokens_sold token_pool xtz_pool_nat = xtz_bought).
{ unfold Spec.get_amount_bought; rewrite H_xtz_bought.
rewrite N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N).
reflexivity. }
rewrite H_xtz_pool_nat; clear H_xtz_pool_nat.
rewrite H_xtz_bought_spec; clear H_xtz_bought H_xtz_bought_spec xtz_pool_nat.
destruct (Z.of_N xtz_bought); clear xtz_bought; revert H.
all: destruct (tez.of_Z _) as [e | xtz_bought_mutez]; simpl; auto.
all: destruct (tez.of_Z (_ - _)) as [e | xtz_pool'] eqn:eq; simpl.
all: intros [H_xtz_bought_mutez H].
all: match goal with
| [ H : False |- _] => intuition
| _ => auto
end.
all: destruct H as [to_contract [H_to_contract [transfer_contract [H_transfer_contract H]]]].
all: injection H; intros H_ret_sto H_ret_ops; clear H.
all: rewrite comp_tez_comp_to_int in H_xtz_bought_mutez.
all: do 5 (split; auto).
all: unfold annotation; rewrite H_to_contract.
all: split with transfer_contract; split with xtz_pool'.
all: rewrite N.add_comm.
all: auto.
- intros [H_min_xtz_bought [H_xtz_pool [H_token_pool [H_tokens_sold H]]]].
do 4 (split; auto).
split with (Z.to_N (tez.to_Z xtz_pool), 0 ~Mutez); split; auto.
split with (Spec.get_amount_bought tokens_sold token_pool (Spec.mutez_to_nat xtz_pool),
get_amount_bought_rem tokens_sold token_pool (Spec.mutez_to_nat xtz_pool)).
rewrite ediv; split.
1:{ unfold Spec.get_amount_bought, get_amount_bought_rem; split.
1: rewrite N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N); auto.
lia. }
unfold Spec.nat_to_mutez in H; revert H; destruct (Z.of_N _).
all: destruct (tez.of_Z _) as [e | xtz_bought_mutez]; simpl; auto.
all: destruct (contract_ _ _ _) as [to_contract | ].
all: match goal with
| [ |- _ /\ False -> _] => intuition
| _ => auto
end.
all: intros [H_xtz_bought_mutez [transfer_contract [xtz_pool' [H_xtz_pool' [H_transfer_contract [H_ret_sto H_ret_ops]]]]]].
all: rewrite comp_tez_comp_to_int; split; auto.
all: unfold Spec.mutez_sub, sub in H_xtz_pool'.
all: rewrite H_xtz_pool'; simpl.
all: split with to_contract; split; auto.
all: split with transfer_contract; split; auto.
all: rewrite N.add_comm; subst; auto.
Qed.
End ep_tokenToXtz.
Section ep_tokenToToken.
Opaque N.mul.
Opaque compare.
Lemma ep_tokenToToken_correct
(p : data dexter_definition.parameter_ep_tokenToToken_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
8 <= fuel ->
eval_precond fuel env Def.ep_tokenToToken
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_tokenToToken env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
destruct p as [[output_dexter_address [min_tokens_bought owner]] [to [tokens_sold deadline]]].
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
do 8 more_fuel; simpl; fold_mutez_goal; clear fuel Hfuel.
rewrite bool_false_not, comp_to_int_Eq, tez.compare_eq_iff, check_deadline_correct, !cmp_nat_lt_zero, !cmp_mutez_lt_zero.
fold_mutez_goal; apply and_both; rewrite and_comm_3.
do 2 apply and_both.
rewrite mutez_to_nat; split.
- intros [H_tokens_sold [H_min_tokens_bought [H_xtz_pool [H_token_pool [[xtz_pool_nat tez] [H_xtz_pool_nat [[xtz_bought rem] H]]]]]]].
injection H_xtz_pool_nat; clear H_xtz_pool_nat; intros _ H_xtz_pool_nat; clear tez.
rewrite ediv in H; destruct H as [[[H_xtz_bought _] _] H]; clear rem.
assert (H_xtz_bought_spec :
Spec.get_amount_bought tokens_sold token_pool xtz_pool_nat = xtz_bought).
{ unfold Spec.get_amount_bought; rewrite H_xtz_bought.
rewrite N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N).
reflexivity. }
unfold Spec.mutez_to_nat, Spec.nat_to_mutez.
rewrite H_xtz_pool_nat; clear H_xtz_pool_nat.
rewrite H_xtz_bought_spec; clear H_xtz_bought H_xtz_bought_spec xtz_pool_nat.
destruct (Z.of_N xtz_bought); clear xtz_bought; revert H.
all: destruct (tez.of_Z _) as [e | xtz_bought_mutez]; simpl; auto.
all: destruct (tez.of_Z (_ - _)) as [e | xtz_pool'] eqn:eq; simpl.
all: match goal with
| [ |- False -> ?P] => intuition
| _ => auto
end.
all: intros [xtzToToken_contract [H_xtzToToken_contract [transfer_contract [H_transfer_contract H]]]].
all: injection H; intros H_ret_sto H_ret_ops; clear H.
all: do 4 (split; auto).
all: split with transfer_contract; split with xtz_pool'.
all: unfold dexter_definition.parameter_ep_xtzToToken_ty.
all: rewrite H_xtzToToken_contract.
all: auto.
- intros [H_tokens_sold [H_min_tokens_bought [H_xtz_pool [H_token_pool H]]]].
do 4 (split; auto).
split with (Z.to_N (tez.to_Z xtz_pool), 0 ~Mutez).
split; auto.
split with (Spec.get_amount_bought tokens_sold token_pool (Spec.mutez_to_nat xtz_pool),
get_amount_bought_rem tokens_sold token_pool (Spec.mutez_to_nat xtz_pool)).
rewrite ediv; split.
1:{ unfold Spec.get_amount_bought, get_amount_bought_rem; split.
1: rewrite N.mul_comm, !(N.mul_comm _ 997%N), (N.mul_comm _ 1000%N); auto.
lia. }
unfold Spec.nat_to_mutez in H; revert H; destruct (Z.of_N _).
all: destruct (tez.of_Z _) as [e | xtz_bought_mutez]; simpl; auto.
all: destruct (tez.of_Z (_ - _)) as [e | xtz_pool'] eqn:eq; simpl.
all: destruct (contract_ _ _ _) as [xtzToToken_contract | ].
all: intros [transfer_contract [xtz_pool'' H]].
all: match goal with
| [ H : False |- ?P] => intuition
| _ => auto
end.
all: destruct H as [H_xtz_pool'' [H_transfer_contract [H_ret_sto H_ret_ops]]].
all: unfold Spec.mutez_sub, sub in H_xtz_pool''.
all: rewrite H_xtz_pool'' in eq; clear H_xtz_pool''.
all: match goal with
| [ |- False ] => discriminate
| _ => auto
end.
all: injection eq; clear eq; intro eq; rewrite eq in H_ret_sto; clear eq xtz_pool''.
all: split with xtzToToken_contract; split; auto.
all: split with transfer_contract; split; auto.
all: subst; auto.
Qed.
End ep_tokenToToken.
Lemma ep_setManager_correct
(p : data dexter_definition.parameter_ep_setManager_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : Datatypes.list (data operation))
(ret_sto : data dexter_definition.storage_ty)
(fuel : Datatypes.nat) :
400 <= fuel ->
eval_precond fuel env Def.ep_setManager
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
Spec.ep_setManager env p sto ret_ops ret_sto.
Proof.
intros Hfuel.
auto_fuel.
destruct_sto sto accounts self_is_updating_token_pool freeze_baker lq_total manager token_address token_pool xtz_pool.
apply and_both_0.
- apply is_false.
- apply and_both_0.
rewrite (eqb_eq mutez).
intuition.
+ rewrite (eqb_eq address).
simpl; intuition congruence.
Qed.
End entrypoints.
End Dexter_verification.
