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


Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import ZArith.
Require Import semantics.
Require Import util.
Require Import entrypoints.
Import error.
Require List.
Require Import Lia.

Definition parameter_ty :=
  ep_node
    (ep_leaf (lambda unit (list operation))) (Some "%do"%string)
    (ep_leaf unit) (Some "%default"%string).
Definition storage_ty := key_hash.

Module manager(C:ContractContext).

Module semantics := Semantics C. Import semantics.

Definition manager : full_contract _ parameter_ty None storage_ty :=
  { UNPAIR;
    IF_LEFT
      { (* 'do' entrypoint *)
        (* Assert no token was sent: *)
        (* to send tokens, the default entry point should be used *)
        PUSH mutez (0 ~mutez);
        AMOUNT;
        ASSERT_CMPEQ;
        (* Assert that the sender is the manager *)
        DUUP;
        IMPLICIT_ACCOUNT;
        ADDRESS;
        SENDER;
        ASSERT_CMPEQ;
        (* Execute the lambda argument *)
        UNIT;
        EXEC;
        PAIR
      }
      { (* 'default' entrypoint *)
        DROP1 ;
        NIL operation ;
        PAIR
      }
  }.

Definition manager_spec
           (env : @proto_env (Some (parameter_ty, None)))
           (storage : data storage_ty)
           (param : data (entrypoints.entrypoint_tree_to_type parameter_ty))
           (new_storage : data storage_ty)
           (returned_operations : data (list operation))
           (fuel : Datatypes.nat) :=
  match param with
  | inr tt =>
    (* %default: anybody can send tokens this does not modify the
    storage and produces no operation. *)
    new_storage = storage /\ returned_operations = nil
  | inl (build_lam _ _ _ lam) =>
    (* %do is only available to the stored manager and rejects non-null amounts*)
    amount env = (0 ~Mutez) /\
    sender env = address_ unit (implicit_account storage) /\
    new_storage = storage /\
    eval_seq (no_self env) lam fuel (tt, tt) = Return (returned_operations, tt)
  end.

Lemma eqb_eq a c1 c2 :
  BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = true <->
  c1 = c2.
Proof.
  rewrite BinInt.Z.eqb_eq.
  rewrite comparison_to_int_Eq.
  apply comparable.compare_eq_iff.
Qed.

Lemma eqb_neq a c1 c2 :
  BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0 = false <->
  c1 <> c2.
Proof.
  split.
  - intros H He.
    apply eqb_eq in He.
    congruence.
  - intro Hneq.
    rewrite <- eqb_eq in Hneq.
    generalize (BinInt.Z.eqb (comparison_to_int (compare a c1 c2)) Z0) Hneq.
    intros []; congruence.
Qed.

Lemma and_right {P Q R : Prop} : P -> (Q <-> R) -> (Q <-> (P /\ R)).
Proof.
  intuition.
Qed.

Lemma and_both {P Q R : Prop} : (Q <-> R) -> ((P /\ Q) <-> (P /\ R)).
Proof.
  intuition.
Qed.

Lemma fold_eval_precond fuel :
  @eval_precond_body (@semantics.eval_precond fuel) =
  @semantics.eval_precond (S fuel).
Proof.
  reflexivity.
Qed.

Lemma if_false_is_and (b : Datatypes.bool) P : (if b then P else false) <-> b = true /\ P.
Proof.
  destruct b.
  - intuition.
  - simpl.
    intuition discriminate.
Qed.

Lemma manager_correct
      (env : @proto_env (Some (parameter_ty, None)))
      (storage : data storage_ty)
      (param : data (entrypoints.entrypoint_tree_to_type parameter_ty))
      (new_storage : data storage_ty)
      (returned_operations : data (list operation))
      (fuel : Datatypes.nat) :
  fuel >= 42 ->
  eval_seq env manager (2 + fuel) ((param, storage), tt) = Return ((returned_operations, new_storage), tt)
  <-> manager_spec env storage param new_storage returned_operations fuel.
Proof.
  intro Hfuel.
  unfold ">=" in Hfuel.
  rewrite return_precond.
  rewrite eval_seq_precond_correct.
  unfold manager_spec.
  more_fuel; simpl.
  more_fuel; simpl.
  destruct param as [(tff, lam)|[]].
  - rewrite (eqb_eq mutez).
    apply and_both.
    rewrite (eqb_eq address).
    apply and_both.
    repeat rewrite fold_eval_precond.
    fold (eval_seq_precond (S (S fuel)) (self_type := None)).
    rewrite <- eval_seq_precond_correct.
    rewrite precond_exists.
    unfold precond_ex.
    split.
    ++ intros ((ops, []), (Hops, Hs)).
       injection Hs; intros; subst.
       auto.
    ++ intros ([], Hlam).
       exists (returned_operations, tt).
       auto.
  - unfold data. simpl. intuition congruence.
Qed.

End manager.