(* 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 contract_semantics.
Require Import entrypoints.
Require Import error.
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_approve_ty parameter_ep_transfer_ty)
        (or (or parameter_ep_getBalance_ty parameter_ep_getAllowance_ty)
            parameter_ep_getTotalSupply_ty).

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

  Parameter parameter_ty : entrypoint_tree.
  Parameter storage_ty : type.

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

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

  Parameter getOwners_mem : forall sto owner,
    getBalanceOpt sto owner = None <->
    cset_mem owner (getOwners sto) = false.

End FA12.

Module FA12Definitions (fa12 : FA12).

  Import fa12.

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

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

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

  Notation isOwner sto owner :=
    (isSome (getBalanceOpt sto owner)).

  Notation isSpender sto owner spender :=
    (isSome (getAllowanceOpt sto owner spender)).

  Notation positive sto :=
    (fun owner => negb (getBalance sto owner =? 0))%N.

  Notation getPositiveOwners sto :=
    (cset_subset (getOwners sto)%N (positive sto)).

  Lemma getPositiveOwners_mem sto owner :
    cset_mem owner (getPositiveOwners sto) <->
    positive sto owner = true.
  Proof.
    rewrite !(cset_mem_subset address).
    destruct cset_mem eqn:eq.
    2: unfold getBalance; rewrite <-getOwners_mem in eq; rewrite eq.
    all: cbn; intuition.
  Qed.

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

  Notation storageValid sto :=
    (getTotalSupply sto = sumOfAllBalances sto).

End FA12Definitions.