Update Aiur to Plonky3 0.6

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

@@ -30,6 +30,32 @@ inputs:
 runs:
   using: composite
   steps:
+    # PR benchmarks execute trusted workflow YAML from the default branch but
+    # load this action from the PR checkout. Ensure a freshly checked-out base
+    # has its pinned Rust toolchain before Lake invokes Cargo.
+    - name: Bootstrap base Rust toolchain
+      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

@@ -7,8 +7,8 @@ inputs:
   cache-workspaces:
     description: Cargo workspaces to cache
     required: false
-  native-codegen:
-    description: Enable code generation for the runner's native CPU
+  avx512-codegen:
+    description: Enable AVX-512 code generation for the Warp x64 fleet's common ISA
     required: false
     default: "true"
 
@@ -40,10 +40,33 @@ runs:
           echo "CARGO_NET_GIT_FETCH_WITH_CLI=true" >> "$GITHUB_ENV"
         fi
 
+    # The fleet mixes Intel Granite Rapids and AMD Zen 5, and a binary may be
+    # built on one and measured on another. Neither vendor's feature set
+    # contains the other's, so `-Ctarget-cpu=native` is not portable across
+    # the fleet: Zen 5 enables SSE4A, which LLVM emits (as INSERTQ, in
+    # witness generation) and Intel traps on with #UD. Pin the measured
+    # intersection instead. x86-64-v4 covers every AVX-512 subset Plonky3
+    # uses; +avx512vbmi2 keeps its VPSHRDQ interleave and +gfni keeps LLVM's
+    # byte-shift lowering. blake3 selects its kernels via CPUID at runtime
+    # and is unaffected. Pinning also makes codegen host-independent, so the
+    # cache key below is sound and main-vs-PR timings stay comparable.
+    - name: Require the fleet's baseline CPU features
+      if: inputs.avx512-codegen == 'true'
+      shell: bash
+      run: |
+        missing=()
+        for f in avx512f avx512bw avx512cd avx512dq avx512vl avx512_vbmi2 gfni; do
+          grep -qw "$f" /proc/cpuinfo || missing+=("$f")
+        done
+        if [ ${#missing[@]} -gt 0 ]; then
+          echo "::error::Runner CPU lacks required feature(s): ${missing[*]}. Benchmark binaries are built for x86-64-v4 +avx512vbmi2,+gfni."
+          exit 1
+        fi
+
     - uses: actions-rust-lang/setup-rust-toolchain@v1
       with:
-        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.
+        rustflags: ${{ inputs.avx512-codegen == 'true' && '-Ctarget-cpu=x86-64-v4 -Ctarget-feature=+avx512vbmi2,+gfni -Dwarnings' || '-Dwarnings' }}
+        # Codegen is pinned above, so `target/` artifacts are interchangeable
+        # across every Warp x64 host.
         cache-key: warp-x64
         cache-workspaces: ${{ inputs.cache-workspaces }}

.github/workflows/merge-tests.yml

@@ -68,8 +68,8 @@ jobs:
       - uses: actions/checkout@v7
       - uses: ./.github/actions/setup-rust-toolchain
         with:
-          # Valgrind cannot decode AVX-512 emitted by native codegen.
-          native-codegen: ${{ matrix.kind != 'valgrind' }}
+          # Valgrind cannot decode the AVX-512 the fleet baseline emits.
+          avx512-codegen: ${{ matrix.kind != 'valgrind' }}
 
       # A merge group has its own SHA, so restore the nearest compatible build
       # produced by ordinary CI and let Lake rebuild anything that changed.

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,21 @@ 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` takes the packed Blake3 digest used by the
+        -- production typecheck path: eight field elements of four bytes.
         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])
+  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,17 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
           let claimBytes := MultiStark.serializeClaims #[claim]
           let vkBytes := aiurSystem.vkBytes
           let pubInput := MultiStark.verifierPubInput vkBytes claimBytes
+          -- Native proof bytes use P3's pruned multiproof format. The
+          -- in-circuit verifier consumes equivalent per-query path advice.
+          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 +628,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