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_definition_manual.v.bak
(* Open Source License *)
(* Copyright (c) 2020 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 Import String ZArith.
Require Import syntax macros semantics comparable util typer.
Import error.
Require List.
Require tez.
Require map.
Require List.
Import List.ListNotations.
(*! Parameter type !*)
Definition parameter_ep_approve_ty : type :=
(pair (* %approve *) (address (* :spender *))
(pair (nat (* :allowance *))
(nat (* :currentAllowance *)))).
Definition parameter_ep_addLiquidity_ty : type :=
(pair (* %addLiquidity *) (pair (address (* :owner *))
(nat (* :minLqtMinted *)))
(pair (nat (* :maxTokensDeposited *))
(timestamp (* :deadline *)))).
Definition parameter_ep_removeLiquidity_ty : type :=
(pair (* %removeLiquidity *) (pair (address (* :owner *))
(pair (address (* :to_ *))
(nat (* :lqtBurned *))))
(pair
(mutez (* :minXtzWithdrawn *))
(pair
(nat (* :minTokensWithdrawn *))
(timestamp (* :deadline *))))).
Definition parameter_ep_xtzToToken_ty : type :=
(pair (* %xtzToToken *) (address (* :to_ *))
(pair (nat (* :minTokensBought *))
(timestamp (* :deadline *)))).
Definition parameter_ep_tokenToXtz_ty : type :=
(pair (* %tokenToXtz *) (pair (address (* :owner *))
(address (* :to_ *)))
(pair (nat (* :tokensSold *))
(pair (mutez (* :minXtzBought *))
(timestamp (* :deadline *))))).
Definition parameter_ep_tokenToToken_ty : type :=
(pair (* %tokenToToken *) (pair (address (* :outputDexterContract *))
(pair (nat (* :minTokensBought *))
(address (* :owner *))))
(pair (address (* :to *))
(pair (nat (* :tokensSold *))
(timestamp (* :deadline *))))).
Definition parameter_ep_updateTokenPool_ty : type :=
(nat (* %updateTokenPool *)).
Definition parameter_ep_setBaker_ty : type :=
(pair (* %setBaker *) (option key_hash)
bool).
Definition parameter_ep_default_ty : type :=
(unit (* %default *)).
Definition parameter_ty : type :=
(or (or (or parameter_ep_approve_ty None
parameter_ep_addLiquidity_ty None) None
(or parameter_ep_removeLiquidity_ty None
parameter_ep_xtzToToken_ty None) None) None
(or (or parameter_ep_tokenToXtz_ty None
parameter_ep_tokenToToken_ty None) None
(or parameter_ep_updateTokenPool_ty None
(or parameter_ep_setBaker_ty None
parameter_ep_default_ty None) None) None) None).
(*! Storage type !*)
Definition storage_ty : type :=
(pair (big_map (* %accounts *) address
(pair nat (* %balance *)
(map address (* %allowances *)
nat (* %allowance_amount *))))
(pair (pair bool (* %freeze_baker *)
nat (* %lqt_total *) )
(pair address (* %manager *)
(pair address (* %token_address *)
nat (* %token_pool *))))).
(*! Contract definition !*)
Definition self_info : self_info := (Some (parameter_ty, None)).
Module Dexter_definition (C:ContractContext).
(*
* (E:Env ST C).
*)
Module Semantics := Semantics C. Import Semantics.
Open Scope string_scope.
Definition DIG2 {self_info a b c SA}
: instruction self_info _ (a ::: b ::: c ::: SA) (c ::: a ::: b ::: SA) :=
DIG (S1 := a ::: b ::: nil) 2 eq_refl.
Definition DIG3 {self_info a b c d SA}
: instruction self_info _ (a ::: b ::: c ::: d ::: SA) (d ::: a ::: b ::: c ::: SA) :=
DIG (S1 := a ::: b ::: c ::: nil) 3 eq_refl.
Definition DIG4 {self_info a b c d e SA}
: instruction self_info _
(a ::: b ::: c ::: d ::: e ::: SA)
(e ::: a ::: b ::: c ::: d ::: SA) :=
DIG (S1 := a ::: b ::: c ::: d ::: nil) 4 eq_refl.
Definition DIG5 {self_info a b c d e f SA}
: instruction self_info _
(a ::: b ::: c ::: d ::: e ::: f ::: SA)
(f ::: a ::: b ::: c ::: d ::: e ::: SA) :=
DIG (S1 := a ::: b ::: c ::: d ::: e ::: nil) 5 eq_refl.
Definition ep_approve :
instruction
self_info _
(parameter_ep_approve_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil)
:= DIP1 ( DUP ) ;;
SWAP ;;
CAR ;;
SENDER ;;
GET (i := get_bigmap _ _) ;;
IF_NONE ( EMPTY_MAP address nat ;;
PUSH nat 0%N ;;
PAIR )
NOOP ;;
DUP ;;
CDR ;;
DIIP
( DUP ) ;;
DIG2 ;;
CAR ;;
GET ;;
IF_NONE ( PUSH nat 0%N )
NOOP ;;
DIIP
( DUP ) ;;
DIG2 ;;
CDR ;;
CDR ;;
COMPARE ;;
EQ ;;
IF NOOP
( PUSH string "Current allowance is not equal." ;;
FAILWITH ) ;;
DUP ;;
CDR ;;
DIG2 ;;
DUP ;;
CAR ;;
DIP1 ( CDR ;;
CAR ;;
SOME ) ;;
UPDATE (i := update_map _ _) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
DIP1 ( DUP ;;
CAR ) ;;
SOME ;;
SENDER ;;
UPDATE (i := update_bigmap _ _) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
SWAP ;;
DROP1 ;;
PAIR ;;
NIL operation ;;
PAIR.
Definition ep_addLiquidity : instruction
self_info _
(parameter_ep_addLiquidity_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
DUP ;;
CDR ;;
CDR ;;
NOW ;;
COMPARE ;;
LT ;;
IF NOOP
( PUSH string "addLiquidity: the current time must be less than the deadline." ;;
FAILWITH ) ;;
DUP ;;
CDR ;;
CAR ;;
PUSH nat 0%N ;;
COMPARE ;;
LT ;;
IF NOOP
( PUSH string "addLiquidity: maxTokensDeposited must be greater than zero." ;;
FAILWITH ) ;;
AMOUNT ;;
PUSH mutez (0 ~mutez) ;;
COMPARE ;;
LT ;;
IF NOOP
( PUSH string "addLiquidity: the amount of XTZ sent to the contract to be greater than zero." ;;
FAILWITH ) ;;
DIP1 ( DUP ) ;;
SWAP ;;
CDR ;;
CAR ;;
CDR ;;
INT ;;
EQ ;;
IF ( AMOUNT ;;
PUSH mutez (1000000 ~mutez) ;;
COMPARE ;;
LE ;;
IF NOOP
( PUSH string "addLiquidity: the initial liquidity amount must be greater than or equal to 1 XTZ." ;;
FAILWITH ) ;;
SWAP ;;
BALANCE ;;
DIP1 ( PUSH mutez (1 ~mutez) ) ;;
EDIV (s := ediv_tez_tez) ;;
IF_NONE ( PUSH string "" ;;
FAILWITH )
( CAR ) ;;
DUP ;;
DIP1 ( DIP1 ( DUP ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
PAIR ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR
) ;;
SWAP ;;
DIIP
( DUP ) ;;
DIG2 ;;
CAR ;;
CAR ;;
DIP1 ( DUP ;;
CAR ) ;;
GET (i := get_bigmap _ _) ;;
IF_NONE ( EMPTY_MAP address nat ;;
PUSH nat 0%N ;;
PAIR )
NOOP ;;
DIG2 ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
SWAP ;;
DROP1 ;;
PAIR ;;
DIP1 ( DUP ;;
CAR ) ;;
SOME ;;
DIIIP
( DUP ) ;;
DIG3 ;;
CAR ;;
CAR ;;
UPDATE (i := update_bigmap _ _) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
SWAP ;;
DROP1 ;;
PAIR ;;
DUP ;;
CDR ;;
CDR ;;
CDR ;;
CDR ;;
DIIP
( DUP ) ;;
DIG2 ;;
CDR ;;
CAR ;;
ADD ;;
DIP1 ( DUP ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
SWAP ;;
PAIR ;;
SWAP ;;
PAIR ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
DIP1 ( DUP ;;
CDR ;;
CAR ;;
DIP1 ( CAR ;;
CAR ) ) ;;
DUP ;;
CDR ;;
CDR ;;
CDR ;;
CAR ;;
CONTRACT (Some "transfer") (pair (pair address address) nat) ;;
IF_NONE ( FAILWITH )
NOOP ;;
PUSH mutez (0 ~mutez) ;;
DIG3 ;;
SELF (self_type := parameter_ty) (self_annot := None) None I ;;
ADDRESS ;;
DIG5 ;;
PAIR ;;
PAIR ;;
TRANSFER_TOKENS ;;
DIP1 ( NIL operation ) ;;
CONS ;;
PAIR )
( AMOUNT ;;
BALANCE ;;
SUB (s := sub_tez_tez ) ;;
DIP1 ( PUSH mutez (1 ~mutez) ) ;;
EDIV (s := ediv_tez_tez ) ;;
IF_NONE ( PUSH string "" ;;
FAILWITH )
( CAR ) ;;
AMOUNT ;;
DIP1 ( PUSH mutez (1 ~mutez) ) ;;
EDIV (s := ediv_tez_tez ) ;;
IF_NONE ( PUSH string "" ;;
FAILWITH )
( CAR ) ;;
DUP ;;
DIIIIP
( DUP ) ;;
DIG4 ;;
CDR ;;
CDR ;;
CDR ;;
CDR ;;
MUL ;;
DIIP
( DUP ) ;;
DIG2 ;;
SWAP ;;
EDIV ;;
IF_NONE ( FAILWITH )
( CAR ) ;;
SWAP ;;
DIIIIP
( DUP ) ;;
DIG4 ;;
CDR ;;
CAR ;;
CDR ;;
MUL ;;
DIP1 ( SWAP ) ;;
EDIV ;;
IF_NONE ( FAILWITH )
( CAR ) ;;
DIIP
( DUP ) ;;
DIG2 ;;
CAR ;;
CDR ;;
DIP1 ( DUP ) ;;
COMPARE ;;
LE ;;
IF NOOP
( PUSH string "addLiquidity: lqtMinted must be greater or equal to minLqtCreated." ;;
FAILWITH ) ;;
DIP1 ( DIP1 ( DUP ) ;;
SWAP ;;
CDR ;;
CAR ;;
DIP1 ( DUP ) ;;
COMPARE ;;
GE ;;
IF NOOP
( PUSH string "addLiquidity: maxTokensDeposited must be greater than or equal to tokens_deposited." ;;
FAILWITH ) ) ;;
DIIIP
( DUP ) ;;
DIG3 ;;
DIIIP
( DUP ) ;;
DIG3 ;;
CAR ;;
CAR ;;
DIP1 ( CAR ) ;;
GET (i := get_bigmap _ _) ;;
IF_NONE ( EMPTY_MAP address nat ;;
PUSH nat 0%N ;;
PAIR )
NOOP ;;
DUP ;;
CAR ;;
DIIP
( DUP ) ;;
DIG2 ;;
ADD ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
SWAP ;;
DROP1 ;;
PAIR ;;
SOME ;;
DIIIP
( DUP ) ;;
DIG3 ;;
CAR ;;
CAR ;;
DIP1 ( DIP1 ( DIG3 ;;
DUP ;;
CAR ) ) ;;
UPDATE (i := update_bigmap _ _) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
SWAP ;;
DROP1 ;;
PAIR ;;
DUP ;;
CDR ;;
CAR ;;
CDR ;;
DIG2 ;;
ADD ;;
DIP1 ( DUP ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
PAIR ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
DUP ;;
CDR ;;
CDR ;;
CDR ;;
CDR ;;
DIIP
( DUP ) ;;
DIG2 ;;
ADD ;;
DIP1 ( DUP ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
SWAP ;;
PAIR ;;
SWAP ;;
PAIR ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
DIP1 ( DIP1 ( CAR ;;
CAR ) ) ;;
DUP ;;
CDR ;;
CDR ;;
CDR ;;
CAR ;;
CONTRACT (Some "transfer") (pair (pair address address) nat) ;;
IF_NONE ( FAILWITH )
NOOP ;;
PUSH mutez (0 ~mutez) ;;
DIG3 ;;
SELF (self_type := parameter_ty) (self_annot := None) None I ;;
ADDRESS ;;
DIG5 ;;
PAIR ;;
PAIR ;;
TRANSFER_TOKENS ;;
DIP1 ( NIL operation ) ;;
CONS ;;
PAIR ).
Definition ep_removeLiquidity : instruction
self_info _
(parameter_ep_removeLiquidity_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
(* TODO: stub *)
DROP1 ;; NIL operation ;; PAIR.
Definition ep_xtzToToken : instruction
self_info _
(parameter_ep_xtzToToken_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
(* TODO: stub *)
DROP1 ;; NIL operation ;; PAIR.
Definition ep_tokenToXtz : instruction
self_info _
(parameter_ep_tokenToXtz_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
(* TODO: stub *)
DROP1 ;; NIL operation ;; PAIR.
Definition ep_updateTokenPool :
instruction
self_info _
(parameter_ep_updateTokenPool_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
DIP1 ( DUP ) ;;
SWAP ;;
CDR ;;
CDR ;;
CDR ;;
CAR ;;
SENDER ;;
COMPARE ;;
EQ ;;
IF NOOP
( PUSH string "Only the tokenAddress can update the tokenPool." ;;
FAILWITH ) ;;
DIP1 ( DUP ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
SWAP ;;
PAIR ;;
SWAP ;;
PAIR ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
NIL operation ;;
PAIR.
Definition ep_setBaker :
instruction
self_info _
(parameter_ep_setBaker_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil)
:= DIP1 ( DUP ) ;;
SWAP ;;
CDR ;;
CDR ;;
CAR ;;
SENDER ;;
COMPARE ;;
EQ ;;
IF NOOP
( PUSH string "Only the manager can set the baker." ;;
FAILWITH ) ;;
DIP1 ( DUP ) ;;
SWAP ;;
CDR ;;
CAR ;;
CAR ;;
NOT ;;
IF NOOP
( PUSH string "Cannot change the baker while freezeBaker is set to True." ;;
FAILWITH ) ;;
DUP ;;
CAR ;;
DIP1 ( CDR ) ;;
SET_DELEGATE ;;
DIP1 ( DIP1 ( DUP ;;
CDR ) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
DIP1 ( DUP ;;
DIP1 ( CDR ) ;;
CAR ) ;;
SWAP ;;
DROP1 ;;
PAIR ;;
PAIR ;;
DIP1 ( DUP ;;
DIP1 ( CAR ) ;;
CDR ) ;;
SWAP ;;
DROP1 ;;
SWAP ;;
PAIR ;;
NIL operation ) ;;
CONS ;;
PAIR.
Definition ep_tokenToToken : instruction
self_info _
(parameter_ep_tokenToToken_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
(* TODO: stub *)
DROP1 ;; NIL operation ;; PAIR.
Definition ep_default : instruction
self_info _
(parameter_ep_default_ty ::: storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
DROP1 ;; NIL operation ;; PAIR.
Definition main : instruction
self_info _
(pair parameter_ty storage_ty ::: nil)
(pair (list operation) storage_ty ::: nil) :=
(* TODO: there is no cast in mi-cho-coq, use NOOP instead *)
(*
* CAST (pair (or (or (or (pair address (pair nat nat)) (pair (pair address nat) (pair nat timestamp))) (or (pair (pair address (pair address nat)) (pair mutez (pair nat timestamp))) (pair address (pair nat timestamp)))) (or (or (pair (pair address address) (pair nat (pair mutez timestamp))) nat) (or (pair (option key_hash) bool) unit))) (pair (pair (big_map address (pair nat (map address nat))) (pair bool nat)) (pair address (pair address nat)))) ;;
*)
NOOP ;;
DUP ;;
CAR ;;
DIP1 ( CDR ) ;;
IF_LEFT ( IF_LEFT ( IF_LEFT ( ep_approve )
( ep_addLiquidity ) )
( IF_LEFT ( ep_removeLiquidity )
( ep_xtzToToken ) ) )
( IF_LEFT ( IF_LEFT ( ep_tokenToXtz )
( ep_tokenToToken ) )
( IF_LEFT ( ep_updateTokenPool )
( IF_LEFT ( ep_setBaker )
( ep_default ) ) ) ).
Definition dex_contract_file : contract_file :=
Mk_contract_file parameter_ty None storage_ty Datatypes.false main.
End Dexter_definition.
