Fix CI foundry tests and align EVM asm

Author: Th0rgal

.github/workflows/test.yml

@@ -101,3 +101,26 @@ jobs:
         env:
           RPC_URL: http://127.0.0.1:8545
         run: ./scripts/deploy_example.sh
+
+  foundry-legacy:
+    name: Foundry legacy contract tests
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+          submodules: recursive
+
+      - name: Install Foundry
+        working-directory: research/lean_only_proto
+        run: ./scripts/install_foundry.sh
+
+      - name: Install solc
+        working-directory: research/lean_only_proto
+        run: ./scripts/install_solc.sh
+
+      - name: Run legacy Foundry tests
+        working-directory: legacy/foundry
+        run: forge test

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "legacy/foundry/lib/forge-std"]
+	path = legacy/foundry/lib/forge-std
+	url = https://github.com/foundry-rs/forge-std

legacy/foundry/foundry.lock

@@ -0,0 +1,8 @@
+{
+  "lib/forge-std": {
+    "tag": {
+      "name": "v1.14.0",
+      "rev": "1801b0541f4fda118a10798fd3486bb7051c5dd6"
+    }
+  }
+}

legacy/foundry/lib/forge-std

@@ -131,6 +131,9 @@ def exampleEntry5 : EntryPoint :=
     selector := 0xb61d4088
     returns := false }
 
+def exampleEntries : List EntryPoint :=
+  [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5]
+
 def healthEntrySet : EntryPoint :=
   { name := "setRisk"
     args := ["collateral", "debt", "minHF"]
@@ -154,4 +157,7 @@ def healthEntryCheck : EntryPoint :=
     selector := 0x1753bbd7
     returns := false }
 
+def healthEntries : List EntryPoint :=
+  [healthEntrySet, healthEntryCheck]
+
 end DumbContracts.Compiler

research/lean_only_proto/DumbContracts/Compiler.lean

@@ -23,13 +23,30 @@ def directProgramAsm : List String :=
   , "EQ"
   , "PUSH tag_addSlot"
   , "JUMPI"
+  , "DUP1"
   , "PUSH4 0x49f583e3"
   , "EQ"
   , "PUSH tag_guardedAddSlot"
   , "JUMPI"
+  , "PUSH4 0xb61d4088"
+  , "EQ"
+  , "PUSH tag_maxStore"
+  , "JUMPI"
   , "PUSH0"
   , "DUP1"
   , "REVERT"
+  , "tag_maxStore:"
+  , "PUSH ret_maxStore"
+  , "PUSH1 0x44"
+  , "CALLDATALOAD"
+  , "PUSH1 0x24"
+  , "CALLDATALOAD"
+  , "PUSH1 0x04"
+  , "CALLDATALOAD"
+  , "PUSH fn_maxStore"
+  , "JUMP"
+  , "ret_maxStore:"
+  , "STOP"
   , "tag_guardedAddSlot:"
   , "PUSH ret_guardedAddSlot"
   , "PUSH1 0x24"
@@ -110,6 +127,36 @@ def directProgramAsm : List String :=
   , "PUSH0"
   , "PUSH guardedAddSlot_check"
   , "JUMP"
+  , "fn_maxStore:"
+  , "SWAP1"
+  , "DUP3"
+  , "SWAP1"
+  , "DUP2"
+  , "DUP2"
+  , "GT"
+  , "PUSH maxStore_then"
+  , "JUMPI"
+  , "maxStore_check:"
+  , "GT"
+  , "ISZERO"
+  , "PUSH maxStore_else"
+  , "JUMPI"
+  , "maxStore_join:"
+  , "POP"
+  , "POP"
+  , "JUMP"
+  , "maxStore_else:"
+  , "SSTORE"
+  , "PUSH0"
+  , "DUP1"
+  , "PUSH maxStore_join"
+  , "JUMP"
+  , "maxStore_then:"
+  , "DUP1"
+  , "DUP4"
+  , "SSTORE"
+  , "PUSH maxStore_check"
+  , "JUMP"
   ]
 
 def pretty (lines : List String) : String :=

research/lean_only_proto/DumbContracts/EvmAsm.lean

@@ -8,10 +8,10 @@ open DumbContracts.Yul
 
 -- Emit Yul/EVM artifacts.
 def main : IO Unit := do
-  let exampleProg := compileProgram [exampleEntry, exampleEntry2, exampleEntry3, exampleEntry4, exampleEntry5]
+  let exampleProg := compileProgram exampleEntries
   let exampleYul := Yul.Pretty.program exampleProg
   IO.FS.writeFile "out/example.yul" exampleYul
-  let healthProg := compileProgram [healthEntrySet, healthEntryCheck]
+  let healthProg := compileProgram healthEntries
   let healthYul := Yul.Pretty.program healthProg
   IO.FS.writeFile "out/health.yul" healthYul
   let evmAsm := DumbContracts.EvmAsm.pretty DumbContracts.EvmAsm.directProgramAsm