WIP: Scale FLT IxVM execution with native setup, compact records, and incremental refinement

[johnchandlerburnham]

Make whole-environment IxVM execution practical to iterate on: move expensive
partition setup into Rust, reduce retained execution records and arithmetic
work, and refine oversized shards without waiting for unrelated shards to
finish. Add explicit, bounded resource handling and a reproducible focused
regression loop for the previously problematic FLT constants.

This PR concerns IxVM execution, not the native Rust kernel's check-rs
performance and not a completed STARK proof of FLT. The native kernel changes
already landed in #617; this branch replays only the two subsequent IxVM commits
onto main, which also includes function grouping from #619.

The focused FLT cases, ordinary/Mathlib closure controls, and mixed/forced-split
rollout gates pass on the pre-rebase implementation. A full execution of all
1,330,204 environment constants in 4,100 source shards is running, not yet
claimed successful. That run uses a frozen pre-rebase binary; it cannot validate
the later integration with main's function grouping.

Motivation

Earlier full attempts exposed several distinct bottlenecks:

• Lean-side coverage and ownership preparation repeatedly decoded the full
  environment before execution could begin.
• A wide Rayon pool and static owned-byte estimates did not prevent memory
  exhaustion. Admission can stop new work, but cannot reclaim an active
  record that continues to grow.
• Arithmetic helpers retained many intermediate limb lists; substitution
  keys distinguished unused trailing arguments; query keys and counters
  often occupied wider storage than their values required.
• Wave-based refinement left split children waiting for an unrelated slow
  peer, while repeated full-shard tests delayed reaching known hard constants.

The changes address these separately. Execution storage, process RSS, cgroup
charges, predicted prover RAM and FFT cost remain distinct measurements.

Changes

Native partition setup and independent setup parallelism

• Keep the metadata-light .ixe mmap, manifest, decoded ownership and audit
  in Rust. Fuse complete constant validation and ownership assignment into
  one parallel pass; only summary counts/timing cross the Lean FFI.
• Verify every constant's content address and complete serialized body,
  including otherwise unreferenced constants. Preserve manifest framing,
  dense IDs, tree coverage and exactly-once block ownership checks.
• Assign all mutual-block projection variants to their owning block. Keep
  ownership and first-error ordering deterministic across worker counts.
• Support both full and selected execution on the native path. The entire
  manifest is still validated for a selection; skipped leaves are reported
  unchanged, never certified by the subset test.
• Use a temporary setup pool, defaulting to at most eight available CPUs,
  independently of --jobs and RAYON_NUM_THREADS. Validate the positive
  IX_AIUR_SETUP_THREADS override before loading the large input and drop
  the setup pool before creating the execution pool.
• Preserve legacy paths for options needing their additional semantics,
  including destination-prover-budget refinement and refined-manifest output.
  The path-based FFI remains an IO operation, not a pure cached file read.

Memory-aware admission and early execution limits

• Read host and ancestor-cgroup headroom, process RSS/swap and memory PSI;
  retain reserves, outstanding reservations and a recent-growth forecast.
  Ramp concurrency using observed completions, not just elapsed time.
• Reserve local and shared execution-storage credits before query storage
  grows. Account for segment/bucket allocation, promotion and simultaneous
  old/new storage during widening or rehash. Drop storage before releasing
  its credits; failed growth is atomic for the affected query map.
• Distinguish local record exhaustion, shared batch exhaustion and semantic
  rejection. Split local-limit failures only between whole blocks. Drain peers
  and retry an unchanged claim after shared-budget pressure, at most twice.
• Keep indivisible oversized blocks as explicit failures. Interrupted
  execution is neither a passed check nor a measured/proven record.
• Fix the admission starvation found during linked validation: short PSI
  spikes still immediately pause admission and reduce concurrency, but only
  sustained pressure, swap growth or insufficient headroom restarts the long
  recovery timer. Recurring brief global stalls cannot indefinitely reset it.
• Report the backoff reason, instantaneous/trend PSI, swap growth, remaining
  recovery delay and next reservation. Malformed telemetry fails closed;
  optional unavailable PSI is handled separately. An idle admission failure
  has a bounded deadline and cannot become partial success.

Accounted-record limits are not hard RSS bounds. Witness construction,
stacks, bigint scratch, allocation overhead and file mappings still require
an independently enforced OS memory cap. This does not suspend active workers,
spill records, or grant a growing shard more memory dynamically.

