diff --git a/Jenkinsfile b/Jenkinsfile index 177c1e93e..4812d92a0 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -21,7 +21,7 @@ pipeline { } } stage('Test') { - options { timeout(time: 15, unit: 'MINUTES') } + options { timeout(time: 30, unit: 'MINUTES') } parallel { stage('Unit') { steps { sh 'make test-unit -j8' } } stage('Symbolic') { steps { sh 'make test-symbolic -j2' } } @@ -31,7 +31,7 @@ pipeline { stage('Integration Proofs') { options { timeout(time: 180, unit: 'MINUTES') } stages { - stage('Audit Proofs') { steps { sh 'make dexter-prove lqt-prove lb-prove -j4' } } + stage('Audit Proofs') { steps { sh 'make dexter-prove lb-prove -j4' } } } } stage('Cross Test') { diff --git a/Makefile b/Makefile index 474db12c7..fde88e75b 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,7 @@ defn-k: defn-llvm defn-prove defn-symbolic defn-compat: defn-contract-expander defn-extractor defn-input-creator defn-output-compare build: build-k build-compat -build-k: build-llvm build-prove build-symbolic build-dexter build-lqt +build-k: build-llvm build-prove build-symbolic build-dexter build-lb build-lqt build-compat: build-contract-expander build-extractor build-input-creator build-output-compare # LLVM diff --git a/common.md b/common.md index 9720a9c50..04fdacf42 100644 --- a/common.md +++ b/common.md @@ -334,29 +334,7 @@ eleven 'anywhere' rules here. Michelson Internal Representation Conversion -------------------------------------------- -This function converts the `other_contracts` field into its internal -represetation. - -```k - syntax Map ::= #OtherContractsMapToKMap(OtherContractsMapEntryList) [function] - | #OtherContractsMapToKMap(String, Map, OtherContractsMapEntryList) [function] - // ---------------------------------------------------------------------------------------- - rule #OtherContractsMapToKMap( .OtherContractsMapEntryList ) => .Map - rule #OtherContractsMapToKMap( Contract A T ; Rs ) - => #OtherContractsMapToKMap(A, #BuildAnnotationMap(.FieldAnnotation, T), Rs) - - rule #OtherContractsMapToKMap(A, TypeMap, Rs) => - #BuildOtherContractsMap(#Address(A), TypeMap) #OtherContractsMapToKMap(Rs) - - syntax Map ::= #BuildOtherContractsMap(Address, Map) [function] - // ------------------------------------------------------------ - rule #BuildOtherContractsMap(A, FA:FieldAnnotation |-> T:TypeName TypeMap:Map) - => A . FA |-> T #BuildOtherContractsMap(A, TypeMap) - - rule #BuildOtherContractsMap(_, .Map) => .Map -``` - -This function converts all other datatypes into their internal represenations. +This function converts datatypes into their internal represenations. ```k syntax DataOrSeq ::= Data | DataList | MapEntryList // Can't subsort DataList to Data, as that would form a cycle. @@ -597,7 +575,7 @@ a contract lookup. => Transfer_tokens #MichelineToNative( P, - #Type({KnownAddrs [ #ParseEntrypoint(A) ]}:>TypeName), + #Type(#LookupEntrypoint(KnownAddrs, #ParseEntrypoint(A))), KnownAddrs, BigMaps ) @@ -605,8 +583,13 @@ a contract lookup. #ParseEntrypoint(A) N requires (isWildcard(N) orBool isInt(N)) - andBool #ParseEntrypoint(A) in_keys(KnownAddrs) andBool #IsLegalMutezValue(M) + + syntax TypeName ::= #LookupEntrypoint(Map, Entrypoint) [function] + // -------------------------------------------------------------- + rule #LookupEntrypoint(Entrypoints, A . FA) => { { Entrypoints [ A ] }:>Map [ FA ] }:>TypeName + requires A in_keys(Entrypoints) + andBool FA in_keys( { Entrypoints [ A ] }:>Map ) ``` We extract a `big_map` by index from the bigmaps map. Note that these have diff --git a/compat.md b/compat.md index 8554f342b..7ef8a8b3a 100644 --- a/compat.md +++ b/compat.md @@ -820,5 +820,12 @@ module OUTPUT-COMPARE _ => #OtherContractsMapToKMap(M) rule real_output AOS ; output EOS => #CheckOutput(EOS, AOS) ... + + syntax Map ::= #OtherContractsMapToKMap(OtherContractsMapEntryList) [function] + | #OtherContractsMapToKMap(String, Map, OtherContractsMapEntryList) [function] + // ---------------------------------------------------------------------------------------- + rule #OtherContractsMapToKMap( .OtherContractsMapEntryList ) => .Map + rule #OtherContractsMapToKMap( Contract A T ; Rs ) + => #Address(A) |-> #BuildAnnotationMap(.FieldAnnotation, T) #OtherContractsMapToKMap(Rs) endmodule ``` diff --git a/ext/k b/ext/k index bf17ff178..75dfe3096 160000 --- a/ext/k +++ b/ext/k @@ -1 +1 @@ -Subproject commit bf17ff178d90f47769f431bb08ae71e006286ded +Subproject commit 75dfe30969531069f5e0bec8e7841e1f24f962b7 diff --git a/michelson.md b/michelson.md index 3687af17c..6db9d2fea 100644 --- a/michelson.md +++ b/michelson.md @@ -40,13 +40,34 @@ the interpreter state so that we can execute Michelson code. We will see it's definition later. ```k -syntax KItem ::= "#Init" + syntax KItem ::= "#PreInit" | "#Init" ``` Here we declare our K-Michelson state configuration. We separate it into type (1)-(3) configuration cells as listed above. By convention, we nest all state cells inside a topmost cell, which we call ``. +```k + syntax AccountState ::= #Account(entrypoints : Map, + storagetype : MaybeType, + storagevalue : MaybeData, + balance : Mutez, + script : MaybeData) +``` + +This macro is convenient for writing proofs. + +```k + syntax Bool ::= #EntrypointExists(Map, Address, FieldAnnotation, Type) + // -------------------------------------------------------------------- + rule #EntrypointExists(Accounts, Address, FieldAnnot, EntrypointType) + => Address in_keys(Accounts) + andBool isAccountState( Accounts [ Address ] ) + andBool FieldAnnot in_keys(entrypoints({ Accounts [ Address ] }:>AccountState)) + andBool entrypoints({ Accounts [ Address ] }:>AccountState) [ FieldAnnot ] ==K #Name(EntrypointType) + [macro] +``` + ```k configuration @@ -60,18 +81,12 @@ The values of many of these cells are accessible via Michelson instructions. ```k #Timestamp(0) #ChainId(.Bytes) - .Map .Map - #Address("InvalidMyAddr") - .Map - .Type - + .Map - .Data - #Mutez(0) + #Address("TestContract") #Nonce(0) - .Data #Mutez(0) #Address("InvalidSourceAddr") @@ -96,7 +111,7 @@ These cells are used to initialize the test context. These cells store the Michelson interpreter runtime state. ```k - $PGM:Pgm ~> #Init + #PreInit ~> $PGM:Pgm ~> #Init (.Stack):InternalStack 111 false @@ -132,7 +147,7 @@ interpreter. | "#LoadContext" // ---------------------------- rule #SwapContext(NewCtxtName, NewCont) ~> Cont:K - => NewCont ~> #Init ~> #LoadContext + => #PreInit ~> NewCont ~> #Init ~> #LoadContext NoContext @@ -177,6 +192,15 @@ module MICHELSON Semantics Initialization ------------------------ +`#PreInit` fires before the program is loaded to prep the configuration structure for state loading. + +```k + rule #PreInit + => #InitContractMap + ... + +``` + `#Init` takes care of initialization. ```k @@ -193,6 +217,17 @@ Semantics Initialization ``` +### Initialize Contract Map + +```k + syntax KItem ::= "#InitContractMap" + rule #InitContractMap => . ... + + .Map => A |-> #Account(.Map, .Type, .Data, #Mutez(0), .Data) + + A +``` + ### Group Loading Below are the rules for loading specific groups. @@ -201,16 +236,32 @@ Below are the rules for loading specific groups. ```k rule parameter T:Type => .K ... - .Map => #BuildAnnotationMap(.FieldAnnotation, T) + A + + A |-> #Account(... entrypoints : .Map => #BuildAnnotationMap(.FieldAnnotation, T)) + ... + rule parameter FA:FieldAnnotation T:Type => .K ... - .Map => #BuildAnnotationMap(FA, T) + A + + A |-> #Account(... entrypoints : .Map => #BuildAnnotationMap(FA, T)) + ... + rule storage T => .K ... - .Type => T + A + + A |-> #Account(... storagetype : .Type => T) + ... + rule code C => .K ... - + A + + A |-> #Account(... script : .Data => C) + ... + rule G:Group ; Gs:Groups => G:Group ~> Gs ... ``` @@ -230,19 +281,37 @@ Below are the rules for loading specific groups. rule chain_id M => .K ... #ChainId(_ => M) - rule self A => .K ... - #Address("InvalidMyAddr" => A) - rule amount I => .K ... #Mutez(0 => I) requires #IsLegalMutezValue(I) rule balance I => .K ... - #Mutez(0 => I) + A + + A |-> #Account(... balance : #Mutez(0 => I)) + ... + requires #IsLegalMutezValue(I) - rule other_contracts { M } => .K ... - .Map => #OtherContractsMapToKMap(M) + // NOTE: This rule does not check whether a contract keyed by NewAddr already exists in the map + rule self NewAddr => .K ... + OldAddr => #Address(NewAddr) + + (OldAddr |-> A:AccountState) => #Address(NewAddr) |-> A + ... + + + // NOTE: These rules do not check whether a contract keyed by A already exists in the map + rule other_contracts { Contract A T ; OtherContracts } + => other_contracts { OtherContracts } + ... + + + (.Map => #Address(A) |-> #Account(#BuildAnnotationMap(.FieldAnnotation, T), .Type, .Data, #Mutez(0), .Data)) + ... + + + rule other_contracts { .OtherContractsMapEntryList } => . ... rule big_maps { M } => .K ... .Map => #BigMapsEntryListToKMap(M) @@ -315,7 +384,11 @@ The following unit test groups are not supported by the symbolic interpreter. ```k syntax KItem ::= "#EnsureLocalEntrypointsInitialized" rule #EnsureLocalEntrypointsInitialized => .K ... - LocalEntrypointMap => #AddDefaultEntry(LocalEntrypointMap, #Type(unit)) + CurrentContract + + CurrentContract |-> #Account(... entrypoints : E => #AddDefaultEntry(E, #Type(unit))) + ... + ``` ```k @@ -333,8 +406,12 @@ The following unit test groups are not supported by the symbolic interpreter. ```k syntax KItem ::= "#ConvertParamToNative" rule #ConvertParamToNative => .K ... - D:Data => #MichelineToNative(D, #Type({ LocalEntrypoints [ %default ] }:>TypeName), .Map, BigMaps) - LocalEntrypoints + CurrentContract + + CurrentContract |-> #Account(... entrypoints : E) + ... + + D:Data => #MichelineToNative(D, #Type({ E [ %default ] }:>TypeName), .Map, BigMaps) BigMaps rule #ConvertParamToNative => .K ... @@ -342,13 +419,20 @@ The following unit test groups are not supported by the symbolic interpreter. syntax KItem ::= "#ConvertStorageToNative" rule #ConvertStorageToNative => .K ... - D:Data => #MichelineToNative(D, #ConvertToType(T), .Map, BigMaps) - T => #ConvertToType(T) + CurrentContract + + CurrentContract |-> #Account(... storagetype : T => #ConvertToType(T), + storagevalue : D:Data => #MichelineToNative(D, #ConvertToType(T), .Map, BigMaps)) + ... + BigMaps rule #ConvertStorageToNative => .K ... - .Data - T => #ConvertToType(T) + CurrentContract + + CurrentContract |-> #Account(... storagetype : T => #ConvertToType(T), storagevalue : .Data) + ... + syntax Type ::= #ConvertToType(MaybeType) [function] rule #ConvertToType(.Type) => unit .AnnotationList @@ -426,15 +510,22 @@ version. syntax KItem ::= #StackToNative(StackElementList, Stack) // ----------------------------------------------------- rule #StackToNative(Stack_elt T D ; Stack, Stack') - => #StackToNative(Stack, [ #Name(T) #MichelineToNative(D, T, Addrs, BigMaps) ] ; Stack') + => #StackToNative(Stack, [ #Name(T) #MichelineToNative(D, T, #AccountStatesToEntrypoints(Contracts, .Map), BigMaps) ] ; Stack') ... - Addrs + Contracts BigMaps requires notBool isSymbolicData(D) rule #StackToNative(.StackElementList, Stack) => .K ... _ => reverseStack(Stack) + + syntax Map ::= #AccountStatesToEntrypoints(accountStates : Map, entrypoints : Map) [function, functional] + // ------------------------------------------------------------------------------------------------- + rule #AccountStatesToEntrypoints(A |-> #Account(... entrypoints : E) AccountStates, Entrypoints) + => #AccountStatesToEntrypoints(AccountStates, (A |-> E) Entrypoints) + + rule #AccountStatesToEntrypoints(.Map, Entrypoints) => Entrypoints ``` ```internalized-rl @@ -473,7 +564,11 @@ version. => #if Script ==K .Data #then {} #else Script #fi ... - + CurrentContract + + CurrentContract |-> #Account(... script : Script) + ... + ``` Execution Semantics @@ -1591,20 +1686,40 @@ These instructions push fresh `contract` literals on the stack corresponding to the given addresses/key hashes. ```k - syntax Instruction ::= CONTRACT(FieldAnnotation, TypeName) - rule CONTRACT AL:AnnotationList T:Type => CONTRACT(#GetFieldAnnot(AL), #Name(T)) ... + syntax Map ::= #GetEntrypoints(Address, accountsMap: Map) [function] + // ----------------------------------------------------------------- + rule #GetEntrypoints(A, Accounts) => entrypoints({Accounts[A]}:>AccountState) requires A in_keys(Accounts) [simplification, anywhere] +``` + +```k + syntax Instruction ::= CONTRACT(FieldAnnotation, TypeName, Map) + rule CONTRACT AL:AnnotationList T:Type + => #AssumeIsAccount(Accounts [ A ]) + ~> CONTRACT(#GetFieldAnnot(AL), #Name(T), #GetEntrypoints(A, Accounts)) + ... + + [address A:Address] ; _SS + Accounts + requires A in_keys(Accounts) + + rule CONTRACT _:AnnotationList T:Type => .K ... + [address A:Address] ; SS + => [option contract #Name(T) None] ; SS + + Accounts + requires notBool(A in_keys(Accounts)) - rule CONTRACT(FA, T) => . ... + rule CONTRACT(FA, T, Entrypoints) => . ... [address A:Address] ; SS => [option contract T Some #Contract(A . FA, T) ] ; SS - ContractMap - requires A . FA in_keys(ContractMap) - andBool ContractMap [ A . FA ] ==K T + requires FA in_keys(Entrypoints) andBool Entrypoints [ FA ] ==K T - rule CONTRACT(_FA, T) => . ... - [address _] ; SS => [option contract T None] ; SS - _ [owise] + rule CONTRACT(FA, T, Entrypoints) => . ... + [address _:Address] ; SS + => [option contract T None] ; SS + + requires notBool( FA in_keys(Entrypoints) andBool Entrypoints [ FA ] ==K T ) rule IMPLICIT_ACCOUNT _AL => . ... [key_hash #KeyHash(A)] ; SS @@ -1617,7 +1732,11 @@ These instructions push blockchain state on the stack. ```k rule BALANCE _A => . ... SS => [mutez B] ; SS - B + ADDR + + ADDR |-> #Account(... balance : B) + ... + rule ADDRESS _AL => . ... [contract T #Contract(A . _, T)] ; SS => [address A] ; SS @@ -1631,18 +1750,20 @@ These instructions push blockchain state on the stack. A syntax Instruction ::= SELF(FieldAnnotation) - rule SELF AL:AnnotationList => SELF(#GetFieldAnnot(AL)) ... + rule SELF AL:AnnotationList => #AssumeIsAccount(Accounts [ A ]) ~> SELF(#GetFieldAnnot(AL)) ... + A + + Accounts + rule SELF(FA) => .K ... SS - => [contract {LocalEntrypointMap [ FA ]}:>TypeName - #Contract(A . FA, {LocalEntrypointMap [ FA ]}:>TypeName)] + => [contract { entrypoints({Accounts[A]}:>AccountState)[ FA ] }:>TypeName + #Contract(A . FA, { entrypoints({Accounts[A]}:>AccountState)[ FA ] }:>TypeName)] ; SS - LocalEntrypointMap - A - ensures FA in_keys( LocalEntrypointMap ) - andBool isTypeName(LocalEntrypointMap [ FA ]) + A + Accounts rule AMOUNT _A => . ... SS => [mutez M] ; SS @@ -2002,16 +2123,16 @@ abstract out pieces of the stack which are non-invariant during loop execution. ) ... - KnownAddrs + Contracts BigMaps - requires #ConcreteMatch(ED, T, KnownAddrs, BigMaps, AD) + requires #ConcreteMatch(ED, T, #AccountStatesToEntrypoints(Contracts, .Map), BigMaps, AD) andBool TN ==K #Name(T) // NOTE: this function protects against unification errors syntax Bool ::= #ConcreteMatch(Data, Type, Map, Map, Data) [function] rule #ConcreteMatch(_:SymbolicData, _, _, _, _) => false rule #ConcreteMatch(ED, T, Addrs, BigMaps, AD) => #Matches(#MichelineToNative(ED,T,Addrs,BigMaps),AD) - requires notBool isSymbolicData(ED) + requires notBool isSymbolicData(ED) ``` ```k @@ -2424,7 +2545,7 @@ We implement fresh lambdas as fresh uninterpreted functions. requires isValue(ArgT, Arg) ``` -### `#AssumeHasType` +### `#AssumeHasType` and `#AssumeIsAccount` Michelson containers are parametric over a type. However, they are implemented in K as non-parametric containers such as `InternalList`, `Map` and `Set` that @@ -2444,6 +2565,20 @@ the item to be of the correct type. rule #AssumeHasType(E, T) => #Assume(E == #MakeFresh(#Type(T))) ... ``` +We need a similar construct for the `` map. + +```k + syntax KItem ::= #AssumeIsAccount(KItem) +``` + +```concrete + rule #AssumeIsAccount(_) => .K ... +``` + +```symbolic + rule #AssumeIsAccount(E) => #Assume(E ==K #Account(?_, ?_, ?_, ?_, ?_)) ... +``` + ```k endmodule ``` diff --git a/tests/proofs/dexter/dexter-spec.md b/tests/proofs/dexter/dexter-spec.md index 31ed7a5d8..6ddc3baf5 100644 --- a/tests/proofs/dexter/dexter-spec.md +++ b/tests/proofs/dexter/dexter-spec.md @@ -70,7 +70,7 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for false #Timestamp(CurrentTime) #Mutez(Amount) - SelfAddress + SelfAddress OldLqt => OldLqt +Int (Amount *Int OldLqt) /Int XtzAmount #Mutez(XtzAmount => XtzAmount +Int Amount) TokenAmount => TokenAmount +Int #ceildiv(Amount *Int TokenAmount, XtzAmount) @@ -79,8 +79,7 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 2) - KnownAddresses - LocalEntrypoints + Accounts _ => [ Transfer_tokens #TokenTransferData(IsFA2, Sender, SelfAddress, TokenId, #ceildiv(Amount *Int TokenAmount, XtzAmount)) #Mutez(0) TokenAddress . %transfer Nonce ] ;; [ Transfer_tokens Pair ((Amount *Int OldLqt) /Int XtzAmount) Owner #Mutez(0) LqtAddress . %mintOrBurn (Nonce +Int 1) ] ;; @@ -93,10 +92,10 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for andBool MinLqtMinted <=Int (Amount *Int OldLqt) /Int XtzAmount andBool #IsLegalMutezValue(Amount +Int XtzAmount) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -105,7 +104,7 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for IsUpdating #Timestamp(CurrentTime) #Mutez(Amount) - SelfAddress + SelfAddress OldLqt => OldLqt +Int (Amount *Int OldLqt) /Int XtzAmount #Mutez(XtzAmount => XtzAmount +Int Amount) TokenAmount => TokenAmount +Int #ceildiv(Amount *Int TokenAmount, XtzAmount) @@ -114,8 +113,7 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 2) - KnownAddresses - LocalEntrypoints + Accounts _ => [ Transfer_tokens #TokenTransferData(IsFA2, Sender, SelfAddress, TokenId, #ceildiv(Amount *Int TokenAmount, XtzAmount)) #Mutez(0) TokenAddress . %transfer Nonce ] ;; [ Transfer_tokens Pair ((Amount *Int OldLqt) /Int XtzAmount) Owner #Mutez(0) LqtAddress . %mintOrBurn (Nonce +Int 1) ] ;; @@ -129,10 +127,10 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for andBool XtzAmount >Int 0 andBool (Amount *Int TokenAmount) %Int XtzAmount =/=Int 0 - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -165,12 +163,37 @@ module DEXTER-ADDLIQUIDITY-NEGATIVE-SPEC requires notBool IsFA2 andBool ( IsUpdating orBool CurrentTime >=Int Deadline - orBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited orBool notBool #IsLegalMutezValue(Amount +Int XtzAmount) orBool XtzAmount ==Int 0 orBool MinLqtMinted >Int (Amount *Int OldLqt) /Int XtzAmount ) + claim #runProof(IsFA2, AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + IsUpdating + #Timestamp(CurrentTime) + #Mutez(Amount) + OldLqt + #Mutez(XtzAmount) + TokenAmount + requires notBool IsFA2 + andBool XtzAmount >Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited + andBool #mod(Amount *Int TokenAmount, XtzAmount) ==Int 0 + + claim #runProof(IsFA2, AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + IsUpdating + #Timestamp(CurrentTime) + #Mutez(Amount) + OldLqt + #Mutez(XtzAmount) + TokenAmount + requires notBool IsFA2 + andBool XtzAmount >Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited + andBool #mod(Amount *Int TokenAmount, XtzAmount) =/=Int 0 + claim #runProof(IsFA2, AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) .Stack => ?_:FailedStack IsUpdating @@ -182,14 +205,37 @@ module DEXTER-ADDLIQUIDITY-NEGATIVE-SPEC requires IsFA2 andBool ( IsUpdating orBool CurrentTime >=Int Deadline - orBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited orBool notBool #IsLegalMutezValue(Amount +Int XtzAmount) - orBool MinLqtMinted >Int (Amount *Int OldLqt) /Int XtzAmount orBool XtzAmount ==Int 0 + orBool MinLqtMinted >Int (Amount *Int OldLqt) /Int XtzAmount ) -``` -TODO: Deal with the case when the token contract or the liquidity token contract don't exist or have the wrong type. + claim #runProof(IsFA2, AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + IsUpdating + #Timestamp(CurrentTime) + #Mutez(Amount) + OldLqt + #Mutez(XtzAmount) + TokenAmount + requires IsFA2 + andBool XtzAmount >Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited + andBool #mod(Amount *Int TokenAmount, XtzAmount) ==Int 0 + + claim #runProof(IsFA2, AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + IsUpdating + #Timestamp(CurrentTime) + #Mutez(Amount) + OldLqt + #Mutez(XtzAmount) + TokenAmount + requires IsFA2 + andBool XtzAmount >Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited + andBool #mod(Amount *Int TokenAmount, XtzAmount) =/=Int 0 +``` ```k endmodule @@ -217,7 +263,7 @@ module DEXTER-REMOVELIQUIDITY-POSITIVE-SPEC false #Timestamp(CurrentTime) #Mutez(0) - SelfAddress + SelfAddress OldLqt => OldLqt -Int LqtBurned #Mutez(XtzAmount => XtzAmount -Int (LqtBurned *Int XtzAmount) /Int OldLqt) TokenAmount => TokenAmount -Int (LqtBurned *Int TokenAmount) /Int OldLqt @@ -226,8 +272,7 @@ module DEXTER-REMOVELIQUIDITY-POSITIVE-SPEC LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 3) - KnownAddresses - LocalEntrypoints // 1027 + Accounts _ => [ Transfer_tokens (Pair (0 -Int LqtBurned) Sender) #Mutez(0) LqtAddress . %mintOrBurn Nonce ] ;; [ Transfer_tokens #TokenTransferData(IsFA2, SelfAddress, To, TokenId, (LqtBurned *Int TokenAmount) /Int OldLqt) #Mutez(0) TokenAddress . %transfer (Nonce +Int 1) ] ;; @@ -239,11 +284,11 @@ module DEXTER-REMOVELIQUIDITY-POSITIVE-SPEC andBool OldLqt >=Int LqtBurned andBool MinXtzWithdrawn <=Int (LqtBurned *Int XtzAmount) /Int OldLqt andBool MinTokensWithdrawn <=Int (LqtBurned *Int TokenAmount) /Int OldLqt - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) - andBool #EntrypointExists(KnownAddresses, To, %default, unit) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, To, %default, unit) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) andBool #IsLegalMutezValue(XtzAmount) andBool #IsLegalMutezValue((LqtBurned *Int XtzAmount) /Int OldLqt) @@ -437,28 +482,23 @@ The contract queries its underlying token contract for its own token balance if 4. if we are running the FA2 version of Dexter, then check that the contract at address `storage.tokenAddress` has a well-typed FA2 `balance_of` entrypoint; otherwise, check that the contract at address `storage.tokenAddress` has a well-typed FA12 `get_balance` entrypoint. -- TODO: Generalize the Michelson `SELF` and `CONTRACT` instructions to properly use annotations. - That way, we can use the actual, full #DexterParamType in the `paramtype` cell, and in the `KnownAddresses` map. - Right now, we need to pretend to have a more specialized type. - ```k claim #runProof(IsFA2, UpdateTokenPool) => . .Stack false => true TokenAddress:Address TokenId - SelfAddress + SelfAddress #Mutez(Amount) Sender Sender - LocalEntrypoints - KnownAddresses + Accounts _ => [ Transfer_tokens Pair #UpdateTokenPoolTransferFrom(IsFA2, SelfAddress, TokenId) #Contract(SelfAddress . %updateTokenPoolInternal, #DexterVersionSpecificParamType(IsFA2)) #Mutez(0) #TokenBalanceEntrypoint(TokenAddress, IsFA2) O ] ;; .InternalList #Nonce(O) => #Nonce(O +Int 1) requires Amount ==Int 0 - andBool #EntrypointExists(KnownAddresses, TokenAddress, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` If any of the conditions are not satisfied, the call fails. @@ -472,15 +512,15 @@ NOTE: The failure conditions are split into two claims with identical configurat #Mutez(Amount) Sender Source - LocalEntrypoints - KnownAddresses + SelfAddress + Accounts requires ( Amount >Int 0 - orBool (notBool #EntrypointExists(KnownAddresses, TokenAddress, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2))) + orBool (notBool #EntrypointExists(Accounts, TokenAddress, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2))) orBool IsUpdating orBool Sender =/=K Source ) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -695,10 +735,9 @@ A buyer sends tokens to the Dexter contract and receives a corresponding amount TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - LocalEntrypoints - SelfAddress:Address + Accounts + SelfAddress:Address #Nonce(N => N +Int 2) - KnownAddresses TokenID _ => [ Transfer_tokens #TokenTransferData(IsFA2, Sender, SelfAddress, TokenID, TokensSold) #Mutez(0) TokenAddress . %transfer N ] @@ -716,10 +755,10 @@ A buyer sends tokens to the Dexter contract and receives a corresponding amount andBool #IsLegalMutezValue(MinXtzBought) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) andBool #IsLegalMutezValue(XtzPool:Int -Int #CurrencyBought (XtzPool:Int, TokenPool:Int, TokensSold:Int)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, To, #token("%default", "FieldAnnotation"), #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -734,7 +773,7 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-1-SPEC #Timestamp(CurrentTime) #Mutez(Amount) _TokenAddress:Address - _LocalEntrypoints + _Accounts requires notBool IsFA2 andBool ( IsUpdating orBool notBool Amount ==Int 0 @@ -754,15 +793,16 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-2-SPEC TokenAddress:Address #Mutez(_XtzPool) TokenPool - LocalEntrypoints + Accounts + SelfAddress requires notBool IsFA2 andBool notBool IsUpdating andBool notBool Amount ==Int 0 andBool notBool CurrentTime Int 0 orBool TokensSold >Int 0) endmodule ``` @@ -778,15 +818,16 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-3-SPEC TokenAddress:Address #Mutez(XtzPool) TokenPool - LocalEntrypoints + Accounts + SelfAddress requires notBool IsFA2 andBool notBool IsUpdating andBool notBool Amount ==Int 0 andBool notBool CurrentTime =Int MinXtzBought andBool #IsLegalMutezValue(MinXtzBought) ) @@ -804,15 +845,16 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-4-SPEC TokenAddress:Address #Mutez(XtzPool) TokenPool - LocalEntrypoints + Accounts + SelfAddress requires notBool IsFA2 andBool notBool IsUpdating andBool notBool Amount ==Int 0 andBool notBool CurrentTime =Int MinXtzBought andBool #IsLegalMutezValue(MinXtzBought) andBool notBool( #CurrencyBought(XtzPool, TokenPool, TokensSold) <=Int XtzPool @@ -847,10 +889,9 @@ As before, a buyer sends tokens to the Dexter contract and receives a correspond TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - LocalEntrypoints - SelfAddress:Address + Accounts + SelfAddress:Address #Nonce(N => N +Int 2) - KnownAddresses TokenID _ => [ Transfer_tokens #TokenTransferData(IsFA2, Sender, SelfAddress, TokenID, TokensSold) #Mutez(0) TokenAddress . %transfer N ] @@ -868,10 +909,10 @@ As before, a buyer sends tokens to the Dexter contract and receives a correspond andBool #IsLegalMutezValue(MinXtzBought) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) andBool #IsLegalMutezValue(XtzPool:Int -Int #CurrencyBought (XtzPool:Int, TokenPool:Int, TokensSold:Int)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, To, #token("%default", "FieldAnnotation"), #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -885,7 +926,7 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-1-SPEC IsUpdating #Mutez(Amount) #Timestamp(CurrentTime) - _LocalEntrypoints + _Accounts requires IsFA2 andBool ( IsUpdating orBool notBool Amount ==Int 0 @@ -902,11 +943,11 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-2-SPEC IsUpdating #Mutez(Amount) #Timestamp(CurrentTime) - LocalEntrypoints + Accounts + SelfAddress TokenPool #Mutez(XtzPool) TokenAddress:Address - KnownAddresses requires IsFA2 andBool notBool IsUpdating andBool Amount ==Int 0 @@ -919,10 +960,10 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-2-SPEC andBool #IsLegalMutezValue(MinXtzBought) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) andBool #IsLegalMutezValue(XtzPool:Int -Int #CurrencyBought (XtzPool:Int, TokenPool:Int, TokensSold:Int)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, To, #token("%default", "FieldAnnotation"), #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -934,11 +975,11 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-3-SPEC IsUpdating #Mutez(Amount) #Timestamp(CurrentTime) - LocalEntrypoints + Accounts + SelfAddress TokenPool #Mutez(XtzPool) TokenAddress:Address - KnownAddresses #Nonce(_N => ?_) requires IsFA2 andBool notBool IsUpdating @@ -952,10 +993,10 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-3-SPEC andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) andBool #IsLegalMutezValue(XtzPool:Int -Int #CurrencyBought (XtzPool:Int, TokenPool:Int, TokensSold:Int)) ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, To, #token("%default", "FieldAnnotation"), #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -978,17 +1019,16 @@ module DEXTER-XTZTOTOKEN-FA12-POSITIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(To, MinTokensBought, #Timestamp(Deadline))) => . .Stack - LocalEntrypoints + Accounts IsUpdating #Mutez(Amount) TokenAddress #Mutez(XtzPool => XtzPool +Int Amount) TokenPool => TokenPool -Int #CurrencyBought(TokenPool, XtzPool, Amount) #Timestamp(CurrentTime) - SelfAddress + SelfAddress #Nonce(N => N +Int 1) TokenID - KnownAddresses _ => [ Transfer_tokens #TokenTransferData(IsFA2, SelfAddress, To, TokenID, #CurrencyBought(TokenPool, XtzPool, Amount)) #Mutez(0) TokenAddress . %transfer N ] ;; .InternalList @@ -1002,9 +1042,9 @@ module DEXTER-XTZTOTOKEN-FA12-POSITIVE-SPEC andBool TokenPool -Int #CurrencyBought ( TokenPool , XtzPool , Amount ) >=Int 0 andBool #IsLegalMutezValue(XtzPool +Int Amount) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -1013,14 +1053,14 @@ module DEXTER-XTZTOTOKEN-FA12-NEGATIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(_To, MinTokensBought, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) .Stack => ?_:FailedStack - LocalEntrypoints + Accounts + SelfAddress IsUpdating #Mutez(Amount) TokenAddress #Mutez(XtzPool) TokenPool #Timestamp(CurrentTime) - KnownAddresses _ requires notBool IsFA2 andBool notBool ( notBool IsUpdating @@ -1031,9 +1071,9 @@ module DEXTER-XTZTOTOKEN-FA12-NEGATIVE-SPEC andBool TokenPool -Int #CurrencyBought ( TokenPool , XtzPool , Amount ) >=Int 0 andBool #IsLegalMutezValue(XtzPool +Int Amount) ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -1042,17 +1082,16 @@ module DEXTER-XTZTOTOKEN-FA2-POSITIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(To, MinTokensBought, #Timestamp(Deadline))) => . .Stack - LocalEntrypoints + Accounts IsUpdating #Mutez(Amount) TokenAddress #Mutez(XtzPool => XtzPool +Int Amount) TokenPool => TokenPool -Int #CurrencyBought(TokenPool, XtzPool, Amount) #Timestamp(CurrentTime) - SelfAddress + SelfAddress #Nonce(N => N +Int 1) TokenID - KnownAddresses _ => [ Transfer_tokens #TokenTransferData(IsFA2, SelfAddress, To, TokenID, #CurrencyBought(TokenPool, XtzPool, Amount)) #Mutez(0) TokenAddress . %transfer N ] ;; .InternalList @@ -1066,9 +1105,9 @@ module DEXTER-XTZTOTOKEN-FA2-POSITIVE-SPEC andBool TokenPool -Int #CurrencyBought ( TokenPool , XtzPool , Amount ) >=Int 0 andBool #IsLegalMutezValue(XtzPool +Int Amount) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -1077,14 +1116,14 @@ module DEXTER-XTZTOTOKEN-FA2-NEGATIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(_To, MinTokensBought, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) .Stack => ?_:FailedStack - LocalEntrypoints + Accounts + SelfAddress IsUpdating #Mutez(Amount) TokenAddress #Mutez(XtzPool) TokenPool #Timestamp(CurrentTime) - KnownAddresses _ requires IsFA2 andBool notBool ( notBool IsUpdating @@ -1095,9 +1134,9 @@ module DEXTER-XTZTOTOKEN-FA2-NEGATIVE-SPEC andBool TokenPool -Int #CurrencyBought ( TokenPool , XtzPool , Amount ) >=Int 0 andBool #IsLegalMutezValue(XtzPool +Int Amount) ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -1127,11 +1166,10 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - SelfAddress - LocalEntrypoints + SelfAddress + Accounts #Nonce(N => N +Int 2) TokenID - KnownAddresses _ => [ Transfer_tokens #TokenTransferData(IsFA2, Sender, SelfAddress, TokenID, TokensSold) #Mutez(0) TokenAddress . %transfer N ] ;; [ Transfer_tokens Pair To Pair MinTokensBought #Timestamp(Deadline) #Mutez(#CurrencyBought(XtzPool, TokenPool, TokensSold)) OutputDexterContract . %xtzToToken (N +Int 1)] @@ -1144,10 +1182,10 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed andBool #CurrencyBought(XtzPool, TokenPool, TokensSold) <=Int XtzPool andBool (TokenPool >Int 0 orBool TokensSold >Int 0) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -1160,11 +1198,10 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - SelfAddress - LocalEntrypoints + SelfAddress + Accounts #Nonce(N => N +Int 2) TokenID - KnownAddresses _ => [ Transfer_tokens #TokenTransferData(IsFA2, Sender, SelfAddress, TokenID, TokensSold) #Mutez(0) TokenAddress . %transfer N ] ;; [ Transfer_tokens Pair To Pair MinTokensBought #Timestamp(Deadline) #Mutez(#CurrencyBought(XtzPool, TokenPool, TokensSold)) OutputDexterContract . %xtzToToken (N +Int 1)] @@ -1177,10 +1214,10 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed andBool #CurrencyBought(XtzPool, TokenPool, TokensSold) <=Int XtzPool andBool (TokenPool >Int 0 orBool TokensSold >Int 0) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -1204,11 +1241,10 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC TokenPool #Timestamp(CurrentTime) _Sender - _SelfAddress - LocalEntrypoints + SelfAddress + Accounts #Nonce(_N => ?_) _TokenID - KnownAddresses _ requires notBool IsFA2 andBool notBool( notBool SelfIsUpdating @@ -1218,10 +1254,10 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC andBool (TokenPool >Int 0 orBool TokensSold >Int 0) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -1236,11 +1272,10 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC TokenPool #Timestamp(CurrentTime) _Sender - _SelfAddress - LocalEntrypoints + SelfAddress + Accounts #Nonce(_N => ?_) _TokenID - KnownAddresses _ requires IsFA2 andBool notBool( notBool SelfIsUpdating @@ -1250,10 +1285,10 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC andBool (TokenPool >Int 0 orBool TokensSold >Int 0) andBool #IsLegalMutezValue(#CurrencyBought(XtzPool, TokenPool, TokensSold)) ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType(IsFA2)) - andBool #EntrypointExists(KnownAddresses, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) - andBool #LocalEntrypointExists(LocalEntrypoints, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType(IsFA2)) + andBool #EntrypointExists(Accounts, OutputDexterContract, %xtzToToken, pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) + andBool #EntrypointExists(Accounts, SelfAddress, %updateTokenPoolInternal, #Type(#DexterVersionSpecificParamType(IsFA2))) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k diff --git a/tests/proofs/dexter/dexter.md b/tests/proofs/dexter/dexter.md index 8dd60d150..088ec6fcf 100644 --- a/tests/proofs/dexter/dexter.md +++ b/tests/proofs/dexter/dexter.md @@ -33,8 +33,10 @@ module DEXTER-LEMMAS ``` ```k - rule X /Int 1 => X [simplification] - rule X *Int 1 => X [simplification] + rule X /Int 1 => X [simplification] + rule X *Int 1 => X [simplification] + rule false orBool @B:Bool => @B [simplification] + rule @B:Bool orBool false => @B [simplification] ``` ```k @@ -590,14 +592,6 @@ If the contract execution fails, storage is not updated. rule #TokenBalanceEntrypointType(false) => #Type(pair address (contract nat)) rule #TokenBalanceEntrypointType(true) => #Type(pair (list (pair address nat)) (contract (list (pair (pair (address) nat) nat)))) - syntax Int ::= #ceildiv (Int, Int) [function] - | #ceildivAux(Int, Int) [function, functional] - // --------------------------------------------------------- - rule #ceildiv (X, Y) => #ceildivAux(X, Y) requires Y =/=Int 0 - rule #ceildivAux(_, Y) => 0 requires Y ==Int 0 - rule #ceildivAux(X, Y) => X /Int Y requires Y =/=Int 0 andBool X %Int Y ==Int 0 - rule #ceildivAux(X, Y) => X /Int Y +Int 1 requires Y =/=Int 0 andBool notBool X %Int Y ==Int 0 - syntax Int ::= #CurrencyBought(Int, Int, Int) [function, functional, smtlib(xtzbought), no-evaluators] // ---------------------------------------------------------------------------------------------------- rule (ToSellAmt *Int 997 *Int ToBuyCurrencyTotal) /Int (ToSellCurrencyTotal *Int 1000 +Int (ToSellAmt *Int 997)) @@ -605,33 +599,25 @@ If the contract execution fails, storage is not updated. [simplification] ``` -```k - syntax Bool ::= #EntrypointExists(Map, Address, FieldAnnotation, Type) -// --------------------------------------------------------------------- - rule #EntrypointExists(KnownAddresses, Addr, FieldAnnot, EntrypointType) - => Addr . FieldAnnot in_keys(KnownAddresses) andBool - KnownAddresses[Addr . FieldAnnot] ==K #Name(EntrypointType) - [macro] - - syntax Bool ::= #LocalEntrypointExists(Map, FieldAnnotation, Type) - // ---------------------------------------------------------------- - rule #LocalEntrypointExists(LocalEntrypoints, FieldAnnot, EntrypointType) - => FieldAnnot in_keys(LocalEntrypoints) andBool - LocalEntrypoints[FieldAnnot] ==K #Name(EntrypointType) - [macro] -``` - ### Avoiding Interpreting Functions If a function value does not play well with the prover or SMT solver, it can be rewritten to `#uninterpreted`. This function has no evaluation rules, so the prover can make no assumptions about it -- it will be assumed it can take on any value. ```k - syntax Int ::= #mulMod(Int, Int, Int) [function, functional, smtlib(mulMod), no-evaluators] + syntax Int ::= #mod(Int, Int) [function, functional, smtlib(mulMod), no-evaluators] | #mulDiv(Int, Int, Int) [function, functional, smtlib(mulDiv), no-evaluators] // ----------------------------------------------------------------------------------------- - rule (X *Int Y) %Int Z => #mulMod(X, Y, Z) [simplification] + rule X %Int Y => #mod(X, Y) [simplification] rule (X *Int Y) /Int Z => #mulDiv(X, Y, Z) [simplification] + + syntax Int ::= #ceildiv (Int, Int) [function] + | #ceildivAux(Int, Int) [function, functional] + // --------------------------------------------------------- + rule #ceildiv (X, Y) => #ceildivAux(X, Y) requires Y =/=Int 0 + rule #ceildivAux(_, Y) => 0 requires Y ==Int 0 + rule #ceildivAux(X, Y) => X /Int Y requires Y =/=Int 0 andBool #mod(X, Y) ==Int 0 + rule #ceildivAux(X, Y) => X /Int Y +Int 1 requires Y =/=Int 0 andBool notBool #mod(X, Y) ==Int 0 ``` ## Putting It All Together diff --git a/tests/proofs/entrypoints-spec.k b/tests/proofs/entrypoints-spec.k new file mode 100644 index 000000000..2f790d051 --- /dev/null +++ b/tests/proofs/entrypoints-spec.k @@ -0,0 +1,64 @@ +requires "../../michelson.md" + +module VERIFICATION + imports MICHELSON +endmodule + +module ENTRYPOINTS-SPEC + imports VERIFICATION + + claim SELF .AnnotationList => . + .Stack => [ contract unit #Contract( SelfAddr . %default, unit ) ] ; .Stack + Accounts + SelfAddr + requires #EntrypointExists(Accounts, SelfAddr, %default, unit .AnnotationList) + + // contract_00, contract_04: Expected contract exists + claim (CONTRACT .AnnotationList #Type(unit)) => .K + [ address #Address(Addr) ] ; .Stack + => [ (option contract unit) Some #Contract( #Address(Addr) . %default, unit ) ] ; .Stack + + Accounts + requires #EntrypointExists(Accounts, #Address(Addr), %default, unit .AnnotationList) + + // contract_01, contract_05: contract does not exist + claim (CONTRACT .AnnotationList #Type(unit)) => .K + [ address #Address(Addr) ] ; .Stack + => [ (option contract unit) None ] ; .Stack + + Accounts + requires notBool #Address(Addr) in_keys(Accounts) + + // contract_03: Contract has different type + claim (CONTRACT .AnnotationList #Type(unit)) => .K + [ address #Address(Addr) ] ; .Stack + => [ (option contract unit) None ] ; .Stack + + Accounts + requires #EntrypointExists(Accounts, #Address(Addr), %default, nat .AnnotationList) + + // contract_06: Non-default entrypoint + claim (CONTRACT #token("%foo" , "FieldAnnotation") .AnnotationList #Type(unit)) => .K + [ address #Address(Addr) ] ; .Stack + => [ (option contract unit) Some #Contract( #Address(Addr) . #token("%foo", "FieldAnnotation"), unit ) ] ; .Stack + + Accounts + requires #EntrypointExists(Accounts, #Address(Addr), #token("%foo", "FieldAnnotation"), unit .AnnotationList) + + // contract_07: Wrong entry point + claim (CONTRACT #token("%baz" , "FieldAnnotation") .AnnotationList #Type(nat)) => .K + [ address #Address(Addr) ] ; .Stack + => [ (option contract nat) None ] ; .Stack + + Accounts + requires notBool #EntrypointExists(Accounts, #Address(Addr), #token("%baz", "FieldAnnotation"), nat .AnnotationList) + + // contract_08: Non-unit type + claim (CONTRACT .AnnotationList #Type(nat)) => .K + [ address #Address(Addr) ] ; .Stack + => [ (option contract nat) Some #Contract( #Address(Addr) . %default, nat ) ] ; .Stack + + Accounts + requires #EntrypointExists(Accounts, #Address(Addr), %default, nat .AnnotationList) + +endmodule diff --git a/tests/proofs/liquidity-baking/lb-spec.md b/tests/proofs/liquidity-baking/lb-spec.md index d3260d73c..0a44c1cf5 100644 --- a/tests/proofs/liquidity-baking/lb-spec.md +++ b/tests/proofs/liquidity-baking/lb-spec.md @@ -62,7 +62,7 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for .Stack #Timestamp(CurrentTime) #Mutez(Amount) - SelfAddress + SelfAddress OldLqt => OldLqt +Int (Amount *Int OldLqt) /Int XtzAmount #Mutez(XtzAmount => XtzAmount +Int Amount) TokenAmount => TokenAmount +Int #ceildiv(Amount *Int TokenAmount, XtzAmount) @@ -70,8 +70,7 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 2) - KnownAddresses - LocalEntrypoints + Accounts _ => [ Transfer_tokens #TokenTransferData(Sender, SelfAddress, #ceildiv(Amount *Int TokenAmount, XtzAmount)) #Mutez(0) TokenAddress . %transfer Nonce ] ;; [ Transfer_tokens Pair ((Amount *Int OldLqt) /Int XtzAmount) Owner #Mutez(0) LqtAddress . %mintOrBurn (Nonce +Int 1) ] ;; @@ -82,12 +81,43 @@ We have one case for when `#ceildiv` results in an upwards rounding, and one for andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) <=Int MaxTokensDeposited andBool MinLqtMinted <=Int (Amount *Int OldLqt) /Int XtzAmount andBool #IsLegalMutezValue(Amount +Int XtzAmount) + andBool (Amount *Int TokenAmount) %Int XtzAmount ==Int 0 - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) + + claim #runProof(AddLiquidity(Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => . + .Stack + #Timestamp(CurrentTime) + #Mutez(Amount) + SelfAddress + OldLqt => OldLqt +Int (Amount *Int OldLqt) /Int XtzAmount + #Mutez(XtzAmount => XtzAmount +Int Amount) + TokenAmount => TokenAmount +Int #ceildiv(Amount *Int TokenAmount, XtzAmount) + TokenAddress:Address + LqtAddress:Address + Sender + #Nonce(Nonce => Nonce +Int 2) + Accounts + _ + => [ Transfer_tokens #TokenTransferData(Sender, SelfAddress, #ceildiv(Amount *Int TokenAmount, XtzAmount)) #Mutez(0) TokenAddress . %transfer Nonce ] ;; + [ Transfer_tokens Pair ((Amount *Int OldLqt) /Int XtzAmount) Owner #Mutez(0) LqtAddress . %mintOrBurn (Nonce +Int 1) ] ;; + .InternalList + + requires CurrentTime Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) <=Int MaxTokensDeposited + andBool MinLqtMinted <=Int (Amount *Int OldLqt) /Int XtzAmount + andBool #IsLegalMutezValue(Amount +Int XtzAmount) + andBool (Amount *Int TokenAmount) %Int XtzAmount =/=Int 0 + + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` + ```k endmodule ``` @@ -115,10 +145,31 @@ module LIQUIDITY-BAKING-ADDLIQUIDITY-NEGATIVE-SPEC TokenAmount requires notBool( CurrentTime Int 0 - andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) <=Int MaxTokensDeposited andBool MinLqtMinted <=Int (Amount *Int OldLqt) /Int XtzAmount andBool #IsLegalMutezValue(Amount +Int XtzAmount) ) + + claim #runProof(AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + #Timestamp(CurrentTime) + #Mutez(Amount) + OldLqt + #Mutez(XtzAmount) + TokenAmount + requires XtzAmount >Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited + andBool #mod(Amount *Int TokenAmount, XtzAmount) ==Int 0 + + claim #runProof(AddLiquidity(_Owner, MinLqtMinted, MaxTokensDeposited, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + #Timestamp(CurrentTime) + #Mutez(Amount) + OldLqt + #Mutez(XtzAmount) + TokenAmount + requires XtzAmount >Int 0 + andBool #ceildiv(Amount *Int TokenAmount, XtzAmount) >Int MaxTokensDeposited + andBool #mod(Amount *Int TokenAmount, XtzAmount) =/=Int 0 ``` TODO: Deal with the case when the token contract or the liquidity token contract don't exist or have the wrong type. @@ -147,7 +198,7 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-POSITIVE-SPEC .Stack #Timestamp(CurrentTime) #Mutez(0) - SelfAddress + SelfAddress OldLqt => OldLqt -Int LqtBurned #Mutez(XtzAmount => XtzAmount -Int (LqtBurned *Int XtzAmount) /Int OldLqt) TokenAmount => TokenAmount -Int (LqtBurned *Int TokenAmount) /Int OldLqt @@ -155,8 +206,7 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-POSITIVE-SPEC LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 3) - KnownAddresses - LocalEntrypoints + Accounts _ => [ Transfer_tokens (Pair (0 -Int LqtBurned) Sender) #Mutez(0) LqtAddress . %mintOrBurn Nonce ] ;; [ Transfer_tokens #TokenTransferData(SelfAddress, To, (LqtBurned *Int TokenAmount) /Int OldLqt) #Mutez(0) TokenAddress . %transfer (Nonce +Int 1) ] ;; @@ -172,10 +222,10 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-POSITIVE-SPEC andBool TokenAmount -Int (LqtBurned *Int TokenAmount) /Int OldLqt >=Int 0 andBool #IsLegalMutezValue(XtzAmount -Int (LqtBurned *Int XtzAmount) /Int OldLqt) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) - andBool #EntrypointExists(KnownAddresses, To, %default, #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -190,15 +240,14 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-NEGATIVE-SPEC .Stack => ?_:FailedStack #Timestamp(CurrentTime) #Mutez(0) - SelfAddress + SelfAddress OldLqt #Mutez(XtzAmount) TokenAmount TokenAddress:Address LqtAddress:Address Sender - KnownAddresses - LocalEntrypoints + Accounts _ => ?_ requires notBool( CurrentTime Int 0 @@ -210,10 +259,10 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-NEGATIVE-SPEC andBool #IsLegalMutezValue(XtzAmount -Int (LqtBurned *Int XtzAmount) /Int OldLqt) ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) - andBool #EntrypointExists(KnownAddresses, To, %default, #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, LqtAddress, %mintOrBurn, pair int %quantity .AnnotationList address %target .AnnotationList) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -282,10 +331,9 @@ even though the final mutez value that is actually used is smaller than or equal TokenPool:Int => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - LocalEntrypoints - SelfAddress:Address + SelfAddress:Address #Nonce(N => N +Int 3) - KnownAddresses + Accounts _ => [ Transfer_tokens #TokenTransferData(Sender, SelfAddress, TokensSold) #Mutez(0) TokenAddress . %transfer N ] ;; [ Transfer_tokens Unit #Mutez(#XtzNetBurn(#CurrencyBought(XtzPool, TokenPool, TokensSold))) To . %default (N +Int 1)] @@ -306,10 +354,10 @@ even though the final mutez value that is actually used is smaller than or equal andBool #CurrencyBought(XtzPool, TokenPool, TokensSold) <=Int XtzPool andBool #IsLegalMutezValue(XtzPool -Int #CurrencyBought(XtzPool, TokenPool, TokensSold)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, To, %default, #Type(unit)) - andBool #EntrypointExists(KnownAddresses, null_address, %default, #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, null_address, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -323,16 +371,15 @@ module LIQUIDITY-BAKING-TOKENTOXTZ-NEGATIVE-1-SPEC #Timestamp(CurrentTime) #Mutez(Amount) TokenAddress:Address - LocalEntrypoints - KnownAddresses + Accounts requires notBool ( Amount ==Int 0 andBool CurrentTime TokenAddress:Address #Mutez(_XtzPool) TokenPool - LocalEntrypoints - KnownAddresses + Accounts requires Amount ==Int 0 andBool CurrentTime TokenAddress:Address #Mutez(XtzPool) TokenPool - LocalEntrypoints - KnownAddresses + Accounts #Nonce(_ => ?_) requires Amount ==Int 0 andBool CurrentTime =Int MinXtzBought ) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, To, %default, #Type(unit)) - andBool #EntrypointExists(KnownAddresses, null_address, %default, #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, To, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, null_address, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -399,8 +444,7 @@ module LIQUIDITY-BAKING-TOKENTOXTZ-NEGATIVE-4-SPEC TokenAddress:Address #Mutez(XtzPool) TokenPool - LocalEntrypoints - KnownAddresses + Accounts #Nonce(_ => ?_) requires Amount ==Int 0 andBool CurrentTime #runProof(XtzToToken(To, MinTokensBought, #Timestamp(Deadline))) => . .Stack - LocalEntrypoints #Mutez(Amount) TokenAddress #Mutez(XtzPool => XtzPool +Int #XtzNetBurn(Amount)) TokenPool => TokenPool -Int #CurrencyBought(TokenPool, XtzPool, #XtzNetBurn(Amount)) #Timestamp(CurrentTime) - SelfAddress + SelfAddress #Nonce(N => N +Int 2) - KnownAddresses + Accounts _ => [ Transfer_tokens #TokenTransferData(SelfAddress, To, #CurrencyBought(TokenPool, XtzPool, #XtzNetBurn(Amount))) #Mutez(0) TokenAddress . %transfer N ] ;; [ Transfer_tokens Unit #Mutez(absInt(#XtzBurnAmount(Amount))) null_address . %default (N +Int 1)] @@ -458,9 +501,9 @@ module LIQUIDITY-BAKING-XTZTOTOKEN-POSITIVE-SPEC andBool #IsLegalMutezValue(#XtzNetBurn(Amount)) // andBool #IsLegalMutezValue(#XtzBurnAmount(Amount)) // this check can be inferred by the SMT solver so we don't explicitly need it - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, null_address, %default, #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, null_address, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) endmodule ``` @@ -469,13 +512,12 @@ module LIQUIDITY-BAKING-XTZTOTOKEN-NEGATIVE-SPEC imports LIQUIDITY-BAKING-VERIFICATION claim #runProof(XtzToToken(_To, MinTokensBought, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) .Stack => ?_:FailedStack - LocalEntrypoints #Mutez(Amount) TokenAddress #Mutez(XtzPool) TokenPool #Timestamp(CurrentTime) - KnownAddresses + Accounts #Nonce(_:Int => ?_:Int) _ requires notBool ( CurrentTime TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime:Int) Sender - SelfAddress - LocalEntrypoints + SelfAddress #Nonce(N => N +Int 3) - KnownAddresses + Accounts _ => [ Transfer_tokens #TokenTransferData(Sender, SelfAddress, TokensSold) #Mutez(0) TokenAddress . %transfer N ] ;; [ Transfer_tokens Pair To Pair MinTokensBought #Timestamp(Deadline) #Mutez(#XtzNetBurn(#CurrencyBought(XtzPool, TokenPool, TokensSold))) OutputDexterContract . %xtzToToken (N +Int 1)] @@ -543,10 +584,10 @@ A buyer sends tokens to the Liquidity Baking contract, converts its to xtz, and andBool #CurrencyBought(XtzPool, TokenPool, TokensSold) <=Int XtzPool andBool #IsLegalMutezValue(XtzPool -Int #CurrencyBought(XtzPool, TokenPool, TokensSold)) - andBool #EntrypointExists(KnownAddresses, TokenAddress, %transfer, #TokenTransferType()) - andBool #EntrypointExists(KnownAddresses, OutputDexterContract, %xtzToToken, #Type(pair address pair nat timestamp)) - andBool #EntrypointExists(KnownAddresses, null_address, %default, #Type(unit)) - andBool #LocalEntrypointExists(LocalEntrypoints, %default, unit) + andBool #EntrypointExists(Accounts, TokenAddress, %transfer, #TokenTransferType()) + andBool #EntrypointExists(Accounts, OutputDexterContract, %xtzToToken, #Type(pair address pair nat timestamp)) + andBool #EntrypointExists(Accounts, null_address, %default, #Type(unit)) + andBool #EntrypointExists(Accounts, SelfAddress, %default, unit) ``` ```k @@ -567,10 +608,9 @@ module LIQUIDITY-BAKING-TOKENTOTOKEN-NEGATIVE-SPEC TokenPool #Timestamp(CurrentTime:Int) _Sender - _SelfAddress - LocalEntrypoints + _SelfAddress #Nonce(_:Int => ?_:Int) - KnownAddresses + Accounts _ requires notBool ( Amount ==Int 0 andBool CurrentTime X [simplification] - rule X *Int 1 => X [simplification] + rule X /Int 1 => X [simplification] + rule X *Int 1 => X [simplification] + rule false orBool @B:Bool => @B [simplification] + rule @B:Bool orBool false => @B [simplification] ``` ```k @@ -404,14 +406,6 @@ If the contract execution fails, storage is not updated. // ------------------------------------------------------------------------------ rule #TokenTransferData(From, To, TokenAmt) => Pair From Pair To TokenAmt [simplification] - syntax Int ::= #ceildiv (Int, Int) [function] - | #ceildivAux(Int, Int) [function, functional] - // --------------------------------------------------------- - rule #ceildiv (X, Y) => #ceildivAux(X, Y) requires Y =/=Int 0 - rule #ceildivAux(_, Y) => 0 requires Y ==Int 0 - rule #ceildivAux(X, Y) => X /Int Y requires Y =/=Int 0 andBool X %Int Y ==Int 0 - rule #ceildivAux(X, Y) => X /Int Y +Int 1 requires Y =/=Int 0 andBool notBool X %Int Y ==Int 0 - syntax Int ::= #CurrencyBought(Int, Int, Int) [function, functional, smtlib(xtzbought), no-evaluators] // ---------------------------------------------------------------------------------------------------- rule (ToSellAmt *Int 999 *Int ToBuyCurrencyTotal) /Int (ToSellCurrencyTotal *Int 1000 +Int (ToSellAmt *Int 999)) @@ -427,33 +421,25 @@ If the contract execution fails, storage is not updated. rule #XtzBurnAmount(XtzAmount) => XtzAmount -Int #XtzNetBurn ( XtzAmount ) [macro] ``` -```k - syntax Bool ::= #EntrypointExists(Map, Address, FieldAnnotation, Type) - // -------------------------------------------------------------------- - rule #EntrypointExists(KnownAddresses, Addr, FieldAnnot, EntrypointType) - => Addr . FieldAnnot in_keys(KnownAddresses) andBool - KnownAddresses[Addr . FieldAnnot] ==K #Name(EntrypointType) - [macro] - - syntax Bool ::= #LocalEntrypointExists(Map, FieldAnnotation, Type) - // ---------------------------------------------------------------- - rule #LocalEntrypointExists(LocalEntrypoints, FieldAnnot, EntrypointType) - => FieldAnnot in_keys(LocalEntrypoints) andBool - LocalEntrypoints[FieldAnnot] ==K #Name(EntrypointType) - [macro] -``` - ### Avoiding Interpreting Functions If a function value does not play well with the prover or SMT solver, it can be rewritten to `#uninterpreted`. This function has no evaluation rules, so the prover can make no assumptions about it -- it will be assumed it can take on any value. ```k - syntax Int ::= #mulMod(Int, Int, Int) [function, functional, smtlib(mulMod), no-evaluators] + syntax Int ::= #mod(Int, Int) [function, functional, smtlib(mulMod), no-evaluators] | #mulDiv(Int, Int, Int) [function, functional, smtlib(mulDiv), no-evaluators] // ----------------------------------------------------------------------------------------- - rule (X *Int Y) %Int Z => #mulMod(X, Y, Z) [simplification] + rule X %Int Y => #mod(X, Y) [simplification] rule (X *Int Y) /Int Z => #mulDiv(X, Y, Z) [simplification] + + syntax Int ::= #ceildiv (Int, Int) [function] + | #ceildivAux(Int, Int) [function, functional] + // --------------------------------------------------------- + rule #ceildiv (X, Y) => #ceildivAux(X, Y) requires Y =/=Int 0 + rule #ceildivAux(_, Y) => 0 requires Y ==Int 0 + rule #ceildivAux(X, Y) => X /Int Y requires Y =/=Int 0 andBool #mod(X, Y) ==Int 0 + rule #ceildivAux(X, Y) => X /Int Y +Int 1 requires Y =/=Int 0 andBool notBool #mod(X, Y) ==Int 0 ``` ## Putting It All Together diff --git a/tests/proofs/lqt/lqt-spec.md b/tests/proofs/lqt/lqt-spec.md index 1a27d8942..38d396371 100644 --- a/tests/proofs/lqt/lqt-spec.md +++ b/tests/proofs/lqt/lqt-spec.md @@ -109,7 +109,34 @@ module LQT-TOKEN-MINTORBURN-SPEC requires Amount ==Int 0 andBool Sender ==K Admin andBool #tokensFor(Tokens, Address) +Int Quantity ==Int 0 - + andBool Address in_keys(Tokens) + + claim #runProof(MintOrBurnParams(Quantity, Address)) => .K ... + .Stack + Tokens => #incrementTokens(Tokens, Address, Quantity) + #Mutez(Amount) + Admin + Sender + TotalSupply => absInt(TotalSupply +Int Quantity) + _ => .InternalList + requires Amount ==Int 0 + andBool Sender ==K Admin + andBool #tokensFor(Tokens, Address) +Int Quantity ==Int 0 + andBool notBool Address in_keys(Tokens) + + claim #runProof(MintOrBurnParams(Quantity, Address)) => .K ... + .Stack + Tokens => #incrementTokens(Tokens, Address, Quantity) + #Mutez(Amount) + Admin + Sender + TotalSupply => absInt(TotalSupply +Int Quantity) + _ => .InternalList + requires Amount ==Int 0 + andBool Sender ==K Admin + andBool #tokensFor(Tokens, Address) +Int Quantity >Int 0 + andBool Address in_keys(Tokens) + claim #runProof(MintOrBurnParams(Quantity, Address)) => .K ... .Stack Tokens => #incrementTokens(Tokens, Address, Quantity) @@ -121,6 +148,7 @@ module LQT-TOKEN-MINTORBURN-SPEC requires Amount ==Int 0 andBool Sender ==K Admin andBool #tokensFor(Tokens, Address) +Int Quantity >Int 0 + andBool notBool Address in_keys(Tokens) claim #runProof(MintOrBurnParams(Quantity, Address)) => Aborted(?_, ?_, ?_, ?_) ... .Stack => ?_:FailedStack @@ -132,6 +160,21 @@ module LQT-TOKEN-MINTORBURN-SPEC andBool Sender ==K Admin andBool #tokensFor(Tokens, Address) +Int Quantity >=Int 0 ) + andBool Address in_keys(Tokens) + + + claim #runProof(MintOrBurnParams(Quantity, Address)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + #Mutez(Amount) + Admin + Sender + requires notBool( Amount ==Int 0 + andBool Sender ==K Admin + andBool #tokensFor(Tokens, Address) +Int Quantity >=Int 0 + ) + andBool notBool Address in_keys(Tokens) + endmodule ``` @@ -149,6 +192,17 @@ module LQT-TOKEN-APPROVE-SPEC _ => .InternalList requires Amount ==Int 0 andBool (#allowanceFor(Allowances, Sender, Spender) >Int 0 impliesBool Value ==Int 0) + andBool (Pair Sender Spender) in_keys(Allowances) + + claim #runProof(ApproveParams(Spender, Value)) => .K ... + .Stack + Allowances => #updateAllowances(Allowances, Sender, Spender, Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool (#allowanceFor(Allowances, Sender, Spender) >Int 0 impliesBool Value ==Int 0) + andBool notBool (Pair Sender Spender) in_keys(Allowances) ``` ```k @@ -160,6 +214,17 @@ module LQT-TOKEN-APPROVE-SPEC requires notBool( Amount ==Int 0 andBool (#allowanceFor(Allowances, Sender, Spender) >Int 0 impliesBool Value ==Int 0) ) + andBool (Pair Sender Spender) in_keys(Allowances) + + claim #runProof(ApproveParams(Spender, Value)) => Aborted(?_, ?_, ?_, ?_) + .Stack => ?_:FailedStack + Allowances + #Mutez(Amount) + Sender + requires notBool( Amount ==Int 0 + andBool (#allowanceFor(Allowances, Sender, Spender) >Int 0 impliesBool Value ==Int 0) + ) + andBool notBool (Pair Sender Spender) in_keys(Allowances) ``` ```k @@ -183,6 +248,47 @@ module LQT-TOKEN-TRANSFER-DIRECT-SPEC andBool #tokensFor(Tokens, From) >=Int Value // Direct spending andBool Sender ==K From + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Direct spending + andBool Sender ==K From + andBool notBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Direct spending + andBool Sender ==K From + andBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Direct spending + andBool Sender ==K From + andBool notBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) ``` ```k @@ -196,6 +302,47 @@ module LQT-TOKEN-TRANSFER-DIRECT-SPEC andBool notBool( Amount ==Int 0 andBool #tokensFor(Tokens, From) >=Int Value ) + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender ==K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + ) + andBool notBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender ==K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + ) + andBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender ==K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + ) + andBool notBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) ``` ```k @@ -208,7 +355,6 @@ module LQT-TOKEN-TRANSFER-PROXY-SPEC imports LQT-TOKEN-VERIFICATION ``` - ```k claim #runProof(TransferParams(From, To, Value)) => .K .Stack @@ -222,6 +368,246 @@ module LQT-TOKEN-TRANSFER-PROXY-SPEC // Spend via proxy andBool Sender =/=K From andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + andBool Value ==Int 0 + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + andBool Value =/=Int 0 + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => .K + .Stack + Tokens => #incrementTokens(#incrementTokens(Tokens, From, 0 -Int Value), To, Value) + Allowances => #updateAllowances(Allowances, From, Sender, #allowanceFor(Allowances, From, Sender) -Int Value) + #Mutez(Amount) + Sender + _ => .InternalList + requires Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + // Spend via proxy + andBool Sender =/=K From + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + +/////////////////////////////////////////////////////////////////////////////// + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) + + claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... + .Stack => ?_:FailedStack + Tokens + Allowances + #Mutez(Amount) + Sender + requires Sender =/=K From + andBool notBool( Amount ==Int 0 + andBool #tokensFor(Tokens, From) >=Int Value + andBool #allowanceFor(Allowances, From, Sender) >=Int Value + ) + andBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) claim #runProof(TransferParams(From, To, Value)) => Aborted(?_, ?_, ?_, ?_) ... .Stack => ?_:FailedStack @@ -234,6 +620,9 @@ module LQT-TOKEN-TRANSFER-PROXY-SPEC andBool #tokensFor(Tokens, From) >=Int Value andBool #allowanceFor(Allowances, From, Sender) >=Int Value ) + andBool notBool (Pair From Sender) in_keys(Allowances) + andBool notBool From in_keys(Tokens) + andBool notBool To in_keys(Tokens) ``` ```k diff --git a/tests/proofs/lqt/lqt.md b/tests/proofs/lqt/lqt.md index f7130a9b5..473da209c 100644 --- a/tests/proofs/lqt/lqt.md +++ b/tests/proofs/lqt/lqt.md @@ -39,6 +39,8 @@ module LQT-TOKEN-LEMMAS rule X *Int 1 => X [simplification] rule X +Int (0 -Int Y) => X -Int Y [simplification] + rule X -Int 0 => X [simplification] + rule X +Int 0 => X [simplification] ``` ```k @@ -225,15 +227,6 @@ If the contract execution fails, storage is not updated. ## Proof Helper Functions -```k - syntax Bool ::= #EntrypointExists(Map, Address, FieldAnnotation, Type) -// --------------------------------------------------------------------- - rule #EntrypointExists(KnownAddresses, Addr, FieldAnnot, EntrypointType) - => Addr . FieldAnnot in_keys(KnownAddresses) andBool - KnownAddresses[Addr . FieldAnnot] ==K #Name(EntrypointType) - [macro] -``` - ```k syntax Map ::= #incrementTokens(Map, Address, quantity: Int) [function, functional] rule #incrementTokens(Tokens, Address, Quantity) => Tokens[ Address <- undef ] requires #tokensFor(Tokens, Address) +Int Quantity ==Int 0 [simplification, anywhere] diff --git a/tests/proofs/multisig-spec.md b/tests/proofs/multisig-spec.md index 6bc0a7388..c944d8905 100644 --- a/tests/proofs/multisig-spec.md +++ b/tests/proofs/multisig-spec.md @@ -107,7 +107,7 @@ The claims that we make have the following structure: ``` claim InitialSourceFragment => FinalSourceFragment InitialStack => FinalStack - %default |-> ContractParameterType + %default |-> ContractParameterType AmountPassedToContract requires Preconditions ensures Postconditions @@ -124,7 +124,7 @@ that satisfies the preconditions, i.e., an instance of the following: ``` InitialSourceFragment InitialStack - %default |-> ContractParameterType + %default |-> ContractParameterType AmountPassedToContract ``` @@ -134,7 +134,7 @@ which is an instance of: ``` FinalSourceFragment FinalStack - %default |-> ContractParameterType + %default |-> ContractParameterType AmountPassedToContract ``` @@ -288,13 +288,16 @@ The side conditions are defined as follows (and marked in the claim below): => [ pair ( list operation ) pair nat pair nat list key Pair uninterpreted ( Id , Unit ) Pair Count +Int 1 Pair Threshold KeyList:InternalList ] ; .Stack #Mutez(Amount:Int) - %default |-> (or .AnnotationList unit .AnnotationList - pair .AnnotationList (pair .AnnotationList nat .AnnotationList - (or .AnnotationList (lambda .AnnotationList unit .AnnotationList (list .AnnotationList operation .AnnotationList )) - pair .AnnotationList nat .AnnotationList - (list .AnnotationList key .AnnotationList ))) - (list .AnnotationList (option .AnnotationList signature .AnnotationList ))) - + MYADDR + + MYADDR |-> #Account(... entrypoints : %default |-> (or .AnnotationList unit .AnnotationList + pair .AnnotationList (pair .AnnotationList nat .AnnotationList + (or .AnnotationList (lambda .AnnotationList unit .AnnotationList (list .AnnotationList operation .AnnotationList )) + pair .AnnotationList nat .AnnotationList + (list .AnnotationList key .AnnotationList ))) + (list .AnnotationList (option .AnnotationList signature .AnnotationList )))) + ... + requires Amount ==Int 0 // --------------------------------------------------------------------------------------------------- (a) andBool size(SigList) ==Int size(KeyList) // -------------------------------------------------------------------------------- (b) andBool numValidSigs(SigList, KeyList) >=Int Threshold // -------------------------------------------------------------------- (c) @@ -386,6 +389,16 @@ for symbolic reasoning. ; .Stack #Mutez(Amount:Int) + MYADDR + + MYADDR |-> #Account(... entrypoints : %default |-> (or .AnnotationList unit .AnnotationList + pair .AnnotationList (pair .AnnotationList nat .AnnotationList + (or .AnnotationList (lambda .AnnotationList unit .AnnotationList (list .AnnotationList operation .AnnotationList )) + pair .AnnotationList nat .AnnotationList + (list .AnnotationList key .AnnotationList ))) + (list .AnnotationList (option .AnnotationList signature .AnnotationList )))) + ... + requires Amount ==Int 0 andBool size(SigList) ==Int size(KeyList) andBool VerifiedKeys >=Int 0 diff --git a/tests/proofs/pretty-spec.md b/tests/proofs/pretty-spec.md index 466d05bce..f6ee55d64 100644 --- a/tests/proofs/pretty-spec.md +++ b/tests/proofs/pretty-spec.md @@ -18,7 +18,6 @@ module VERIFICATION DIP { EMPTY_MAP timestamp key_hash ; DROP } ; NONE map (set mutez) address ; IF_NONE { } { } ; - PUSH bool True ; DROP } @@ -27,9 +26,6 @@ module VERIFICATION endmodule ``` - - | BinaryBlockInstName AnnotationList Block Block - ```k module PRETTY-SPEC imports VERIFICATION diff --git a/tests/proofs/return-spec.k b/tests/proofs/return-spec.k index 8e21aeeb6..a8fbce307 100644 --- a/tests/proofs/return-spec.k +++ b/tests/proofs/return-spec.k @@ -25,19 +25,16 @@ module RETURN-SPEC } ; PAIR .AnnotationList } => .K - [ (pair unit unit) Pair Unit Unit ] ; .Stack => [ (pair (list operation) unit) Pair [ Transfer_tokens Unit #Mutez(A) #Address("SourceAddr") . %default ?_ ] ;; .InternalList Unit ] ; .Stack - %default |-> unit .AnnotationList - unit .AnnotationList - #Mutez(0) + [ (pair unit unit) Pair Unit Unit ] ; .Stack => [ (pair (list operation) unit) Pair [ Transfer_tokens Unit #Mutez(A) SourceAddr . %default ?_ ] ;; .InternalList Unit ] ; .Stack #Mutez(A) #Timestamp(0) - #Address("OwnAddr") - #Address("SourceAddr") . %default |-> unit - #Address("SourceAddr") - #Address("SenderAddr") + Accounts + SourceAddr + SenderAddr #ChainId(_) #Nonce(?_ => ?_) requires A >Int 0 + andBool #EntrypointExists(Accounts, SourceAddr, %default, #Type(unit)) claim @@ -59,14 +56,11 @@ module RETURN-SPEC PAIR .AnnotationList } => .K [ (pair unit unit) Pair Unit Unit ] ; .Stack => [ (pair (list operation) unit) Pair .InternalList Unit ] ; .Stack - %default |-> unit .AnnotationList - unit .AnnotationList - #Mutez(0) #Mutez(0) #Timestamp(0) - #Address("OwnAddr") - #Address("SourceAddr") . %default |-> unit - #Address("SourceAddr") - #Address("SenderAddr") + Accounts + SourceAddr + SenderAddr #ChainId(_) + requires #EntrypointExists(Accounts, SourceAddr, %default, #Type(unit)) endmodule diff --git a/tests/proofs/sum-to-n-spec.k b/tests/proofs/sum-to-n-spec.k index 70b5b6ef6..7207b92fb 100644 --- a/tests/proofs/sum-to-n-spec.k +++ b/tests/proofs/sum-to-n-spec.k @@ -21,7 +21,8 @@ module SUM-TO-N-SPEC { PAIR .AnnotationList ; LEFT .AnnotationList nat .AnnotationList } } => .K [(or (pair int int) int) Left (Pair A:Int B:Int)] ; .Stack => [int (B +Int ((A *Int (A +Int 1)) /Int 2))] ; .Stack - %default |-> nat .AnnotationList + ADDR + ADDR |-> #Account(... entrypoints : %default |-> nat .AnnotationList) ... nat .AnnotationList requires A >=Int 0 andBool B >=Int 0 endmodule