fix(aiur): reject forged results and cyclic call traces

[johnchandlerburnham]

Aiur could accept supplied traces for false public results or recursive calls
with no finite execution. This PR repairs four demonstrated trace defects
and a native Merkle commitment-binding defect. Regression tests construct
the offending witnesses and openings directly.

The implementation also reduces the cost of the repaired system through
checked call-order specialization, narrower rank and byte lookups, BLAKE3
and arithmetic changes, and smaller host data structures. Across 83 kernel
fixtures, summed raw FFT cost is 41.17% below the initial repair and
1.72% below original main. Proving time and memory vary by workload.
In its matched comparison, BLAKE3 unrolling improves Vector.append proving
time at the cost of 19.93–34.40% larger proofs across five claims and
slower verification.

Soundness repairs

1. Inactive rows cannot supply results. Enforce
   multiplicity * (1 - selector) = 0 on function and memory rows. This
   rejects the supplied witness for 3 * 5 = 16 and covers every grouped
   member. It adds a quadratic constraint without widening traces or lookups.
   Regressions.

2. Calls require a well-founded order. Every constrained call advances a
   checked static component order, increases a bounded 48-bit rank within a
   recursive component, or satisfies a checked unit-step relation on a
   self-edge. This rejects self-supporting and mutually recursive witnesses.
   Honest recursion, shared callees and advice promotion remain supported.
   Regressions.

3. Lookup messages have checked shapes. Validate public entry visibility,
   claim and call input/output arities, and continuation yields. This prevents
   zero padding from interpreting an empty return's rank seven as output
   seven. Entry shapes are cached at construction; these guards add no AIR
   columns or FFT work.
   Regressions.

4. Only terminal single-function circuits omit lookup argument gates.
   Having one selector was insufficient: an empty branch could still write a
   store lookup and change a live message's channel. Branching circuits now
   retain their gates. Degree-aware grouping accounts for those gates when
   choosing the lookup layout.
   Regressions.

5. Merkle caps must authenticate every active matrix. For trace
   log-degrees d, log-blowup b and cap height c, require
   min(c, b + max(d)) <= b + d_i for each matrix. This rejects caps that
   omit a shorter matrix's injection layer, including the supplied altered
   openings. The guard adds no trace columns or FFT work; default cap zero
   takes a constant-time check. The recursive verifier already requires zero.
   Regressions.

Construction also checks control/selector counts and component assignments.
Verification bounds lookup consumers below the field characteristic and
requires both byte tables to be active at their exact fixed heights. These
supporting guards make the counting and range assumptions explicit.

Within a ranked component, a call requests caller_rank + 1 + gap and the
callee return binds that rank. Three u16 limbs bound both rank and gap below
2^48; their sum stays below the Goldilocks characteristic. Cross-component
calls still bind the callee's rank. Independently checked component and
unit-counter certificates leave 322 of 759 constrained functions ranked
in the final IxVM program. Unsupported recursion keeps dynamic ranks.

The Lean theorems establish order and cycle results under their stated row
relations. Compiler/native checks and supplied-trace tests cover the
implementation boundary; complete compiler-to-AIR preservation and
cryptographic soundness remain outside those theorems. The precise
invariants are in the soundness notes.

Final modeled FFT cost

Measured on 2026-09-13–14 UTC. Baselines are fixed revisions: original main
58eb0977, initial repair 79d8764c, and final branch 585cea90.
Raw costs model transform work using each revision's native compiled shapes
and executed unique-query counts on identical fixtures. Proving measurements
appear separately below. Original main predates the repairs.

Workload	Original main	Initial repair	Final branch	Change from initial repair	Change from main
83 kernels, summed	83,870,409,350	140,120,053,356	82,430,187,516	-41.17%	-1.72%
Nat.add_comm	320,320,758	447,620,334	286,975,003	-35.89%	-10.41%
Vector.append	9,146,677,300	16,965,462,208	9,839,265,329	-42.00%	+7.57%
Shard pipeline	6,972,965,120	10,627,864,237	6,054,354,863	-43.03%	-13.17%

All 83 kernels improve over the initial repair, with 31.36% median reduction
and a 16.77–59.07% range. Compared with original main, 80 are cheaper.
The three regressions are Array.append_assoc (+7.86%), Vector.append
(+7.57%) and IxVMPerf.context_tower (+5.61%). The shard pipeline is
measured separately from the 83-kernel distribution.

FFT cost by change

Each row gives absolute raw FFT costs after that change. Host-memory and
query-storage changes preserve the FFT pins; the query-storage row includes
the substitution rollback. Temporary substitution and regrouping layouts
are excluded from this retained sequence.

