https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 10366a22de97e7dbababf7ca5acb9fd648bd9b70 authored by Arvid Jakobsson on 30 April 2021, 10:24:31 UTC
Merge branch 'cpmm2-verification--xtzToToken' into 'arvid@cpmm2-verification'
Merge branch 'cpmm2-verification--xtzToToken' into 'arvid@cpmm2-verification'
Tip revision: 10366a2
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.
Require Import dexter_storage.
Notation "'let!' x ':=' X 'in' Y" :=
(match X with Return x => Y | Failed _ _ => Logic.False end)
(at level 200, x pattern, X at level 100, Y at level 200).
Notation "'let?' x ':=' X 'in' Y" :=
(match X with Some x => Y | None => Logic.False end)
(at level 200, x pattern, X at level 100, Y at level 200).
Definition transaction_fee := 999%N.
Definition null_address : (data address) := (Implicit (Mk_key_hash "1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU")).
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.
(*+ Global invariants. +*)
Definition invariant sto :=
(sto_tokenPool sto > 0)%N.
(*+ 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 _ _ =>
Logic.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 => Logic.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 !*)
Definition N_div_opt (a divisor : N) : Datatypes.option N :=
if N.eq_dec divisor 0 then
None
else
Some (a / divisor)%N.
(* [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 * N) :=
let divisor := (input_pool * 1000 + (input_amount * transaction_fee))%N in
semantics.ediv_N (input_amount * transaction_fee * output_pool) divisor.
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) /\
let? (xtz_bought, _) :=
get_amount_bought tokens_sold (sto_tokenPool sto) (mutez_to_nat (sto_xtzPool sto))
in
let! xtz_bought_mutez := nat_to_mutez xtz_bought in
let xtz_tmp := (xtz_bought * 999)%N in
let! xtz_tmp_mutez := nat_to_mutez xtz_tmp in
let? (xtz_bought_net_burn, tmp_mod) := semantics.ediv_N xtz_tmp 1000%N in
let! xtz_bought_net_burn_mutez := nat_to_mutez xtz_bought_net_burn in
let! tmp_mod_mutez := nat_to_mutez tmp_mod in
cmp_leb min_xtz_bought xtz_bought_net_burn_mutez /\
let? to_contract := contract_ None unit to in
let! xtz_pool' := sub _ _ _ Sub_variant_tez_tez (sto_xtzPool sto) xtz_bought_net_burn_mutez in
exists token_contract_ep_transfer,
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
/\
let? null_contract := contract_ None unit null_address in
let! burn_amount_tez := sub _ _ _ Sub_variant_tez_tez xtz_bought_mutez xtz_bought_net_burn_mutez in
let op_burn := transfer_xtz env burn_amount_tez null_contract in
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_net_burn_mutez to_contract;
op_burn
].
(*
* (*! 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 /\
let xtzPool := mutez_to_nat (sto_xtzPool sto) in
let nat_amount := mutez_to_nat (amount env) in
let amount_net_burn := ((nat_amount * 999) / 1000)%N in
let! burn_amount_tmp := sub _ _ _ Sub_variant_nat_nat nat_amount amount_net_burn in
let burn_amount := Z.abs_N burn_amount_tmp in
let? (tokens_bought, _) :=
get_amount_bought amount_net_burn
(mutez_to_nat (sto_xtzPool sto))
(sto_tokenPool sto)
in
(tokens_bought >= min_tokens_bought)%N /\
let! new_token_pool_tmp := sub _ _ _ Sub_variant_nat_nat (sto_tokenPool sto) tokens_bought in
if negb (new_token_pool_tmp >=? 0)%Z then
Logic.False
else
let new_token_pool := Z.to_N new_token_pool_tmp in
let! amount_net_burn_mutez := nat_to_mutez amount_net_burn in
let! xtzPool' := add _ _ _ Add_variant_tez_tez (sto_xtzPool sto) amount_net_burn_mutez in
let sto := sto_set_xtzPool sto xtzPool' in
let sto := sto_set_tokenPool sto new_token_pool in
let? null_contract := contract_ None unit null_address in
let! burn_amount_tez := nat_to_mutez burn_amount in
let op_burn := transfer_xtz env burn_amount_tez null_contract in
ret_sto = sto /\
exists token_contract_ep_transfer,
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer
/\
ret_ops = [
fa12.transfer env token_contract_ep_transfer
{| fa12.from := env_self_address_ep_default;
fa12.to := to;
fa12.amount := tokens_bought |};
op_burn
].
(*! 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
let? output_dexter_ep_xtzToToken_contract :=
contract_ (Some "%xtzToToken")
dexter_definition.parameter_ep_xtzToToken_ty
output_dexter_address
in
amount env = (0 ~Mutez) /\
check_deadline deadline /\
(* The following binding simplifies the proof. *)
let! _ := tez.of_Z (Z.of_N (tokens_sold * 999) * tez.to_Z (sto_xtzPool sto)) in
let? (xtz_bought, xtz_bought_mod) :=
get_amount_bought tokens_sold (sto_tokenPool sto) (mutez_to_nat (sto_xtzPool sto))
in
let! xtz_bought_mutez := nat_to_mutez xtz_bought in
(* The following bindings simplify the proof. *)
let! _ := nat_to_mutez xtz_bought_mod in
let! _ := nat_to_mutez (xtz_bought * 999)%N in
let? (xtz_bought_net_burn, xtz_bought_net_burn_mod) :=
semantics.ediv_Z (Z.of_N xtz_bought * 999)%Z 1000%Z
in
let! xtz_bought_net_burn_mutez := nat_to_mutez (Z.to_N xtz_bought_net_burn) in
(* The following bindings simplify the proof. *)
let! _ := nat_to_mutez xtz_bought_net_burn_mod in
let! xtz_pool' := sub _ _ _ Sub_variant_tez_tez (sto_xtzPool sto) xtz_bought_net_burn_mutez in
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 /\
exists token_contract_ep_transfer,
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
let op1 :=
fa12.transfer env
token_contract_ep_transfer
{| fa12.from := env_sender;
fa12.to := env_self_address_ep_default;
fa12.amount := tokens_sold |}
in
let op2 :=
transfer_tokens env
dexter_definition.parameter_ep_xtzToToken_ty
(to, (min_tokens_bought, deadline))
xtz_bought_net_burn_mutez
output_dexter_ep_xtzToToken_contract
in
let! burn_amount_mutez :=
sub _ _ _ Sub_variant_tez_tez xtz_bought_mutez xtz_bought_net_burn_mutez
in
let? null_contract := contract_ None unit null_address in
let op_burn := transfer_xtz env burn_amount_mutez null_contract in
ret_ops = [ op1; op2; op_burn ].
(*
* (*! 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 p))) => ep_addLiquidity env p sto ret_ops ret_sto
| (inl (inl (inr p))) => ep_default env p sto ret_ops ret_sto
| (inl (inr (inl p))) => ep_removeLiquidity env p sto ret_ops ret_sto
| (inl (inr (inr p))) => ep_tokenToToken env p sto ret_ops ret_sto
| (inr (inl p)) => ep_tokenToXtz env p sto ret_ops ret_sto
| (inr (inr p)) => ep_xtzToToken env p sto ret_ops ret_sto
end.
