[MicroProofs]

Summary

Second part of plan 08 (plans/08-optimizer.md). This PR completes the retained scope of Chunk 7 (known-case and field simplification), adds the Chunk 8 representation cancellation, and connects the accepted pipeline to production assembly. Twenty commits, seven changesets.

Behavior change: nash build and nash test now default to trace-preserving O1, so the generated UPLC changes for every project. -O0 keeps the baseline lowering that builds used before.

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

Known-case folding, Chunk 7

Each rule landed as an isolated trial commit, then as an adoption commit that adds it to the shared pipeline. Malformed branch tables and unknown subjects stay unchanged in every rule.

• Let-bound native constructors (trial bound constructor case folding, adopt bound constructor folding). The pass tracks constructor bindings and their variable aliases. Non-variable fields get one name at the construction site, and matching branches receive aliases to them. The constructor stays until ordinary cleanup proves it unused, so escaping values and repeated matches work. Strict fields stay evaluated once, in source order.
• Native lists (trial and adopt native list case folding). Covers literal ProtoList subjects and exactly saturated MkCons values. MkCons stays strict at its original position, because the builtin also checks the runtime shapes of its operands.
• Literal Data (trial and adopt literal Data case folding). Selects DataI, DataB, DataList, DataMap or DataConstr for Constant::Data subjects and their aliases. This is shape selection, not wrap and unwrap cancellation.
• Data producers (Data wrapper, collection Data and ConstrData case folding). Folds cases on values built by saturated IData, BData, ListData, MapData and ConstrData calls.
• Constructor fields (fold fields of known native constructors). Folds field accesses on known native constructors. Strict field evaluation, escaping values and malformed runtime shapes are preserved.
• Integer and byte cases (fold known integer and byte cases). Folds known native integer and byte case subjects. Invalid tables and runtime failures are preserved.

Representation cancellation, Chunk 8

• New nash-ir::inverse pass (trial direct integer representation cancellation, cancel proven representation round trips).
• It cancels integer, byte, list and map Data round trips and UTF-8 round trips. A cancellation needs structural runtime-shape evidence; the reverse direction needs the precise Data variant or valid UTF-8.
• Let-bound operands stay at their original evaluation point. Constructor Data projections and reconstruction reuse variables through retained strict bindings, so all tag, field and variant checks stay.
• The pass runs before ANF and again in the O1 cleanup loop.

O1 as the default (feat(codegen): default builds and tests to trace-preserving O1)

• crates/nash-codegen/src/optimizer.rs holds the production O1 pipeline. Snapshots (tests/support/optimizer.rs) and tools/optimizer-perf now render and measure this same pipeline instead of a test-only copy.
• nash-config adds OptimizationLevel (O0, O1; default O1) and the optimize project field, which accepts 0 or 1.
• nash build and nash test accept -O0, -O1 and --optimize 0|1. The CLI option overrides the project configuration.
• O1 keeps all enabled user and compiler traces and their order. It does not enable or disable traces.
• O0 uses lower. O1 uses lower_with_constant_sharing. Explicit comptime evaluation stays on O0 with its existing budget semantics.
• docs/cli.md, docs/codegen.md, docs/overview.md, docs/testing.md and SPEC.md are updated to match.

Stack safety (fix(codegen): use heap work lists throughout assembly, fix(ir): print Core with heap work lists)

• Default O1 exposed a stack overflow in the driver ledger_contexts fixture.
• Core walk and map, occurrence and free-variable analysis, hygiene, ANF, beta splicing, recursion rewriting, lowering, constant sharing, De Bruijn conversion and target validation now use heap work lists. This applies to O0 and O1. Assembly does not enlarge the thread stack.
• The UPLC term printer and the Core term printer also use explicit work lists.
• docs/research/compiler-stack-audit.md records the reproduced failures and the recursive paths that are still open.

Tests and measurements (refactor(test): consolidate optimizer coverage)

• Codegen optimizer tests are grouped by pass. known_case.rs holds the Boolean, constructor, list and Data suites. dead_code.rs holds the binding and recursive reachability suites. unused_params.rs is one pre-ANF suite. inverse.rs is new.
• 683 snapshot files change: 528 added, 71 modified, 84 removed. The consolidation moved snapshots between modules.
• tools/optimizer-perf/baseline.json grows from 23 to 108 rows. The 85 new rows are representation cancellation cases shared with the semantic tests.

Not in this PR

• Recursive unused-parameter removal.
• Chunk 9 (constant builtin evaluation) and Chunk 10 (single-field native pair projection).
• The Chunk 11 final composition and convergence review.
• The remaining stack audit candidates: flat source chains, IR type metadata, nested constants, module graph cycles and type unification.

Test plan

• 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