Merge pull request #529 from ethereum/tstore-samalws-msoos

TSTORE/TLOAD + MCOPY + updated SelfDestruct

.github/workflows/build.yml

@@ -53,13 +53,13 @@ jobs:
       - uses: DeterminateSystems/magic-nix-cache-action@main
       # cabal complains if we don't do this...
       - name: cabal update
-        run: nix-shell --pure --command "cabal update"
+        run: nix develop --command bash -c "cabal update"
       # can't be run in nix build due to network usage
       - name: run rpc tests
-        run: nix-shell --pure --command "cabal --active-repositories=:none run rpc-tests"
+        run: nix develop --command bash -c "cabal --active-repositories=:none run rpc-tests"
       # if we run this in nix build we often get killed due to oom in ci
       - name: run ethereum tests
-        run: nix-shell --pure --command "cabal --active-repositories=:none run ethereum-tests"
+        run: nix develop --command bash -c "cabal --active-repositories=:none run ethereum-tests"
 
   build-windows-bitwuzla:
     name: bitwuzla-build (win64 target)
@@ -174,13 +174,13 @@ jobs:
       - uses: actions/checkout@v4
         with:
           repository: ethereum/solidity
-          ref: 1c8745c54a239d20b6fb0f79a8bd2628d779b27e
+          ref: 8a97fa7a1db1ec509221ead6fea6802c684ee887
           path: ethereum-solidity
 
       - uses: actions/checkout@v4
         with:
           repository: ethereum/tests
-          ref: v12.2
+          ref: v13
           path: ethereum-tests
 
       - uses: actions/checkout@v4
@@ -207,7 +207,7 @@ jobs:
           echo CVC5_PATH="$PWD/cvc5-Win64-static/bin" >> "$GITHUB_ENV"
           # solc
           mkdir solc
-          curl --retry 5 -fsSL https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-windows.exe -o solc/solc.exe
+          curl --retry 5 -fsSL https://github.com/ethereum/solidity/releases/download/v0.8.26/solc-windows.exe -o solc/solc.exe
           echo DAPP_SOLC="$PWD/solc/solc.exe" >> "$GITHUB_ENV"
           echo DAPP_SOLC_PATH="$PWD/solc/" >> "$GITHUB_ENV"
           # repos

CHANGELOG.md

@@ -30,7 +30,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Add `freshAddresses` field in `VMOpts` so that initial fresh address can be given as input
 - Add documentation about limitations and workarounds
 - More verbose error messages in case of symbolic arguments to opcode
-* Tests to enforce that in Expr and Prop, constants are on the LHS whenever possible
+- Tests to enforce that in Expr and Prop, constants are on the LHS whenever possible
+- Support for MCOPY and TSTORE/TLOAD, i.e. EIP 5656 + 1153 + 4788
 
 ## Fixed
 - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing
@@ -43,6 +44,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   a different approach.
 - `initial-storage` option of `hevm symbolic` is respected
 - `caller` option of `hevm symbolic` is now respected
+* Thanks to the new simplification rules, we can now enable more conformance tests
 
 ## [0.53.0] - 2024-02-23
 

bench/bench.hs

@@ -82,7 +82,7 @@ runBCTest x =
   result <- Stepper.interpret (Fetch.zero 0 Nothing) vm0 Stepper.runFully
   writeTrace vm0
 
-  maybeReason <- BCTests.checkExpectation False x result
+  maybeReason <- BCTests.checkExpectation x result
   pure $ isNothing maybeReason
 
 

cli/cli.hs

@@ -498,6 +498,7 @@ vmFromCommand cmd = do
           , txAccessList   = mempty -- TODO: support me soon
           , allowFFI       = False
           , freshAddresses = 0
+          , beaconRoot     = 0
           }
         word f def = fromMaybe def (f cmd)
         word64 f def = fromMaybe def (f cmd)
@@ -583,6 +584,7 @@ symvmFromCommand cmd calldata = do
       , txAccessList   = mempty
       , allowFFI       = False
       , freshAddresses = 0
+      , beaconRoot     = 0
       }
     word f def = fromMaybe def (f cmd)
     word64 f def = fromMaybe def (f cmd)

flake.nix

@@ -4,18 +4,17 @@
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
     nixpkgs.url = "github:nixos/nixpkgs/nixpkgs-unstable";
-    # TODO: we are broken with latest foundry
-    foundry.url = "github:shazow/foundry.nix/6089aad0ef615ac8c7b0c948d6052fa848c99523";
+    foundry.url = "github:shazow/foundry.nix/47f8ae49275eeff9bf0526d45e3c1f76723bb5d3";
     flake-compat = {
       url = "github:edolstra/flake-compat";
       flake = false;
     };
     solidity = {
-      url = "github:ethereum/solidity/1c8745c54a239d20b6fb0f79a8bd2628d779b27e";
+      url = "github:ethereum/solidity/8a97fa7a1db1ec509221ead6fea6802c684ee887";
       flake = false;
     };
     ethereum-tests = {
-      url = "github:ethereum/tests/v12.4";
+      url = "github:ethereum/tests/v13";
       flake = false;
     };
     forge-std = {
@@ -36,7 +35,7 @@
           overlays = [solc-pkgs.overlay];
           config = { allowBroken = true; };
         });
-        solc = (solc-pkgs.mkDefault pkgs pkgs.solc_0_8_24);
+        solc = (solc-pkgs.mkDefault pkgs pkgs.solc_0_8_26);
         testDeps = with pkgs; [
           go-ethereum
           solc
@@ -185,6 +184,7 @@
         in haskellPackages.shellFor {
           packages = _: [ (hevmBase pkgs) ];
           buildInputs = [
+            curl
             haskellPackages.cabal-install
             mdbook
             yarn