diff --git a/Conform/Main.lean b/Conform/Main.lean index 6047341..ff4a5b6 100644 --- a/Conform/Main.lean +++ b/Conform/Main.lean @@ -36,32 +36,31 @@ open EvmYul.Conform in def log (testFile : System.FilePath) (testName : String) (result : TestResult) : IO Unit := IO.FS.withFile logFile .append λ h ↦ h.putStrLn s!"{testFile.fileName.get!}[{testName}] - {result}\n" - /- GeneralStateTests: - Cancun 2m59 - Total tests: 187 - The post was NOT equal to the resulting state: 65 - Succeeded: 122 - Success rate of: 65.240642 - - Pyspecs 22m35 - Total tests: 2150 - The post was NOT equal to the resulting state: 1695 - Succeeded: 455 - Success rate of: 21.162791 + Cancun + Total tests: 173 + The post was NOT equal to the resulting state: 5 + Succeeded: 168 + Success rate of: 97.109827 + + Pyspecs 24m14 + Total tests: 1549 + The post was NOT equal to the resulting state: 255 + Succeeded: 1294 + Success rate of: 83.537766 Shanghai 0m42 Total tests: 27 - The post was NOT equal to the resulting state: 23 - Succeeded: 4 - Success rate of: 14.814815 + The post was NOT equal to the resulting state: 5 + Succeeded: 22 + Success rate of: 81.481481 stArgsZeroOneBalance 1m47 Total tests: 96 - The post was NOT equal to the resulting state: 6 - Succeeded: 90 - Success rate of: 93.750000 + The post was NOT equal to the resulting state: 0 + Succeeded: 96 + Success rate of: 100.000000 stAttackTest 0m16 Total tests: 2 @@ -69,25 +68,25 @@ GeneralStateTests: Succeeded: 0 Success rate of: 0.000000 - stBadOpcode 75m51 + stBadOpcode ??m Total tests: 4249 - The post was NOT equal to the resulting state: 574 - Succeeded: 3675 - Success rate of: 86.490939 + The post was NOT equal to the resulting state: 1333 + Succeeded: 2916 + Success rate of: 68.627912 stBugs 0m23 Total tests: 9 - The post was NOT equal to the resulting state: 2 - Succeeded: 7 - Success rate of: 77.777778 + The post was NOT equal to the resulting state: 0 + Succeeded: 9 + Success rate of: 100.000000 stCallCodes - stCallCreateCallCodeTest 1m5 Total tests: 55 - The post was NOT equal to the resulting state: 22 - Succeeded: 33 - Success rate of: 60.000000 + The post was NOT equal to the resulting state: 8 + Succeeded: 47 + Success rate of: 85.454545 stCallDelegateCodesCallCodeHomestead - @@ -101,9 +100,9 @@ GeneralStateTests: stCodeCopyTest 0m16 Total tests: 2 - The post was NOT equal to the resulting state: 1 - Succeeded: 1 - Success rate of: 50.000000 + The post was NOT equal to the resulting state: 0 + Succeeded: 2 + Success rate of: 100.000000 stCodeSizeLimit 0m23 Total tests: 9 @@ -113,51 +112,51 @@ GeneralStateTests: stCreate2 3m10 Total tests: 183 - The post was NOT equal to the resulting state: 76 - Succeeded: 107 - Success rate of: 58.469945 + The post was NOT equal to the resulting state: 47 + Succeeded: 136 + Success rate of: 74.316940 stCreateTest 3m10 Total tests: 196 - The post was NOT equal to the resulting state: 107 - Succeeded: 89 - Success rate of: 45.408163 + The post was NOT equal to the resulting state: 80 + Succeeded: 116 + Success rate of: 59.183673 stDelegatecallTestHomestead 0m52 Total tests: 33 - The post was NOT equal to the resulting state: 26 - Succeeded: 7 - Success rate of: 21.212121 + The post was NOT equal to the resulting state: 6 + Succeeded: 27 + Success rate of: 81.818182 - stEIP150singleCodeGasPrices 8m11 + stEIP150singleCodeGasPrices 7m15 Total tests: 450 - The post was NOT equal to the resulting state: 336 - Succeeded: 114 - Success rate of: 25.333333 + The post was NOT equal to the resulting state: 49 + Succeeded: 401 + Success rate of: 89.111111 stEIP150Specific 0m38 Total tests: 23 - The post was NOT equal to the resulting state: 19 - Succeeded: 4 - Success rate of: 17.391304 + The post was NOT equal to the resulting state: 6 + Succeeded: 17 + Success rate of: 73.913043 stEIP1559 26m52 Total tests: 1845 - The post was NOT equal to the resulting state: 632 - Succeeded: 1213 - Success rate of: 65.745257 + The post was NOT equal to the resulting state: 238 + Succeeded: 1607 + Success rate of: 87.100271 stEIP158Specific 0m22 Total tests: 8 - The post was NOT equal to the resulting state: 7 - Succeeded: 1 - Success rate of: 12.500000 + The post was NOT equal to the resulting state: 5 + Succeeded: 3 + Success rate of: 37.500000 stEIP2930 1m50 Total tests: 140 - The post was NOT equal to the resulting state: 126 - Succeeded: 14 - Success rate of: 10.000000 + The post was NOT equal to the resulting state: 120 + Succeeded: 20 + Success rate of: 14.285714 stEIP3607 0m27 Total tests: 12 @@ -167,15 +166,15 @@ GeneralStateTests: stExample 0m53 Total tests: 39 - The post was NOT equal to the resulting state: 35 - Succeeded: 4 - Success rate of: 10.256410 + The post was NOT equal to the resulting state: 6 + Succeeded: 33 + Success rate of: 84.615385 stExtCodeHash 1m20 Total tests: 69 - The post was NOT equal to the resulting state: 66 - Succeeded: 3 - Success rate of: 4.347826 + The post was NOT equal to the resulting state: 52 + Succeeded: 17 + Success rate of: 24.637681 stHomesteadSpecific 0m19 Total tests: 5 @@ -185,21 +184,21 @@ GeneralStateTests: stInitCodeTest 0m37 Total tests: 22 - The post was NOT equal to the resulting state: 16 - Succeeded: 6 - Success rate of: 27.272727 + The post was NOT equal to the resulting state: 2 + Succeeded: 20 + Success rate of: 90.909091 stLogTests 1m2 Total tests: 46 - The post was NOT equal to the resulting state: 20 - Succeeded: 26 - Success rate of: 56.521739 + The post was NOT equal to the resulting state: 5 + Succeeded: 41 + Success rate of: 89.130435 stMemExpandingEIP150Calls 0m26 Total tests: 14 - The post was NOT equal to the resulting state: 13 - Succeeded: 1 - Success rate of: 7.142857 + The post was NOT equal to the resulting state: 6 + Succeeded: 8 + Success rate of: 57.142857 stMemoryStressTest 2m46 Total tests: 82 @@ -215,39 +214,39 @@ GeneralStateTests: stNonZeroCallsTest 0m38 Total tests: 24 - The post was NOT equal to the resulting state: 14 - Succeeded: 10 - Success rate of: 41.666667 + The post was NOT equal to the resulting state: 8 + Succeeded: 16 + Success rate of: 66.666667 - stPreCompiledContracts 14m47 - Total tests: 950 - The post was NOT equal to the resulting state: 758 - Succeeded: 192 - Success rate of: 20.210526 + stPreCompiledContracts 15m21 + Total tests: 894 + The post was NOT equal to the resulting state: 67 + Succeeded: 827 + Success rate of: 92.505593 - stPreCompiledContracts2 29m18 + stPreCompiledContracts2 56m40 Total tests: 226 - The post was NOT equal to the resulting state: 204 - Succeeded: 22 - Success rate of: 9.734513 + The post was NOT equal to the resulting state: 36 + Succeeded: 190 + Success rate of: 84.070796 - stQuadraticComplexityTest 0m41 + stQuadraticComplexityTest 6m32 Total tests: 32 - The post was NOT equal to the resulting state: 26 - Succeeded: 6 - Success rate of: 18.750000 + The post was NOT equal to the resulting state: 10 + Succeeded: 22 + Success rate of: 68.750000 stRandom 6m5 Total tests: 308 - The post was NOT equal to the resulting state: 54 - Succeeded: 254 - Success rate of: 82.467532 + The post was NOT equal to the resulting state: 6 + Succeeded: 302 + Success rate of: 98.051948 - stRandom2 4m1 - Total tests: 219 - The post was NOT equal to the resulting state: 13 - Succeeded: 206 - Success rate of: 94.063927 + stRandom2 3m50 + Total tests: 218 + The post was NOT equal to the resulting state: 6 + Succeeded: 212 + Success rate of: 97.247706 stRecursiveCreate 0m15 Total tests: 1 @@ -257,27 +256,27 @@ GeneralStateTests: stRefundTest 0m40 Total tests: 26 - The post was NOT equal to the resulting state: 10 - Succeeded: 16 - Success rate of: 61.538462 + The post was NOT equal to the resulting state: 5 + Succeeded: 21 + Success rate of: 80.769231 stReturnDataTest 4m56 - Total tests: 273 - The post was NOT equal to the resulting state: 44 - Succeeded: 229 - Success rate of: 83.882784 + Total tests: 269 + The post was NOT equal to the resulting state: 12 + Succeeded: 257 + Success rate of: 95.539033 stRevertTest 4m44 - Total tests: 262 - The post was NOT equal to the resulting state: 57 - Succeeded: 205 - Success rate of: 78.244275 + Total tests: 233 + The post was NOT equal to the resulting state: 23 + Succeeded: 210 + Success rate of: 90.128755 stSelfBalance 0m58 Total tests: 42 - The post was NOT equal to the resulting state: 39 - Succeeded: 3 - Success rate of: 7.142857 + The post was NOT equal to the resulting state: 1 + Succeeded: 41 + Success rate of: 97.619048 stShift 0m54 Total tests: 42 @@ -293,15 +292,15 @@ GeneralStateTests: stSolidityTest 0m38 Total tests: 23 - The post was NOT equal to the resulting state: 16 - Succeeded: 7 - Success rate of: 30.434783 + The post was NOT equal to the resulting state: 9 + Succeeded: 14 + Success rate of: 60.869565 stSpecialTest 0m35 Total tests: 20 - The post was NOT equal to the resulting state: 8 - Succeeded: 12 - Success rate of: 60.000000 + The post was NOT equal to the resulting state: 6 + Succeeded: 14 + Success rate of: 70.000000 stSStoreTest 9m10 Total tests: 475 @@ -311,27 +310,27 @@ GeneralStateTests: stStackTests 3m53 Total tests: 209 - The post was NOT equal to the resulting state: 144 - Succeeded: 65 - Success rate of: 31.100478 + The post was NOT equal to the resulting state: 1 + Succeeded: 208 + Success rate of: 99.521531 - stStaticCall 7m56 - Total tests: 469 - The post was NOT equal to the resulting state: 397 - Succeeded: 72 - Success rate of: 15.351812 + stStaticCall 15m39 + Total tests: 468 + The post was NOT equal to the resulting state: 55 + Succeeded: 413 + Success rate of: 88.247863 stStaticFlagEnabled 0m46 Total tests: 34 - The post was NOT equal to the resulting state: 34 - Succeeded: 0 - Success rate of: 0.000000 + The post was NOT equal to the resulting state: 9 + Succeeded: 25 + Success rate of: 73.529412 stSystemOperationsTest 1m41 Total tests: 83 - The post was NOT equal to the resulting state: 50 - Succeeded: 33 - Success rate of: 39.759036 + The post was NOT equal to the resulting state: 14 + Succeeded: 69 + Success rate of: 83.132530 stTimeConsuming 81m20 Total tests: 5190 @@ -347,33 +346,33 @@ GeneralStateTests: stTransitionTest 0m20 Total tests: 6 - The post was NOT equal to the resulting state: 3 - Succeeded: 3 - Success rate of: 50.000000 + The post was NOT equal to the resulting state: 0 + Succeeded: 6 + Success rate of: 100.000000 stWalletTest 0m58 Total tests: 41 - The post was NOT equal to the resulting state: 30 - Succeeded: 11 - Success rate of: 26.829268 + The post was NOT equal to the resulting state: 0 + Succeeded: 41 + Success rate of: 100.000000 stZeroCallsRevert 0m29 Total tests: 16 - The post was NOT equal to the resulting state: 3 - Succeeded: 13 - Success rate of: 81.250000 + The post was NOT equal to the resulting state: 0 + Succeeded: 16 + Success rate of: 100.000000 stZeroCallsTest 0m38 Total tests: 24 - The post was NOT equal to the resulting state: 14 - Succeeded: 10 - Success rate of: 41.666667 + The post was NOT equal to the resulting state: 12 + Succeeded: 12 + Success rate of: 50.000000 stZeroKnowledge 13m15 Total tests: 944 - The post was NOT equal to the resulting state: 568 - Succeeded: 376 - Success rate of: 39.830508 + The post was NOT equal to the resulting state: 411 + Succeeded: 533 + Success rate of: 56.461864 stZeroKnowledge2 9m40 Total tests: 519 @@ -383,44 +382,47 @@ GeneralStateTests: VMTests 9m16 Total tests: 571 - The post was NOT equal to the resulting state: 30 - Succeeded: 541 - Success rate of: 94.746060 + The post was NOT equal to the resulting state: 25 + Succeeded: 546 + Success rate of: 95.621716 -/ /- -InvalidBlocks 2m56 +InvalidBlocks 2m56 Total tests: 126 - The post was NOT equal to the resulting state: 98 - Succeeded: 28 - Success rate of: 22.222222 + The post was NOT equal to the resulting state: 4 + Succeeded: 122 + Success rate of: 96.825397 -/ /- -TransitionTests - Total tests: 17 - The post was NOT equal to the resulting state: 17 +TransitionTests 1m3 + Total tests: 0 + The post was NOT equal to the resulting state: 0 Succeeded: 0 - Success rate of: 0.000000 + Success rate of: NaN +^^^ No Cancun tests here -/ /- -ValidBlocks +ValidBlocks 15m40 Total tests: 437 - The post was NOT equal to the resulting state: 215 - Succeeded: 222 - Success rate of: 50.800915 + The post was NOT equal to the resulting state: 112 + Succeeded: 325 + Success rate of: 74.370709 -/ def directoryBlacklist : List System.FilePath := [ "EthereumTests/BlockchainTests/GeneralStateTests/stCallCodes" -- 86 tests , "EthereumTests/BlockchainTests/GeneralStateTests/stCallDelegateCodesCallCodeHomestead" -- 58 tests - , "EthereumTests/BlockchainTests/GeneralStateTests/stCallDelegateCodesHomestead" + , "EthereumTests/BlockchainTests/GeneralStateTests/stCallDelegateCodesHomestead" -- 58 tests ] def fileBlacklist : List System.FilePath := - [ "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_25000.json" - , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_20500.json" - , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexpRandomInput.json" - , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_35000.json" - , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_22000.json" - , "EthereumTests/BlockchainTests/GeneralStateTests/stRevertTest/RevertPrecompiledTouchExactOOG_Paris.json" + [ "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_25000.json" -- 4 + , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_20500.json" -- 4 + , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexpRandomInput.json" -- 6 + , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_35000.json" -- 4 + , "EthereumTests/BlockchainTests/GeneralStateTests/stPreCompiledContracts2/modexp_0_0_0_22000.json" -- 4 + , "EthereumTests/BlockchainTests/GeneralStateTests/stRevertTest/RevertPrecompiledTouch_nonce.json" -- 4 + , "EthereumTests/BlockchainTests/GeneralStateTests/stRevertTest/RevertPrecompiledTouch_noncestorage.json" -- 4 + , "EthereumTests/BlockchainTests/GeneralStateTests/stRevertTest/RevertPrecompiledTouch_storage_Paris.json" -- 4 ] def main : IO Unit := do @@ -447,7 +449,6 @@ def main : IO Unit := do let res ← ExceptT.run <| EvmYul.Conform.processTestsOfFile - -- (whitelist := #["opc2FDiffPlaces_d24g0v0_Cancun"]) -- (whitelist := #["add_d1g0v0_Cancun"]) -- (whitelist := #["add_d3g0v0_Cancun"]) -- (whitelist := #["add_d4g0v0_Cancun"]) diff --git a/Conform/Model.lean b/Conform/Model.lean index c7bd32d..ee96daf 100644 --- a/Conform/Model.lean +++ b/Conform/Model.lean @@ -5,6 +5,7 @@ import Lean.Data.Json import EvmYul.Operations import EvmYul.Wheels import EvmYul.State.Withdrawal +import EvmYul.State.Block import EvmYul.EVM.State @@ -91,17 +92,17 @@ TODO - Temporary. -/ private local instance : Repr Json := ⟨λ s _ ↦ Json.pretty s⟩ -structure BlockEntry := - blockHeader : BlockHeader - rlp : Json - transactions : Transactions - uncleHeaders : Json - withdrawals : Withdrawals - exception : String -- TODO - I am guessing there is a closed set of these to turn into a sum. - blocknumber : Nat - deriving Inhabited, Repr +-- structure BlockEntry := +-- blockHeader : BlockHeader +-- rlp : ByteArray +-- transactions : Transactions +-- ommers : Array BlockHeader +-- withdrawals : Withdrawals +-- exception : String -- TODO - I am guessing there is a closed set of these to turn into a sum. +-- -- blocknumber : Nat +-- deriving Inhabited, Repr -abbrev Blocks := Array BlockEntry +-- abbrev Blocks := Array BlockEntry /-- In theory, parts of the TestEntry could deserialise immediately into the underlying `EVM.State`. @@ -113,10 +114,10 @@ an EVM model and write translations between them where convenient. structure TestEntry := info : Json := "" blocks : Blocks - genesisBlockHeader : Json := "" + genesisBlockHeader : BlockHeader genesisRLP : Json := "" lastblockhash : Json := "" - network : Json := "" + network : String postState : Post pre : Pre sealEngine : Json := "" diff --git a/Conform/TestParser.lean b/Conform/TestParser.lean index 2af49d6..203b8bd 100644 --- a/Conform/TestParser.lean +++ b/Conform/TestParser.lean @@ -94,6 +94,7 @@ instance : FromJson BlockHeader where fromJson? json := do try pure { + hash := ← json.getObjValAsD! UInt256 "hash" parentHash := ← json.getObjValAsD! UInt256 "parentHash" ommersHash := TODO -- TODO - Set to whatever the KEC(RLP()) evaluates to. beneficiary := ← json.getObjValAsD! AccountAddress "coinbase" @@ -108,12 +109,14 @@ instance : FromJson BlockHeader where timestamp := ← json.getObjValAsD! _ "timestamp" <&> UInt256.toNat extraData := ← json.getObjValAsD! ByteArray "extraData" minHash := TODO -- TODO - Does not seem to be used in Υ? - chainId := 1 -- (5) + chainId := ← json.getObjValAsD UInt256 "chainId" 1 -- (5) nonce := 0 -- [deprecated] 0. baseFeePerGas := ← json.getObjValAsD! _ "baseFeePerGas" <&> UInt256.toNat parentBeaconBlockRoot := ← json.getObjValAsD! ByteArray "parentBeaconBlockRoot" prevRandao := ← json.getObjValAsD! UInt256 "mixHash" - withdrawalsRoot := ← json.getObjValAsD! ByteArray "withdrawalsRoot" + withdrawalsRoot := ← json.getObjValAsD! (Option ByteArray) "withdrawalsRoot" + blobGasUsed := ← json.getObjValAsD! (Option UInt256) "blobGasUsed" + excessBlobGas := ← json.getObjValAsD! (Option UInt256) "excessBlobGas" } catch exct => dbg_trace s!"OOOOPSIE: {exct}\n json: {json}" default @@ -140,17 +143,17 @@ TODO - Currently we return `AccessListTransaction`. No idea if this is what we w instance : FromJson Transaction where fromJson? json := do let baseTransaction : Transaction.Base := { - nonce := ← json.getObjValAsD! UInt256 "nonce" - gasLimit := ← json.getObjValAsD! UInt256 "gasLimit" - recipient := ← match json.getObjVal? "to" with - | .error _ => .ok .none - | .ok ok => do let str ← ok.getStr? - if str.isEmpty then .ok .none else FromJson.fromJson? str - value := ← json.getObjValAsD! UInt256 "value" - r := ← json.getObjValAsD! ByteArray "r" - s := ← json.getObjValAsD! ByteArray "s" - data := ← json.getObjValAsD! ByteArray "data" - dbgSender := ← json.getObjValAsD! AccountAddress "sender" + nonce := ← json.getObjValAsD! UInt256 "nonce" + gasLimit := ← json.getObjValAsD! UInt256 "gasLimit" + recipient := ← match json.getObjVal? "to" with + | .error _ => .ok .none + | .ok ok => do let str ← ok.getStr? + if str.isEmpty then .ok .none else FromJson.fromJson? str + value := ← json.getObjValAsD! UInt256 "value" + r := ← json.getObjValAsD! ByteArray "r" + s := ← json.getObjValAsD! ByteArray "s" + data := ← json.getObjValAsD! ByteArray "data" + expectedSender := ← json.getObjValAsD! AccountAddress "sender" } match json.getObjVal? "accessList" with @@ -170,13 +173,24 @@ instance : FromJson Transaction where -- dbg_trace "Constructing an access transaction." return .access ⟨baseTransaction, accessListTransaction, ⟨← FromJson.fromJson? gasPrice⟩⟩ | .error _ => - -- dbg_trace "Constructing an dynamic transaction." - return .dynamic ⟨ - baseTransaction, - accessListTransaction, - ← json.getObjValAsD! UInt256 "maxFeePerGas", - ← json.getObjValAsD! UInt256 "maxPriorityFeePerGas" - ⟩ + let dynamic : DynamicFeeTransaction := + ⟨ baseTransaction + , accessListTransaction + , ← json.getObjValAsD! UInt256 "maxFeePerGas" + , ← json.getObjValAsD! UInt256 "maxPriorityFeePerGas" + ⟩ + match json.getObjVal? "maxFeePerBlobGas" with + | .error _ => + pure <| .dynamic dynamic + | .ok maxFeePerBlobGas => + -- dbg_trace "Constructing a blob transaction." + pure <| + .blob + ⟨ dynamic + , ← FromJson.fromJson? maxFeePerBlobGas + , ← json.getObjValAsD! (List ByteArray) "blobVersionedHashes" + ⟩ + where accessListToRBMap (this : AccessList) : Batteries.RBMap AccountAddress (Array UInt256) compare := this.foldl (init := ∅) λ m ⟨addr, list⟩ ↦ m.insert addr list @@ -202,25 +216,26 @@ instance : FromJson Transaction where TODO - - `EthereumTests/BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_blob_tx_contract_creation.json` - ????? -/ -private def blockEntryOfJson (json : Json) : Except String BlockEntry := do +private def blockOfJson (json : Json) : Except String Block := do -- The exception, if exists, is always in the outermost object regardless of the `` (see this function's docs). let exception ← json.getObjValAsD! String "expectException" -- Descend to `rlp_decoded` - Format₁ if exists, Format₀ otherwise. let json ← json.getObjValAsD Json "rlp_decoded" json pure { - blockHeader := ← json.getObjValAsD! BlockHeader "blockHeader" - rlp := ← json.getObjValAsD! Json "rlp" + blockHeader := ← json.getObjValAsD! BlockHeader "blockHeader" + rlp := ← json.getObjValAsD! ByteArray "rlp" transactions := ← json.getObjValAsD! Transactions "transactions" - uncleHeaders := ← json.getObjValAsD! Json "uncleHeaders" - withdrawals := ← json.getObjValAsD! Withdrawals "withdrawals" - blocknumber := ← json.getObjValAsD _ "blocknumber" "1" >>= tryParseBlocknumber + ommers := ← json.getObjValAsD! (Array BlockHeader) "uncleHeaders" + withdrawals := ← json.getObjValAsD! Withdrawals "withdrawals" + -- The block's number should be in the header. + -- blocknumber := ← json.getObjValAsD _ "blocknumber" "1" >>= tryParseBlocknumber exception := exception } where tryParseBlocknumber (s : String) : Except String Nat := s.toNat?.elim (.error "Cannot parse `blocknumber`.") .ok -instance : FromJson BlockEntry := ⟨blockEntryOfJson⟩ +instance : FromJson Block := ⟨blockOfJson⟩ deriving instance FromJson for TestEntry diff --git a/Conform/TestRunner.lean b/Conform/TestRunner.lean index 17b89fa..ab39cbc 100644 --- a/Conform/TestRunner.lean +++ b/Conform/TestRunner.lean @@ -30,7 +30,6 @@ def VerySlowTests : Array String := , "TouchToEmptyAccountRevert2_Paris_d0g0v0_Cancun" , "stateRevert_d1g0v0_Cancun" , "RevertPrefoundEmptyOOG_Paris_d0g0v0_Cancun" - -- TODO: Are there multiple tests with this name? , "callcallcallcode_001_OOGMAfter_d0g0v0_Cancun" , "callcallcallcode_001_OOGMBefore_d0g0v0_Cancun" , "CreateOOGafterInitCodeRevert_d0g0v0_Cancun" @@ -86,7 +85,6 @@ def VerySlowTests : Array String := , "buffer_d33g0v0_Cancun" , "buffer_d36g0v0_Cancun" , "modexpTests_d120g0v0_Cancun" - -- TODO: revisit the following 9 , "precompsEIP2929Cancun_d22g0v0_Cancun" , "precompsEIP2929Cancun_d40g0v0_Cancun" -- TODO: It actually passes , "precompsEIP2929Cancun_d58g0v0_Cancun" @@ -96,23 +94,95 @@ def VerySlowTests : Array String := , "idPrecomps_d66g0v0_Cancun" , "idPrecomps_d5g0v0_Cancun" -- PANIC at unsafePerformIO EvmYul.PerformIO , "idPrecomps_d4g0v0_Cancun" - , "buffer_d21g0v0_Cancun" , "buffer_d33g0v0_Cancun" , "buffer_d36g0v0_Cancun" , "failed_tx_xcf416c53_Paris_d0g0v0_Cancun" , "CALLBlake2f_MaxRounds_d0g0v0_Cancun" - -- , "CallEcrecover_Overflow_d2g0v0_Cancun" -- PANIC at unsafePerformIO EvmYul.PerformIO , "19_oogUndoesTransientStore_d0g0v0_Cancun" , "20_oogUndoesTransientStoreInCall_d0g0v0_Cancun" - -- , "callcodecallcall_100_OOGMBefore_d0g0v0_Cancun" - -- , "callcodecallcodecallcode_111_OOGMBefore_d0g0v0_Cancun" - -- , "callcallcodecall_010_OOGE_d0g0v0_Cancun" - -- , "callcodecallcall_100_OOGMAfter_d0g0v0_Cancun" - -- , "callcodecall_10_OOGE_d0g0v0_Cancun" - -- , "callcodecallcode_11_OOGE_d0g0v0_Cancun" - -- , "callcallcodecallcode_011_OOGE_d0g0v0_Cancun" - -- , "callcallcode_01_OOGE_d0g0v0_Cancun" + , "modexp_modsize0_returndatasize_d2g0v0_Cancun" + , "modexp_modsize0_returndatasize_d3g0v0_Cancun" + , "modexp_modsize0_returndatasize_d4g0v0_Cancun" + , "static_CallEcrecover0_0input_d5g0v0_Cancun" + , "RevertPrecompiledTouch_Paris_d0g0v0_Cancun" + , "RevertPrecompiledTouch_Paris_d1g0v0_Cancun" + , "RevertPrecompiledTouch_Paris_d2g0v0_Cancun" + , "RevertPrecompiledTouch_Paris_d3g0v0_Cancun" + , "modexp_d15g3v0_Cancun" + , "modexp_d18g2v0_Cancun" + , "modexp_d15g2v0_Cancun" + , "modexp_d15g0v0_Cancun" + , "modexp_d16g2v0_Cancun" + , "modexp_d21g0v0_Cancun" + , "modexp_d15g1v0_Cancun" + , "modexp_d21g1v0_Cancun" + , "modexp_d21g2v0_Cancun" + , "RevertRemoteSubCallStorageOOG_d1g0v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d12g0v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d12g1v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d12g2v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d20g0v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d20g1v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d20g2v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d28g1v0_Cancun" -- index out of bounds + , "RevertPrecompiledTouchExactOOG_Paris_d28g0v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d28g2v0_Cancun" -- really? + , "RevertPrecompiledTouchExactOOG_Paris_d4g0v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d4g1v0_Cancun" + , "RevertPrecompiledTouchExactOOG_Paris_d4g2v0_Cancun" + , "modexp_d21g3v0_Cancun" + , "modexp_d22g0v0_Cancun" + , "modexp_d22g1v0_Cancun" + , "modexp_d22g2v0_Cancun" + , "modexp_d22g3v0_Cancun" + , "modexp_d28g0v0_Cancun" + , "modexp_d28g1v0_Cancun" + , "modexp_d28g2v0_Cancun" + , "modexp_d28g3v0_Cancun" + , "modexp_d29g0v0_Cancun" + , "modexp_d29g1v0_Cancun" + , "modexp_d29g2v0_Cancun" + , "modexp_d29g3v0_Cancun" + , "modexp_d2g0v0_Cancun" + , "modexp_d2g1v0_Cancun" + , "modexp_d2g2v0_Cancun" + , "modexp_d2g3v0_Cancun" + , "modexp_d30g0v0_Cancun" + , "modexp_d30g1v0_Cancun" + , "modexp_d30g2v0_Cancun" + , "modexp_d30g3v0_Cancun" + , "modexp_d36g2v0_Cancun" + , "modexp_d36g1v0_Cancun" + , "modexp_d36g0v0_Cancun" + , "modexp_d36g3v0_Cancun" + , "modexp_d37g1v0_Cancun" + , "modexp_d37g0v0_Cancun" + , "modexp_d37g2v0_Cancun" + , "modexp_d37g3v0_Cancun" + , "modexp_d9g1v0_Cancun" + , "modexp_d9g0v0_Cancun" + , "modexp_d9g3v0_Cancun" + , "modexp_d9g2v0_Cancun" + , "precompsEIP2929Cancun_d112g0v0_Cancun" + , "precompsEIP2929Cancun_d130g0v0_Cancun" + , "precompsEIP2929Cancun_d148g0v0_Cancun" + , "precompsEIP2929Cancun_d166g0v0_Cancun" + , "precompsEIP2929Cancun_d184g0v0_Cancun" + , "precompsEIP2929Cancun_d247g0v0_Cancun" + , "precompsEIP2929Cancun_d256g0v0_Cancun" + , "precompsEIP2929Cancun_d266g0v0_Cancun" + , "precompsEIP2929Cancun_d202g0v0_Cancun" + , "precompsEIP2929Cancun_d220g0v0_Cancun" + , "precompsEIP2929Cancun_d238g0v0_Cancun" + , "precompsEIP2929Cancun_d274g0v0_Cancun" + , "precompsEIP2929Cancun_d292g0v0_Cancun" + , "precompsEIP2929Cancun_d310g0v0_Cancun" + , "randomStatetest650_d0g0v0_Cancun" + , "src/GeneralStateTestsFiller/Pyspecs/byzantium/eip198_modexp_precompile/test_modexp.py::test_modexp[fork_Cancun-blockchain_test-EIP-198-case3-raw-input-out-of-gas]" + , "src/GeneralStateTestsFiller/Pyspecs/byzantium/eip198_modexp_precompile/test_modexp.py::test_modexp[fork_Cancun-blockchain_test-ModExpInput_base_-exponent_-modulus_-ExpectedOutput_call_return_code_0x01-returned_data_0x]" + , "src/GeneralStateTestsFiller/Pyspecs/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Cancun-precompile_5-blockchain_test-amount_1]" + , "src/GeneralStateTestsFiller/Pyspecs/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Cancun-precompile_5-blockchain_test-amount_0]" -- "sha3_d5g0v0_Cancun", -- best guess: `lookupMemoryRange'{'}{''}` are slow; I guess we will need an faster structure than Finmap -- "sha3_d6g0v0_Cancun" -- same problem as `sha3_d5g0v0_Cancun` I'm guessing ] @@ -201,7 +271,18 @@ end def executeTransaction (transaction : Transaction) (s : EVM.State) (header : BlockHeader) : Except EVM.Exception EVM.State := do let _TODOfuel := 2^13 - let (ypState, substate, z) ← EVM.Υ (debugMode := false) _TODOfuel s.accountMap header.chainId header.baseFeePerGas header transaction -- (dbgOverrideSender := transaction.base.dbgSender) + -- Validate transaction + match transaction with + | .blob t => + if header.blobGasUsed == none || header.excessBlobGas == none then .error (.InvalidTransaction .TYPE_3_TX_PRE_FORK) + match t.blobVersionedHashes with + | [] => .error (.InvalidTransaction .TYPE_3_TX_ZERO_BLOBS) + | hs => + if hs.any (λ h ↦ h[0]? != .some VERSIONED_HASH_VERSION_KZG) then + .error (.InvalidTransaction .TYPE_3_TX_ZERO_BLOBS) + | _ => pure () + + let (ypState, substate, z) ← EVM.Υ (debugMode := false) _TODOfuel s.accountMap header.chainId header.baseFeePerGas header transaction transaction.base.expectedSender -- as EIP 4788 (https://eips.ethereum.org/EIPS/eip-4788). @@ -217,14 +298,55 @@ def executeTransaction (transaction : Transaction) (s : EVM.State) (header : Blo /-- This assumes that the `transactions` are ordered, as they should be in the test suit. -/ -def executeTransactions (blocks : Blocks) (s₀ : EVM.State) : Except EVM.Exception EVM.State := do +def processBlocks (s₀ : EVM.State) : Except EVM.Exception EVM.State := do + let blocks := s₀.blocks + + -- Validate `excessBlobGas` + let parentHeaders := #[s₀.genesisBlockHeader] ++ blocks.map Block.blockHeader + let withParentHeaders := parentHeaders.zip blocks + withParentHeaders.forM + λ (parentHeader, block) ↦ do + if calcExcessBlobGas parentHeader != block.blockHeader.excessBlobGas then + if !block.exception.isEmpty then + let e : EVM.Exception := .BlockException_INCORRECT_EXCESS_BLOB_GAS + dbg_trace s!"Expected exception: {block.exception}; got exception: {repr e} - we need to reconcile these as we debug tests. Currently, we mark the test as 'passed' as I assume this is the right kind of exception, but it doesn't need to be the case necessarily." + throw <| EVM.Exception.ExpectedException block.exception + else + .error .BlockException_INCORRECT_EXCESS_BLOB_GAS + blocks.foldlM processBlock s₀ - where processBlock (s : EVM.State) (block : BlockEntry) : Except EVM.Exception EVM.State := do + where processBlock (s : EVM.State) (block : Block) : Except EVM.Exception EVM.State := do -- We should not check the timestamp. Some tests have timestamp less than 1710338135 but still need EIP-4788 -- let FORK_TIMESTAMP := 1710338135 let _TODOfuel := 2^13 - let SYSTEM_ADDRESS := 0xfffffffffffffffffffffffffffffffffffffffe - let BEACON_ROOTS_ADDRESS := 0x000F3df6D732807Ef1319fB7B8bB8522d0Beac02 + let SYSTEM_ADDRESS : AccountAddress := 0xfffffffffffffffffffffffffffffffffffffffe + let BEACON_ROOTS_ADDRESS : AccountAddress := 0x000F3df6D732807Ef1319fB7B8bB8522d0Beac02 + let MAX_BLOB_GAS_PER_BLOCK := 786432 + + -- dbg_trace s!"blobGasUsed: {block.blockHeader.blobGasUsed}, excessBlobGas: {block.blockHeader.excessBlobGas}" + match block.blockHeader.blobGasUsed, block.blockHeader.excessBlobGas with + | some _, none | none, some _ => + if !block.exception.isEmpty then + let e : EVM.Exception := .BlockException_INCORRECT_BLOCK_FORMAT + dbg_trace s!"Expected exception: {block.exception}; got exception: {repr e} - we need to reconcile these as we debug tests. Currently, we mark the test as 'passed' as I assume this is the right kind of exception, but it doesn't need to be the case necessarily." + throw <| EVM.Exception.ExpectedException block.exception + else + .error .BlockException_INCORRECT_BLOCK_FORMAT + | _, _ => pure () + + -- Validate `blobGasUsed` + let blobGasUsed := List.sum <| Array.data <| block.transactions.map ((Option.getD · 0) ∘ getTotalBlobGas) + match block.blockHeader.blobGasUsed with + | none => pure () + | some bGU => + if blobGasUsed != bGU || blobGasUsed > MAX_BLOB_GAS_PER_BLOCK then + if !block.exception.isEmpty then + let e : EVM.Exception := .BlockException_INCORRECT_BLOB_GAS_USED + dbg_trace s!"Expected exception: {block.exception}; got exception: {repr e} - we need to reconcile these as we debug tests. Currently, we mark the test as 'passed' as I assume this is the right kind of exception, but it doesn't need to be the case necessarily." + throw <| EVM.Exception.ExpectedException block.exception + else + .error .BlockException_INCORRECT_BLOB_GAS_USED + -- if no code exists at `BEACON_ROOTS_ADDRESS`, the call must fail silently let s ← match s.accountMap.find? BEACON_ROOTS_ADDRESS with @@ -236,6 +358,7 @@ def executeTransactions (blocks : Blocks) (s₀ : EVM.State) : Except EVM.Except EVM.Θ (debugMode := false) _TODOfuel + [] .empty s.accountMap default @@ -270,17 +393,20 @@ def executeTransactions (blocks : Blocks) (s₀ : EVM.State) : Except EVM.Except ) s let σ ← - ( try - applyWithdrawals - s.accountMap - block.blockHeader.withdrawalsRoot - block.withdrawals - catch e => - if !block.exception.isEmpty then - dbg_trace s!"Expected exception: {block.exception}; got exception: {repr e} - we need to reconcile these as we debug tests. Currently, we mark the test as 'passed' as I assume this is the right kind of exception, but it doesn't need to be the case necessarily." - throw <| EVM.Exception.ExpectedException block.exception - else throw e - ) + match block.blockHeader.withdrawalsRoot with + | some wR => + ( try + applyWithdrawals + s.accountMap + wR + block.withdrawals + catch e => + if !block.exception.isEmpty then + dbg_trace s!"Expected exception: {block.exception}; got exception: {repr e} - we need to reconcile these as we debug tests. Currently, we mark the test as 'passed' as I assume this is the right kind of exception, but it doesn't need to be the case necessarily." + throw <| EVM.Exception.ExpectedException block.exception + else throw e + ) + | none => pure s.accountMap pure <| { s with accountMap := σ } -- pure s @@ -290,9 +416,9 @@ def executeTransactions (blocks : Blocks) (s₀ : EVM.State) : Except EVM.Except NB we can throw away the final state if it coincided with the expected one, hence `.none`. -/ -def preImpliesPost (pre : Pre) (post : Post) (blocks : Blocks) : Except EVM.Exception (Option EVM.State) := do +def preImpliesPost (pre : Pre) (post : Post) (genesisBlockHeader : BlockHeader) (blocks : Blocks) : Except EVM.Exception (Option EVM.State) := do try - let resultState ← executeTransactions blocks pre.toEVMState + let resultState ← processBlocks {pre.toEVMState with blocks := blocks, genesisBlockHeader := genesisBlockHeader} let result : AddrMap AccountEntry := resultState.toState.accountMap.foldl (λ r addr ⟨nonce, balance, storage, _, _, code⟩ ↦ r.insert addr ⟨nonce, balance, storage, code⟩) default @@ -305,7 +431,6 @@ def preImpliesPost (pre : Pre) (post : Post) (blocks : Blocks) : Except EVM.Exce | e => throw e -- local instance : MonadLift (Except EVM.Exception) (Except Conform.Exception) := ⟨Except.mapError .EVMError⟩ - -- vvvvvvvvvvvvvv DO NOT DELETE PLEASE vvvvvvvvvvvvvvvvvv def DONOTDELETEMEFORNOW : AccountMap := Batteries.RBMap.ofList [(1, { dflt with storage := Batteries.RBMap.ofList [(44, 45), (46, 47)] compare }), (3, default)] compare where dflt : Account := default @@ -320,8 +445,8 @@ instance (priority := high) : Repr AccountMap := ⟨λ m _ ↦ result := result ++ s!"{sk} → {sv}\n" return result⟩ -def processTest (entry : TestEntry) (verbose : Bool := true) : TestResult := - let result := preImpliesPost entry.pre entry.postState entry.blocks +def processTest (entry : TestEntry) (verbose : Bool := true) : TestResult := do + let result := preImpliesPost entry.pre entry.postState entry.genesisBlockHeader entry.blocks match result with | .error err => .mkFailed s!"{repr err}" | .ok result => errorF <$> result @@ -341,11 +466,14 @@ def processTestsOfFile (file : System.FilePath) let path := file let file ← Lean.Json.fromFile file let test ← Lean.FromJson.fromJson? (α := Test) file - -- dbg_trace s!"tests before guard: {test.toTests.map Prod.fst}" - let tests := guardBlacklist ∘ guardWhitelist <| test.toTests + let tests := test.toTests + let cancunTests := guardCancum tests + -- dbg_trace s!"Non Cancun tests ignored: {tests.length - cancunTests.length}" + let tests := guardBlacklist ∘ guardWhitelist <| cancunTests -- dbg_trace s!"tests after guard: {tests.map Prod.fst}" tests.foldlM (init := ∅) λ acc (testname, test) ↦ -- dbg_trace s!"TESTING {testname} FROM {path}" + -- dbg_trace s!"network : {test.network}" pure <| acc.insert testname (processTest test) -- try -- processTest test >>= pure ∘ @@ -360,6 +488,8 @@ def processTestsOfFile (file : System.FilePath) if whitelist.isEmpty then tests else tests.filter (λ (name, _) ↦ name ∈ whitelist) guardBlacklist (tests : List (String × TestEntry)) := tests.filter (λ (name, _) ↦ name ∉ GlobalBlacklist ++ blacklist) + guardCancum (tests : List (String × TestEntry)) := + tests.filter (λ (_, test) ↦ test.network.take 6 == "Cancun") end Conform diff --git a/EthereumTests b/EthereumTests index 08839f5..87df47a 160000 --- a/EthereumTests +++ b/EthereumTests @@ -1 +1 @@ -Subproject commit 08839f54ebdeb808ff4171a7ddb8803dfa8963a8 +Subproject commit 87df47ae335bfdd7a106158ade8fa8ff1a33d51b diff --git a/EvmYul/EVM/Exception.lean b/EvmYul/EVM/Exception.lean index ab129a5..716d793 100644 --- a/EvmYul/EVM/Exception.lean +++ b/EvmYul/EVM/Exception.lean @@ -1,4 +1,4 @@ -import EvmYul.EVM.State +import EvmYul.Wheels namespace EvmYul @@ -12,7 +12,9 @@ inductive InvalidTransactionException where | UpFrontPayment : InvalidTransactionException | BaseFeeTooHigh : InvalidTransactionException | InconsistentFees : InvalidTransactionException - | DataGreaterThan9152 : InvalidTransactionException + | InitCodeDataGreaterThan49152 : InvalidTransactionException + | TYPE_3_TX_ZERO_BLOBS : InvalidTransactionException + | TYPE_3_TX_PRE_FORK : InvalidTransactionException instance : Repr InvalidTransactionException where reprPrec s _ := @@ -24,7 +26,9 @@ instance : Repr InvalidTransactionException where | .UpFrontPayment => "UpFrontPayment" | .BaseFeeTooHigh => "BaseFeeTooHigh" | .InconsistentFees => "InconsistentFees" - | .DataGreaterThan9152 => "DataGreaterThan9152" + | .InitCodeDataGreaterThan49152 => "InitCodeDataGreaterThan49152" + | .TYPE_3_TX_ZERO_BLOBS => "TYPE_3_TX_ZERO_BLOBS" + | .TYPE_3_TX_PRE_FORK => "TYPE_3_TX_PRE_FORK" -- TODO - fix / cleanup. inductive Exception where @@ -37,7 +41,7 @@ inductive Exception where | ReceiverMustExistWithNonZeroValue : Exception | Underflow : Exception | Overflow : Exception - | StopInvoked (s : EVM.State) : Exception + -- | StopInvoked (s : EVM.State) : Exception | OutOfFuel : Exception | OutOfGass : Exception | InvalidTransaction : @@ -47,6 +51,9 @@ inductive Exception where | BogusExceptionToBeReplaced (s : String) : Exception | ExpectedException (s : String) : Exception | SenderRecoverError : String → Exception + | BlockException_INCORRECT_EXCESS_BLOB_GAS : Exception + | BlockException_INCORRECT_BLOB_GAS_USED : Exception + | BlockException_INCORRECT_BLOCK_FORMAT instance : Repr Exception where reprPrec s _ := match s with @@ -59,7 +66,7 @@ instance : Repr Exception where | .ReceiverMustExistWithNonZeroValue => "ReceiverMustExistWithNonZeroValue" | .Underflow => "Underflow" | .Overflow => "Overflow" - | .StopInvoked _ => "Execution halted by STOP." + -- | .StopInvoked _ => "Execution halted by STOP." | .OutOfFuel => "OutOfFuel" | .OutOfGass => "OutOfGass" | .InvalidTransaction e => "InvalidTransaction: " ++ repr e @@ -69,6 +76,9 @@ instance : Repr Exception where | .BogusExceptionToBeReplaced s => s!"BogusExceptionToBeReplaced: {s}" | .ExpectedException s => s!"Expected exception: {s}" | .SenderRecoverError s => "SenderRecoverError: " ++ s + | .BlockException_INCORRECT_EXCESS_BLOB_GAS => "BlockException_INCORRECT_EXCESS_BLOB_GAS" + | .BlockException_INCORRECT_BLOB_GAS_USED => "BlockException_INCORRECT_BLOB_GAS_USED" + | .BlockException_INCORRECT_BLOCK_FORMAT => "BlockException_INCORRECT_BLOCK_FORMAT" end EVM diff --git a/EvmYul/EVM/Gas.lean b/EvmYul/EVM/Gas.lean index 0cab9cb..59c4dde 100644 --- a/EvmYul/EVM/Gas.lean +++ b/EvmYul/EVM/Gas.lean @@ -1,8 +1,4 @@ -import EvmYul.Maps.YPState -import EvmYul.MachineState -import EvmYul.State.Substate -import EvmYul.State.ExecutionEnv -import EvmYul.EVM.Exception +import EvmYul.EVM.State import EvmYul.StateOps namespace EvmYul @@ -53,6 +49,7 @@ def Gkeccak256 : ℕ := 30 def Gkeccak256word : ℕ := 6 def Gcopy : ℕ := 3 def Gblockhash : ℕ := 20 +def HASH_OPCODE_GAS : ℕ := 3 end FeeSchedule @@ -65,7 +62,7 @@ def Wzero : List (Operation .EVM) := [.STOP, .RETURN, .REVERT] def Wbase : List (Operation .EVM) := [ .ADDRESS, .ORIGIN, .CALLER, .CALLVALUE, .CALLDATASIZE, .CODESIZE, .GASPRICE, .COINBASE, .TIMESTAMP, .NUMBER, .PREVRANDAO, .GASLIMIT, .CHAINID, .RETURNDATASIZE, .POP, .PC, .MSIZE, .GAS, - .BASEFEE, .PUSH0] + .BASEFEE, .BLOBBASEFEE, .PUSH0] def Wverylow : List (Operation .EVM) := [ .ADD, .SUB, .NOT, .LT, .GT, .SLT, .SGT, .EQ, .ISZERO, .AND, .OR, .XOR, .BYTE, .SHL, .SHR, .SAR, @@ -139,7 +136,7 @@ with the definition of `C_<>` functions that are described inline along with the It would be worth restructing everything to obtain cleaner separation of concerns. -/ -def Csstore (s : State) : Except EVM.Exception UInt256 := do +def Csstore (s : EVM.State) : Except EVM.Exception UInt256 := do let { stack := μₛ, accountMap := σ, executionEnv.codeOwner := Iₐ, .. } := s let .some { storage := σ, ostorage := σ₀, .. } := σ.find? Iₐ | throw .SenderMustExist let storeAddr := μₛ[0]! @@ -193,32 +190,33 @@ def Ctload : UInt256 := -/ def L (n : UInt256) := n.val - (n.val / 64) -/-- -NB Assumes stack coherence. --/ -def Ccall (μₛ : Stack UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) : UInt256 := - Cgascap σ μ μₛ A + Cextra σ μₛ A - where - /- - NB Slightly redundant as we could reference the `Ccall` parameters directly, - but this is a bit closer to the YP for now. - -/ - t := AccountAddress.ofUInt256 μₛ[1]! +def Cnew (t : AccountAddress) (val : UInt256) (σ : AccountMap) := + if EvmYul.State.dead σ t && val != 0 then Gnewaccount else 0 - Cnew (σ : AccountMap) (μₛ : Stack UInt256) := - if EvmYul.State.dead σ t && μₛ[2]! != 0 then Gnewaccount else 0 +def Cxfer (val : UInt256) : ℕ := + if val != 0 then Gcallvalue else 0 - Cxfer (μₛ : Stack UInt256) := - if μₛ[2]! != 0 then Gcallvalue else 0 +def Cextra (t : AccountAddress) (val : UInt256) (σ : AccountMap) (A : Substate) := + Caccess t A + Cxfer val + Cnew t val σ - Cextra (σ : AccountMap) (μₛ : Stack UInt256) (A : Substate) := - Caccess t A + Cxfer μₛ + Cnew σ μₛ +def Cgascap (t : AccountAddress) (val g : UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) := + if μ.gasAvailable >= Cextra t val σ A then + -- dbg_trace s!"gasAvailable {μ.gasAvailable} >= Cextra {Cextra σ μₛ A}" + min (L (μ.gasAvailable - Cextra t val σ A)) g + else + g - Cgascap (σ : AccountMap) (μ : MachineState) (μₛ : Stack UInt256) (A : Substate) := - if μ.gasAvailable >= Cextra σ μₛ A then min (L (μ.gasAvailable - Cextra σ μₛ A)) μₛ[0]! else μₛ[0]! +def Ccallgas (t : AccountAddress) (val g : UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) : UInt256 := + match val with + | 0 => Cgascap t val g σ μ A + | _ => Cgascap t val g σ μ A + GasConstants.Gcallstipend - Ccallgas (σ : AccountMap) (μₛ : Stack UInt256) (A : Substate) := - if μₛ[2]! != 0 then Cgascap σ μ μₛ A + Gcallstipend else Cgascap σ μ μₛ A +/-- +NB Assumes stack coherence. +-/ +def Ccall (t : AccountAddress) (val g : UInt256) (σ : AccountMap) (μ : MachineState) (A : Substate) : UInt256 := + -- dbg_trace s!"Ccall: {Cgascap μₛ σ μ A} + {Cextra σ μₛ A}" + Ccallgas t val g σ μ A + Cextra t val σ A /-- (65) @@ -251,10 +249,20 @@ private def C' (s : State) (instr : Operation .EVM) : Except EVM.Exception UInt2 | .SLOAD => return Csload μₛ A I | .TLOAD => return Ctload | .BLOCKHASH => return Gblockhash + /- + By `μₛ[2]` the YP means the value that is to be transferred, + not what happens to be on the stack at index 2. Therefore it is 0 for + `DELEGATECALL` and `STATICCALL`. + -/ + | .CALL => return Ccall (AccountAddress.ofUInt256 μₛ[1]!) μₛ[2]! μₛ[0]! σ μ A + | .CALLCODE => return Ccall (AccountAddress.ofUInt256 μₛ[1]!) μₛ[2]! μₛ[0]! σ μ A + | .DELEGATECALL => return Ccall (AccountAddress.ofUInt256 μₛ[1]!) 0 μₛ[0]! σ μ A + | .STATICCALL => return Ccall (AccountAddress.ofUInt256 μₛ[1]!) 0 μₛ[0]! σ μ A + | .BLOBHASH => return HASH_OPCODE_GAS | w => pure <| if w ∈ Wcopy then Gverylow + Gcopy * (μₛ[2]! / 32 : ℚ).ceil else if w ∈ Wextaccount then Caccess (AccountAddress.ofUInt256 μₛ[0]!) A else - if w ∈ Wcall then Ccall μₛ σ μ A else + -- if w ∈ Wcall then Ccall μₛ σ μ A else if w ∈ Wzero then Gzero else if w ∈ Wbase then Gbase else if w ∈ Wverylow then Gverylow else diff --git a/EvmYul/EVM/Instr.lean b/EvmYul/EVM/Instr.lean index c9f6414..de2c584 100644 --- a/EvmYul/EVM/Instr.lean +++ b/EvmYul/EVM/Instr.lean @@ -67,6 +67,8 @@ def serializeBlockInstr : BOp .EVM → UInt8 | .CHAINID => 0x46 | .SELFBALANCE => 0x47 | .BASEFEE => 0x48 + | .BLOBHASH => 0x49 + | .BLOBBASEFEE => 0x4a def serializeStackMemFlowInstr : SMSFOp .EVM → UInt8 | .POP => 0x50 @@ -188,235 +190,239 @@ def serializeInstr : Operation .EVM → UInt8 | .Log l => serializeLogInstr l | .System s => serializeSysInstr s - def δ : Operation .EVM → Option ℕ - | .STOP => some 0 - | .ADD => some 2 - | .MUL => some 2 - | .SUB => some 2 - | .DIV => some 2 - | .SDIV => some 2 - | .MOD => some 2 - | .SMOD => some 2 - | .ADDMOD => some 3 - | .MULMOD => some 3 - | .EXP => some 2 - | .SIGNEXTEND => some 2 - | .LT => some 2 - | .GT => some 2 - | .SLT => some 2 - | .SGT => some 2 - | .EQ => some 2 - | .ISZERO => some 1 - | .AND => some 2 - | .OR => some 2 - | .XOR => some 2 - | .NOT => some 1 - | .BYTE => some 2 - | .SHL => some 2 - | .SHR => some 2 - | .SAR => some 2 - | .KECCAK256 => some 2 - | .ADDRESS => some 0 - | .BALANCE => some 1 - | .ORIGIN => some 0 - | .CALLER => some 0 - | .CALLVALUE => some 0 - | .CALLDATALOAD => some 1 - | .CALLDATASIZE => some 0 - | .CALLDATACOPY => some 3 - | .CODESIZE => some 0 - | .CODECOPY => some 3 - | .GASPRICE => some 0 - | .EXTCODESIZE => some 4 - | .EXTCODECOPY => some 4 - | .RETURNDATASIZE => some 0 - | .RETURNDATACOPY => some 3 - | .EXTCODEHASH => some 1 - | .BLOCKHASH => some 1 - | .COINBASE => some 0 - | .TIMESTAMP => some 0 - | .NUMBER => some 0 - | .PREVRANDAO => some 0 - | .GASLIMIT => some 0 - | .CHAINID => some 0 - | .SELFBALANCE => some 0 - | .BASEFEE => some 0 - | .POP => some 1 - | .MLOAD => some 1 - | .MSTORE => some 2 - | .MSTORE8 => some 1 - | .SLOAD => some 1 - | .SSTORE => some 2 - | .PC => some 0 - | .MSIZE => some 0 - | .GAS => some 0 - | .Push _ => some 0 - | .DUP1 => some 1 - | .DUP2 => some 2 - | .DUP3 => some 3 - | .DUP4 => some 4 - | .DUP5 => some 5 - | .DUP6 => some 6 - | .DUP7 => some 7 - | .DUP8 => some 8 - | .DUP9 => some 9 - | .DUP10 => some 10 - | .DUP11 => some 11 - | .DUP12 => some 12 - | .DUP13 => some 13 - | .DUP14 => some 14 - | .DUP15 => some 15 - | .DUP16 => some 16 - | .SWAP1 => some 2 - | .SWAP2 => some 3 - | .SWAP3 => some 4 - | .SWAP4 => some 5 - | .SWAP5 => some 6 - | .SWAP6 => some 7 - | .SWAP7 => some 8 - | .SWAP8 => some 9 - | .SWAP9 => some 10 - | .SWAP10 => some 11 - | .SWAP11 => some 12 - | .SWAP12 => some 13 - | .SWAP13 => some 14 - | .SWAP14 => some 15 - | .SWAP15 => some 16 - | .SWAP16 => some 17 - | .LOG0 => some 2 - | .LOG1 => some 3 - | .LOG2 => some 4 - | .LOG3 => some 5 - | .LOG4 => some 6 - | .JUMP => some 1 - | .JUMPI => some 2 - | .JUMPDEST => some 0 - | .TLOAD => some 1 - | .TSTORE => some 2 - | .MCOPY => some 3 - | .CREATE => some 3 - | .CALL => some 7 - | .CALLCODE => some 7 - | .RETURN => some 2 - | .DELEGATECALL => some 6 - | .CREATE2 => some 4 - | .STATICCALL => some 6 - | .REVERT => some 2 - | .INVALID => none - | .SELFDESTRUCT => some 1 +def δ : Operation .EVM → Option ℕ + | .STOP => some 0 + | .ADD => some 2 + | .MUL => some 2 + | .SUB => some 2 + | .DIV => some 2 + | .SDIV => some 2 + | .MOD => some 2 + | .SMOD => some 2 + | .ADDMOD => some 3 + | .MULMOD => some 3 + | .EXP => some 2 + | .SIGNEXTEND => some 2 + | .LT => some 2 + | .GT => some 2 + | .SLT => some 2 + | .SGT => some 2 + | .EQ => some 2 + | .ISZERO => some 1 + | .AND => some 2 + | .OR => some 2 + | .XOR => some 2 + | .NOT => some 1 + | .BYTE => some 2 + | .SHL => some 2 + | .SHR => some 2 + | .SAR => some 2 + | .KECCAK256 => some 2 + | .ADDRESS => some 0 + | .BALANCE => some 1 + | .ORIGIN => some 0 + | .CALLER => some 0 + | .CALLVALUE => some 0 + | .CALLDATALOAD => some 1 + | .CALLDATASIZE => some 0 + | .CALLDATACOPY => some 3 + | .CODESIZE => some 0 + | .CODECOPY => some 3 + | .GASPRICE => some 0 + | .EXTCODESIZE => some 1 + | .EXTCODECOPY => some 4 + | .RETURNDATASIZE => some 0 + | .RETURNDATACOPY => some 3 + | .EXTCODEHASH => some 1 + | .BLOCKHASH => some 1 + | .COINBASE => some 0 + | .TIMESTAMP => some 0 + | .NUMBER => some 0 + | .PREVRANDAO => some 0 + | .GASLIMIT => some 0 + | .CHAINID => some 0 + | .SELFBALANCE => some 0 + | .BASEFEE => some 0 + | .BLOBHASH => some 1 + | .BLOBBASEFEE => some 0 + | .POP => some 1 + | .MLOAD => some 1 + | .MSTORE => some 2 + | .MSTORE8 => some 1 + | .SLOAD => some 1 + | .SSTORE => some 2 + | .PC => some 0 + | .MSIZE => some 0 + | .GAS => some 0 + | .Push _ => some 0 + | .DUP1 => some 1 + | .DUP2 => some 2 + | .DUP3 => some 3 + | .DUP4 => some 4 + | .DUP5 => some 5 + | .DUP6 => some 6 + | .DUP7 => some 7 + | .DUP8 => some 8 + | .DUP9 => some 9 + | .DUP10 => some 10 + | .DUP11 => some 11 + | .DUP12 => some 12 + | .DUP13 => some 13 + | .DUP14 => some 14 + | .DUP15 => some 15 + | .DUP16 => some 16 + | .SWAP1 => some 2 + | .SWAP2 => some 3 + | .SWAP3 => some 4 + | .SWAP4 => some 5 + | .SWAP5 => some 6 + | .SWAP6 => some 7 + | .SWAP7 => some 8 + | .SWAP8 => some 9 + | .SWAP9 => some 10 + | .SWAP10 => some 11 + | .SWAP11 => some 12 + | .SWAP12 => some 13 + | .SWAP13 => some 14 + | .SWAP14 => some 15 + | .SWAP15 => some 16 + | .SWAP16 => some 17 + | .LOG0 => some 2 + | .LOG1 => some 3 + | .LOG2 => some 4 + | .LOG3 => some 5 + | .LOG4 => some 6 + | .JUMP => some 1 + | .JUMPI => some 2 + | .JUMPDEST => some 0 + | .TLOAD => some 1 + | .TSTORE => some 2 + | .MCOPY => some 3 + | .CREATE => some 3 + | .CALL => some 7 + | .CALLCODE => some 7 + | .RETURN => some 2 + | .DELEGATECALL => some 6 + | .CREATE2 => some 4 + | .STATICCALL => some 6 + | .REVERT => some 2 + | .INVALID => none + | .SELFDESTRUCT => some 1 - def α : Operation .EVM → Option ℕ - | .STOP => some 0 - | .ADD => some 1 - | .MUL => some 1 - | .SUB => some 1 - | .DIV => some 1 - | .SDIV => some 1 - | .MOD => some 1 - | .SMOD => some 1 - | .ADDMOD => some 1 - | .MULMOD => some 1 - | .EXP => some 1 - | .SIGNEXTEND => some 1 - | .LT => some 1 - | .GT => some 1 - | .SLT => some 1 - | .SGT => some 1 - | .EQ => some 1 - | .ISZERO => some 1 - | .AND => some 1 - | .OR => some 1 - | .XOR => some 1 - | .NOT => some 1 - | .BYTE => some 1 - | .SHL => some 1 - | .SHR => some 1 - | .SAR => some 1 - | .KECCAK256 => some 1 - | .ADDRESS => some 1 - | .BALANCE => some 1 - | .ORIGIN => some 1 - | .CALLER => some 1 - | .CALLVALUE => some 1 - | .CALLDATALOAD => some 1 - | .CALLDATASIZE => some 1 - | .CALLDATACOPY => some 0 - | .CODESIZE => some 1 - | .CODECOPY => some 0 - | .GASPRICE => some 1 - | .EXTCODESIZE => some 1 - | .EXTCODECOPY => some 0 - | .RETURNDATASIZE => some 1 - | .RETURNDATACOPY => some 0 - | .EXTCODEHASH => some 1 - | .BLOCKHASH => some 1 - | .COINBASE => some 1 - | .TIMESTAMP => some 1 - | .NUMBER => some 1 - | .PREVRANDAO => some 1 - | .GASLIMIT => some 1 - | .CHAINID => some 1 - | .SELFBALANCE => some 1 - | .BASEFEE => some 1 - | .POP => some 0 - | .MLOAD => some 1 - | .MSTORE => some 0 - | .MSTORE8 => some 0 - | .SLOAD => some 1 - | .SSTORE => some 0 - | .PC => some 1 - | .MSIZE => some 1 - | .GAS => some 1 - | .JUMP => some 0 - | .JUMPI => some 0 - | .JUMPDEST => some 0 - | .TLOAD => some 1 - | .TSTORE => some 0 - | .MCOPY => some 0 - | .Push _ => some 1 - | .DUP1 => some 2 - | .DUP2 => some 3 - | .DUP3 => some 4 - | .DUP4 => some 5 - | .DUP5 => some 6 - | .DUP6 => some 7 - | .DUP7 => some 8 - | .DUP8 => some 9 - | .DUP9 => some 10 - | .DUP10 => some 11 - | .DUP11 => some 12 - | .DUP12 => some 13 - | .DUP13 => some 14 - | .DUP14 => some 15 - | .DUP15 => some 16 - | .DUP16 => some 16 - | .SWAP1 => some 2 - | .SWAP2 => some 3 - | .SWAP3 => some 4 - | .SWAP4 => some 5 - | .SWAP5 => some 6 - | .SWAP6 => some 7 - | .SWAP7 => some 8 - | .SWAP8 => some 9 - | .SWAP9 => some 10 - | .SWAP10 => some 11 - | .SWAP11 => some 12 - | .SWAP12 => some 13 - | .SWAP13 => some 14 - | .SWAP14 => some 15 - | .SWAP15 => some 16 - | .SWAP16 => some 17 - | .Log _ => some 0 - | .CREATE => some 1 - | .CALL => some 1 - | .CALLCODE => some 1 - | .RETURN => some 0 - | .DELEGATECALL => some 1 - | .CREATE2 => some 1 - | .STATICCALL => some 0 - | .REVERT => some 0 - | .INVALID => none - | .SELFDESTRUCT => some 0 +def α : Operation .EVM → Option ℕ + | .STOP => some 0 + | .ADD => some 1 + | .MUL => some 1 + | .SUB => some 1 + | .DIV => some 1 + | .SDIV => some 1 + | .MOD => some 1 + | .SMOD => some 1 + | .ADDMOD => some 1 + | .MULMOD => some 1 + | .EXP => some 1 + | .SIGNEXTEND => some 1 + | .LT => some 1 + | .GT => some 1 + | .SLT => some 1 + | .SGT => some 1 + | .EQ => some 1 + | .ISZERO => some 1 + | .AND => some 1 + | .OR => some 1 + | .XOR => some 1 + | .NOT => some 1 + | .BYTE => some 1 + | .SHL => some 1 + | .SHR => some 1 + | .SAR => some 1 + | .KECCAK256 => some 1 + | .ADDRESS => some 1 + | .BALANCE => some 1 + | .ORIGIN => some 1 + | .CALLER => some 1 + | .CALLVALUE => some 1 + | .CALLDATALOAD => some 1 + | .CALLDATASIZE => some 1 + | .CALLDATACOPY => some 0 + | .CODESIZE => some 1 + | .CODECOPY => some 0 + | .GASPRICE => some 1 + | .EXTCODESIZE => some 1 + | .EXTCODECOPY => some 0 + | .RETURNDATASIZE => some 1 + | .RETURNDATACOPY => some 0 + | .EXTCODEHASH => some 1 + | .BLOCKHASH => some 1 + | .COINBASE => some 1 + | .TIMESTAMP => some 1 + | .NUMBER => some 1 + | .PREVRANDAO => some 1 + | .GASLIMIT => some 1 + | .CHAINID => some 1 + | .SELFBALANCE => some 1 + | .BASEFEE => some 1 + | .BLOBHASH => some 1 + | .BLOBBASEFEE => some 1 + | .POP => some 0 + | .MLOAD => some 1 + | .MSTORE => some 0 + | .MSTORE8 => some 0 + | .SLOAD => some 1 + | .SSTORE => some 0 + | .PC => some 1 + | .MSIZE => some 1 + | .GAS => some 1 + | .JUMP => some 0 + | .JUMPI => some 0 + | .JUMPDEST => some 0 + | .TLOAD => some 1 + | .TSTORE => some 0 + | .MCOPY => some 0 + | .Push _ => some 1 + | .DUP1 => some 2 + | .DUP2 => some 3 + | .DUP3 => some 4 + | .DUP4 => some 5 + | .DUP5 => some 6 + | .DUP6 => some 7 + | .DUP7 => some 8 + | .DUP8 => some 9 + | .DUP9 => some 10 + | .DUP10 => some 11 + | .DUP11 => some 12 + | .DUP12 => some 13 + | .DUP13 => some 14 + | .DUP14 => some 15 + | .DUP15 => some 16 + | .DUP16 => some 16 + | .SWAP1 => some 2 + | .SWAP2 => some 3 + | .SWAP3 => some 4 + | .SWAP4 => some 5 + | .SWAP5 => some 6 + | .SWAP6 => some 7 + | .SWAP7 => some 8 + | .SWAP8 => some 9 + | .SWAP9 => some 10 + | .SWAP10 => some 11 + | .SWAP11 => some 12 + | .SWAP12 => some 13 + | .SWAP13 => some 14 + | .SWAP14 => some 15 + | .SWAP15 => some 16 + | .SWAP16 => some 17 + | .Log _ => some 0 + | .CREATE => some 1 + | .CALL => some 1 + | .CALLCODE => some 1 + | .RETURN => some 0 + | .DELEGATECALL => some 1 + | .CREATE2 => some 1 + | .STATICCALL => some 0 + | .REVERT => some 0 + | .INVALID => none + | .SELFDESTRUCT => some 0 def parseInstr : UInt8 → Option (Operation .EVM) | 0x00 => some .STOP @@ -475,6 +481,8 @@ def parseInstr : UInt8 → Option (Operation .EVM) | 0x46 => some .CHAINID | 0x47 => some .SELFBALANCE | 0x48 => some .BASEFEE + | 0x49 => some .BLOBHASH + | 0x4a => some .BLOBBASEFEE | 0x50 => some .POP | 0x51 => some .MLOAD diff --git a/EvmYul/EVM/PrimOps.lean b/EvmYul/EVM/PrimOps.lean index c1eb788..c24cc00 100644 --- a/EvmYul/EVM/PrimOps.lean +++ b/EvmYul/EVM/PrimOps.lean @@ -59,6 +59,17 @@ def executionEnvOp (debugMode : Bool) (op : ExecutionEnv → UInt256) : Transfor .ok <| evmState.replaceStackAndIncrPC (evmState.stack.push result) +def unaryExecutionEnvOp (debugMode : Bool) (op : ExecutionEnv → UInt256 → UInt256) : Transformer := + λ evmState ↦ + match evmState.stack.pop with + | some ⟨ s , μ₀⟩ => Id.run do + let result := op evmState.executionEnv μ₀ + if debugMode then + dbg_trace s!"result: {result}" + .ok <| + evmState.replaceStackAndIncrPC (s.push result) + | _ => .error EVM.Exception.InvalidStackSizeException + def machineStateOp (op : MachineState → UInt256) : Transformer := λ evmState ↦ .ok <| @@ -141,6 +152,7 @@ def unaryStateOp dbg_trace s!"called with μ₀: {μ₀}" let (state', b) := op evmState.toState μ₀ let evmState' := {evmState with toState := state'} + if debugMode then dbg_trace s!"got result: {b}" .ok <| evmState'.replaceStackAndIncrPC (stack'.push b) | _ => .error EVM.Exception.InvalidStackSizeException diff --git a/EvmYul/EVM/Semantics.lean b/EvmYul/EVM/Semantics.lean index 12944a6..ecdcd85 100644 --- a/EvmYul/EVM/Semantics.lean +++ b/EvmYul/EVM/Semantics.lean @@ -10,6 +10,7 @@ import EvmYul.Maps.YPState import EvmYul.State.AccountOps import EvmYul.State.ExecutionEnv import EvmYul.State.Substate +import EvmYul.State.TransactionOps import EvmYul.EVM.Exception import EvmYul.EVM.Gas @@ -147,6 +148,82 @@ local instance : MonadLift Option (Except EVM.Exception) := ⟨Option.option (.error .InvalidStackSizeException) .ok⟩ mutual + +def call (debugMode : Bool) (fuel : Nat) + (blobVersionedHashes : List ByteArray) + (gas source recipient t value value' inOffset inSize outOffset outSize : UInt256) + (permission : Bool) + (state : SharedState) + : + Except EVM.Exception (UInt256 × SharedState) +:= do + match fuel with + | 0 => dbg_trace "nofuel"; .ok (1, state) + | .succ f => + -- m[μs[3] . . . (μs[3] + μs[4] − 1)] + let (i, newMachineState) := state.toMachineState.readBytes inOffset inSize + -- t ≡ μs[1] mod 2^160 + let t : AccountAddress := AccountAddress.ofUInt256 t + let recipient : AccountAddress := AccountAddress.ofUInt256 recipient + let source : AccountAddress := AccountAddress.ofUInt256 source + let Iₐ := state.executionEnv.codeOwner + let σ := state.accountMap + let Iₑ := state.executionEnv.depth + let callgas := Ccallgas t value gas σ state.toMachineState state.substate + let (cA, σ', g', A', z, o) ← do + -- TODO - Refactor condition and possibly share with CREATE + if value ≤ (σ.find? Iₐ |>.option 0 Account.balance) ∧ Iₑ < 1024 then + let A' := state.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} + let resultOfΘ ← + Θ (debugMode := debugMode) + (fuel := f) + blobVersionedHashes + (createdAccounts := state.createdAccounts) + (σ := σ) -- σ in Θ(σ, ..) + (A := A') -- A* in Θ(.., A*, ..) + (s := source) + (o := state.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) + (r := recipient) -- t in Θ(.., t, ..) + (c := toExecute σ t) + (g := callgas) + (p := state.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) + (v := value) + (v' := value') + (d := i) + (e := Iₑ + 1) + (H := state.executionEnv.header) + (w := permission) -- I_w in Θ(.., I_W) + pure resultOfΘ + else + -- otherwise (σ, CCALLGAS(σ, μ, A), A, 0, ()) + .ok + (state.createdAccounts, state.toState.accountMap, callgas, state.toState.substate, false, .some .empty) + -- n ≡ min({μs[6], ‖o‖}) + let n : UInt256 := min outSize (o.elim 0 (UInt256.ofNat ∘ ByteArray.size)) + + -- TODO - Check what happens when `o = .none`. + let μ'ₘ := newMachineState.writeBytes (o.getD .empty) outOffset n -- μ′_m[μs[5] ... (μs[5] + n − 1)] = o[0 ... (n − 1)] + let μ'ₒ := o -- μ′o = o + let μ'_g := μ'ₘ.gasAvailable + g' -- Ccall is subtracted in X as part of C + + let codeExecutionFailed : Bool := !z + let notEnoughFunds : Bool := value > (σ.find? state.executionEnv.codeOwner |>.elim 0 Account.balance) -- TODO - Unify condition with CREATE. + let callDepthLimitReached : Bool := state.executionEnv.depth == 1024 + let x : UInt256 := if codeExecutionFailed || notEnoughFunds || callDepthLimitReached then 0 else 1 -- where x = 0 if the code execution for this operation failed, or if μs[2] > σ[Ia]b (not enough funds) or Ie = 1024 (call depth limit reached); x = 1 otherwise. + + -- NB. `MachineState` here does not contain the `Stack` nor the `PC`, thus incomplete. + let μ'incomplete : MachineState := + { μ'ₘ with + returnData := μ'ₒ.getD .empty -- TODO - Check stuff wrt. .none + gasAvailable := μ'_g + } + + let result : SharedState := { state with accountMap := σ', substate := A', createdAccounts := cA } + let result := { + result with toMachineState := μ'incomplete + } + .ok (x, result) + def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Option (UInt256 × Nat)) := .none) : EVM.Transformer := match fuel with | 0 => .ok @@ -249,6 +326,7 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti let Λ := Lambda debugMode f + evmState.executionEnv.blobVersionedHashes evmState.createdAccounts σStar evmState.toState.substate @@ -316,6 +394,7 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti let σStar := σ.insert Iₐ {σ_Iₐ with nonce := σ_Iₐ.nonce + 1} let Λ := Lambda debugMode f + evmState.executionEnv.blobVersionedHashes evmState.createdAccounts σStar evmState.toState.substate @@ -356,7 +435,6 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti .error .InvalidStackSizeException -- TODO: Factor out the semantics for `CALL`, `CALLCODE`, `DELEGATECALL`, `STATICCALL` | .CALL => do - -- dbg_trace /- op -/ "CALL" -- Names are from the YP, these are: -- μ₀ - gas -- μ₁ - to @@ -365,78 +443,16 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti -- μ₄ - inSize -- μ₅ - outOffsize -- μ₆ - outSize - -- dbg_trace "POPPING" let (stack, μ₀, μ₁, μ₂, μ₃, μ₄, μ₅, μ₆) ← evmState.stack.pop7 - let t : AccountAddress := AccountAddress.ofUInt256 μ₁ -- t ≡ μs[1] mod 2^160 if debugMode then - dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} ({toHex t.toByteArray |>.takeRight 5}) μ₂: {μ₂} μ₃: {μ₃} μ₄: {μ₄} μ₅: {μ₅} μ₆: {μ₆}" - -- dbg_trace "POPPED OK; μ₁ : {μ₁}" - -- dbg_trace s!"Pre call, we have: {Finmap.pretty evmState.accountMap}" - let ((cA, σ', g', A', z, o), newMachineState) ← do - -- TODO - Refactor condition and possibly share with CREATE - if μ₂ ≤ (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.option 0 Account.balance) ∧ evmState.executionEnv.depth < 1024 then - -- dbg_trace s!"DBG REMOVE; Calling address: {t}" - let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} - -- dbg_trace s!"looking up memory range: {evmState.toMachineState.readBytes μ₃ μ₄}" - let (i, newMachineState) := evmState.toMachineState.readBytes μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] - let resultOfΘ ← - Θ (debugMode := debugMode) - (fuel := f) -- TODO meh - (createdAccounts := evmState.createdAccounts) - (σ := evmState.accountMap) -- σ in Θ(σ, ..) - (A := A') -- A* in Θ(.., A*, ..) - (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) - (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) - (r := t) -- t in Θ(.., t, ..) - (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' - (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) - (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) - (v := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) - (v' := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) - (d := i) -- i in Θ(.., i, ..) - (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) - (H := evmState.executionEnv.header) - (w := evmState.executionEnv.perm) -- I_W in Θ(.., I_W) - pure (resultOfΘ, newMachineState) - -- TODO gas - CCALLGAS(σ, μ, A) - else - -- otherwise (σ, CCALLGAS(σ, μ, A), A, 0, ()) - .ok - ( (evmState.createdAccounts, evmState.toState.accountMap, μ₀, evmState.toState.substate, false, .some .empty) - , evmState.toMachineState - ) - -- dbg_trace s!"THETA OK with accounts: {repr σ'}" - let n : UInt256 := min μ₆ (o.elim 0 (UInt256.ofNat ∘ ByteArray.size)) -- n ≡ min({μs[6], ‖o‖}) -- TODO - Why is this using... set??? { } brackets ??? - -- TODO I am assuming here that μ' is μ with the updates mentioned in the CALL section. Check. - - -- TODO - Note to self. Check how writeWord/writeBytes is implemented. By a cursory look, we play loose with UInt8 -> UInt256 (c.f. e.g. `calldatacopy`) and then the interplay with the WordSize parameter. - -- TODO - Check what happens when `o = .none`. - let μ'ₘ := newMachineState.writeBytes (o.getD .empty) μ₅ n -- μ′_m[μs[5] ... (μs[5] + n − 1)] = o[0 ... (n − 1)] - let μ'ₒ := o -- μ′o = o - let μ'_g := g' -- TODO gas - μ′g ≡ μg − CCALLGAS(σ, μ, A) + g - - let codeExecutionFailed : Bool := z -- TODO - This is likely wrong. - let notEnoughFunds : Bool := μ₂ > (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.elim 0 Account.balance) -- TODO - Unify condition with CREATE. - let callDepthLimitReached : Bool := evmState.executionEnv.depth == 1024 - let x : UInt256 := if codeExecutionFailed || notEnoughFunds || callDepthLimitReached then 0 else 1 -- where x = 0 if the code execution for this operation failed, or if μs[2] > σ[Ia]b (not enough funds) or Ie = 1024 (call depth limit reached); x = 1 otherwise. - + dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} ({toHex μ₁.toByteArray |>.takeRight 5}) μ₂: {μ₂} μ₃: {μ₃} μ₄: {μ₄} μ₅: {μ₅} μ₆: {μ₆}" + let (x, state') ← + call debugMode f evmState.executionEnv.blobVersionedHashes μ₀ evmState.executionEnv.codeOwner μ₁ μ₁ μ₂ μ₂ μ₃ μ₄ μ₅ μ₆ evmState.executionEnv.perm evmState.toSharedState let μ'ₛ := stack.push x -- μ′s[0] ≡ x - - -- NB. `MachineState` here does not contain the `Stack` nor the `PC`, thus incomplete. - let μ'incomplete : MachineState := - { μ'ₘ with - returnData := μ'ₒ.getD .empty -- TODO - Check stuff wrt. .none - gasAvailable := μ'_g - } - - let σ' : EVM.State := { evmState with accountMap := σ', substate := A', createdAccounts := cA } - let σ' := { - σ' with toMachineState := μ'incomplete - }.replaceStackAndIncrPC μ'ₛ - - .ok σ' + let evmState' := + { evmState with toSharedState := state'}.replaceStackAndIncrPC μ'ₛ + .ok evmState' | .CALLCODE => - -- dbg_trace /- op -/ "CALL" do -- Names are from the YP, these are: -- μ₀ - gas @@ -446,84 +462,16 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti -- μ₄ - inSize -- μ₅ - outOffsize -- μ₆ - outSize - -- dbg_trace "POPPING" let (stack, μ₀, μ₁, μ₂, μ₃, μ₄, μ₅, μ₆) ← evmState.stack.pop7 if debugMode then - dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} μ₂: {μ₂} μ₃: {μ₃} μ₄: {μ₄} μ₅: {μ₅} μ₆: {μ₆}" - -- dbg_trace "POPPED OK; μ₁ : {μ₁}" - -- dbg_trace s!"Pre call, we have: {Finmap.pretty evmState.accountMap}" - let ((cA, σ', g', A', z, o), newMachineState) ← do - -- TODO - Refactor condition and possibly share with CREATE - if μ₂ ≤ (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.option 0 Account.balance) ∧ evmState.executionEnv.depth < 1024 then - let t : AccountAddress := AccountAddress.ofUInt256 μ₁ -- t ≡ μs[1] mod 2^160 - -- dbg_trace s!"DBG REMOVE; Calling address: {t}" - let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} - let .some tDirect := evmState.accountMap.find? t | default - -- dbg_trace s!"looking up memory range: {evmState.toMachineState.readBytes μ₃ μ₄}" - let (i, newMachineState) := evmState.toMachineState.readBytes μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] - let resultOfΘ ← - Θ - (debugMode := debugMode) - (fuel := f) -- TODO meh - (createdAccounts := evmState.createdAccounts) - (σ := evmState.accountMap) -- σ in Θ(σ, ..) - (A := A') -- A* in Θ(.., A*, ..) - (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) - (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) - (r := evmState.executionEnv.codeOwner) -- t in Θ(.., t, ..) - (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' - (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) - (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) - (v := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) - (v' := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) - (d := i) -- i in Θ(.., i, ..) - (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) - (H := evmState.executionEnv.header) - (w := evmState.executionEnv.perm) -- I_W in Θ(.., I_W) - pure (resultOfΘ, newMachineState) - -- TODO gas - CCALLGAS(σ, μ, A) - else - -- otherwise (σ, CCALLGAS(σ, μ, A), A, 0, ()) - .ok - ( (evmState.createdAccounts, evmState.toState.accountMap, μ₀, evmState.toState.substate, false, .some .empty) - , evmState.toMachineState - ) - -- dbg_trace s!"THETA OK with accounts: {repr σ'}" - let n : UInt256 := min μ₆ (o.elim 0 (UInt256.ofNat ∘ ByteArray.size)) -- n ≡ min({μs[6], ‖o‖}) -- TODO - Why is this using... set??? { } brackets ??? - -- TODO I am assuming here that μ' is μ with the updates mentioned in the CALL section. Check. - - -- TODO - Note to self. Check how writeWord/writeBytes is implemented. By a cursory look, we play loose with UInt8 -> UInt256 (c.f. e.g. `calldatacopy`) and then the interplay with the WordSize parameter. - -- TODO - Check what happens when `o = .none`. - -- dbg_trace s!"REPORT - μ₅: {μ₅} n: {n} o: {o}" - -- dbg_trace "Θ will copy memory now" - let μ'ₘ := newMachineState.writeBytes (o.getD .empty) μ₅ n -- μ′_m[μs[5] ... (μs[5] + n − 1)] = o[0 ... (n − 1)] - -- dbg_trace s!"μ'ₘ: {μ'ₘ.memory}" - -- dbg_trace s!"REPORT - μ'ₘ: {Finmap.pretty μ'ₘ.memory}" - let μ'ₒ := o -- μ′o = o - let μ'_g := g' -- TODO gas - μ′g ≡ μg − CCALLGAS(σ, μ, A) + g - - let codeExecutionFailed : Bool := z -- TODO - This is likely wrong. - let notEnoughFunds : Bool := μ₂ > (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.elim 0 Account.balance) -- TODO - Unify condition with CREATE. - let callDepthLimitReached : Bool := evmState.executionEnv.depth == 1024 - let x : UInt256 := if codeExecutionFailed || notEnoughFunds || callDepthLimitReached then 0 else 1 -- where x = 0 if the code execution for this operation failed, or if μs[2] > σ[Ia]b (not enough funds) or Ie = 1024 (call depth limit reached); x = 1 otherwise. - + dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} ({toHex μ₁.toByteArray |>.takeRight 5}) μ₂: {μ₂} μ₃: {μ₃} μ₄: {μ₄} μ₅: {μ₅} μ₆: {μ₆}" + let (x, state') ← + call debugMode f evmState.executionEnv.blobVersionedHashes μ₀ evmState.executionEnv.codeOwner evmState.executionEnv.codeOwner μ₁ μ₂ μ₂ μ₃ μ₄ μ₅ μ₆ evmState.executionEnv.perm evmState.toSharedState let μ'ₛ := stack.push x -- μ′s[0] ≡ x - - -- NB. `MachineState` here does not contain the `Stack` nor the `PC`, thus incomplete. - let μ'incomplete : MachineState := - { μ'ₘ with - returnData := μ'ₒ.getD .empty -- TODO - Check stuff wrt. .none - gasAvailable := μ'_g - } - - let σ' : EVM.State := { evmState with accountMap := σ', substate := A', createdAccounts := cA } - let σ' := { - σ' with toMachineState := μ'incomplete - }.replaceStackAndIncrPC μ'ₛ - - .ok σ' + let evmState' := + { evmState with toSharedState := state'}.replaceStackAndIncrPC μ'ₛ + .ok evmState' | .DELEGATECALL => - -- dbg_trace /- op -/ "DELEGATECALL" do -- Names are from the YP, these are: -- μ₀ - gas @@ -532,86 +480,17 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti -- μ₄ - inSize -- μ₅ - outOffsize -- μ₆ - outSize - -- dbg_trace "POPPING" -- TODO: Use indices correctly let (stack, μ₀, μ₁, /-μ₂,-/ μ₃, μ₄, μ₅, μ₆) ← evmState.stack.pop6 if debugMode then - dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} μ₂: {μ₃} μ₃: {μ₄} μ₄: {μ₅} μ₅: {μ₆}" - -- dbg_trace "POPPED OK; μ₁ : {μ₁}" - -- dbg_trace s!"Pre call, we have: {Finmap.pretty evmState.accountMap}" - let ((cA, σ', g', A', z, o), newMachineState) ← do - -- TODO - Refactor condition and possibly share with CREATE - if evmState.executionEnv.depth < 1024 then - let t : AccountAddress := AccountAddress.ofUInt256 μ₁ -- t ≡ μs[1] mod 2^160 - -- dbg_trace s!"DBG REMOVE; Calling address: {t}" - let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} - let .some tDirect := evmState.accountMap.find? t | default - let tDirect := tDirect.code -- We use the code directly without an indirection a'la `codeMap[t]`. - -- dbg_trace s!"looking up memory range: {evmState.toMachineState.readBytes μ₃ μ₄}" - let (i, newMachineState) := evmState.toMachineState.readBytes μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] - -- dbg_trace s!"code: {toHex tDirect}" - let resultOfΘ ← - Θ (debugMode := debugMode) - (fuel := f) -- TODO meh - (createdAccounts := evmState.createdAccounts) - (σ := evmState.accountMap) -- σ in Θ(σ, ..) - (A := A') -- A* in Θ(.., A*, ..) - (s := evmState.executionEnv.source) -- Iₛ in Θ(.., Iₐ, ..) - (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) - (r := evmState.executionEnv.codeOwner) -- t in Θ(.., t, ..) - (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' - (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) - (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) - (v := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) - (v' := evmState.executionEnv.weiValue) -- μₛ[2] in Θ(.., μₛ[2], ..) - (d := i) -- i in Θ(.., i, ..) - (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) - (H := evmState.executionEnv.header) - (w := evmState.executionEnv.perm) -- I_W in Θ(.., I_W) - pure (resultOfΘ, newMachineState) - -- TODO gas - CCALLGAS(σ, μ, A) - else - -- otherwise (σ, CCALLGAS(σ, μ, A), A, 0, ()) - .ok - ( (evmState.createdAccounts, evmState.toState.accountMap, μ₀, evmState.toState.substate, false, .some .empty) - , evmState.toMachineState - ) - -- dbg_trace s!"THETA OK with accounts: {repr σ'}" - let n : UInt256 := min μ₆ (o.elim 0 (UInt256.ofNat ∘ ByteArray.size)) -- n ≡ min({μs[6], ‖o‖}) -- TODO - Why is this using... set??? { } brackets ??? - -- TODO I am assuming here that μ' is μ with the updates mentioned in the CALL section. Check. - - -- TODO - Note to self. Check how writeWord/writeBytes is implemented. By a cursory look, we play loose with UInt8 -> UInt256 (c.f. e.g. `calldatacopy`) and then the interplay with the WordSize parameter. - -- TODO - Check what happens when `o = .none`. - -- dbg_trace s!"REPORT - μ₅: {μ₅} n: {n} o: {o}" - -- dbg_trace "Θ will copy memory now" - let μ'ₘ := newMachineState.writeBytes (o.getD .empty) μ₅ n -- μ′_m[μs[5] ... (μs[5] + n − 1)] = o[0 ... (n − 1)] - -- dbg_trace s!"μ'ₘ: {μ'ₘ.memory}" - -- dbg_trace s!"REPORT - μ'ₘ: {Finmap.pretty μ'ₘ.memory}" - let μ'ₒ := o -- μ′o = o - let μ'_g := g' -- TODO gas - μ′g ≡ μg − CCALLGAS(σ, μ, A) + g - - let codeExecutionFailed : Bool := z -- TODO - This is likely wrong. - -- let notEnoughFunds : Bool := μ₂ > (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.elim 0 Account.balance) -- TODO - Unify condition with CREATE. - let callDepthLimitReached : Bool := evmState.executionEnv.depth == 1024 - let x : UInt256 := if codeExecutionFailed || callDepthLimitReached then 0 else 1 -- where x = 0 if the code execution for this operation failed, or if μs[2] > σ[Ia]b (not enough funds) or Ie = 1024 (call depth limit reached); x = 1 otherwise. - + dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} ({toHex μ₁.toByteArray |>.takeRight 5}) μ₂: {μ₃} μ₃: {μ₄} μ₄: {μ₅} μ₅: {μ₆}" + let (x, state') ← + call debugMode f evmState.executionEnv.blobVersionedHashes μ₀ evmState.executionEnv.source evmState.executionEnv.codeOwner μ₁ 0 evmState.executionEnv.weiValue μ₃ μ₄ μ₅ μ₆ evmState.executionEnv.perm evmState.toSharedState let μ'ₛ := stack.push x -- μ′s[0] ≡ x - - -- NB. `MachineState` here does not contain the `Stack` nor the `PC`, thus incomplete. - let μ'incomplete : MachineState := - { μ'ₘ with - returnData := μ'ₒ.getD .empty -- TODO - Check stuff wrt. .none - gasAvailable := μ'_g - } - - let σ' : EVM.State := { evmState with accountMap := σ', substate := A', createdAccounts := cA } - let σ' := { - σ' with toMachineState := μ'incomplete - }.replaceStackAndIncrPC μ'ₛ - - .ok σ' + let evmState' := + { evmState with toSharedState := state'}.replaceStackAndIncrPC μ'ₛ + .ok evmState' | .STATICCALL => - -- dbg_trace /- op -/ "CALL" do -- Names are from the YP, these are: -- μ₀ - gas @@ -621,83 +500,15 @@ def step (debugMode : Bool) (fuel : ℕ) (instr : Option (Operation .EVM × Opti -- μ₄ - inSize -- μ₅ - outOffsize -- μ₆ - outSize - -- dbg_trace "POPPING" let (stack, μ₀, μ₁, /- μ₂, -/ μ₃, μ₄, μ₅, μ₆) ← evmState.stack.pop6 if debugMode then - dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} μ₂: {μ₃} μ₃: {μ₄} μ₄: {μ₅} μ₅: {μ₆}" - -- dbg_trace "POPPED OK; μ₁ : {μ₁}" - -- dbg_trace s!"Pre call, we have: {Finmap.pretty evmState.accountMap}" - let ((cA, σ', g', A', z, o), newMachineState) ← do - -- TODO - Refactor condition and possibly share with CREATE - if 0 ≤ (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.option 0 Account.balance) ∧ evmState.executionEnv.depth < 1024 then - let t : AccountAddress := AccountAddress.ofUInt256 μ₁ -- t ≡ μs[1] mod 2^160 - -- dbg_trace s!"DBG REMOVE; Calling address: {t}" - let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} - let .some tDirect := evmState.accountMap.find? t | default - let tDirect := tDirect.code -- We use the code directly without an indirection a'la `codeMap[t]`. - -- dbg_trace s!"looking up memory range: {evmState.toMachineState.readBytes μ₃ μ₄}" - let (i, newMachineState) := evmState.toMachineState.readBytes μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] - let resultOfΘ ← - Θ (debugMode := debugMode) - (fuel := f) -- TODO meh - (createdAccounts := evmState.createdAccounts) - (σ := evmState.accountMap) -- σ in Θ(σ, ..) - (A := A') -- A* in Θ(.., A*, ..) - (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) - (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) - (r := t) -- t in Θ(.., t, ..) - (c := toExecute evmState.accountMap t) -- t in Θ(.., t, ..) except 'dereferenced' - (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) - (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) - (v := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) - (v' := 0) -- μₛ[2] in Θ(.., μₛ[2], ..) - (d := i) -- i in Θ(.., i, ..) - (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) - (H := evmState.executionEnv.header) - (w := false) -- I_W in Θ(.., I_W) - pure (resultOfΘ, newMachineState) - -- TODO gas - CCALLGAS(σ, μ, A) - else - -- otherwise (σ, CCALLGAS(σ, μ, A), A, 0, ()) - .ok - ( (evmState.createdAccounts, evmState.toState.accountMap, μ₀, evmState.toState.substate, false, .some .empty) - , evmState.toMachineState - ) - -- dbg_trace s!"THETA OK with accounts: {repr σ'}" - let n : UInt256 := min μ₆ (o.elim 0 (UInt256.ofNat ∘ ByteArray.size)) -- n ≡ min({μs[6], ‖o‖}) -- TODO - Why is this using... set??? { } brackets ??? - -- TODO I am assuming here that μ' is μ with the updates mentioned in the CALL section. Check. - - -- TODO - Note to self. Check how writeWord/writeBytes is implemented. By a cursory look, we play loose with UInt8 -> UInt256 (c.f. e.g. `calldatacopy`) and then the interplay with the WordSize parameter. - -- TODO - Check what happens when `o = .none`. - -- dbg_trace s!"REPORT - μ₅: {μ₅} n: {n} o: {o}" - -- dbg_trace "Θ will copy memory now" - let μ'ₘ := newMachineState.writeBytes (o.getD .empty) μ₅ n -- μ′_m[μs[5] ... (μs[5] + n − 1)] = o[0 ... (n − 1)] - -- dbg_trace s!"μ'ₘ: {μ'ₘ.memory}" - -- dbg_trace s!"REPORT - μ'ₘ: {Finmap.pretty μ'ₘ.memory}" - let μ'ₒ := o -- μ′o = o - let μ'_g := g' -- TODO gas - μ′g ≡ μg − CCALLGAS(σ, μ, A) + g - - let codeExecutionFailed : Bool := z -- TODO - This is likely wrong. - let notEnoughFunds : Bool := 0 > (evmState.accountMap.find? evmState.executionEnv.codeOwner |>.elim 0 Account.balance) -- TODO - Unify condition with CREATE. - let callDepthLimitReached : Bool := evmState.executionEnv.depth == 1024 - let x : UInt256 := if codeExecutionFailed || notEnoughFunds || callDepthLimitReached then 0 else 1 -- where x = 0 if the code execution for this operation failed, or if μs[2] > σ[Ia]b (not enough funds) or Ie = 1024 (call depth limit reached); x = 1 otherwise. - + dbg_trace s!"called with μ₀: {μ₀} μ₁: {μ₁} ({toHex μ₁.toByteArray |>.takeRight 5}) μ₂: {μ₃} μ₃: {μ₄} μ₄: {μ₅} μ₅: {μ₆}" + let (x, state') ← + call debugMode f evmState.executionEnv.blobVersionedHashes μ₀ evmState.executionEnv.codeOwner μ₁ μ₁ 0 0 μ₃ μ₄ μ₅ μ₆ false evmState.toSharedState let μ'ₛ := stack.push x -- μ′s[0] ≡ x - - -- NB. `MachineState` here does not contain the `Stack` nor the `PC`, thus incomplete. - let μ'incomplete : MachineState := - { μ'ₘ with - returnData := μ'ₒ.getD .empty -- TODO - Check stuff wrt. .none - gasAvailable := μ'_g - } - - let σ' : EVM.State := { evmState with accountMap := σ', substate := A', createdAccounts := cA } - let σ' := { - σ' with toMachineState := μ'incomplete - }.replaceStackAndIncrPC μ'ₛ - - .ok σ' - + let evmState' := + { evmState with toSharedState := state'}.replaceStackAndIncrPC μ'ₛ + .ok evmState' | instr => EvmYul.step debugMode instr evmState /-- @@ -709,6 +520,7 @@ def X (debugMode : Bool) (fuel : ℕ) (evmState : State) : Except EVM.Exception | .succ f => let I_b := evmState.toState.executionEnv.code let instr@(w, _) := decode I_b evmState.pc |>.getD (.STOP, .none) + -- dbg_trace s!"gas available in X {evmState.gasAvailable} for {w.pretty}" -- (159) let W (w : Operation .EVM) (s : Stack UInt256) : Bool := @@ -764,6 +576,8 @@ def X (debugMode : Bool) (fuel : ℕ) (evmState : State) : Except EVM.Exception -- NB we still need to check gas, because `Z` needs to call `C`, which needs `μ'ᵢ`. -- We first call `step` to obtain `μ'ᵢ`, which we then use to compute `C`. let evmState' ← step debugMode f instr evmState + -- if w == .DELEGATECALL then + -- dbg_trace s!"gas available after step DELEGATECALL {evmState'.gasAvailable}" -- NB: (327) -- w := if pc < I.code.size -- then match EVM.decode I.code pc with @@ -778,13 +592,18 @@ def X (debugMode : Bool) (fuel : ℕ) (evmState : State) : Except EVM.Exception -- Similarly, we cannot reach a situation in which the stack elements are not available -- on the stack because this is guarded above. As such, `C` can be pure here. let gasCost ← C evmState evmState'.activeWords w - -- dbg_trace s!"gasCost: {gasCost}, gasAvailable: {evmState.gasAvailable}" - if evmState.gasAvailable < gasCost then + -- dbg_trace s!"gasAvailable: {evmState.gasAvailable}; gasCost: {gasCost} for instruction {w.pretty}" + if debugMode && evmState.gasAvailable < gasCost then + dbg_trace s!"gasAvailable: {evmState.gasAvailable} < gasCost: {gasCost} for instruction {w.pretty}" + if evmState.gasAvailable < gasCost then do -- Out of gas. This is a part of `Z`, as such, we have the same return value. -- dbg_trace "Out of gass!" -- dbg_trace s!"gas available: {evmState.gasAvailable}; gas cost: {gasCost}" .ok ({evmState with accountMap := ∅}, none) - else + else do + let evmState' := {evmState' with gasAvailable := evmState'.gasAvailable - gasCost} + -- dbg_trace s!"new gas available after {w.pretty}: {evmState.gasAvailable - gasCost}" + -- dbg_trace s!"gas cost after {w.pretty}: {gasCost}" match H evmState'.toMachineState w with -- The YP does this in a weird way. -- NB in our model, we need the max memory touched of the executed instruction -- before we can check whether there is enough gas to execute the instruction. @@ -793,7 +612,7 @@ def X (debugMode : Bool) (fuel : ℕ) (evmState : State) : Except EVM.Exception -- the gas cost and only then execute, I am unsure as of right now. -- Interestingly, the YP is defining `C` with parameters that are much 'broader' -- than what is strictly necessary, e.g. we are decoding an instruction, instead of getting one in input. - | none => X debugMode f {evmState' with gasAvailable := evmState.gasAvailable - gasCost} + | none => X debugMode f evmState' | some o => if w == .REVERT then -- The Yellow Paper says we don't call the "iterator function" "O" for `REVERT`, @@ -837,20 +656,21 @@ def Ξ -- Type `Ξ` using `\GX` or `\Xi` gasAvailable := g } let (evmState', o) ← X debugMode f freshEvmState - if debugMode then - dbg_trace s!"Ξ executed {evmState'.execLength} primops" + -- if debugMode then + -- dbg_trace s!"Ξ executed {evmState'.execLength} primops" let finalGas := evmState'.gasAvailable -- TODO(check): Do we need to compute `C` here one more time? return (evmState'.createdAccounts, evmState'.accountMap, finalGas, evmState'.substate, o) def Lambda (debugMode : Bool) (fuel : ℕ) + (blobVersionedHashes : List ByteArray) (createdAccounts : Batteries.RBSet AccountAddress compare) -- needed for EIP-6780 (σ : YPState) (A : Substate) (s : AccountAddress) -- sender (o : AccountAddress) -- original transactor - (g : UInt256) -- available gas + (g : UInt256) -- available gas (p : UInt256) -- gas price (v : UInt256) -- endowment (i : ByteArray) -- the initialisation EVM code @@ -932,6 +752,7 @@ def Lambda , header := H , depth := e + 1 , perm := w + , blobVersionedHashes := blobVersionedHashes } match Ξ debugMode f createdAccounts σStar g AStar exEnv with -- TODO - Gas model. | .error e => @@ -1028,6 +849,7 @@ NB - This is implemented using the 'boolean' fragment with ==, <=, ||, etc. -/ def Θ (debugMode : Bool) (fuel : Nat) + (blobVersionedHashes : List ByteArray) (createdAccounts : Batteries.RBSet AccountAddress compare) (σ : YPState) (A : Substate) @@ -1089,6 +911,7 @@ def Θ (debugMode : Bool) | ToExecute.Precompiled _ => default | ToExecute.Code code => code header := H + blobVersionedHashes := blobVersionedHashes } let @@ -1133,7 +956,7 @@ end open Batteries (RBMap RBSet) -def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transaction) (dbgOverrideSender : Option AccountAddress := .none) +def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transaction) (expectedSender : AccountAddress) : Except EVM.Exception AccountAddress := do -- dbg_trace "Transaction: {repr T}" @@ -1149,35 +972,35 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio if t.w ∈ [27, 28] then t.w - 27 else - if t.w ≠ 35 + chainId * 2 ∧ t.w ≠ 36 + chainId * 2 then - (t.w - 35 - chainId) % 2 -- `chainId` not subtracted in the Yellow paper but in the EEL spec + if t.w = 35 + chainId * 2 ∨ t.w = 36 + chainId * 2 then + (t.w - 35) % 2 -- `chainId` not subtracted in the Yellow paper but in the EEL spec else t.w - | .access t | .dynamic t => t.yParity + | .access t | .dynamic t | .blob t => t.yParity if v ∉ [0, 1] then .error <| .InvalidTransaction .InvalidSignature let h_T := -- (318) match T with | .legacy _ => KEC T_RLP - | _ => KEC <| ByteArray.mk #[.ofNat T.type] ++ T_RLP + | _ => KEC <| ByteArray.mk #[T.type] ++ T_RLP let (S_T : AccountAddress) ← -- (323) - match dbgOverrideSender with - | .none => - match ECDSARECOVER h_T (ByteArray.mk #[.ofNat v]) T.base.r T.base.s with - | .ok s => - pure <| Fin.ofNat <| fromBytesBigEndian <| - ((KEC s).extract 12 32 /- 160 bits = 20 bytes -/ ).data.data - | .error s => .error <| .SenderRecoverError s - | .some sender => pure sender - + match ECDSARECOVER h_T (ByteArray.mk #[.ofNat v]) T.base.r T.base.s with + | .ok s => + pure <| Fin.ofNat <| fromBytesBigEndian <| + ((KEC s).extract 12 32 /- 160 bits = 20 bytes -/ ).data.data + | .error s => .error <| .SenderRecoverError s + if S_T != expectedSender then + .error <| .SenderRecoverError s!"Recovered sender ({toHex S_T.toByteArray}) ≠ expected sender ({toHex expectedSender.toByteArray})" -- dbg_trace s!"Looking for S_T: {S_T} in: σ: {repr σ}" -- "Also, with a slight abuse of notation ... " let (senderCode, senderNonce, senderBalance) := match σ.find? S_T with | some sender => (sender.code, sender.nonce, sender.balance) - | none => (.empty, 0, 0) + | none => + dbg_trace s!"could not find sender {toHex S_T.toByteArray}" + (.empty, 0, 0) if senderCode ≠ .empty then .error <| .InvalidTransaction .SenderCodeNotEmpty @@ -1186,12 +1009,13 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio match T with | .legacy t | .access t => t.gasLimit * t.gasPrice + t.value | .dynamic t => t.gasLimit * t.maxFeePerGas + t.value - -- dbg_trace "sender balance: {senderBalance}" + | .blob t => t.gasLimit * t.maxFeePerGas + t.value + (getTotalBlobGas T).getD 0 * t.maxFeePerBlobGas + -- dbg_trace s!"v₀: {v₀}, senderBalance: {senderBalance}" if v₀ > senderBalance then .error <| .InvalidTransaction .UpFrontPayment if H_f > match T with - | .dynamic t => t.maxFeePerGas + | .dynamic t | .blob t => t.maxFeePerGas | .legacy t | .access t => t.gasPrice then .error <| .InvalidTransaction .BaseFeeTooHigh @@ -1199,7 +1023,7 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio match T.base.recipient with | some _ => T.base.data.size | none => 0 - if n > 49152 then .error <| .InvalidTransaction .DataGreaterThan9152 + if n > 49152 then .error <| .InvalidTransaction .InitCodeDataGreaterThan49152 match T with | .dynamic t => @@ -1210,9 +1034,9 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio where L_X (T : Transaction) : Except EVM.Exception 𝕋 := -- (317) let accessEntryRLP : AccountAddress × Array UInt256 → 𝕋 - | ⟨a, s⟩ => .𝕃 [.𝔹 (AccountAddress.toByteArray a), .𝕃 (s.map (𝕋.𝔹 ∘ BE ∘ UInt256.toNat)).toList] - let accessEntriesRLP (aEs : Array (AccountAddress × Array UInt256)) : 𝕋 := - .𝕃 (aEs.map accessEntryRLP |>.toList) + | ⟨a, s⟩ => .𝕃 [.𝔹 (AccountAddress.toByteArray a), .𝕃 (s.map (𝕋.𝔹 ∘ UInt256.toByteArray)).toList] + let accessEntriesRLP (aEs : List (AccountAddress × Array UInt256)) : 𝕋 := + .𝕃 (aEs.map accessEntryRLP) match T with | /- 0 -/ .legacy t => if t.w ∈ [27, 28] then @@ -1226,7 +1050,7 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio , t.data ] else - if t.w ≠ 35 + chainId * 2 ∧ t.w ≠ 36 + chainId * 2 then + if t.w = 35 + chainId * 2 ∨ t.w = 36 + chainId * 2 then .ok ∘ .𝕃 ∘ List.map .𝔹 <| [ BE t.nonce -- Tₙ , BE t.gasPrice -- Tₚ @@ -1239,7 +1063,9 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio , .empty , .empty ] - else .error <| .InvalidTransaction .IllFormedRLP + else + dbg_trace "IllFormedRLP legacy transacion: Tw = {t.w}; chainId = {chainId}" + .error <| .InvalidTransaction .IllFormedRLP | /- 1 -/ .access t => .ok ∘ .𝕃 <| @@ -1251,7 +1077,7 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio .𝔹 (t.recipient.option .empty AccountAddress.toByteArray) -- Tₜ , .𝔹 (BE t.value) -- T_v , .𝔹 t.data -- p - , accessEntriesRLP <| RBSet.toList t.accessList |>.toArray -- T_A + , accessEntriesRLP <| RBSet.toList t.accessList -- T_A ] | /- 2 -/ .dynamic t => .ok ∘ .𝕃 <| @@ -1264,14 +1090,30 @@ def checkTransactionGetSender (σ : YPState) (chainId H_f : ℕ) (T : Transactio .𝔹 (t.recipient.option .empty AccountAddress.toByteArray) -- Tₜ , .𝔹 (BE t.value) -- Tᵥ , .𝔹 t.data -- p - , accessEntriesRLP <| RBSet.toList t.accessList |>.toArray -- T_A + , accessEntriesRLP <| RBSet.toList t.accessList -- T_A ] + | /- 3 -/ .blob t => + .ok ∘ .𝕃 <| + [ .𝔹 (BE t.chainId) -- T_c + , .𝔹 (BE t.nonce) -- Tₙ + , .𝔹 (BE t.maxPriorityFeePerGas) -- T_f + , .𝔹 (BE t.maxFeePerGas) -- Tₘ + , .𝔹 (BE t.gasLimit) -- T_g + , -- If Tₜ is ∅ it becomes the RLP empty byte sequence and thus the member of 𝔹₀ + .𝔹 (t.recipient.option .empty AccountAddress.toByteArray) -- Tₜ + , .𝔹 (BE t.value) -- Tᵥ + , .𝔹 t.data -- p + , accessEntriesRLP <| RBSet.toList t.accessList -- T_A + , .𝔹 (BE t.maxFeePerBlobGas) + , .𝕃 (t.blobVersionedHashes.map .𝔹) + ] + -- Type Υ using \Upsilon or \GU -def Υ (debugMode : Bool) (fuel : ℕ) (σ : YPState) (chainId H_f : ℕ) (H : BlockHeader) (T : Transaction) (dbgOverrideSender : Option AccountAddress := .none) +def Υ (debugMode : Bool) (fuel : ℕ) (σ : YPState) (chainId H_f : ℕ) (H : BlockHeader) (T : Transaction) (expectedSender : AccountAddress) : Except EVM.Exception (YPState × Substate × Bool) := do - let S_T ← checkTransactionGetSender σ chainId H_f T dbgOverrideSender + let S_T ← checkTransactionGetSender σ chainId H_f T expectedSender -- "here can be no invalid transactions from this point" let g₀ := -- (64) let g₀_data := @@ -1300,15 +1142,21 @@ def Υ (debugMode : Bool) (fuel : ℕ) (σ : YPState) (chainId H_f : ℕ) (H : B let f := match T with | .legacy t | .access t => t.gasPrice - H_f - | .dynamic t => min t.maxPriorityFeePerGas (t.maxFeePerGas - H_f) + | .dynamic t | .blob t => min t.maxPriorityFeePerGas (t.maxFeePerGas - H_f) -- The effective gas price let p := -- (66) match T with | .legacy t | .access t => t.gasPrice - | .dynamic _ => f + H_f + | .dynamic _ | .blob _ => f + H_f let senderAccount := { senderAccount with - balance := senderAccount.balance - T.base.gasLimit * p -- (74) + /- + https://eips.ethereum.org/EIPS/eip-4844 + "The actual blob_fee as calculated via calc_blob_fee is deducted from + the sender balance before transaction execution and burned, and is not + refunded in case of transaction failure." + -/ + balance := senderAccount.balance - T.base.gasLimit * p - calcBlobFee H T -- (74) nonce := senderAccount.nonce + 1 -- (75) ostorage := senderAccount.storage -- Needed for `Csstore`. } @@ -1334,14 +1182,14 @@ def Υ (debugMode : Bool) (fuel : ℕ) (σ : YPState) (chainId H_f : ℕ) (H : B match T.base.recipient with | none => do let (_, _, σ_P, g', A, z, _) := - match Lambda debugMode fuel createdAccounts σ₀ AStar S_T S_T g p T.base.value T.base.data 0 none H true with + match Lambda debugMode fuel T.blobVersionedHashes createdAccounts σ₀ AStar S_T S_T g p T.base.value T.base.data 0 none H true with | .none => dbg_trace "Lambda returned none; this should probably not be happening; test semantics will be off."; default | .some x => x pure (σ_P, g', A, z) | some t => -- Proposition (71) suggests the recipient can be inexistent let (_, σ_P, g', A, z, _) ← - Θ debugMode fuel createdAccounts σ₀ AStar S_T S_T t (toExecute σ₀ t) g p T.base.value T.base.value T.base.data 0 H true + Θ debugMode fuel T.blobVersionedHashes createdAccounts σ₀ AStar S_T S_T t (toExecute σ₀ t) g p T.base.value T.base.value T.base.data 0 H true -- dbg_trace "Θ gave back σ_P: {repr σ_P}" pure (σ_P, g', A, z) -- The amount to be refunded (82) diff --git a/EvmYul/Operations.lean b/EvmYul/Operations.lean index 1aaf845..752d14a 100644 --- a/EvmYul/Operations.lean +++ b/EvmYul/Operations.lean @@ -299,6 +299,8 @@ inductive BOp : OperationType → Type where -/ | protected SELFBALANCE : BOp τ | protected BASEFEE : BOp τ + | protected BLOBHASH : BOp τ + | protected BLOBBASEFEE : BOp τ deriving DecidableEq, Repr /-- @@ -632,6 +634,8 @@ abbrev GASLIMIT {τ : OperationType} : Operation τ := .Block .GASLIMIT abbrev CHAINID {τ : OperationType} : Operation τ := .Block .CHAINID abbrev SELFBALANCE {τ : OperationType} : Operation τ := .Block .SELFBALANCE abbrev BASEFEE {τ : OperationType} : Operation τ := .Block .BASEFEE +abbrev BLOBHASH {τ : OperationType} : Operation τ := .Block .BLOBHASH +abbrev BLOBBASEFEE {τ : OperationType} : Operation τ := .Block .BLOBBASEFEE abbrev POP {τ : OperationType} : Operation τ := .StackMemFlow .POP abbrev MLOAD {τ : OperationType} : Operation τ := .StackMemFlow .MLOAD diff --git a/EvmYul/Semantics.lean b/EvmYul/Semantics.lean index 4cea13f..87322d2 100644 --- a/EvmYul/Semantics.lean +++ b/EvmYul/Semantics.lean @@ -66,6 +66,11 @@ private def dispatchExecutionEnvOp (debugMode : Bool) (τ : OperationType) (op : | .EVM => EVM.executionEnvOp debugMode op | .Yul => Yul.executionEnvOp op +private def dispatchUnaryExecutionEnvOp (debugMode : Bool) (τ : OperationType) (op : ExecutionEnv → UInt256 → UInt256) : Transformer τ := + match τ with + | .EVM => EVM.unaryExecutionEnvOp debugMode op + | .Yul => Yul.unaryExecutionEnvOp op + private def dispatchMachineStateOp (τ : OperationType) (op : MachineState → UInt256) : Transformer τ := match τ with | .EVM => EVM.machineStateOp op @@ -294,6 +299,9 @@ def step {τ : OperationType} (debugMode : Bool) (op : Operation τ) : Transform | τ, .GASLIMIT => dispatchStateOp τ EvmYul.State.gasLimit | τ, .CHAINID => dispatchStateOp τ EvmYul.State.chainId | τ, .SELFBALANCE => dispatchStateOp τ EvmYul.State.selfbalance + | τ, .BASEFEE => dispatchExecutionEnvOp debugMode τ EvmYul.basefee + | τ, .BLOBHASH => dispatchUnaryExecutionEnvOp debugMode τ blobhash + | τ, .BLOBBASEFEE => dispatchExecutionEnvOp debugMode τ EvmYul.ExecutionEnv.getBlobGasprice | .EVM, .POP => λ evmState ↦ diff --git a/EvmYul/State.lean b/EvmYul/State.lean index 7317337..9673a44 100644 --- a/EvmYul/State.lean +++ b/EvmYul/State.lean @@ -28,7 +28,8 @@ structure State where executionEnv : ExecutionEnv -- Instead of keeping a map from `parentHash` to `Block`, we instead store the blocks we need. - blocks : List Block + blocks : Blocks + genesisBlockHeader : BlockHeader -- TODO(Keccak Stuff + I guess this will be gone so no need to nuke the `Finmap` just now keccakMap : Batteries.RBMap (List UInt256) UInt256 compare diff --git a/EvmYul/State/Block.lean b/EvmYul/State/Block.lean index a97981f..355ee62 100644 --- a/EvmYul/State/Block.lean +++ b/EvmYul/State/Block.lean @@ -2,11 +2,16 @@ import Mathlib.Data.Finset.Basic import EvmYul.State.BlockHeader import EvmYul.State.Transaction +import EvmYul.State.Withdrawal namespace EvmYul instance : Repr (Finset BlockHeader) := ⟨λ _ _ ↦ "Dummy Repr for ommers. TODO - change this :)."⟩ +abbrev Transactions := Array Transaction + +abbrev Withdrawals := Array Withdrawal + /-- `Block`. `B`. Section 4.3. `blockHeader` `H` @@ -15,10 +20,17 @@ instance : Repr (Finset BlockHeader) := ⟨λ _ _ ↦ "Dummy Repr for ommers. TO -/ structure Block where blockHeader : BlockHeader - transactions : List Transaction - ommers : Finset BlockHeader := ∅ - deriving Inhabited, BEq, Repr + rlp : ByteArray + transactions : Transactions + withdrawals : Withdrawals + exception : String + -- An empty array which was previously reserved for ommer block headers, + ommers : Array BlockHeader := ∅ + -- blocknumber : Nat + deriving BEq, Inhabited, Repr attribute [deprecated] Block.ommers +abbrev Blocks := Array Block + end EvmYul diff --git a/EvmYul/State/BlockHeader.lean b/EvmYul/State/BlockHeader.lean index 98d851b..5f430d0 100644 --- a/EvmYul/State/BlockHeader.lean +++ b/EvmYul/State/BlockHeader.lean @@ -27,6 +27,7 @@ namespace EvmYul `parentBeaconBlockRoot` (EIP-4877) -/ structure BlockHeader where + hash : UInt256 parentHash : UInt256 ommersHash : UInt256 beneficiary : AccountAddress @@ -46,8 +47,42 @@ structure BlockHeader where prevRandao : UInt256 baseFeePerGas : ℕ parentBeaconBlockRoot : ByteArray - withdrawalsRoot : ByteArray -deriving DecidableEq, Inhabited, Repr + withdrawalsRoot : Option ByteArray + blobGasUsed : Option UInt256 + excessBlobGas : Option UInt256 +deriving DecidableEq, Inhabited, Repr, BEq + +def TARGET_BLOB_GAS_PER_BLOCK := 393216 + +def calcExcessBlobGas (parent : BlockHeader) : Option UInt256 := do + let parentExcessBlobGas ← parent.excessBlobGas + let parentBlobGasUsed ← parent.blobGasUsed + if parentExcessBlobGas + parentBlobGasUsed < TARGET_BLOB_GAS_PER_BLOCK then + pure 0 + else + pure <| parentExcessBlobGas + parentBlobGasUsed - TARGET_BLOB_GAS_PER_BLOCK + +-- See https://eips.ethereum.org/EIPS/eip-4844#gas-accounting +partial def fakeExponential0 (i output factor numerator denominator : UInt256) : (numeratorAccum : UInt256) → UInt256 + | 0 => + output / denominator + | numeratorAccum => + let output := output + numeratorAccum + let numeratorAccum := (numeratorAccum * numerator) / (denominator * i) + let i := i + 1 + fakeExponential0 i output factor numerator denominator numeratorAccum + +def fakeExponential (factor numerator denominator : UInt256) : UInt256 := + fakeExponential0 1 0 factor numerator denominator (factor * denominator) + +def MIN_BASE_FEE_PER_BLOB_GAS := 1 +def BLOB_BASE_FEE_UPDATE_FRACTION := 3338477 + +def BlockHeader.getBlobGasprice (h : BlockHeader) : UInt256 := + fakeExponential + MIN_BASE_FEE_PER_BLOB_GAS + (h.excessBlobGas.getD 0) + BLOB_BASE_FEE_UPDATE_FRACTION attribute [deprecated] BlockHeader.difficulty attribute [deprecated] BlockHeader.nonce diff --git a/EvmYul/State/ExecutionEnv.lean b/EvmYul/State/ExecutionEnv.lean index 3b2c2e5..07fdb93 100644 --- a/EvmYul/State/ExecutionEnv.lean +++ b/EvmYul/State/ExecutionEnv.lean @@ -28,9 +28,19 @@ structure ExecutionEnv := header : BlockHeader depth : ℕ perm : Bool + blobVersionedHashes : List ByteArray deriving DecidableEq, Inhabited, Repr def prevRandao (e : ExecutionEnv) : UInt256 := e.header.prevRandao +def basefee (e : ExecutionEnv) : UInt256 := + e.header.baseFeePerGas + +def ExecutionEnv.getBlobGasprice (e : ExecutionEnv) : UInt256 := e.header.getBlobGasprice + +def blobhash (e : ExecutionEnv) (i : UInt256) : UInt256 := + e.blobVersionedHashes[i]?.option 0 + (.ofNat ∘ fromBytesBigEndian ∘ Array.data ∘ ByteArray.data) + end EvmYul diff --git a/EvmYul/State/Transaction.lean b/EvmYul/State/Transaction.lean index 86ee604..3fc0d2a 100644 --- a/EvmYul/State/Transaction.lean +++ b/EvmYul/State/Transaction.lean @@ -21,14 +21,14 @@ open Batteries (RBMap RBSet) TODO: In case of recipient = none, it means contract creation and data should be treated as init? -/ structure Transaction.Base where - nonce : UInt256 - gasLimit : UInt256 - recipient : Option AccountAddress - value : UInt256 - r : ByteArray - s : ByteArray - data : ByteArray - dbgSender : AccountAddress + nonce : UInt256 + gasLimit : UInt256 + recipient : Option AccountAddress + value : UInt256 + r : ByteArray + s : ByteArray + data : ByteArray + expectedSender : AccountAddress deriving BEq, Repr -- "EIP-2930 (type 1) and EIP-1559 (type 2) transactions also have:"" @@ -107,25 +107,34 @@ structure DynamicFeeTransaction extends Transaction.Base, Transaction.WithAccess maxPriorityFeePerGas : UInt256 deriving BEq, Repr +structure BlobTransaction extends DynamicFeeTransaction where + maxFeePerBlobGas : UInt256 + blobVersionedHashes : List ByteArray +deriving BEq, Repr + inductive Transaction where | legacy : LegacyTransaction → Transaction | access : AccessListTransaction → Transaction | dynamic : DynamicFeeTransaction → Transaction + | blob : BlobTransaction → Transaction deriving BEq, Repr def Transaction.base : Transaction → Transaction.Base | legacy t => t.toBase | access t => t.toBase | dynamic t => t.toBase + | blob t => t.toBase def Transaction.getAccessList : Transaction → Array (AccountAddress × Array UInt256) | legacy _ => #[] | access t => RBSet.toList t.accessList |>.toArray | dynamic t => RBSet.toList t.accessList |>.toArray + | blob t => RBSet.toList t.accessList |>.toArray -def Transaction.type : Transaction → Nat +def Transaction.type : Transaction → UInt8 | .legacy _ => 0 | .access _ => 1 | .dynamic _ => 2 + | .blob _ => 3 end EvmYul diff --git a/EvmYul/State/TransactionOps.lean b/EvmYul/State/TransactionOps.lean index be8bbb4..47b7543 100644 --- a/EvmYul/State/TransactionOps.lean +++ b/EvmYul/State/TransactionOps.lean @@ -1,11 +1,31 @@ import EvmYul.State.Transaction +import EvmYul.State.BlockHeader +import EvmYul.State.ExecutionEnv namespace EvmYul def Transaction.to? : Transaction → Option AccountAddress - | .legacy t | .access t | .dynamic t => t.recipient + -- TODO: Blob transactions can never have `to` + | .legacy t | .access t | .dynamic t | .blob t => t.recipient def Transaction.data : Transaction → ByteArray - | .legacy t | .access t | .dynamic t => t.data + | .legacy t | .access t | .dynamic t | .blob t => t.data + +def GAS_PER_BLOB := 2^17 +def VERSIONED_HASH_VERSION_KZG : UInt8 := 1 + +def getTotalBlobGas (t : Transaction) : Option ℕ := + match t with + | .blob t => GAS_PER_BLOB * t.blobVersionedHashes.length + | _ => none + +def Transaction.blobVersionedHashes (t : Transaction) : List ByteArray := + match t with + | .blob t => t.blobVersionedHashes + | _ => [] + +def calcBlobFee (header: BlockHeader) (t : Transaction) : ℕ := + let totalBlobGas := getTotalBlobGas t |>.getD 0 + totalBlobGas * header.getBlobGasprice end EvmYul diff --git a/EvmYul/State/Withdrawal.lean b/EvmYul/State/Withdrawal.lean index 55613f3..dd02601 100644 --- a/EvmYul/State/Withdrawal.lean +++ b/EvmYul/State/Withdrawal.lean @@ -20,7 +20,7 @@ structure Withdrawal where validatorIndex : UInt64 address : AccountAddress amount : UInt64 -deriving Repr +deriving Repr, BEq namespace Withdrawal diff --git a/EvmYul/StateOps.lean b/EvmYul/StateOps.lean index 433d168..4f9e927 100644 --- a/EvmYul/StateOps.lean +++ b/EvmYul/StateOps.lean @@ -147,7 +147,6 @@ def sload (self : State) (spos : UInt256) : State × UInt256 := (state', v) def sstore (self : State) (spos sval : UInt256) : State := - -- dbg_trace "sstore called with spos: {spos} sval: {sval}" let Iₐ := self.executionEnv.codeOwner self.lookupAccount Iₐ |>.option self λ acc ↦ let self' := self.setAccount Iₐ (acc.updateStorage spos sval) diff --git a/EvmYul/Yul/Exception.lean b/EvmYul/Yul/Exception.lean index b548473..f7f455b 100644 --- a/EvmYul/Yul/Exception.lean +++ b/EvmYul/Yul/Exception.lean @@ -6,7 +6,7 @@ inductive Exception where | InvalidArguments : Exception | NotEncodableRLP : Exception | InvalidInstruction : Exception - | StopInvoked : Exception + -- | StopInvoked : Exception end Yul diff --git a/EvmYul/Yul/PrimOps.lean b/EvmYul/Yul/PrimOps.lean index 7ab9d70..2c3221e 100644 --- a/EvmYul/Yul/PrimOps.lean +++ b/EvmYul/Yul/PrimOps.lean @@ -36,6 +36,12 @@ def execQuadOp (f : Primop.Quaternary) : Transformer def executionEnvOp (op : ExecutionEnv → UInt256) : Transformer := λ yulState _ ↦ .ok (yulState, .some <| op yulState.executionEnv) +def unaryExecutionEnvOp (op : ExecutionEnv → UInt256 → UInt256) : Transformer := + λ yulState lits ↦ + match lits with + | [a] => .ok (yulState, .some <| op yulState.executionEnv a) + | _ => .error .InvalidArguments + def machineStateOp (op : MachineState → UInt256) : Transformer := λ yulState _ ↦ .ok (yulState, .some <| op yulState.toMachineState)