Stage	Nat.add_comm	Vector.append	Shard pipeline
Original main (58eb0977)	320,320,758	9,146,677,300	6,972,965,120
Initial repair (79d8764c)	447,620,334	16,965,462,208	10,627,864,237
Derived callee ranks (6385126f)	440,435,264	16,510,547,185	10,431,803,035
Static component ranks (288c4c2b)	397,590,325	14,018,670,718	9,407,996,708
Compiled-degree lookup tuning (c7a5a979)	372,875,520	12,740,924,143	8,523,899,042
Byte advice and witness metadata (470eaea2)	372,875,520	12,740,924,143	8,523,899,042
Omit acyclic timestamps (9ad3e2a8)	372,875,520	12,740,924,143	8,523,899,042
Checked carry fusion (07c84d4c)	372,875,520	12,740,919,237	8,523,837,053
Streamed multiplication (a3c1c95b)	372,875,520	12,740,919,237	8,523,726,964
Query storage and lookup follow-up (34baee46)	372,875,520	12,740,919,237	8,523,726,964
Checked existing counters (ec8432ee)	365,650,158	12,434,446,688	8,228,184,055
Consolidated byte lookups (9c8a6545)	339,435,758	12,408,232,288	8,201,969,655
Bounded BLAKE3 reader (1e881534)	325,204,176	11,897,791,056	7,608,017,400
Three u16 rank limbs (e1d74d12)	316,646,988	10,869,115,402	7,222,546,870
Unrolled BLAKE3 (da9ab1a1)	287,737,607	9,946,607,515	6,082,019,144
Two-u16 comparisons (09e95317)	287,148,501	9,905,491,333	6,066,318,982
Current: lowering Let helper (585cea90)	286,975,003	9,839,265,329	6,054,354,863

The full 83-kernel distribution catches effects that the three representative
workloads can hide:

Optimization	Comparison	Median reduction	Minimum–maximum	Fixtures improved
Derived callee ranks	79d8764c → 6385126f	1.13%	0.02–2.69%	83 / 83
Static component ranks	6385126f → 288c4c2b	6.65%	0.12–18.39%	83 / 83
Lookup tuning	288c4c2b → c7a5a979	4.44%	0.10–9.21%	83 / 83
Checked carry fusion	9ad3e2a8 → 07c84d4c	0.00%	0.00–2.43%	27 / 83
Streamed multiplication	07c84d4c → a3c1c95b	0.00%	0.00–40.01%	14 / 83
Checked existing counters	34baee46 → ec8432ee	1.41%	0.06–2.65%	83 / 83
Consolidated byte lookups	ec8432ee → 9c8a6545	10.91%	0.21–20.22%	83 / 83
Bounded BLAKE3 reader	9c8a6545 → 1e881534	3.14%	0.09–5.70%	83 / 83
Three u16 rank limbs	1e881534 → e1d74d12	0.07%	−5.06–8.69%	42 / 83
Unrolled BLAKE3 compression	e1d74d12 → da9ab1a1	7.24%	0.30–12.49%	83 / 83
Two-u16 comparisons	da9ab1a1 → 09e95317	0.10%	0.001–1.586%	83 / 83
Lowering Let helper	09e95317 → 585cea90	0.03%	0.00–0.68%	80 / 83
All retained FFT optimizations	79d8764c → 585cea90	31.36%	16.77–59.07%	83 / 83

Reductions use the stated before/after revisions. A negative reduction is a
regression; unchanged fixtures are included when calculating the median.
The combined median is calculated from final versus initial costs for each
fixture, independently of the per-step medians. The shard is separate.

Raw FFT cost uses unique-query heights. The padded comparison rounds each
nonempty function/memory height to a power of two and keeps byte tables at
their fixed heights. It includes advice queries and does not separately
filter inactive rows. Both are transform-work models; measured proving time
also includes execution, witness construction and non-FFT arithmetic.

The retained changes reduce work as follows:

Change	Final behavior and measured effect
Call-order specialization and lookup tuning	Derive callee ranks in call messages, omit ranks where static order or checked counters suffice, and choose lookup groups from compiled degrees within the PCS limit. Each retained lookup grouping is accepted only if it does not raise the FFT model at any row height.
Byte-table consolidation	AND/OR share XOR and comparison shares subtraction, preserving outputs and selector gates. Removes 26,214,400 FFT units from every fixture at this step. The later u16 channel adds one main column back.
Three-u16 ranks	Preserve the 48-bit bound with half the rank/gap columns and the same three range queries. Kernel FFT sum falls 6.48% raw / 6.82% padded at this step. Its fixed-table cost raises 41 small raw fixtures by at most 5.06%.
Bounded BLAKE3 reader	A checked counter permits a three-input byte reader; block/digest/tree state stays in the outer loop. Per-byte main/stage-two widths fall 29/20 → 15/8. Kernel FFT sum falls 4.80% raw / 4.66% padded at this step.
Unrolled BLAKE3 compression	Seven fixed rounds and the digest fold form one acyclic row. Compression rows fall eightfold; all other function/memory counts stay identical. Kernel FFT sum falls 9.99% raw / 10.38% padded, and the shard 15.79% / 17.14%, at this step.
Two-u16 comparisons	Six u16 limbs replace twelve byte columns, using the existing scalar table and six range queries. Both input bounds and boolean carries remain checked. Kernel FFT sum falls 0.32% raw / 0.34% padded, with all 83 kernels and the shard improving.
Lowering Let helper	Put the three-call branch in its own ranked row. Common-walk widths fall 34/18 → 30/14; existing query counts stay identical. Kernel FFT sum falls 0.38% raw / 0.39% padded, with 80 fixtures improving and three unchanged.
Checked arithmetic fusion	Reduce carry operations and stream radix-2^16 multiplication rows into the accumulator. Carry fusion improves 27 kernels and multiplication fusion another 14; unaffected pins remain equal. Exponentiation saves 40.01% FFT work at the multiplication step.

