https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 416793b544257750fdc08474933a5c139fe3e056 authored by Yann Regis-Gianas on 08 March 2021, 10:11:49 UTC
Dexter2/Spec: Take care of division by zero
Dexter2/Spec: Take care of division by zero
Tip revision: 416793b
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.
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)
(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.
* do 3 (apply and_both_0; [rewrite eqb_eq;reflexivity|]).
* rewrite bool_false_not, check_deadline_correct, comp_to_int_Eq, tez.compare_eq_iff, !cmp_nat_lt_zero, !comparison_to_int_tez_compare_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_spec 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: apply comparison_to_int_compare_spec_cmp_leb_tez 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_spec; 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 <- comparison_to_int_compare_spec_cmp_leb_tez; 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.
*)
Admitted.