(* Open Source License *) (* Copyright (c) 2020 Nomadic Labs. *) (* 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 String. Require Import syntax. Require error. Require parser_helpers. Require dexter_fa2_parse. (*! Parameter type !*) (*+ Extract entrypoint type by name +*) Definition is_annotation an (oan' : Datatypes.option String.string) := match oan' with | None => false | Some an' => if String.string_dec an an' then true else false end. Fixpoint get_ep_ty_by_name (ty: type) (ep : String.string) : Datatypes.list type := match ty with | (or a an1 b an2) => if is_annotation ep an1 then cons a nil else if is_annotation ep an2 then cons b nil else (get_ep_ty_by_name a ep) ++ (get_ep_ty_by_name b ep) | _ => nil end. Fixpoint get_ep_ty_by_name1 (ty: type) (ep : String.string) : Datatypes.option type := match get_ep_ty_by_name ty ep with | cons ty nil => Some ty | _ => None end. (*+ Parameter type definitions +*) Definition parameter_ty := Eval cbv in contract_file_parameter dexter_fa2_parse.dex_fa2_contract_file. Definition parameter_ep_approve_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%approve") I. Definition parameter_ep_addLiquidity_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%addLiquidity") I. Definition parameter_ep_removeLiquidity_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%removeLiquidity") I. Definition parameter_ep_xtzToToken_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%xtzToToken") I. Definition parameter_ep_tokenToXtz_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%tokenToXtz") I. Definition parameter_ep_tokenToToken_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%tokenToToken") I. Definition parameter_ep_updateTokenPool_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%updateTokenPool") I. Definition parameter_ep_updateTokenPoolInternal_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%updateTokenPoolInternal") I. Definition parameter_ep_setBaker_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%setBaker") I. Definition parameter_ep_setManager_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%setManager") I. Definition parameter_ep_default_ty := Eval cbv in get_opt (get_ep_ty_by_name1 parameter_ty "%default") I. (*! Storage type !*) Definition storage_ty : type := Eval cbv in contract_file_storage dexter_fa2_parse.dex_fa2_contract_file. Require Import semantics. Module Storage (C:ContractContext). Module semantics := Semantics C. Import semantics. (* Generated by split.py *) Definition sto_accounts (sto : data storage_ty) : data (big_map address (pair nat (map address nat))) := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => accounts end. Definition sto_selfIsUpdatingTokenPool (sto : data storage_ty) : data bool := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => selfIsUpdatingTokenPool end. Definition sto_freezeBaker (sto : data storage_ty) : data bool := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => freezeBaker end. Definition sto_lqtTotal (sto : data storage_ty) : data nat := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => lqtTotal end. Definition sto_manager (sto : data storage_ty) : data address := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => manager end. Definition sto_tokenAddress (sto : data storage_ty) : data address := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => tokenAddress end. Definition sto_tokenId (sto : data storage_ty) : data nat := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => tokenId end. Definition sto_tokenPool (sto : data storage_ty) : data nat := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => tokenPool end. Definition sto_xtzPool (sto : data storage_ty) : data mutez := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => xtzPool end. Definition sto_set_accounts (sto : data storage_ty) (accounts' : data (big_map address (pair nat (map address nat)))) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts', ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) end. Definition sto_set_selfIsUpdatingTokenPool (sto : data storage_ty) (selfIsUpdatingTokenPool' : data bool) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool', (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) end. Definition sto_set_freezeBaker (sto : data storage_ty) (freezeBaker' : data bool) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker', lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) end. Definition sto_set_lqtTotal (sto : data storage_ty) (lqtTotal' : data nat) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal')), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) end. Definition sto_set_manager (sto : data storage_ty) (manager' : data address) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager', (tokenAddress, tokenId)), (tokenPool, xtzPool)))) end. Definition sto_set_tokenAddress (sto : data storage_ty) (tokenAddress' : data address) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress', tokenId)), (tokenPool, xtzPool)))) end. Definition sto_set_tokenId (sto : data storage_ty) (tokenId' : data nat) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId')), (tokenPool, xtzPool)))) end. Definition sto_set_tokenPool (sto : data storage_ty) (tokenPool' : data nat) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool', xtzPool)))) end. Definition sto_set_xtzPool (sto : data storage_ty) (xtzPool' : data mutez) : data storage_ty := match sto with | (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool)))) => (accounts, ((selfIsUpdatingTokenPool, (freezeBaker, lqtTotal)), ((manager, (tokenAddress, tokenId)), (tokenPool, xtzPool')))) end. End Storage. (*! Contract definition !*) Definition self_type : self_info := (Some (parameter_ty, None)). Import error.Notations. Definition ep_instruction tff ep_ty : Type := typer.instruction self_type tff (ep_ty ::: storage_ty ::: nil) (pair (list operation) storage_ty ::: nil). Definition ep_from_typer_result s (ep_ty : type) : error.M (sigT (fun b => ep_instruction b ep_ty)) := parser_helpers.michelson_type_checked_M s 100 self_type (ep_ty :: storage_ty ::: nil) (pair (list operation) storage_ty ::: nil). Definition from_sig_to_error ep_ty (v : (sigT (fun b => ep_instruction b ep_ty))) : error.M (ep_instruction false ep_ty) := match v with | existT _ true code => error.Failed _ (error.Assertion_Failure _ tt) | existT _ false code => error.Return code end. Definition ep_from_string s (ep_ty : type) : error.M (ep_instruction false ep_ty) := let! v := ep_from_typer_result s ep_ty in let! v' := from_sig_to_error _ v in error.Return v'. Definition ep_approve := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_approve parameter_ep_approve_ty) I). Definition ep_addLiquidity := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_addLiquidity parameter_ep_addLiquidity_ty) I). Definition ep_removeLiquidity := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_removeLiquidity parameter_ep_removeLiquidity_ty) I). Definition ep_xtzToToken := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_xtzToToken parameter_ep_xtzToToken_ty) I). Definition ep_tokenToXtz := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_tokenToXtz parameter_ep_tokenToXtz_ty) I). Definition ep_tokenToToken := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_tokenToToken parameter_ep_tokenToToken_ty) I). Definition ep_updateTokenPool := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_updateTokenPool parameter_ep_updateTokenPool_ty) I). Definition ep_updateTokenPoolInternal := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_updateTokenPoolInternal parameter_ep_updateTokenPoolInternal_ty) I). Definition ep_setBaker := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_setBaker parameter_ep_setBaker_ty) I). Definition ep_setManager := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_setManager parameter_ep_setManager_ty) I). Definition ep_default := Eval cbv in (error.extract (ep_from_string dexter_fa2_string.ep_default parameter_ep_default_ty) I). (*! Main !*) Definition main := Eval cbv in contract_file_code dexter_fa2_parse.dex_fa2_contract_file. (*! Alternate main !*) (* This should be the same as [main], however, the contract above renders something that is too slow to work on. *) Require Import macros. Definition main2 : instruction self_type _ (pair parameter_ty storage_ty ::: nil) (pair (list operation) storage_ty ::: nil) := Instruction_seq { DUP ; CAR ; DIP1 { CDR } ; IF_LEFT { IF_LEFT { IF_LEFT { ep_approve } { ep_addLiquidity } } { IF_LEFT { ep_removeLiquidity } { IF_LEFT { ep_xtzToToken } { ep_tokenToXtz } } } } { IF_LEFT { IF_LEFT { ep_tokenToToken } { IF_LEFT { ep_updateTokenPool } { ep_updateTokenPoolInternal } } } { IF_LEFT { ep_setBaker } { IF_LEFT { ep_setManager } { ep_default } } } } }. (* TODO: This is currently not true. To fix it, entrypoints should be instruction_seq and not instruction *) (* * Lemma main_eq_main2 : main = main2. Admitted. *)