Each percentage in this table compares that change with its immediate
baseline. The final table above measures the combined branch directly.

Proving time, memory and tradeoffs

The BLAKE3 compression comparison uses 80 verified proofs: five claims,
four layouts and four rounds, rotating each layout through every run
position. The table reports four-round medians for e1d74d12 → da9ab1a1
(original compression → full unrolling). These timings belong to that
optimization; the two subsequent changes are reported separately below.

Claim	Prove median, before → after (s)	Process peak, before → after (MiB)	Proof bytes, before → after
Nat	0.206577 → 0.205856 (-0.35%)	1380.18 → 1383.04 (+0.21%)	6,528,763 → 8,774,907 (+34.40%)
Nat.add_comm	0.647684 → 0.639331 (-1.29%)	3713.69 → 3696.70 (-0.46%)	10,713,293 → 12,957,869 (+20.95%)
Vector.append	6.990151 → 6.623373 (-5.25%)	7009.40 → 6704.04 (-4.36%)	11,290,934 → 13,540,822 (+19.93%)
IxVMPrim.nat_mul_big	0.518614 → 0.499342 (-3.72%)	3423.79 → 3424.13 (+0.01%)	10,119,041 → 12,363,905 (+22.18%)
IxVMPerf.mul_wide	0.555146 → 0.547965 (-1.29%)	3504.10 → 3502.94 (-0.03%)	10,428,118 → 12,675,670 (+21.55%)

Vector proves faster in every matched pair, with non-overlapping time
ranges (6.898–7.058 s → 6.581–6.867 s) and lower process peaks. A separate
earlier 30-proof comparison also verifies and observes 5.00% faster
Vector proving and 3.53% lower process peak RSS. The smaller claims have
overlapping time ranges and nearly unchanged process peaks.

Full unrolling grows proofs 19.93–34.40% and raises verification medians
16.07–21.54% in this comparison. Two-round and four-round layouts save less
kernel FFT work
(3.38% and 5.51% raw), with smaller proof growth (4.15–7.23% and
12.40–21.27%). Full unrolling is retained for its FFT and large-workload
proving gains; all byte operations and checks are preserved.

Other measured effects are summarized below. These are separate matched
experiments at their stated revisions; their timing percentages are not
combined into a branch-wide speedup.

Optimization and comparison	Measured results	Tradeoff or scope
Constant-time byte advice (matched old/native helpers)	At input 1,048,576, function queries 4,118 → 2 and median execution 2.546 → 0.942 ms. Caller still checks byte bounds and reconstruction.	Isolated hint benchmark; all FFT pins stay unchanged. Maximum-u32 execution is checked, but not timed.
Witness metadata (c7a5a979 → 470eaea2)	Metadata 72 → 16 bytes/active row. On 1,048,576 rows, median witness time 100.019 → 61.581 ms and process RSS 284.84 → 225.25 MiB.	Witness-only fixture; no STARK is produced. Shared member metadata is included in allocated-byte accounting.
Omitted acyclic timestamps (470eaea2 → 9ad3e2a8)	Full-closure proof process peaks fall 5.35–8.30%; omit 16.9–33.2% of function timestamps.	Proving changes range from −6.98% to +0.53%. Ranked completion order and advice promotion are preserved; FFT pins stay unchanged.
Packed query storage (10a4ba50 → cd1df1e5)	Key/output payload falls 70.00–77.46%. Proof process peaks fall 16.75–17.18% on three smaller claims and 1.67% on Vector.	Proving changes range from −2.86% to +5.34%; Vector is 3.78% slower. Exact decoded equality, lossless widening and full-field multiplicities are preserved.
Packed-storage follow-up (5e2f65f1 → 34baee46)	Vector executes 14.47% fewer instructions than the initial packed implementation and removes 2,576,234 pointer-payload bytes.	Still 15.52% more instructions than full-width storage. Contended timings establish no additional stable speedup or process-RSS gain.
Arithmetic fusion (07c84d4c → a3c1c95b)	Exponentiation median proving 0.978295 → 0.785132 s (−19.74%), faster in all three pairs.	Other proving results are mixed; Nat.add_comm is 7.50% slower in this comparison. Carry fusion alone gives no consistent proving-speed gain.
BLAKE3 reader (9c8a6545 → 1e881534)	Vector proves 4.86% faster with 3.18% lower process RSS.	Smaller workloads have mixed time/RSS results; proofs grow 0.042–0.233%.
Three-u16 ranks (1e881534 → e1d74d12)	Vector proves 4.90% faster with 10.07% lower process RSS; all five proof sizes shrink 5.28–7.11%.	Large multiplication proves 5.38% slower; small FFT regressions are included above.
Two-u16 comparisons (da9ab1a1 → 09e95317)	Proofs shrink 0.25–0.51%; Vector whole-process instructions fall 0.37% in an eight-pair follow-up.	First Vector prove median is 4.81% slower; the follow-up is 0.63% faster with overlapping ranges. No stable proving-speed gain is established. All 56 proofs verify.
Lowering Let helper (09e95317 → 585cea90)	Nat.add_comm median proving falls 3.94%, faster in all four pairs; four proof sizes shrink 0.016–0.119%.	Vector’s proof grows 0.23% and proving median rises 1.03%. All prove-time ranges overlap; these measurements establish no stable proving-speed gain. The execution-only follow-up is 1.78% slower with effectively unchanged instructions. All 40 proofs verify.

