(* 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 ZArith.
Require Import List.
Require Import Sorted.
Require Import comparable.
Require Import syntax.
Require Import semantics.
Require Import utils.

Module annot.

  Import String.

  Notation transfer := "%transfer".
  Notation approve := "%approve".
  Notation getAllowance := "%getAllowance".
  Notation getBalance := "%getBalance".
  Notation getTotalSupply := "%getTotalSupply".

End annot.

(** Parameter type definitions. *)
Definition parameter_ep_transfer_ty
  := pair address (pair address nat).

Definition parameter_ep_approve_ty
  := pair address nat.

Definition parameter_ep_getAllowance_ty
  := pair (pair address address) (contract nat).

Definition parameter_ep_getBalance_ty
  := pair address (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 FA12Types.

  Parameter parameter_ty : type.
  Parameter storage_ty : type.

End FA12Types.

Module Self (FT : FA12Types).

  Import FT.

  Notation self_type := (Some (parameter_ty, None)).

End Self.

Module Type FA12Data (C : ContractContext) (FT : FA12Types).

  Module semantics := Semantics C.
  Import semantics.

  Import FT.

  (** Given a parameter, determines the applicable FA1.2 entrypoint, if any. *)
  Parameter extract_fa12_ep : data parameter_ty -> data (option fa12_parameter_ty).

  (** Given a storage and an owner, returns the balance of the owner if it exists. *)
  Parameter getBalanceOpt : data storage_ty -> data address -> data (option 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.

  (** Given a storage, an owner, and a spender, returns the allowance the owner has allocated for the spender, if any. *)
  Parameter getAllowanceOpt : data storage_ty -> data address -> data address -> data (option 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.

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

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

End FA12Data.

Module FA12Notations (C : ContractContext) (FT : FA12Types) (FD : FA12Data C FT).

  Import FD.

  Notation getBalance sto owner :=
    match getBalanceOpt sto owner with
       | Some v => v
       | None => 0%N
     end.

  Notation getAllowance sto owner spender :=
    match getAllowanceOpt sto owner spender with
       | Some v => v
       | None => 0%N
     end.

  Notation isOwner sto owner :=
    match getBalanceOpt sto owner with
      | None => false
      | Some _ => true
    end.

  Notation isSpender sto owner spender :=
    match getAllowanceOpt sto owner spender with
      | None => false
      | Some _ => true
    end.

  Notation addBalance sto :=
    (fun owner sum => getBalance sto owner + sum)%N.

  Definition sumOfBalances sto (owners : cset_set address) :=
    let (l, _) := owners in
    fold_right (addBalance sto) 0%N l.

  Notation sumOfAllBalances sto :=
    (sumOfBalances sto (getOwners sto)).

  Definition storageValid sto :=
    getTotalSupply sto = sumOfAllBalances sto.

End FA12Notations.

Module Type FA12Axioms (C : ContractContext) (FT : FA12Types) (FD : FA12Data C FT).

  Import FD.
  Import semantics.

  Module fa12Notations := FA12Notations C FT FD.
  Import fa12Notations.

  Parameter ep_transfer_required : forall (q : data parameter_ep_transfer_ty),
    exists p, extract_fa12_ep p = Some (inl (inl q)).

  Parameter ep_approve_required : forall (q : data parameter_ep_approve_ty),
    exists p, extract_fa12_ep p = Some (inl (inr q)).

  Parameter ep_getAllowance_required : forall (q : data parameter_ep_getAllowance_ty),
    exists p, extract_fa12_ep p = Some (inr (inl q)).

  Parameter ep_getBalance_required : forall (q : data parameter_ep_getBalance_ty),
    exists p, extract_fa12_ep p = Some (inr (inr (inl q))).

  Parameter ep_getTotalSupply_required : forall (q : data parameter_ep_getTotalSupply_ty),
    exists p, extract_fa12_ep p = Some (inr (inr (inr q))).

  Parameter getBalance_setBalance_eq : forall sto owner amount,
    getBalance (setBalance sto owner amount) owner = amount. 

  Parameter getBalance_setBalance_neq : forall sto owner owner' amount,
    owner <> owner' ->
    getBalance (setBalance sto owner amount) owner' =
    getBalance sto owner'.

  Parameter getAllowance_setAllowance_eq : forall sto owner spender amount,
    getAllowance (setAllowance sto owner spender amount) owner spender =
    amount.

  Parameter getAllowance_setAllowance_neq : forall sto owner owner' spender spender' amount,
    owner <> owner' \/ spender <> spender' ->
    getAllowance (setAllowance sto owner spender amount) owner' spender' =
    getAllowance sto owner' spender'.

  Parameter getAllowance_setBalance : forall sto owner sender spender amount,
    getAllowance (setBalance sto owner amount) sender spender =
    getAllowance sto sender spender.

  Parameter getBalance_setAllowance : forall sto owner sender spender amount,
    getBalance (setAllowance sto sender spender amount) owner =
    getBalance sto owner.

  Parameter getOwners_mem : forall sto owner,
    cset_mem owner (getOwners sto) = isOwner sto owner.

End FA12Axioms.