Skip to content

feat: plan 07 codegen - #22

Merged
MicroProofs merged 14 commits into
mainfrom
plan-7
Sep 14, 2026
Merged

MicroProofs merged 14 commits into
mainfrom
plan-7

Conversation

@MicroProofs

Copy link
Copy Markdown
Contributor

Summary

Implements plan 07 (plans/07-codegen.md): two new crates, nash-ir (Core IR) and nash-codegen (Can -> Core -> UPLC), plus the minimum Plan 09 hooks needed to run validators end to end (nash build). Fourteen commits: three research docs, one design doc, two frontend commits, three codegen commits, one build commit, two diagnostic fixes, two snapshot-hygiene commits, one changeset commit.

Versioning: seven changesets. Minor bumps for nash-ast, nash-can, nash-constrain, nash-solve, nash-plutus, nash-ir, nash-codegen, nash-driver, nash-report, nash-cli; patch for nash-nitpick and nash-parse. See .sampo/changesets/codegen-*.md and diagnostic-*.md.

Design (docs(codegen): define specialization identity, docs/research/*)

  • Three research notes assess substitution-based inference, trait dictionaries versus specialization, and higher-rank versus higher-kinded polymorphism. Outcome: keep union-find inference; compile-time specialization only, no runtime dictionaries.
  • docs/codegen.md specifies specialization identity: lexical definition identity + executable trait evidence + demanded runtime layouts. Complete substitutions are metadata, not key material. Layout demand propagates to a fixed point. Codegen diagnoses growing layouts as a resource error rather than looping. Trait-free polymorphic recursion through opaque values gets one body with Ty::Erased.

Frontend (feat(solve), feat(frontend))

  • Solver publishes solved types for every canonical expression and pattern, in the owning scheme's type-variable scope. Covers annotated branches, alias patterns, nested scopes, recursive definitions and higher-kinded partial aliases.
  • assert, fail, todo, trace and comptime canonicalize and type-check with source locations, dependency tracking and nitpick coverage.

Codegen (feat(codegen): add executable Core foundation, feat(codegen): specialize source into UPLC)

  • nash-ir: Core IR with explicit representations (Big / Const / Term / Erased), builders, exhaustive traversal helpers, pretty printer.
  • nash-plutus: UPLC text printer with lexical DeBruijn names, checked Name -> DeBruijn, complete DefaultFunction inventory, Flat encoding, single-wrapped CBOR.
  • nash-codegen: Can -> Core lowering (can_to_core), lazy one-level ADT layout conversion (ty_of), complete Builtin mapping with force/arity checks, shared Maranget decision trees for little ADTs / tuples / native lists / Data patterns, checked Data casts with recursive validation, nominal records and labeled constructor layouts with scoped accessor sharing (decoders stay lazy in unselected branches), self and mutual recursion rewriting with static-argument handling, evidence normalization (Given, Super, defaults, ReflexiveLift, StructuralEq), layout-demand analysis, finite specialization worklist with explicit body/type-depth and work limits, trace levels, bounded comptime evaluation, reachable program assembly.
  • Generalized local values that need evidence or native layout are compile-time templates evaluated per specialization; other locals stay strict. Strict nullary recursive values are diagnosed.
  • Tests: focused semantic assertions on the CEK machine plus Core / UPLC / budget snapshots.

Build (feat(build): emit validator scripts and close plan 07)

  • Driver build_with(db, graph, origins, finish) retains solved module tables until the finish callback returns; failed frontend builds do not invoke it. check_main_parameters runs after solving; validator entry-point diagnostics added.
  • nash build [PATH] --out build --trace-level silent|compact|verbose --compiler-traces compiles every validator module to Plutus V3 .uplc, .flat and .cbor (one CBOR byte string wrapping the Flat bytes). No optimizer yet.
  • examples/vesting/: Vesting and parameterized VestingParam with a test-only Cardano.Tx context. Fixtures cover successful and failed claims and cancellations and record unoptimized budgets: claim 6,719,849 CPU / 28,411 mem; cancel 6,909,610 / 29,381; parameterized 6,933,057 / 29,113 and 6,957,610 / 29,681.
  • plans/09-validators-build.md records what was brought forward; Plan 09 is not marked complete.

Diagnostics (fix(report), fix(cli), test: …)

  • Terminal output keeps miette diagnostic codes and error/warning markers. Source paths render relative to the workspace or package root; file hyperlinks stay absolute. JSON and LSP keep absolute identities.
  • Colorless rendered-diagnostic snapshots expanded across parser, canonicalizer, solver, driver and CLI. Source-driven snapshots record Nash source instead of Rust assertion text; codegen snapshots moved to source-compilation tests; snapshot_hygiene.rs checks snapshot metadata.

Deferred

  • Optimizer, --optimize: Plan 08.
  • Config defaults, other target versions, script hashes, stale-output removal: Plan 09.
  • Power-assert rewriting in test bodies: Plan 10.
  • BigField node for optimizer reasoning about Big record access, if needed.

Test plan

  • cargo fmt --all -- --check
  • cargo clippy --all-targets --all-features -- -D warnings
  • cargo insta test --workspace --check --unreferenced reject — 3,180 passed, 0 failed, 3 ignored; no pending or unreferenced snapshots
  • cargo run -p nash-cli -- check tests/core — 23 modules, 215 declarations
  • cargo run -p nash-cli -- build examples/vesting --trace-level verbose --compiler-traces — 25 modules, Vesting 603 Flat bytes, VestingParam 608 Flat bytes, all six output files written
  • crates/nash-codegen/tests/vesting.rs and crates/nash-driver/tests/vesting.rs: eight fixture outcomes, Flat/text round trips, rejection of Term validator parameters
  • 157 scratch projects match expectations: 37 pass, 120 expected failures (per plan record)
  • Each intermediate commit passed fmt, strict clippy and workspace tests

https://claude.ai/code/session_01ScuAeUCfNGXAznfEEKDH1X

Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
Signed-off-by: microproofs <kwhitemsg@gmail.com>
@MicroProofs
MicroProofs merged commit 3cb7a0f into main Sep 14, 2026
9 checks passed
@MicroProofs
MicroProofs deleted the plan-7 branch September 14, 2026 05:57
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant