perf(ixvm): reduce FLT checking costs and witness memory

[arthurpaulino]

Recover the remaining FLT checks without reverting delayed-let inference or tuning reduction fuel.

Changes:

• Strengthen delayed application contexts across unused Let/Local prefixes. Count raw bindings separately from type-context slots, lift the inferred type back, and keep introductions and pure-let contexts delayed.
• Stop minimum loose-variable-index scans at zero, preserving the exact summaries and memo keys while skipping irrelevant subtrees.
• Compare projected function heads through definitionally equal scrutinees before unfolding their potentially large arguments.
• Multiply U64 limbs in radix 2^16. Range-check decomposition advice and constrain reconstruction below the field modulus; reuse the checked high limb or its modular successor when propagating a one-bit carry.
• Fill pre-sized witness arenas directly in parallel instead of retaining converted partial buffers and copying growing arenas. Preserve stable offsets, channel contents and hints; test against serial construction.

Add two small synthetic FFT guards, prototyped with direct ix check runs: context strengthening costs 514,164,080 versus 808,853,595 with that path disabled; varied multi-limb multiplication costs 266,740,297 versus 277,782,128 with the previous arithmetic. Retain the existing let/row guards, regenerate the native executor, and refresh all affected suite FFT pins.

Native validation with full hashing and closure checking, no proving:

• Init+Std+Lean+Batteries: 64/64 shards pass; 14,154,767,400,043 total FFT.
• Mathlib: 256/256 pass; 147,662,851,272,684 total FFT.
• Anthropic FLT: 4099/4099 pass; 1,371,135,736,576,741 total FFT.

FLT validation refines overloaded shard 504 into four children, placing its four expensive certificates separately. Exact/disjoint coverage, unchanged external assumptions, and all 4095 untouched claim digests were verified. Shards 2083, 2747 and 3949 passed isolated retries after timeouts or host memory pressure during the concurrent sweep. This is not a claim that all original shards finish under the original concurrent schedule.

Against main 5430a5d, the same 4077 successful FLT claims fall from 1,539,563,003,720,477 to 1,331,530,648,023,083 FFT (-13.51%). All remain successful: 4036 are cheaper and 41 more expensive. Do not compare the full new total with the incomplete baseline subtotal as though coverage matched.

The rebuilt IxVM suite passes its exact FFT pins, adversarial rejection checks, and native/bytecode parity checks. Temporary diagnostic stubs and CheckCmd fixtures are removed; environment/shard files and sweep logs stay outside the commit.

[arthurpaulino]

!benchmark fresh

[argument-ci-bot]

!benchmark — main vs a39e444

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

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

