[MicroProofs]

Summary

Third and last part of plan 08 (plans/08-optimizer.md). This PR completes Chunks 6, 9, 10 and 11, adds a new Chunk 12 (application fusion, native packing and late UPLC cleanup), and lands the first chunk of the new plan 15 (plans/15-o2-optimizer.md): silent O2. Twelve commits, eight changesets. SPEC.md marks plan 08 complete and plan 15 partial.

Behavior changes:

• The default O1 pipeline does more work, so the generated UPLC changes for every project. -O0 output is unchanged.
• nash build and nash test accept -O2 / --optimize 2, and nash.jsonc accepts "optimize": 2. O2 is never the default.
• O2 removes trace message computations even when they fail or diverge. A program that fails inside a trace message under O0/O1 can return a value under O2.
• The language adds read-only .fst and .snd access for known builtin pair types.

Versioning: minor bumps for nash-codegen, nash-solve, nash-config, nash-driver and nash-cli; patch for nash-ir, nash-report and nash-plutus. See .sampo/changesets/.

Post-ANF placement (perf(codegen): run constructor and inverse folding only after ANF)

• The early known_case::reduce_constr and inverse::reduce calls before ANF are removed.
• Constructor folding and representation cancellation now run only in the post-ANF cleanup loops. Those loops already follow bindings that codegen produces and opportunities that inlining exposes.
• The 23 source and validator performance rows are unchanged. The baseline records the regressions in synthetic direct-expression cases.

Constant builtin evaluation, Chunk 9

• Integration (integrate bounded constant folding into O1). New nash-ir::constant_fold pass with a callback that codegen supplies, so nash-ir stays independent of codegen. It folds saturated builtin calls with literal arguments through ANF bindings, then repeats cleanup.
• Limits removed (fold and clean up to an unbudgeted fixed point). The 128-attempt cap, the per-call CPU and memory allowance, the payload byte, node and depth gates, the allowlist and the Flat growth gate are gone. Every pure, representable, successful call folds. The loop stops only when folding and cleanup both leave Core unchanged.
• A runtime failure leaves the original call in place. It never becomes a compile error. Invalid constants and unsafe large negative Data literals also stay as runtime calls.
• nash-plutus adds eval_constant_builtin, a direct evaluator with no budget. Out-of-range constant indices and constructor tags now return errors instead of a panic. Whole-byte left shifts are corrected, and shift, rotate and list-drop accept arbitrary-size inputs.
• O0 and explicit comptime keep their existing policies.

Pair projection and pair access, Chunk 10

• Restricted pair cancellation (cancel single-field constructor pair cases). New nash-ir::pair_projection. A one-branch CaseKind::Pair becomes a fstPair / sndPair projection only when constructor inverse cleanup then removes that projection. Producer bindings stay strict. The general projection rule from the trial is not adopted.
• Typed .fst / .snd (add typed fst and snd pair access). p.fst, p.snd and the accessor functions .fst, .snd resolve for known builtin pair types and their aliases, and lower directly to the pair builtins. The receiver type must be known. Records with fields named fst or snd keep ordinary record semantics. Record update and record patterns on pairs are rejected with pair-specific diagnostics. docs/syntax.md has the new section.

Recursive unused parameters, Chunk 6 (remove unused recursive parameters before ANF)

• nash-ir::unused_params now handles self-recursive and mutually recursive groups, after static lifting and before the single ANF pass.
• Liveness starts at real uses and propagates backward through bare-variable forwarding until stable. Forwarding alone does not keep a parameter live.
• Non-atomic arguments stay evaluated in source order at entry calls and recursive calls. A partial, escaping or oversaturated use, or an unsupported type view, leaves the whole group unchanged.
• All-unused workers become delayed recursive values. Recursion lowering and dead-member cleanup support mutual groups that contain such workers.

Composition and convergence, Chunk 11

