diff --git a/.github/workflows/ignored.yml b/.github/workflows/ignored.yml
index cb0af803..38c7e7a2 100644
--- a/.github/workflows/ignored.yml
+++ b/.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
diff --git a/Ix/Ixon.lean b/Ix/Ixon.lean
index dd3f1113..20317255 100644
--- a/Ix/Ixon.lean
+++ b/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
 
diff --git a/Tests/Aiur/Hashes.lean b/Tests/Aiur/Hashes.lean
index 63d53b9b..b185fa2c 100644
--- a/Tests/Aiur/Hashes.lean
+++ b/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]
diff --git a/Tests/FFI.lean b/Tests/FFI.lean
index 6c98b2e1..dedad854 100644
--- a/Tests/FFI.lean
+++ b/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
diff --git a/Tests/FFI/Basic.lean b/Tests/FFI/Basic.lean
index 37462f6d..2f3df4d8 100644
--- a/Tests/FFI/Basic.lean
+++ b/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
diff --git a/Tests/FFI/Lifecycle.lean b/Tests/FFI/Lifecycle.lean
new file mode 100644
index 00000000..3f3b54a4
--- /dev/null
+++ b/Tests/FFI/Lifecycle.lean
@@ -0,0 +1,253 @@
+/-
+  FFI lifecycle tests: non-roundtrip code paths focused on memory management.
+  Exercises external objects, serialization pipelines, and hash FFI.
+-/
+module
+
+public import LSpec
+public import Ix.Keccak
+public import Tests.Sha256
+public import Ix.Ixon
+public import Tests.Gen.Ixon
+public import Tests.FFI.Ixon
+
+open LSpec SlimCheck Gen Ixon
+open Tests.Gen.Ixon
+open Tests.FFI.Ixon (rawEnvEq)
+
+namespace Tests.FFI.Lifecycle
+
+/-! ## Keccak external object lifecycle tests -/
+
+/-- Basic hash lifecycle: init → update → finalize -/
+def keccakBasicTests : TestSeq :=
+  -- Known test vector: SHA3-256 of [0]
+  let input : ByteArray := ⟨#[0]⟩
+  let expected : ByteArray := ⟨#[
+    188, 54, 120, 158, 122, 30, 40, 20, 54, 70, 66, 41, 130, 143, 129, 125,
+    102, 18, 247, 180, 119, 214, 101, 145, 255, 150, 169, 224, 100, 188, 201, 138
+  ]⟩
+  let result := Keccak.hash input
+  test "Keccak basic hash [0]" (result == expected) ++
+  -- Empty input
+  let emptyResult := Keccak.hash ByteArray.empty
+  test "Keccak empty input produces 32 bytes" (emptyResult.size == 32) ++
+  -- Determinism: same input twice
+  let result2 := Keccak.hash input
+  test "Keccak deterministic" (result == result2)
+
+/-- Multi-update lifecycle: init → update × N → finalize
+    Creates N+1 external Hasher objects, exercising the destructor path. -/
+def keccakMultiUpdateTests : TestSeq :=
+  -- Multi-update should produce same result as single update of concatenated input
+  let chunk1 : ByteArray := ⟨#[1, 2, 3]⟩
+  let chunk2 : ByteArray := ⟨#[4, 5, 6]⟩
+  let chunk3 : ByteArray := ⟨#[7, 8, 9]⟩
+  let combined : ByteArray := ⟨#[1, 2, 3, 4, 5, 6, 7, 8, 9]⟩
+  let singleHash := Keccak.hash combined
+  let multiHash :=
+    let h := Keccak.Hasher.init ()
+    let h := h.update chunk1
+    let h := h.update chunk2
+    let h := h.update chunk3
+    h.finalize
+  test "Keccak multi-update == single" (singleHash == multiHash) ++
+  -- Many updates to stress the external object destructor
+  let manyHash := Id.run do
+    let mut h := Keccak.Hasher.init ()
+    for i in [:20] do
+      h := h.update ⟨#[i.toUInt8]⟩
+    return h.finalize
+  test "Keccak 20 updates produces 32 bytes" (manyHash.size == 32)
+
+/-- Large input to exercise large ByteArray across FFI boundary -/
+def keccakLargeInputTests : TestSeq :=
+  let large : ByteArray := ⟨Array.range 4096 |>.map Nat.toUInt8⟩
+  let result := Keccak.hash large
+  test "Keccak large input (4096 bytes)" (result.size == 32) ++
+  -- Verify determinism on large input
+  let result2 := Keccak.hash large
+  test "Keccak large input deterministic" (result == result2)
+
+/-! ## SHA256 hashing tests -/
+
+def sha256Tests : TestSeq :=
+  -- Empty input: SHA-256("") = e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
+  let emptyHash := Sha256.hash ByteArray.empty
+  let expectedEmpty : ByteArray := ⟨#[
+    0xe3, 0xb0, 0xc4, 0x42, 0x98, 0xfc, 0x1c, 0x14, 0x9a, 0xfb, 0xf4, 0xc8, 0x99, 0x6f, 0xb9, 0x24,
+    0x27, 0xae, 0x41, 0xe4, 0x64, 0x9b, 0x93, 0x4c, 0xa4, 0x95, 0x99, 0x1b, 0x78, 0x52, 0xb8, 0x55
+  ]⟩
+  test "SHA256 empty" (emptyHash == expectedEmpty) ++
+  -- "abc": SHA-256("abc") = ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad
+  let abcHash := Sha256.hash ⟨#[0x61, 0x62, 0x63]⟩
+  let expectedAbc : ByteArray := ⟨#[
+    0xba, 0x78, 0x16, 0xbf, 0x8f, 0x01, 0xcf, 0xea, 0x41, 0x41, 0x40, 0xde, 0x5d, 0xae, 0x22, 0x23,
+    0xb0, 0x03, 0x61, 0xa3, 0x96, 0x17, 0x7a, 0x9c, 0xb4, 0x10, 0xff, 0x61, 0xf2, 0x00, 0x15, 0xad
+  ]⟩
+  test "SHA256 abc" (abcHash == expectedAbc) ++
+  -- Determinism: hash same input twice
+  let hash1 := Sha256.hash ⟨#[1, 2, 3]⟩
+  let hash2 := Sha256.hash ⟨#[1, 2, 3]⟩
+  test "SHA256 deterministic" (hash1 == hash2) ++
+  test "SHA256 produces 32 bytes" (hash1.size == 32)
+
+/-! ## Ixon serialization roundtrip tests (ser_env → de_env) -/
+
+/-- Compare RawEnv after serde: only check consts, named, comms.
+    The serde pipeline normalizes the names table and may add string blobs
+    for name components, so names and blobs are not compared structurally. -/
+private def serdeEnvEq (a b : RawEnv) : Bool :=
+  a.consts.size == b.consts.size &&
+  a.named.size == b.named.size &&
+  a.comms.size == b.comms.size &&
+  a.consts.all fun rc =>
+    b.consts.any fun rc' => rc.addr == rc'.addr &&
+      rc.const.info == rc'.const.info &&
+      rc.const.sharing.size == rc'.const.sharing.size &&
+      rc.const.refs.size == rc'.const.refs.size &&
+      rc.const.univs.size == rc'.const.univs.size
+
+def serdeTests : TestSeq :=
+  -- Empty RawEnv
+  let empty : RawEnv := { consts := #[], named := #[], blobs := #[], comms := #[] }
+  let emptyBytes := rsSerEnvFFI empty
+  let emptyResult := rsDeEnvFFI emptyBytes
+  .individualIO "serde empty RawEnv" none (do
+    match emptyResult with
+    | .ok decoded => pure (serdeEnvEq decoded empty, 0, 0, if serdeEnvEq decoded empty then none else some "mismatch")
+    | .error e => pure (false, 0, 0, some s!"deserialization failed: {e}")) .done ++
+  -- RawEnv with data (include name entries for all referenced addresses)
+  let testAddr := Address.blake3 (ByteArray.mk #[1, 2, 3])
+  let testExpr : Expr := .sort 0
+  let testDef : Definition := {
+    kind := .defn, safety := .safe, lvls := 0,
+    typ := testExpr, value := testExpr
+  }
+  let testConst : Constant := {
+    info := .defn testDef, sharing := #[], refs := #[], univs := #[]
+  }
+  let testRawConst : RawConst := { addr := testAddr, const := testConst }
+  let testComm : Comm := { secret := testAddr, payload := testAddr }
+  let testRawComm : RawComm := { addr := testAddr, comm := testComm }
+  let testRawBlob : RawBlob := { addr := testAddr, bytes := ByteArray.mk #[1, 2, 3] }
+  let testName := Ix.Name.mkStr Ix.Name.mkAnon "test"
+  let testRawNamed : RawNamed := {
+    name := testName, addr := testAddr, constMeta := .empty
+  }
+  let testNameEntry : RawNameEntry := { addr := testAddr, name := testName }
+  let withData : RawEnv := {
+    consts := #[testRawConst],
+    named := #[testRawNamed],
+    blobs := #[testRawBlob],
+    comms := #[testRawComm],
+    names := #[testNameEntry]
+  }
+  let dataBytes := rsSerEnvFFI withData
+  let dataResult := rsDeEnvFFI dataBytes
+  .individualIO "serde RawEnv with data" none (do
+    match dataResult with
+    | .ok decoded => pure (serdeEnvEq decoded withData, 0, 0, if serdeEnvEq decoded withData then none else some "mismatch")
+    | .error e => pure (false, 0, 0, some s!"deserialization failed: {e}")) .done
+
+/-- Generate a ConstantInfo without embedded Address fields.
+    Projections contain Addresses that would need name entries;
+    these simpler variants only contain Expr/Univ/Nat fields. -/
+private def genSimpleConstantInfo : Gen ConstantInfo :=
+  frequency [
+    (10, .defn <$> genDefinition),
+    (5, .recr <$> genRecursor),
+    (10, .axio <$> genAxiom),
+    (10, .quot <$> genQuotient),
+  ]
+
+/-- Generate a well-formed RawEnv where every address has a name entry.
+    The serde pipeline requires all addresses to be resolvable in the
+    name table; random RawEnvs almost always violate this. -/
+private def genSerdeRawEnv : Gen RawEnv := do
+  -- Build a pool of (address, name) pairs; all addresses used below come from here
+  let poolSize ← Gen.choose Nat 2 8
+  let mut pool : Array (Address × Ix.Name) := #[]
+  for i in [:poolSize] do
+    let addr ← genAddress
+    pool := pool.push (addr, Ix.Name.mkNat Ix.Name.mkAnon i)
+  let pickAddr : Gen Address := do
+    let idx ← Gen.choose Nat 0 (pool.size - 1)
+    pure pool[idx]!.1
+  -- Name entries for every address in the pool
+  let names : Array RawNameEntry := pool.map fun (addr, name) => { addr, name }
+  -- Consts: pool addresses, empty refs/sharing/univs (no extra address lookups)
+  let numConsts ← Gen.choose Nat 0 3
+  let mut consts : Array RawConst := #[]
+  for _ in [:numConsts] do
+    let addr ← pickAddr
+    let info ← genSimpleConstantInfo
+    consts := consts.push { addr, const := { info, sharing := #[], refs := #[], univs := #[] } }
+  -- Named: pool addresses with empty metadata
+  let numNamed ← Gen.choose Nat 0 3
+  let mut named : Array RawNamed := #[]
+  for _ in [:numNamed] do
+    let idx ← Gen.choose Nat 0 (pool.size - 1)
+    let (addr, name) := pool[idx]!
+    named := named.push { name, addr, constMeta := .empty }
+  -- Blobs: pool addresses
+  let numBlobs ← Gen.choose Nat 0 3
+  let mut blobs : Array RawBlob := #[]
+  for _ in [:numBlobs] do
+    let addr ← pickAddr
+    let bytes ← Tests.Gen.Ixon.genByteArray
+    blobs := blobs.push { addr, bytes }
+  -- Comms: pool addresses
+  let numComms ← Gen.choose Nat 0 2
+  let mut comms : Array RawComm := #[]
+  for _ in [:numComms] do
+    let addr ← pickAddr
+    let secret ← pickAddr
+    let payload ← pickAddr
+    comms := comms.push { addr, comm := { secret, payload } }
+  -- Deduplicate by key: the Rust side uses HashMaps, so duplicates collapse
+  let consts' := consts.foldl (init := (#[] : Array RawConst)) fun acc x =>
+    if acc.any (·.addr == x.addr) then acc else acc.push x
+  let named' := named.foldl (init := (#[] : Array RawNamed)) fun acc x =>
+    if acc.any (·.name == x.name) then acc else acc.push x
+  let blobs' := blobs.foldl (init := (#[] : Array RawBlob)) fun acc x =>
+    if acc.any (·.addr == x.addr) then acc else acc.push x
+  let comms' := comms.foldl (init := (#[] : Array RawComm)) fun acc x =>
+    if acc.any (·.addr == x.addr) then acc else acc.push x
+  pure { consts := consts', named := named', blobs := blobs', comms := comms', names }
+
+/-- Wrapper so we can give well-formed RawEnvs their own SampleableExt instance. -/
+private structure serdeRawEnv where
+  env : RawEnv
+
+private instance : Repr serdeRawEnv where
+  reprPrec e n := reprPrec e.env n
+
+private instance : Shrinkable serdeRawEnv where
+  shrink _ := []
+
+private instance : SampleableExt serdeRawEnv :=
+  SampleableExt.mkSelfContained (serdeRawEnv.mk <$> genSerdeRawEnv)
+
+/-- Check that serialize → deserialize roundtrips for a well-formed RawEnv. -/
+def serdeRoundtripOk (env : RawEnv) : Bool :=
+  match rsDeEnvFFI (rsSerEnvFFI env) with
+  | .ok decoded => serdeEnvEq decoded env
+  | .error _ => false
+
+/-- Property test: random well-formed RawEnv → serialize → deserialize → compare -/
+def serdePropertyTest : TestSeq :=
+  checkIO "serde RawEnv roundtrip" (∀ e : serdeRawEnv, serdeRoundtripOk e.env)
+
+/-! ## Test Suite -/
+
+public def suite : List TestSeq := [
+  keccakBasicTests,
+  keccakMultiUpdateTests,
+  keccakLargeInputTests,
+  sha256Tests,
+  serdeTests,
+  serdePropertyTest,
+]
+
+end Tests.FFI.Lifecycle
diff --git a/Tests/Ix/Ixon.lean b/Tests/Ix/Ixon.lean
index 9355efc7..ab547fc7 100644
--- a/Tests/Ix/Ixon.lean
+++ b/Tests/Ix/Ixon.lean
@@ -13,32 +13,32 @@ open Tests.FFI.Ixon (rsEqUnivSerialization rsEqExprSerialization rsEqConstantSer
 
 def univSerde (u : Univ) : Bool :=
   let bytes := serUniv u
-  match desUniv bytes with
+  match deUniv bytes with
   | .ok u' => u == u'
   | .error _ => false
 
 def exprSerde (e : Expr) : Bool :=
   let bytes := serExpr e
-  match desExpr bytes with
+  match deExpr bytes with
   | .ok e' => e == e'
   | .error _ => false
 
 def constantSerde (c : Constant) : Bool :=
   let bytes := serConstant c
-  match desConstant bytes with
+  match deConstant bytes with
   | .ok c' => c == c'
   | .error _ => false
 
 def commSerde (c : Comm) : Bool :=
   let bytes := serComm c
-  match desComm bytes with
+  match deComm bytes with
   | .ok c' => c == c'
   | .error _ => false
 
 def envSerde (raw : RawEnv) : Bool :=
   let env := raw.toEnv
   let bytes1 := serEnv env
-  match desEnv bytes1 with
+  match deEnv bytes1 with
   | .ok env' =>
     let bytes2 := serEnv env'
     bytes1 == bytes2  -- Byte-level equality after roundtrip
@@ -130,7 +130,7 @@ def sharingTest4 : Bool :=
   let e4 := Expr.lam (.sort 0) (.app (.var 0) (.var 0))
   let (rewritten4, _) := Ix.Sharing.applySharing #[e4]
   let serialized := serExpr rewritten4[0]!
-  match desExpr serialized with
+  match deExpr serialized with
   | .ok e => e == rewritten4[0]!
   | .error _ => false
 
@@ -144,7 +144,7 @@ def sharingUnits : TestSeq :=
 
 def envSerdeUnit (env : Env) : Bool :=
   let bytes1 := serEnv env
-  match desEnv bytes1 with
+  match deEnv bytes1 with
   | .ok env' =>
     let bytes2 := serEnv env'
     bytes1 == bytes2
diff --git a/Tests/Ix/RustSerialize.lean b/Tests/Ix/RustSerialize.lean
index 88c10d60..862b300f 100644
--- a/Tests/Ix/RustSerialize.lean
+++ b/Tests/Ix/RustSerialize.lean
@@ -17,7 +17,7 @@ open LSpec
 
 namespace Tests.RustSerialize
 
-/-- Test Rust serde roundtrip: compile → rsSerEnv → rsDesEnv → Lean serEnv → byte compare -/
+/-- Test Rust serde roundtrip: compile → rsSerEnv → rsDeEnv → Lean serEnv → byte compare -/
 def testRustSerdeRoundtrip : TestSeq :=
   .individualIO "Rust Serialize/Deserialize Roundtrip" none (do
     let leanEnv ← get_env!
@@ -52,9 +52,9 @@ def testRustSerdeRoundtrip : TestSeq :=
     IO.println ""
 
     -- Step 4: Deserialize Rust bytes with Rust
-    IO.println s!"[Step 4] Deserializing Rust bytes with Rust (rsDesEnv)..."
+    IO.println s!"[Step 4] Deserializing Rust bytes with Rust (rsDeEnv)..."
     let rustDesStart ← IO.monoMsNow
-    let roundtrippedFromRust ← match Ixon.rsDesEnv rustBytes with
+    let roundtrippedFromRust ← match Ixon.rsDeEnv rustBytes with
       | .ok env => pure env
       | .error e => do
         IO.println s!"[Step 4] FAILED: {e}"
diff --git a/Tests/Sha256.lean b/Tests/Sha256.lean
new file mode 100644
index 00000000..56b36dff
--- /dev/null
+++ b/Tests/Sha256.lean
@@ -0,0 +1,12 @@
+module
+
+public section
+
+namespace Sha256
+
+@[extern "rs_sha256"]
+opaque hash : @& ByteArray → ByteArray
+
+end Sha256
+
+end
diff --git a/lake-manifest.json b/lake-manifest.json
index 7af6c508..249967e0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,10 +25,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c",
+   "rev": "f89c732c481f87a47465041c6d7d659e1812848b",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c",
+   "inputRev": "f89c732c481f87a47465041c6d7d659e1812848b",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
diff --git a/lakefile.lean b/lakefile.lean
index 16d37449..abd0c773 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -15,7 +15,7 @@ require LSpec from git
   "https://github.com/argumentcomputer/LSpec" @ "928f27c7de8318455ba0be7461dbdf7096f4075a"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "f89c732c481f87a47465041c6d7d659e1812848b"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.28.0"
diff --git a/src/ffi/ixon/env.rs b/src/ffi/ixon/env.rs
index 143fb23c..5b312e8c 100644
--- a/src/ffi/ixon/env.rs
+++ b/src/ffi/ixon/env.rs
@@ -370,12 +370,12 @@ pub extern "C" fn rs_ser_env(obj: LeanIxonRawEnv) -> LeanByteArray {
 }
 
 // =============================================================================
-// rs_des_env: Deserialize bytes to an Ixon.RawEnv
+// rs_de_env: Deserialize bytes to an Ixon.RawEnv
 // =============================================================================
 
 /// FFI: Deserialize ByteArray -> Except String Ixon.RawEnv via Rust's Env.get. Pure.
 #[unsafe(no_mangle)]
-pub extern "C" fn rs_des_env(obj: LeanByteArray) -> LeanExcept {
+pub extern "C" fn rs_de_env(obj: LeanByteArray) -> LeanExcept {
   let data = obj.as_bytes();
   let mut slice: &[u8] = data;
   match IxonEnv::get(&mut slice) {
@@ -385,7 +385,7 @@ pub extern "C" fn rs_des_env(obj: LeanByteArray) -> LeanExcept {
       LeanExcept::ok(raw_env)
     },
     Err(e) => {
-      let msg = format!("rs_des_env: {}", e);
+      let msg = format!("rs_de_env: {}", e);
       LeanExcept::error_string(&msg)
     },
   }