https://gitlab.com/nomadic-labs/mi-cho-coq
Revision d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC, committed by kristinas on 11 May 2021, 09:41:59 UTC
1 parent f70493e
Tip revision: d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC
Added README
Added README
Tip revision: d116674
fa12_interface.v
(* 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.

Computing file changes ...