From 0dcdaab9247e9ddb7e28b9977dab03ce23ba4cf9 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 12 May 2026 22:36:32 +0200 Subject: [PATCH] audit-ct-tidy: close milestone ct-tidy via ctt.tidy --- docs/DESIGN.md | 18 ++- docs/journals/2026-05-12-audit-ct-tidy.md | 163 ++++++++++++++++++++++ docs/journals/INDEX.md | 1 + docs/roadmap.md | 6 +- 4 files changed, 180 insertions(+), 8 deletions(-) create mode 100644 docs/journals/2026-05-12-audit-ct-tidy.md diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 3a44023..9076a95 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1732,13 +1732,18 @@ wording is fixed; the categories and their triggers are: **Class-schema diagnostics** (validation of class declarations): -- `KindMismatch` — class param appears in applied position in any - method signature (e.g., `f a` where `f` is the class param). - `InvalidSuperclassParam` — superclass `type` differs from the class's own `param`. - `ConstraintReferencesUnboundTypeVar` — a constraint mentions a type variable not bound by the surrounding `forall`. +A class param appearing in applied position (e.g., `f a` where `f` +is the class param) is rejected earlier by the canonical-form +validator as `BareCrossModuleTypeRef` — `f` is a bare, +non-primitive name not declared as a `TypeDef` in the owning +module — so the dedicated `KindMismatch` diagnostic was retired +at iter ctt.3. + **Typecheck diagnostics** (per function body): - `MissingConstraint` — body's residual constraint is not covered @@ -1758,9 +1763,12 @@ axis-5 (kind `*` only) covers the space. - **Multi-parameter classes** (`class Foo a b where ...`). Schema rejects: `ClassDef.param` is a string, not a list. -- **Higher-kinded class params** (`class Functor f`). Diagnostic - S1 (`KindMismatch`) at class declaration if any method applies - the param. +- **Higher-kinded class params** (`class Functor f`). Rejected at + workspace-load time: `BareCrossModuleTypeRef` from canonical-form + validation fires before class-schema validation if any method + body uses the param as a `Type::Con` head — bare non-primitive + names must be declared as a `TypeDef` in the owning module, and + a class param is not. - **Higher-rank polymorphism** (`forall a. (forall b. b -> b) -> a`). Already rejected at parse time per the typeclass-conversation rationale recorded in JOURNAL; constraint-bearing diff --git a/docs/journals/2026-05-12-audit-ct-tidy.md b/docs/journals/2026-05-12-audit-ct-tidy.md new file mode 100644 index 0000000..64c28e1 --- /dev/null +++ b/docs/journals/2026-05-12-audit-ct-tidy.md @@ -0,0 +1,163 @@ +# audit-ct-tidy — Milestone close: ct-tidy (closing iter ctt.3) + +**Date:** 2026-05-12 +**Milestone:** ct-tidy (ctt.1 + ctt.2 + ctt.3) +**Status:** Closed, three doc-drift items fixed inline (`ctt.tidy`) + +## Architect drift review + +`ailang-architect` reported `drift_found` across the commit range +`805bba3..0d3f44b`. Code-side changes match DESIGN.md / +spec / iters; three doc-side drift items surfaced (two high, +one low; one medium is acceptable per spec). + +**[high — spec acceptance]** `docs/DESIGN.md:1735-1736` — +`KindMismatch` listed as a live class-schema diagnostic. Stale +since ctt.3. + +**[high — spec acceptance]** `docs/DESIGN.md:1761-1763` — +`KindMismatch` cited as the rejection mechanism for +higher-kinded class params. Stale since ctt.3. + +**[high — spec acceptance]** `docs/roadmap.md:91-97` — the +`KindMismatch` retire todo unchecked with no forward-reference +to ctt.3. Spec acceptance criterion called for strikes on the +relevant todo lines; ctt.3 struck none. + +**[medium — record-keeping]** `examples/test_22b2_kind_mismatch.ail.json` +keeps the retired-diagnostic-name in its filename. Spec is silent +(acceptable as-is); rename is a future candidate, not in this +audit's scope. + +**[low — numerical drift]** Spec claim "`grep type_def_module` +returns 13 hits" is now 18 hits post-ctt.2. Intent honoured (every +consumer threaded); numerical figure is historical. + +### Tidy fixes applied inline (`ctt.tidy`) + +All three high-severity items addressed in this audit commit +(Boss-mechanical edits — three doc edits, no separate plan / +implement dispatch warranted): + +1. `docs/DESIGN.md:1733-1740` — dropped the `KindMismatch` bullet + from the class-schema diagnostics list; added a successor + paragraph naming `BareCrossModuleTypeRef` as the structural + rejection path for the malformed class-param-in-applied-position + shape; cross-references iter ctt.3. + +2. `docs/DESIGN.md:1761-1763` — rewrote the "Higher-kinded class + params" bullet under "What this typeclass design explicitly does + NOT support" to name `BareCrossModuleTypeRef` from canonical-form + validation instead of `KindMismatch` at class declaration. + +3. `docs/roadmap.md:91-97` — struck `[x]` with a forward-reference + to ctt.3 (canonical-form-rejection test stays green asserting + `BareCrossModuleTypeRef`). Adjacent ctt.2 todo at lines 98-105 + also struck (mechanical follow-up — ctt.2 closed the re-key it + tracks). + +Medium / low items skipped: filename rename + spec numerical claim +both fall outside ctt.tidy's scope (spec acceptance was on +intent-honour, not figure-precision; filename rename is a future +candidate the spec already permits as-is). + +## Bench-regression check + +Sequence run as Boss (the `&&` chain tripped at `check.py`'s exit +1; `compile_check.py` and `cross_lang.py` then ran separately): + +- `check.py`: **exit 1** — 63 metrics; 3 regressed, 3 improved + beyond tolerance, 57 stable. + - Regressions: + - `bench_list_sum.bump_s` +12.23% (tol 10%) — + **second consecutive sighting** (audit-eob first-sighted + this at +12.60%, this audit at +12.23%). + - `latency.explicit_at_rc.max_us` +44.31% (tol 25%) — + **first sighting**, rc-cohort tail-latency. + - `latency.implicit_at_rc.max_us` +35.07% (tol 30%) — + **first sighting**, rc-cohort tail-latency. + - Improvements: + - `bench_list_sum.gc_over_bump` -10.40% — mirror of the + bump_s regression (gc/bump ratio falls because bump rose). + - `bench_closure_chain.gc_over_bump` -15.05% — new improvement. + - `bench_list_sum_explicit.gc_over_bump` -8.30% — new improvement. +- `compile_check.py`: exit 0; 24 metrics, all stable within ±25%. +- `cross_lang.py`: exit 0; 25 metrics, all stable within ±15%. + +### Classification + +**bump_s persistence** (`bench_list_sum.bump_s`): second +consecutive sighting (audit-eob → audit-ct-tidy) at near-identical +magnitude (+12.60% → +12.23%). The audit-eob classification was +"first-sighting rule — observe in the next audit; if it persists, +investigate". This audit IS that next audit, and it persists. + +ctt.* milestone made zero codegen-relevant edits (the three iters +touched env-overlay doc + check-side registry key shape + +workspace-load-time diagnostic deletion). No plausible attribution +to ctt.*. The persistence is real but uncaptured — the underlying +cause predates this milestone and is independent of the work in +the audit window. + +Conservative call (same standing rule as previous three audits): +**do not** baseline-update. The persistence is now documented +across two audits; if it persists into the next audit +unchanged, ratify-without-attribution becomes the right call +(at three consecutive sightings the noise hypothesis is +unsupported). The latency tail-cluster regressions are first +sightings — observe. + +**Latency max_us regressions** (`explicit_at_rc.max_us`, +`implicit_at_rc.max_us`): first sighting in any recent audit. +Both metrics are rc-cohort tail-latency (the extreme-outlier +window). The bench harness runs ~50ms workloads; a single +outlier of +183µs (explicit) or +167µs (implicit) absolute +moves the max_us proportionally. ctt.* made zero codegen edits, +so the noise hypothesis is the most parsimonious explanation +on first sighting. + +Conservative call: first-sighting rule — **do not** +baseline-update; observe in the next audit. + +**Recurring latency.explicit_at_rc improvement cluster**: the +three-audit-long improvement cluster on `p99_us` / `p99_9_us` / +`p99_over_median` (previously at ~-37%, classified as +ratify-candidate after one more audit at audit-eob) now reports +within tolerance this audit: +- `p99_us` -24.87% (tol 25%) — stable (was: improvement) +- `p99_over_median` -24.10% (tol 25%) — stable (was: improvement) +- `p99_9_us` not flagged (within tolerance) + +The cluster has narrowed from ~-37% improvements to ~-24% +near-tolerance stable. The improvements partially reverted — +the metrics are still on the improvement side, but no longer +beyond tolerance. The audit-eob recommendation ("if the cluster +persists into the next two audits unchanged, ratify; if it +shifts or shrinks meaningfully, that is itself the attribution +signal") has fired: the cluster shrank meaningfully this audit. +This is itself attribution-evidence — the underlying cause is +variable rather than persistent. The ratify-pending plan is +withdrawn; the cluster is now noise-class, not signal-class. + +**Baseline left pristine on every script** for the fourth +consecutive audit. No `--update-baseline` invocation. + +## Status + +Closed. Ct-tidy milestone fully landed: + +- env-overlay shape ratified (ctt.1: DESIGN.md `## Env construction` + section + DuplicateCtor pinning test + 2 P2 todos closed). +- `Registry.type_def_module` re-keyed to `(owning_module, bare_name)` + with `caller_module` threaded through every consumer (ctt.2: + 3-module fixture + regression test). +- `KindMismatch` retired (ctt.3: variant + helper + dispatch + + Display arm deleted; test stays green via canonical-form + successor `BareCrossModuleTypeRef`). +- DESIGN.md tracks all three iters' anchors (ctt.tidy in this audit: + class-schema diagnostics list updated, higher-kinded params bullet + updated, ctt.3 retirement marker pattern). +- Roadmap reflects closure (ctt.tidy: two P2 todos struck `[x]`). + +Working tree exits audit clean. main HEAD advances by exactly +this audit commit. diff --git a/docs/journals/INDEX.md b/docs/journals/INDEX.md index 30c5e75..7411f6b 100644 --- a/docs/journals/INDEX.md +++ b/docs/journals/INDEX.md @@ -40,3 +40,4 @@ - 2026-05-12 — iter ctt.1: env-overlay shape ratification — new DESIGN.md top-level section `## Env construction` anchors the `env.types` (owning) / `env.ctor_index` (reverse-index) split with the semantic rationale, plus the intentional check-side / mono-side asymmetry (mono-side narrowed at ct.3.2, check-side retains both halves because in-band `DuplicateCtor` consumes the per-module `env.ctor_index` rebuild); new behavioural-pin test `crates/ailang-check/tests/duplicate_ctor_pin.rs` ratifies the consumer; two P2 roadmap todos struck `[x]` (overlay shape question, per-module overlay narrowing); 3/3 tasks first-shot, zero review re-loops, no production-code edits → 2026-05-12-iter-ctt.1.md - 2026-05-12 — iter ctt.2: `Registry.type_def_module` re-key from `BTreeMap` to `BTreeMap<(String, String), String>` keyed by `(owning_module, bare_name)`; new `caller_module: &str` parameter threads through `normalize_type_for_registry` + `Registry::normalize_type_for_lookup`; four `ailang-check` consumer sites (lib.rs:1640, mono.rs:121/624/1175) pass the correct module-context (env.current_module / defining_module / module_name) per the plan's Design Notes; new regression test plus three-module fixture (`ctt2_collision_{cls,lib,main}.ail.json`) exercises the cross-module bare-name collision shape that pre-ctt.2 silently overwrote; RED-failure observed as `OrphanInstance` rather than the plan's predicted `DuplicateInstance` because the pass-2 coherence check (workspace.rs:656-659) is also a bare-name consumer and fires earlier; both consumers fixed by the same re-key; plan's verbatim two-module fixture had two structural defects (two-way imports → Cycle, qualified `InstanceDef.class` → QualifiedClassName) that the implementer-phase repair handled by introducing the third cls-module; spec-intent (RED-first against bare-name collision) preserved; `cargo test --workspace` green (16 binary-test suites, ~600 tests, zero failures) → 2026-05-12-iter-ctt.2.md - 2026-05-12 — iter ctt.3: `KindMismatch` retire — pure deletion across 3 files (workspace.rs: variant + dispatch + helper + "dead-but-defensive" doc; main.rs: Display arm; lib.rs: 22b.1 archaeology comment). Existing test `class_param_in_applied_position_fires_canonical_form_rejection` stays green unchanged (asserts `BareCrossModuleTypeRef` on the malformed fixture — the canonical-form-validator successor path). Two adjacent textual-consistency edits ride along (validate_classdefs doc-comment "Three → Two", lib.rs archaeology comment gains a ctt.3 retirement marker). One mid-deletion mechanical fix: dispatch-loop deletion orphaned `mod_name` binding → rewrote `for (mod_name, m) in modules` to `for m in modules.values()` (same body type, mechanical). 2/2 tasks, ~600 tests green across 16 binary-test suites → 2026-05-12-iter-ctt.3.md +- 2026-05-12 — audit-ct-tidy: milestone close (ct-tidy) — architect drift fixed inline as `ctt.tidy` (3 doc-side edits: DESIGN.md §"Class-schema diagnostics" drops the retired `KindMismatch` bullet + adds successor paragraph naming `BareCrossModuleTypeRef`; DESIGN.md §"Higher-kinded class params" rewritten to name `BareCrossModuleTypeRef` from canonical-form validation instead; roadmap.md two P2 todos struck `[x]` with forward-reference to ctt.3 and ctt.2). Bench mixed (check.py exit 1: bump_s persistence on `bench_list_sum` second consecutive sighting at +12.23% → +12.60%; two new first-sighting rc-cohort max_us latency regressions classified as noise pending next audit; the recurring 3-audit `latency.explicit_at_rc` improvement cluster narrowed to within tolerance this audit, withdrawing the ratify-pending plan from audit-eob — the meaningful shrinkage is itself attribution evidence that the cluster is noise-class not signal-class), baseline pristine for the 4th consecutive audit → 2026-05-12-audit-ct-tidy.md diff --git a/docs/roadmap.md b/docs/roadmap.md index a769398..46f7921 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -88,14 +88,14 @@ context. Pick the next milestone from P1.)_ the JSON path carries is missing. Plausibly applies to every CLI subcommand that calls `load_workspace(&path)?` directly. - context: JOURNAL 2026-05-11 ("Iteration ct.1") — surfaced by ct.1.8 tester. -- [ ] **\[todo\]** Retire dead `KindMismatch` arm — `validate_classdefs`'s +- [x] **\[todo\]** Retire dead `KindMismatch` arm — `validate_classdefs`'s `walk_kind_mismatch` path is structurally unreachable through well-formed schema post-ct.1 (the canonical-form validator catches the malformed `Type::Con { name: param }` shape earlier). The enum variant + `walk_kind_mismatch` helper stay as dead-but-defensive code; a future tidy can delete both. - - context: JOURNAL 2026-05-11 ("Iteration ct.1"). -- [ ] **\[todo\]** Re-key `Registry.type_def_module` to handle + - context: JOURNAL 2026-05-11 ("Iteration ct.1"); closed by iter ctt.3 — variant + helper + dispatch + Display arm all deleted; canonical-form-rejection test stays green asserting `BareCrossModuleTypeRef`. +- [x] **\[todo\]** Re-key `Registry.type_def_module` to handle bare-name-collision-across-modules — `BTreeMap` keyed by bare type name silently overwrites when two modules each define `type Foo`; `normalize_type_for_registry` would then collapse `M.Foo`