From 4ac42c7e9bb9043eadd65751ed5e0ef2933584dd Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 21 Jan 2025 13:09:59 -0300 Subject: [PATCH 01/14] EIP-4844: Add DynamicFee transaction type --- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 14 +++++++++----- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 2 ++ .../kproj/evm-semantics/serialization.md | 6 +++++- .../kproj/evm-semantics/state-utils.md | 19 +++++++++++++++++++ 4 files changed, 35 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 9c1efd77d1..bb610c60f8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -442,6 +442,7 @@ Productions related to transactions | "Legacy" | "AccessList" | "DynamicFee" + | "Blob" // ------------------------------ syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function] @@ -449,20 +450,23 @@ Productions related to transactions rule #dasmTxPrefix (Legacy) => 0 rule #dasmTxPrefix (AccessList) => 1 rule #dasmTxPrefix (DynamicFee) => 2 + rule #dasmTxPrefix (Blob) => 3 syntax TxType ::= #asmTxPrefix ( Int ) [symbol(#asmTxPrefix), function] // ----------------------------------------------------------------------- rule #asmTxPrefix (0) => Legacy rule #asmTxPrefix (1) => AccessList rule #asmTxPrefix (2) => DynamicFee + rule #asmTxPrefix (3) => Blob - syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx + syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx // -------------------------------------------------------- - syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)] - | LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)] - syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] - syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] + syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)] + | LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)] + syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] + syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] + syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: Bytes ) [symbol(BlobTxData)] // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 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 9e8be97698..ddc04cf40c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -167,6 +167,8 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 // T_f 0 // T_m .TxType // T_x + 0 + .Bytes 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 13a582cb6c..7df1cf75aa 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -141,7 +141,8 @@ The encoding schemes are applied in `#rlpEcondeTxData`. rule #hashTxData( TXDATA ) => Keccak256raw( #rlpEncodeTxData(TXDATA) ) requires isLegacyTx (TXDATA) rule #hashTxData( TXDATA ) => Keccak256raw( b"\x01" +Bytes #rlpEncodeTxData(TXDATA) ) requires isAccessListTx(TXDATA) rule #hashTxData( TXDATA ) => Keccak256raw( b"\x02" +Bytes #rlpEncodeTxData(TXDATA) ) requires isDynamicFeeTx(TXDATA) -``` + rule #hashTxData( TXDATA ) => Keccak256raw( b"\x03" +Bytes #rlpEncodeTxData(TXDATA) ) requires isBlobTx (TXDATA) +``` The EVM test-sets are represented in JSON format with hex-encoding of the data and programs. Here we provide some standard parser/unparser functions for that format. @@ -349,6 +350,9 @@ Encoding rule #rlpEncodeTxData( DynamicFeeTxData(TN, TF, TM, TG, TT, TV, DATA, TC, [TA]) ) => #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] ) + + rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA], TB, TVH ] ) syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function] // --------------------------------------------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index 22410352e1..c521bafb93 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -426,6 +426,25 @@ The `"rlp"` key loads the block information. DynamicFee ... + + rule [[ #getTxData( TXID ) => BlobTxData(TN, TP, TF, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] + + TXID + TN + TP + TG + TT + TV + DATA + CID + TA + TP + TF + TB + TVH + Blob + ... + ``` - `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559 From 189b694650eca1b21e0285cd7e8fe8af2856c0a3 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 21 Jan 2025 13:21:42 -0300 Subject: [PATCH 02/14] Fix test-integrations --- tests/failing/ContractCreationSpam_d0g0v0.json.expected | 6 ++++++ ...allcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index cbb2b47964..0e4f7eb1d4 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -319,6 +319,12 @@ Legacy + + 0 + + + b"" + diff --git a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected index e8d4d81c45..5a4dc876c7 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -365,6 +365,12 @@ Legacy + + 0 + + + b"" + From 1aec9d43d9be6ce1b368820991aaf4af7ea1281b Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Tue, 21 Jan 2025 14:53:56 -0300 Subject: [PATCH 03/14] Set field `to` to be not `nil` in Blob transactions From the EIP specification: "The field `to` deviates slightly from the semantics with the exception that it *MUST NOT* be `nil` and therefore must always represent a 20-byte address. This means that blob transactions cannot have the form of a create transaction." --- .../src/kevm_pyk/kproj/evm-semantics/evm-types.md | 10 ++++++++-- .../kevm_pyk/kproj/evm-semantics/serialization.md | 15 +++++++++------ 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index bb610c60f8..b995f60cad 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -337,6 +337,8 @@ Bytes helper functions - `#asInteger` will interpret a stack of bytes as a single arbitrary-precision integer (with MSB first). - `#asAccount` will interpret a stack of bytes as a single account id (with MSB first). Differs from `#asWord` only in that an empty stack represents the empty account, not account zero. +- `asAccountNotNil` will interpret a stack of bytes as a single account id (with MSB first), but will fail if the + stack is empty. - `#asByteStack` will split a single word up into a `Bytes`. - `#range(WS, N, W)` access the range of `WS` beginning with `N` of width `W`. - `#padToWidth(N, WS)` and `#padRightToWidth` make sure that a `Bytes` is the correct size. @@ -350,11 +352,14 @@ Bytes helper functions // ------------------------------------------------------------------------- rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete] - syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function] + syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function] + syntax AccountNotNil ::= #asAccountNotNil ( Bytes ) [symbol(#asAccountNotNil), function] // ---------------------------------------------------------------------- rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0 rule #asAccount(BS) => #asWord(BS) [owise] + rule #asAccountNotNil(BS) => #asWord(BS) requires lengthBytes(BS) >Int 0 + syntax Bytes ::= #asByteStack ( Int ) [symbol(#asByteStack), function, total] // ----------------------------------------------------------------------------- rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete] @@ -385,6 +390,7 @@ Accounts ```k syntax Account ::= ".Account" | Int + syntax AccountNotNil ::= Int // ----------------------------------- syntax AccountCode ::= Bytes @@ -466,7 +472,7 @@ Productions related to transactions | LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)] syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] - syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: Bytes ) [symbol(BlobTxData)] + syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: Bytes ) [symbol(BlobTxData)] // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- endmodule 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 7df1cf75aa..1fb06a7cc7 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -229,15 +229,18 @@ Unparsing ``` - `#addrBytes` Takes an Account and represents it as a 20-byte wide Bytes (or an empty Bytes for a null address) +- `#addrBytesNotNil` Takes an Account and represents it as a 20-byte wide Bytes. It throws an error if the account is null. - `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes ```k - syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function] - | #wordBytes ( Int ) [symbol(#wordBytes), function] + syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function] + | #addrBytesNotNil ( AccountNotNil ) [symbol(#addrBytesNotNil), function] + | #wordBytes ( Int ) [symbol(#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) + rule #addrBytes(.Account) => .Bytes + rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT) + rule #addrBytesNotNil(ACCTNN) => #padToWidth(20, #asByteStack(ACCTNN)) requires #rangeAddress(ACCTNN) + rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD) ``` Recursive Length Prefix (RLP) @@ -352,7 +355,7 @@ Encoding => #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] ) rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) ) - => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA], TB, TVH ] ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, TVH ] ) syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function] // --------------------------------------------------------------------------------------------- From 71fb9fdc96a97f64100e636abb5efa517ae500c6 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 22 Jan 2025 15:39:48 -0300 Subject: [PATCH 04/14] Setting `txVersionedHashes` as `JSONs` Implementing parsing features for `txVersionedHashes` and `txMaxBlobFee` --- .../kevm_pyk/kproj/evm-semantics/driver.md | 16 ++++++- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- .../kproj/evm-semantics/serialization.md | 4 +- .../kproj/evm-semantics/state-utils.md | 47 ++++++++++++++----- .../ContractCreationSpam_d0g0v0.json.expected | 2 +- ...ecall_110_OOGMAfter_2_d0g0v0.json.expected | 2 +- 7 files changed, 56 insertions(+), 19 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index aec91f92b7..93b6deeb56 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -360,6 +360,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` rule loadTransaction _ { "s" : (TS:Bytes => #padToWidth(32, TS)), _ } ... requires lengthBytes(TS) loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes => #asWord(V)), _ } ... rule loadTransaction _ { "maxFeePerGas" : (V:Bytes => #asWord(V)), _ } ... + rule loadTransaction _ { "maxFeePerBlobGas" : (V:Bytes => #asWord(V)), _ } ... ``` ### Checking State @@ -545,7 +546,7 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : (_KEY : (VALUE:String => #parseByteStack(VALUE))) ... rule check "transactions" : ("to" : (VALUE:Bytes => #asAccount(VALUE))) ... rule check "transactions" : ( KEY : (VALUE:Bytes => #padToWidth(32, VALUE))) ... requires KEY in (SetItem("r") SetItem("s")) andBool lengthBytes(VALUE) check "transactions" : ( KEY : (VALUE:Bytes => #asWord(VALUE))) ... requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas")) + rule check "transactions" : ( KEY : (VALUE:Bytes => #asWord(VALUE))) ... requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas") SetItem("maxFeePerBlobGas")) rule check "transactions" : ("type" : (VALUE:Int => #asmTxPrefix(VALUE))) ... rule check "transactions" : "accessList" : [ ACCESSLIST , REST ] => check "transactions" : "accessList" : ACCESSLIST ~> check "transactions" : "accessList" : [ REST ] ... @@ -556,6 +557,11 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : "accessList" : [ .JSONs ] => .K ... rule check "transactions" : "accessList" : "address" : ADDR : "storageKeys" : KEY => .K ... ListItem(TXID) ... TXID TA ... requires isInAccessList(ADDR, KEY, TA) + + rule check "transactions" : "blobVersionedHashes" : [ .JSONs ] => .K ... + rule check "transactions" : "blobVersionedHashes" : [ VHASH, REST ] => check "transactions" : "blobVersionedHashes" : VHASH ~> check "transactions" : "blobVersionedHashes" : [ REST ] ... + rule check "transactions" : ("blobVersionedHashes" : VHASH ) => .K ... ListItem(TXID) ... TXID VH ... requires isInVersionedHashes(VHASH, VH) + rule check "transactions" : ("data" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("gasLimit" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("gasPrice" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... @@ -569,6 +575,7 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : ("type" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("maxFeePerGas" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("maxPriorityFeePerGas" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... + rule check "transactions" : ("maxFeePerBlobGas" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("sender" : VALUE) => .K ... ListItem(TXID) ... TXID TW TR TS ... B requires #sender( #getTxData(TXID), TW, TR, TS, B ) ==K VALUE syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function] @@ -583,6 +590,13 @@ Here we check the other post-conditions associated with an EVM test. rule isInAccessListStorage(KEY, [SKEY, REST]) => #if KEY ==Int #asWord(SKEY) #then true #else isInAccessListStorage(KEY, [REST]) #fi + + // Different from AccessList, Versioned Hashs doesn't contains a list of key-value jsons, but a list of strings finishing in .JSOns like [ "0x01...", "0x02", .JSONs] + syntax Bool ::= isInVersionedHashes(Bytes, JSON) [symbol(isInVersionedHashes), function] + rule isInVersionedHashes(_, [.JSONs]) => false + rule isInVersionedHashes(KEY, [SKEY, REST]) => #if KEY ==K SKEY + #then true + #else isInVersionedHashes(KEY, [REST]) #fi ``` TODO: case with nonzero ommers. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index b995f60cad..124566f191 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -472,7 +472,7 @@ Productions related to transactions | LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)] syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] - syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: Bytes ) [symbol(BlobTxData)] + syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: JSONs ) [symbol(BlobTxData)] // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 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 ddc04cf40c..e34628b74d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -168,7 +168,7 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 // T_m .TxType // T_x 0 - .Bytes + [ .JSONs ] 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 1fb06a7cc7..07524b6150 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -354,8 +354,8 @@ Encoding rule #rlpEncodeTxData( DynamicFeeTxData(TN, TF, TM, TG, TT, TV, DATA, TC, [TA]) ) => #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] ) - rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) ) - => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, TVH ] ) + rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, [TVH]) ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, [TVH] ] ) syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function] // --------------------------------------------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index c521bafb93..a61626e59c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -276,7 +276,8 @@ The `"rlp"` key loads the block information. , "nonce" : TN , "r" : TR , "s" : TS , "to" : TT , "v" : TW , "value" : TV , "type" : #dasmTxPrefix(Legacy) , "maxPriorityFeePerGas" : TP - , "maxFeePerGas": TP , .JSONs + , "maxFeePerGas": TP , "maxFeePerBlobGas" : 0 + , "blobVersionedHashes" : [ .JSONs ] , .JSONs } ~> load "transaction" : [ REST ] ... @@ -284,11 +285,12 @@ The `"rlp"` key loads the block information. rule load "transaction" : [ [TYPE , [TC, TN, TP, TG, TT, TV, TI, TA, TY , TR, TS ]] , REST ] => mkTX !ID:Int - ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP - , "nonce" : TN , "r" : TR , "s" : TS - , "to" : TT , "v" : TY , "value" : TV - , "accessList" : TA , "type" : TYPE , "chainID" : TC - , "maxPriorityFeePerGas" : TP , "maxFeePerGas": TP + ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP + , "nonce" : TN , "r" : TR , "s" : TS + , "to" : TT , "v" : TY , "value" : TV + , "accessList" : TA , "type" : TYPE , "chainID" : TC + , "maxPriorityFeePerGas" : TP , "maxFeePerGas" : TP + , "maxFeePerBlobGas" : 0 , "blobVersionedHashes" : [ .JSONs ] , .JSONs } ~> load "transaction" : [ REST ] @@ -303,13 +305,28 @@ The `"rlp"` key loads the block information. , "nonce" : TN , "r" : TR , "s" : TS , "to" : TT , "v" : TY , "value" : TV , "accessList" : TA , "type" : TYPE , "chainID" : TC - , "maxFeePerGas" : TF , .JSONs + , "maxFeePerGas" : TF , "maxFeePerBlobGas" : 0 + , "blobVersionedHashes" : [ .JSONs ] , .JSONs } ~> load "transaction" : [ REST ] ... requires #asWord(TYPE) ==Int #dasmTxPrefix(DynamicFee) + rule load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, TY, TVH, TB, TR, TS ]] , REST ] + => mkTX !ID:Int + ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP + , "nonce" : TN , "r" : TR , "s" : TS + , "to" : TT , "v" : TY , "value" : TV + , "accessList" : TA , "type" : TYPE , "chainID" : TC + , "maxFeePerGas" : TF , "maxFeePerBlobGas" : TB , "blobVersionedHashes" : TVH + , .JSONs + } + ~> load "transaction" : [ REST ] + ... + + requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob) + syntax EthereumCommand ::= "loadTransaction" Int JSON // ----------------------------------------------------- rule loadTransaction _ { .JSONs } => .K ... @@ -356,6 +373,12 @@ The `"rlp"` key loads the block information. rule loadTransaction TXID { "maxFeePerGas" : TF:Int, REST => REST } ... TXID _ => TF ... + + rule loadTransaction TXID { "maxFeePerBlobGas" : TB:Int, REST => REST } ... + TXID _ => TB ... + + rule loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... + TXID _ => [TVH] ... ``` ### Getting State @@ -427,7 +450,7 @@ The `"rlp"` key loads the block information. ... - rule [[ #getTxData( TXID ) => BlobTxData(TN, TP, TF, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] + rule [[ #getTxData( TXID ) => BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] TXID TN @@ -438,10 +461,10 @@ The `"rlp"` key loads the block information. DATA CID TA - TP - TF - TB - TVH + TPF + TM + TB + TVH Blob ... diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index 0e4f7eb1d4..d0a29be279 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -323,7 +323,7 @@ 0 - b"" + [ .JSONs ] diff --git a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected index 5a4dc876c7..2ad735c760 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -369,7 +369,7 @@ 0 - b"" + [ .JSONs ] From 969520f60b19c77536b1dcf3f4e54f1dc227bf7e Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 22 Jan 2025 16:10:56 -0300 Subject: [PATCH 05/14] Fromatting --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 124566f191..f7f7d9cd37 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -466,7 +466,7 @@ Productions related to transactions rule #asmTxPrefix (3) => Blob syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx - // -------------------------------------------------------- + // ----------------------------------------------------------------- syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)] | LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)] 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 07524b6150..036e9ac596 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -236,7 +236,7 @@ Unparsing syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function] | #addrBytesNotNil ( AccountNotNil ) [symbol(#addrBytesNotNil), function] | #wordBytes ( Int ) [symbol(#wordBytes), function] - // ---------------------------------------------------------------------- + // ---------------------------------------------------------------------------------------- rule #addrBytes(.Account) => .Bytes rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT) rule #addrBytesNotNil(ACCTNN) => #padToWidth(20, #asByteStack(ACCTNN)) requires #rangeAddress(ACCTNN) From c97e10e0705e22d1a99184f50776b732d3d2e17a Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 22 Jan 2025 17:15:01 -0300 Subject: [PATCH 06/14] Fixing `AccountNotNil` as an alias --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index f7f7d9cd37..e5bac2f2a2 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -390,7 +390,7 @@ Accounts ```k syntax Account ::= ".Account" | Int - syntax AccountNotNil ::= Int + syntax AccountNotNil = Int // ----------------------------------- syntax AccountCode ::= Bytes From d7c1f5a12266a8988ff579fe31156e98854d20c9 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:12:44 -0300 Subject: [PATCH 07/14] Fix typo MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index e47711fca2..595b31fc40 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -623,7 +623,7 @@ Here we check the other post-conditions associated with an EVM test. #then true #else isInAccessListStorage(KEY, [REST]) #fi - // Different from AccessList, Versioned Hashs doesn't contains a list of key-value jsons, but a list of strings finishing in .JSOns like [ "0x01...", "0x02", .JSONs] + // Different from AccessList, Versioned Hashs doesn't contains a list of key-value jsons, but a list of strings finishing in .JSONs like [ "0x01...", "0x02", .JSONs] syntax Bool ::= isInVersionedHashes(Bytes, JSON) [symbol(isInVersionedHashes), function] rule isInVersionedHashes(_, [.JSONs]) => false rule isInVersionedHashes(KEY, [SKEY, REST]) => #if KEY ==K SKEY From 31d7a6dcdb8a17ab3cba8bcf6ce71dd1b9244b91 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:13:14 -0300 Subject: [PATCH 08/14] Fix indentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md | 1 + 1 file changed, 1 insertion(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 595b31fc40..56f8ca56af 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -625,6 +625,7 @@ Here we check the other post-conditions associated with an EVM test. // Different from AccessList, Versioned Hashs doesn't contains a list of key-value jsons, but a list of strings finishing in .JSONs like [ "0x01...", "0x02", .JSONs] syntax Bool ::= isInVersionedHashes(Bytes, JSON) [symbol(isInVersionedHashes), function] + // --------------------------------------------------------------------------------------- rule isInVersionedHashes(_, [.JSONs]) => false rule isInVersionedHashes(KEY, [SKEY, REST]) => #if KEY ==K SKEY #then true From 5f518951bb0785be4b1daf0be844791619ebb2b2 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:13:32 -0300 Subject: [PATCH 09/14] Fix dash size MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index e5bac2f2a2..4da96f791a 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -354,7 +354,7 @@ Bytes helper functions syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function] syntax AccountNotNil ::= #asAccountNotNil ( Bytes ) [symbol(#asAccountNotNil), function] - // ---------------------------------------------------------------------- + // ---------------------------------------------------------------------------------------- rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0 rule #asAccount(BS) => #asWord(BS) [owise] From 3dc6e5ae8500660cf7bf59ca215c332a86e1b0ca Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:13:50 -0300 Subject: [PATCH 10/14] Fix dash size MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 4da96f791a..0ec7d405f5 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -449,7 +449,7 @@ Productions related to transactions | "AccessList" | "DynamicFee" | "Blob" - // ------------------------------ + // ------------------------ syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function] // ------------------------------------------------------------------------- From 3c4b3265af4c916820345f451e5073d1ad47f160 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:14:05 -0300 Subject: [PATCH 11/14] Fix dash size MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 0ec7d405f5..9b5a5d53f0 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -473,7 +473,7 @@ Productions related to transactions syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: JSONs ) [symbol(BlobTxData)] - // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- endmodule ``` From 7827f0887c6e5bdd0c7bbc8685152d0212b746de Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:16:24 -0300 Subject: [PATCH 12/14] Fix dash size MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 9b5a5d53f0..430f17b033 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -391,7 +391,7 @@ Accounts ```k syntax Account ::= ".Account" | Int syntax AccountNotNil = Int - // ----------------------------------- + // -------------------------- syntax AccountCode ::= Bytes // ---------------------------- From d0deb5dd2ee64f30dddd9123075147eac40051e5 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 11:32:42 -0300 Subject: [PATCH 13/14] Deleting `#addrBytesNotNil` and using `#addrBytes({TT}:>Account)` instead --- .../kevm_pyk/kproj/evm-semantics/serialization.md | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) 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 036e9ac596..795da4782c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -233,14 +233,12 @@ Unparsing - `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes ```k - syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function] - | #addrBytesNotNil ( AccountNotNil ) [symbol(#addrBytesNotNil), function] - | #wordBytes ( Int ) [symbol(#wordBytes), function] + syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function] + | #wordBytes ( Int ) [symbol(#wordBytes), function] // ---------------------------------------------------------------------------------------- - rule #addrBytes(.Account) => .Bytes - rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT) - rule #addrBytesNotNil(ACCTNN) => #padToWidth(20, #asByteStack(ACCTNN)) requires #rangeAddress(ACCTNN) - rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD) + 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) ``` Recursive Length Prefix (RLP) @@ -355,7 +353,7 @@ Encoding => #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] ) rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, [TVH]) ) - => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, [TVH] ] ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes({TT}:>Account), TV, DATA, [TA], TB, [TVH] ] ) syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function] // --------------------------------------------------------------------------------------------- From db28fabe4425ed6050f609b8c0b1ad05994112a6 Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 23 Jan 2025 12:24:15 -0300 Subject: [PATCH 14/14] Fix indentetion and dash size --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 795da4782c..f6ae417b26 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -235,10 +235,10 @@ Unparsing ```k syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function] | #wordBytes ( Int ) [symbol(#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) + rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT) + rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD) ``` Recursive Length Prefix (RLP)