mir.5 is the typed-MIR milestone's closing iteration. Its CODE half had
already converged before the iteration began, so mir.5 ships no code —
it ratifies into the design/ ledger the boundary the code already holds.
Verified at iteration entry (empirically, not from the spec sketch):
- all four named re-derivers grep-clean in codegen: synth_with_extras,
synth_arg_type, type_home_module, the second infer_module_with_cross;
- lower_workspace takes &MirWorkspace (codegen consumes MIR);
- MTerm::New is unreachable!() — raw-buf.4 desugars Term::New to
(app T.new …) before codegen, so there is no element-type
re-derivation left to relocate;
- #51 / #53 (the element-type / new-T codegen crashes) are closed;
their residue was fixed by ee4107c / 420f75f plus the New-desugar,
not by a separate raw-buf patch track.
Ledger work (the mir.5 deliverable):
- NEW design/contracts/0018-check-codegen-boundary.md: the invariant
"codegen re-derives nothing; MIR is total over what check proved;
a codegen arm that recomputes a fact instead of reading MIR is
drift." Ratifier: lower_to_mir_ty.rs::callee_classification_builtin_and_static.
- 0013-typeclasses invariant 2 retracted: codegen no longer re-resolves
cross-module names via an import_map fallback; lower_to_mir::classify_callee
resolves the reference once into Callee::Static and codegen consumes it.
- 0003-pipeline.md: the "lower to MIR" line names the real stage
(elaborate_workspace → MirWorkspace → lower_workspace) and a new
paragraph states the boundary, cross-referencing 0018.
- INDEX.md: boundary contract row added; qualified-xref re-pointed at
lower_to_mir + 0018.
- codegen_import_map_fallback_pin.rs doc-comment made honest — it pins
the post-mono AST precondition classify_callee relies on, not a
codegen-side resolution that no longer exists. Assertions unchanged;
the test stays green.
- spec 0060 gains a mir.5 refinement note recording the early code
convergence.
Acceptance criteria 1-7 of docs/specs/0060-typed-mir.md are all met.
Full workspace suite green (exit 0, 0 failed, 2 ignored); 708 passed
carried from mir.4 (no test added or removed).
Not done here (deliberately): the milestone #7 (raw-buf) subsumption
note is an external Gitea tracker write; the /boss auto-mode classifier
declined it as an unauthorised external write and it is surfaced to the
user rather than worked around. The end-to-end milestone fieldtest
remains the deliberate manual close-gate before the tracker milestone
is marked done.
refs #51#53
Architect drift review at raw-buf milestone close (after 55d76ae closed
#43) surfaced three items; this commit clears them. All three lockstep-
invariant pairs were confirmed intact and the effective-name keying was
confirmed consistent across the desugar→lift boundary (lift_letrecs reads
the desugared tree's effective names too).
1. [high] Honesty fix. `fresh_binder`'s doc-comment (and 55d76ae's body)
claimed "authored names cannot contain `$` — the lexer reserves it".
False: the lexer (ailang-surface) reserves only `.`, not `$`. The
`$`-for-synthetic convention is not enforced. So collision-freedom
rests solely on the `used` + in-scope-`scope` probe, which does not
see an authored `<base>$<n>` that is out of scope at mint time but
later binds under the same `(def, name)` key — the very collision
class this fix closes. Latent (no fixture uses a `$` binder), but the
stated rationale was wrong. Doc-comment now describes the probe
honestly and names the gap + its two possible closures (enforce the
reservation, or seed `used` with every authored binder name in the
def). The enforce-or-retract decision is the next-direction follow-up.
2. [medium] design/models/0003-pipeline.md — "desugar currently only
flattens nested constructor patterns" no longer matches the code
(it now also alpha-renames shadowing binders). Corrected to current
state (honesty-rule).
3. [low] design/contracts/0008-memory-model.md — the three drop gates
all key on `(def_name, binder_name)` consume_count, silently relying
on per-fn binder-name injectivity, which the ledger never stated.
Added that invariant as an explicit precondition of the gates, with
the desugar guarantee and its ratifying tests.
No code-logic change; doc-comment + ledger only.
All 176 files in the four accumulating directories now use a
zero-padded 4-digit counter prefix that reflects creation order
(`NNNN-slug.md`). The counter is assigned per directory in strict
git-log creation order; ties broken alphabetically by original name.
The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is
dropped — the date is recoverable from git log and the counter
carries the ordering.
A file's counter is stable for the life of the file: never reassigned,
never reused, never compacted. Deleted files retire their counter;
subsequent files do not fill the gap. This is the property that lets
cross-references stay literal — refs use the full filename including
the counter (`design/contracts/0007-honesty-rule.md`) so they grep
cleanly and resolve directly without a glob step.
313 cross-references updated across .md/.rs/.toml/.c/.json files
(test pins, include_str! paths, design-INDEX entries, baseline notes,
runtime C comments, inter-contract markdown links incl. bare basename
and `../models/foo.md` forms).
CLAUDE.md gets a new "File-naming convention" section spelling out
the rule and rationale. skills/brainstorm/SKILL.md and
skills/planner/SKILL.md updated so new spec/plan creation produces
counter-prefixed names from the start.
The full test suite (cargo test --workspace) passes.
Brummel