https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: d7b21f4f74735ee5a48d9a8c09af765c38a30d44 authored by Guillaume Claret on 12 March 2021, 11:19:43 UTC
[mi-cho-coq] Replace String.string_dec by String.eqb
[mi-cho-coq] Replace String.string_dec by String.eqb
Tip revision: d7b21f4
dexter_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. *)
(* Coq *)
Require List.
Require Import String.
Require Import NArith.
Open Scope string_scope.
Import List.ListNotations.
Open Scope list_scope.
Require Import ZArith.
(* Mi-Cho-Coq *)
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import util.
Import error.
(* Contracts *)
Require Import contract_semantics.
(* Dexter *)
Require dexter_definition.
Definition env_ty := Eval cbv in (@proto_env dexter_definition.self_type).
(* Abstracts over an FA12 contract *)
Module fa12.
(* Entrypoint "transfer" *)
Definition ep_transfer_annot := "%transfer".
Definition ep_transfer_ty :=
(pair address (* :from *)
(pair address (* :to *) nat (* :value *))).
Definition ep_transfer := data (contract ep_transfer_ty).
Record Transfer :=
{ from : data address ;
to : data address ;
amount : data nat }.
Definition transfer
(env : env_ty)
(contract : ep_transfer)
(transfer : Transfer) :=
transfer_tokens env
ep_transfer_ty
(transfer.(from), (transfer.(to), transfer.(amount)))
(0 ~Mutez)
contract.
(* [is_ep_transfer adr contract] holds if [contract] corresponds to entrypoint %transfer
* in a fa12 token contract at [adr]
*)
Definition is_ep_transfer (env : env_ty) adr contract :=
contract_ (Some ep_transfer_annot)
ep_transfer_ty adr = Some contract.
(* Entrypoint "getBalance" *)
Definition ep_getBalance_annot := "%getBalance".
(* (view (address :owner) nat) %getBalance *)
Definition ep_getBalance_ty :=
(pair address (* :owner *)
(contract nat) (* callback *)).
Definition ep_getBalance := data (contract ep_getBalance_ty).
Definition getBalance (env : env_ty) (fa12_contract : ep_getBalance) (owner : data address) (callback : data (contract nat)) :=
transfer_tokens env
ep_getBalance_ty
(owner, callback)
(0 ~Mutez)
fa12_contract.
(* [is_ep_getBalance adr contract] holds if [contract] corresponds to entrypoint %getBalance
* in a fa12 token contract at [adr]
*)
Definition is_ep_getBalance (env : env_ty) adr contract :=
contract_ (Some ep_getBalance_annot)
ep_getBalance_ty adr = Some contract.
End fa12.
(* Abstracts over the associated FA12 LQT contract *)
Module lqt.
(* Entrypoint "mintOrBurn" *)
Definition ep_mintOrBurn_annot := "%mintOrBurn".
Definition ep_mintOrBurn_ty :=
(pair int (* %quantity *)
address (* %target *)).
Definition ep_mintOrBurn := data (contract ep_mintOrBurn_ty).
Record MintOrBurn :=
{ quantity : data int ;
target : data address }.
Definition mintOrBurn
(env : env_ty)
(contract : ep_mintOrBurn)
(mintOrBurn : MintOrBurn) :=
transfer_tokens env
ep_mintOrBurn_ty
(mintOrBurn.(quantity), mintOrBurn.(target))
(0 ~Mutez)
contract.
Record Mint :=
{ minted : data nat ;
to : data address }.
Definition mint
(env : env_ty)
(contract : ep_mintOrBurn)
(mint : Mint) :=
mintOrBurn env contract {| quantity := Z.of_N mint.(minted) ;
target := mint.(to) |}.
Record Burn :=
{ burned : data nat ;
from : data address }.
Definition burn
(env : env_ty)
(contract : ep_mintOrBurn)
(burn : Burn) :=
mintOrBurn env contract {| quantity := (0 - Z.of_N burn.(burned))%Z ;
target := burn.(from) |}.
(* [is_ep_mintOrBurn adr contract] holds if [contract] corresponds
to entrypoint %mintOrBurn at [adr] *)
Definition is_ep_mintOrBurn (env : env_ty) adr contract :=
contract_ (Some ep_mintOrBurn_annot)
ep_mintOrBurn_ty adr = Some contract.
End lqt.
(* less confusing name for pure XTZ transfers *)
Definition transfer_xtz (env : env_ty) amount to :=
transfer_tokens env unit tt amount to.
(** Helpers for comparison +*)
Section Compare.
Context { A : comparable_type }.
Definition cmp_ltb : comparable_data A -> comparable_data A -> Datatypes.bool :=
fun a b => match compare _ a b with | Lt => true | _ => false end.
Definition cmp_gtb : comparable_data A -> comparable_data A -> Datatypes.bool :=
fun a b => match compare _ a b with | Gt => true | _ => false end.
Definition cmp_eqb : comparable_data A -> comparable_data A -> Datatypes.bool :=
fun a b => match compare _ a b with | Eq => true | _ => false end.
Definition cmp_leb : comparable_data A -> comparable_data A -> Datatypes.bool :=
fun a b => match compare _ a b with | Eq | Lt => true | _ => false end.
Definition cmp_geb : comparable_data A -> comparable_data A -> Datatypes.bool :=
fun a b => match compare _ a b with | Eq | Gt => true | _ => false end.
Definition cmp_neqb : comparable_data A -> comparable_data A -> Datatypes.bool :=
fun a b => match compare _ a b with | Eq => false | _ => true end.
End Compare.
(** Getters/setters for the storage type *)
Import dexter_definition.Storage.
(*+ Entry point specifications +*)
(* Assumption: all entrypoints consume one their stack a value of
its parameter (specific to the entrypoint) and the storage and
produces a list of operations and an updated storage. *)
(*! Entry point: ep_addLiquidity !*)
Section entrypoints.
Variable (env : env_ty).
Definition env_sender := sender env.
Definition env_source := source env.
Definition env_self_address'
: forall (annot_opt : annot_o)
(H : isSome (get_entrypoint_opt annot_opt dexter_definition.parameter_ty None)),
data (contract (get_opt (get_entrypoint_opt annot_opt dexter_definition.parameter_ty None) H))
:= fun annot_opt H => (self env annot_opt H).
Definition env_self_address_ep_default : data address :=
address_ dexter_definition.parameter_ep_default_ty (env_self_address' None I).
Definition env_self_address_ep_updateTokenPoolInternal : data address :=
address_ dexter_definition.parameter_ep_updateTokenPoolInternal_ty
(env_self_address' (Some "%updateTokenPoolInternal") I).
(** Working with mutez *)
Definition mutez_to_nat (m : data mutez) : data nat := Z.to_N (tez.to_Z m).
(** Contract-specific Specification helpers *)
(* A check_deadline fails if the deadline is passed or exactly now *)
Definition check_deadline (deadline : data timestamp) : Prop :=
cmp_ltb (now env) deadline.
Definition mutez_add (a b sum : data mutez) : Prop :=
add _ _ _ Add_variant_tez_tez a b = Return sum.
Definition mutez_sub (a b diff : data mutez) : Prop :=
sub _ _ _ Sub_variant_tez_tez a b = Return diff.
Definition Nceiling (a b : N) : N :=
match N.div_eucl a b with
| (q, 0%N) => q
| (q, r) => q + 1%N
end.
Definition ep_addLiquidity
(p : data dexter_definition.parameter_ep_addLiquidity_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
let '(owner, (min_lqt_minted, (max_tokens_deposited, deadline))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
sto_xtzPool sto <> (0 ~Mutez) /\
let amount_nat := mutez_to_nat (amount env) in
let token_adr := sto_tokenAddress sto in
let lqt_adr := sto_lqtAddress sto in
exists token_contract_ep_transfer lqt_contract_ep_mintOrBurn xtz_pool',
fa12.is_ep_transfer env token_adr token_contract_ep_transfer /\
lqt.is_ep_mintOrBurn env lqt_adr lqt_contract_ep_mintOrBurn /\
mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\
let lqt_created := ((sto_lqtTotal sto * amount_nat) / (mutez_to_nat (sto_xtzPool sto)))%N in
let token_deposited :=
Nceiling (sto_tokenPool sto * amount_nat)
(mutez_to_nat (sto_xtzPool sto)) in
(min_lqt_minted <= lqt_created)%N /\
(token_deposited <= max_tokens_deposited)%N /\
let sto := sto_set_lqtTotal sto (sto_lqtTotal sto + lqt_created)%N in
let sto := sto_set_tokenPool sto (sto_tokenPool sto + token_deposited)%N in
let sto := sto_set_xtzPool sto xtz_pool' in
ret_sto = sto /\
ret_ops = [
fa12.transfer env token_contract_ep_transfer
{| fa12.from := env_sender;
fa12.to := env_self_address_ep_default;
fa12.amount := token_deposited |};
lqt.mint env lqt_contract_ep_mintOrBurn
{| lqt.minted := lqt_created ;
lqt.to := owner |}
].
(*! Entry point: default !*)
Definition ep_default
(p : data dexter_definition.parameter_ep_default_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
~ sto_selfIsUpdatingTokenPool sto /\
exists xtz_pool',
mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\
let sto := sto_set_xtzPool sto xtz_pool' %N in
ret_sto = sto /\ ret_ops = nil.
(*! Entry point: removeLiquidity !*)
Definition nat_to_mutez (n : data nat) : (M (data mutez)) := tez.of_Z (Z.of_N n).
Definition ep_removeLiquidity
(p : data dexter_definition.parameter_ep_removeLiquidity_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
let '(to, (lqt_burned, (min_xtz_withdrawn, (min_tokens_withdrawn, deadline)))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
check_deadline deadline /\
(lqt_burned <= sto_lqtTotal sto)%N /\
(sto_lqtTotal sto <> 0)%N /\
let xtz_withdrawn := (((mutez_to_nat (sto_xtzPool sto)) * lqt_burned )
/ sto_lqtTotal sto)%N in
(xtz_withdrawn >= mutez_to_nat min_xtz_withdrawn)%N /\
match nat_to_mutez xtz_withdrawn with
| Failed _ _ =>
False
| Return xtz_withdrawn_mutez =>
let tokens_withdrawn := ((sto_tokenPool sto * lqt_burned) / sto_lqtTotal sto)%N in
(tokens_withdrawn >= min_tokens_withdrawn)%N /\
(tokens_withdrawn <= sto_tokenPool sto)%N /\
exists xtz_pool',
mutez_sub (sto_xtzPool sto) xtz_withdrawn_mutez xtz_pool' /\
(* check that the receiver account [to] exists with type unit *)
match contract_ None unit to with
(* to contract does not exist *)
| None => False
| Some to_contract =>
(* verify that the token contract exists with the appropriate type at the
* transfer entrypoint *)
exists token_contract_ep_transfer lqt_contract_ep_mintOrBurn,
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
lqt.is_ep_mintOrBurn env (sto_lqtAddress sto) lqt_contract_ep_mintOrBurn /\
let sto := sto_set_xtzPool sto xtz_pool' in
let sto := sto_set_tokenPool sto (sto_tokenPool sto - tokens_withdrawn)%N in
let sto := sto_set_lqtTotal sto (sto_lqtTotal sto - lqt_burned)%N in
ret_sto = sto /\
ret_ops = [
lqt.burn env lqt_contract_ep_mintOrBurn
{| lqt.burned := lqt_burned ;
lqt.from := env_sender |};
fa12.transfer env token_contract_ep_transfer
{| fa12.from := env_self_address_ep_default;
fa12.to := to;
fa12.amount := tokens_withdrawn |};
transfer_xtz env xtz_withdrawn_mutez to_contract
]
end
end.
(*! Entry point: setBaker !*)
Definition ep_setBaker
(p : data dexter_definition.parameter_ep_setBaker_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
let (new_baker, freeze_baker) := p in
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
env_sender = sto_manager sto /\
~ sto_freezeBaker sto /\
ret_ops = [set_delegate env new_baker] /\
ret_sto = sto_set_freezeBaker sto freeze_baker.
(*! Entry point: tokenToXtz !*)
(* [get_amount_bought input_amount input_pool output_pool] calculates the
* conversion of [input_amount] from [input_pool] to [output_pool]
* with a withheld fee of 0.003%.
*
* When called thus:
* get_amount_bought input_amount (get_token_pool sto) (mutez_to_nat (sto_xtzPool sto))
* it calculates the number of tez tokens obtained when selling [input_amount] fa12 tokens.
*
* When called thus:
* get_amount_bought input_amount (mutez_to_nat (sto_xtzPool sto)) (get_token_pool sto)
* it calculates the number of fa12 tokens obtained when selling [input_amount] tez tokens.
*
*)
Definition get_amount_bought
(input_amount : N)
(input_pool : N)
(output_pool : N) : Datatypes.option N :=
let divisor := (input_pool * 1000 + (input_amount * 997))%N in
if N.eq_dec divisor 0 then
None
else
Some ((input_amount * 997 * output_pool) / divisor)%N.
(* Example: floor(100 * 997 * 100000 / (100000 * 1000 + amount * 997)) = floor(99.6) = 99 *)
Example get_amount_bought_ex1 : (get_amount_bought 100 100000 100000) = Some 99%N.
Proof. reflexivity. Qed.
Definition ep_tokenToXtz
(p : data dexter_definition.parameter_ep_tokenToXtz_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
let '(to, (tokens_sold, (min_xtz_bought, deadline))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
amount env = (0 ~Mutez) /\
match
get_amount_bought tokens_sold
(sto_tokenPool sto)
(mutez_to_nat (sto_xtzPool sto))
with
| None => False
| Some xtz_bought =>
match nat_to_mutez xtz_bought with
| Return xtz_bought_mutez =>
cmp_leb min_xtz_bought xtz_bought_mutez /\
match contract_ None unit to with
(* to contract does not exist *)
| None => False
| Some to_contract =>
exists token_contract_ep_transfer xtz_pool',
mutez_sub (sto_xtzPool sto) xtz_bought_mutez xtz_pool' /\
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
let sto := sto_set_tokenPool sto (sto_tokenPool sto + tokens_sold)%N in
let sto := sto_set_xtzPool sto xtz_pool' %N in
ret_sto = sto /\
ret_ops = [
fa12.transfer env token_contract_ep_transfer
{| fa12.from := env_sender;
fa12.to := env_self_address_ep_default;
fa12.amount := tokens_sold |};
transfer_xtz env xtz_bought_mutez to_contract
]
end
| Failed _ _ => False
end
end.
(*! Entry point: updateTokenPool !*)
Definition ep_updateTokenPool
(param : data dexter_definition.parameter_ep_updateTokenPool_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
exists token_contract_ep_getBalance,
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
env_sender = env_source /\
fa12.is_ep_getBalance env (sto_tokenAddress sto) token_contract_ep_getBalance /\
ret_ops = [
fa12.getBalance
env
token_contract_ep_getBalance
env_self_address_ep_default (* owner *)
(env_self_address' (Some "%updateTokenPoolInternal") I) (* callback *)
] /\
ret_sto = sto_set_selfIsUpdatingTokenPool sto true.
(*! Entry point: updateTokenPoolInternal !*)
Definition ep_updateTokenPoolInternal
(token_pool : data dexter_definition.parameter_ep_updateTokenPoolInternal_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
amount env = (0 ~Mutez) /\
env_sender = sto_tokenAddress sto /\
sto_selfIsUpdatingTokenPool sto /\
ret_ops = [] /\
ret_sto = (sto_set_selfIsUpdatingTokenPool (sto_set_tokenPool sto token_pool) false).
(*! Entry point: xtzToToken !*)
Definition ep_xtzToToken
(p : data dexter_definition.parameter_ep_xtzToToken_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
let '(to, (min_tokens_bought, deadline)) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
match
get_amount_bought (mutez_to_nat (amount env))
(mutez_to_nat (sto_xtzPool sto))
(sto_tokenPool sto)
with
| None =>
False
| Some tokens_bought =>
(*
==
((amount * 997 * (sto_tokenPool sto))
/ ((mutez_to_nat (sto_xtzPool sto)) * 1000 + (amount * 997)))
*)
(tokens_bought >= min_tokens_bought)%N /\
(tokens_bought <= sto_tokenPool sto )%N /\
exists xtz_pool' token_contract_ep_transfer,
mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
let sto := sto_set_tokenPool sto (sto_tokenPool sto - tokens_bought)%N in
let sto := sto_set_xtzPool sto xtz_pool' %N in
ret_sto = sto /\
ret_ops = [
fa12.transfer env token_contract_ep_transfer
{| fa12.from := env_self_address_ep_default;
fa12.to := to;
fa12.amount := tokens_bought |}
]
end.
(*! Entry point: tokenToToken !*)
Definition ep_tokenToToken
(p : data dexter_definition.parameter_ep_tokenToToken_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
let '(output_dexter_address, (min_tokens_bought, (to, (tokens_sold, deadline)))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
amount env = (0 ~Mutez) /\
match
get_amount_bought tokens_sold
(sto_tokenPool sto)
(mutez_to_nat (sto_xtzPool sto))
with
| None => False
| Some xtz_bought =>
match nat_to_mutez xtz_bought with
| Return xtz_bought_mutez =>
exists token_contract_ep_transfer xtz_pool',
match contract_ (Some "%xtzToToken")
dexter_definition.parameter_ep_xtzToToken_ty
output_dexter_address
with
| Some output_dexter_ep_xtzToToken_contract =>
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
mutez_sub (sto_xtzPool sto) xtz_bought_mutez xtz_pool' /\
let sto := sto_set_tokenPool sto (sto_tokenPool sto + tokens_sold)%N in
let sto := sto_set_xtzPool sto xtz_pool' %N in
ret_sto = sto /\
ret_ops = [
fa12.transfer env
token_contract_ep_transfer
{| fa12.from := env_sender;
fa12.to := env_self_address_ep_default;
fa12.amount := tokens_sold |};
transfer_tokens env
dexter_definition.parameter_ep_xtzToToken_ty
(to, (min_tokens_bought, deadline))
xtz_bought_mutez
output_dexter_ep_xtzToToken_contract]
| None => False
end
| Failed _ _ => False
end
end.
(*! Entry point: setManager !*)
Definition ep_setManager
(new_manager : data dexter_definition.parameter_ep_setManager_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
env_sender = sto_manager sto /\
ret_ops = [] /\
ret_sto = sto_set_manager sto new_manager.
(*! Entry point: setLqtAddress !*)
(* The initial value of lqtAddress is only changeable by the manager
when set to the zeroth tz1 address, which is
tz1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU
If changed from this address, it can no longer be changed. *)
Definition tz1Zero := (Implicit (Mk_key_hash "1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU")).
Definition ep_setLqtAddress
(new_lqtAddress : data dexter_definition.parameter_ep_setLqtAddress_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
env_sender = sto_manager sto /\
sto_lqtAddress sto = tz1Zero /\
ret_ops = [] /\
ret_sto = sto_set_lqtAddress sto new_lqtAddress.
End entrypoints.
(*! Full spec !*)
Definition main
(env : env_ty)
(p : data dexter_definition.parameter_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
match p with
| (inl (inl (inl (inl p)))) => ep_addLiquidity env p sto ret_ops ret_sto
| (inl (inl (inl (inr p)))) => ep_default env p sto ret_ops ret_sto
| (inl (inl (inr (inl p)))) => ep_removeLiquidity env p sto ret_ops ret_sto
| (inl (inl (inr (inr p)))) => ep_setBaker env p sto ret_ops ret_sto
| (inl (inr (inl (inl p)))) => ep_setLqtAddress env p sto ret_ops ret_sto
| (inl (inr (inl (inr p)))) => ep_setManager env p sto ret_ops ret_sto
| (inl (inr (inr (inl p)))) => ep_tokenToToken env p sto ret_ops ret_sto
| (inl (inr (inr (inr p)))) => ep_tokenToXtz env p sto ret_ops ret_sto
| (inr (inl (inl p))) => ep_updateTokenPool env p sto ret_ops ret_sto
| (inr (inl (inr p))) => ep_updateTokenPoolInternal env p sto ret_ops ret_sto
| (inr (inr p)) => ep_xtzToToken env p sto ret_ops ret_sto
end.
