From 9ab1eacfe05cbf91a8be92f0c1579e785044b4b1 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 13 Aug 2026 16:26:53 +0000 Subject: [PATCH 1/2] bench: add Vector.append, String.split, Array.extract_append to aiur-recursive The CI recursive-verifier benchmark now covers the heavy tier (kernel scale) alongside Nat.add_comm: recursiveConstants grows to four fixed IxVM statements, all resolving in InitStd. A run that exceeds the CI RAM ceiling still lands as an OOM row rather than failing the upload. --- .github/workflows/bench-main.yml | 5 +++-- .github/workflows/bench-pr.yml | 6 +++--- Ix/Cli/BenchCmd.lean | 13 ++++++------- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 17a90125..179857ee 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -245,8 +245,9 @@ jobs: # - decompile: the inverse of compile. Roundtrip correctness is # checked elsewhere (`ix validate` / roundtrip tests) — this only # measures speed and memory. - # - aiur-recursive: proves the IxVM typecheck of two fixed constants - # (Nat.add_comm, Array.extract_append), runs the in-circuit + # - aiur-recursive: proves the IxVM typecheck of four fixed constants + # (Nat.add_comm, Vector.append, String.split, + # Array.extract_append), runs the in-circuit # verifier over each proof, then proves THAT — the cost of # recursion at kernel scale. A fixed subset instead of the # Vectors.csv fan-out: its `env` field names the (already-cached) diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index db88afa8..4a5321e7 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -32,9 +32,9 @@ # - zisk / sp1 / ooc: `execute`. # - compile: `ix compile .lean` → `.ixe`. # - decompile: `ix decompile` over the compile run's fresh `.ixe`. -# - aiur-recursive: a fixed IxVM statement (Nat.add_comm; the heavy-tier -# Array.extract_append is dropped for now — significantly more -# expensive even at 50 queries) proved and recursively verified via +# - aiur-recursive: fixed IxVM statements (Nat.add_comm plus the +# heavy-tier Vector.append, String.split, and Array.extract_append) +# proved and recursively verified via # bench-typecheck --recursive; always schedules exactly one run # regardless of BENCH_ENVS (the constants resolve in whichever env's # .ixe the entry carries). diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index 9df9c336..eb63c0ee 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -251,7 +251,7 @@ def backendSpecs : List BackendSpec := [ -- `recursiveConstants`): IxVM recursion on real statements — prove each -- constant's typecheck, execute the in-circuit multi-stark verifier -- over the fresh proof, then prove THAT execution. The same measurement - -- as the aiur recursive mode above, but over a fixed two-constant + -- as the aiur recursive mode above, but over a fixed four-constant -- subset so CI schedules exactly one entry instead of the whole -- Vectors.csv fan-out. { name := "aiur-recursive", defaultMode := "prove", inputs := .fixedConfigs, @@ -343,18 +343,17 @@ def findBackend (name : String) : Option BackendSpec := /-- The `aiur-recursive` backend's rows: fixed IxVM statements, proved and recursively verified by `bench-typecheck --recursive` under the recursion-tuned parameters (50 queries at log-blowup 2, ~100-bit - soundness — this benchmarks *secure* recursion). Currently only - `Nat.add_comm` (cheap tier — the small end of the IxVM cost range): - `Array.extract_append` (heavy tier — kernel scale) is dropped for now, - its recursion being significantly more expensive even at 50 queries; - re-add it when the verifier prover slims down. A stage that exceeds + soundness — this benchmarks *secure* recursion). `Nat.add_comm` + (cheap tier) is the small end of the IxVM cost range; + `Vector.append`, `String.split`, and `Array.extract_append` (heavy + tier — kernel scale) are the expensive end. A stage that exceeds the CI RAM ceiling lands as an OOM row — the honest signal that secure recursion at that scale does not yet fit. (Measured 2026-08 at 100 queries: `Nat.add_comm`'s outer prove peaked ~195 GiB on the ~123 GiB runners; the 50-query halving is what gives it a chance to fit.) -/ def recursiveConstants : List String := - ["Nat.add_comm"] + ["Nat.add_comm", "Vector.append", "String.split", "Array.extract_append"] def BackendSpec.testbedFor (b : BackendSpec) (mode : String) : Option String := (b.testbeds.find? (·.1 == mode)).map (·.2) From 652279ce406bb9783599410af9ab6aef4fc1825f Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 13 Aug 2026 16:51:31 +0000 Subject: [PATCH 2/2] =?UTF-8?q?bench:=20drop=20Array.extract=5Fappend=20fr?= =?UTF-8?q?om=20aiur-recursive=20=E2=80=94=20OOMs=20on=20CI?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Even at 50 queries its outer prove exceeds the CI RAM ceiling; re-add it when the verifier prover slims down. The heavy tier keeps Vector.append and String.split. --- .github/workflows/bench-main.yml | 5 ++--- .github/workflows/bench-pr.yml | 4 ++-- Ix/Cli/BenchCmd.lean | 21 +++++++++++---------- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/.github/workflows/bench-main.yml b/.github/workflows/bench-main.yml index 179857ee..f5fb8d87 100644 --- a/.github/workflows/bench-main.yml +++ b/.github/workflows/bench-main.yml @@ -245,9 +245,8 @@ jobs: # - decompile: the inverse of compile. Roundtrip correctness is # checked elsewhere (`ix validate` / roundtrip tests) — this only # measures speed and memory. - # - aiur-recursive: proves the IxVM typecheck of four fixed constants - # (Nat.add_comm, Vector.append, String.split, - # Array.extract_append), runs the in-circuit + # - aiur-recursive: proves the IxVM typecheck of three fixed constants + # (Nat.add_comm, Vector.append, String.split), runs the in-circuit # verifier over each proof, then proves THAT — the cost of # recursion at kernel scale. A fixed subset instead of the # Vectors.csv fan-out: its `env` field names the (already-cached) diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml index 4a5321e7..a4e19ad4 100644 --- a/.github/workflows/bench-pr.yml +++ b/.github/workflows/bench-pr.yml @@ -33,8 +33,8 @@ # - compile: `ix compile .lean` → `.ixe`. # - decompile: `ix decompile` over the compile run's fresh `.ixe`. # - aiur-recursive: fixed IxVM statements (Nat.add_comm plus the -# heavy-tier Vector.append, String.split, and Array.extract_append) -# proved and recursively verified via +# heavy-tier Vector.append and String.split; Array.extract_append +# is dropped for now — it OOMs on CI) proved and recursively verified via # bench-typecheck --recursive; always schedules exactly one run # regardless of BENCH_ENVS (the constants resolve in whichever env's # .ixe the entry carries). diff --git a/Ix/Cli/BenchCmd.lean b/Ix/Cli/BenchCmd.lean index eb63c0ee..cdfb361a 100644 --- a/Ix/Cli/BenchCmd.lean +++ b/Ix/Cli/BenchCmd.lean @@ -223,7 +223,7 @@ def backendSpecs : List BackendSpec := [ -- large closures exceed the RAM ceiling and land as `status: oom` rows -- that bmf drops), which is why it's marked `unscheduled`: a testbed for -- local `--mode recursive` runs only — never uploaded to bencher, never - -- plotted. CI tracks the same measurement over the fixed two-constant + -- plotted. CI tracks the same measurement over the fixed three-constant -- subset via the aiur-recursive backend below. { name := "aiur", defaultMode := "prove", inputs := .perConstant, testbeds := [("prove", "aiur-check-prove-x64-32x"), @@ -251,7 +251,7 @@ def backendSpecs : List BackendSpec := [ -- `recursiveConstants`): IxVM recursion on real statements — prove each -- constant's typecheck, execute the in-circuit multi-stark verifier -- over the fresh proof, then prove THAT execution. The same measurement - -- as the aiur recursive mode above, but over a fixed four-constant + -- as the aiur recursive mode above, but over a fixed three-constant -- subset so CI schedules exactly one entry instead of the whole -- Vectors.csv fan-out. { name := "aiur-recursive", defaultMode := "prove", inputs := .fixedConfigs, @@ -345,15 +345,16 @@ def findBackend (name : String) : Option BackendSpec := recursion-tuned parameters (50 queries at log-blowup 2, ~100-bit soundness — this benchmarks *secure* recursion). `Nat.add_comm` (cheap tier) is the small end of the IxVM cost range; - `Vector.append`, `String.split`, and `Array.extract_append` (heavy - tier — kernel scale) are the expensive end. A stage that exceeds - the CI RAM ceiling lands as an OOM row — the honest signal that - secure recursion at that scale does not yet fit. (Measured 2026-08 at - 100 queries: `Nat.add_comm`'s outer prove peaked ~195 GiB on the - ~123 GiB runners; the 50-query halving is what gives it a chance to - fit.) -/ + `Vector.append` and `String.split` (heavy tier — kernel scale) are + the expensive end. `Array.extract_append` is dropped for now — it + OOMs on CI even at 50 queries; re-add it when the verifier prover + slims down. A stage that exceeds the CI RAM ceiling lands as an OOM + row — the honest signal that secure recursion at that scale does not + yet fit. (Measured 2026-08 at 100 queries: `Nat.add_comm`'s outer + prove peaked ~195 GiB on the ~123 GiB runners; the 50-query halving + is what gives it a chance to fit.) -/ def recursiveConstants : List String := - ["Nat.add_comm", "Vector.append", "String.split", "Array.extract_append"] + ["Nat.add_comm", "Vector.append", "String.split"] def BackendSpec.testbedFor (b : BackendSpec) (mode : String) : Option String := (b.testbeds.find? (·.1 == mode)).map (·.2)