Require Import cpmm_spec. Require Import cpmm_verification_ep_addLiquidity. Require Import cpmm_verification_ep_removeLiquidity. Require Import cpmm_verification_ep_default. Require Import cpmm_verification_ep_tokenToXtz. Require Import cpmm_verification_ep_xtzToToken. Require Import cpmm_verification_ep_tokenToToken.
cpmm_spec.ep_addLiquidity is the high-level specification of addLiquidity and ep_addLiquidity is the Michelson code for this entrypoint.
cpmm_spec.ep_addLiquidity = fun (env : env_ty) (p : data cpmm_definition.parameter_ep_addLiquidity_ty) (sto : data cpmm_definition.storage_ty) (ret_ops : data (list operation)) (ret_sto : data cpmm_definition.storage_ty) => let '(owner, (min_lqt_minted, (max_tokens_deposited, deadline))) := p in check_deadline env 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 : {sao : address_constant * annot_o | get_address_type sao = Some fa12.ep_transfer_ty}) (lqt_contract_ep_mintOrBurn : {sao : address_constant * annot_o | get_address_type sao = Some lqt.ep_mintOrBurn_ty}) (xtz_pool' : data mutez), 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) in let token_deposited := Nceiling (sto_tokenPool sto * amount_nat) (mutez_to_nat (sto_xtzPool sto)) in min_lqt_minted <= lqt_created /\ token_deposited <= max_tokens_deposited /\ (let sto0 := sto_set_lqtTotal sto (sto_lqtTotal sto + lqt_created) in let sto1 := sto_set_tokenPool sto0 (sto_tokenPool sto0 + token_deposited) in let sto2 := sto_set_xtzPool sto1 xtz_pool' in ret_sto = sto2 /\ ret_ops = [fa12.transfer env token_contract_ep_transfer {| Spec.fa12.from := env_sender env; Spec.fa12.to := env_self_address_ep_default env; Spec.fa12.amount := token_deposited |}; lqt.mint env lqt_contract_ep_mintOrBurn {| Spec.lqt.minted := lqt_created; Spec.lqt.to := owner |}]))) : env_ty -> data cpmm_definition.parameter_ep_addLiquidity_ty -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Propep_addLiquidity = SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ NOW (SEQ COMPARE (SEQ GE (SEQ (IF_TRUE (SEQ (DROP 4 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 3)) (Tail_fail FAILWITH))) (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool true 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (Vector.cons Datatypes.bool false 39 (Vector.cons Datatypes.bool false 38 (Vector.cons Datatypes.bool false 37 (Vector.cons Datatypes.bool false 36 (Vector.cons Datatypes.bool false 35 (Vector.cons Datatypes.bool false 34 (Vector.cons Datatypes.bool false 33 (Vector.cons Datatypes.bool false 32 (Vector.cons Datatypes.bool false 31 (Vector.cons Datatypes.bool false 30 (...))))))))))))))))))))))))))))))))))) I))) (SEQ (DIG 4 eq_refl) (SEQ DUP (SEQ (DUG 5 eq_refl) (SEQ CDR (SEQ CAR (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ AMOUNT (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool true 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (...))))))))))))))))))))))))) I))) (SEQ SWAP (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ (DUG 2 eq_refl) (SEQ (DIG 6 eq_refl) (SEQ DUP (SEQ (DUG 7 eq_refl) (SEQ CDR (SEQ CDR (SEQ CAR (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ MUL (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ (DIG 2 eq_refl) (SEQ (DIG 6 eq_refl) (SEQ DUP (SEQ (DUG 7 eq_refl) (SEQ CAR (SEQ (DIG 3 eq_refl) (SEQ MUL (...)))))))))))))))))))))))))))))))))))))))) { })))))))))))))))))) : instruction_seq (Some (or (or (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp)))) (Some "%addLiquidity") unit (Some "%default")) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%removeLiquidity") (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%tokenToToken")) None) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp)))) (Some "%tokenToXtz") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))) (Some "%xtzToToken")) None, None)) false (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp))) ::: pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address)))) ::: []) (pair (list operation) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address))))) ::: [])
We show that they are semantically equivalent.
ep_addLiquidity_correct
: forall (env : proto_env) (p : data cpmm_definition.parameter_ep_addLiquidity_ty)
(sto : data cpmm_definition.storage_ty) (ret_ops : Datatypes.list (data operation))
(ret_sto : data cpmm_definition.storage_ty),
eval0_seq_precond env cpmm_verification_ep_addLiquidity.Def.ep_addLiquidity
(fun x : stack (pair (list operation) cpmm_verification_ep_addLiquidity.Def.storage_ty ::: []) =>
x = (ret_ops, ret_sto, tt)) (p, (sto, tt)) <->
cpmm_verification_ep_addLiquidity.Spec.ep_addLiquidity env p sto ret_ops ret_sto
cpmm_spec.ep_removeLiquidity is the high-level specification of removeLiquidity and ep_removeLiquidity is the Michelson code for this entrypoint.
cpmm_spec.ep_removeLiquidity = fun (env : env_ty) (p : data cpmm_definition.parameter_ep_removeLiquidity_ty) (sto : data cpmm_definition.storage_ty) (ret_ops : data (list operation)) (ret_sto : data cpmm_definition.storage_ty) => let '(to, (lqt_burned, (min_xtz_withdrawn, (min_tokens_withdrawn, deadline)))) := p in amount env = (0 ~Mutez) /\ check_deadline env deadline /\ lqt_burned <= sto_lqtTotal sto /\ sto_lqtTotal sto <> 0 /\ (let xtz_withdrawn := mutez_to_nat (sto_xtzPool sto) * lqt_burned / sto_lqtTotal sto in xtz_withdrawn >= mutez_to_nat min_xtz_withdrawn /\ (let! xtz_withdrawn_mutez := nat_to_mutez xtz_withdrawn in let tokens_withdrawn := sto_tokenPool sto * lqt_burned / sto_lqtTotal sto in tokens_withdrawn >= min_tokens_withdrawn /\ tokens_withdrawn <= sto_tokenPool sto /\ (exists xtz_pool' : data mutez, mutez_sub (sto_xtzPool sto) xtz_withdrawn_mutez xtz_pool' /\ (let? to_contract := contract_ None unit to in exists (token_contract_ep_transfer : {sao : address_constant * annot_o | get_address_type sao = Some fa12.ep_transfer_ty}) (lqt_contract_ep_mintOrBurn : {sao : address_constant * annot_o | get_address_type sao = Some lqt.ep_mintOrBurn_ty}), 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 sto0 := sto_set_xtzPool sto xtz_pool' in let sto1 := sto_set_tokenPool sto0 (sto_tokenPool sto0 - tokens_withdrawn) in let sto2 := sto_set_lqtTotal sto1 (sto_lqtTotal sto1 - lqt_burned) in ret_sto = sto2 /\ ret_ops = [lqt.burn env lqt_contract_ep_mintOrBurn {| Spec.lqt.burned := lqt_burned; Spec.lqt.from := env_sender env |}; fa12.transfer env token_contract_ep_transfer {| Spec.fa12.from := env_self_address_ep_default env; Spec.fa12.to := to; Spec.fa12.amount := tokens_withdrawn |}; transfer_xtz env xtz_withdrawn_mutez to_contract]))))) : env_ty -> data cpmm_definition.parameter_ep_removeLiquidity_ty -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Propep_removeLiquidity = SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ NOW (SEQ COMPARE (SEQ GE (SEQ (IF_TRUE (SEQ (DROP 5 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 3)) (Tail_fail FAILWITH))) (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool false 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (Vector.cons Datatypes.bool false 39 (Vector.cons Datatypes.bool false 38 (Vector.cons Datatypes.bool false 37 (Vector.cons Datatypes.bool false 36 (Vector.cons Datatypes.bool false 35 (...)))))))))))))))))))))))))))))) I))) (SEQ AMOUNT (SEQ COMPARE (SEQ GT (SEQ (IF_TRUE (SEQ (DROP 5 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 10)) (Tail_fail FAILWITH))) (SEQ (DIG 4 eq_refl) (SEQ DUP (SEQ (DUG 5 eq_refl) (SEQ CDR (SEQ CDR (SEQ CAR (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool true 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (...)))))))))))))))))) I))) (SEQ (DIG 6 eq_refl) (SEQ DUP (SEQ (DUG 7 eq_refl) (SEQ CDR (SEQ CAR (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ (DIG 4 eq_refl) (SEQ DUP (SEQ (DUG 5 eq_refl) (SEQ MUL (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun ... => Bool.Is_true ...) (Vector.cons Datatypes.bool true 63 (...)) I))) (SEQ SWAP (SEQ MUL (SEQ (DIG 5 eq_refl) (SEQ DUP (...))))))))))))))))))))))))))))) { })))))) { }))))))))))))))))))))))) : instruction_seq (Some (or (or (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp)))) (Some "%addLiquidity") unit (Some "%default")) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%removeLiquidity") (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%tokenToToken")) None) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp)))) (Some "%tokenToXtz") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))) (Some "%xtzToToken")) None, None)) false (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp)))) ::: pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address)))) ::: []) (pair (list operation) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address))))) ::: [])
We show that they are semantically equivalent.
ep_removeLiquidity_correct
: forall (env : env_ty) (p : data cpmm_definition.parameter_ep_removeLiquidity_ty)
(sto : data cpmm_definition.storage_ty) (ret_ops : Datatypes.list (data operation))
(ret_sto : data cpmm_definition.storage_ty),
eval0_seq_precond env cpmm_verification_ep_removeLiquidity.Def.ep_removeLiquidity
(fun x : stack (pair (list operation) cpmm_verification_ep_removeLiquidity.Def.storage_ty ::: []) =>
x = (ret_ops, ret_sto, tt)) (p, (sto, tt)) <->
cpmm_verification_ep_removeLiquidity.Spec.ep_removeLiquidity env p sto ret_ops ret_sto
cpmm_spec.ep_tokenToXtz is the high-level specification of tokenToXtz and ep_tokenToXtz is the Michelson code for this entrypoint.
cpmm_spec.ep_tokenToXtz = fun (env : env_ty) (p : data cpmm_definition.parameter_ep_tokenToXtz_ty) (sto : data cpmm_definition.storage_ty) (ret_ops : data (list operation)) (ret_sto : data cpmm_definition.storage_ty) => let '(to, (tokens_sold, (min_xtz_bought, deadline))) := p in check_deadline env 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 in let! _ := nat_to_mutez xtz_tmp in let? (xtz_bought_net_burn, tmp_mod) := semantics.ediv_N xtz_tmp 1000 in let! xtz_bought_net_burn_mutez := nat_to_mutez xtz_bought_net_burn in let! _ := 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 mutez mutez mutez Sub_variant_tez_tez (sto_xtzPool sto) xtz_bought_mutez in exists token_contract_ep_transfer : {sao : address_constant * annot_o | get_address_type sao = Some fa12.ep_transfer_ty}, fa12.is_ep_transfer env (sto_tokenAddress sto) token_contract_ep_transfer /\ (let sto0 := sto_set_tokenPool sto (sto_tokenPool sto + tokens_sold) in let sto1 := sto_set_xtzPool sto0 xtz_pool' in ret_sto = sto1 /\ (let? null_contract := contract_ None unit null_address in let! burn_amount_tez := sub mutez mutez mutez 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 {| Spec.fa12.from := env_sender env; Spec.fa12.to := env_self_address_ep_default env; Spec.fa12.amount := tokens_sold |}; transfer_xtz env xtz_bought_net_burn_mutez to_contract; op_burn])))) : env_ty -> data cpmm_definition.parameter_ep_tokenToXtz_ty -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Propep_tokenToXtz = SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ NOW (SEQ COMPARE (SEQ GE (SEQ (IF_TRUE (SEQ (DROP 4 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 3)) (Tail_fail FAILWITH))) (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool false 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (Vector.cons Datatypes.bool false 39 (Vector.cons Datatypes.bool false 38 (Vector.cons Datatypes.bool false 37 (Vector.cons Datatypes.bool false 36 (Vector.cons Datatypes.bool false 35 (Vector.cons Datatypes.bool false 34 (Vector.cons Datatypes.bool false 33 (Vector.cons Datatypes.bool false 32 (Vector.cons Datatypes.bool false 31 (Vector.cons Datatypes.bool false 30 (...))))))))))))))))))))))))))))))))))) I))) (SEQ AMOUNT (SEQ COMPARE (SEQ GT (SEQ (IF_TRUE (SEQ (DROP 4 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 10)) (Tail_fail FAILWITH))) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 999)) (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ MUL (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 1000)) (SEQ (DIG 5 eq_refl) (SEQ DUP (SEQ (DUG 6 eq_refl) (SEQ CAR (SEQ MUL (SEQ ADD (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool true 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (...))))))))))))))))) I))) (SEQ (DIG 5 eq_refl) (SEQ DUP (SEQ (DUG 6 eq_refl) (SEQ CDR (SEQ CAR (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 999)) (SEQ (DIG 4 eq_refl) (SEQ DUP (SEQ (DUG 5 eq_refl) (SEQ MUL (SEQ MUL (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (...) (...)) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ (PUSH (...) (...)) (SEQ SWAP (...)))))))))))))))))))))))))))))))))) { })))))) { })))))))))))))))))) : instruction_seq (Some (or (or (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp)))) (Some "%addLiquidity") unit (Some "%default")) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%removeLiquidity") (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%tokenToToken")) None) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp)))) (Some "%tokenToXtz") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))) (Some "%xtzToToken")) None, None)) false (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp))) ::: pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address)))) ::: []) (pair (list operation) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address))))) ::: [])
We show that they are semantically equivalent.
ep_tokenToXtz_correct
: forall (env : proto_env) (p : data cpmm_definition.parameter_ep_tokenToXtz_ty)
(sto : data cpmm_definition.storage_ty) (ret_ops : Datatypes.list (data operation))
(ret_sto : data cpmm_definition.storage_ty),
cpmm_verification_ep_tokenToXtz.Spec.arithmetic_invariant sto ->
eval0_seq_precond env cpmm_verification_ep_tokenToXtz.Def.ep_tokenToXtz
(fun x : stack (pair (list operation) cpmm_verification_ep_tokenToXtz.Def.storage_ty ::: []) =>
x = (ret_ops, ret_sto, tt)) (p, (sto, tt)) <->
cpmm_verification_ep_tokenToXtz.Spec.ep_tokenToXtz env p sto ret_ops ret_sto
cpmm_spec.ep_xtzToToken is the high-level specification of xtzTotoken and ep_xtzToToken is the Michelson code for this entrypoint.
cpmm_spec.ep_xtzToToken = fun (env : env_ty) (p : data cpmm_definition.parameter_ep_xtzToToken_ty) (sto : data cpmm_definition.storage_ty) (ret_ops : data (list operation)) (ret_sto : data cpmm_definition.storage_ty) => let '(to, (min_tokens_bought, deadline)) := p in check_deadline env 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 in let! burn_amount_tmp := sub nat nat int 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 /\ (let! new_token_pool_tmp := sub nat nat int 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 mutez mutez mutez Add_variant_tez_tez (sto_xtzPool sto) amount_net_burn_mutez in let sto0 := sto_set_xtzPool sto xtzPool' in let sto1 := sto_set_tokenPool sto0 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 = sto1 /\ (exists token_contract_ep_transfer : {sao : address_constant * annot_o | get_address_type sao = Some fa12.ep_transfer_ty}, fa12.is_ep_transfer env (sto_tokenAddress sto1) token_contract_ep_transfer /\ ret_ops = [fa12.transfer env token_contract_ep_transfer {| Spec.fa12.from := env_self_address_ep_default env; Spec.fa12.to := to; Spec.fa12.amount := tokens_bought |}; op_burn]))) : env_ty -> data cpmm_definition.parameter_ep_xtzToToken_ty -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Propep_xtzToToken = SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ NOW (SEQ COMPARE (SEQ GE (SEQ (IF_TRUE (SEQ (DROP 3 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 3)) (Tail_fail FAILWITH))) (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool true 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (Vector.cons Datatypes.bool false 39 (Vector.cons Datatypes.bool false 38 (Vector.cons Datatypes.bool false 37 (Vector.cons Datatypes.bool false 36 (Vector.cons Datatypes.bool false 35 (Vector.cons Datatypes.bool false 34 (Vector.cons Datatypes.bool false 33 (Vector.cons Datatypes.bool false 32 (Vector.cons Datatypes.bool false 31 (Vector.cons Datatypes.bool false 30 (Vector.cons Datatypes.bool false 29 (Vector.cons Datatypes.bool false 28 (Vector.cons Datatypes.bool false 27 (Vector.cons Datatypes.bool false 26 (Vector.cons Datatypes.bool false 25 (...)))))))))))))))))))))))))))))))))))))))) I))) (SEQ (DIG 3 eq_refl) (SEQ DUP (SEQ (DUG 4 eq_refl) (SEQ CDR (SEQ CAR (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ AMOUNT (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool true 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (Vector.cons Datatypes.bool false 39 (Vector.cons Datatypes.bool false 38 (Vector.cons Datatypes.bool false 37 (Vector.cons Datatypes.bool false 36 (Vector.cons Datatypes.bool false 35 (...)))))))))))))))))))))))))))))) I))) (SEQ SWAP (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 1000)) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 999)) (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ MUL (SEQ EDIV (SEQ (IF_NONE (SEQ (PUSH (Comparable_type string) (Comparable_constant string "DIV by 0")) (Tail_fail FAILWITH)) { }) (SEQ CAR (SEQ DUP (SEQ (DIG 2 eq_refl) (SEQ SUB (SEQ ABS (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 999)) (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ MUL (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 1000)) (SEQ (DIG 4 eq_refl) (SEQ MUL (SEQ ADD (SEQ (DIG 5 eq_refl) (SEQ DUP (SEQ (DUG 6 eq_refl) (SEQ CAR (SEQ (PUSH (...) (...)) (SEQ (...) (...))))))))))))))))))))))))))))))))))))))))))))) { }))))))))))))) : instruction_seq (Some (or (or (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp)))) (Some "%addLiquidity") unit (Some "%default")) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%removeLiquidity") (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%tokenToToken")) None) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp)))) (Some "%tokenToXtz") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))) (Some "%xtzToToken")) None, None)) false (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp)) ::: pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address)))) ::: []) (pair (list operation) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address))))) ::: [])
We show that they are semantically equivalent.
ep_xtzToToken_correct
: forall (env : proto_env) (p : data cpmm_definition.parameter_ep_xtzToToken_ty)
(sto : data cpmm_definition.storage_ty) (ret_ops : Datatypes.list (data operation))
(ret_sto : data cpmm_definition.storage_ty),
eval0_seq_precond env cpmm_verification_ep_xtzToToken.Def.ep_xtzToToken
(fun x : stack (pair (list operation) cpmm_verification_ep_xtzToToken.Def.storage_ty ::: []) =>
x = (ret_ops, ret_sto, tt)) (p, (sto, tt)) <->
cpmm_verification_ep_xtzToToken.Spec.ep_xtzToToken env p sto ret_ops ret_sto
cpmm_spec.ep_tokenToToken is the high-level specification of tokenToToken and ep_tokenToToken is the Michelson code for this entrypoint.
cpmm_spec.ep_tokenToToken = fun (env : env_ty) (p : data cpmm_definition.parameter_ep_tokenToToken_ty) (sto : data cpmm_definition.storage_ty) (ret_ops : data (list operation)) (ret_sto : data cpmm_definition.storage_ty) => let '(output_cpmm_address, (min_tokens_bought, (to, (tokens_sold, deadline)))) := p in let? output_cpmm_ep_xtzToToken_contract := contract_ (Some "%xtzToToken") cpmm_definition.parameter_ep_xtzToToken_ty output_cpmm_address in amount env = (0 ~Mutez) /\ check_deadline env deadline /\ (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 let! _ := nat_to_mutez xtz_bought_mod in let! _ := nat_to_mutez (xtz_bought * 999) in let? (xtz_bought_net_burn, xtz_bought_net_burn_mod) := semantics.ediv_Z (Z.of_N xtz_bought * 999) 1000 in let! xtz_bought_net_burn_mutez := nat_to_mutez (Z.to_N xtz_bought_net_burn) in let! _ := nat_to_mutez xtz_bought_net_burn_mod in let! xtz_pool' := sub mutez mutez mutez Sub_variant_tez_tez (sto_xtzPool sto) xtz_bought_mutez in let sto0 := sto_set_tokenPool sto (sto_tokenPool sto + tokens_sold) in let sto1 := sto_set_xtzPool sto0 xtz_pool' in ret_sto = sto1 /\ (exists token_contract_ep_transfer : {sao : address_constant * annot_o | get_address_type sao = Some fa12.ep_transfer_ty}, fa12.is_ep_transfer env (sto_tokenAddress sto1) token_contract_ep_transfer /\ (let op1 := fa12.transfer env token_contract_ep_transfer {| Spec.fa12.from := env_sender env; Spec.fa12.to := env_self_address_ep_default env; Spec.fa12.amount := tokens_sold |} in let op2 := transfer_tokens env cpmm_definition.parameter_ep_xtzToToken_ty (to, (min_tokens_bought, deadline)) xtz_bought_net_burn_mutez output_cpmm_ep_xtzToToken_contract in let! burn_amount_mutez := sub mutez mutez mutez 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]))) : env_ty -> data cpmm_definition.parameter_ep_tokenToToken_ty -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Propep_tokenToToken = SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ SWAP (SEQ DUP (SEQ CDR (SEQ SWAP (SEQ CAR (SEQ (DIG 4 eq_refl) (SEQ (CONTRACT (Some "%xtzToToken") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp)))) (SEQ (IF_NONE (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 31)) (Tail_fail FAILWITH)) { }) (SEQ (PUSH (Comparable_type mutez) (Comparable_constant mutez (exist (fun t : int64bv.int64 => Bool.Is_true (negb (int64bv.sign t))) (Vector.cons Datatypes.bool false 63 (Vector.cons Datatypes.bool false 62 (Vector.cons Datatypes.bool false 61 (Vector.cons Datatypes.bool false 60 (Vector.cons Datatypes.bool false 59 (Vector.cons Datatypes.bool false 58 (Vector.cons Datatypes.bool false 57 (Vector.cons Datatypes.bool false 56 (Vector.cons Datatypes.bool false 55 (Vector.cons Datatypes.bool false 54 (Vector.cons Datatypes.bool false 53 (Vector.cons Datatypes.bool false 52 (Vector.cons Datatypes.bool false 51 (Vector.cons Datatypes.bool false 50 (Vector.cons Datatypes.bool false 49 (Vector.cons Datatypes.bool false 48 (Vector.cons Datatypes.bool false 47 (Vector.cons Datatypes.bool false 46 (Vector.cons Datatypes.bool false 45 (Vector.cons Datatypes.bool false 44 (Vector.cons Datatypes.bool false 43 (Vector.cons Datatypes.bool false 42 (Vector.cons Datatypes.bool false 41 (Vector.cons Datatypes.bool false 40 (Vector.cons Datatypes.bool false 39 (Vector.cons Datatypes.bool false 38 (Vector.cons Datatypes.bool false 37 (Vector.cons Datatypes.bool false 36 (Vector.cons Datatypes.bool false 35 (Vector.cons Datatypes.bool false 34 (Vector.cons Datatypes.bool false 33 (Vector.cons Datatypes.bool false 32 (...))))))))))))))))))))))))))))))))) I))) (SEQ AMOUNT (SEQ COMPARE (SEQ GT (SEQ (IF_TRUE (SEQ (DROP 6 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 10)) (Tail_fail FAILWITH))) (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ NOW (SEQ COMPARE (SEQ GE (SEQ (IF_TRUE (SEQ (DROP 6 eq_refl) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 3)) (Tail_fail FAILWITH))) (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 999)) (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ MUL (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 1000)) (SEQ (DIG 7 eq_refl) (SEQ DUP (SEQ (DUG 8 eq_refl) (SEQ CAR (SEQ MUL (SEQ ADD (SEQ (DIG 6 eq_refl) (SEQ DUP (SEQ (DUG 7 eq_refl) (SEQ CDR (SEQ CAR (SEQ (PUSH (Comparable_type nat) (Comparable_constant nat 999)) (SEQ (DIG 4 eq_refl) (SEQ DUP (SEQ (DUG 5 eq_refl) (SEQ MUL (...)))))))))))))))))))))))) { })))))))) { })))))))))))))))))))))))))) : instruction_seq (Some (or (or (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp)))) (Some "%addLiquidity") unit (Some "%default")) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%removeLiquidity") (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%tokenToToken")) None) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp)))) (Some "%tokenToXtz") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))) (Some "%xtzToToken")) None, None)) false (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp)))) ::: pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address)))) ::: []) (pair (list operation) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address))))) ::: [])
We show that they are semantically equivalent.
ep_tokenToToken_correct
: forall (env : proto_env) (p : data cpmm_definition.parameter_ep_tokenToToken_ty)
(sto : data cpmm_definition.storage_ty) (ret_ops : Datatypes.list (data operation))
(ret_sto : data cpmm_definition.storage_ty),
eval0_seq_precond env Def.ep_tokenToToken
(fun x : stack (pair (list operation) Def.storage_ty ::: []) => x = (ret_ops, ret_sto, tt))
(p, (sto, tt)) <-> Spec.ep_tokenToToken env p sto ret_ops ret_sto
cpmm_spec.ep_default is the high-level specification of default and ep_default is the Michelson code for this entrypoint.
cpmm_spec.ep_default = fun (env : env_ty) (_ : data cpmm_definition.parameter_ep_default_ty) (sto : data cpmm_definition.storage_ty) (ret_ops : data (list operation)) (ret_sto : data cpmm_definition.storage_ty) => exists xtz_pool' : data mutez, mutez_add (sto_xtzPool sto) (amount env) xtz_pool' /\ (let sto0 := sto_set_xtzPool sto xtz_pool' in ret_sto = sto0 /\ ret_ops = []) : env_ty -> data cpmm_definition.parameter_ep_default_ty -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Propep_default = SEQ (DROP 1 eq_refl) (SEQ DUP (SEQ CDR (SEQ CDR (SEQ AMOUNT (SEQ (DIG 2 eq_refl) (SEQ DUP (SEQ (DUG 3 eq_refl) (SEQ CDR (SEQ CAR (SEQ ADD (SEQ PAIR (SEQ SWAP (SEQ CAR (SEQ PAIR (SEQ (NIL operation) (SEQ PAIR { })))))))))))))))) : instruction_seq (Some (or (or (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type nat) (Comparable_type timestamp)))) (Some "%addLiquidity") unit (Some "%default")) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%removeLiquidity") (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))))) (Some "%tokenToToken")) None) None (or (pair (Comparable_type address) (pair (Comparable_type nat) (pair (Comparable_type mutez) (Comparable_type timestamp)))) (Some "%tokenToXtz") (pair (Comparable_type address) (pair (Comparable_type nat) (Comparable_type timestamp))) (Some "%xtzToToken")) None, None)) false (unit ::: pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address)))) ::: []) (pair (list operation) (pair (Comparable_type nat) (pair (Comparable_type mutez) (pair (Comparable_type nat) (pair (Comparable_type address) (Comparable_type address))))) ::: [])
We show that they are semantically equivalent.
ep_default_correct
: forall (env : proto_env) (p : data cpmm_definition.parameter_ep_default_ty)
(sto : data cpmm_definition.storage_ty) (ret_ops : Datatypes.list (data operation))
(ret_sto : data cpmm_definition.storage_ty),
eval0_seq_precond env cpmm_verification_ep_default.Def.ep_default
(fun x : stack (pair (list operation) cpmm_verification_ep_default.Def.storage_ty ::: []) =>
x = (ret_ops, ret_sto, tt)) (p, (sto, tt)) <->
cpmm_verification_ep_default.Spec.ep_default env p sto ret_ops ret_sto
The following invariant is sufficient to ensure that the CPMM will neither get stuck nor issue a division by zero.
Record arithmetic_invariant (sto : data cpmm_definition.storage_ty) : Prop := Build_arithmetic_invariant
{ token_pool_is_nonnegative : 0 < sto_tokenPool sto;
xtz_pool_is_nonnegative : 0 < mutez_to_nat (sto_xtzPool sto);
lqt_total_is_nonnegative : 0 < sto_lqtTotal sto;
product_lower_bound_inv : product_lower_bound sto }
where product_lower_bound is defined as follows:
product_lower_bound =
fun sto : data cpmm_definition.storage_ty =>
sto_lqtTotal sto * sto_lqtTotal sto <= sto_tokenPool sto * mutez_to_nat (sto_xtzPool sto)
: data cpmm_definition.storage_ty -> Prop
We show that each entrypoint preserves this invariant for all entrypoints except removeLiquidity.
addLiquidity_safe : forall env : env_ty, ep_addLiquidity_preserves_invariant envtokenToToken_safe : forall env : env_ty, ep_tokenToToken_preserves_invariant envxtzToToken_safe : forall env : env_ty, ep_xtzToToken_preserves_invariant envtokenToToken_safe : forall env : env_ty, ep_tokenToToken_preserves_invariant envtokenToXtz_safe : forall env : env_ty, ep_tokenToXtz_preserves_invariant env
Indeed, removeLiquidity needs an extra external hypothesis: nobody can empty the liquidity. This is guaranteed externally by an initial deposit assigned to the null address.
removeLiquidity_safe
: forall env : env_ty, ep_removeLiquidity_with_external_assumption_about_liquidity_removal_preserves_invariant env
where
ep_removeLiquidity_with_external_assumption_about_liquidity_removal_preserves_invariant = fun env : env_ty => forall p : comparable_data address * (N * (comparable_data mutez * (comparable_data nat * comparable_data timestamp))), ep_preserves_invariant (ep_removeLiquidity_with_external_assumption_about_liquidity_removal env p) arithmetic_invariant : env_ty -> Propep_removeLiquidity_with_external_assumption_about_liquidity_removal = fun (env : env_ty) (p : comparable_data address * (N * (comparable_data mutez * (comparable_data nat * comparable_data timestamp)))) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty) => let '(_, (lqt_burned, (_, (_, _)))) := p in lqt_burned < sto_lqtTotal sto /\ cpmm_spec.ep_removeLiquidity env p sto ops sto' : env_ty -> comparable_data address * (N * (comparable_data mutez * (comparable_data nat * comparable_data timestamp))) -> data cpmm_definition.storage_ty -> data (list operation) -> data cpmm_definition.storage_ty -> Prop
For each entrypoint, we show how the product of supplies evolves.
ep_addLiquidity_increases_product = fun env : env_ty => forall (p : data cpmm_definition.parameter_ep_addLiquidity_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), cpmm_spec.ep_addLiquidity env p sto ops sto' -> let X := mutez_to_nat (sto_xtzPool sto) in let X' := mutez_to_nat (sto_xtzPool sto') in let T := sto_tokenPool sto in let T' := sto_tokenPool sto' in let A := Z.to_N (tez.to_Z (amount env)) in X' * T' = (X + A) * (T + Nceiling (T * A) X) /\ X * T <= X' * T' : env_ty -> PropaddLiquidity_increases_product : forall env : env_ty, ep_addLiquidity_increases_product envep_removeLiquidity_decreases_product = fun env : env_ty => forall (p : data cpmm_definition.parameter_ep_removeLiquidity_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), cpmm_spec.ep_removeLiquidity env p sto ops sto' -> let X := mutez_to_nat (sto_xtzPool sto) in let X' := mutez_to_nat (sto_xtzPool sto') in let T := sto_tokenPool sto in let T' := sto_tokenPool sto' in let L := sto_lqtTotal sto in let (A, _) := snd p in X' * T' = (X - X * A / L) * (T - T * A / L) /\ X' * T' <= X * T : env_ty -> PropremoveLiquidity_decreases_product : forall env : env_ty, ep_removeLiquidity_decreases_product envep_xtzToToken_increases_product = fun env : env_ty => forall (p : data cpmm_definition.parameter_ep_xtzToToken_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> cpmm_spec.ep_xtzToToken env p sto ops sto' -> let X := mutez_to_nat (sto_xtzPool sto) in let X' := mutez_to_nat (sto_xtzPool sto') in let T := sto_tokenPool sto in let T' := sto_tokenPool sto' in let A := mutez_to_nat (amount env) in X' * T' = (X + A * 999 / 1000) * (T - A * 999 / 1000 * 999 * T / (X * 1000 + A * 999 / 1000 * 999)) /\ X * T <= X' * T' : env_ty -> PropxtzToToken_increases_product : forall env : env_ty, ep_xtzToToken_increases_product envep_tokenToXtz_increases_product = fun env : env_ty => forall (p : data cpmm_definition.parameter_ep_tokenToXtz_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), cpmm_spec.ep_tokenToXtz env p sto ops sto' -> let X := mutez_to_nat (sto_xtzPool sto) in let X' := mutez_to_nat (sto_xtzPool sto') in let T := sto_tokenPool sto in let T' := sto_tokenPool sto' in let (A, _) := snd p in X' * T' = (X - A * 999 * X / (T * 1000 + A * 999)) * (T + A) /\ X * T <= X' * T' : env_ty -> ProptokenToXtz_increases_product : forall env : env_ty, ep_tokenToXtz_increases_product envep_tokenToToken_increases_product = fun env : env_ty => forall (p : data cpmm_definition.parameter_ep_tokenToToken_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), cpmm_spec.ep_tokenToToken env p sto ops sto' -> let X := mutez_to_nat (sto_xtzPool sto) in let X' := mutez_to_nat (sto_xtzPool sto') in let T := sto_tokenPool sto in let T' := sto_tokenPool sto' in let A := fst (snd (snd (snd p))) in X' * T' = (X - A * 999 * X / (T * 1000 + A * 999)) * (T + A) /\ X * T <= X' * T' : env_ty -> ProptokenToToken_increases_product : forall env : env_ty, ep_tokenToToken_increases_product envep_default_increases_product = fun env : env_ty => forall (p : data cpmm_definition.parameter_ep_default_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), cpmm_spec.ep_default env p sto ops sto' -> let T := sto_tokenPool sto in let T' := sto_tokenPool sto' in let X := mutez_to_nat (sto_xtzPool sto) in let X' := mutez_to_nat (sto_xtzPool sto') in let A := mutez_to_nat (amount env) in T' * X' = T * (X + A) /\ T * X <= T' * X' : env_ty -> Propdefault_increases_product : forall env : env_ty, ep_default_increases_product env
We prove the following key property named "Ratio between Product and Squared Liquidity Increases" for all entrypoints.
ratio_product_squared_liquidity_increases = fun sto sto' : data cpmm_definition.storage_ty => ratio_product_squared_liquidity sto <= ratio_product_squared_liquidity sto' : data cpmm_definition.storage_ty -> data cpmm_definition.storage_ty -> PropaddLiquidity_ensures_rpsli : forall (env : cpmm_verification_ep_addLiquidity.Spec.env_ty) (p : data cpmm_definition.parameter_ep_addLiquidity_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> cpmm_verification_ep_addLiquidity.Spec.ep_addLiquidity env p sto ops sto' -> ratio_product_squared_liquidity_increases sto sto'removeLiquidity_ensures_rpsli : forall (env : cpmm_verification_ep_removeLiquidity.Spec.env_ty) (p : data cpmm_definition.parameter_ep_removeLiquidity_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> cpmm_verification_ep_removeLiquidity.Spec.ep_removeLiquidity env p sto ops sto' -> ratio_product_squared_liquidity_increases sto sto'xtzToToken_ensures_rpsli : forall (env : cpmm_verification_ep_xtzToToken.Spec.env_ty) (p : data cpmm_definition.parameter_ep_xtzToToken_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> cpmm_verification_ep_xtzToToken.Spec.ep_xtzToToken env p sto ops sto' -> ratio_product_squared_liquidity_increases sto sto'tokenToXtz_ensures_rpsli : forall (env : cpmm_verification_ep_tokenToXtz.Spec.env_ty) (p : data cpmm_definition.parameter_ep_tokenToXtz_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> cpmm_verification_ep_tokenToXtz.Spec.ep_tokenToXtz env p sto ops sto' -> ratio_product_squared_liquidity_increases sto sto'tokenToToken_ensures_rpsli : forall (env : Spec.env_ty) (p : data cpmm_definition.parameter_ep_tokenToToken_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> Spec.ep_tokenToToken env p sto ops sto' -> ratio_product_squared_liquidity_increases sto sto'default_ensures_rpsli : forall (env : cpmm_verification_ep_default.Spec.env_ty) (p : data cpmm_definition.parameter_ep_default_ty) (sto : data cpmm_definition.storage_ty) (ops : data (list operation)) (sto' : data cpmm_definition.storage_ty), invariant sto -> invariant sto' -> cpmm_verification_ep_default.Spec.ep_default env p sto ops sto' -> ratio_product_squared_liquidity_increases sto sto'