Completion-driven refinement

• Replace the native driver's wave barrier with a bounded FIFO completion
  coordinator outside Rayon. Children become ready after parent cleanup,
  while unrelated attempts may remain active.
• Share one execution pool, admission controller and aggregate budget across
  all generations. Active tasks plus unconsumed completions are bounded by
  the pool width; Rayon workers do not wait for admission permits.
• Preserve exact selected block ownership, mutual projections and claim
  construction through recursive splits. Drain launched work on errors and
  keep retry/termination limits explicit.
• Track settlement of original selected shards separately from execution
  attempts. A split parent settles only when all descendants finish; settlement
  may include failure, so the final report remains the success criterion.
• Report scheduler: "completion-driven", executed attempts,
  max_generation, deterministic final labels, and waves: null. Do not
  fabricate a measured parent peak from its children's records.

Compact query records and reusable hashes

• Store canonical query columns in lossless byte/u32/full-field segments,
  widening only as values require. Reconstruct memory-query outputs from
  insertion indices after checking that invariant; retain function outputs.
• Preserve exact key equality, insertion order, row IDs, multiplicities,
  hint promotion, logical witnesses and field semantics. Hashes accelerate
  lookup; they never replace an equality check.
• Compute a canonical key hash once and carry owned scalar metadata across
  recursive calls/returns and memory insertion. Never retain a borrowed
  hash-table bucket across recursive growth or remove a required re-probe.
• Add opt-in u32 multiplicity segments with lossless full-field promotion.
  Fallible updates propagate through generated and interpreted execution,
  including memo hits and promotion. Field wrap does not truncate or saturate.
• Keep IX_AIUR_COMPACT_MULTIPLICITIES off by default. Add bounded-output,
  opt-in query/multiplicity diagnostics to measure tradeoffs, not an unbounded
  per-query history in ordinary execution.

Arithmetic and substitution work reduction

• Replace the recursive byte-division hint with constant-time host hinting,
  retaining the checked range, carry and reconstruction relations.
• Build multiplication rows linearly; use carry-specialized addition where
  its preconditions are established. Fuse later product rows into addition
  without allocating separate product and shifted intermediate lists.
• Preserve raw limb-list results, including empty/denormalized cases, rather
  than testing only the final mathematical integer. Keep multiplication and
  addition carries distinct and retain a useful empty-accumulator fast path.
• Project unused trailing substitution entries out of memo keys. Preserve
  the original substitution-window length and binder depth so higher variables
  still shift correctly. Sparse removal of interior holes is not implemented.
• Express projected keys in checked Aiur code, not hidden Rust-only cache
  equivalences. Add independent Lean models/lemmas, differential tests against
  the previous algorithms, invalid-input cases and small prove/verify fixtures.
• Reject malformed byte-gadget inputs with typed errors before mutation,
  rather than bounds/conversion panics. Preserve the distinction between
  unconstrained hint evaluation and the relations that subsequently check it.

Arithmetic and substitution changes can alter logical query counts and FFT
costs; they are not merely invisible storage transformations. Cost pins are
reviewed explicitly, including fixtures where an optimization is a tradeoff.
The Lean lemmas do not amount to a full proof of the Aiur compiler or kernel.

Focused regressions and integration with current main

• Add the Lean bench-ixvm-focus helper and documented reproducible commands.
  Isolate previously failing singleton blocks from a completed report while
  retaining the rest of a complete, disjoint manifest and its aggregation tree.
• Persist selected block IDs and source/refined manifest identities in a
  sidecar. Reuse the same inputs across frozen binaries; this is not cached
  successful checking of skipped declarations.
• Integrate compact query views with main's grouped trace builder. Keep shared
  per-member metadata and only member/query indices for selected rows; preserve
  member order, selector offsets and the original function-channel identities.
• Fix the grouped prover-peak row mapping: a circuit must sum its member
  functions' query counts before hypothetical subdivision, not index one
  function by circuit number. Counts remain conservative about zero-multiplicity
  hint rows; exact active-row accounting is still a separate follow-up.
• Extend exact trace/lookup comparisons and honest/tampered proof tests to a
  grouped circuit with nested hint promotion and mixed-width values. Preserve
  surviving groups rather than disabling grouping to pass tests. Remove the
  obsolete list_snoc.U8_8 member, which linear limb construction eliminated;
  newly introduced functions keep their default singleton circuits.
