(* 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 NArith.
Require Import ZArith.
Require Import Coq.micromega.Lia.

(* Mi-Cho-Coq *)
Require Import semantics.
Import syntax.
Import comparable.

Require Import util.
Import error.

(* Contracts *)
Require Import contract_semantics.

(* Dexter *)
Require Import dexter_spec.
Require Import dexter_util.


  Module Tactics.
    Ltac auto_fuel :=
      repeat match goal with
             | [ |- context G[eval_precond] ]
               => more_fuel; simpl
             end.

    Tactic Notation "step" integer(k) reference(contract) :=
      do k (more_fuel ;
            cbn beta delta [
                  eval_precond_opcode
                    eval_seq_precond_body eval_seq_precond_body_aux
                    eval_precond eval_precond_body contract ] iota zeta);
         simpl stack_split;
         simpl stack_app;
         cbn iota beta.


    (* TODO: Arvid: This tactic, and its usage could be omitted if the
    appropriate mutez definitions and operations are rendered
    Opaque *)
    Ltac fold_mutez_goal :=
      match goal with
      | [ |- context[(exist (A := Vector.t _ _) ?P ?bv ?Hpbv)] ] =>
        match bv with
          (Vector.cons ?T ?f ?len ?l) =>
          let z := eval cbn in (int64bv.to_Z bv) in
              replace (exist P bv Hpbv)
          with (exist P (int64bv.of_Z_safe z eq_refl) Hpbv)
            by reflexivity
        end
      end.

    Ltac N_add_comm y :=
      match goal with
        [ |- context[(?x + y)%N]] =>
        replace (x + y)%N with (y + x)%N
          by apply N.add_comm
      end.

    Ltac ex_and_comm_intro x :=
      repeat rewrite ex_and_comm;
      apply forall_ex; intro x.

    (** Dexter specification-specific tactics *)
    Hint Unfold
         dexter_spec.nat_to_mutez
         dexter_spec.mutez_to_nat
         dexter_spec.mutez_sub
         dexter_spec.env_sender : spec.

    Ltac unfold_spec :=
      autounfold with spec.
  End Tactics.

  (*! Lemmas on specification !*)

  Lemma comparison_to_int_spec_cmp_eqb :
    forall a x y,
      dexter_spec.cmp_eqb x y =
      (comparison_to_int (compare a x y) =? 0)%Z.
  Proof.
    intros a x y. unfold dexter_spec.cmp_eqb. now destruct (compare _ _ _).
  Qed.

  Lemma comparison_to_int_compare_spec_cmp_leb_tez x y :
    @dexter_spec.cmp_leb mutez x y <->
    (comparison_to_int (tez.compare y x) >=? 0)%Z = true.
  Proof.
    change tez.compare with (compare mutez).
    unfold dexter_spec.cmp_leb.
    destruct (compare mutez x y) eqn:eq.
    1: rewrite compare_eq_comm in eq.
    2: rewrite compare_gt_lt in eq.
    3: rewrite <- compare_gt_lt in eq.
    all: rewrite eq; unfold Z.geb; simpl; intuition; auto.
  Qed.

  Lemma comparison_to_int_compare_spec_cmp_geb_nat :
    forall a b,
      (@dexter_spec.cmp_geb nat a b) =
      (comparison_to_int (compare int (Z.of_N a - Z.of_N b) 0) >=? 0)%Z.
  Proof.
    intros a b.

    unfold dexter_spec.cmp_geb.

    rewrite comparison_to_int_compare_int_geb.
    rewrite Z.geb_leb.

    destruct (compare_nat_compare_spec a b); symmetry;
      destruct (Z.leb_spec0 0%Z (Z.of_N a - Z.of_N b)); try congruence; try lia.
  Qed.

  Lemma mutez_add_correct:
    forall (x y z : tez.mutez),
      tez.of_Z (tez.to_Z y + tez.to_Z x) = Return z <->
      dexter_spec.mutez_add x y z.
  Proof. intros x y. now rewrite Z.add_comm. Qed.

  Lemma check_deadline_correct :
    forall env deadline,
      (comparison_to_int (now env ?= deadline) <? 0)%Z = true <->
      dexter_spec.check_deadline env deadline.
  Proof.
    intros env deadline.
    unfold dexter_spec.check_deadline, dexter_spec.cmp_ltb. simpl.
    destruct (_ ?= _)%Z; cbv; intuition.
  Qed.

  Lemma check_deadline_correct_alt :
    forall env deadline,
      (comparison_to_int (compare timestamp (now env) deadline) >=? 0)%Z = false <->
      dexter_spec.check_deadline env deadline.
  Proof.
    intros env deadline.
    unfold dexter_spec.check_deadline, dexter_spec.cmp_ltb. simpl.
    Transparent compare. simpl. Opaque compare.
    destruct (_ ?= _)%Z; cbv; intuition.
  Qed.

  (*! Spec_NCeiling !*)

  Lemma Spec_Nceiling_mod :
    forall (x y : N),
      (x mod y = 0)%N ->
      dexter_spec.Nceiling x y = (x / y)%N.
  Proof.
    intros x y H.
    unfold dexter_spec.Nceiling.
    rewrite surjective_pairing with (p := N.div_eucl _ _).
    unfold N.modulo in H.
    now rewrite H.
  Qed.

  Lemma Spec_Nceiling_rem :
    forall (x y : N),
      (x mod y <> 0)%N ->
      dexter_spec.Nceiling x y = (x / y + 1)%N.
  Proof.
    intros x y H.
    unfold dexter_spec.Nceiling.
    rewrite surjective_pairing with (p := N.div_eucl _ _).
    unfold N.modulo in H.
    destruct (snd _) eqn:Heqn; intuition.
  Qed.