Executable projection of spec 0062 (#55) into four tasks: (1) the
borrow-return reject, (2) the borrow-over-value reject, (3) a throwaway
`ail migrate-modes` pass (parse -> Implicit->Own, keep explicit
own/borrow -> print explicit), (4) the atomic cutover (run the
migration over the corpus + hand-fix the read-only-heap params the
now-universal linearity check flags, delete the variant + all
compile sites compiler-driven, parser bare-slot reject, reset the hash
pins, flip the leak pin, update both contracts, drop the throwaway).
Placeholder-free; all seven surface fixtures parse-gated against HEAD.
Spec 0062 marked approved (user, 2026-06-01) and its soundness
re-validated against post-#56 HEAD: the three own-return-provenance /
regime-A fixtures still exit 1 under [consume-while-borrowed]; #56's
application-is-a-borrow change does not weaken them (none is an
application of a borrowed binder).
plan-recon folded four spec-enumeration corrections into the plan:
- kernel migration target is raw_buf/source.ail, not the retired
kernel_stub/source.ail the spec cited;
- FIVE hash pins shift, not the two the spec named (embed_export_hash,
eq_ord_e2e, mono_hash_stability are the missed twins);
- design/contracts/0002-data-model.md also documents the "implicit"
JSON form and is drift-anchored -> updates alongside 0008;
- real counts are 261 fn-type fixtures (spec ~208) and 17 fn_implicit
references (spec 16); the compiler is the authoritative enumerator.
refs #55
Design spec for #55, superseding #54. Deletes ParamMode::Implicit in a
single cutover -> binary {Own, Borrow}; no defaulted ownership mode
survives on any fn-type slot, authored or compiler-synthesised.
The grounding pass corrected the central architecture claim. Both #55
and the first draft assumed a new return-provenance check was needed to
reject an own-return aliasing a borrowed binder, "silently accepted
today". Running the candidate fixtures through the live `ail check`
falsified that: consume-while-borrowed already rejects all three
provenance paths -- direct passthrough, let-indirection, and borrow
escaping into a returned constructor (regime A). Own-return soundness
and regime A are already-green properties. The cutover therefore adds
exactly one new check (borrow-return rejection) plus one signature-level
reject (borrow-over-value), not two new provenance analyses.
Scope decisions ratified: keyword stays verbal (own/borrow), ParamMode
keeps its name; totality is strict including value-type slots (every
slot moded, (own value) trivial, (borrow value) an error, bare slot a
parse error) so an LLM author needs no heap/value knowledge.
The leak fix (spec 0061 symptom) falls out of Implicit->Own at the
synthesis sites: the old typechecker made Implicit and Own
indistinguishable (mode_eq), so setting Own changes no typecheck
outcome -- it only flips the codegen dec gate from skip to emit.
Out of scope: re-enabling borrow-returns (needs the escape/liveness
axis), multi-return, mode polymorphism.
grounding-check: PASS (7 assumptions ratified against named green tests;
all fenced ail blocks validated against the live tool).
refs #55
Brummel