https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 08edb74856d05a9ecdbc5dc5e40903aee308bd1b authored by Arvid Jakobsson on 28 September 2020, 21:46:43 UTC
[dexter] update proof for exchange entrypoints
[dexter] update proof for exchange entrypoints
Tip revision: 08edb74
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. *)
Require List.
Require Import String.
Require Import Michocoq.macros.
Import syntax.
Import comparable.
Require Import NArith.
Require Import semantics.
Require Import util.
Import error.
Require dexter_definition.
Open Scope string_scope.
Import List.ListNotations.
Open Scope list_scope.
Require Import ZArith.
Module Dexter_spec (C:ContractContext).
Module semantics := Semantics C. Import semantics.
(** Some helpers over the environment *)
(* 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).
Definition transfer
(env : @proto_env dexter_definition.self_type)
(contract : ep_transfer)
(from to : data address)
(amount : data nat) :=
transfer_tokens env
ep_transfer_ty
(from, (to, 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 : @proto_env dexter_definition.self_type) 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 : @proto_env dexter_definition.self_type) (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 : @proto_env dexter_definition.self_type) adr contract :=
contract_ (Some ep_getBalance_annot)
ep_getBalance_ty adr = Some contract.
End fa12.
(** Convenience functions for maps *)
Section Map.
Definition map_empty
{k : comparable_type} {v : Set} : map.map (comparable_data k) v (compare k) :=
map.empty _ _ (compare k).
Definition map_get
{k : comparable_type} {v : Set}
(key : comparable_data k)
(m : map.map (comparable_data k) v (compare k)) : Datatypes.option v :=
map.get _ _ (compare k) key m.
Definition map_get_def
{k : comparable_type} {v : Set}
(key : comparable_data k)
(m : map.map (comparable_data k) v (compare k))
(def : v) : v :=
match map_get key m with
| Some v => v
| None => def
end.
Definition map_update
{k : comparable_type} {v : Set}
(key : comparable_data k)
(value : Datatypes.option v)
(m : map.map (comparable_data k) v (compare k)) :
map.map (comparable_data k) v (compare k) :=
map.update _ _ (compare k) (comparable.compare_eq_iff k) (comparable.lt_trans k) (comparable.gt_trans k) key value m.
End Map.
(** 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 *)
Module Storage := dexter_definition.Storage C.
Import Storage.
(* composed functions *)
Section ComposedStorage.
Definition account_empty :
data (pair nat (* %balance *) (map (* %allowances *) address nat))
:= (0%N, map.empty _ _ _).
Definition get_account_balance (sto : data dexter_definition.storage_ty) (adr : data address) : data nat :=
let '(balance, all) := map_get_def adr (sto_accounts sto) account_empty in
balance.
(* Sets the balance of [adr] to [balance] in [sto]. If [sto] does not contain a binding for [adr],
* then an empty account is created for [adr], with no allowances and a balance of [balance]. *)
Definition set_account_balance
(sto : data dexter_definition.storage_ty)
(adr : data address) (balance : data nat) :
data dexter_definition.storage_ty :=
let '(balance_old, all) := map_get_def adr (sto_accounts sto) account_empty in
let acts' := map_update adr (Some (balance, all)) (sto_accounts sto) in
sto_set_accounts sto acts'.
Definition get_allowance
(sto : data dexter_definition.storage_ty)
(owner sender : data address) : data nat :=
let '(_, allowances) := map_get_def owner (sto_accounts sto) account_empty in
map_get_def sender allowances 0%N.
(* Sets the allowance for [sender] from [owner] to [allowance] in
[sto]. If [sto] does not contain a binding for [owner], then an
empty account is created for [owner], with only the allowance for
[owner] and an empty balance. *)
Definition set_allowance
(sto : data dexter_definition.storage_ty)
(owner sender : data address) (allowance : data nat)
: data dexter_definition.storage_ty :=
let '(balance, allowances) := map_get_def owner (sto_accounts sto) account_empty in
let allowances' := map_update sender (Some allowance) allowances in
let acts' := map_update owner (Some (balance, allowances')) (sto_accounts sto) in
sto_set_accounts sto acts'.
End ComposedStorage.
(*+ 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 : @proto_env dexter_definition.self_type).
Definition env_sender := sender 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 dexter_definition.self_type 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_header
(p : data dexter_definition.parameter_ep_addLiquidity_ty)
(sto : data dexter_definition.storage_ty) :=
let '((owner, min_lqt_minted), (max_tokens_deposited, deadline)) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
(0 < max_tokens_deposited)%N /\
(0 < min_lqt_minted)%N /\
amount env <> (0 ~Mutez).
Definition ep_addLiquidity_no_lqt
(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
let amount_nat := mutez_to_nat (amount env) in
let lqt_total := sto_lqtTotal sto in
let token_adr := sto_tokenAddress sto in
exists token_contract_ep_transfer xtz_pool',
fa12.is_ep_transfer env token_adr token_contract_ep_transfer /\
mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\
(1000000 <= amount_nat)%N /\
let sto1 := sto_set_lqtTotal sto amount_nat in
let sto2 := set_account_balance sto1 owner amount_nat in
let token_deposited := max_tokens_deposited in
let sto3 := sto_set_tokenPool sto2 ((sto_tokenPool sto) + max_tokens_deposited)%N in
let sto4 := sto_set_xtzPool sto3 xtz_pool' in
let token_transfer := fa12.transfer env token_contract_ep_transfer
owner
env_self_address_ep_default
token_deposited in
ret_sto = sto4 /\
ret_ops = [token_transfer].
Definition ep_addLiquidity_some_lqt
(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_xtzPool sto <> (0 ~Mutez) /\
let amount_nat := mutez_to_nat (amount env) in
let lqt_total := sto_lqtTotal sto in
let token_adr := sto_tokenAddress sto in
exists token_contract_ep_transfer xtz_pool',
fa12.is_ep_transfer env token_adr token_contract_ep_transfer /\
mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\
let lqt_created := ((lqt_total * amount_nat) / (mutez_to_nat (sto_xtzPool sto)))%N in
(min_lqt_minted <= lqt_created)%N /\
let sto1 := sto_set_lqtTotal sto (sto_lqtTotal sto + lqt_created)%N in
let new_balance := (get_account_balance sto owner + lqt_created)%N in
let sto2 := set_account_balance sto1 owner new_balance in
(* Formalization note: here, / refers to div, defined such that a / b = q,
* where a = b * q + r , 0 <= r < b.
* As sto_tokenPool sto, amount_nat, (mutez_to_nat
* (sto_xtzPool sto)) are all nat (thus positive),
* this is the same as floor( a / b )
**)
let token_deposited :=
Nceiling (sto_tokenPool sto * amount_nat)
(mutez_to_nat (sto_xtzPool sto)) in
(token_deposited > 0)%N /\
(token_deposited <= max_tokens_deposited)%N /\
let sto3 := sto_set_tokenPool sto2 (sto_tokenPool sto + token_deposited)%N in
let sto4 := sto_set_xtzPool sto3 xtz_pool' in
let token_transfer := fa12.transfer env token_contract_ep_transfer
owner
env_self_address_ep_default
token_deposited in
ret_sto = sto4 /\
ret_ops = [token_transfer].
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) :=
ep_addLiquidity_header p sto /\
let lqt_total := sto_lqtTotal sto in
match lqt_total with
(* First liquidity provider *)
| 0%N => ep_addLiquidity_no_lqt p sto ret_ops ret_sto
(*
* First liquidity provider must give at least 1tz
*)
| _ => ep_addLiquidity_some_lqt p sto ret_ops ret_sto
end.
(*
* PROP-AL-000: if Dexter does not have permission to transfer the owner’s FA1.2 tokens, it will fail.
*)
Lemma prop_al_000 :
forall (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),
ep_addLiquidity p sto ret_ops ret_sto ->
(* This is not really provable from dexter, as
* it concerns the internals of FA1.2 *)
True.
Proof. Admitted.
(*
* PROP-AL-001: if now is greater than deadline, it will fail.
*)
Lemma prop_al_001 :
forall (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
~ check_deadline deadline ->
~ ep_addLiquidity p sto ret_ops ret_sto.
Proof. Admitted.
(*
* PROP-AL-002: if min_lqt_minted is 0, it will fail.
*)
Lemma prop_al_002 :
forall (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
(0 = min_lqt_minted)%N ->
~ ep_addLiquidity p sto ret_ops ret_sto ->
(* This is not really provable from dexter, as
* it concerns the internals of FA1.2 *)
True.
Proof. Admitted.
(*
* PROP-AL-003: if max_tokens_deposited is 0, it will fail.
*)
Lemma prop_al_003 :
forall (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
(0 = max_tokens_deposited)%N ->
~ ep_addLiquidity p sto ret_ops ret_sto ->
(* This is not really provable from dexter, as
* it concerns the internals of FA1.2 *)
True.
Proof. Admitted.
(*
* PROP-AL-004: if now is less than deadline, lqt_pool is zero, min_lqt_minted is greater than zero, amount is greater than or equal to one tez, Dexter has permission to transfer max_tokens_deposited from owner’s FA1.2 tokens, owner has at least max_tokens_deposited FA1.2 tokens and token_address is a FA1.2 contract, then it should succeed.
*)
Lemma prop_al_004 :
forall (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),
ep_addLiquidity p sto ret_ops ret_sto ->
(* TODO: This basically
* just restates the full specification so I don't see the point. *)
True.
Proof. Admitted.
(*
* PROP-AL-005: If PROP-AL-004 is true, then storage will be updated such that lqt_total := amount, token_pool += max_tokens_deposited, xtz_pool += amount.
*)
Lemma prop_al_005 :
forall (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),
ep_addLiquidity p sto ret_ops ret_sto ->
(* TODO: This basically
* just restates the full specification so I don't see the point. *)
True.
Proof. Admitted.
(*
* PROP-AL-006: if now is less than deadline, lqt_pool is greater than zero, min_lqt_minted is greater than zero, tokens_deposited less than or equal to max_tokens_deposited, amount is greater than zero, Dexter has permission to transfer tokens_deposited from owner’s FA1.2 tokens, owner has at least tokens_deposited FA1.2 tokens and token_address is a FA1.2 contract, then it should succeed.
*)
Lemma prop_al_006 :
forall (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),
ep_addLiquidity p sto ret_ops ret_sto ->
(* TODO: This basically
* just restates the full specification so I don't see the point. *)
True.
Proof. Admitted.
(*
* PROP-AL-007: Assume PROP-AL-006, then storage will be updated such that lqt_total := floor(lqt_total * amount / xtz_pool), accounts[owner].balance := floor(lqt_total * amount / xtz_pool), token_pool += tokens_deposit and xtz_pool += amount.
*)
Lemma prop_al_007 :
forall (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),
ep_addLiquidity p sto ret_ops ret_sto ->
(* TODO: This basically
* just restates the full specification so I don't see the point. *)
True.
Proof. Admitted.
(*! Entry point: ep_approve !*)
Definition ep_approve
(p : data dexter_definition.parameter_ep_approve_ty)
(sto : data dexter_definition.storage_ty)
(ret_ops : data (list operation))
(ret_sto : data dexter_definition.storage_ty) :=
amount env = (0 ~Mutez) /\
~ sto_selfIsUpdatingTokenPool sto /\
let '(spender, (new_allowance, current_allowance)) := p in
match map_get env_sender (sto_accounts sto) with
| None =>
current_allowance = 0%N /\
let allowances := map_update spender (Some new_allowance) map_empty in
let accounts' := map_update env_sender (Some (0%N, allowances)) (sto_accounts sto) in
ret_sto = sto_set_accounts sto accounts'
| Some (act_balance, allowances) =>
current_allowance = map_get_def spender allowances 0%N /\
let allowances' := map_update spender (Some new_allowance) allowances in
let accounts' := map_update env_sender (Some (act_balance, allowances')) (sto_accounts sto) in
ret_sto = sto_set_accounts sto accounts'
end /\ ret_ops = nil.
(* TODO: PROP-APR-000..005 *)
(*! 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 sto1 := sto_set_xtzPool sto xtz_pool' %N in
ret_sto = sto1 /\ ret_ops = nil.
(*
* PROP-D-000: For any amount of xtz sent (the value in AMOUNT), xtz_pool will be set to +=xtz_pool + amount at the end of the operation
*)
Lemma prop_d_000 :
forall (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),
ep_default p sto ret_ops ret_sto ->
exists xtz_pool',
mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\
sto_xtzPool ret_sto = sto_xtzPool ret_sto.
Proof.
(*
* intros.
* destruct H as [xtz_pool' Hxtz_pool].
* exists xtz_pool'. intuition.
* Qed.
*)
Admitted.
(*! Entry point: removeLiquidity !*)
(* [check_allowance_update sto owner sender amount] holds if [sender] is allowed to spend
[amount] in the name of [owner]. If [owner] = [sender] then this always holds.
Otherwise, it is verified that:
allowance >= amount
where allowance = storage.accounts[owner].allowances[sender].
if allowance is undefined, since either storage.accounts[owner] or
storage.accounts[owner].allowances[sender] is undefined,
then allowance is 0. in other words, even if no allowance is set,
sender can spend 0 tokens in the name of owner.Arith_status
If the check is successful, a new storage is returned, where the
allowance of [owner] for [sender] is decremented by [amount] if [owner] <> [sender].
If [owner] == [sender] the [sto] is returned.
*)
Definition check_allowance_update
(sto : data dexter_definition.storage_ty)
(owner sender : data address)
(amount : data nat) : Datatypes.option (data dexter_definition.storage_ty) :=
if cmp_eqb owner sender then
Some sto
else
match map_get owner (sto_accounts sto) with
| Some (_, allowances) =>
match map_get sender allowances with
| Some current_allowance =>
if cmp_geb current_allowance amount then
Some (set_allowance sto owner sender (current_allowance - amount))%N
else None
| None => None
end
| None => None
end.
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 '((owner, (to, lqt_burned)),
(min_xtz_withdrawn,
(min_tokens_withdrawn, deadline))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
check_deadline deadline /\
(* parameter verification *)
min_xtz_withdrawn <> (0 ~Mutez)%Z /\
min_tokens_withdrawn <> 0%N /\
sto_lqtTotal sto <> 0%N /\
lqt_burned <> 0%N /\
match map_get owner (sto_accounts sto) with
| None => False
| Some (balance, _) =>
(balance >= lqt_burned)%N /\
(lqt_burned <= sto_lqtTotal sto)%N /\
match check_allowance_update sto owner env_sender lqt_burned with
(* Allowance check failed *)
| None => False
(* Allowance check passed *)
| Some sto1 =>
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 _ _ =>
(* Note Arvid: I'm unsure what to say in this case.
* probably the contract will just fail if the withdrawn amount
* cannot be represented as mutez.
* however, other checks preclude this possibility:
* - lqt_burned <= get_account_balance sto owner
* -> lqt_burned < lqt_total
* and mutez with drawn is a fraction of the (mutez_to_nat
* (sto_xtzPool sto)), which is representable as mutez.
*
* This False says that it is not possible that the contracts
* executes without error in this case.
*
*)
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 /\
let sto2 := sto_set_tokenPool sto1 (sto_tokenPool sto - tokens_withdrawn)%N in
exists xtz_pool',
mutez_sub (sto_xtzPool sto) xtz_withdrawn_mutez xtz_pool' /\
let sto3 := sto_set_xtzPool sto2 xtz_pool' in
(* 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,
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
let sto4 := set_account_balance
sto3 owner (get_account_balance sto owner - lqt_burned)%N in
let sto5 := sto_set_lqtTotal
sto4 (sto_lqtTotal sto - lqt_burned)%N in
ret_sto = sto5 /\
ret_ops = [
fa12.transfer env token_contract_ep_transfer env_self_address_ep_default to tokens_withdrawn;
transfer_tokens env unit tt xtz_withdrawn_mutez to_contract
]
end
end
end
end.
(*
* PROP-RL-000: Regardless of other parameter values, if xtz sent is greater than zero, this operation will fail. (All other PROP-RL properties assume that AMOUNT is zero).
*)
Ltac destruct_pairs :=
match goal with
| x : data (pair _ _) |- _ => destruct x; destruct_pairs
| _ => idtac
end.
Lemma prop_rl_000 :
forall (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),
amount env <> (0 ~Mutez) ->
~ ep_removeLiquidity p sto ret_ops ret_sto.
Proof.
intros [ ] sto ret_ops ret_sto HamountNz.
destruct_pairs.
intros Hep_correct.
simpl in Hep_correct.
intuition.
Qed.
(*
* PROP-RL-001: For any deadline value greater than or equal to NOW, the operation will fail.
*)
Lemma prop_rl_001 :
forall (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 '((owner, (to, lqt_burned)),
(min_xtz_withdrawn,
(min_tokens_withdrawn, deadline))) := p in
~ check_deadline deadline ->
~ ep_removeLiquidity p sto ret_ops ret_sto.
Proof.
intros p sto ret_ops ret_sto.
destruct p as ((owner, (to, lqt_burned)),
(min_xtz_withdrawn, (min_tokens_withdrawn, deadline))).
unfold ep_removeLiquidity. intuition.
Qed.
(* TODO: PROP-RL-002..008, 010 *)
(* PROP-RL-009: For any deadline value less than NOW,
min_xtz_withdrawn greater than zero, min_tokens_withdrawn greater
than zero, xtz_withdrawn greater than or equal to min_xtz_withdrawn,
tokens_withdrawn greater than or equal to min_tokens_withdrawn,
lqt_burned less than or equal to accounts[owner].balance, if to has
a parameter of unit (or is an entrypoint with parameter unit),
tokens_withdrawn will be given to to via the token_address contract
and xtz_withdrawn will be sent to to. If to or its provided entry
point do not have parameter of type unit, this operation will
fail. *)
Lemma prop_rl_009 :
forall (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),
(*
* ep_removeLiquidity p sto ret_ops ret_sto ->
* (* TODO reformalize the above. However, this basically
* just restates the full specification so I don't see the point. *)
*)
False.
Admitted.
(*! 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.
(*
* PROP-SB-000: Regardless of other parameter values, if xtz sent is greater than zero, this operation will fail. (All other PROP-SB properties assume that AMOUNT is zero).
*)
Lemma prop_sb_000 :
forall (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),
amount env <> (0 ~Mutez) ->
~ ep_setBaker p sto ret_ops ret_sto.
Proof.
intros [ ] sto ret_ops ret_sto HamountNz.
destruct_pairs.
intros Hep_correct.
simpl in Hep_correct.
intuition.
Qed.
(*
* PROP-SB-001: For any sender that is not the manager, the operation will fail.
*)
Lemma prop_sb_001 :
forall (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),
env_sender <> sto_manager sto ->
~ ep_setBaker p sto ret_ops ret_sto.
Proof.
intros [ ] sto ret_ops ret_sto HamountNz.
destruct_pairs.
intros Hep_correct.
simpl in Hep_correct.
intuition.
Qed.
(*
* PROP-SB-002: For any sender that is the manager and freeze_baker is true, the operation will fail.
*)
Lemma prop_sb_002 :
forall (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),
env_sender = sto_manager sto ->
sto_freezeBaker sto ->
~ ep_setBaker p sto ret_ops ret_sto.
Proof.
intros [ ] sto ret_ops ret_sto HamountNz HbakerFrozen.
destruct_pairs.
intros Hep_correct.
simpl in Hep_correct.
intuition.
Qed.
(*
* PROP-SB-003: For any sender that is the manager, freeze_baker is false, and baker is None, if the contract currently has a baker it will remove it, otherwise the operation will fail.
*)
Lemma prop_sb_003 :
forall (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),
(*
* ep_setBaker p sto ret_ops ret_sto ->
* (* TODO reformalize the above. However, this follows from the
* specification of ep_setBaker, and the semantics of operations
* in Tezos. However, the latter is not formalized in mi-cho-coq
* and cannot thus be verified here. *)
*)
False.
Admitted.
(*
* PROP-SB-004: For any sender that is the manager, freeze_baker is false, and baker is a baker address, if baker is a valid baker address that is not the current baker or there is no baker, it will set the contract’s baker to baker, otherwise it will fail (trying to set the same baker or setting to an invalid baker)
*)
Lemma prop_sb_004 :
forall (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),
(*
* ep_setBaker p sto ret_ops ret_sto -> (* TODO reformalize
* the above, however, same remark as above. *)
*)
False.
Admitted.
(*! 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) : N :=
((input_amount * 997 * output_pool)
/ (input_pool * 1000 + (input_amount * 997)))%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) = 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 '((owner, to), (tokens_sold, (min_xtz_bought, deadline))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
amount env = (0 ~Mutez) /\
min_xtz_bought <> (0 ~Mutez) /\
sto_xtzPool sto <> (0 ~Mutez) /\
(sto_tokenPool sto <> 0)%N /\
(tokens_sold <> 0)%N /\
let xtz_bought := get_amount_bought tokens_sold
(sto_tokenPool sto)
(mutez_to_nat (sto_xtzPool sto)) in
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' /\
let sto1 := sto_set_tokenPool sto (sto_tokenPool sto + tokens_sold)%N in
let sto2 := sto_set_xtzPool sto1 xtz_pool' %N in
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
ret_sto = sto2 /\
ret_ops = [
transfer_tokens env unit tt xtz_bought_mutez to_contract;
fa12.transfer env token_contract_ep_transfer owner env_self_address_ep_default tokens_sold
]
end
| Failed _ _ => False
end.
(*! Entry point: updateTokenPool !*)
Definition ep_updateTokenPool
(sender_key_hash : 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,
env_sender = address_ unit (implicit_account sender_key_hash) /\
~ sto_selfIsUpdatingTokenPool sto /\
amount env = (0 ~Mutez) /\
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.
(*
* PROP-UTB-000: Regardless of other parameter values, if xtz sent is greater than zero, this operation will fail. (All other PROP-UTB properties assume that AMOUNT is zero).
*)
Lemma prop_utb_000 :
forall (p : 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),
amount env <> (0 ~Mutez) ->
~ ep_updateTokenPool p sto ret_ops ret_sto.
Proof.
intros [ ] sto ret_ops ret_sto HamountNz.
destruct_pairs.
intros [ fa12_ep_getBalance H ].
intuition.
Qed.
(*
* PROP-UTB-001: If the contract at token_address does not have a getBalance entrypoint, it will fail (the originator of the contract is responsible for making sure token_address points to a valid FA1.2 contract).
*)
Lemma prop_utb_001 :
forall (p : 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),
~ isSome (contract_
(Some fa12.ep_getBalance_annot)
fa12.ep_getBalance_ty
(sto_tokenAddress sto)) ->
~ ep_updateTokenPool p sto ret_ops ret_sto.
Proof.
(*
* intros p sto ret_ops ret_sto.
* unfold isSome.
* destruct (contract_ _) eqn:HcontractNex; intro H. intuition.
* unfold ep_updateTokenPool.
* intros [contract [ _ [ HcontractEx _ ]]].
* congruence.
* Qed.
*)
Admitted.
(*
* PROP-UTB-002: If the contract at token_address has a getBalance entrypoint with the expected type signature (?), and the expected properties of Update Token Balance Internal are met, then token_pool will be updated and called_by_dexter will be false.
*)
Lemma prop_utb_002 :
forall (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),
(*
* ep_updateTokenPool p sto ret_ops ret_sto ->
* (* This property follows from the correctness of updateTokenPool &
* updateTokenPoolInternal, and presumably, the semantics of the
* inter-contract execution of model. However, the latter is not yet
* modelled in mi-cho-coq, so this property cannot be proved yet. *)
*)
False.
Admitted.
(*! 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 /\
amount env <> (0 ~Mutez) /\
(min_tokens_bought <> 0)%N /\
sto_xtzPool sto <> (0 ~Mutez) /\
(sto_tokenPool sto <> 0)%N /\
let tokens_bought := get_amount_bought (mutez_to_nat (amount env))
(mutez_to_nat (sto_xtzPool sto))
(sto_tokenPool sto) in
(*
==
((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 sto1 := sto_set_tokenPool sto (sto_tokenPool sto - tokens_bought)%N in
let sto2 := sto_set_xtzPool sto1 xtz_pool' %N in
ret_sto = sto2 /\
ret_ops = [fa12.transfer env token_contract_ep_transfer env_self_address_ep_default to tokens_bought].
(* TODO: PROP-XTT-000..002 *)
(*
* PROP-UTBI-000: Regardless of other parameter values, if xtz sent is greater than zero, this operation will fail. (All other PROP-UTBI properties assume that AMOUNT is zero).
*)
Lemma prop_utbi_000 :
forall (p : 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) ->
~ ep_updateTokenPoolInternal p sto ret_ops ret_sto.
Proof.
intros p sto ret_ops ret_sto HamountNz.
intros Hep_correct.
unfold ep_updateTokenPoolInternal in Hep_correct.
intuition.
Qed.
(*
* PROP-UTBI-001: For any sender that is not equal to token_address, the operation will fail.
*)
Lemma prop_utbi_001 :
forall (p : 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),
env_sender <> sto_tokenAddress sto ->
~ ep_updateTokenPoolInternal p sto ret_ops ret_sto.
Proof.
intros p sto ret_ops ret_sto HsenderNeq.
intros Hep_correct.
unfold ep_updateTokenPoolInternal in Hep_correct.
intuition.
Qed.
(*
* PROP-UTBI-002: For any sender that is equal to token_address, and called_by_dexter is not true, the operation will fail.
*)
Lemma prop_utbi_002 :
forall (p : 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),
(*
* ep_updateTokenPoolInternal p sto ret_ops ret_sto -> (* TODO reformalize the above *)
*)
env_sender = sto_tokenAddress sto ->
~ sto_selfIsUpdatingTokenPool sto ->
~ ep_updateTokenPoolInternal p sto ret_ops ret_sto.
Proof.
intros p sto ret_ops ret_sto HsenderNeq Hncalled.
intros Hep_correct.
unfold ep_updateTokenPoolInternal in Hep_correct.
intuition.
Qed.
(*
* PROP-UTBI-002: For any sender that is equal to token_address, and called_by_dexter is true, storage token_pool will be set to parameter token_pool, and called_by_dexter will be set to false.
*)
Lemma prop_utbi_003 :
forall (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),
(*
* ep_updateTokenPoolInternal p sto ret_ops ret_sto ->
* (* this is just a reformulation of the full spec again *)
*)
False.
Admitted.
(*! 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,
owner)),
(to,
(tokens_sold,
deadline))) := p in
~ sto_selfIsUpdatingTokenPool sto /\
check_deadline deadline /\
amount env = (0 ~Mutez) /\
(min_tokens_bought <> 0)%N /\
sto_xtzPool sto <> (0 ~Mutez) /\
(sto_tokenPool sto <> 0)%N /\
(tokens_sold <> 0)%N /\
let xtz_bought := get_amount_bought tokens_sold
(sto_tokenPool sto)
(mutez_to_nat (sto_xtzPool sto)) in
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 =>
mutez_sub (sto_xtzPool sto) xtz_bought_mutez xtz_pool' /\
let sto1 := sto_set_tokenPool sto (sto_tokenPool sto + tokens_sold)%N in
let sto2 := sto_set_xtzPool sto1 xtz_pool' %N in
fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\
ret_sto = sto2 /\
ret_ops = [
transfer_tokens env
dexter_definition.parameter_ep_xtzToToken_ty
(to, (min_tokens_bought, deadline))
xtz_bought_mutez
output_dexter_ep_xtzToToken_contract ;
fa12.transfer env
token_contract_ep_transfer
owner
env_self_address_ep_default
tokens_sold
]
| None => False
end
| Failed _ _ => False
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.
End entrypoints.
(*! Full spec !*)
Definition main
(env : @proto_env dexter_definition.self_type)
(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_approve env p sto ret_ops ret_sto
| (inl (inl (inr p))) => ep_addLiquidity env p sto ret_ops ret_sto
| (inl (inr (inl p))) => ep_removeLiquidity env p sto ret_ops ret_sto
| (inl (inr (inr (inl p)))) => ep_xtzToToken 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_tokenToToken env p sto ret_ops ret_sto
| (inr (inl (inr (inl p)))) => ep_updateTokenPool env p sto ret_ops ret_sto
| (inr (inl (inr (inr p)))) => ep_updateTokenPoolInternal env p sto ret_ops ret_sto
| (inr (inr (inl p))) => ep_setBaker env p sto ret_ops ret_sto
| (inr (inr (inr (inl p)))) => ep_setManager env p sto ret_ops ret_sto
| (inr (inr (inr (inr p)))) => ep_default env p sto ret_ops ret_sto
end.
End Dexter_spec.