• Regenerate/check Rust executors through the Lean emitter. Large generated
  diffs include function-index renumbering and error propagation; the generated
  files are not hand-maintained alternative implementations.

Validation and measurements

Completed pre-rebase validation

• Aiur release unit tests passed in both feature configurations: 52 passed,
  four opt-in tests ignored. FFI: 67 passed, two external/live tests ignored in
  each configuration; strict Clippy and formatting passed.
• Thirty stress repetitions of all 27 admission tests passed. Tests cover
  1/2/64 workers, nested Rayon work, early children, pressure retries, panic/error
  cleanup, unknown telemetry, malformed outcomes and starvation/idle failures.
• Sequential lake build ix and lake build IxTests passed; all three generated
  targets matched ix codegen --check.
• Linked tests passed: 7,148 arithmetic/substitution assertions, 831 production
  IxVM assertions including 243 generated/interpreted parity checks, and native
  partition tests with compact counters both off and on. Recursive verifier,
  aggregation, small honest proofs and tampering rejection were also exercised.
• Eighteen rotating previous/full/compact runs on Core and Mathlib-prime
  extracted closures passed with identical claims, ownership and estimated
  proving cost. These are closure controls, not full Mathlib IxVM execution.

Measured improvements and limits

All timings below are historical pre-function-grouping measurements using
matched selections and preserved binaries. They are not measurements of the
rebased branch or a statistically established full-corpus speedup.

Experiment	Control	Candidate	Interpretation
Four hard FLT singletons, fused arithmetic	990.3s execution	881.1s	About 11% lower execution time in one pair; all four pass
Same four cases, prehashed queries after typed-byte fix	903.6s	871.1s	About 3.6% lower in one pair; peak RSS essentially unchanged
Mixed ordinary/heavy selection, completion queue	304.876s	304.048s	591 constants pass; effectively unchanged without splitting
Forced refinement at 8 GiB per record	190.821s	184.091s	590 constants pass in 18 attempts / 11 final parts; about 3.5% lower in this pair

• Native setup originally measured 42.133s versus approximately 817.9s from
  the Lean control's timestamps, combining native decoding, parallelism and
  removal of duplicate work. Cache state/concurrent activity differed; this
  is not a 19x whole-execution claim. Separately, independent setup workers
  reduced the focused serial coverage phase from 161.234s to about 21–23s.
• The current full run's setup took 36.979s: 15.250s loading plus 21.728s
  complete coverage/ownership validation on eight setup threads.
• Compact multiplicities reduce GNU-time peak RSS by approximately 4% across
  the four hard singleton pairs. Execution is broadly flat and one case is
  slower. Small/Core and Mathlib timing controls are noisy, with no universal
  throughput gain; compact multiplicities remain opt-in.
• Storage compression preserves exact main and lookup traces. Substitution
  projection has mixed circuit-cost effects: the initial production fixture
  sum increased about 0.13%, despite substantial sharing wins in the targeted
  fixture. Fused multiplication later improved 13 of 81 production pins with
  the other 68 unchanged; repeated-input synthetic cases can still regress.
• Forced refinement matched exact final block lists, claim digests, statuses,
  ownership counts and predicted proof peaks, not just pass counts. Its real
  trace shows a split child starting while an original peer still executes.
  GNU-time peak RSS was 39.38 versus 39.13 GiB; both runs had no swap or major
  faults. The 8 GiB limit is a test trigger, not a production recommendation.

Completed rebase validation

• Main's Complete anonymous checking of AnthropicFLT and reduce repeated kernel work #617 tree was verified identical to the old kernel-stack tip before
  rebasing only the two IxVM commits onto eea8f5d8.
• Resolved grouped-trace/storage integration and retained both added wide-carry
  fixtures when merging the FFT-pin lists. Measured and reviewed the combined
  grouped system before updating all 81 exact constant pins and the shard pin.
• Fresh Aiur tests: 54 passed, four ignored in each feature configuration,
  including grouped compact/full proof parity, expanded exact trace comparisons
  and the group-member row-count regression. FFI tests pass in both feature
  configurations (67, two ignored); strict combined Clippy and formatting pass.
• First linked integration caught the removed limb helper's stale group entry.
  Review also found main's function/circuit-index mismatch in prover estimates;
  the fix sums group members and has a dedicated regression. Final reruns cover
  both corrections; the earlier successful unit run did not establish them.
