(* 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 main.
Require Import util.
Require Import utils.
Require Import fa12_interface.
Require fa12_dexter_string.

Module annot.

  Import String.

  Notation mintOrBurn := "%mintOrBurn".

End annot.

(** Parameter type definitions. *)
Definition parameter_ep_mintOrBurn_ty
  := pair int address.

(** FA1.2 types implementation *)
Module fa12TypesImpl.

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

  Definition ledger_ty : type := big_map address nat.

  Definition allowances_ty : type := big_map (Cpair address address) nat.

  Definition storage_ty : type :=
    pair ledger_ty (pair allowances_ty (pair address nat)).

End fa12TypesImpl.

(** FA1.2 data implementation *)
Module FA12DataImpl (C : ContractContext).

  Module semantics := Semantics C.
  Import semantics.

  Import fa12TypesImpl.

  Definition extract_fa12_ep (p : data parameter_ty) : data (option fa12_parameter_ty) :=
    match p with
      | inl (inl (inl q)) => Some (inl (inr q))
      | inl (inl (inr q)) => Some (inr (inl q))
      | inl (inr (inl q)) => Some (inr (inr (inl q)))
      | inl (inr (inr q)) => Some (inr (inr (inr q)))
      | inr (inl _) => None
      | inr (inr q) => Some (inl (inl q))
    end.

  Definition getBalanceOpt (sto : data storage_ty) (owner : data address) : data (option nat) :=
    let '(ledger, _) := sto
    in cmap_get address owner ledger.

  Definition setBalance (sto : data storage_ty) (owner : data address) (balance' : data nat) : data storage_ty :=
    let '(ledger, (allowances, (admin, supply))) := sto in
    let balanceOpt := if (compare_equal balance' 0%N) then None else (Some balance') in
    let ledger' := cmap_update address owner balanceOpt ledger in
    (ledger', (allowances, (admin, supply))).

  Definition getAllowanceOpt (sto : data storage_ty) (owner spender : data address) : data (option nat) :=
    let '(_, (allowances, _)) := sto in
    cmap_get (Cpair address address) (owner, spender) allowances.

  Definition setAllowance (sto : data storage_ty) (owner spender : data address) (allowance' : data nat) : data storage_ty :=
    let '(ledger, (allowances, (admin, supply))) := sto in
    let allowanceOpt := if (compare_equal allowance' 0%N) then None else (Some allowance') in
    let allowances' := cmap_update (Cpair address address) (owner, spender) allowanceOpt allowances in
    (ledger, (allowances', (admin, supply))).

  Definition getAdmin (sto : data storage_ty) : data address :=
    let '(_, (_, (admin, _))) := sto in admin.

  Definition getTotalSupply (sto : data storage_ty) : data nat :=
    let '(_, (_, (_, supply))) := sto in supply.

  Definition setTotalSupply (sto : data storage_ty) (supply' : data nat) : data storage_ty :=
    let '(ledger, (allowances, (admin, _))) := sto in
    (ledger, (allowances, (admin, supply'))).

  Definition getOwners (sto : data storage_ty) : set.set (data address) (compare address).
  Proof.
    destruct sto as [ledger _]; cbn.
    exists (List.map fst (map.to_list _ _ _ ledger)).
    apply Sorted.Sorted_StronglySorted.
    1: exact (lt_trans address).
    destruct ledger as [ | k v l]; cbn.
    - auto.
    - induction l as [ | k k' v' H_k_k' l IHl]; cbn.
      all: constructor; auto.
  Defined.

End FA12DataImpl.

Module FA12AxiomsImpl (C : ContractContext).

  Import fa12TypesImpl.

  Module fa12DataImpl := FA12DataImpl C.
  Import fa12DataImpl.

  Import semantics.

  Module fa12Notations := FA12Notations C fa12TypesImpl fa12DataImpl.
  Import fa12Notations.

  Lemma ep_transfer_required (q : data parameter_ep_transfer_ty) :
    exists p, extract_fa12_ep p = Some (inl (inl q)).
  Proof.
    split with (inr (inr q)); auto.
  Qed.

  Lemma ep_approve_required (q : data parameter_ep_approve_ty) :
    exists p, extract_fa12_ep p = Some (inl (inr q)).
  Proof.
    split with (inl (inl (inl q))); auto.
  Qed.

  Lemma ep_getAllowance_required (q : data parameter_ep_getAllowance_ty) :
    exists p, extract_fa12_ep p = Some (inr (inl q)).
  Proof.
    split with (inl (inl (inr q))); auto.
  Qed.

  Lemma ep_getBalance_required (q : data parameter_ep_getBalance_ty) :
    exists p, extract_fa12_ep p = Some (inr (inr (inl q))).
  Proof.
    split with (inl (inr (inl q))); auto.
  Qed.

  Lemma ep_getTotalSupply_required (q : data parameter_ep_getTotalSupply_ty) :
    exists p, extract_fa12_ep p = Some (inr (inr (inr q))).
  Proof.
    split with (inl (inr (inr q))); auto.
  Qed.

  Opaque compare.

  Lemma getBalance_setBalance_eq sto owner amount :
    getBalance (setBalance sto owner amount) owner = amount.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z eqn:eq.
    all: rewrite map_get_update_eq; auto.
    rewrite eqb_eq in eq; subst; auto.
  Qed.

  Lemma getBalance_setBalance_neq sto owner owner' amount :
    owner <> owner' ->
    getBalance (setBalance sto owner amount) owner' =
    getBalance sto owner'.
  Proof.
    intro H.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z.
    all: rewrite map_get_update_neq; auto.
  Qed.

  Lemma getAllowance_setAllowance_eq sto owner spender amount :
    getAllowance (setAllowance sto owner spender amount) owner spender = amount.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z eqn:eq.
    all: rewrite map_get_update_eq; auto.
    rewrite eqb_eq in eq; subst; auto.
  Qed.

  Lemma getAllowance_setAllowance_neq sto owner owner' spender spender' amount :
    owner <> owner' \/ spender <> spender' ->
    getAllowance (setAllowance sto owner spender amount) owner' spender' =
    getAllowance sto owner' spender'.
  Proof.
    intro H.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct (_ =? _)%Z.
    all: rewrite map_get_update_neq; auto.
    all: intro H'; injection H'; intuition.
  Qed.

  Lemma getAllowance_setBalance sto owner sender spender amount :
    getAllowance (setBalance sto owner amount) sender spender =
    getAllowance sto sender spender.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn; auto.
  Qed.

  Lemma getBalance_setAllowance sto owner sender spender amount :
    getBalance (setAllowance sto sender spender amount) owner =
    getBalance sto owner.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn; auto.
  Qed.

  Lemma getOwners_mem sto owner :
    cset_mem owner (getOwners sto) = isOwner sto owner.
  Proof.
    destruct sto as [ledger [allowance [admin supply]]]; cbn.
    destruct ledger as [ | k v ledger]; cbn.
    - auto.
    - revert v.
      induction ledger as [ | k k' v' H_k_k' l IHl]; cbn.
      all: intro v.
      + destruct compare; auto.
      + destruct compare eqn:H_owner_k at 1 3; cbn.
        all: auto; apply IHl.
  Qed.

End FA12AxiomsImpl.

Import fa12TypesImpl.

Module self := Self fa12TypesImpl.
Import self.

Definition contract
  := Eval cbv in extract (contract_file_M fa12_dexter_string.contract 500) I.

Definition main :
  instruction self_type false
              (pair parameter_ty storage_ty ::: nil)
              (pair (list operation) storage_ty ::: nil) :=
  Instruction_seq (contract_file_code contract).