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_camlcase.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 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_camlcase_string.
(** FA1.2 types implementation *)
Module fa12TypesImpl.
Definition parameter_ty : type :=
or (or parameter_ep_approve_ty (Some annot.approve)
parameter_ep_transfer_ty (Some annot.transfer)) 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.
Definition storage_ty : type :=
pair (big_map address (pair nat (map address nat))) 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 q) => Some (inl (inr q))
| inl (inr q) => Some (inl (inl q))
| inr q => Some (inr q)
end.
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) : set.set (data address) (compare address).
Proof.
destruct sto as [ledger supply]; 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).
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 (inl (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 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 (inr (inl 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 (inr (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 (inr (inr (inr q))); auto.
Qed.
Opaque map.empty.
Opaque map.update.
Opaque compare.
Lemma getBalance_setBalance_eq sto owner amount :
getBalance (setBalance sto owner amount) owner = amount.
Proof.
destruct sto as [ledger supply]; cbn.
destruct map.get as [[balance allowances] | ]; cbn.
all: rewrite map.map_updateeq; 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.
Lemma getAllowance_setAllowance_eq sto owner spender amount :
getAllowance (setAllowance sto owner spender amount) owner spender = amount.
Proof.
destruct sto as [ledger supply]; cbn.
destruct map.get as [[balance allowances] | ]; cbn.
all: rewrite !map.map_updateeq; 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 supply]; cbn.
all: destruct (compare_equal owner owner') eqn:eq.
all: rewrite ?eqb_eq, ?eqb_neq in eq; subst.
all: destruct map.get as [[balance allowances] | ]; cbn.
all: try rewrite map.map_updateeq.
all: rewrite map.map_updateneq; auto.
all: 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 supply]; cbn.
all: destruct (compare_equal owner sender) eqn:eq.
all: rewrite ?eqb_eq, ?eqb_neq in eq; subst.
all: destruct map.get as [[balance allowances] | ]; cbn.
all: try rewrite map.map_updateeq; auto.
all: rewrite map.map_updateneq; 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 supply]; cbn.
all: destruct (compare_equal owner sender) eqn:eq.
all: rewrite ?eqb_eq, ?eqb_neq in eq; subst.
all: destruct map.get as [[balance allowances] | ]; cbn.
all: try rewrite map.map_updateeq; auto.
all: try rewrite map.map_updateneq; auto.
Qed.
Lemma getOwners_mem sto owner :
cset_mem owner (getOwners sto) = isOwner sto owner.
Proof.
destruct sto as [ledger 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: intros [balance allowances].
+ 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_camlcase_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).

Computing file changes ...