Aggregate-first recursion: lift shard proofs, fold `CheckEnv` claims, and verify one root#598

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.

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

Open

johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first

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

-Original file line number
+Diff 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 @@

Benchmarks/AggregatePolicy.lean

Large diffs are not rendered by default.

Benchmarks/Compile/lake-manifest.json

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

Benchmarks/RecursionDebug.lean

-Original file line number
+Diff line change
@@ Expand Up @@
  match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with
  | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none
  | .ok (claimBytes, proof, _) =>
- -- `verify_claim`'s public input is the 32-G blake3 digest of the
- -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck).
+ -- `verify_claim`'s public input is the packed blake3 digest of the
+ -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck:
+ -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`).
  let digest := Address.blake3 claimBytes
- pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof)
+ pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof)
  let t1 ← IO.monoNanosNow
- let proofBytes := proof.toBytes
- IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes"
+ IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes"
  -- Sanity: the inner proof must verify out-of-circuit before we chase the
  -- recursive verifier.
  match aiurSystem.verify claim proof with
  | .ok () => IO.println "inner proof verifies out-of-circuit: ok"
  | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}"
- return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim])
+ -- The in-circuit verifier consumes the per-query advice transport, not
+ -- the pruned-multiproof wire format.
+ match aiurSystem.proofToAdviceBytes claim proof with
+ | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none
+ | .ok adviceBytes =>
+ return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim])
 def main (args : List String) : IO UInt32 := do
  let ixePath := (argStr args "--ixe").getD "init.ixe"
@@ Expand All / @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do @@
  let mode := (argStr args "--mode").getD "native"
  let skipDeps := args.contains "--skip-deps"
  let fri := friParams (argNat args "--queries" 100)
+ if fri.numQueries == 0 then
+ IO.eprintln "error: --queries must be positive"
+ return 1
  let depth := argNat args "--depth" 2
  let stackLimit := argNat args "--stack" 40
  IO.FS.createDirAll dir
@@ Expand Down @@

Benchmarks/Typecheck.lean

Large diffs are not rendered by default.

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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time. , '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 contentNavigation Menu Sign inAppearance settings AI CODE CREATIONGitHub CopilotWrite better code with AI GitHub Copilot appDirect agents from issue to merge MCP RegistryIntegrate external tools DEVELOPER WORKFLOWSActionsAutomate any workflow CodespacesInstant dev environments IssuesPlan and track work Code ReviewManage code changes Code QualityEnforce quality at merge APPLICATION SECURITYGitHub Advanced SecurityFind and fix vulnerabilities Code securitySecure your code as you build Secret protectionStop leaks before they start EXPLOREWhy GitHub Documentation Blog Changelog Marketplace View all features BY COMPANY SIZEEnterprises Small and medium teams Startups Nonprofits BY USE CASEApp Modernization DevSecOps DevOps CI/CD View all use cases BY INDUSTRYHealthcare Financial services Manufacturing Government View all industries View all solutions EXPLORE BY TOPICAI Software Development DevOps Security View all topics EXPLORE BY TYPECustomer stories Events & webinars Ebooks & reports Business insights GitHub Skills SUPPORT & SERVICESDocumentation Customer support Community forum Trust center Partners View all resources COMMUNITYGitHub SponsorsFund open source developers PROGRAMSSecurity Lab Maintainer Community GitHub Stars Archive Program REPOSITORIESTopics Trending Collections ENTERPRISE SOLUTIONSEnterprise platformAI-powered developer platform AVAILABLE ADD-ONSGitHub Advanced SecurityEnterprise-grade security features Copilot for BusinessEnterprise-grade AI features Premium SupportEnterprise-grade 24/7 support Pricing Sign in Sign upAppearance settings You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert Uh oh! There was an error while loading. Please reload this page. argumentcomputer /ixPublic Notifications You must be signed in to change notification settings Fork 3 Star 91 Code Issues10 Pull requests17 Actions Projects Security and quality0 Insights Additional navigation options Code Issues Pull requests Actions Projects Security and quality Insights Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root#598 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 Open johnchandlerburnham wants to merge 40 commits into main from jcb/aggregate-first Conversation 1 Commits 40 Checks 0 Files changed Uh oh! There was an error while loading. Please reload this page. Open Aggregate-first recursion: lift shard proofs, fold CheckEnv claims, and verify one root #598 Show file tree Hide file tree Changes from all commits Commits Show all changes 40 commits Select commit Hold shift + click to select a range 70d73e6 feat: implement aggregate-first lift/join pipeline johnchandlerburnham Aug 27, 2026c83f6d9 feat: add structural aggregate joins johnchandlerburnham Aug 28, 20266ea4bba feat: support single-shard aggregate roots johnchandlerburnham Aug 28, 2026ccf17ce feat: audit aggregate recursion activation and parameters johnchandlerburnham Aug 28, 202666fb376 aiur: virtual-gas meter + QueryRecordHandle for per-constant cost pro… arthurpaulino Aug 24, 20261639996 aiur: batch weights; budget-gated proves that split in place samuelburnham Aug 28, 2026f529e09 aiur: model-driven splitting, exec-only audits, corrected-manifest emit samuelburnham Aug 27, 20267de7a7b aiur: quality pass, --ram-budget semantics, settled seed sizing samuelburnham Aug 28, 20265646af6 feat: add verified aggregate proof cache johnchandlerburnham Aug 28, 202620f5e62 bench: aiur-sharded-env exercises the split audit samuelburnham Aug 28, 2026614cf55 perf(aggregate): avoid repeated shard closure walks samuelburnham Aug 28, 2026a3372b6 feat: parallelize aggregate proof scheduling johnchandlerburnham Aug 28, 2026f43447c aiur: scale static shard seeds by block profile samuelburnham Aug 28, 202680854d1 bench(aggregate): add tiny Init pair end-to-end benchmark samuelburnham Aug 28, 2026319df80 fmt, clippy samuelburnham Aug 28, 20266c20e1c bench: measure aggregate flat joins johnchandlerburnham Aug 28, 20265665aa3 Bump Rust toolchain to 1.98 samuelburnham Aug 22, 2026b017104 Bump multi-stark: width-binding policy, height bound, P3 v0.6.0 samuelburnham Aug 22, 2026093365d Bump Blake3.lean and lean-ffi for Rust 1.98 samuelburnham Aug 24, 2026428d6ac bench: feed the recursive phase advice bytes, fix RecursionDebug's claim samuelburnham Aug 24, 20264a265c7 aggregate: adapt recursion pipeline to pruned FRI proofs johnchandlerburnham Aug 29, 202633c618d feat: ixAggr heterogeneous recursive aggregation toplevel arthurpaulino Aug 29, 202691d1dd1 aggregate: converge production pipeline on ixAggr johnchandlerburnham Aug 29, 2026b70042d bench: add converged aggregate policy handoff johnchandlerburnham Aug 29, 2026eec6064 merge: main into aggregate-first johnchandlerburnham Aug 30, 2026f0909c7 Update Aiur to Plonky3 0.6 arthurpaulino Sep 1, 2026eab18e4 Provision Rust for fresh benchmark base builds arthurpaulino Sep 1, 2026840932a Verify native Plonky3 multiproofs recursively arthurpaulino Sep 1, 202682dcc9d Merge branch 'ap/bump-p3' into jcb/aggregate-first johnchandlerburnham Sep 1, 2026bbee830 Fix multi-stark PR77 merge resolution johnchandlerburnham Sep 1, 20265d1c637 Add a pinned CUDA 13.2 development shell johnchandlerburnham Sep 1, 2026ec7e2dc merge: prove-time RAM gate, split-in-place proving and corrected mani… johnchandlerburnham Sep 2, 2026df4157b manifest v2: measured-peaks section in the Lean reader, tree-preservi… johnchandlerburnham Sep 2, 2026f0da4f7 ix shard refine: selective, tree-preserving partition refinement with… johnchandlerburnham Sep 2, 20265db19c7 claim-addressed progress: shard-proof index, ix prove --skip-proven, … johnchandlerburnham Sep 2, 2026f29e7ca Revert "Fix multi-stark PR77 merge resolution" (back to the Mathlib r… johnchandlerburnham Sep 2, 202654da708 Calibrate Aiur prover RSS envelope from Mathlib johnchandlerburnham Sep 2, 20269a88bac Parallelize aggregate startup johnchandlerburnham Sep 2, 2026955744b Defer aggregate setup into worker tasks johnchandlerburnham Sep 2, 202677d132d Move Stage 2 orchestration to Rust johnchandlerburnham Sep 2, 2026 File filter Filter by extension Filter by extension .json (2) .lean (42) .lock (7) .md (1) .nix (1) .rs (41) .toml (2) .yml (1) All 8 file types selected Only manifest files Viewed files Clear filters Conversations Failed to load comments. Loading Uh oh! There was an error while loading. Please reload this page. Jump to Jump to file Failed to load files. Loading Uh oh! There was an error while loading. Please reload this page. Diff view Unified Split Hide whitespace Diff view Unified Split Hide whitespace .github/actions/log-cpu/action.yml action.yml Benchmarks/AggregatePolicy.lean AggregatePolicy.lean Benchmarks/Compile/lake-manifest.json lake-manifest.json Benchmarks/RecursionDebug.lean RecursionDebug.lean Benchmarks/Typecheck.lean Typecheck.lean Cargo.lock Cargo.lock Cargo.toml Cargo.toml Ix/Aggr.lean Aggr.lean Ix/Aggr/Circuit.lean Circuit.lean Ix/Aggr/Host.lean Host.lean Ix/Aiur/Protocol.lean Protocol.lean Ix/Aiur/Semantics/BytecodeFfi.lean BytecodeFfi.lean Ix/Aiur/Stages/Codegen.lean Codegen.lean Ix/Aiur/Statistics.lean Statistics.lean Ix/Cli/AggregateCmd.lean AggregateCmd.lean Ix/Cli/BenchCmd.lean BenchCmd.lean Ix/Cli/BenchPlots.lean BenchPlots.lean Ix/Cli/CheckCmd.lean CheckCmd.lean Ix/Cli/CodegenCmd.lean CodegenCmd.lean Ix/Cli/ProveCmd.lean ProveCmd.lean Ix/Cli/RefineCmd.lean RefineCmd.lean Ix/Cli/ShardCmd.lean ShardCmd.lean Ix/Cli/ShardProofIndex.lean ShardProofIndex.lean Ix/Cli/VerifyCmd.lean VerifyCmd.lean Ix/Common.lean Common.lean Ix/IxVM/ClaimHarness.lean ClaimHarness.lean Ix/IxVM/Core.lean Core.lean Ix/IxVM/Kernel/Subst.lean Subst.lean Ix/KernelCheck.lean KernelCheck.lean Ix/MultiStark.lean MultiStark.lean Ix/MultiStark/Aggregate.lean Aggregate.lean Ix/MultiStark/Deserialize.lean Deserialize.lean Ix/MultiStark/Host.lean Host.lean Ix/MultiStark/Pcs.lean Pcs.lean Ix/MultiStark/SystemDeserialize.lean SystemDeserialize.lean Ix/MultiStark/Verifier.lean Verifier.lean Ix/Store.lean Store.lean Main.lean Main.lean Tests/Aggr.lean Aggr.lean Tests/AggrActivation.lean AggrActivation.lean Tests/AggrSemantics.lean AggrSemantics.lean Tests/Ix/BenchMeasures.lean BenchMeasures.lean Tests/Ix/Ixes.lean Ixes.lean Tests/Main.lean Main.lean Tests/MultiStark.lean MultiStark.lean crates/aiur/src/constraints.rs constraints.rs crates/aiur/src/execute.rs execute.rs crates/aiur/src/gadgets/bytes1.rs bytes1.rs crates/aiur/src/gadgets/bytes2.rs bytes2.rs crates/aiur/src/lib.rs lib.rs crates/aiur/src/memory.rs memory.rs crates/aiur/src/querymap.rs querymap.rs crates/aiur/src/synthesis.rs synthesis.rs crates/aiur/src/vk_codec.rs vk_codec.rs crates/common/src/address.rs address.rs crates/compile/src/compile.rs compile.rs crates/compile/src/compile/aux_gen/brecon.rs brecon.rs crates/compile/src/compile/aux_gen/cases_on.rs cases_on.rs crates/compile/src/compile/env.rs env.rs crates/compile/src/compile/mutual.rs mutual.rs crates/ffi/src/aiur.rs aiur.rs crates/ffi/src/aiur/aggregate.rs aggregate.rs crates/ffi/src/aiur/protocol.rs protocol.rs crates/ffi/src/catalog.rs catalog.rs crates/ffi/src/kernel.rs kernel.rs crates/ffi/src/lean.rs lean.rs crates/ffi/src/lean_env.rs lean_env.rs crates/ffi/src/lean_ixon/sharing.rs sharing.rs crates/ixon/src/diff.rs diff.rs crates/ixon/src/proof.rs proof.rs crates/ixvm-codegen/src/aiur_ix_aggr.rs aiur_ix_aggr.rs crates/ixvm-codegen/src/aiur_ix_aggr_runner.rs aiur_ix_aggr_runner.rs crates/ixvm-codegen/src/aiur_ixvm.rs aiur_ixvm.rs crates/ixvm-codegen/src/aiur_ixvm_runner.rs aiur_ixvm_runner.rs crates/ixvm-codegen/src/aiur_ixvm_witness.rs aiur_ixvm_witness.rs crates/ixvm-codegen/src/aiur_multi_stark.rs aiur_multi_stark.rs crates/ixvm-codegen/src/aiur_multi_stark_runner.rs aiur_multi_stark_runner.rs crates/ixvm-codegen/src/lib.rs lib.rs crates/kernel/src/claim.rs claim.rs crates/kernel/src/def_eq.rs def_eq.rs crates/kernel/src/inductive.rs inductive.rs crates/kernel/src/ingress.rs ingress.rs crates/kernel/src/perf.rs perf.rs crates/kernel/src/shard.rs shard.rs crates/kernel/src/tc.rs tc.rs crates/kernel/src/whnf.rs whnf.rs docs/benchmarking.md benchmarking.md flake.lock flake.lock flake.nix flake.nix lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean rust-toolchain.toml rust-toolchain.toml sp1/Cargo.lock Cargo.lock sp1/guest/Cargo.lock Cargo.lock zisk/Cargo.lock Cargo.lock zisk/agg-guest/Cargo.lock Cargo.lock zisk/guest/Cargo.lock Cargo.lock There are no files selected for viewing 26 changes: 26 additions & 0 deletions 26 .github/actions/log-cpu/action.yml Show comments View file Open in desktop Original file line number Diff line number Diff 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 764 changes: 764 additions & 0 deletions 764 Benchmarks/AggregatePolicy.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. 4 changes: 2 additions & 2 deletions 4 Benchmarks/Compile/lake-manifest.json Show comments View file Open in desktop Original file line number Diff line number Diff 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 20 changes: 14 additions & 6 deletions 20 Benchmarks/RecursionDebug.lean Show comments View file Open in desktop Original file line number Diff line number Diff line change Expand Up @@ -102,19 +102,24 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with | .error e => IO.eprintln s!"proveAddrWithEnv failed: {e}"; return none | .ok (claimBytes, proof, _) => -- `verify_claim`'s public input is the 32-G blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck). -- `verify_claim`'s public input is the packed blake3 digest of the -- serialized `Ix.Claim` (same recipe as `ix verify` / bench-typecheck: -- 8 G elements of 4 LE bytes each, `ClaimHarness.packedDigestKey`). let digest := Address.blake3 claimBytes pure (Aiur.buildClaim funIdx (digest.hash.data.map .ofUInt8) #[], proof) pure (Aiur.buildClaim funIdx (IxVM.ClaimHarness.packedDigestKey digest) #[], proof) let t1 ← IO.monoNanosNow let proofBytes := proof.toBytes IO.println s!"inner prove: {secs t0 t1} s, proof {proofBytes.size} bytes" IO.println s!"inner prove: {secs t0 t1} s, proof {proof.toBytes.size} bytes" -- Sanity: the inner proof must verify out-of-circuit before we chase the -- recursive verifier. match aiurSystem.verify claim proof with | .ok () => IO.println "inner proof verifies out-of-circuit: ok" | .error e => IO.eprintln s!"⚠ inner proof FAILS out-of-circuit verify: {e}" return some (proofBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) -- The in-circuit verifier consumes the per-query advice transport, not -- the pruned-multiproof wire format. match aiurSystem.proofToAdviceBytes claim proof with | .error e => IO.eprintln s!"advice re-encoding failed: {e}"; return none | .ok adviceBytes => return some (adviceBytes, aiurSystem.vkBytes, MultiStark.serializeClaims #[claim]) def main (args : List String) : IO UInt32 := do let ixePath := (argStr args "--ixe").getD "init.ixe" Expand All @@ -126,6 +131,9 @@ def main (args : List String) : IO UInt32 := do let mode := (argStr args "--mode").getD "native" let skipDeps := args.contains "--skip-deps" let fri := friParams (argNat args "--queries" 100) if fri.numQueries == 0 then IO.eprintln "error: --queries must be positive" return 1 let depth := argNat args "--depth" 2 let stackLimit := argNat args "--stack" 40 IO.FS.createDirAll dir Expand Down 323 changes: 301 additions & 22 deletions 323 Benchmarks/Typecheck.lean Show comments View file Open in desktop Large diffs are not rendered by default. Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Loading Oops, something went wrong. Uh oh! There was an error while loading. Please reload this page. Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later. Footer © 2026 GitHub, Inc. Footer navigation Terms Privacy Security Status Community Docs Contact You can’t perform that action at this time.