https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 904c90cfc336a0d4190fb1f04fc42377c562d97e authored by kristinas on 03 June 2021, 09:41:17 UTC
Using entrypoint trees instead of parameters.
Using entrypoint trees instead of parameters.
Tip revision: 904c90c
fa12_spec.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 NArith.
Require Import syntax.
Require Import contract_semantics.
Require Import fa12_interface.
Import List.ListNotations.
Open Scope list_scope.
Module FA12Specification (fa12 : FA12).
Module fa12Definitions := FA12Definitions fa12.
Import fa12Definitions fa12.
(** Entry point specifications *)
Section EntryPoints.
Variable (env : @proto_env self_type).
Notation sender := (sender env).
(** Entry point: ep_approve *)
Definition ep_approve
(p : data parameter_ep_approve_ty)
(sto : data storage_ty)
(ret_ops : data (list operation))
(ret_sto : data storage_ty) :=
let '(spender, new_allowance) := p in
let current_allowance := getAllowance sto sender spender in
(sender <> spender -> current_allowance = 0%N \/ new_allowance = 0%N) /\
(forall owner, getBalance ret_sto owner = getBalance sto owner) /\
(forall sender' spender', sender <> sender' \/ spender <> spender' ->
getAllowance ret_sto sender' spender' = getAllowance sto sender' spender') /\
(sender <> spender -> getAllowance ret_sto sender spender = new_allowance).
(** Entry point: ep_transfer *)
Definition ep_transfer
(p : data parameter_ep_transfer_ty)
(sto : data storage_ty)
(ret_ops : data (list operation))
(ret_sto : data storage_ty) :=
let '(from, (to, amount)) := p in
(forall owner, owner <> from /\ owner <> to ->
getBalance ret_sto owner = getBalance sto owner) /\
(from <> to -> getBalance ret_sto from + amount = getBalance sto from)%N /\
(from <> to -> getBalance ret_sto to = amount + getBalance sto to)%N /\
(from = to -> getBalance ret_sto from = getBalance sto from) /\
(forall owner spender, owner <> from \/ spender <> sender ->
getAllowance ret_sto owner spender = getAllowance sto owner spender) /\
(from <> sender -> getAllowance ret_sto from sender + amount = getAllowance sto sender from)%N.
(** Entry point: ep_getBalance *)
Definition ep_getBalance
(p : data parameter_ep_getBalance_ty)
(sto : data storage_ty)
(ret_ops : data (list operation))
(ret_sto : data storage_ty) :=
let '(owner, contr) := p in
let balance := getBalance sto owner in
let op := transfer_tokens nat I balance (amount env) contr in
ret_sto = sto /\ ret_ops = [op].
(** Entry point ep_getAllowance *)
Definition ep_getAllowance
(p : data parameter_ep_getAllowance_ty)
(sto : data storage_ty)
(ret_ops : data (list operation))
(ret_sto : data storage_ty) :=
let '((owner, spender), contr) := p in
let allowance := getAllowance sto owner spender in
let op := transfer_tokens nat I allowance (amount env) contr in
ret_sto = sto /\ ret_ops = [op].
(** Entry point: ep_getTotalSupply *)
Definition ep_getTotalSupply
(p : data parameter_ep_getTotalSupply_ty)
(sto : data storage_ty)
(ret_ops : data (list operation))
(ret_sto : data storage_ty) :=
let '(_, contr) := p in
let supply := getTotalSupply sto in
let op := transfer_tokens nat I supply (amount env) contr in
ret_sto = sto /\ ret_ops = [op].
End EntryPoints.
End FA12Specification.