• Both Lean executables rebuilt successfully and all three generated Rust
  targets match the emitter. Native full/selected partition integration passes
  with outer compact counters off and on. Grouped/ungrouped small proofs,
  arithmetic/substitution and recursive/aggregation regressions pass: 7,571
  assertion lines in the combined linked log, with no failed assertions.
• The production grouped run passed 927 assertions and failed only its 82 old
  FFT pins. Against main's 79 common constants, 43 improve and 36 regress;
  summed modeled FFT cost changes from 84,477,374,813 to 84,486,051,280
  (+0.0103%). Largest regression: nat_lor_lit, +0.430%; nat_pow_big improves
  25.19%. The shard fixture changes from 6,946,001,069 to 7,008,644,066
  (+0.902%). These reviewed model-cost tradeoffs are not wall-time measurements.
• A second production measurement reproduced all 81 costs and the shard cost
  exactly. It was intended as an ungrouped control, but AiurTestEnv.build
  explicitly applies its groups and does not use the CLI's environment switch;
  it is therefore a repeated grouped run, not evidence of ungrouped/pre-rebase
  parity. No harness behavior was weakened to make that comparison pass.
• Final production rerun with the reviewed exact pins passed: 831 passing
  assertion lines, zero assertion failures, exit status zero. This includes
  all 81 constant cost pins, the shard cost pin, and generated/interpreted
  executor parity. The final validation also rebuilt IxTests successfully
  and reconfirmed the parallel FFI tests (final-validation.log).
• The running FLT result belongs to frozen commit d2d58abd, not to the rebase.
  Function grouping changes circuit layouts, verifying keys and estimated
  proving cost even where execution semantics are unchanged.
  Direct source comparison confirms that all three generated executors, the
  arithmetic/substitution kernel, execution core and native scheduler are
  unchanged by this rebase; that does not substitute for grouped witness and
  estimate validation.

Full FLT run — in progress

• Started September 9 at 15:12:02 UTC on the 64-core / 495 GiB CPU box.
• All 1,330,204 constants passed startup coverage/ownership validation; all
  4,100 original shards are selected, including the four isolated heavy cases.
• Up to 64 execution workers, eight setup workers; 128 GiB accounted-record
  limit, independent 320 GiB/no-swap supervisor ceiling and a 24-hour deadline.
  Compact counters and profiling are off. Admission determines actual concurrency.
• No destination prover budget, selected-subset flag, cached-proof reuse or
  STARK generation. Final success requires every original shard's final
  descendants to pass; a resource abort or supervisor exit is not success.
• Final outcome, total attempts, remaining failures and whole-run measurements:
  pending. Do not publish this as completed full-FLT execution.

Reproduction

Use the pinned development environment and build the CLI/test executable
sequentially, since their Rust archive feature sets differ:

nix develop
lake build ix
lake build IxTests
.lake/build/bin/ix codegen --check
.lake/build/bin/IxTests native-partition
.lake/build/bin/IxTests --ignored ixvm
.lake/build/bin/IxTests aiur-prove
lake exe bench-ixvm-focus --self-test

For full execution, use a complete manifest and fresh report paths. Run this
inside an independently memory/time-bounded supervisor; the environment variable
below limits accounted records, not the entire process:

IX_AIUR_SETUP_THREADS=8 \
IX_AIUR_EXEC_MAX_BYTES=137438953472 \
IX_AIUR_COMPACT_MULTIPLICITIES=0 \
RAYON_NUM_THREADS=64 LEAN_NUM_THREADS=1 \
  .lake/build/bin/ix check --ixe ENV.ixe --ixes FULL.ixes \
    --jobs 64 --keep-going --report report.json --json results.json

See Benchmarks/IxVM/README.md for focused manifests, diagnostic modes,
resource-limit semantics and matched compact/full control procedures.

Review boundaries and follow-ups

• Review native setup/FFI and coverage checks in crates/ffi/src/aiur/check*,
  resource policy in admission*, memory* and protocol.rs, and storage/error
  propagation in crates/aiur/src/{querymap*,execute*}.
• Review arithmetic/substitution source and independent regressions under
  Ix/IxVM/Kernel/ and Tests/Ix/IxVM/, then check generated-source consistency.
• Resource reporting, refined claim ownership and honest/negative proving
  tests are part of the acceptance criteria, not just elapsed-time comparisons.
• Not implemented here: sparse interior substitution projection, profile-driven
  helper inlining, bulk/tail memory tiers, elastic grants, checkpoint/spill,
  exact active-function-row peak estimates or memory-bounded proof construction.
