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