Packed storage uses canonical byte/u32/full-field columns and widens when
a value requires it. Direct encoding/decoding, implicit memory outputs and
hash reuse reduce overhead while retaining exact key equality and completion
semantics. The RAM estimator now sums grouped rows correctly and includes
extension-field, row-writer and metadata storage. Its historical 43/40 RSS
calibration still needs full-scale validation against the pinned prover.

Substitution-prefix sharing was reverted and function regrouping was not
retained: their small model gains did not justify the measured time, memory
or proof-size costs. Production uses complete substitution keys; their
semantic regressions remain.

The real proof matrices use frozen executables and identical serialized
claims, eight Rayon workers, blowup four, cap zero, 100 FRI queries,
final-polynomial log length zero, maximum log arity one and no proof of work.
The prove timer includes execution, witness construction and STARK proving;
loading, setup, the separate execution pass, serialization and verification
are outside it. Process RSS is GNU time's whole-process high-water mark.
Sampled prove-window peaks cover a different scope and show mixed changes.
The four-layout compression matrix encountered other host activity, so
small timing differences remain uncertain. Results from separate timing
windows are reported independently.

Compatibility and validation

Rebuild Lean and Rust systems, all three generated executors, and
verification keys together, then regenerate proofs. The branch changes
AIR/lookup layouts, the internal component metadata, some function indices
and private helper arities. Public claim encoding and hash results are
preserved. Malformed claims, metadata and unsafe cap configurations now reject.

• 10,866 primary assertions pass, including source/bytecode agreement,
  proofs, recursive verification, arithmetic, hashing and aggregation.
• 845 IxVM assertions pass, covering adversarial executions, generated
  executor parity, all 83 kernel plus shard FFT pins, and production/full
  component certificates.
• 98 native tests pass under each of default and parallel features:
  91 Aiur and seven generated-executor tests; four opt-in benchmarks remain
  ignored in the normal suite.
• Component analysis matches an independent oracle on all 512 directed
  three-vertex graphs; native counter tests cover 4,096 graph/rank cases.
  Range/byte tests exhaust all 65,536 values or pairs and exercise forged
  limbs, cross-channel messages, inactive rows and decoded keys. New u32
  comparisons also reject supplied witnesses that satisfy the local
  polynomials but violate a limb bound, and cover advice promotion.
• Independent BLAKE3 references cover arbitrary word states, block/chunk
  boundaries, remainders and wrong digests. All 80 proofs across four
  compression layouts and 30 earlier unroll proofs verify with exact
  FFT references; the two timing windows are reported separately.
  All 40 matched u32-comparison proofs and 16 Vector follow-up proofs
  also verify with exact references, as do the 40 lowering-helper proofs.
  Two additional binding proofs cover whole and nested Let lowering.
• Warning-free Lean build, workspace Clippy with all targets and
  ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi, Rust formatting, and freshness
  checks for all three generated executors pass (799/262/263 functions).

Validation commands

CARGO_BUILD_JOBS=8 RAYON_NUM_THREADS=8 lake build --wfail ix IxTests bench-typecheck
IX_COMPILE_WORKERS=4 RAYON_NUM_THREADS=8 lake env .lake/build/bin/IxTests
IX_COMPILE_WORKERS=4 RAYON_NUM_THREADS=8 lake env .lake/build/bin/IxTests --ignored ixvm
CARGO_BUILD_JOBS=8 RAYON_NUM_THREADS=8 cargo test --release --locked -p aiur -p ixvm-codegen -- --test-threads=1
CARGO_BUILD_JOBS=8 RAYON_NUM_THREADS=8 cargo test --release --locked -p aiur -p ixvm-codegen --features parallel -- --test-threads=1
cargo clippy --workspace --locked --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings
cargo fmt --all -- --check
RAYON_NUM_THREADS=8 lake env .lake/build/bin/ix codegen --check

