(* 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 fold_mutez :=
  repeat match goal with
         | [ H : context G [tez.valid_mutez ?X] |- _ ] =>
           match X with
           | Vector.cons _ _ _ _ =>
             let x := fresh "V" in
             pose (x := X);
             fold x in H
           | _ => fail
           end

         | [ |- context G [tez.valid_mutez ?X] ] =>
           match X with
           | Vector.cons _ _ _ _ =>
             let x := fresh "V" in
             pose (x := X);
             fold x
           | _ => fail
           end
         end;
    repeat match goal with
         | [ |- context G [ tez.to_Z (tez.valid_mutez ?V) ] ] =>
           let Y := fresh "CV" in
           pose (Y := int64bv.to_Z V); cbv in Y;
           let x := context G [ Y ] in
           change x; unfold Y; clear Y; try clear V
         | [ H : context G [ tez.to_Z (tez.valid_mutez ?V) ] |- _ ] =>
           let Y := fresh "CV" in
           pose (Y := int64bv.to_Z V); cbv in Y;
           let x := context G [ Y ] in
           change x in H; unfold Y in H; clear Y; try clear V
         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.

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_seq_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 [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. clear fuel Hfuel.

  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.
         +++ unfold annotation.
             option_step. try easy.
             eexists. eexists.
             intuition; eauto.
    + 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.