• Full FLT execution is still a rollout gate. Whole-FLT STARK generation and
  aggregate proof verification remain separate work, regardless of its outcome.

[johnchandlerburnham]

!benchmark fresh

[argument-ci-bot]

❌ benchmark run failed

Workflow logs

[johnchandlerburnham]

!benchmark fresh

[argument-ci-bot]

!benchmark — main vs 3e7586a

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 · 7 with regressions · 3 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.047 s	13.037 s	+44.1% (1.44× slower) ⚠️	36.759 s	42.156 s	+14.7% (1.15× slower) ⚠️	75.490	65.830	-12.8% (1.15× slower) ⚠️	73.49 GiB	74.55 GiB	+1.5%	5.06 MiB	5.07 MiB	+0.2%	28.3 ms	32.2 ms	+14.0% (1.14× slower) ⚠️	137.19B	140.31B	+2.3%
Char.ofOrdinal_le_of_le	7.063 s	9.995 s	+41.5% (1.42× slower) ⚠️	31.496 s	35.039 s	+11.2% (1.11× slower) ⚠️	87.720	78.860	-10.1% (1.11× slower) ⚠️	66.16 GiB	66.20 GiB	+0.1%	5.05 MiB	5.07 MiB	+0.5%	28.2 ms	30.3 ms	+7.6% (1.08× slower) ⚠️	105.30B	107.10B	+1.7%
Array.extract_append	6.501 s	9.670 s	+48.7% (1.49× slower) ⚠️	27.171 s	34.886 s	+28.4% (1.28× slower) ⚠️	59.110	46.040	-22.1% (1.28× slower) ⚠️	53.81 GiB	63.85 GiB	+18.7% (1.19× larger) ⚠️	4.92 MiB	4.97 MiB	+1.1%	29.3 ms	30.8 ms	+5.2% (1.05× slower) ⚠️	99.03B	103.13B	+4.1% ⚠️
Std.HashMap	4.117 s	5.661 s	+37.5% (1.38× slower) ⚠️	17.928 s	19.556 s	+9.1% (1.09× slower) ⚠️	113.900	104.420	-8.3% (1.09× slower) ⚠️	37.63 GiB	37.70 GiB	+0.2%	4.97 MiB	5.06 MiB	+1.8%	29.1 ms	28.6 ms	-1.6%	63.51B	64.47B	+1.5%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	3.726 s	5.278 s	+41.7% (1.42× slower) ⚠️	16.597 s	18.746 s	+12.9% (1.13× slower) ⚠️	112.490	99.600	-11.5% (1.13× slower) ⚠️	35.45 GiB	36.10 GiB	+1.8%	4.95 MiB	5.03 MiB	+1.7%	28.1 ms	29.4 ms	+4.6% ⚠️	57.01B	58.23B	+2.1%
String.append	433.3 ms	493.3 ms	+13.8% (1.14× slower) ⚠️	1.779 s	1.892 s	+6.3% (1.06× slower) ⚠️	183.800	172.870	-5.9% (1.06× slower) ⚠️	5.02 GiB	4.57 GiB	-9.0% (1.10× smaller) 🟢	4.70 MiB	4.72 MiB	+0.4%	27.0 ms	26.7 ms	-1.3%	3.51B	3.52B	+0.3%
Nat.add_comm	266.5 ms	261.2 ms	-2.0%	736.3 ms	760.2 ms	+3.2% ⚠️	62.470	60.510	-3.1% ⚠️	3.98 GiB	3.53 GiB	-11.3% (1.13× smaller) 🟢	4.50 MiB	4.50 MiB	+0.1%	25.0 ms	26.2 ms	+4.7% ⚠️	321.32M	321.22M	-0.0%

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.411 s	3.450 s	+43.1% (1.43× slower) ⚠️	21.470 s	22.920 s	+6.8% (1.07× slower) ⚠️	129.250	121.070	-6.3% (1.07× slower) ⚠️	56.05 GiB	54.51 GiB	-2.8%	2.21 MiB	4.00 MiB	+81.1% (1.81× larger) ⚠️	13.0 ms	22.1 ms	+70.3% (1.70× slower) ⚠️	108.59B	106.79B	-1.7%
Char.ofOrdinal_le_of_le	2.383 s	3.435 s	+44.2% (1.44× slower) ⚠️	21.577 s	22.937 s	+6.3% (1.06× slower) ⚠️	128.050	120.460	-5.9% (1.06× slower) ⚠️	56.01 GiB	55.39 GiB	-1.1%	2.21 MiB	4.01 MiB	+81.0% (1.81× larger) ⚠️	13.5 ms	22.7 ms	+68.0% (1.68× slower) ⚠️	107.48B	107.21B	-0.3%
Array.extract_append	2.352 s	3.449 s	+46.7% (1.47× slower) ⚠️	20.717 s	22.554 s	+8.9% (1.09× slower) ⚠️	77.520	71.210	-8.1% (1.09× slower) ⚠️	52.94 GiB	53.48 GiB	+1.0%	2.21 MiB	4.01 MiB	+81.0% (1.81× larger) ⚠️	12.6 ms	22.9 ms	+81.9% (1.82× slower) ⚠️	104.92B	105.52B	+0.6%
Std.HashMap	2.389 s	3.371 s	+41.1% (1.41× slower) ⚠️	21.272 s	21.681 s	+1.9%	95.990	94.190	-1.9%	54.43 GiB	52.13 GiB	-4.2% 🟢	2.22 MiB	4.00 MiB	+80.4% (1.80× larger) ⚠️	12.6 ms	22.0 ms	+74.0% (1.74× slower) ⚠️	105.80B	104.65B	-1.1%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	2.375 s	3.348 s	+41.0% (1.41× slower) ⚠️	20.656 s	22.241 s	+7.7% (1.08× slower) ⚠️	90.380	83.940	-7.1% (1.08× slower) ⚠️	52.84 GiB	52.07 GiB	-1.5%	2.21 MiB	4.01 MiB	+81.7% (1.82× larger) ⚠️	12.6 ms	23.2 ms	+84.5% (1.84× slower) ⚠️	105.31B	104.47B	-0.8%
String.append	2.216 s	3.141 s	+41.8% (1.42× slower) ⚠️	19.855 s	21.253 s	+7.0% (1.07× slower) ⚠️	16.470	15.390	-6.6% (1.07× slower) ⚠️	50.66 GiB	49.96 GiB	-1.4%	2.21 MiB	4.00 MiB	+81.1% (1.81× larger) ⚠️	13.0 ms	23.0 ms	+77.0% (1.77× slower) ⚠️	96.36B	95.07B	-1.3%
Nat.add_comm	2.060 s	2.912 s	+41.3% (1.41× slower) ⚠️	19.867 s	21.075 s	+6.1% (1.06× slower) ⚠️	2.320	2.180	-6.0% (1.06× slower) ⚠️	50.56 GiB	49.91 GiB	-1.3%	2.21 MiB	4.01 MiB	+81.7% (1.82× larger) ⚠️	12.4 ms	24.0 ms	+93.7% (1.94× slower) ⚠️	89.07B	87.78B	-1.4%

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	58.229 s	1m 5.1s	+11.8% (1.12× slower) ⚠️	47.660	42.640	-10.5% (1.12× slower) ⚠️	73.49 GiB	74.55 GiB	+1.5%
Char.ofOrdinal_le_of_le	53.073 s	57.976 s	+9.2% (1.09× slower) ⚠️	52.060	47.660	-8.5% (1.09× slower) ⚠️	66.16 GiB	66.20 GiB	+0.1%
Array.extract_append	47.888 s	57.440 s	+19.9% (1.20× slower) ⚠️	33.540	27.960	-16.6% (1.20× slower) ⚠️	53.81 GiB	63.85 GiB	+18.7% (1.19× larger) ⚠️
Std.HashMap	39.200 s	41.236 s	+5.2% (1.05× slower) ⚠️	52.090	49.520	-4.9% (1.05× slower) ⚠️	54.43 GiB	52.13 GiB	-4.2% 🟢
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq	37.253 s	40.987 s	+10.0% (1.10× slower) ⚠️	50.120	45.550	-9.1% (1.10× slower) ⚠️	52.84 GiB	52.07 GiB	-1.5%
String.append	21.634 s	23.144 s	+7.0% (1.07× slower) ⚠️	15.120	14.130	-6.5% (1.07× slower) ⚠️	50.66 GiB	49.96 GiB	-1.4%
Nat.add_comm	20.603 s	21.835 s	+6.0% (1.06× slower) ⚠️	2.230	2.110	-5.4% (1.06× slower) ⚠️	50.56 GiB	49.91 GiB	-1.3%

Workflow logs