(* 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 syntax.
Require Import semantics.
Require Import NArith.
Require Import ZArith.
Require Import comparable.
Require Import error.

Import List.ListNotations.

Open Scope list_scope.

Module annot.

  Import String.

  Definition transfer : string := "%transfer".
  Definition approve : string := "%approve".
  Definition getAllowance : string := "%getAllowance".
  Definition getBalance : string := "%getBalance".
  Definition getTotalSupply : string := "%getTotalSupply".

End annot.

(*! Parameter type definitions. !*)
Definition parameter_ep_transfer_ty
  := pair address (* :from *) (pair address (* :to *) nat (* :value *)).

Definition parameter_ep_approve_ty
  := pair address (* :spender *) nat (* :value *).

Definition parameter_ep_getAllowance_ty
  := pair (pair address (* :owner *) address (* :spender *)) (contract nat).

Definition parameter_ep_getBalance_ty
  := pair address (* :owner *) (contract nat).

Definition parameter_ep_getTotalSupply_ty
  := pair unit (contract nat).

Definition fa12_parameter_ty
  := or (or parameter_ep_transfer_ty (Some annot.transfer)
            parameter_ep_approve_ty (Some annot.approve)) None
        (or parameter_ep_getAllowance_ty (Some annot.getAllowance)
            (or parameter_ep_getBalance_ty (Some annot.getBalance)
                parameter_ep_getTotalSupply_ty (Some annot.getTotalSupply)) None) None.

(** Parameterizing over the implementation details for the FA1.2 contract. *)

Module Type FA12ContextTypes.

  Parameter parameter_ty : type.
  Parameter storage_ty : type.

End FA12ContextTypes.

Module Type FA12ContextData (C : ContractContext) (FT : FA12ContextTypes).

  Module semantics := Semantics C.
  Import semantics.

  Import FT.

  (** A storage can be invalid if, e.g., its totalSupply field does not equal the sum of balances. *)
  Parameter storage_valid : data storage_ty -> Prop.

  (** Given a parameter and a storage, determines the applicable FA1.2 entrypoint, if any.
      The storage can have additional fields, e.g., paused, that affect the FA1.2 entrypoints;
      for instance, if paused = true then the approve and transfer entrypoints are not applicable. *)
  Parameter extract_fa12_ep : data parameter_ty -> data storage_ty -> data (option fa12_parameter_ty).

  (** Given a storage and an owner, returns the balance of the owner if it exists; returns 0 otherwise. *)
  Parameter getBalance : data storage_ty -> data address -> data nat.

  (** Given a storage, an owner, and an amount, sets the balance of the owner to amount. *)
  Parameter setBalance : data storage_ty -> data address -> data nat -> data storage_ty.

  (** Setting the balance in a valid storage results in a valid storage. *) 
  Parameter setBalance_valid : forall sto owner amount, storage_valid sto -> storage_valid (setBalance sto owner amount).

  (** Returns the list of owners that have balances. *)
  Parameter getOwners : data storage_ty -> data (list address).

  (** Given a storage, an owner, and a spender, returns the allowance the owner has allocated for the spender, if any.
      Returns 0 if the owner does not have a balance or the spender has no allowance with the owner. *)
  Parameter getAllowance : data storage_ty -> data address -> data address -> data nat.

  (** Given a storage, an owner, a spender, and an amount, sets the allowance of the sender with the owner to amount. *)
  Parameter setAllowance : data storage_ty -> data address -> data address -> data nat -> data storage_ty.

  (** Setting the allowance in a valid storage results in a valid storage. *) 
  Parameter setAllowance_valid : forall sto owner spender amount, storage_valid sto -> storage_valid (setAllowance sto owner spender amount).

  (** Returns the total sum of balances. *)
  Parameter getTotalSupply : data storage_ty -> data nat.

End FA12ContextData.

Module err.

  Import String.

  Definition UnsafeAllowanceChange : string := "UnsafeAllowanceChange".

  Definition NotEnoughBalance : string := "NotEnoughBalance".

  Definition NotEnoughAllowance : string := "NotEnoughAllowance".

End err.

Module Self (FT : FA12ContextTypes).

  Import FT.

  Definition self_type : self_info := Some (parameter_ty, None).

End Self.

Module FA12Spec (C : ContractContext) (FT : FA12ContextTypes) (FD : FA12ContextData C FT).

  Module self := Self FT.
  Import self.

  Import FT.
  Import FD.
  Import semantics.

  (** Entry point specifications *)

  Section EntryPoints.

    Variable (env : @proto_env self_type).

    Definition sender := sender env.

    (** Entry point success: ep_approve *)
    Definition ep_approve_ret
               (p : data parameter_ep_approve_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      let '(spender, new_allowance) := p in
      let current_allowance := getAllowance sto sender spender in
      (current_allowance = 0%N \/ new_allowance = 0%N) /\
      ret_sto = setAllowance sto sender spender new_allowance /\
      ret_ops = nil.

    (** Entry point error: ep_approve *)
    Definition ep_approve_fail
               (p : data parameter_ep_approve_ty)
               (sto : data storage_ty)
               (e : exception) :=
      let '(spender, new_allowance) := p in
      let current_allowance := getAllowance sto sender spender in
      (current_allowance > 0 /\ new_allowance > 0)%N /\
      (e = Assertion_Failure _ (err.UnsafeAllowanceChange, current_allowance)).

    (** Entry point success: ep_transfer *)
    Definition ep_transfer_ret
               (p : data parameter_ep_transfer_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      let '(from, (to, amount)) := p in
      let from_balance := getBalance sto from in
      let from_balance' := getBalance ret_sto from in
      let to_balance := getBalance sto to in
      let sto' := setBalance sto from from_balance' in
      let sto'' := setBalance sto' to (to_balance + amount)%N in
      from_balance = (from_balance' + amount)%N /\
      match compare _ sender from with
         | Eq => ret_sto = sto''
         | _ => let current_allowance := getAllowance sto from sender in
                let current_allowance' := getAllowance ret_sto from sender in
                current_allowance = (current_allowance' + amount)%N /\
                ret_sto = setAllowance sto'' from sender current_allowance'
      end /\ ret_ops = nil.

    (** Entry point error: ep_transfer *)
    (** We assume from != to *)
    Definition ep_transfer_fail
               (p : data parameter_ep_transfer_ty)
               (sto : data storage_ty)
               (e : exception) :=
      let '(from, (to, amount)) := p in
      let from_balance := getBalance sto from in
      ((amount > from_balance)%N /\
       (e = Assertion_Failure _ (err.NotEnoughBalance, (amount, from_balance)))) \/
      match compare _ sender from with
         | Eq => False
         | _ => let current_allowance := getAllowance sto from sender in
                ((current_allowance < amount)%N /\
                 (e = Assertion_Failure _ (err.NotEnoughAllowance, (amount, current_allowance))))
      end.

    (** Entry point success: ep_getTotalSupply *)
    Definition ep_getTotalSupply_ret
               (p : data parameter_ep_getTotalSupply_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      let '(_, contr) := p in
      let value := getTotalSupply sto in
      exists tez,
      let token_transfer := transfer_tokens env nat value tez contr in
      value = List.fold_right (fun owner sum => (getBalance sto owner + sum)%N) 0%N (getOwners sto) /\
      ret_sto = sto /\ ret_ops = [token_transfer].

    (** Entry point success: ep_getBalance *)
    Definition ep_getBalance_ret
               (p : data parameter_ep_getBalance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      let '(owner, contr) := p in
      exists tez,
      let token_transfer := transfer_tokens env nat (getBalance sto owner) tez contr in
      ret_sto = sto /\ ret_ops = [token_transfer].

    (** Entry point success: ep_getAllowance *)
    Definition ep_getAllowance_ret
               (p : data parameter_ep_getAllowance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      let '((owner, spender), contr) := p in
      exists tez,
      let token_transfer := transfer_tokens env nat (getAllowance sto owner spender) tez contr in
      ret_sto = sto /\ ret_ops = [token_transfer].

  End EntryPoints.

  (** Full spec *)
  Definition main
             (env : @proto_env self_type)
             (p : data fa12_parameter_ty)
             (sto : data storage_ty)
             (m : M (stack (pair (list operation) storage_ty ::: nil))) :=
    match p with
      | (inl (inl p)) => match m with
                           | Return ((ret_ops, ret_sto), tt) => ep_transfer_ret env p sto ret_ops ret_sto
                           | Failed _ e => ep_transfer_fail env p sto e
                         end
      | (inl (inr p)) => match m with
                           | Return ((ret_ops, ret_sto), tt) => ep_approve_ret env p sto ret_ops ret_sto
                           | Failed _ e => ep_approve_fail env p sto e
                         end
      | (inr (inl p)) => match m with
                           | Return ((ret_ops, ret_sto), tt) => ep_getAllowance_ret env p sto ret_ops ret_sto
                           | _ => False
                         end
      | (inr (inr (inl p))) => match m with
                                 | Return ((ret_ops, ret_sto), tt) => ep_getBalance_ret env p sto ret_ops ret_sto
                                 | _ => False
                               end
      | (inr (inr (inr p))) => match m with
                                 | Return ((ret_ops, ret_sto), tt) => ep_getTotalSupply_ret env p sto ret_ops ret_sto
                                 | _ => False
                               end
    end.

End FA12Spec.