All 83 kernel FFT measurements

Integer-rounded raw costs for the fixed revisions above. The final column
uses original main as its denominator; reductions use the initial repair.

Kernel fixture	Original main	Initial repair	Final branch	Reduction from initial repair	Change from main
HEq	129,561,906	130,092,790	108,238,714	16.80%	-16.46%
HEq.rec	133,623,510	137,362,242	112,280,861	18.26%	-15.97%
Eq.rec	133,010,671	136,027,876	111,473,585	18.05%	-16.19%
Nat	129,621,454	130,060,261	108,243,336	16.77%	-16.49%
Nat.add	170,017,266	197,695,257	145,849,134	26.23%	-14.22%
Nat.add_comm	320,320,758	447,620,334	286,975,003	35.89%	-10.41%
Nat.decEq	373,889,414	567,581,286	356,647,644	37.16%	-4.61%
Nat.decLe	806,851,440	1,315,310,972	781,109,313	40.61%	-3.19%
Nat.sub_le_of_le_add	1,934,072,047	3,328,720,460	1,924,713,930	42.18%	-0.48%
Nat.shiftRight_succ	1,440,427,524	2,445,999,615	1,424,472,143	41.76%	-1.11%
Trans.mk	137,030,955	145,076,422	116,187,053	19.91%	-15.21%
Array.append_assoc	8,942,722,073	16,621,232,050	9,645,457,338	41.97%	+7.86%
Vector.append	9,146,677,300	16,965,462,208	9,839,265,329	42.00%	+7.57%
IxVMPrim.nat_add_lit	212,562,390	262,801,388	181,755,914	30.84%	-14.49%
IxVMPrim.nat_sub_lit	227,018,404	284,521,561	193,565,408	31.97%	-14.74%
IxVMPrim.nat_mul_lit	203,023,243	246,518,065	172,120,120	30.18%	-15.22%
IxVMPrim.nat_mul_big	201,532,839	244,385,255	171,049,382	30.01%	-15.13%
IxVMPrim.nat_div_lit	1,404,629,363	2,381,418,249	1,386,769,606	41.77%	-1.27%
IxVMPrim.nat_mod_lit	1,431,635,704	2,425,927,469	1,411,394,862	41.82%	-1.41%
IxVMPrim.nat_succ_lit	144,182,615	151,050,620	119,372,490	20.97%	-17.21%
IxVMPrim.nat_pred_lit	165,781,989	183,486,510	136,833,404	25.43%	-17.46%
IxVMPrim.nat_gcd_lit	2,205,281,085	3,785,736,196	2,183,477,855	42.32%	-0.99%
IxVMPrim.nat_land_lit	3,614,023,887	6,215,635,638	3,557,998,635	42.76%	-1.55%
IxVMPrim.nat_lor_lit	3,616,139,531	6,218,494,242	3,559,510,707	42.76%	-1.57%
IxVMPrim.nat_xor_lit	3,635,365,296	6,246,434,034	3,574,459,542	42.78%	-1.68%
IxVMPrim.nat_shl_lit	232,546,611	291,579,290	196,702,459	32.54%	-15.41%
IxVMPrim.nat_shr_lit	1,419,952,900	2,403,043,114	1,398,427,642	41.81%	-1.52%
IxVMPrim.nat_pow_big	394,444,673	624,316,509	255,557,217	59.07%	-35.21%
IxVMPrim.nat_beq_lit	200,563,953	245,012,105	171,737,291	29.91%	-14.37%
IxVMPrim.nat_ble_lit	196,027,245	236,989,197	167,149,562	29.47%	-14.73%
IxVMPrim.nat_cases_big	165,979,714	184,684,065	137,897,476	25.33%	-16.92%
IxVMPrim.nat_dec_le	824,803,643	1,342,961,129	796,613,783	40.68%	-3.42%
IxVMPrim.nat_dec_lt	836,382,068	1,361,042,944	806,557,880	40.74%	-3.57%
IxVMPrim.nat_dec_eq	413,163,878	628,894,977	390,904,124	37.84%	-5.39%
IxVMPrim.str_size_lit	2,535,275,859	4,285,000,756	2,456,083,092	42.68%	-3.12%
IxVMPrim.bv_to_nat_lit	2,110,179,170	3,606,708,590	2,081,224,725	42.30%	-1.37%
IxVMInd.Even	206,433,604	251,494,925	174,892,773	30.46%	-15.28%
IxVMInd.Odd	206,438,231	251,504,665	174,897,586	30.46%	-15.28%
IxVMInd.Even.rec	225,289,131	282,364,930	192,198,609	31.93%	-14.69%
IxVMInd.Odd.rec	225,288,202	282,364,002	192,197,680	31.93%	-14.69%
IxVMInd.IdxTeleN.rec	160,786,136	177,402,027	133,887,511	24.53%	-16.73%
IxVMInd.IdxTeleB.rec	160,784,445	177,400,336	133,885,820	24.53%	-16.73%
IxVMInd.SoloA.rec	155,960,075	169,266,008	129,383,237	23.56%	-17.04%
IxVMInd.SoloB.rec	155,959,238	169,265,171	129,382,400	23.56%	-17.04%
IxVMInd.UnsafeSquash	131,441,226	132,544,402	109,397,466	17.46%	-16.77%
IxVMInd.Tree	131,235,133	132,484,806	109,619,583	17.26%	-16.47%
IxVMInd.Tree.rec	141,939,288	149,744,671	119,038,764	20.51%	-16.13%
IxVMInd.DedupM	134,567,476	136,883,294	111,803,709	18.32%	-16.92%
IxVMInd.DedupM.rec	148,905,382	160,258,504	124,695,389	22.19%	-16.26%
IxVMInd.DepthM	132,968,937	134,821,747	110,812,633	17.81%	-16.66%
IxVMInd.DepthM.rec	144,439,261	154,000,589	121,469,804	21.12%	-15.90%
String.Internal.append	2,505,741,376	4,239,729,239	2,430,974,538	42.66%	-2.98%
_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec	3,705,214,978	6,331,329,170	3,611,288,746	42.96%	-2.53%
Lean.Syntax.rec	2,568,020,495	4,337,298,464	2,485,436,024	42.70%	-3.22%
IxVMInd.AuxTie	324,084,157	421,081,929	266,404,278	36.73%	-17.80%
IxVMInd.AuxTie.rec	369,734,259	496,204,215	308,418,169	37.84%	-16.58%
IxVMInd.HiddenIdx	130,534,316	131,311,692	108,849,353	17.11%	-16.61%
IxVMInd.HiddenIdx.rec	133,887,001	136,869,443	111,857,414	18.27%	-16.45%
IxVMInd.thmMajorUse	513,390,983	803,735,348	490,670,269	38.95%	-4.43%
IxVMInd.partialKRec	150,145,230	162,145,600	125,955,599	22.32%	-16.11%
IxVMInd.deepRebase	221,120,959	278,922,839	191,453,221	31.36%	-13.42%
String.Slice.Pattern.Model.NoPrefixPatternModel.rec	3,482,661,414	6,023,770,121	3,455,995,894	42.63%	-0.77%
Lean.Widget.TaggedText.rec	2,537,347,634	4,295,817,454	2,462,919,411	42.67%	-2.93%
Lean.Doc.Part.rec	2,582,681,092	4,370,674,121	2,505,636,582	42.67%	-2.98%
Lean.Doc.Block.rec	2,815,192,541	4,812,252,515	2,759,410,730	42.66%	-1.98%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A	132,539,812	134,133,524	110,353,411	17.73%	-16.74%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec	136,173,435	139,577,096	113,247,617	18.86%	-16.84%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1	135,089,400	139,282,130	113,328,566	18.63%	-16.11%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2	135,089,400	139,282,130	113,328,566	18.63%	-16.11%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1	135,089,400	139,282,130	113,328,566	18.63%	-16.11%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M	132,835,071	134,632,062	110,680,644	17.79%	-16.68%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec	144,806,931	153,819,023	121,168,039	21.23%	-16.32%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1	144,805,348	153,817,441	121,166,456	21.23%	-16.32%
_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2	135,089,400	139,282,130	113,328,566	18.63%	-16.11%
strOfListFoldSize	2,817,854,521	4,742,118,434	2,710,309,882	42.85%	-3.82%
strOfListFoldSizeAscii	2,818,697,757	4,743,185,354	2,710,818,874	42.85%	-3.83%
IxVMPrim.lazy_ble_offset	233,714,099	296,886,064	200,155,437	32.58%	-14.36%
IxVMPrim.lazy_unit_cast	552,027,642	853,952,001	515,556,139	39.63%	-6.61%
IxVMPrim.sizeof_unit	160,797,387	174,561,290	132,098,740	24.33%	-17.85%
IxVMPerf.let_continuations	163,740,427	196,207,899	144,702,530	26.25%	-11.63%
IxVMPerf.mul_row	420,640,365	566,690,116	373,082,715	34.16%	-11.31%
IxVMPerf.context_tower	514,164,080	866,051,473	543,014,527	37.30%	+5.61%
IxVMPerf.mul_wide	266,740,297	379,467,156	219,608,490	42.13%	-17.67%

