ci: Fix ignored.yml and update FFI tests

.github/workflows/ignored.yml

@@ -14,26 +14,43 @@ concurrency:
 
 jobs:
   ignored-test:
-    runs-on: warp-ubuntu-latest-x64-32x # Needs 128 GB RAM for Lean compilation
+    runs-on: warp-ubuntu-latest-x64-32x
     steps:
       - uses: actions/checkout@v6
       - uses: actions-rust-lang/setup-rust-toolchain@v1
+      # Only restore the cache, since `ci.yml` will save the test binary to the cache first
+      - uses: actions/cache/restore@v4
+        with:
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
       - uses: leanprover/lean-action@v1
         with:
           auto-config: false
-          test: true
-          test-args: "-- --ignored"
+          # `test-args` is currently broken, so we run `lake test` separately
+          # Restore once https://github.com/leanprover/lean-action/pull/153 is merged
+          # test: true
+          # test-args: "-- --ignored"
+          use-github-cache: false
+      - run: lake test -- --ignored
 
-  valgrind:
-    runs-on: warp-ubuntu-latest-x64-16x
+  valgrind-ffi:
+    runs-on: warp-ubuntu-latest-x64-8x
     steps:
       - uses: actions/checkout@v6
       - uses: actions-rust-lang/setup-rust-toolchain@v1
+      # Only restore the cache, since `ci.yml` will save the test binary to the cache first
+      - uses: actions/cache/restore@v4
+        with:
+          path: .lake
+          key: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: lake-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
       - uses: leanprover/lean-action@v1
         with:
           auto-config: false
           build: true
           build-args: "IxTests"
+          use-github-cache: false
       - name: Install valgrind
         run: sudo apt-get update && sudo apt-get install -y valgrind
       - name: Run tests under valgrind
@@ -44,4 +61,4 @@ jobs:
             --errors-for-leak-kinds=definite \
             --track-origins=yes \
             --error-exitcode=1 \
-            .lake/build/bin/IxTests -- --include-ignored aiur aiur-hashes ixvm
+            .lake/build/bin/IxTests -- ffi

Ix/Ixon.lean

@@ -1034,13 +1034,13 @@ instance : Serialize Constant where
 /-! ## Convenience functions for serialization -/
 
 def serUniv (u : Univ) : ByteArray := runPut (putUniv u)
-def desUniv (bytes : ByteArray) : Except String Univ := runGet getUniv bytes
+def deUniv (bytes : ByteArray) : Except String Univ := runGet getUniv bytes
 
 def serExpr (e : Expr) : ByteArray := runPut (putExpr e)
-def desExpr (bytes : ByteArray) : Except String Expr := runGet getExpr bytes
+def deExpr (bytes : ByteArray) : Except String Expr := runGet getExpr bytes
 
 def serConstant (c : Constant) : ByteArray := runPut (putConstant c)
-def desConstant (bytes : ByteArray) : Except String Constant := runGet getConstant bytes
+def deConstant (bytes : ByteArray) : Except String Constant := runGet getConstant bytes
 
 /-! ## Metadata Serialization -/
 
@@ -1359,7 +1359,7 @@ instance : Serialize Comm where
 
 /-- Convenience serialization for Comm (untagged). -/
 def serComm (c : Comm) : ByteArray := runPut (putComm c)
-def desComm (bytes : ByteArray) : Except String Comm := runGet getComm bytes
+def deComm (bytes : ByteArray) : Except String Comm := runGet getComm bytes
 
 /-- Serialize Comm with Tag4{0xE, 5} header. -/
 def putCommTagged (c : Comm) : PutM Unit := do
@@ -1765,7 +1765,7 @@ end Env
 def serEnv (env : Env) : ByteArray := runPut (Env.putEnv env)
 
 /-- Deserialize an Env from bytes. -/
-def desEnv (bytes : ByteArray) : Except String Env := runGet Env.getEnv bytes
+def deEnv (bytes : ByteArray) : Except String Env := runGet Env.getEnv bytes
 
 /-- Compute section sizes for debugging. Returns (blobs, consts, names, named, comms). -/
 def envSectionSizes (env : Env) : Nat × Nat × Nat × Nat × Nat := Id.run do
@@ -1825,12 +1825,12 @@ opaque rsSerEnvFFI : @& RawEnv → ByteArray
 def rsSerEnv (env : Env) : ByteArray :=
   rsSerEnvFFI env.toRawEnv
 
-@[extern "rs_des_env"]
-opaque rsDesEnvFFI : @& ByteArray → Except String RawEnv
+@[extern "rs_de_env"]
+opaque rsDeEnvFFI : @& ByteArray → Except String RawEnv
 
 /-- Deserialize bytes to an Ixon.Env using Rust. -/
-def rsDesEnv (bytes : ByteArray) : Except String Env :=
-  return (← rsDesEnvFFI bytes).toEnv
+def rsDeEnv (bytes : ByteArray) : Except String Env :=
+  return (← rsDeEnvFFI bytes).toEnv
 
 end Ixon
 

Tests/Aiur/Hashes.lean

