diff --git a/README.md b/README.md index 2100ec6523..02966e28e6 100644 --- a/README.md +++ b/README.md @@ -281,7 +281,7 @@ Files produced by test runs, e.g. kompiled definition and logs, can be found in For Developers -------------- -If built from the source, the `kevm-pyk` executable will be installed in a virtual environemtn handled by Poetry. +If built from the source, the `kevm-pyk` executable will be installed in a virtual environment handled by Poetry. You can call `kevm-pyk --help` to get a quick summary of how to use the script. Run the file `tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json`: diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index c99a33531a..6ebb73007b 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.589" +version = "1.0.590" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index a9e84edca7..df47a5f1b6 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.589' +VERSION: Final = '1.0.590' diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md index 676d5f70d2..fca29562ba 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md @@ -27,9 +27,9 @@ module BIN-RUNTIME imports EVM-ABI syntax Contract - syntax Bytes ::= #binRuntime ( Contract ) [alias, klabel(binRuntime), symbol, function, no-evaluators] - | #initBytecode ( Contract ) [alias, klabel(initBytecode), symbol, function, no-evaluators] - // ------------------------------------------------------------------------------------------------------ + syntax Bytes ::= #binRuntime ( Contract ) [alias, symbol(binRuntime) , function, no-evaluators] + | #initBytecode ( Contract ) [alias, symbol(initBytecode), function, no-evaluators] + // -------------------------------------------------------------------------------------------------- endmodule ``` diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 07b21059b7..4d7f208079 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -183,9 +183,9 @@ Our semantics is modal, with the initial mode being set on the command line via - `VMTESTS` skips `CALL*` and `CREATE` operations. ```k - syntax Mode ::= "NORMAL" [klabel(NORMAL), symbol] - | "VMTESTS" [klabel(VMTESTS), symbol] - // --------------------------------------------------- + syntax Mode ::= "NORMAL" [symbol(NORMAL) ] + | "VMTESTS" [symbol(VMTESTS)] + // ------------------------------------------- ``` State Stacks diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md index 5b6653e7f9..085f29445f 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -57,7 +57,8 @@ In particular, this means that `#gas(_) false`, and `#gas(_) <=G module INFINITE-GAS imports GAS - syntax Gas ::= #gas(Int) [klabel(infGas), symbol, smtlib(infGas)] + syntax Gas ::= #gas(Int) [symbol(infGas), smtlib(infGas)] + // --------------------------------------------------------- rule #gas(G) +Gas G' => #gas(G +Int G') rule #gas(G) -Gas G' => #gas(G -Int G') @@ -207,8 +208,8 @@ module GAS-FEES rule [Cinitcode.new]: Cinitcode(SCHED, INITCODELEN) => Ginitcodewordcost < SCHED > *Int ( INITCODELEN up/Int 32 ) requires Ghasmaxinitcodesize << SCHED >> [concrete] rule [Cinitcode.old]: Cinitcode(SCHED, _) => 0 requires notBool Ghasmaxinitcodesize << SCHED >> [concrete] - syntax Bool ::= #accountEmpty ( AccountCode , Int , Int ) [function, total, klabel(accountEmpty), symbol] - // --------------------------------------------------------------------------------------------------------- + syntax Bool ::= #accountEmpty ( AccountCode , Int , Int ) [function, total, symbol(accountEmpty)] + // ------------------------------------------------------------------------------------------------- rule #accountEmpty(CODE, NONCE, BAL) => CODE ==K .Bytes andBool NONCE ==Int 0 andBool BAL ==Int 0 syntax Gas ::= #allBut64th ( Gas ) [symbol(#allBut64th_Gas), overload(#allBut64th), function, total, smtlib(gas_allBut64th_Gas)] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md index 7832f81be9..af784ca907 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md @@ -78,17 +78,17 @@ module SOLIDITY-FIELDS syntax Contract syntax Field syntax ContractAccess ::= Contract - | ContractAccess "." Field [klabel(contract_access_field), symbol] - | ContractAccess "[" Int "]" [klabel(contract_access_index), symbol] - // -------------------------------------------------------------------------------------------- + | ContractAccess "." Field [symbol(contract_access_field)] + | ContractAccess "[" Int "]" [symbol(contract_access_index)] + // ------------------------------------------------------------------------------------ - syntax Int ::= #loc ( ContractAccess ) [klabel(contract_access_loc), function, symbol] - // -------------------------------------------------------------------------------------- + syntax Int ::= #loc ( ContractAccess ) [symbol(contract_access_loc), function] + // ------------------------------------------------------------------------------ rule #loc(_:Contract) => 0 rule #loc(C [ I ]) => #hash(#loc(C), I) - syntax Int ::= #hash ( Int , Int ) [klabel(contract_access_hash), function, symbol] - // ----------------------------------------------------------------------------------- + syntax Int ::= #hash ( Int , Int ) [symbol(contract_access_hash), function] + // --------------------------------------------------------------------------- rule #hash(I1, I2) => keccak(#bufStrict(32, I2) +Bytes #bufStrict(32, I1)) endmodule diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md index 78491f535c..94ec093152 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md @@ -95,8 +95,8 @@ module JSON-RPC .List - syntax JSON ::= "undef" [klabel(JSON-RPCundef), symbol] - // ------------------------------------------------------- + syntax JSON ::= "undef" [symbol(JSON-RPCundef)] + // ----------------------------------------------- syntax Bool ::= isProperJson ( JSON ) [klabel(isProperJson), function] | isProperJsonList ( JSONs ) [klabel(isProperJsonList), function] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index d46be3575d..8dd7628f1b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -54,8 +54,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Default Schedule ```k - syntax Schedule ::= "DEFAULT" [klabel(DEFAULT_EVM), symbol, smtlib(schedule_DEFAULT)] - // ------------------------------------------------------------------------------------- + syntax Schedule ::= "DEFAULT" [symbol(DEFAULT_EVM), smtlib(schedule_DEFAULT)] + // ----------------------------------------------------------------------------- rule Gzero < DEFAULT > => 0 rule Gbase < DEFAULT > => 2 rule Gverylow < DEFAULT > => 3 @@ -150,8 +150,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Frontier Schedule ```k - syntax Schedule ::= "FRONTIER" [klabel(FRONTIER_EVM), symbol, smtlib(schedule_FRONTIER)] - // ---------------------------------------------------------------------------------------- + syntax Schedule ::= "FRONTIER" [symbol(FRONTIER_EVM), smtlib(schedule_FRONTIER)] + // -------------------------------------------------------------------------------- rule Gtxcreate < FRONTIER > => 21000 rule SCHEDCONST < FRONTIER > => SCHEDCONST < DEFAULT > requires SCHEDCONST =/=K Gtxcreate @@ -161,8 +161,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Homestead Schedule ```k - syntax Schedule ::= "HOMESTEAD" [klabel(HOMESTEAD_EVM), symbol, smtlib(schedule_HOMESTEAD)] - // ------------------------------------------------------------------------------------------- + syntax Schedule ::= "HOMESTEAD" [symbol(HOMESTEAD_EVM), smtlib(schedule_HOMESTEAD)] + // ----------------------------------------------------------------------------------- rule SCHEDCONST < HOMESTEAD > => SCHEDCONST < DEFAULT > rule SCHEDFLAG << HOMESTEAD >> => SCHEDFLAG << DEFAULT >> @@ -171,8 +171,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Tangerine Whistle Schedule ```k - syntax Schedule ::= "TANGERINE_WHISTLE" [klabel(TANGERINE_WHISTLE_EVM), symbol, smtlib(schedule_TANGERINE_WHISTLE)] - // ------------------------------------------------------------------------------------------------------------------- + syntax Schedule ::= "TANGERINE_WHISTLE" [symbol(TANGERINE_WHISTLE_EVM), smtlib(schedule_TANGERINE_WHISTLE)] + // ----------------------------------------------------------------------------------------------------------- rule Gbalance < TANGERINE_WHISTLE > => 400 rule Gsload < TANGERINE_WHISTLE > => 200 rule Gcall < TANGERINE_WHISTLE > => 700 @@ -194,8 +194,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Spurious Dragon Schedule ```k - syntax Schedule ::= "SPURIOUS_DRAGON" [klabel(SPURIOUS_DRAGON_EVM), symbol, smtlib(schedule_SPURIOUS_DRAGON)] - // ------------------------------------------------------------------------------------------------------------- + syntax Schedule ::= "SPURIOUS_DRAGON" [symbol(SPURIOUS_DRAGON_EVM), smtlib(schedule_SPURIOUS_DRAGON)] + // ----------------------------------------------------------------------------------------------------- rule Gexpbyte < SPURIOUS_DRAGON > => 50 rule maxCodeSize < SPURIOUS_DRAGON > => 24576 @@ -210,8 +210,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Byzantium Schedule ```k - syntax Schedule ::= "BYZANTIUM" [klabel(BYZANTIUM_EVM), symbol, smtlib(schedule_BYZANTIUM)] - // ------------------------------------------------------------------------------------------- + syntax Schedule ::= "BYZANTIUM" [symbol(BYZANTIUM_EVM), smtlib(schedule_BYZANTIUM)] + // ----------------------------------------------------------------------------------- rule Rb < BYZANTIUM > => 3 *Int eth rule SCHEDCONST < BYZANTIUM > => SCHEDCONST < SPURIOUS_DRAGON > requires notBool ( SCHEDCONST ==K Rb ) @@ -226,8 +226,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Constantinople Schedule ```k - syntax Schedule ::= "CONSTANTINOPLE" [klabel(CONSTANTINOPLE_EVM), symbol, smtlib(schedule_CONSTANTINOPLE)] - // ---------------------------------------------------------------------------------------------------------- + syntax Schedule ::= "CONSTANTINOPLE" [symbol(CONSTANTINOPLE_EVM), smtlib(schedule_CONSTANTINOPLE)] + // -------------------------------------------------------------------------------------------------- rule Rb < CONSTANTINOPLE > => 2 *Int eth rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM > requires notBool ( SCHEDCONST ==K Rb ) @@ -243,8 +243,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Petersburg Schedule ```k - syntax Schedule ::= "PETERSBURG" [klabel(PETERSBURG_EVM), symbol, smtlib(schedule_PETERSBURG)] - // ---------------------------------------------------------------------------------------------- + syntax Schedule ::= "PETERSBURG" [symbol(PETERSBURG_EVM), smtlib(schedule_PETERSBURG)] + // -------------------------------------------------------------------------------------- rule SCHEDCONST < PETERSBURG > => SCHEDCONST < CONSTANTINOPLE > rule Ghasdirtysstore << PETERSBURG >> => false @@ -255,8 +255,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Istanbul Schedule ```k - syntax Schedule ::= "ISTANBUL" [klabel(ISTANBUL_EVM), symbol, smtlib(schedule_ISTANBUL)] - // ---------------------------------------------------------------------------------------- + syntax Schedule ::= "ISTANBUL" [symbol(ISTANBUL_EVM), smtlib(schedule_ISTANBUL)] + // -------------------------------------------------------------------------------- rule Gecadd < ISTANBUL > => 150 rule Gecmul < ISTANBUL > => 6000 rule Gecpairconst < ISTANBUL > => 45000 @@ -289,8 +289,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Berlin Schedule ```k - syntax Schedule ::= "BERLIN" [klabel(BERLIN_EVM), symbol, smtlib(schedule_BERLIN)] - // ---------------------------------------------------------------------------------- + syntax Schedule ::= "BERLIN" [symbol(BERLIN_EVM), smtlib(schedule_BERLIN)] + // -------------------------------------------------------------------------- rule Gcoldsload < BERLIN > => 2100 rule Gcoldaccountaccess < BERLIN > => 2600 rule Gwarmstorageread < BERLIN > => 100 @@ -319,8 +319,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### London Schedule ```k - syntax Schedule ::= "LONDON" [klabel(LONDON_EVM), symbol, smtlib(schedule_LONDON)] - // ---------------------------------------------------------------------------------- + syntax Schedule ::= "LONDON" [symbol(LONDON_EVM), smtlib(schedule_LONDON)] + // -------------------------------------------------------------------------- rule Rselfdestruct < LONDON > => 0 rule Rsstoreclear < LONDON > => Gsstorereset < LONDON > +Int Gaccessliststoragekey < LONDON > rule Rmaxquotient < LONDON > => 5 @@ -341,8 +341,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Merge Schedule ```k - syntax Schedule ::= "MERGE" [klabel(MERGE_EVM), symbol, smtlib(schedule_MERGE)] - // ------------------------------------------------------------------------------- + syntax Schedule ::= "MERGE" [symbol(MERGE_EVM), smtlib(schedule_MERGE)] + // ----------------------------------------------------------------------- rule Rb < MERGE > => 0 rule SCHEDCONST < MERGE > => SCHEDCONST < LONDON > requires notBool SCHEDCONST ==K Rb @@ -355,8 +355,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Shanghai Schedule ```k - syntax Schedule ::= "SHANGHAI" [klabel(SHANGHAI_EVM), symbol, smtlib(schedule_SHANGHAI)] - // ---------------------------------------------------------------------------------------- + syntax Schedule ::= "SHANGHAI" [symbol(SHANGHAI_EVM), smtlib(schedule_SHANGHAI)] + // -------------------------------------------------------------------------------- rule maxInitCodeSize < SHANGHAI > => 2 *Int maxCodeSize < SHANGHAI > rule Ginitcodewordcost < SHANGHAI > => 2 rule SCHEDCONST < SHANGHAI > => SCHEDCONST < MERGE > diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 884b625a17..3fd8c34359 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -61,13 +61,13 @@ Address/Hash Helpers - `#blockHeaderHash` computes the hash of a block header given all the block data. ```k - syntax Int ::= #blockHeaderHash( Int , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int , Int , Bytes , Int , Int ) [function, klabel(blockHeaderHash), symbol] - | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, klabel(#blockHashHeaderBytes), symbol] - | #blockHeaderHash( Int , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int , Int , Bytes , Int , Int , Int) [function, klabel(blockHeaderHashBaseFee), symbol] - | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, klabel(#blockHashHeaderBaseFeeBytes), symbol] - | #blockHeaderHash( Int , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int) [function, klabel(blockHeaderHashWithdrawals), symbol] - | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, klabel(#blockHashHeaderWithdrawalsBytes), symbol] - // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + syntax Int ::= #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int ) [function, symbol(blockHeaderHash) ] + | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(#blockHashHeaderBytes) ] + | #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int ) [function, symbol(blockHeaderHashBaseFee) ] + | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(#blockHashHeaderBaseFeeBytes) ] + | #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int ) [function, symbol(blockHeaderHashWithdrawals) ] + | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, symbol(#blockHashHeaderWithdrawalsBytes)] + // ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- rule #blockHeaderHash(HP:Bytes, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN) => #parseHexWord( Keccak256( #rlpEncode( [ HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN ] ) ) ) @@ -113,8 +113,8 @@ Address/Hash Helpers - `#hashSignedTx` Takes transaction data. Returns the hash of the rlp-encoded transaction with R S and V. ```k - syntax Bytes ::= #hashSignedTx( Int , Int , Int , Account , Int , Bytes , Int , Bytes , Bytes ) [klabel(#hashSignedTx), function] - | #hashTxData ( TxData ) [klabel(#hashTxData), function] + syntax Bytes ::= #hashTxData ( TxData ) [klabel(#hashTxData), function] + | #hashSignedTx( Int , Int , Int , Account , Int , Bytes , Int , Bytes , Bytes ) [klabel(#hashSignedTx), function] // --------------------------------------------------------------------------------------------------------------------------------- rule #hashSignedTx(TN, TP, TG, TT, TV, TD, TW, TR, TS) => Keccak256raw( #rlpEncode([ TN, TP, TG, #addrBytes(TT), TV, TD, TW, TR, TS ]) ) @@ -142,8 +142,8 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s - `#parseAccessListStorageKeys` interprets a JSON list object as a Set, casting each string element as a `Word`. ```k - syntax Int ::= #parseHexWord ( String ) [klabel(#parseHexWord), function] - | #parseWord ( String ) [klabel(#parseWord), function] + syntax Int ::= #parseWord ( String ) [klabel(#parseWord), function] + | #parseHexWord ( String ) [klabel(#parseHexWord), function] // ------------------------------------------------------------------------- rule #parseHexWord("") => 0 rule #parseHexWord("0x") => 0 @@ -163,11 +163,10 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s | #parseByteStack ( String ) [symbol(parseByteStack), function, memo] // --------------------------------------------------------------------------------------- rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", "")) - rule #parseHexBytes(S) => #parseHexBytesAux(#alignHexString(S)) + rule #parseHexBytesAux("") => .Bytes - rule #parseHexBytesAux(S) => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE) - requires lengthString(S) >=Int 2 + rule #parseHexBytesAux(S) => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE) requires lengthString(S) >=Int 2 syntax Map ::= #parseMap ( JSON ) [klabel(#parseMap), function] // --------------------------------------------------------------- @@ -183,7 +182,7 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s | #parseAccessListStorageKeys ( JSONs , List ) [klabel(#parseAccessListStorageKeysAux), function] // -------------------------------------------------------------------------------------------------------------- rule #parseAccessListStorageKeys( J ) => #parseAccessListStorageKeys(J, .List) - rule #parseAccessListStorageKeys([S:Bytes, REST], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#asWord(S)) RESULT ) + rule #parseAccessListStorageKeys([S:Bytes, REST ], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#asWord(S)) RESULT ) rule #parseAccessListStorageKeys([ .JSONs ], RESULT:List) => RESULT ``` @@ -192,16 +191,16 @@ Unparsing - `#padByte` ensures that the `String` interperetation of a `Int` is wide enough. ```k - syntax String ::= #padByte( String ) [klabel(#padByte), function] - // ----------------------------------------------------------------- + syntax String ::= #padByte ( String ) [klabel(#padByte), function] + // ------------------------------------------------------------------ rule #padByte( S ) => S requires lengthString(S) ==K 2 rule #padByte( S ) => "0" +String S requires lengthString(S) ==K 1 - syntax String ::= #unparseQuantity( Int ) [klabel(#unparseQuantity), function] - // ------------------------------------------------------------------------------ + syntax String ::= #unparseQuantity ( Int ) [klabel(#unparseQuantity), function] + // ------------------------------------------------------------------------------- rule #unparseQuantity( I ) => "0x" +String Base2String(I, 16) - syntax String ::= #unparseData ( Int, Int ) [klabel(#unparseData), function] + syntax String ::= #unparseData ( Int, Int ) [klabel(#unparseData ), function] | #unparseDataBytes ( Bytes ) [klabel(#unparseDataBytes), function] // --------------------------------------------------------------------------------------- rule #unparseData( DATA, LENGTH ) => #unparseDataBytes(#padToWidth(LENGTH,#asByteStack(DATA))) @@ -213,9 +212,9 @@ Unparsing - `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes ```k - syntax Bytes ::= #addrBytes( Account ) [klabel(#addrBytes), function] - | #wordBytes( Int ) [klabel(#wordBytes), function] - // --------------------------------------------------------------------- + syntax Bytes ::= #addrBytes ( Account ) [klabel(#addrBytes), function] + | #wordBytes ( Int ) [klabel(#wordBytes), function] + // ---------------------------------------------------------------------- rule #addrBytes(.Account) => .Bytes rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT) rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD) @@ -239,12 +238,12 @@ Encoding example: `#rlpEncode( [ 0, 1, 1, "", #parseByteStack("0xef880") ] )` ```k - syntax Bytes ::= #rlpEncodeInt ( Int ) [klabel(#rlpEncodeInt), function] - | #rlpEncodeWord ( Int ) [klabel(#rlpEncodeWord), function] + syntax Bytes ::= #rlpEncodeInt ( Int ) [klabel(#rlpEncodeInt ), function] + | #rlpEncodeWord ( Int ) [klabel(#rlpEncodeWord ), function] | #rlpEncodeAddress ( Account ) [klabel(#rlpEncodeAddress), function] - | #rlpEncodeString ( String ) [klabel(#rlpEncodeString), function] - | #rlpEncodeBytes ( Bytes ) [klabel(#rlpEncodeBytes), function] - | #rlpEncode ( JSON ) [klabel(#rlpEncode), function] + | #rlpEncodeString ( String ) [klabel(#rlpEncodeString ), function] + | #rlpEncodeBytes ( Bytes ) [klabel(#rlpEncodeBytes ), function] + | #rlpEncode ( JSON ) [klabel(#rlpEncode ), function] | #rlpEncode ( JSONs, StringBuffer ) [klabel(#rlpEncodeJsonAux), function] // ----------------------------------------------------------------------------------------- rule #rlpEncodeInt(0) => b"\x80" @@ -277,8 +276,8 @@ Encoding rule #rlpEncodeLength(BYTES, OFFSET) => #rlpEncodeLength(BYTES, OFFSET, #asByteStack(lengthBytes(BYTES))) requires notBool ( lengthBytes(BYTES) #asByteStack(lengthBytes(BL) +Int OFFSET +Int 55) +Bytes BL +Bytes BYTES - syntax Bytes ::= #rlpEncodeFullAccount( Int, Int, Map, Bytes ) [klabel(#rlpEncodeFullAccount), function] - // -------------------------------------------------------------------------------------------------------- + syntax Bytes ::= #rlpEncodeFullAccount ( Int , Int , Map , Bytes ) [klabel(#rlpEncodeFullAccount), function] + // ------------------------------------------------------------------------------------------------------------ rule [rlpAcct]: #rlpEncodeFullAccount( NONCE, BAL, STORAGE, CODE ) => #rlpEncodeLength( #rlpEncodeInt(NONCE) +Bytes #rlpEncodeInt(BAL) @@ -287,10 +286,10 @@ Encoding , 192 ) - syntax Bytes ::= #rlpEncodeReceipt ( Int , Int , Bytes , List ) [klabel(#rlpEncodeReceipt), function] - | #rlpEncodeLogs ( List ) [klabel(#rlpEncodeLogs), function] - | #rlpEncodeLogsAux ( List, StringBuffer ) [klabel(#rlpEncodeLogsAux), function] - | #rlpEncodeTopics ( List, StringBuffer ) [klabel(#rlpEncodeTopics), function] + syntax Bytes ::= #rlpEncodeTopics ( List , StringBuffer ) [klabel(#rlpEncodeTopics ), function] + | #rlpEncodeReceipt ( Int , Int , Bytes , List ) [klabel(#rlpEncodeReceipt), function] + | #rlpEncodeLogs ( List ) [klabel(#rlpEncodeLogs ), function] + | #rlpEncodeLogsAux ( List , StringBuffer ) [klabel(#rlpEncodeLogsAux), function] // ----------------------------------------------------------------------------------------------------- rule [rlpReceipt]: #rlpEncodeReceipt(RS, RG, RB, RL) => #rlpEncodeLength( #rlpEncodeInt(RS) @@ -318,8 +317,8 @@ Encoding , ( OUT => OUT +String Bytes2String( #rlpEncodeWord(X) ) ) ) - syntax Bytes ::= #rlpEncodeTxData( TxData ) [klabel(#rlpEncodeTxData), function] - // -------------------------------------------------------------------------------- + syntax Bytes ::= #rlpEncodeTxData ( TxData ) [klabel(#rlpEncodeTxData), function] + // --------------------------------------------------------------------------------- rule #rlpEncodeTxData( LegacyTxData( TN, TP, TG, TT, TV, TD ) ) => #rlpEncode( [ TN, TP, TG, #addrBytes(TT), TV, TD ] ) @@ -361,12 +360,12 @@ Encoding , 192 ) - syntax Bytes ::= MerkleMapRLP( Map, Int ) [klabel(MerkleMapRLP), function] - // -------------------------------------------------------------------------- + syntax Bytes ::= MerkleMapRLP ( Map , Int ) [klabel(MerkleMapRLP), function] + // ---------------------------------------------------------------------------- rule MerkleMapRLP(M, I) => #rlpMerkleH( #rlpEncodeMerkleTree( { M[I] orDefault .MerkleTree }:>MerkleTree ) ) - syntax Bytes ::= #rlpMerkleH ( Bytes ) [function,klabel(MerkleRLPAux)] - // ---------------------------------------------------------------------- + syntax Bytes ::= #rlpMerkleH ( Bytes ) [function, klabel(MerkleRLPAux)] + // ----------------------------------------------------------------------- rule #rlpMerkleH ( X ) => #rlpEncodeBytes( #parseByteStack( Keccak256( X ) ) ) requires lengthBytes(X) >=Int 32 @@ -381,16 +380,16 @@ Decoding - `#rlpDecodeList` RLP decodes a single `Bytes` into a `JSONs`, interpereting the input as the RLP encoding of a list. ```k - syntax JSON ::= #rlpDecode(Bytes) [klabel(#rlpDecode), function] - | #rlpDecode(Bytes, LengthPrefix) [klabel(#rlpDecodeAux), function] - // --------------------------------------------------------------------------------- + syntax JSON ::= #rlpDecode ( Bytes ) [klabel(#rlpDecode ), function] + | #rlpDecode ( Bytes , LengthPrefix) [klabel(#rlpDecodeAux), function] + // ------------------------------------------------------------------------------------ rule #rlpDecode(BYTES) => #rlpDecode(BYTES, #decodeLengthPrefix(BYTES, 0)) rule #rlpDecode(BYTES, #str( LEN, POS)) => substrBytes(BYTES, POS, POS +Int LEN) rule #rlpDecode(BYTES, #list(_LEN, POS)) => [#rlpDecodeList(BYTES, POS)] - syntax JSONs ::= #rlpDecodeList(Bytes, Int) [klabel(#rlpDecodeList), function] - | #rlpDecodeList(Bytes, Int, LengthPrefix) [klabel(#rlpDecodeListAux), function] - // ----------------------------------------------------------------------------------------------- + syntax JSONs ::= #rlpDecodeList (Bytes , Int ) [klabel(#rlpDecodeList ), function] + | #rlpDecodeList (Bytes , Int , LengthPrefix) [klabel(#rlpDecodeListAux), function] + // -------------------------------------------------------------------------------------------------- rule #rlpDecodeList(BYTES, POS) => #rlpDecodeList(BYTES, POS, #decodeLengthPrefix(BYTES, POS)) requires POS .JSONs [owise] rule #rlpDecodeList(BYTES, POS, _:LengthPrefixType(L, P)) => #rlpDecode(substrBytes(BYTES, POS, L +Int P)) , #rlpDecodeList(BYTES, L +Int P) @@ -414,8 +413,8 @@ Decoding rule #decodeLengthPrefixLength(#list, BYTES, START, B0) => #decodeLengthPrefixLength(#list, START, B0 -Int 192 -Int 56 +Int 1, #asWord(substrBytes(BYTES, START +Int 1, START +Int 1 +Int (B0 -Int 192 -Int 56 +Int 1)))) rule #decodeLengthPrefixLength(TYPE, START, LL, L) => TYPE(L, START +Int 1 +Int LL) - syntax JSONs ::= #rlpDecodeTransaction(Bytes) [klabel(#rlpDecodeTransaction), function] - // --------------------------------------------------------------------------------------- + syntax JSONs ::= #rlpDecodeTransaction ( Bytes ) [klabel(#rlpDecodeTransaction), function] + // ------------------------------------------------------------------------------------------ rule #rlpDecodeTransaction(T) => #range(T, 0, 1), #rlpDecode(#range(T, 1, lengthBytes(T) -Int 1)) ``` @@ -429,25 +428,23 @@ Merkle Patricia Tree syntax KItem ::= Int | MerkleTree // For testing purposes syntax MerkleTree ::= ".MerkleTree" - | MerkleBranch ( Map, String ) [klabel(MerkleBranch)] + | MerkleBranch ( Map, String ) [klabel(MerkleBranch )] | MerkleExtension ( Bytes, MerkleTree ) [klabel(MerkleExtension)] - | MerkleLeaf ( Bytes, String ) [klabel(MerkleLeaf)] + | MerkleLeaf ( Bytes, String ) [klabel(MerkleLeaf )] // ------------------------------------------------------------------------------------- - syntax MerkleTree ::= MerkleUpdate ( MerkleTree, String, String ) [klabel(MerkleUpdate), function] + syntax MerkleTree ::= MerkleUpdate ( MerkleTree, String, String ) [klabel(MerkleUpdate ), function] | MerkleUpdate ( MerkleTree, Bytes, String ) [klabel(MerkleUpdateAux), function] - | MerklePut ( MerkleTree, Bytes, String ) [klabel(MerklePut), function] - | MerkleDelete ( MerkleTree, Bytes ) [klabel(MerkleDelete), function] + | MerklePut ( MerkleTree, Bytes, String ) [klabel(MerklePut ), function] + | MerkleDelete ( MerkleTree, Bytes ) [klabel(MerkleDelete ), function] // ----------------------------------------------------------------------------------------------------- rule MerkleUpdate ( TREE, S:String, VALUE ) => MerkleUpdate ( TREE, #nibbleize ( String2Bytes( S ) ), VALUE ) rule MerkleUpdate ( TREE, PATH:Bytes, VALUE ) => MerklePut ( TREE, PATH, VALUE ) requires VALUE =/=String "" rule MerkleUpdate ( TREE, PATH:Bytes, "" ) => MerkleDelete ( TREE, PATH ) - rule MerklePut ( .MerkleTree, PATH:Bytes, VALUE ) => MerkleLeaf ( PATH, VALUE ) - - rule MerklePut ( MerkleLeaf ( LEAFPATH, _ ), PATH, VALUE ) - => MerkleLeaf( LEAFPATH, VALUE ) + rule MerklePut ( .MerkleTree, PATH, VALUE ) => MerkleLeaf( PATH, VALUE ) + rule MerklePut ( MerkleLeaf ( LEAFPATH, _ ), PATH, VALUE ) => MerkleLeaf( LEAFPATH, VALUE ) requires LEAFPATH ==K PATH rule MerklePut ( MerkleLeaf ( LEAFPATH, LEAFVALUE ), PATH, VALUE ) @@ -535,7 +532,7 @@ Merkle Tree Aux Functions ```k syntax Bytes ::= #nibbleize ( Bytes ) [klabel(#nibbleize), function] - | #byteify ( Bytes ) [klabel(#byteify), function] + | #byteify ( Bytes ) [klabel(#byteify ), function] // -------------------------------------------------------------------- rule #nibbleize ( B ) => ( #range( #asByteStack ( B [ 0 ] /Int 16 ), 0, 1 ) +Bytes ( #range( #asByteStack ( B [ 0 ] %Int 16 ), 0, 1 ) ) @@ -564,8 +561,8 @@ Merkle Tree Aux Functions rule HPEncodeAux ( X ) => 2 requires notBool X ==Int 0 syntax Map ::= #cleanBranchMap ( Map ) [klabel(#cleanBranchMap), function] - | #cleanBranchMapAux ( Map, List, Set ) [klabel(#cleanBranchMapAux), function] - // ------------------------------------------------------------------------------------------- + | #cleanBranchMapAux ( Map , List, Set ) [klabel(#cleanBranchMapAux), function] + // -------------------------------------------------------------------------------------------- rule #cleanBranchMap( M ) => #cleanBranchMapAux( M, keys_list(M), .Set ) rule #cleanBranchMapAux( M, .List, S ) => removeAll( M, S ) @@ -676,7 +673,7 @@ Tree Root Helper Functions rule #precompiledAccountsMapAux( (ListItem( ACCT ) => .List) _, M => M[#parseByteStack ( #unparseData( ACCT, 20 ) ) <- #emptyContractRLP] ) syntax Bytes ::= "#emptyContractRLP" [function] - // ------------------------------------------------ + // ----------------------------------------------- rule #emptyContractRLP => #rlpEncodeLength( #rlpEncodeInt(0) +Bytes #rlpEncodeInt(0) +Bytes #rlpEncodeBytes( #parseByteStack( Keccak256(b"\x80") ) ) diff --git a/package/version b/package/version index 18e96d5faf..67a3b03096 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.589 +1.0.590