[arthurpaulino]

!benchmark fresh

[argument-ci-bot]

!benchmark — main vs b189530

backends: aiur=prove · envs: InitStd · baseline: fresh (benchmark products rebuilt, base-SHA run, bencher bypassed)

aiur · InitStd · prove — main from: base run @ 58eb097 (fresh — bencher bypassed)

7 constants · 7 with regressions · 7 with improvements (|Δ| > 3.0% on any metric).

IxVM on FRI (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	8.542 s	9.720 s	+13.8% (1.14× slower) ⚠️	35.314 s	40.541 s	+14.8% (1.15× slower) ⚠️	78.580	68.450	-12.9% (1.15× slower) ⚠️	72.49 GiB	78.57 GiB	+8.4% (1.08× larger) ⚠️	5.16 MiB	7.01 MiB	+35.8% (1.36× larger) ⚠️	29.8 ms	49.0 ms	+64.1% (1.64× slower) ⚠️	132.99B	145.18B	+9.2% (1.09× more) ⚠️
Array.extract_append	6.338 s	7.179 s	+13.3% (1.13× slower) ⚠️	26.634 s	32.591 s	+22.4% (1.22× slower) ⚠️	60.300	49.280	-18.3% (1.22× slower) ⚠️	53.24 GiB	63.99 GiB	+20.2% (1.20× larger) ⚠️	5.01 MiB	6.85 MiB	+36.9% (1.37× larger) ⚠️	28.3 ms	39.0 ms	+37.5% (1.38× slower) ⚠️	95.20B	116.63B	+22.5% (1.23× more) ⚠️
Char.ofOrdinal_le_of_le	6.163 s	6.939 s	+12.6% (1.13× slower) ⚠️	29.325 s	32.200 s	+9.8% (1.10× slower) ⚠️	94.220	85.810	-8.9% (1.10× slower) ⚠️	62.76 GiB	65.23 GiB	+3.9% ⚠️	5.16 MiB	7.01 MiB	+35.8% (1.36× larger) ⚠️	29.3 ms	39.5 ms	+34.9% (1.35× slower) ⚠️	95.52B	102.31B	+7.1% (1.07× more) ⚠️
Std.HashMap	3.957 s	4.216 s	+6.5% (1.07× slower) ⚠️	17.235 s	18.813 s	+9.2% (1.09× slower) ⚠️	118.480	108.540	-8.4% (1.09× slower) ⚠️	36.50 GiB	38.89 GiB	+6.5% (1.07× larger) ⚠️	5.08 MiB	7.00 MiB	+37.8% (1.38× larger) ⚠️	28.6 ms	38.0 ms	+33.0% (1.33× slower) ⚠️	61.01B	64.67B	+6.0% (1.06× more) ⚠️
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	3.545 s	3.885 s	+9.6% (1.10× slower) ⚠️	16.096 s	18.247 s	+13.4% (1.13× slower) ⚠️	115.990	102.320	-11.8% (1.13× slower) ⚠️	35.07 GiB	37.35 GiB	+6.5% (1.06× larger) ⚠️	5.05 MiB	6.98 MiB	+38.2% (1.38× larger) ⚠️	29.0 ms	40.3 ms	+38.6% (1.39× slower) ⚠️	55.56B	59.28B	+6.7% (1.07× more) ⚠️
String.append	434.1 ms	457.7 ms	+5.4% (1.05× slower) ⚠️	1.793 s	1.953 s	+8.9% (1.09× slower) ⚠️	182.420	167.470	-8.2% (1.09× slower) ⚠️	4.84 GiB	5.69 GiB	+17.6% (1.18× larger) ⚠️	4.80 MiB	6.63 MiB	+38.0% (1.38× larger) ⚠️	27.6 ms	36.2 ms	+31.2% (1.31× slower) ⚠️	3.45B	3.42B	-0.6%
Nat.add_comm	262.2 ms	269.6 ms	+2.8%	741.7 ms	759.5 ms	+2.4%	62.020	60.570	-2.3%	4.43 GiB	4.09 GiB	-7.6% (1.08× smaller) 🟢	4.60 MiB	6.39 MiB	+38.8% (1.39× larger) ⚠️	25.4 ms	33.4 ms	+31.5% (1.32× slower) ⚠️	320.32M	286.98M	-10.4% (1.12× fewer) 🟢

FRI verifier on FRI (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	throughput (const/s) (main)	throughput (const/s) (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	2.463 s	2.694 s	+9.4% (1.09× slower) ⚠️	21.961 s	27.728 s	+26.3% (1.26× slower) ⚠️	126.360	100.080	-20.8% (1.26× slower) ⚠️	56.66 GiB	71.32 GiB	+25.9% (1.26× larger) ⚠️	2.20 MiB	3.78 MiB	+71.7% (1.72× larger) ⚠️	12.2 ms	19.9 ms	+63.2% (1.63× slower) ⚠️	110.55B	98.89B	-10.6% (1.12× fewer) 🟢
Array.extract_append	2.377 s	2.658 s	+11.8% (1.12× slower) ⚠️	20.960 s	27.266 s	+30.1% (1.30× slower) ⚠️	76.620	58.900	-23.1% (1.30× slower) ⚠️	54.60 GiB	68.72 GiB	+25.9% (1.26× larger) ⚠️	2.20 MiB	3.78 MiB	+71.8% (1.72× larger) ⚠️	12.3 ms	20.9 ms	+69.5% (1.70× slower) ⚠️	105.50B	96.17B	-8.8% (1.10× fewer) 🟢
Char.ofOrdinal_le_of_le	2.510 s	2.740 s	+9.2% (1.09× slower) ⚠️	21.645 s	27.655 s	+27.8% (1.28× slower) ⚠️	127.650	99.910	-21.7% (1.28× slower) ⚠️	56.84 GiB	70.07 GiB	+23.3% (1.23× larger) ⚠️	2.21 MiB	3.78 MiB	+70.9% (1.71× larger) ⚠️	13.6 ms	20.3 ms	+49.4% (1.49× slower) ⚠️	110.68B	98.96B	-10.6% (1.12× fewer) 🟢
Std.HashMap	2.491 s	2.664 s	+7.0% (1.07× slower) ⚠️	21.290 s	27.459 s	+29.0% (1.29× slower) ⚠️	95.910	74.370	-22.5% (1.29× slower) ⚠️	55.14 GiB	70.02 GiB	+27.0% (1.27× larger) ⚠️	2.20 MiB	3.78 MiB	+71.9% (1.72× larger) ⚠️	12.5 ms	19.6 ms	+56.6% (1.57× slower) ⚠️	108.13B	97.81B	-9.5% (1.11× fewer) 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	2.468 s	2.689 s	+9.0% (1.09× slower) ⚠️	21.297 s	27.687 s	+30.0% (1.30× slower) ⚠️	87.660	67.430	-23.1% (1.30× slower) ⚠️	54.67 GiB	70.08 GiB	+28.2% (1.28× larger) ⚠️	2.19 MiB	3.79 MiB	+72.5% (1.73× larger) ⚠️	12.3 ms	20.2 ms	+63.6% (1.64× slower) ⚠️	107.01B	97.66B	-8.7% (1.10× fewer) 🟢
String.append	2.205 s	2.548 s	+15.5% (1.16× slower) ⚠️	19.640 s	20.062 s	+2.2%	16.650	16.300	-2.1%	50.68 GiB	50.65 GiB	-0.1%	2.21 MiB	3.78 MiB	+70.8% (1.71× larger) ⚠️	12.5 ms	20.0 ms	+59.3% (1.59× slower) ⚠️	96.08B	90.94B	-5.3% (1.06× fewer) 🟢
Nat.add_comm	2.172 s	2.342 s	+7.8% (1.08× slower) ⚠️	19.767 s	19.836 s	+0.4%	2.330	2.320	-0.4%	50.76 GiB	48.83 GiB	-3.8% 🟢	2.21 MiB	3.78 MiB	+70.8% (1.71× larger) ⚠️	12.3 ms	20.1 ms	+63.5% (1.63× slower) ⚠️	90.48B	84.24B	-6.9% (1.07× fewer) 🟢

Aggregate flat join (7 constants)

constant	execute-time (main)	execute-time (PR)	Δ%	prove-time (main)	prove-time (PR)	Δ%	peak-ram (main)	peak-ram (PR)	Δ%	proof-size (main)	proof-size (PR)	Δ%	verify-time (main)	verify-time (PR)	Δ%	fft-cost (main)	fft-cost (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a
Array.extract_append	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a
Char.ofOrdinal_le_of_le	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a
Std.HashMap	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a
String.append	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a
Nat.add_comm	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a	n/a

Pipeline total (7 constants)

constant	total-time (main)	total-time (PR)	Δ%	pipeline-throughput (const/s) (main)	pipeline-throughput (const/s) (PR)	Δ%	pipeline-peak-ram (main)	pipeline-peak-ram (PR)	Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append	57.274 s	1m 8.3s	+19.2% (1.19× slower) ⚠️	48.450	40.650	-16.1% (1.19× slower) ⚠️	72.49 GiB	78.57 GiB	+8.4% (1.08× larger) ⚠️
Array.extract_append	47.594 s	59.856 s	+25.8% (1.26× slower) ⚠️	33.740	26.830	-20.5% (1.26× slower) ⚠️	54.60 GiB	68.72 GiB	+25.9% (1.26× larger) ⚠️
Char.ofOrdinal_le_of_le	50.970 s	59.855 s	+17.4% (1.17× slower) ⚠️	54.210	46.160	-14.8% (1.17× slower) ⚠️	62.76 GiB	70.07 GiB	+11.7% (1.12× larger) ⚠️
Std.HashMap	38.525 s	46.272 s	+20.1% (1.20× slower) ⚠️	53	44.130	-16.7% (1.20× slower) ⚠️	55.14 GiB	70.02 GiB	+27.0% (1.27× larger) ⚠️
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	37.393 s	45.933 s	+22.8% (1.23× slower) ⚠️	49.930	40.650	-18.6% (1.23× slower) ⚠️	54.67 GiB	70.08 GiB	+28.2% (1.28× larger) ⚠️
String.append	21.432 s	22.015 s	+2.7%	15.260	14.850	-2.7%	50.68 GiB	50.65 GiB	-0.1%
Nat.add_comm	20.508 s	20.596 s	+0.4%	2.240	2.230	-0.4%	50.76 GiB	48.83 GiB	-3.8% 🟢

Workflow logs