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

Require Import NArith.
Require Import ZArith.
Require Import syntax.
Require Import semantics.
Require Import comparable.
Require Import error.
Require Import utils.
Require Import fa12_interface.
Require Import fa12_dexter.

Import List.ListNotations.

Open Scope list_scope.

Module FA12DexterSpec (C : ContractContext).

  Module fa12AxiomsImpl := FA12AxiomsImpl C.
  Import fa12AxiomsImpl.
 
  Import fa12TypesImpl fa12DataImpl fa12Notations.
  Import self semantics.

  (** Entry point specifications *)
  Section EntryPoints.

    Variable (env : @proto_env self_type).

    Notation sender := (sender env).

    (** Entry point: ep_approve *)
    Definition ep_approve
               (p : data parameter_ep_approve_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(spender, allowance') := p in
      let allowance := getAllowance sto sender spender in
      (allowance = 0%N \/ allowance' = 0%N) /\
      ret_sto = setAllowance sto sender spender allowance' /\
      ret_ops = nil.

    (** Entry point: ep_transfer *)
    Definition ep_transfer
               (p : data parameter_ep_transfer_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(from, (to, value)) := p in
      exists from_balance',
      let from_balance := getBalance sto from in
      from_balance = (from_balance' + value)%N /\
      let sto' := setBalance sto from from_balance' in
      let to_balance := getBalance sto' to in
      let sto'' := setBalance sto' to (to_balance + value)%N in
      if (compare_equal sender from)
         then ret_sto = sto'' /\ ret_ops = nil
         else exists allowance',
              let allowance := getAllowance sto from sender in
              allowance = (allowance' + value)%N /\
              ret_sto = setAllowance sto'' from sender allowance' /\
              ret_ops = nil.

    (** Entry point: ep_mintOrBurn *)
    Definition ep_mintOrBurn
               (p : data parameter_ep_mintOrBurn_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(amount, owner) := p in
      sender = getAdmin sto /\ exists balance',
      let balance := getBalance sto owner in
      Z.of_N balance' = (Z.of_N balance + amount)%Z /\
      let supply' := Z.abs_N (Z.of_N (getTotalSupply sto) + amount)%Z in
      ret_sto = setBalance (setTotalSupply sto supply') owner balance' /\
      ret_ops = nil.

    (** Entry point: ep_getTotalSupply *)
    Definition ep_getTotalSupply
               (p : data parameter_ep_getTotalSupply_ty)
               (sto : data storage_ty)
               (ret_ops : data (list operation))
               (ret_sto : data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(_, contr) := p in
      let supply := getTotalSupply sto in
      let op := transfer_tokens env nat supply (0 ~Mutez) contr in
      ret_sto = sto /\ ret_ops = [op].

    (** Entry point: ep_getBalance *)
    Definition ep_getBalance
               (p : data parameter_ep_getBalance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '(owner, contr) := p in
      let balance := getBalance sto owner in
      let op := transfer_tokens env nat balance (0 ~Mutez) contr in
      ret_sto = sto /\ ret_ops = [op].

    (** Entry point: ep_getAllowance *)
    Definition ep_getAllowance
               (p : data parameter_ep_getAllowance_ty)
               (sto : data storage_ty)
               (ret_ops :  data (list operation))
               (ret_sto :  data storage_ty) :=
      amount env = (0 ~Mutez) /\
      let '((owner, spender), contr) := p in
      let allowance := getAllowance sto owner spender in
      let op := transfer_tokens env nat allowance (0 ~Mutez) contr in
      ret_sto = sto /\ ret_ops = [op].

  End EntryPoints.

  (** Full spec *)
  Definition spec
             (env : @proto_env self_type)
             (p : data parameter_ty)
             (sto : data storage_ty)
             (ret_ops : data (list operation))
             (ret_sto : data storage_ty) :=
    match p with
      | inl (inl (inl q)) => ep_approve env q sto ret_ops ret_sto
      | inl (inl (inr q)) => ep_getAllowance env q sto ret_ops ret_sto
      | inl (inr (inl q)) => ep_getBalance env q sto ret_ops ret_sto
      | inl (inr (inr q)) => ep_getTotalSupply env q sto ret_ops ret_sto
      | inr (inl q) => ep_mintOrBurn env q sto ret_ops ret_sto
      | inr (inr q) => ep_transfer env q sto ret_ops ret_sto
    end.

End FA12DexterSpec.