(* 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 Sorted.
Require Import syntax.
Require Import entrypoints.
Require Import contract_semantics.
Require Import comparable.
Require Import error.
Require Import main.
Require Import utils.
Require Import fa12_interface.
Require fa12_camlcase_string.

Opaque compare.

(** FA1.2 implementation *)
Module fa12CamlCase <: FA12.

  Definition parameter_ty : entrypoint_tree :=
    ep_node (ep_node (ep_leaf parameter_ep_approve_ty) (Some annot.approve)
                     (ep_leaf parameter_ep_transfer_ty) (Some annot.transfer)) None
            (ep_node (ep_leaf parameter_ep_getAllowance_ty) (Some annot.getAllowance)
                     (ep_node (ep_leaf parameter_ep_getBalance_ty) (Some annot.getBalance)
                              (ep_leaf parameter_ep_getTotalSupply_ty) (Some annot.getTotalSupply)) None) None.

  Definition storage_ty : type :=
    pair (big_map address (pair nat (map address nat))) nat.

  Definition getBalanceOpt (sto : data storage_ty) (owner : data address) : data (option nat) :=
    let (ledger, _) := sto in
    match cmap_get address owner ledger with
      | None => None
      | Some (balance, _) => Some balance
    end.

  Definition setBalance (sto : data storage_ty) (owner : data address) (balance' : data nat) : data storage_ty :=
    let '(ledger, supply) := sto in
    let (balance, allowances) := cmap_get_def address owner (0%N, cmap_empty address) ledger in
    let ledger' := cmap_update address owner (Some (balance', allowances)) ledger in
    (ledger', supply).

  Definition getAllowanceOpt (sto : data storage_ty) (owner spender : data address) : data (option nat) :=
    let (ledger, _) := sto in
    match cmap_get address owner ledger with
      | None => None
      | Some (_, allowances) => cmap_get address spender allowances
    end.

  Definition setAllowance (sto : data storage_ty) (owner spender : data address) (allowance' : data nat) : data storage_ty :=
    let (ledger, supply) := sto in
    let (balance, allowances) := cmap_get_def address owner (0%N, cmap_empty address) ledger in
    let allowances' := cmap_update address spender (Some allowance') allowances in
    let ledger' := cmap_update address owner (Some (balance, allowances')) ledger in
    (ledger', supply).

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

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

  Lemma getOwners_mem sto owner :
    getBalanceOpt sto owner = None <->
    cset_mem owner (getOwners sto) = false.
  Proof.
    destruct sto as [ledger supply]; cbn.
    destruct ledger as [ | owner' [balance' allowances'] l]; cbn.
    1: intuition.
    revert balance' allowances'.
    induction l as [owner' | owner' owner'' [balance'' allowances''] H_owner'_owner'' l IHl]; cbn.
    all: intros balance' allowances'.
    all: destruct (compare _ owner owner') eqn:H_owner_owner'.
    6: apply IHl.
    all: intuition; discriminate.
  Qed.

End fa12CamlCase. (**

Import fa12CamlCase.

Lemma getTotalSupply_setBalance (sto : data storage_ty) (owner : data address) (balance' : data nat) :
  getTotalSupply (setBalance sto owner balance') =
    getTotalSupply sto.
Proof.
  destruct sto as [ledger supply]; cbn.
  destruct map.get as [[balance allowances] | ].
  all: auto.
Qed.

  Lemma getTotalSupply_setAllowance (sto : data storage_ty) (owner spender : data address) (allowance' : data nat) :
    getTotalSupply (setAllowance sto owner spender allowance') =
    getTotalSupply sto.
  Proof.
    destruct sto as [ledger supply]; cbn.
    destruct map.get as [[balance allowances] | ].
    all: 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 supply]; cbn.
    destruct map.get as [[balance allowances] | ]; cbn.
    all: rewrite map.map_updateneq; auto.
  Qed. *)








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