https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 7ccb33612808dc6eba01b4d54e638e3ebade2924 authored by Raphaƫl Cauderlier on 18 March 2021, 11:08:58 UTC
Use the fuel-free WP in Dexter proofs
Use the fuel-free WP in Dexter proofs
Tip revision: 7ccb336
dexter_verification_ep_tokenToXtz.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. *)
(* Coq *)
Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import NArith.
Require Import ZArith.
Require Import Coq.Setoids.Setoid.
Require Import Coq.micromega.Lia.
From Coq Require Import Program.Tactics.
(* Mi-Cho-Coq *)
Require Import semantics.
Require Import util.
Import error.
Require List.
(* Dexter *)
Require dexter_definition.
Require dexter_spec.
Require Import dexter_util.
Require Import dexter_spec_util.
Module Spec := dexter_spec.
Module Def := dexter_definition.
Import Def.Storage.
Import Tactics.
Require Import contract_semantics.
(* It's better not to unfold compare in this proof,
* this makes it easier to use util.eqb_eq.
*)
Opaque N.mul.
Opaque N.add.
Opaque Z.modulo.
Opaque compare.
Ltac if_step :=
match goal with [ H : context G[if ?X then _ else _] |- _] =>
let Heq := fresh "Hif" in
destruct X eqn:Heq
| [ |- context G[if ?X then _ else _] ] =>
let Heq := fresh "Hif" in
destruct X eqn:Heq
end; try easy.
Ltac error_step :=
match goal with
[ H : context G [ match ?X with | Failed _ _ => _ | Return _ => _ end ] |- _ ] =>
destruct X eqn:?Hstep; try easy
| [ |- context G [ match ?X with | Failed _ _ => _ | Return _ => _ end ] ] =>
destruct X eqn:?Hstep; try easy
end.
Ltac option_step :=
match goal with
| [ H : ?X = _ |- context G [ match ?X with | Some _ => _ | None => _ end ] ] =>
rewrite H
end
|| match goal with
| [ H : context G [ match ?X with | Some _ => _ | None => _ end ] |- _ ] =>
destruct X eqn:?Hstep; try easy
| [ |- context G [ match ?X with | Some _ => _ | None => _ end ] ] =>
destruct X eqn:?Hstep; try easy
end.
Ltac simplify_eqs :=
repeat multimatch goal with
| [ H : Some _ = Some _ |- _ ] => inversion H; subst; clear H
| [ H : Return _ = Return _ |- _ ] => inversion H; subst; clear H
| [ H : (_, _) = (_, _) |- _ ] => inversion H; subst; clear H
| [ H : (_ :: _)%list = (_ :: _)%list |- _ ] => inversion H; subst; clear H
end.
Ltac fold_amount :=
repeat multimatch goal with
| [ H : context G [ @amount dexter_definition.self_type ] |- _ ] =>
fail
| [ H : context G [ @amount ?T ] |- _ ] =>
let x := context G [ @amount dexter_definition.self_type ] in
change x in H
end.
Ltac one_rewrite :=
repeat multimatch goal with
| [ H : _ = _ |- _ ] => solve [rewrite H; auto]
end.
Ltac easy_match :=
repeat multimatch goal with
| [ H : ?X = _ |- match ?X with _ => _ end ] => solve [rewrite H; auto]
end.
Definition ep_tokenToXtz := Eval vm_compute in Def.ep_tokenToXtz.
Lemma ep_tokenToXtz_same : Def.ep_tokenToXtz = ep_tokenToXtz.
Proof.
reflexivity.
Qed.
Lemma ep_tokenToXtz_correct
(env : @proto_env dexter_definition.self_type)
(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) :
eval0_seq_precond 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.
rewrite ep_tokenToXtz_same.
destruct p as [owner [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.
simpl.
do 4 (try apply and_both_0).
- rewrite bool_false_not. easy.
- rewrite <- check_deadline_correct.
rewrite comparison_to_int_opp.
rewrite comparison_to_int_Z_compare_ltb.
rewrite comparison_to_int_leb.
rewrite Z.leb_gt.
rewrite <- Zlt_is_lt_bool.
easy.
- rewrite Z_gtb_false_leb_iff.
apply comparison_to_int_tez_compare_le_zero.
- unfold Spec.fa12.transfer, Spec.fa12.is_ep_transfer, Spec.mutez_sub,
Spec.fa12.ep_transfer_annot, Spec.fa12.ep_transfer_ty,
Spec.get_amount_bought, Spec.nat_to_mutez, Spec.mutez_to_nat, Spec.cmp_leb in * |- *.
split.
+ intro Heval.
repeat (destruct_conjs; destruct_exists; unfold precond in * |- *;
simplify_eqs).
fold_mutez.
rewrite Z.div_1_r in * |- *.
rewrite Z.mul_1_r in * |- *.
rewrite Z.mod_1_r in * |- *.
simpl in * |- *.
simplify_eqs.
rewrite ediv_spec in * |- *.
destruct_conjs. subst.
error_step.
destruct_conjs.
error_step.
simplify_eqs.
destruct (N.eq_dec (accounts * 1000 + tokens_sold * 997) 0) eqn:Hr.
++ lia.
++ error_step. split; simplify_eqs.
+++ simplify_eqs. rewrite compare_antisym. unfold CompOpp.
destruct (compare mutez m0 min_xtz_bought); cbn in H |- *; auto. congruence.
+++ rewrite H4.
eexists; eexists.
split; [eassumption|].
split; [eassumption|].
split; [reflexivity|].
reflexivity.
+ intro Hspec.
destruct (N.eq_dec (accounts * 1000 + tokens_sold * 997) 0) eqn:Hr.
++ easy.
++ error_step. destruct_conjs. option_step. destruct_exists. destruct_conjs. subst.
simpl in * |- *. fold_mutez.
eexists.
split.
+++ error_step. rewrite Z.mod_1_r in * |-. simpl in * |- *. unfold tez.of_Z in * |-.
cbv in Hstep1. congruence. rewrite Z.div_1_r.
rewrite Z.mod_1_r in Hstep1. simpl in * |- *. unfold tez.of_Z in * |-. cbv in Hstep1.
inversion Hstep1. eauto.
+++ fold_mutez. simpl.
eexists.
rewrite ediv_spec. intuition.
lia.
unfold precond.
rewrite Z.mul_1_r. rewrite Hstep.
intuition; try easy.
apply comparison_to_int_lt_0_false; auto.
eexists.
intuition; try easy; eauto.
eexists.
intuition; try easy; eauto.
one_rewrite.
Qed.