https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 01bc61c108297c690802d90a12ab124d16bbc048 authored by Arvid Jakobsson on 28 September 2020, 11:58:34 UTC
Merge branch 'fa12-verification' into 'dev'
Merge branch 'fa12-verification' into 'dev'
Tip revision: 01bc61c
fa12_camlcase_spec.v
(* Open Source License *)
(* Copyright (c) 2019 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 fa12_context.
Import List.ListNotations.
Open Scope list_scope.
Module FA12CamlCaseSpec (C : ContractContext) (FT : FA12ContextTypes) (FD : FA12ContextData C FT).
Import FT.
Import FD.
Import semantics.
(** 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
ret_ops = nil /\
if (address_equal sender spender)
then ret_sto = sto
else let current_allowance := getAllowance sto sender spender in
(current_allowance = 0%N \/ new_allowance = 0%N) /\
ret_sto = setAllowance 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
ret_ops = nil /\
if (address_equal from to)
then ret_sto = sto
else isOwner sto from /\ exists from_balance',
let from_balance := getBalance sto from in
let to_balance := getBalance sto to in
let sto' := setBalance sto from from_balance' in
let sto'' := setBalance sto' to (to_balance + amount)%N in
from_balance = (from_balance' + amount)%N /\
if (address_equal sender from)
then ret_sto = sto''
else isSpender sto from sender /\ exists current_allowance',
let current_allowance := getAllowance sto from sender in
current_allowance = (current_allowance' + amount)%N /\
ret_sto = setAllowance sto'' from sender current_allowance'.
(** 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 sum := List.fold_right (fun owner sum => (getBalance sto owner + sum)%N) 0%N (getOwners sto) in
let op := transfer_tokens env nat supply (0 ~Mutez) contr in
supply = sum /\ ret_sto = sto /\ ret_ops = [op].
(** 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 op := transfer_tokens env nat (getBalance sto owner) (0 ~Mutez) contr in
isOwner sto owner /\ ret_sto = sto /\ ret_ops = [op].
(** Entry point success: 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 op := transfer_tokens env nat (getAllowance sto owner spender) (0 ~Mutez) contr in
isOwner sto owner /\ isSpender sto owner spender /\
ret_sto = sto /\ ret_ops = [op].
End EntryPoints.
(** Full spec *)
Definition main
(env : @proto_env self_type)
(p : data fa12_parameter_ty)
(sto : data storage_ty)
(ret_ops : data (list operation))
(ret_sto : data storage_ty) :=
match p with
| (inl (inl p)) => ep_transfer env p sto ret_ops ret_sto
| (inl (inr p)) => ep_approve env p sto ret_ops ret_sto
| (inr (inl p)) => ep_getAllowance env p sto ret_ops ret_sto
| (inr (inr (inl p))) => ep_getBalance env p sto ret_ops ret_sto
| (inr (inr (inr p))) => ep_getTotalSupply env p sto ret_ops ret_sto
end.
End FA12CamlCaseSpec.