• Review (complete optimizer composition and convergence review). Five regression tests: a mixed cleanup pipeline with phase, type and hygiene evidence; a same-node-count rewrite that exposes more cleanup; a reachable recursive cycle rendered without evaluation; cleanup-exposed signature removal; and a 130-call fixture that reaches a folding fixed point.
• Joint fixed point (revisit static lifting after cleanup). Static lifting, unused-parameter removal, constant folding and cleanup now repeat together until Core pointers are unchanged. Before this, a second O1 run could still remove work: cleanupExposesStatic gave 46 Flat bytes after one run and 39 after two. One run now gives 39.
• All-static oversaturated self-calls bind the forced worker result before the extra arguments, so call operands stay atomic.
• ANF still runs exactly once. The shared fixture harness checks that a second O1 run produces identical closed Flat output, after it renders the snapshot.

Application fusion, native packing and late UPLC cleanup, Chunk 12 (fuse O1 applications and clean up late UPLC)

All three are O1 rules. They preserve enabled traces, failure and termination.

• Fusion. single_use::inline turns let p = f a in p b into f a b when p has one direct use, the operands are atomic and the intermediate type views agree.
• Late cleanup. New nash-codegen::uplc_optimizer. It removes identity applications without dropping argument evaluation, substitutes single-use values, removes unused value bindings and cancels direct force/delay pairs. Substitution rejects possible name capture. Recursive self-application is never unfolded.
• Native packing. An application spine becomes Case(Constr(0, args), [function]) when the function and all arguments are UPLC values. Packing starts at three arguments, which is the first arity where the two native nodes replace more Apply nodes.
• lower::lower_optimized is the common O1 entry point for production, shared snapshots, source tests and performance checks. O0 and the isolated sharing APIs are unchanged.

Silent O2, plan 15 Chunk 2 (add silent O2 compilation and trace erasure)

• New nash-codegen::silent pass and optimizer::optimize_silent. O2 erases every Core trace operation, then runs the O1 pipeline.
• Erasure covers CoreKind::Trace and direct Builtin.Trace in saturated, partial, aliased and first-class positions. A bare builtin reference becomes a typed no-log function. The value that a trace returns still evaluates, and work outside the trace stays strict.
• nash-config adds OptimizationLevel::O2 and Build::validate. O2 with compact or verbose tracing, or with compiler traces, is an error (BuildConflict) in project config and after CLI overrides.
• nash test defaults to verbose traces under O0/O1 and to silent under O2. Runner status reporting is not affected.
• docs/cli.md and docs/codegen.md describe the level and the erasure boundary.

Tests and measurements

• 501 snapshot files change: 183 added, 317 modified, 1 renamed. Changed snapshots keep their original O0 sections.
• tools/optimizer-perf/baseline.json grows from 108 to 199 rows and from 10 to 13 sources. All 199 cases produce identical O1 code after one, two and three runs.
• Recorded results, from the research notes:

Change	Case	Flat bytes	CPU
Constant folding	108-row baseline	26 rows improve, 82 unchanged
Pair cancellation	source decoding	94 → 45	1,681,280 → 878,161
Recursive parameters	mutual source	93 → 81	3,196,554 → 2,876,554
Joint fixed point	cleanupExposesStatic	46 → 39	2,161,056 → 1,921,056
Fusion and packing	staged call	53 → 50	2,278,264 → 2,166,264
O2	aliased builtin trace loop	57 → 39	2,643,550 → 1,921,056

• New research notes under docs/research/: constant-fold-trial.md, pair-projection-trial.md, recursive-parameters.md, optimizer-convergence.md, application-packing-trial.md and o2-silence-trial.md. Raw trial reports are in tools/optimizer-perf/trials/.

Not in this PR

• Plan 15 Chunks 3 to 5: known-arity grouping, lambda and binding movement, and the O2 composition review.
• Any trace-dependent rewrite beyond erasure. O2 is erasure followed by O1.
• Plan 14 (explicit Big constructor tags).

Test plan

The last commit records 3,896 passing workspace tests, strict Clippy on the repository and on the performance workspace, and 199 matching performance cases.

• cargo fmt --all -- --check
• cargo clippy --all-targets --all-features -- -D warnings
• cargo nextest run --workspace
• cargo check --manifest-path tools/optimizer-perf/Cargo.toml
• Manual CLI check of nash build -O2 and nash test -O2, because automated tests call the Rust APIs and do not launch the binary