(* Open Source License *)
(* Copyright (c) 2021 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.
Lemma ep_addLiquidity_wp :
forall (env : @proto_env dexter_definition.self_type)
(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,
400 <= fuel ->
eval_precond fuel env Def.ep_addLiquidity
(fun x => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <->
(let (_, y) := p in
let (x0, _) := p in
let (_, y1) := y in
let (x2, _) := y in
let (_, y3) := y1 in
let (x4, _) := y1 in
let (_, y5) := sto in
let (_, y6) := y5 in
let (_, y7) := y6 in
let (x8, _) := y7 in
x8 = false /\
(comparison_to_int (compare timestamp (now env) y3) >=? 0)%Z = false /\
(let (_, y9) := sto in
let (x10, _) := y9 in
exists y11 : N * tez.mutez,
match tez.of_Z (Z.of_N (Z.to_N (tez.to_Z x10 mod tez.to_Z (1 ~Mutez)))) with
| Failed _ _ => None
| Return rem => Some (Z.to_N (tez.to_Z x10 / tez.to_Z (1 ~Mutez)), rem)
end = Some y11 /\
(let (x11, _) := y11 in
exists y13 : N * tez.mutez,
match tez.of_Z (Z.of_N (Z.to_N (tez.to_Z (amount env) mod tez.to_Z (1 ~Mutez)))) with
| Failed _ _ => None
| Return rem => Some (Z.to_N (tez.to_Z (amount env) / tez.to_Z (1 ~Mutez)), rem)
end = Some y13 /\
(let (x12, _) := y13 in
let (_, y15) := sto in
let (_, y16) := y15 in
let (x15, _) := y16 in
exists y18 : N * N,
ediv_N (x12 * x15) x11 = Some y18 /\
(let (x16, _) := y18 in
let (x17, _) := sto in
exists y21 : N * N,
ediv_N (x12 * x17) x11 = Some y21 /\
(let (_, y22) := y21 in
let (x19, _) := y21 in
if (comparison_to_int (compare nat y22 0%N) =? 0)%Z
then
(comparison_to_int (compare nat x19 x4) >? 0)%Z = false /\
(comparison_to_int (compare nat x16 x2) <? 0)%Z = false /\
(let (_, y24) := sto in
let (_, y25) := y24 in
let (_, y26) := y25 in
let (_, y27) := sto in
let (_, y28) := y27 in
let (x25, _) := y28 in
let (_, y30) := sto in
let (_, _) := y30 in
let (_, _) := sto in
let (x29, _) := sto in
let (_, y34) := sto in
let (x31, _) := y34 in
precond (tez.of_Z (tez.to_Z x31 + tez.to_Z (amount env)))
(fun z : tez.mutez =>
let (_, y36) := y26 in
let (_, y37) := y36 in
let (_, y38) := y37 in
let (x35, _) := y38 in
exists
y40 : data (contract (pair (Comparable_type address) (pair (Comparable_type address) (Comparable_type nat)))),
contract_ (Some "%transfer"%string)
(pair (Comparable_type address) (pair (Comparable_type address) (Comparable_type nat))) x35 =
Some y40 /\
(let (_, y41) := y26 in
let (_, y42) := y41 in
let (_, y43) := y42 in
let (_, y44) := y43 in
exists
y45 : data (contract (pair (Comparable_type int) (Comparable_type address))),
contract_ (Some "%mintOrBurn"%string) (pair (Comparable_type int) (Comparable_type address)) y44 = Some y45 /\
((transfer_tokens env
(pair (Comparable_type address) (pair (Comparable_type address) (Comparable_type nat)))
(sender env, (address_ unit (self env None I), x19)) (0 ~Mutez) y40
:: transfer_tokens env (pair (Comparable_type int) (Comparable_type address))
(Z.of_N x16, x0) (0 ~Mutez) y45 :: nil)%list, ((x29 + x19)%N, (z, ((x25 + x16)%N, y26))), tt) =
(ret_ops, ret_sto, tt))))
else
(comparison_to_int (compare nat (1 + x19)%N x4) >? 0)%Z = false /\
(comparison_to_int (compare nat x16 x2) <? 0)%Z = false /\
(let (_, y24) := sto in
let (_, y25) := y24 in
let (_, y26) := y25 in
let (_, y27) := sto in
let (_, y28) := y27 in
let (x25, _) := y28 in
let (_, y30) := sto in
let (_, _) := y30 in
let (_, _) := sto in
let (x29, _) := sto in
let (_, y34) := sto in
let (x31, _) := y34 in
precond (tez.of_Z (tez.to_Z x31 + tez.to_Z (amount env)))
(fun z : tez.mutez =>
let (_, y36) := y26 in
let (_, y37) := y36 in
let (_, y38) := y37 in
let (x35, _) := y38 in
exists
y40 : data (contract (pair (Comparable_type address) (pair (Comparable_type address) (Comparable_type nat)))),
contract_ (Some "%transfer"%string)
(pair (Comparable_type address) (pair (Comparable_type address) (Comparable_type nat))) x35 =
Some y40 /\
(let (_, y41) := y26 in
let (_, y42) := y41 in
let (_, y43) := y42 in
let (_, y44) := y43 in
exists
y45 : data (contract (pair (Comparable_type int) (Comparable_type address))),
contract_ (Some "%mintOrBurn"%string) (pair (Comparable_type int) (Comparable_type address)) y44 = Some y45 /\
((transfer_tokens env
(pair (Comparable_type address) (pair (Comparable_type address) (Comparable_type nat)))
(sender env, (address_ unit (self env None I), (1 + x19)%N)) (0 ~Mutez) y40
:: transfer_tokens env (pair (Comparable_type int) (Comparable_type address))
(Z.of_N x16, x0) (0 ~Mutez) y45 :: nil)%list, ((x29 + (1 + x19))%N, (z, ((x25 + x16)%N, y26))), tt) =
(ret_ops, ret_sto, tt)))))))))).
Proof.
intros env p sto ret_ops ret_sto fuel Hfuel.
do 6 (more_fuel; simpl).
reflexivity.
Qed.