@@ -4,11 +4,9 @@ public import Tests.Aiur.Common
 public import Ix.IxVM.ByteStream
 public import Ix.IxVM.Blake3
 public import Ix.IxVM.Sha256
+public import Tests.Sha256
 public import Blake3
 
-@[extern "rs_sha256"]
-opaque rsSha256 : @&ByteArray → ByteArray
-
 def mkBlake3HashTestCase (size : Nat) : AiurTestCase :=
   let inputBytes := Array.range size |>.map Nat.toUInt8
   let outputBytes := Blake3.hash ⟨inputBytes⟩ |>.val.data
@@ -19,7 +17,7 @@ def mkBlake3HashTestCase (size : Nat) : AiurTestCase :=
 
 def mkSha256HashTestCase (size : Nat) : AiurTestCase :=
   let inputBytes := Array.range size |>.map Nat.toUInt8
-  let outputBytes := rsSha256 ⟨inputBytes⟩ |>.data
+  let outputBytes := Sha256.hash ⟨inputBytes⟩ |>.data
   let input := inputBytes.map .ofUInt8
   let output := outputBytes.map .ofUInt8
   let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0]

Tests/FFI.lean

@@ -7,10 +7,11 @@ module
 public import Tests.FFI.Basic
 public import Tests.FFI.Ix
 public import Tests.FFI.Ixon
+public import Tests.FFI.Lifecycle
 
 namespace Tests.FFI
 
 public def suite : List LSpec.TestSeq :=
-  Tests.FFI.Basic.suite ++ Tests.FFI.Ix.suite ++ Tests.FFI.Ixon.suite
+  Tests.FFI.Basic.suite ++ Tests.FFI.Ix.suite ++ Tests.FFI.Ixon.suite ++ Tests.FFI.Lifecycle.suite
 
 end Tests.FFI

Tests/FFI/Basic.lean

@@ -94,6 +94,9 @@ def largeNatTests : TestSeq :=
 def hashMapEq (m1 m2 : Std.HashMap Nat Nat) : Bool :=
   m1.size == m2.size && m1.toList.all fun (k, v) => m2.get? k == some v
 
+def dHashMapRawEq (m1 m2 : DHashMapRaw Nat (fun _ => Nat)) : Bool :=
+  m1.size == m2.size && m1.toList.all fun ⟨k, v⟩ => m2.get? k == some v
+
 def assocListEq (l1 l2 : AssocList Nat (fun _ => Nat)) : Bool :=
   let toSimpleList (l : AssocList Nat (fun _ => Nat)) : List (Nat × Nat) :=
     l.toList.map fun ⟨k, v⟩ => (k, v)
@@ -111,6 +114,14 @@ def hashMapTests : TestSeq :=
   test "HashMap empty" (hashMapEq (roundtripHashMapNatNat {}) {}) ++
   test "HashMap single" (hashMapEq (roundtripHashMapNatNat (({} : Std.HashMap Nat Nat).insert 1 42)) (({} : Std.HashMap Nat Nat).insert 1 42))
 
+def dHashMapRawTests : TestSeq :=
+  let emptyMap : DHashMapRaw Nat (fun _ => Nat) := {}
+  let single : DHashMapRaw Nat (fun _ => Nat) := ({} : DHashMapRaw Nat (fun _ => Nat)).insert 1 42
+  let double : DHashMapRaw Nat (fun _ => Nat) := (({} : DHashMapRaw Nat (fun _ => Nat)).insert 1 42).insert 2 99
+  test "DHashMapRaw empty" (dHashMapRawEq (roundtripDHashMapRawNatNat emptyMap) emptyMap) ++
+  test "DHashMapRaw single" (dHashMapRawEq (roundtripDHashMapRawNatNat single) single) ++
+  test "DHashMapRaw double" (dHashMapRawEq (roundtripDHashMapRawNatNat double) double)
+
 def boolTests : TestSeq :=
   test "Bool true" (roundtripBool true == true) ++
   test "Bool false" (roundtripBool false == false)
@@ -122,6 +133,7 @@ public def suite : List TestSeq := [
   largeNatTests,
   assocListTests,
   hashMapTests,
+  dHashMapRawTests,
   boolTests,
   checkIO "Nat roundtrip" (∀ n : Nat, roundtripNat n == n),
   checkIO "String roundtrip" (∀ s : String, roundtripString s == s),
@@ -131,6 +143,9 @@ public def suite : List TestSeq := [
   checkIO "Point roundtrip" (∀ p : Point, roundtripPoint p == p),
   checkIO "NatTree roundtrip" (∀ t : NatTree, roundtripNatTree t == t),
   checkIO "HashMap Nat Nat roundtrip" (∀ m : Std.HashMap Nat Nat, hashMapEq (roundtripHashMapNatNat m) m),
+  checkIO "DHashMapRaw Nat Nat roundtrip" (∀ m : Std.HashMap Nat Nat,
+    let raw := m.toList.foldl (init := ({} : DHashMapRaw Nat (fun _ => Nat))) fun acc (k, v) => acc.insert k v
+    dHashMapRawEq (roundtripDHashMapRawNatNat raw) raw),
 ]
 
 end Tests.FFI.Basic