chore: Update multi stark

Benchmarks/Compile/lake-manifest.json

@@ -132,10 +132,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "db25a8a21579d8211eec4347402721f5674bf2c1",
+   "rev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "db25a8a21579d8211eec4347402721f5674bf2c1",
+   "inputRev": "e6e908bfd3af607ab44fb462fa2276a2c81addba",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",

Benchmarks/RecursionDebug.lean

@@ -101,19 +101,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool)
       match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with
       | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none
       | .ok (claimBytes, proof, _) =>
-        -- `verify_claim`'s public input is the 32-G blake3 digest of the
-        -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck).
+        -- `verify_claim`'s public input is the packed blake3 digest of the
+        -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck:
+        -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`).
         let digest := Address.blake3 claimBytes
-        pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof)
+        pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof)
   let t1 ← IO.monoNanosNow
-  let proofBytes := proof.toBytes
-  IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes"
+  IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes"
   -- Sanity: the inner proof must verify out-of-circuit before we chase the
   -- recursive verifier.
   match aiurSystem.verify claim proof with
   | .ok () => IO.println "inner proof verifies out-of-circuit: ok"
   | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}"
-  return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim])
+  -- The in-circuit verifier consumes the per-query advice transport, not
+  -- the pruned-multiproof wire format.
+  match aiurSystem.proofToAdviceBytes claim proof with
+  | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none
+  | .ok adviceBytes =>
+    return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim])
 
 def main (args : List String) : IO UInt32 := do
   let ixePath := (argStr args "--ixe").getD "init.ixe"

Benchmarks/Typecheck.lean

@@ -595,10 +595,18 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
           let claimBytes := MultiStark.serializeClaims #[claim]
           let vkBytes := aiurSystem.vkBytes
           let pubInput := MultiStark.verifierPubInput vkBytes claimBytes
+          -- The in-circuit verifier consumes the per-query advice transport;
+          -- `proofBytes` (the pruned-multiproof wire format) stays the
+          -- reported proof size but is not parseable in-circuit.
+          let adviceBytes ← match aiurSystem.proofToAdviceBytes claim proof with
+            | .ok bytes => pure bytes
+            | .error e =>
+              IO.eprintln s!"  ❌ advice re-encoding for {r.name} FAILED: {e}"
+              continue
           -- Native path: the advice buffer is built in Rust from the raw
           -- byte blobs and execution routes through the codegen'd verifier.
           let (rvRes, rvSec) ← timed fun _ =>
-            vCompiled.bytecode.executeMultiStark vIdx pubInput proofBytes
+            vCompiled.bytecode.executeMultiStark vIdx pubInput adviceBytes
               vkBytes claimBytes useInterp
           match rvRes with
           | .error e =>
@@ -624,7 +632,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
             (← IO.getStdout).flush
             TracingTexray.resetPeakTreeRss
             let ((rvClaim, rvProof), rvProveSec) ← timed fun _ =>
-              vSystem.proveMultiStark vIdx pubInput proofBytes vkBytes
+              vSystem.proveMultiStark vIdx pubInput adviceBytes vkBytes
                 claimBytes useInterp
             let rvPeak ← TracingTexray.peakTreeRssBytes
             let rvProofBytes := Aiur.Proof.toBytes rvProof