(* 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.