From 411379e3514071e03b20921b254071b4ddd5c210 Mon Sep 17 00:00:00 2001 From: Stephen Skeirik Date: Fri, 13 Aug 2021 21:02:30 -0500 Subject: [PATCH] Rename contract cells $ sed -i 's/contracts>/accounts>/g' $(git grep -l '') $ sed -i 's/currentContract>/currentAccount>/g' $(git grep -l '') --- michelson.md | 106 +++++++++++------------ tests/proofs/dexter/dexter-spec.md | 84 +++++++++--------- tests/proofs/entrypoints-spec.k | 16 ++-- tests/proofs/liquidity-baking/lb-spec.md | 38 ++++---- tests/proofs/multisig-spec.md | 12 +-- tests/proofs/return-spec.k | 8 +- tests/proofs/sum-to-n-spec.k | 4 +- 7 files changed, 134 insertions(+), 134 deletions(-) diff --git a/michelson.md b/michelson.md index dd5693df6..6db9d2fea 100644 --- a/michelson.md +++ b/michelson.md @@ -83,9 +83,9 @@ The values of many of these cells are accessible via Michelson instructions. #ChainId(.Bytes) .Map - .Map + .Map - #Address("TestContract") + #Address("TestContract") #Nonce(0) .Data #Mutez(0) @@ -222,10 +222,10 @@ Semantics Initialization ```k syntax KItem ::= "#InitContractMap" rule #InitContractMap => . ... - + .Map => A |-> #Account(.Map, .Type, .Data, #Mutez(0), .Data) - - A + + A ``` ### Group Loading @@ -236,32 +236,32 @@ Below are the rules for loading specific groups. ```k rule parameter T:Type => .K ... - A - + A + A |-> #Account(... entrypoints : .Map => #BuildAnnotationMap(.FieldAnnotation, T)) ... - + rule parameter FA:FieldAnnotation T:Type => .K ... - A - + A + A |-> #Account(... entrypoints : .Map => #BuildAnnotationMap(FA, T)) ... - + rule storage T => .K ... - A - + A + A |-> #Account(... storagetype : .Type => T) ... - + rule code C => .K ... - A - + A + A |-> #Account(... script : .Data => C) ... - + rule G:Group ; Gs:Groups => G:Group ~> Gs ... ``` @@ -286,30 +286,30 @@ Below are the rules for loading specific groups. requires #IsLegalMutezValue(I) rule balance I => .K ... - A - + A + A |-> #Account(... balance : #Mutez(0 => I)) ... - + requires #IsLegalMutezValue(I) // 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 => #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 } => . ... @@ -384,11 +384,11 @@ The following unit test groups are not supported by the symbolic interpreter. ```k syntax KItem ::= "#EnsureLocalEntrypointsInitialized" rule #EnsureLocalEntrypointsInitialized => .K ... - CurrentContract - + CurrentContract + CurrentContract |-> #Account(... entrypoints : E => #AddDefaultEntry(E, #Type(unit))) ... - + ``` ```k @@ -406,11 +406,11 @@ The following unit test groups are not supported by the symbolic interpreter. ```k syntax KItem ::= "#ConvertParamToNative" rule #ConvertParamToNative => .K ... - CurrentContract - + CurrentContract + CurrentContract |-> #Account(... entrypoints : E) ... - + D:Data => #MichelineToNative(D, #Type({ E [ %default ] }:>TypeName), .Map, BigMaps) BigMaps @@ -419,20 +419,20 @@ The following unit test groups are not supported by the symbolic interpreter. syntax KItem ::= "#ConvertStorageToNative" rule #ConvertStorageToNative => .K ... - CurrentContract - + CurrentContract + CurrentContract |-> #Account(... storagetype : T => #ConvertToType(T), storagevalue : D:Data => #MichelineToNative(D, #ConvertToType(T), .Map, BigMaps)) ... - + BigMaps rule #ConvertStorageToNative => .K ... - CurrentContract - + CurrentContract + CurrentContract |-> #Account(... storagetype : T => #ConvertToType(T), storagevalue : .Data) ... - + syntax Type ::= #ConvertToType(MaybeType) [function] rule #ConvertToType(.Type) => unit .AnnotationList @@ -513,7 +513,7 @@ version. => #StackToNative(Stack, [ #Name(T) #MichelineToNative(D, T, #AccountStatesToEntrypoints(Contracts, .Map), BigMaps) ] ; Stack') ... - Contracts + Contracts BigMaps requires notBool isSymbolicData(D) @@ -564,11 +564,11 @@ version. => #if Script ==K .Data #then {} #else Script #fi ... - CurrentContract - + CurrentContract + CurrentContract |-> #Account(... script : Script) ... - + ``` Execution Semantics @@ -1699,14 +1699,14 @@ to the given addresses/key hashes. ... [address A:Address] ; _SS - Accounts + Accounts requires A in_keys(Accounts) rule CONTRACT _:AnnotationList T:Type => .K ... [address A:Address] ; SS => [option contract #Name(T) None] ; SS - Accounts + Accounts requires notBool(A in_keys(Accounts)) rule CONTRACT(FA, T, Entrypoints) => . ... @@ -1732,11 +1732,11 @@ These instructions push blockchain state on the stack. ```k rule BALANCE _A => . ... SS => [mutez B] ; SS - ADDR - + ADDR + ADDR |-> #Account(... balance : B) ... - + rule ADDRESS _AL => . ... [contract T #Contract(A . _, T)] ; SS => [address A] ; SS @@ -1751,10 +1751,10 @@ These instructions push blockchain state on the stack. syntax Instruction ::= SELF(FieldAnnotation) rule SELF AL:AnnotationList => #AssumeIsAccount(Accounts [ A ]) ~> SELF(#GetFieldAnnot(AL)) ... - A - + A + Accounts - + rule SELF(FA) => .K ... SS @@ -1762,8 +1762,8 @@ These instructions push blockchain state on the stack. #Contract(A . FA, { entrypoints({Accounts[A]}:>AccountState)[ FA ] }:>TypeName)] ; SS - A - Accounts + A + Accounts rule AMOUNT _A => . ... SS => [mutez M] ; SS @@ -2123,7 +2123,7 @@ abstract out pieces of the stack which are non-invariant during loop execution. ) ... - Contracts + Contracts BigMaps requires #ConcreteMatch(ED, T, #AccountStatesToEntrypoints(Contracts, .Map), BigMaps, AD) andBool TN ==K #Name(T) @@ -2565,7 +2565,7 @@ 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. +We need a similar construct for the `` map. ```k syntax KItem ::= #AssumeIsAccount(KItem) diff --git a/tests/proofs/dexter/dexter-spec.md b/tests/proofs/dexter/dexter-spec.md index 680bce5c9..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,7 +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) - Accounts + 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) ] ;; @@ -104,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) @@ -113,7 +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) - Accounts + 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) ] ;; @@ -263,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 @@ -272,7 +272,7 @@ module DEXTER-REMOVELIQUIDITY-POSITIVE-SPEC LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 3) - Accounts + 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) ] ;; @@ -488,11 +488,11 @@ The contract queries its underlying token contract for its own token balance if false => true TokenAddress:Address TokenId - SelfAddress + SelfAddress #Mutez(Amount) Sender Sender - Accounts + 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 @@ -512,8 +512,8 @@ NOTE: The failure conditions are split into two claims with identical configurat #Mutez(Amount) Sender Source - SelfAddress - Accounts + SelfAddress + Accounts requires ( Amount >Int 0 orBool (notBool #EntrypointExists(Accounts, TokenAddress, #if IsFA2 #then %balance_of #else %getBalance #fi, #TokenBalanceEntrypointType(IsFA2))) orBool IsUpdating @@ -735,8 +735,8 @@ A buyer sends tokens to the Dexter contract and receives a corresponding amount TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - Accounts - SelfAddress:Address + Accounts + SelfAddress:Address #Nonce(N => N +Int 2) TokenID _ @@ -773,7 +773,7 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-1-SPEC #Timestamp(CurrentTime) #Mutez(Amount) _TokenAddress:Address - _Accounts + _Accounts requires notBool IsFA2 andBool ( IsUpdating orBool notBool Amount ==Int 0 @@ -793,8 +793,8 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-2-SPEC TokenAddress:Address #Mutez(_XtzPool) TokenPool - Accounts - SelfAddress + Accounts + SelfAddress requires notBool IsFA2 andBool notBool IsUpdating andBool notBool Amount ==Int 0 @@ -818,8 +818,8 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-3-SPEC TokenAddress:Address #Mutez(XtzPool) TokenPool - Accounts - SelfAddress + Accounts + SelfAddress requires notBool IsFA2 andBool notBool IsUpdating andBool notBool Amount ==Int 0 @@ -845,8 +845,8 @@ module DEXTER-TOKENTOXTZ-FA12-NEGATIVE-4-SPEC TokenAddress:Address #Mutez(XtzPool) TokenPool - Accounts - SelfAddress + Accounts + SelfAddress requires notBool IsFA2 andBool notBool IsUpdating andBool notBool Amount ==Int 0 @@ -889,8 +889,8 @@ As before, a buyer sends tokens to the Dexter contract and receives a correspond TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - Accounts - SelfAddress:Address + Accounts + SelfAddress:Address #Nonce(N => N +Int 2) TokenID _ @@ -926,7 +926,7 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-1-SPEC IsUpdating #Mutez(Amount) #Timestamp(CurrentTime) - _Accounts + _Accounts requires IsFA2 andBool ( IsUpdating orBool notBool Amount ==Int 0 @@ -943,8 +943,8 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-2-SPEC IsUpdating #Mutez(Amount) #Timestamp(CurrentTime) - Accounts - SelfAddress + Accounts + SelfAddress TokenPool #Mutez(XtzPool) TokenAddress:Address @@ -975,8 +975,8 @@ module DEXTER-TOKENTOXTZ-FA2-NEGATIVE-3-SPEC IsUpdating #Mutez(Amount) #Timestamp(CurrentTime) - Accounts - SelfAddress + Accounts + SelfAddress TokenPool #Mutez(XtzPool) TokenAddress:Address @@ -1019,14 +1019,14 @@ module DEXTER-XTZTOTOKEN-FA12-POSITIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(To, MinTokensBought, #Timestamp(Deadline))) => . .Stack - Accounts + 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 _ @@ -1053,8 +1053,8 @@ module DEXTER-XTZTOTOKEN-FA12-NEGATIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(_To, MinTokensBought, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) .Stack => ?_:FailedStack - Accounts - SelfAddress + Accounts + SelfAddress IsUpdating #Mutez(Amount) TokenAddress @@ -1082,14 +1082,14 @@ module DEXTER-XTZTOTOKEN-FA2-POSITIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(To, MinTokensBought, #Timestamp(Deadline))) => . .Stack - Accounts + 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 _ @@ -1116,8 +1116,8 @@ module DEXTER-XTZTOTOKEN-FA2-NEGATIVE-SPEC imports DEXTER-VERIFICATION claim #runProof(IsFA2, XtzToToken(_To, MinTokensBought, #Timestamp(Deadline))) => Aborted(?_, ?_, ?_, ?_) .Stack => ?_:FailedStack - Accounts - SelfAddress + Accounts + SelfAddress IsUpdating #Mutez(Amount) TokenAddress @@ -1166,8 +1166,8 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - SelfAddress - Accounts + SelfAddress + Accounts #Nonce(N => N +Int 2) TokenID _ @@ -1198,8 +1198,8 @@ A buyer sends tokens to the Dexter contract, converts its to xtz, and then immed TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - SelfAddress - Accounts + SelfAddress + Accounts #Nonce(N => N +Int 2) TokenID _ @@ -1241,8 +1241,8 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC TokenPool #Timestamp(CurrentTime) _Sender - SelfAddress - Accounts + SelfAddress + Accounts #Nonce(_N => ?_) _TokenID _ @@ -1272,8 +1272,8 @@ module DEXTER-TOKENTOTOKEN-NEGATIVE-SPEC TokenPool #Timestamp(CurrentTime) _Sender - SelfAddress - Accounts + SelfAddress + Accounts #Nonce(_N => ?_) _TokenID _ diff --git a/tests/proofs/entrypoints-spec.k b/tests/proofs/entrypoints-spec.k index 823780033..2f790d051 100644 --- a/tests/proofs/entrypoints-spec.k +++ b/tests/proofs/entrypoints-spec.k @@ -9,8 +9,8 @@ module ENTRYPOINTS-SPEC claim SELF .AnnotationList => . .Stack => [ contract unit #Contract( SelfAddr . %default, unit ) ] ; .Stack - Accounts - SelfAddr + Accounts + SelfAddr requires #EntrypointExists(Accounts, SelfAddr, %default, unit .AnnotationList) // contract_00, contract_04: Expected contract exists @@ -18,7 +18,7 @@ module ENTRYPOINTS-SPEC [ address #Address(Addr) ] ; .Stack => [ (option contract unit) Some #Contract( #Address(Addr) . %default, unit ) ] ; .Stack - Accounts + Accounts requires #EntrypointExists(Accounts, #Address(Addr), %default, unit .AnnotationList) // contract_01, contract_05: contract does not exist @@ -26,7 +26,7 @@ module ENTRYPOINTS-SPEC [ address #Address(Addr) ] ; .Stack => [ (option contract unit) None ] ; .Stack - Accounts + Accounts requires notBool #Address(Addr) in_keys(Accounts) // contract_03: Contract has different type @@ -34,7 +34,7 @@ module ENTRYPOINTS-SPEC [ address #Address(Addr) ] ; .Stack => [ (option contract unit) None ] ; .Stack - Accounts + Accounts requires #EntrypointExists(Accounts, #Address(Addr), %default, nat .AnnotationList) // contract_06: Non-default entrypoint @@ -42,7 +42,7 @@ module ENTRYPOINTS-SPEC [ address #Address(Addr) ] ; .Stack => [ (option contract unit) Some #Contract( #Address(Addr) . #token("%foo", "FieldAnnotation"), unit ) ] ; .Stack - Accounts + Accounts requires #EntrypointExists(Accounts, #Address(Addr), #token("%foo", "FieldAnnotation"), unit .AnnotationList) // contract_07: Wrong entry point @@ -50,7 +50,7 @@ module ENTRYPOINTS-SPEC [ address #Address(Addr) ] ; .Stack => [ (option contract nat) None ] ; .Stack - Accounts + Accounts requires notBool #EntrypointExists(Accounts, #Address(Addr), #token("%baz", "FieldAnnotation"), nat .AnnotationList) // contract_08: Non-unit type @@ -58,7 +58,7 @@ module ENTRYPOINTS-SPEC [ address #Address(Addr) ] ; .Stack => [ (option contract nat) Some #Contract( #Address(Addr) . %default, nat ) ] ; .Stack - Accounts + 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 beb0f01fa..bae80b2cb 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,7 +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) - Accounts + 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) ] ;; @@ -146,7 +146,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 @@ -154,7 +154,7 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-POSITIVE-SPEC LqtAddress:Address Sender #Nonce(Nonce => Nonce +Int 3) - Accounts + 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) ] ;; @@ -188,14 +188,14 @@ module LIQUIDITY-BAKING-REMOVELIQUIDITY-NEGATIVE-SPEC .Stack => ?_:FailedStack #Timestamp(CurrentTime) #Mutez(0) - SelfAddress + SelfAddress OldLqt #Mutez(XtzAmount) TokenAmount TokenAddress:Address LqtAddress:Address Sender - Accounts + Accounts _ => ?_ requires notBool( CurrentTime Int 0 @@ -279,9 +279,9 @@ even though the final mutez value that is actually used is smaller than or equal TokenPool:Int => TokenPool +Int TokensSold #Timestamp(CurrentTime) Sender - SelfAddress:Address + SelfAddress:Address #Nonce(N => N +Int 3) - Accounts + 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)] @@ -319,7 +319,7 @@ module LIQUIDITY-BAKING-TOKENTOXTZ-NEGATIVE-1-SPEC #Timestamp(CurrentTime) #Mutez(Amount) TokenAddress:Address - Accounts + Accounts requires notBool ( Amount ==Int 0 andBool CurrentTime TokenAddress:Address #Mutez(_XtzPool) TokenPool - Accounts + Accounts requires Amount ==Int 0 andBool CurrentTime TokenAddress:Address #Mutez(XtzPool) TokenPool - Accounts + Accounts #Nonce(_ => ?_) requires Amount ==Int 0 andBool CurrentTime TokenAddress:Address #Mutez(XtzPool) TokenPool - Accounts + Accounts #Nonce(_ => ?_) requires Amount ==Int 0 andBool CurrentTime #Mutez(XtzPool => XtzPool +Int #XtzNetBurn(Amount)) TokenPool => TokenPool -Int #CurrencyBought(TokenPool, XtzPool, #XtzNetBurn(Amount)) #Timestamp(CurrentTime) - SelfAddress + SelfAddress #Nonce(N => N +Int 2) - Accounts + 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)] @@ -465,7 +465,7 @@ module LIQUIDITY-BAKING-XTZTOTOKEN-NEGATIVE-SPEC #Mutez(XtzPool) TokenPool #Timestamp(CurrentTime) - Accounts + Accounts #Nonce(_:Int => ?_:Int) _ requires notBool ( CurrentTime TokenPool => TokenPool +Int TokensSold #Timestamp(CurrentTime:Int) Sender - SelfAddress + SelfAddress #Nonce(N => N +Int 3) - Accounts + 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)] @@ -556,9 +556,9 @@ module LIQUIDITY-BAKING-TOKENTOTOKEN-NEGATIVE-SPEC TokenPool #Timestamp(CurrentTime:Int) _Sender - _SelfAddress + _SelfAddress #Nonce(_:Int => ?_:Int) - Accounts + Accounts _ requires notBool ( Amount ==Int 0 andBool CurrentTime [ 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) - MYADDR - + 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 )) @@ -297,7 +297,7 @@ The side conditions are defined as follows (and marked in the claim below): (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) @@ -389,8 +389,8 @@ for symbolic reasoning. ; .Stack #Mutez(Amount:Int) - MYADDR - + 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 )) @@ -398,7 +398,7 @@ for symbolic reasoning. (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/return-spec.k b/tests/proofs/return-spec.k index 7741d0537..db07e479b 100644 --- a/tests/proofs/return-spec.k +++ b/tests/proofs/return-spec.k @@ -28,11 +28,11 @@ module RETURN-SPEC [ (pair unit unit) Pair Unit Unit ] ; .Stack => [ (pair (list operation) unit) Pair [ Transfer_tokens Unit #Mutez(A) #Address("SourceAddr") . %default ?_ ] ;; .InternalList Unit ] ; .Stack #Mutez(A) #Timestamp(0) - + #Address("SourceAddr") |-> #Account(... entrypoints : %default |-> unit, storagetype : unit .AnnotationList) ... - + #Address("SourceAddr") #Address("SenderAddr") #ChainId(_) @@ -61,11 +61,11 @@ module RETURN-SPEC [ (pair unit unit) Pair Unit Unit ] ; .Stack => [ (pair (list operation) unit) Pair .InternalList Unit ] ; .Stack #Mutez(0) #Timestamp(0) - + #Address("SourceAddr") |-> #Account(... entrypoints : %default |-> unit, storagetype : unit .AnnotationList) ... - + #Address("SourceAddr") #Address("SenderAddr") #ChainId(_) diff --git a/tests/proofs/sum-to-n-spec.k b/tests/proofs/sum-to-n-spec.k index 6a3e1a452..7207b92fb 100644 --- a/tests/proofs/sum-to-n-spec.k +++ b/tests/proofs/sum-to-n-spec.k @@ -21,8 +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 - ADDR - ADDR |-> #Account(... entrypoints : %default |-> nat .AnnotationList) ... + ADDR + ADDR |-> #Account(... entrypoints : %default |-> nat .AnnotationList) ... nat .AnnotationList requires A >=Int 0 andBool B >=Int 0 endmodule