Skip to content

refactor: plan 6.5 frontend hardening and concise diagnostics - #20

Merged
MicroProofs merged 11 commits into
mainfrom
clean-up-plan-6.5
Sep 10, 2026
Merged

refactor: plan 6.5 frontend hardening and concise diagnostics#20
MicroProofs merged 11 commits into
mainfrom
clean-up-plan-6.5

Conversation

@MicroProofs

Copy link
Copy Markdown
Contributor

Summary

Plan 6.5: frontend hardening before Plan 07, plus the concise-diagnostics refactor. Two plan files: plans/frontend-hardening.md (eight chunks, one commit each) and plans/diagnostics-refactor.md (two commits). Verification record: docs/frontend-hardening-verification.md. Eleven commits, one per verified chunk.

Net: 801 files, +11,254 / −13,203. Production Rust across the inference pipeline drops from 21,208 to 20,574 lines; the Constraint tree and the intermediate inference Type are gone.

Versioning: nine changesets. Minor bumps for nash-region, nash-source, nash-parse, nash-can, nash-constrain, nash-solve, nash-driver, nash-report, nash-language-server, nash-cli; patch bumps where a crate is only touched incidentally. See .sampo/changesets/.

Parser (perf(parse), fix(parse) ×3)

  • Accumulator copies removed. Function application and operator chains append one parsed argument instead of copying the accumulated list. Arena retention for 1,000 / 2,000 / 4,000 operands: 4.19 MB / 16.8 MB / — before; 261 KB / 523 KB / 1.05 MB after (with the wider Region). Growth is linear. Regression test checks operand count, full consumption and bounded growth.
  • UTF-8 at the boundary. Parser::new(&bump, src: &str). All seven unchecked UTF-8 conversions replaced with checked ones. A compile-fail doctest rejects byte input. Snapshots for raw Unicode, mixed Unicode/escapes, CRLF normalization.
  • Source-sized coordinates. Region uses usize, bounded by the source allocation (isize::MAX), so no fallible constructor. Region grows from 8 to 32 bytes on 64-bit hosts; CLAUDE.md updated. LSP checks its 32-bit limit explicitly instead of truncating. Oversized Unicode escapes saturate as an invalid-code marker without integer overflow. Positions beyond 65,535 covered by CLI JSON tests.
  • Bounded nesting. At most 64 simultaneous recursive expression/pattern/type entries. Exhaustion is committed across backtracking and reports EXCESSIVE NESTING at the first exhausted position. Flat sequences (access chains, lambda arguments, else-if, let definitions, case arms, union variants) and nested comments iterate. 512 parentheses previously aborted on a 2 MiB stack; tests run on that stack in debug and release.

Driver, canonicalizer, solver (refactor(driver), refactor(can), perf(types), refactor(types))

  • Interface cache removed. InterfaceCache, ModuleMeta, load/save, serde derives and the cache-only error had no active caller. bincode leaves the workspace. In-memory Interface/Export and fingerprint tests remain.
  • Borrowed local scopes. Five scope entry points borrow module data and binding maps through a parent chain instead of cloning the whole Env. Shadowing, let-group visibility, free-variable bookkeeping and sorted suggestions unchanged; three baseline snapshots captured against the old implementation.
  • Bounded trait lookup. Selection, evidence, entailment and missing-impl suggestions share one ordered ImplKey range helper (start at the trait with an empty head, stop when the trait changes). Equivalence regression compares every candidate key and payload against the old full-map filter across 18 combinations.
  • Direct AST inference. nash-solve/src/solve/{infer,expressions,patterns}.rs infer straight from the canonical AST into the existing union-find and predicate engine. nash-constrain keeps union-find types, canonical instantiation and error types; expression.rs, pattern.rs, module.rs and the constraint tree are deleted. The driver passes the canonical module to the solver. Preserved: ranks, generalization, recursive groups, annotations, aliases, higher-kinded applications, representation predicates, deferred fields, ordered diagnostics, independent-error recovery, SolvedTypes/evidence contracts.
    • Differential audit: 426 complete records match the original engine byte for byte (all 411 originals plus new fixtures); only pointer NodeIds and unordered map iteration normalized. Twenty-two extra probes match.
    • Seven new recovery regressions (recursive occurs-check timing, separate annotated-branch expectations, Cons tail expectations, canonical alias headers) failed against the first direct implementation and pass now; their snapshots come from the original engine.
    • Adoption gates met: behavioral parity, net production-code reduction (−634 lines), no dual engines.

Diagnostics (refactor(report), refactor(syntax))

  • Fixed snippet shapes replaced with arbitrary source labels and related reports across files. code/snippet.rs deleted.
  • Stable diagnostic codes independent of display titles. LSP uses them.
  • Expectation origins retained and labelled (annotation, earlier element or branch). Opening delimiters labelled for missing or wrong closers, including underindented closers and comments.
  • Syntax, naming, type, pattern and warning prose rewritten concise: expected/actual types, at most one hint. Type diffs retained.
  • JSON gains code, severity, labels, suggestions, related. Messages no longer embed source drawings; consumers render the labels. docs/diagnostics.md rewritten.

Docs

  • docs/overview.md, docs/traits.md, SPEC.md describe the direct-inference pipeline, coordinate rules, scope borrowing and nesting limit. plans/06-diagnostics.md links the refactor.

Deferred

  • Plan 07 untouched.
  • Region at 32 bytes is accepted; a compact representation is possible later if AST size matters.

Test plan

  • cargo fmt --all -- --check
  • cargo clippy --all-targets --all-features -- -D warnings
  • cargo insta test --workspace --check --unreferenced reject — 2,968 passed, 0 failed, 3 ignored; no pending or unreferenced snapshots
  • cargo run -p nash-cli -- check tests/core — 23 modules, 215 declarations
  • cargo test --release -p nash-parse — Unicode/escapes, coordinates beyond 65,535, lookahead, oversized escapes, nesting on a 2 MiB stack, long flat sequences (per verification record)
  • Parser allocation probes in debug and release
  • Inference differential audit: 426/426 records match; two original-engine runs identical
  • Trait-lookup equivalence regression against the old filter
  • Seven negative CLI scratch projects keep their diagnostics; qualified recursive-group project compiles
  • Each intermediate commit passed fmt, workspace check, strict clippy and full tests

https://claude.ai/code/session_01ScuAeUCfNGXAznfEEKDH1X

Signed-off-by: microproofs <kwhitemsg@gmail.com>
Accept str instead of arbitrary byte buffers. Checked conversions prevent invalid string creation through the safe parser API.

Signed-off-by: microproofs <kwhitemsg@gmail.com>
Use source-sized coordinates and checked protocol conversion. Preserve full diagnostic widths and reject Unicode code overflow.

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 e3e72a7 into main Sep 10, 2026
9 checks passed
@MicroProofs
MicroProofs deleted the clean-up-plan-6.5 branch September 10, 2026 23:49
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