perf(ixvm): avoid repeated substitution and row copying in FLT checks

[arthurpaulino]

Two targeted changes address the large NumberField, Weierstrass and RubinSilverberg proofs from AnthropicFLT:

• Keep checked let types and delayed values in a local inference environment, materializing terms only when needed. Preserve context-sensitive memo keys; whnf and definitional equality still operate on ordinary expressions.
• Build multiplication rows with Cons instead of repeatedly copying a growing output prefix. Preserve limb arithmetic, carry checks and exact results.

Remove the obsolete function group referencing the eliminated limb-list snoc helper, regenerate the native executor, and refresh the existing IxVM FFT pins. No diagnostic stubs or ad hoc test runners are included.

Validation:

• All three focused FLT subjects finish within the 600s bytecode cap on the pre-grouping base (218s / 553s / 472s). These were subject-only diagnostics with hash/dependency checks temporarily disabled, not full FLT validation.
• On main at 4c91254, all 64 ISLB shards pass with full verification: 183,062 owned constants, 32 workers, 89.78s wall time.
• Rebuilt IxTests; lake test -- --ignored ixvm passes in 3m27s after repinning, including native/bytecode parity. Codegen consistency checks pass.

This is a targeted performance tradeoff: 49 constant pins decrease and 30 increase (largest +2.11%); the shard-pipeline pin is refreshed too.

[arthurpaulino]

!benchmark fresh

[argument-ci-bot]

!benchmark — main vs 849d2ac

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

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

7 constants · 4 with regressions · 5 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.687 s	8.814 s	+1.5%	35.525 s	35.375 s	-0.4%	78.110	78.450	+0.4%	73.48 GiB	74.36 GiB	+1.2%	5.06 MiB	5.15 MiB	+1.7%	28.2 ms	28.6 ms	+1.4%	137.19B	137.25B	+0.0%
Char.ofOrdinal_le_of_le	6.920 s	6.775 s	-2.1%	30.864 s	30.229 s	-2.1%	89.520	91.400	+2.1%	66.23 GiB	66.46 GiB	+0.3%	5.05 MiB	5.13 MiB	+1.7%	27.8 ms	29.2 ms	+4.7% ⚠️	105.30B	104.89B	-0.4%
Array.extract_append	6.479 s	6.434 s	-0.7%	26.092 s	26.351 s	+1.0%	61.550	60.950	-1.0%	53.80 GiB	54.50 GiB	+1.3%	4.92 MiB	4.99 MiB	+1.6%	29.1 ms	28.0 ms	-3.6% 🟢	99.03B	99.33B	+0.3%
Std.HashMap	4.072 s	4.046 s	-0.6%	17.429 s	16.801 s	-3.6% 🟢	117.160	121.540	+3.7% 🟢	37.65 GiB	36.96 GiB	-1.8%	4.97 MiB	5.06 MiB	+1.7%	28.8 ms	29.9 ms	+3.5% ⚠️	63.51B	63.74B	+0.4%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	3.564 s	3.597 s	+1.0%	16.032 s	15.931 s	-0.6%	116.450	117.190	+0.6%	35.52 GiB	35.87 GiB	+1.0%	4.95 MiB	5.03 MiB	+1.8%	27.3 ms	29.5 ms	+8.1% (1.08× slower) ⚠️	57.01B	57.14B	+0.2%
String.append	430.6 ms	433.6 ms	+0.7%	1.730 s	1.757 s	+1.6%	189.060	186.100	-1.6%	6.16 GiB	5.12 GiB	-16.8% (1.20× smaller) 🟢	4.70 MiB	4.78 MiB	+1.7%	26.7 ms	26.1 ms	-2.1%	3.51B	3.54B	+0.9%
Nat.add_comm	262.1 ms	262.7 ms	+0.2%	730.1 ms	743.7 ms	+1.9%	63	61.850	-1.8%	4.50 GiB	4.40 GiB	-2.1%	4.50 MiB	4.58 MiB	+1.8%	24.5 ms	24.5 ms	+0.1%	321.32M	321.98M	+0.2%

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.392 s	2.456 s	+2.7%	20.764 s	21.025 s	+1.3%	133.640	131.980	-1.2%	56.09 GiB	56.74 GiB	+1.2%	2.21 MiB	2.20 MiB	-0.5%	12.8 ms	12.3 ms	-3.8% 🟢	108.59B	110.14B	+1.4%
Char.ofOrdinal_le_of_le	2.383 s	2.399 s	+0.7%	20.889 s	20.965 s	+0.4%	132.270	131.790	-0.4%	55.98 GiB	56.68 GiB	+1.2%	2.21 MiB	2.20 MiB	-0.5%	20.3 ms	13.3 ms	-34.6% (1.53× faster) 🟢	107.48B	109.02B	+1.4%
Array.extract_append	2.336 s	2.339 s	+0.1%	19.865 s	20.175 s	+1.6%	80.850	79.600	-1.5%	53.09 GiB	54.54 GiB	+2.7%	2.21 MiB	2.21 MiB	-0.3%	12.6 ms	12.2 ms	-3.0%	104.92B	105.85B	+0.9%
Std.HashMap	2.381 s	2.405 s	+1.0%	20.381 s	20.586 s	+1.0%	100.190	99.190	-1.0%	54.57 GiB	55.21 GiB	+1.2%	2.22 MiB	2.20 MiB	-0.7%	12.5 ms	13.2 ms	+5.0% (1.05× slower) ⚠️	105.80B	107.70B	+1.8%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	2.347 s	2.414 s	+2.8%	20.045 s	20.600 s	+2.8%	93.140	90.630	-2.7%	52.91 GiB	54.77 GiB	+3.5% ⚠️	2.21 MiB	2.20 MiB	-0.4%	12.4 ms	12.8 ms	+3.1% ⚠️	105.31B	107.16B	+1.8%
String.append	2.193 s	2.191 s	-0.1%	19.069 s	18.989 s	-0.4%	17.150	17.220	+0.4%	50.88 GiB	50.63 GiB	-0.5%	2.21 MiB	2.20 MiB	-0.3%	12.8 ms	13.1 ms	+2.2%	96.36B	96.93B	+0.6%
Nat.add_comm	2.043 s	2.024 s	-0.9%	19.001 s	18.816 s	-1.0%	2.420	2.440	+0.8%	50.56 GiB	50.60 GiB	+0.1%	2.21 MiB	2.19 MiB	-0.6%	12.1 ms	12.6 ms	+3.9% ⚠️	89.07B	89.26B	+0.2%

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	56.289 s	56.400 s	+0.2%	49.300	49.200	-0.2%	73.48 GiB	74.36 GiB	+1.2%
Char.ofOrdinal_le_of_le	51.753 s	51.194 s	-1.1%	53.390	53.970	+1.1%	66.23 GiB	66.46 GiB	+0.3%
Array.extract_append	45.957 s	46.526 s	+1.2%	34.950	34.520	-1.2%	53.80 GiB	54.54 GiB	+1.4%
Std.HashMap	37.810 s	37.386 s	-1.1%	54.010	54.620	+1.1%	54.57 GiB	55.21 GiB	+1.2%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	36.077 s	36.532 s	+1.3%	51.750	51.110	-1.2%	52.91 GiB	54.77 GiB	+3.5% ⚠️
String.append	20.798 s	20.746 s	-0.3%	15.720	15.760	+0.3%	50.88 GiB	50.63 GiB	-0.5%
Nat.add_comm	19.731 s	19.559 s	-0.9%	2.330	2.350	+0.9%	50.56 GiB	50.60 GiB	+0.1%

Workflow logs