Ixon: .ixe bundle format — main/assumptions header, metadata-last sections, blob integrity

Ix/Cli/CompileCmd.lean

@@ -109,8 +109,8 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   -- Persist the serialized IxonEnv (`Env::put` bytes) to disk so subsequent
   -- runs (e.g. `ix check-ixon`) can skip the Lean → IxOn compile step. The
   -- resulting file is the canonical streaming format produced by
-  -- `Ixon.Env::put` (see `src/ix/ixon/serialize.rs:1093-1297`); it round-trips
-  -- through `Ixon.Env::get`.
+  -- `Ixon.Env::put` (see `crates/ixon/src/serialize.rs` and the `.ixe`
+  -- layout spec in `docs/Ixon.md`); it round-trips through `Ixon.Env::get`.
   let writeStart ← IO.monoMsNow
   IO.FS.writeBinFile outPath bytes
   let writeMs := (← IO.monoMsNow) - writeStart

Tests/FFI/Lifecycle.lean

@@ -137,10 +137,11 @@ def serdeTests : TestSeq :=
   -- Empty RawEnv. Only data construction happens eagerly; FFI is deferred
   -- inside `mkSerdeRoundtripTest`.
   let empty : RawEnv := { consts := #[], named := #[], blobs := #[], comms := #[] }
-  -- RawEnv with data. The const's `addr` must be the canonical content
-  -- hash (`Address.blake3 (serConstant c)`) — the Rust loader verifies
-  -- `Address::hash(bytes) == addr` on load. Blobs and comms don't carry
-  -- a content-hash invariant, so `testAddr` is fine there.
+  -- RawEnv with data. Consts AND blobs must be content-addressed — the
+  -- Rust loader verifies `Address::hash(bytes) == addr` per entry for
+  -- both. `testAddr` is blake3 of `[1,2,3]`, which is exactly the blob's
+  -- bytes below, so the blob invariant holds; comms carry no
+  -- content-hash invariant, so `testAddr` is fine there too.
   let testAddr := Address.blake3 (ByteArray.mk #[1, 2, 3])
   let testExpr : Expr := .sort 0
   let testDef : Definition := {
@@ -220,13 +221,12 @@ private def genSerdeRawEnv : Gen RawEnv := 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
+  -- Blobs: content-addressed (the loaders verify blake3(bytes) == addr)
   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 }
+    blobs := blobs.push { addr := Address.blake3 bytes, bytes }
   -- Comms: pool addresses
   let numComms ← Gen.choose Nat 0 2
   let mut comms : Array RawComm := #[]

Tests/Gen/Ixon.lean

@@ -457,9 +457,12 @@ def genRawConst : Gen RawConst := do
 def genRawNamed : Gen RawNamed :=
   RawNamed.mk <$> genIxName 3 <*> genAddress <*> pure .empty
 
-/-- Generate a RawBlob -/
-def genRawBlob : Gen RawBlob :=
-  RawBlob.mk <$> genAddress <*> genByteArray
+/-- Generate a RawBlob whose `addr` is the canonical content hash of
+    `bytes`. Readers verify `Address.blake3 bytes == addr` per entry
+    (blob-tampering defense), so arbitrary addresses are rejected. -/
+def genRawBlob : Gen RawBlob := do
+  let bytes ← genByteArray
+  pure { addr := Address.blake3 bytes, bytes }
 
 /-- Generate a RawComm -/
 def genRawComm : Gen RawComm :=
@@ -469,13 +472,29 @@ def genRawComm : Gen RawComm :=
 def genRawNameEntry : Gen RawNameEntry :=
   RawNameEntry.mk <$> genAddress <*> genIxName 3
 
-/-- Generate a RawEnv with small arrays to avoid memory issues -/
-def genRawEnv : Gen RawEnv :=
-  RawEnv.mk <$> genSmallArray genRawConst
-    <*> genSmallArray genRawNamed
-    <*> genSmallArray genRawBlob
-    <*> genSmallArray genRawComm
-    <*> genSmallArray genRawNameEntry
+/-- Generate a RawEnv with small arrays to avoid memory issues. `main`
+    (when present) references a generated const — writers/readers check
+    `main ∈ consts`. Assumptions and hint keys are opaque addresses. -/
+def genRawEnv : Gen RawEnv := do
+  let consts ← genSmallArray genRawConst
+  let named ← genSmallArray genRawNamed
+  let blobs ← genSmallArray genRawBlob
+  let comms ← genSmallArray genRawComm
+  let names ← genSmallArray genRawNameEntry
+  let main ←
+    if consts.size > 0 then
+      frequency [
+        (1, pure none),
+        (1, do
+          let i ← Gen.choose Nat 0 (consts.size - 1)
+          pure (consts[i % consts.size]?.map (·.addr))),
+      ]
+    else pure none
+  let assumptionList ← genList genAddress
+  let assumptions := assumptionList.toArray.qsort fun a b => (compare a b).isLT
+  let hintList ← genList (Prod.mk <$> genAddress <*> genReducibilityHints)
+  let anonHints := hintList.toArray.qsort fun a b => (compare a.1 b.1).isLT
+  pure { consts, named, blobs, comms, names, main, assumptions, anonHints }
 
 instance : Shrinkable RawConst where
   shrink rc := (fun c => { rc with const := c }) <$> Shrinkable.shrink rc.const
@@ -486,18 +505,36 @@ instance : Shrinkable RawNamed where
     | _ => [{ rn with constMeta := .empty }]
 
 instance : Shrinkable RawBlob where
-  shrink rb := if rb.bytes.size > 0 then [{ rb with bytes := ByteArray.empty }] else []
+  shrink rb :=
+    -- Keep the content-address invariant: shrunk bytes need the
+    -- matching hash or the loaders reject the shrunk case.
+    if rb.bytes.size > 0 then
+      [{ addr := Address.blake3 ByteArray.empty, bytes := ByteArray.empty }]
+    else []
 
 instance : Shrinkable RawComm where
   shrink _ := []
 
 instance : Shrinkable RawEnv where
   shrink env :=
-    (if env.consts.size > 0 then [{ env with consts := env.consts.pop }] else []) ++
+    -- Popping a const may orphan `main` (writers reject main ∉ consts),
+    -- so clear it when its target is dropped.
+    (if env.consts.size > 0 then
+      let popped := env.consts.pop
+      let main := match env.main with
+        | some m => if popped.any (·.addr == m) then env.main else none
+        | none => none
+      [{ env with consts := popped, main }]
+     else []) ++
     (if env.named.size > 0 then [{ env with named := env.named.pop }] else []) ++
     (if env.blobs.size > 0 then [{ env with blobs := env.blobs.pop }] else []) ++
     (if env.comms.size > 0 then [{ env with comms := env.comms.pop }] else []) ++
-    (if env.names.size > 0 then [{ env with names := env.names.pop }] else [])
+    (if env.names.size > 0 then [{ env with names := env.names.pop }] else []) ++
+    (if env.assumptions.size > 0 then [{ env with assumptions := env.assumptions.pop }] else []) ++
+    (if env.anonHints.size > 0 then [{ env with anonHints := env.anonHints.pop }] else []) ++
+    (match env.main with
+      | some _ => [{ env with main := none }]
+      | none => [])
 
 instance : SampleableExt RawConst := SampleableExt.mkSelfContained genRawConst
 instance : SampleableExt RawNamed := SampleableExt.mkSelfContained genRawNamed

Tests/Ix/Compile.lean

@@ -337,8 +337,8 @@ def testCrossImpl : TestSeq :=
         IO.println s!"[Step 4]   Lean blob stats: total={fmtBytes leanTotalBlobData}, max={fmtBytes leanMaxBlob}, avg={fmtBytes leanAvgBlob}, big(>1kB)={leanBig}, huge(>100kB)={leanHuge}"
         IO.println s!"[Step 4]   Lean top 10 blob sizes: {leanTopSizes.map fmtBytes}"
 
-        let (leanBlobs, leanConsts, leanNames, leanNamed, leanComms) := Ixon.envSectionSizes leanIxonEnv
-        IO.println s!"[Step 4]   Lean sections: blobs={fmtBytes leanBlobs}, consts={fmtBytes leanConsts}, names={fmtBytes leanNames}, named={fmtBytes leanNamed}, comms={fmtBytes leanComms}"
+        let (leanBlobs, leanConsts, leanHints, leanNames, leanNamed, leanComms) := Ixon.envSectionSizes leanIxonEnv
+        IO.println s!"[Step 4]   Lean sections: blobs={fmtBytes leanBlobs}, consts={fmtBytes leanConsts}, hints={fmtBytes leanHints}, names={fmtBytes leanNames}, named={fmtBytes leanNamed}, comms={fmtBytes leanComms}"
         let leanEnvBytes := serializeEnv leanIxonEnv
         IO.println s!"[Step 4]   Lean env done: {fmtBytes leanEnvBytes.size}"
 
@@ -358,8 +358,8 @@ def testCrossImpl : TestSeq :=
         IO.println s!"[Step 4]   Rust blob stats: total={fmtBytes rustTotalBlobData}, max={fmtBytes rustMaxBlob}, avg={fmtBytes rustAvgBlob}, big(>1kB)={rustBig}, huge(>100kB)={rustHuge}"
         IO.println s!"[Step 4]   Rust top 10 blob sizes: {rustTopSizes.map fmtBytes}"
 
-        let (rustBlobs, rustConsts, rustNames, rustNamed, rustComms) := Ixon.envSectionSizes phases.compileEnv
-        IO.println s!"[Step 4]   Rust sections: blobs={fmtBytes rustBlobs}, consts={fmtBytes rustConsts}, names={fmtBytes rustNames}, named={fmtBytes rustNamed}, comms={fmtBytes rustComms}"
+        let (rustBlobs, rustConsts, rustHints, rustNames, rustNamed, rustComms) := Ixon.envSectionSizes phases.compileEnv
+        IO.println s!"[Step 4]   Rust sections: blobs={fmtBytes rustBlobs}, consts={fmtBytes rustConsts}, hints={fmtBytes rustHints}, names={fmtBytes rustNames}, named={fmtBytes rustNamed}, comms={fmtBytes rustComms}"
         let rustEnvBytes := serializeEnv phases.compileEnv
         IO.println s!"[Step 4]   Rust env done: {fmtBytes rustEnvBytes.size}"
         let serTime := (← IO.monoMsNow) - serStart

Tests/Ix/Ixon.lean

@@ -153,9 +153,11 @@ def envSerdeUnit (env : Env) : Bool :=
 def envUnitTests : TestSeq :=
   -- Test 1: Empty env
   let emptyEnv : Env := {}
-  -- Test 2: Env with only a blob
-  let blobAddr := Address.blake3 (ByteArray.mk #[1, 2, 3])
-  let envWithBlob : Env := { blobs := ({} : Std.HashMap _ _).insert blobAddr (ByteArray.mk #[4, 5, 6]) }
+  -- Test 2: Env with only a blob. Blob addresses must be the content
+  -- hash of the bytes — readers verify per entry.
+  let blobBytes := ByteArray.mk #[4, 5, 6]
+  let blobAddr := Address.blake3 blobBytes
+  let envWithBlob : Env := { blobs := ({} : Std.HashMap _ _).insert blobAddr blobBytes }
   -- Test 3: Env with a simple name (no named entry)
   let testName := Ix.Name.mkStr Ix.Name.mkAnon "test"
   let testNameAddr := testName.getHash
@@ -179,15 +181,34 @@ def envUnitTests : TestSeq :=
   let payloadAddr := Address.blake3 (ByteArray.mk #[13, 14, 15])
   let commAddr := Address.blake3 (ByteArray.mk #[16, 17, 18])
   let envWithBlobAndComm : Env := {
-    blobs := ({} : Std.HashMap _ _).insert blobAddr (ByteArray.mk #[4, 5, 6]),
+    blobs := ({} : Std.HashMap _ _).insert blobAddr blobBytes,
     comms := ({} : Std.HashMap _ _).insert commAddr (Comm.mk secretAddr payloadAddr)
   }
+  -- Test 7: Bundle env — main + assumptions + anonHints exercise the
+  -- bundle header and §3.
+  let bundleDef : Definition := {
+    kind := .defn, safety := .safe, lvls := 0, typ := .sort 0, value := .sort 0
+  }
+  let bundleConst : Constant := {
+    info := .defn bundleDef, sharing := #[], refs := #[], univs := #[]
+  }
+  let bundleConstAddr := Address.blake3 (serConstant bundleConst)
+  let bundleEnv : Env := Id.run do
+    let mut env : Env := {}
+    env := env.storeConst bundleConstAddr bundleConst
+    return { env with
+      main := some bundleConstAddr
+      assumptions := ({} : Std.HashSet Address)
+        |>.insert (Address.blake3 (ByteArray.mk #[42]))
+        |>.insert (Address.blake3 (ByteArray.mk #[43]))
+      anonHints := ({} : Std.HashMap _ _).insert bundleConstAddr (.regular 5) }
   test "Empty env roundtrip" (envSerdeUnit emptyEnv) ++
   test "Env with blob roundtrip" (envSerdeUnit envWithBlob) ++
   test "Env with name roundtrip" (envSerdeUnit envWithName) ++
   test "Env with named (empty meta) roundtrip" (envSerdeUnit envWithNamed) ++
   test "Env with nested name roundtrip" (envSerdeUnit envWithNestedName) ++
-  test "Env with blob+comm roundtrip" (envSerdeUnit envWithBlobAndComm)
+  test "Env with blob+comm roundtrip" (envSerdeUnit envWithBlobAndComm) ++
+  test "Bundle env (main/assumptions/hints) roundtrip" (envSerdeUnit bundleEnv)
 
 /-! ## Cross-implementation serialization comparison tests -/
 
@@ -204,15 +225,22 @@ def envSerializationMatches (raw : RawEnv) : Bool :=
   let env := raw.toEnv
   rsEqEnvSerialization raw (serEnv env)
 
+/-- Strict byte equality between the pure-Lean writer and the Rust
+    writer over the same RawEnv (a stronger check than
+    `rsEqEnvSerialization`'s content comparison). -/
+def envBytesMatchRust (raw : RawEnv) : Bool :=
+  serEnv raw.toEnv == rsSerEnvFFI raw
+
 /-- Unit tests for Lean==Rust serialization comparison -/
 def envSerializationUnitTests : TestSeq :=
   -- Test 1: Empty env
   let emptyRaw : RawEnv := { consts := #[], named := #[], blobs := #[], comms := #[] }
-  -- Test 2: Env with one blob
-  let blobAddr := Address.blake3 (ByteArray.mk #[1, 2, 3])
+  -- Test 2: Env with one blob (content-addressed: readers verify).
+  let blobBytes := ByteArray.mk #[4, 5, 6]
+  let blobAddr := Address.blake3 blobBytes
   let blobRaw : RawEnv := {
     consts := #[], named := #[],
-    blobs := #[{ addr := blobAddr, bytes := ByteArray.mk #[4, 5, 6] }],
+    blobs := #[{ addr := blobAddr, bytes := blobBytes }],
     comms := #[]
   }
   -- Test 3: Env with one comm
@@ -227,13 +255,35 @@ def envSerializationUnitTests : TestSeq :=
   -- Test 4: Env with blob + comm
   let blobCommRaw : RawEnv := {
     consts := #[], named := #[],
-    blobs := #[{ addr := blobAddr, bytes := ByteArray.mk #[4, 5, 6] }],
+    blobs := #[{ addr := blobAddr, bytes := blobBytes }],
     comms := #[{ addr := commAddr, comm := Comm.mk secretAddr payloadAddr }]
   }
+  -- Test 5: Bundle env — the directed cross-language vector for the
+  -- bundle header (main/assumptions) and §3 anon_hints.
+  let bundleDef : Definition := {
+    kind := .defn, safety := .safe, lvls := 0, typ := .sort 0, value := .sort 0
+  }
+  let bundleConst : Constant := {
+    info := .defn bundleDef, sharing := #[], refs := #[], univs := #[]
+  }
+  let bundleConstAddr := Address.blake3 (serConstant bundleConst)
+  let bundleRaw : RawEnv := {
+    consts := #[{ addr := bundleConstAddr, const := bundleConst }],
+    named := #[], blobs := #[], comms := #[],
+    main := some bundleConstAddr,
+    assumptions := #[
+      Address.blake3 (ByteArray.mk #[42]),
+      Address.blake3 (ByteArray.mk #[43])],
+    anonHints := #[(bundleConstAddr, .regular 5)]
+  }
   test "Empty env Lean==Rust" (envSerializationMatches emptyRaw) ++
   test "Blob env Lean==Rust" (envSerializationMatches blobRaw) ++
   test "Comm env Lean==Rust" (envSerializationMatches commRaw) ++
-  test "Blob+Comm env Lean==Rust" (envSerializationMatches blobCommRaw)
+  test "Blob+Comm env Lean==Rust" (envSerializationMatches blobCommRaw) ++
+  test "Bundle env Lean==Rust" (envSerializationMatches bundleRaw) ++
+  test "Empty env bytes Lean==Rust" (envBytesMatchRust emptyRaw) ++
+  test "Blob env bytes Lean==Rust" (envBytesMatchRust blobRaw) ++
+  test "Bundle env bytes Lean==Rust" (envBytesMatchRust bundleRaw)
 
 /-! ## Canonical env merkle root: Lean vs. Rust agreement -/
 

crates/ffi/src/compile.rs

@@ -485,6 +485,10 @@ pub extern "C" fn rs_compile_phases(
     raw_ixon_env.set_obj(2, blobs_arr);
     raw_ixon_env.set_obj(3, comms_arr);
     raw_ixon_env.set_obj(4, names_arr);
+    crate::lean_ixon::env::set_raw_env_bundle_fields(
+      &raw_ixon_env,
+      &compile_stt.env,
+    );
 
     let result = LeanIxCompilePhases::alloc(0);
     result.set_obj(0, raw_env);
@@ -581,6 +585,7 @@ pub extern "C" fn rs_compile_env_to_ixon(
     result.set_obj(2, blobs_arr);
     result.set_obj(3, comms_arr);
     result.set_obj(4, names_arr);
+    crate::lean_ixon::env::set_raw_env_bundle_fields(&result, &compile_stt.env);
     LeanIOResult::ok(result)
   }
 }

crates/ffi/src/lean.rs

@@ -52,13 +52,15 @@ lean_ffi::lean_inductive! {
   LeanIxonRawBlob         [ { num_obj: 2 } ];
   LeanIxonRawComm         [ { num_obj: 2 } ];
   LeanIxonRawNameEntry    [ { num_obj: 2 } ];
-  LeanIxonRawEnv          [ { num_obj: 5 } ];
+  // consts, named, blobs, comms, names, main, assumptions, anonHints
+  LeanIxonRawEnv          [ { num_obj: 8 } ];
 
   // Lazy/anon deserialization (`rs_de_env_lazy`): zero-copy const windows
-  // (addr + offset + len), name->addr + hint, and copied blobs.
+  // (addr + offset + len), name->addr + hint, copied blobs, and the
+  // bundle header fields (main, assumptions).
   LeanIxonRawConstSlice   [ { num_obj: 1, num_64: 2 } ];
   LeanIxonRawNamedLite    [ { num_obj: 2, num_64: 2 } ];
-  LeanIxonRawEnvLazy      [ { num_obj: 3 } ];
+  LeanIxonRawEnvLazy      [ { num_obj: 5 } ];
 
   // --- Ixon multi-variant inductives ---