7 constants · 5 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	9.147 s	8.782 s	-4.0% 🟢	37.210 s	35.925 s	-3.5% 🟢	74.580	77.240	+3.6% 🟢	74.28 GiB	72.48 GiB	-2.4%	5.15 MiB	5.16 MiB	+0.2%	28.6 ms	30.3 ms	+5.8% (1.06× slower) ⚠️	137.25B	132.99B	-3.1% 🟢
Char.ofOrdinal_le_of_le	6.953 s	6.277 s	-9.7% (1.11× faster) 🟢	31.734 s	29.636 s	-6.6% (1.07× faster) 🟢	87.070	93.230	+7.1% (1.07× faster) 🟢	66.37 GiB	62.77 GiB	-5.4% (1.06× smaller) 🟢	5.13 MiB	5.16 MiB	+0.5%	29.7 ms	32.5 ms	+9.6% (1.10× slower) ⚠️	104.89B	95.52B	-8.9% (1.10× fewer) 🟢
Array.extract_append	6.486 s	6.399 s	-1.4%	27.514 s	27.184 s	-1.2%	58.370	59.080	+1.2%	54.57 GiB	53.13 GiB	-2.6%	4.99 MiB	5.02 MiB	+0.5%	29.4 ms	29.4 ms	-0.0%	99.33B	95.20B	-4.2% 🟢
Std.HashMap	4.248 s	3.827 s	-9.9% (1.11× faster) 🟢	18.734 s	17.283 s	-7.7% (1.08× faster) 🟢	109	118.150	+8.4% (1.08× faster) 🟢	36.98 GiB	36.33 GiB	-1.8%	5.06 MiB	5.08 MiB	+0.4%	30.8 ms	29.5 ms	-4.3% 🟢	63.74B	61.01B	-4.3% 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	3.709 s	3.515 s	-5.2% (1.06× faster) 🟢	16.694 s	16.331 s	-2.2%	111.840	114.320	+2.2%	35.91 GiB	34.97 GiB	-2.6%	5.03 MiB	5.06 MiB	+0.5%	30.3 ms	29.6 ms	-2.3%	57.14B	55.56B	-2.8%
String.append	437.7 ms	430.0 ms	-1.7%	1.851 s	1.828 s	-1.2%	176.700	178.880	+1.2%	5.02 GiB	5.35 GiB	+6.6% (1.07× larger) ⚠️	4.78 MiB	4.81 MiB	+0.5%	27.0 ms	28.8 ms	+6.7% (1.07× slower) ⚠️	3.54B	3.45B	-2.6%
Nat.add_comm	285.6 ms	265.5 ms	-7.0% (1.08× faster) 🟢	796.8 ms	766.4 ms	-3.8% 🟢	57.730	60.020	+4.0% 🟢	4.49 GiB	4.61 GiB	+2.7%	4.58 MiB	4.61 MiB	+0.7%	29.5 ms	25.5 ms	-13.5% (1.16× faster) 🟢	321.98M	320.32M	-0.5%

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.517 s	2.504 s	-0.5%	21.916 s	21.839 s	-0.3%	126.620	127.070	+0.4%	56.58 GiB	56.57 GiB	-0.0%	2.20 MiB	2.21 MiB	+0.6%	12.7 ms	12.8 ms	+0.7%	110.14B	109.89B	-0.2%
Char.ofOrdinal_le_of_le	2.417 s	2.565 s	+6.1% (1.06× slower) ⚠️	21.710 s	21.914 s	+0.9%	127.270	126.090	-0.9%	56.72 GiB	56.50 GiB	-0.4%	2.20 MiB	2.20 MiB	-0.1%	13.5 ms	13.1 ms	-3.0% 🟢	109.02B	110.42B	+1.3%
Array.extract_append	2.364 s	2.575 s	+8.9% (1.09× slower) ⚠️	20.992 s	21.293 s	+1.4%	76.500	75.420	-1.4%	54.68 GiB	54.85 GiB	+0.3%	2.21 MiB	2.19 MiB	-0.6%	12.4 ms	12.8 ms	+3.0% ⚠️	105.85B	106.81B	+0.9%
Std.HashMap	2.490 s	2.464 s	-1.1%	21.474 s	21.472 s	-0.0%	95.090	95.100	+0.0%	55.30 GiB	55.07 GiB	-0.4%	2.20 MiB	2.21 MiB	+0.3%	15.8 ms	12.3 ms	-22.2% (1.28× faster) 🟢	107.70B	107.73B	+0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	2.373 s	2.442 s	+2.9%	21.364 s	21.463 s	+0.5%	87.390	86.990	-0.5%	54.75 GiB	55.13 GiB	+0.7%	2.20 MiB	2.21 MiB	+0.4%	13.5 ms	13.2 ms	-2.0%	107.16B	107.86B	+0.7%
String.append	2.229 s	2.286 s	+2.6%	19.858 s	20.279 s	+2.1%	16.470	16.130	-2.1%	50.63 GiB	50.60 GiB	-0.1%	2.20 MiB	2.20 MiB	+0.0%	14.2 ms	12.6 ms	-10.9% (1.12× faster) 🟢	96.93B	97.95B	+1.0%
Nat.add_comm	2.179 s	2.249 s	+3.2% ⚠️	20.289 s	19.739 s	-2.7%	2.270	2.330	+2.6%	50.57 GiB	50.61 GiB	+0.1%	2.19 MiB	2.20 MiB	+0.2%	12.9 ms	15.2 ms	+17.3% (1.17× slower) ⚠️	89.26B	91.86B	+2.9%

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
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
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
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	59.126 s	57.764 s	-2.3%	46.930	48.040	+2.4%	74.28 GiB	72.48 GiB	-2.4%
Char.ofOrdinal_le_of_le	53.443 s	51.550 s	-3.5% 🟢	51.700	53.600	+3.7% 🟢	66.37 GiB	62.77 GiB	-5.4% (1.06× smaller) 🟢
Array.extract_append	48.506 s	48.477 s	-0.1%	33.110	33.130	+0.1%	54.68 GiB	54.85 GiB	+0.3%
Std.HashMap	40.208 s	38.756 s	-3.6% 🟢	50.790	52.690	+3.7% 🟢	55.30 GiB	55.07 GiB	-0.4%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	38.058 s	37.794 s	-0.7%	49.060	49.400	+0.7%	54.75 GiB	55.13 GiB	+0.7%
String.append	21.709 s	22.107 s	+1.8%	15.060	14.790	-1.8%	50.63 GiB	50.60 GiB	-0.1%
Nat.add_comm	21.086 s	20.505 s	-2.8%	2.180	2.240	+2.8%	50.57 GiB	50.61 GiB	+0.1%

Workflow logs