lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
samuelburnham wants to merge 5 commits into
base:main
Choose a base branch
from
Draft

lakefile: drop Blake3 from the native-decide dynlib #607

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f0909c7
Update Aiur to Plonky3 0.6
arthurpaulino Sep 1, 2026
eab18e4
Provision Rust for fresh benchmark base builds
arthurpaulino Sep 1, 2026
840932a
Verify native Plonky3 multiproofs recursively
arthurpaulino Sep 1, 2026
feb014d
Pin benchmark codegen to the CI fleet's common ISA
samuelburnham Sep 1, 2026
a2d2fa5
lakefile: drop Blake3 from the native-decide dynlib
samuelburnham Sep 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
26 changes: 26 additions & 0 deletions .github/actions/log-cpu/action.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down
33 changes: 28 additions & 5 deletions .github/actions/setup-rust-toolchain/action.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
exit 1
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 }}
4 changes: 2 additions & 2 deletions .github/workflows/merge-tests.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down
4 changes: 2 additions & 2 deletions Benchmarks/Compile/lake-manifest.json
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down
14 changes: 8 additions & 6 deletions Benchmarks/RecursionDebug.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down
11 changes: 9 additions & 2 deletions Benchmarks/Typecheck.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
lakefile: drop Blake3 from the native-decide dynlib#607

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Draft

samuelburnham
wants to merge
5
commits into

base:main
Choose a base branch

from

 Draft


lakefile: drop Blake3 from the native-decide dynlib
#607
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


5 commits


Select commit
Hold shift + click to select a range
f0909c7

Update Aiur to Plonky3 0.6


arthurpaulino Sep 1, 2026
eab18e4

Provision Rust for fresh benchmark base builds


arthurpaulino Sep 1, 2026
840932a

Verify native Plonky3 multiproofs recursively


arthurpaulino Sep 1, 2026
feb014d

Pin benchmark codegen to the CI fleet's common ISA


samuelburnham Sep 1, 2026
a2d2fa5

lakefile: drop Blake3 from the native-decide dynlib


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


26 changes: 26 additions & 0 deletions
.github/actions/log-cpu/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 }}
Expand Down

33 changes: 28 additions & 5 deletions
.github/actions/setup-rust-toolchain/action.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"

Expand All@@ -27,10 +27,33 @@ runs:
 exit 1
 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 }}

4 changes: 2 additions & 2 deletions
.github/workflows/merge-tests.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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.
Expand Down

4 changes: 2 additions & 2 deletions
Benchmarks/Compile/lake-manifest.json

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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",
Expand Down

14 changes: 8 additions & 6 deletions
Benchmarks/RecursionDebug.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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"
Expand Down

11 changes: 9 additions & 2 deletions
Benchmarks/Typecheck.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -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 =>
Expand All@@ -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
Expand Down
Loading