chore: Update multi stark

.github/actions/log-cpu/action.yml

@@ -30,6 +30,34 @@ inputs:
 runs:
   using: composite
   steps:
+    # A PR benchmark runs trusted workflow YAML from the default branch but
+    # loads this action from the PR checkout. Bridge that one-revision gap: the
+    # default-branch workflow invokes this label immediately before rebuilding
+    # a fresh base. Once bench-pr.yml's explicit setup step lands, the toolchain
+    # is already installed and this exits immediately.
+    - name: Bootstrap base Rust toolchain for trusted PR workflow
+      if: inputs.label == 'Base benchmark binary build CPU'
+      shell: bash
+      run: |
+        set -euo pipefail
+
+        toolchain_file=base/rust-toolchain.toml
+        [ -f "$toolchain_file" ] || { echo "::error::$toolchain_file is missing"; exit 1; }
+        channel=$(awk -F '"' '/^[[:space:]]*channel[[:space:]]*=/ { print $2; exit }' "$toolchain_file")
+        profile=$(awk -F '"' '/^[[:space:]]*profile[[:space:]]*=/ { print $2; exit }' "$toolchain_file")
+        if [[ ! "$channel" =~ ^[A-Za-z0-9._+-]+$ ]]; then
+          echo "::error::$toolchain_file has an invalid Rust channel"
+          exit 1
+        fi
+        case "${profile:-default}" in
+          minimal|default|complete) ;;
+          *) echo "::error::$toolchain_file has an invalid Rust profile"; exit 1 ;;
+        esac
+
+        rustup run "$channel" rustc --version >/dev/null 2>&1 && exit 0
+        echo "Installing Rust $channel (${profile:-default} profile) for the fresh base build"
+        rustup toolchain install "$channel" --profile "${profile:-default}" --no-self-update
+
     - shell: bash
       env:
         CPU_LABEL: ${{ inputs.label }}

.github/actions/setup-rust-toolchain/action.yml

@@ -4,6 +4,9 @@ description: >-
   artifacts.
 
 inputs:
+  toolchain:
+    description: Rust toolchain to install; defaults to the repository toolchain file
+    required: false
   cache-workspaces:
     description: Cargo workspaces to cache
     required: false
@@ -29,6 +32,7 @@ runs:
 
     - uses: actions-rust-lang/setup-rust-toolchain@v1
       with:
+        toolchain: ${{ inputs.toolchain }}
         rustflags: ${{ inputs.native-codegen == 'true' && '-Ctarget-cpu=native -Dwarnings' || '-Dwarnings' }}
         # `target/` may contain host-executed native code. Every caller runs
         # within the Warp x64 compatibility domain.

.github/workflows/bench-pr.yml

@@ -733,6 +733,25 @@ jobs:
           echo "cached=$cached" >> "$GITHUB_OUTPUT"
           echo "base .ixe: $([ "$ixe" = true ] && echo restored from cache || echo compiling in the base run)"
           echo "base binaries: $([ "$cached" = true ] && echo restored from cache || echo building from source)"
+      # A fresh comparison deliberately bypasses the base binary cache. Install
+      # the Rust version declared by that checkout before Lake invokes Cargo;
+      # provisioning the PR's Lean toolchain above does not install base Rust.
+      - name: Resolve base Rust toolchain
+        if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true'
+        id: base-rust
+        run: |
+          channel="$(awk -F '"' '/^[[:space:]]*channel[[:space:]]*=/ { print $2; exit }' base/rust-toolchain.toml)"
+          if [ -z "$channel" ]; then
+            echo "::error::base/rust-toolchain.toml does not declare a channel"
+            exit 1
+          fi
+          echo "channel=$channel" >> "$GITHUB_OUTPUT"
+      - name: Set up base Rust toolchain
+        if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached != 'true'
+        uses: ./.github/actions/setup-rust-toolchain
+        with:
+          toolchain: ${{ steps.base-rust.outputs.channel }}
+          cache-workspaces: base
       - name: Log cached base binary build CPU
         if: steps.decide.outputs.run-base == 'true' && steps.base-src.outputs.cached == 'true'
         uses: ./.github/actions/log-cpu

Benchmarks/Compile/lake-manifest.json

@@ -182,10 +182,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

@@ -102,19 +102,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

@@ -592,10 +592,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 =>
@@ -621,7 +629,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
             (← IO.getStdout).flush
             TracingTexray.resetPeakTreeRss
             let (rvProveRes, rvProveSec) ← timed fun _ =>
-              vSystem.proveMultiStark vIdx pubInput proofBytes vkBytes
+              vSystem.proveMultiStark vIdx pubInput adviceBytes vkBytes
                 claimBytes useInterp
             let (rvClaim, rvProof) ← match rvProveRes with
               | .ok result => pure result