ci: track the 4-to-1 aggregation proven on one thread

.github/workflows/bench.yml

@@ -85,6 +85,7 @@ jobs:
           - name: aggregate-leanxmss-100-2to1
           - name: aggregate-leanxmss-100-4to1
           - name: aggregate-leanxmss-100-2to1-1thread
+          - name: aggregate-leanxmss-100-4to1-1thread
           - name: flock-hash-batch-262144
           - name: flock-arithmetic-batch
           - name: pcs-throughput

AGENTS.md

@@ -189,7 +189,7 @@ Addition with carries, comparisons, shifts, AND/OR, multiplication and division
 - **Witness generation is word arithmetic wherever a circuit has a generator, and the generic walk of the gate list, bit by bit, elsewhere**: ALU, LOAD, STORE, LD, SD, SHIFT, MULH and HASH fill by `Fill::Instance` (`ClassCircuit::fill`), MUL by `Fill::Batch8` on AVX2 only, and every clock circuit has one (`ClassSpec::clock_witness`: `Clock::witness`, and for EXT's, whose ports past the clock's split the flags and add 8 and 16 to the pointers, `Ext::clock_witness` on top of `Clock::witness_with`); DIV and MUL off AVX2 walk. Each generator computes the circuit's values natively and writes its rows in the order the circuit makes its products (all but the multipliers' through `rv::circuits::Products`), so a change to a circuit's gate list must change its generator too. Each is pinned to the walk by a test that covers edge words (zero, all ones, the sign bits, every shift amount, every misalignment) and random instances: `semantics::tests::word_witness_is_the_walk` for ALU, the memory classes and SHIFT, and their own for MUL, MULH, HASH and the clock circuits (`clock::tests::the_word_witness_is_the_gate_walk`, every table's, EXT's included). A new generator needs such a test. HASH's generator is unrolled, so every carry run's place is a constant.
 - **Circuit sizes are structure, not measurements**: `k_log` (its `ClassCircuit`'s) and `clock_k_log` per class are pinned in its `ClassSpec` and asserted against the built circuits; product counts are in `doc/leanvm` Annex C. A product can be committed straight at an output port's position (`flock::circuit::Builder::and_output`), which saves the copy; the clock circuit's step uses it.
 
-CI compares every PR with its base, never with a history. The base is the merge commit's first parent; a workflow builds and runs both on one runner and saves both as an artifact, and a `workflow_run` workflow on the default branch (`main`, the only branch GitHub runs those from) posts them on the PR as one comment, edited on every run and deleted once nothing changed. The posting workflows never run the PR's code: they take only the PR number from a run's artifact, a fork's included, post nothing unless GitHub's API says that PR's head is the commit the run measured, and check every name and number before it reaches the comment. **Exact counts**: `counts.yml` runs `cargo leanvm bench --cycles-only`, every program at the sizes above without a proof (`cycles`, the program's own instructions; `proven-rows`, table heights after padding; `committed`, witness words) and the two aggregation trees above, one case per tree and kind of node (`aggregate-leanxmss-400-2to1-first` and `-node`, `aggregate-leanxmss-400-4to1-first` and `-node`, from `counted_trees()`: `rows`, the circuit's own; `proven-rows` and `committed` as for a program), puts the tables in each run's summary from the same pass (`--markdown-file "$GITHUB_STEP_SUMMARY"`, which appends what `--markdown` prints), saves the artifact `counts` and fails on any increase; `counts-comment.yml` posts the counts that changed. A tree's name says its shape, `Nto1` for N proofs combined into 1 at every node; `-first` is a first-level node (the RISC-V verifier in rows over N leaf proofs) and `-node` a higher node (the recursion verifier in rows over N child proofs). **Proving**: `bench.yml` runs one job per testbed and benchmark: each case of `proven()` in `bins/leanvm/src/tracked.rs` (at the sizes a 16 GB runner holds: leanXMSS, leanSPHINCS, Falcon, the state proofs and the shielded transfers at a quarter, no leanDA; leanXMSS also on one thread, `leanxmss-100-1thread`, which the CLI proves in a process of its own with `LEANVM_NUM_THREADS=1` since the pool is sized once per process), each of `proven_trees()` (the two aggregation trees above over leanXMSS at a quarter, `aggregate-leanxmss-100-2to1` and `aggregate-leanxmss-100-4to1`: the leaf proven once, then one first-level node and one node over copies of it, the two benchmarks `<case>-first` and `<case>-node`, each node's stages the children of a `Prove` span around it and the node's peak memory including the first-level node's; the 2-to-1 tree also on one thread, `aggregate-leanxmss-100-2to1-1thread`, proven whole, leaf included, in a process of its own like `leanxmss-100-1thread`), and each `benches/` target above with every benchmark it prints (flock's two at `FLOCK_N_LOG=18`, pcs's `throughput` at its default size). Each job builds both sides and runs them in turns, base, PR, PR, base, for `ROUNDS` rounds: `cargo leanvm bench --only <case>` gives the proving time, the proof's size in bytes (exact: the inputs are seeded and grinding takes the smallest nonce), the time of each of the proof's stages (`stage.<name>`, the `Prove` span's direct children, `--tracing`'s first level, timed by a `tracing` layer that enables spans only), the process's peak resident memory (`peak-memory`, that case's alone since each job proves one), the proving passes' heap as the global allocator counts it (`heap-peak`, the most bytes live at once above those live when a pass began, and `allocations`, its allocations and reallocations, each the largest over the measured passes; host-side setup is outside them), and the verifying time, and a target's `--json` its own measures: `latency` for a whole operation (flock's proving times with the witness excluded, pcs's commit and open), `per-op` in nanoseconds per call for `kernels`, a hashed block of `hash_throughput` and one NTT encode. `bench-comment.yml` posts a size that changed and a time that moved the same way in every round with a median ratio at least 1% from one, every result collapsed beneath; it gates nothing. Run in turns on one runner, the comparison does not depend on which machine the job landed on, which a history across GitHub's runners does (one runner label spans CPU models of different speeds). The testbeds are self-hosted runners, `x86-64` on `size-attester7870-x64` (an Intel Xeon Gold 6548N, 32 vCPUs, 64 GB) and `arm64` on `size-attester7870-arm64` (an Arm Neoverse-V2, 16 vCPUs, 64 GB), each built for `target-cpu=native` since base and PR build and run on that one machine: x86-64 measures the AVX-512, VPCLMULQDQ and GFNI arms, and arm64 the NEON field kernels, which are chosen at compile time on `aes` and `sha3` (a generic aarch64 target enables neither, so the arm64 job fails early if its build does not enable them or the CPU lacks what the build enables). Each job prints the CPU and its relevant features, and keys its cache on the CPU model so a native build is never reused on another CPU. In a fork's own repository, which has no such runners, the testbeds fall back to GitHub-hosted runners with a pinned ISA, since a cached native build dies of SIGILL on an older CPU: `ubuntu-latest` built for `target-cpu=haswell`, and `ubuntu-24.04-arm` built for `target-cpu=neoverse-n2` plus `+aes,+sha3`. A benchmark's name is what base and PR are matched by, so renaming one or changing its input shows it as new, as does one the base cannot run (it cannot build the target, or its first base run fails or prints no JSON, and the job carries on with the PR's runs alone).
+CI compares every PR with its base, never with a history. The base is the merge commit's first parent; a workflow builds and runs both on one runner and saves both as an artifact, and a `workflow_run` workflow on the default branch (`main`, the only branch GitHub runs those from) posts them on the PR as one comment, edited on every run and deleted once nothing changed. The posting workflows never run the PR's code: they take only the PR number from a run's artifact, a fork's included, post nothing unless GitHub's API says that PR's head is the commit the run measured, and check every name and number before it reaches the comment. **Exact counts**: `counts.yml` runs `cargo leanvm bench --cycles-only`, every program at the sizes above without a proof (`cycles`, the program's own instructions; `proven-rows`, table heights after padding; `committed`, witness words) and the two aggregation trees above, one case per tree and kind of node (`aggregate-leanxmss-400-2to1-first` and `-node`, `aggregate-leanxmss-400-4to1-first` and `-node`, from `counted_trees()`: `rows`, the circuit's own; `proven-rows` and `committed` as for a program), puts the tables in each run's summary from the same pass (`--markdown-file "$GITHUB_STEP_SUMMARY"`, which appends what `--markdown` prints), saves the artifact `counts` and fails on any increase; `counts-comment.yml` posts the counts that changed. A tree's name says its shape, `Nto1` for N proofs combined into 1 at every node; `-first` is a first-level node (the RISC-V verifier in rows over N leaf proofs) and `-node` a higher node (the recursion verifier in rows over N child proofs). **Proving**: `bench.yml` runs one job per testbed and benchmark: each case of `proven()` in `bins/leanvm/src/tracked.rs` (at the sizes a 16 GB runner holds: leanXMSS, leanSPHINCS, Falcon, the state proofs and the shielded transfers at a quarter, no leanDA; leanXMSS also on one thread, `leanxmss-100-1thread`, which the CLI proves in a process of its own with `LEANVM_NUM_THREADS=1` since the pool is sized once per process), each of `proven_trees()` (the two aggregation trees above over leanXMSS at a quarter, `aggregate-leanxmss-100-2to1` and `aggregate-leanxmss-100-4to1`: the leaf proven once, then one first-level node and one node over copies of it, the two benchmarks `<case>-first` and `<case>-node`, each node's stages the children of a `Prove` span around it and the node's peak memory including the first-level node's; both trees also on one thread, `aggregate-leanxmss-100-2to1-1thread` and `aggregate-leanxmss-100-4to1-1thread`, each proven whole, leaf included, in a process of its own like `leanxmss-100-1thread`), and each `benches/` target above with every benchmark it prints (flock's two at `FLOCK_N_LOG=18`, pcs's `throughput` at its default size). Each job builds both sides and runs them in turns, base, PR, PR, base, for `ROUNDS` rounds: `cargo leanvm bench --only <case>` gives the proving time, the proof's size in bytes (exact: the inputs are seeded and grinding takes the smallest nonce), the time of each of the proof's stages (`stage.<name>`, the `Prove` span's direct children, `--tracing`'s first level, timed by a `tracing` layer that enables spans only), the process's peak resident memory (`peak-memory`, that case's alone since each job proves one), the proving passes' heap as the global allocator counts it (`heap-peak`, the most bytes live at once above those live when a pass began, and `allocations`, its allocations and reallocations, each the largest over the measured passes; host-side setup is outside them), and the verifying time, and a target's `--json` its own measures: `latency` for a whole operation (flock's proving times with the witness excluded, pcs's commit and open), `per-op` in nanoseconds per call for `kernels`, a hashed block of `hash_throughput` and one NTT encode. `bench-comment.yml` posts a size that changed and a time that moved the same way in every round with a median ratio at least 1% from one, every result collapsed beneath; it gates nothing. Run in turns on one runner, the comparison does not depend on which machine the job landed on, which a history across GitHub's runners does (one runner label spans CPU models of different speeds). The testbeds are self-hosted runners, `x86-64` on `size-attester7870-x64` (an Intel Xeon Gold 6548N, 32 vCPUs, 64 GB) and `arm64` on `size-attester7870-arm64` (an Arm Neoverse-V2, 16 vCPUs, 64 GB), each built for `target-cpu=native` since base and PR build and run on that one machine: x86-64 measures the AVX-512, VPCLMULQDQ and GFNI arms, and arm64 the NEON field kernels, which are chosen at compile time on `aes` and `sha3` (a generic aarch64 target enables neither, so the arm64 job fails early if its build does not enable them or the CPU lacks what the build enables). Each job prints the CPU and its relevant features, and keys its cache on the CPU model so a native build is never reused on another CPU. In a fork's own repository, which has no such runners, the testbeds fall back to GitHub-hosted runners with a pinned ISA, since a cached native build dies of SIGILL on an older CPU: `ubuntu-latest` built for `target-cpu=haswell`, and `ubuntu-24.04-arm` built for `target-cpu=neoverse-n2` plus `+aes,+sha3`. A benchmark's name is what base and PR are matched by, so renaming one or changing its input shows it as new, as does one the base cannot run (it cannot build the target, or its first base run fails or prints no JSON, and the job carries on with the PR's runs alone).
 
 `bench.yml`'s jobs each run `scripts/ab.sh --ci` on their benchmark, and the script owns the whole comparison (which benchmarks are `benches/` targets, the settings they run with, the order of the rounds, the tolerance of a base that cannot run, `ab.json`), so a local run of it makes the comparison CI makes. `counts.yml` keeps its own steps; `scripts/ab.sh counts` is the same comparison. Run from the Actions tab (`workflow_dispatch`), `bench.yml` compares any two refs on the same testbeds (inputs `head`, default the branch it runs on, and `base`, default the head's first parent, passed to `ab.sh --base`) and leaves its artifacts only, since `bench-comment.yml` posts for PRs alone.
 

bins/leanvm/src/tracked.rs

@@ -7,9 +7,9 @@
 //! runners (16 GB, `.github/workflows/bench.yml`) takes the sizes that fit them (leanXMSS and
 //! leanSPHINCS at a quarter, and no leanDA, whose one blob is its smallest run), and a PR's
 //! base and head are proven in turns on one runner and compared there. leanXMSS at a quarter,
-//! and the 2-to-1 tree over it, are also proven on one thread, in a process of their own
-//! (`ONE_THREAD`). A case's name is what a PR's results are matched by, so renaming one or
-//! changing its input shows it as new.
+//! and the 2-to-1 and 4-to-1 trees over it, are also proven on one thread, in a process of
+//! their own (`ONE_THREAD`). A case's name is what a PR's results are matched by, so renaming
+//! one or changing its input shows it as new.
 //!
 //! An aggregation tree is tracked the same way: each kind of node's circuit counted without a
 //! proof (the leaf's run measured gives the shape its proofs announce), and one node of each
@@ -84,7 +84,11 @@ fn proven() -> [(&'static str, Build); 8] {
 /// `LEANVM_NUM_THREADS`, so unless this process's pool is one thread already, such a case is
 /// proven by a child: this executable run again with `LEANVM_NUM_THREADS=1` (`on_one_thread`),
 /// a tree's leaf proof included.
-const ONE_THREAD: [&str; 2] = ["leanxmss-100-1thread", "aggregate-leanxmss-100-2to1-1thread"];
+const ONE_THREAD: [&str; 3] = [
+    "leanxmss-100-1thread",
+    "aggregate-leanxmss-100-2to1-1thread",
+    "aggregate-leanxmss-100-4to1-1thread",
+];
 
 /// An aggregation tree over copies of one case's proof: first-level nodes of `arity_0` leaves,
 /// nodes of `arity` tree proofs. A tree's name ends `<N>to1` when both are `N`: every node
@@ -151,9 +155,8 @@ fn counted_trees() -> Vec<Aggregation> {
 type BuildTree = fn(&'static str) -> Aggregation;
 
 /// Aggregation trees proven: the counted trees' arities over leaves of a size proven above, and
-/// the 2-to-1 tree again on one thread. Each gives two benchmarks, `<name>-first` and
-/// `<name>-node`.
-fn proven_trees() -> [(&'static str, BuildTree); 3] {
+/// both trees again on one thread. Each gives two benchmarks, `<name>-first` and `<name>-node`.
+fn proven_trees() -> [(&'static str, BuildTree); 4] {
     [
         ("aggregate-leanxmss-100-2to1", |name| {
             Aggregation::new(name, Workload::leanxmss(100), 2, 2)
@@ -164,6 +167,9 @@ fn proven_trees() -> [(&'static str, BuildTree); 3] {
         ("aggregate-leanxmss-100-2to1-1thread", |name| {
             Aggregation::new(name, Workload::leanxmss(100), 2, 2)
         }),
+        ("aggregate-leanxmss-100-4to1-1thread", |name| {
+            Aggregation::new(name, Workload::leanxmss(100), 4, 4)
+        }),
     ]
 }