From a84ba596cfb6d02ab9900a61794b46a4ab00eadb Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 16:19:07 +0200 Subject: [PATCH] plan: eliminate the Implicit ownership default (0121) 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 --- docs/plans/0121-eliminate-implicit-mode.md | 970 +++++++++++++++++++++ docs/specs/0062-eliminate-implicit-mode.md | 6 +- 2 files changed, 975 insertions(+), 1 deletion(-) create mode 100644 docs/plans/0121-eliminate-implicit-mode.md diff --git a/docs/plans/0121-eliminate-implicit-mode.md b/docs/plans/0121-eliminate-implicit-mode.md new file mode 100644 index 0000000..68525a1 --- /dev/null +++ b/docs/plans/0121-eliminate-implicit-mode.md @@ -0,0 +1,970 @@ +# Eliminate the Implicit ownership default — Implementation Plan + +> **Parent spec:** `docs/specs/0062-eliminate-implicit-mode.md` +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement` +> skill to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Delete `ParamMode::Implicit` in a single cutover so +`ParamMode` becomes binary `{Own, Borrow}` and no fn-type slot — +authored or synthesised — carries a defaulted ownership mode. + +**Architecture:** Four tasks. Tasks 1–2 add the two new +signature-level rejects (borrow-return, borrow-over-value) while +`Implicit` still exists — each leaves a green, independently +committable tree. Task 3 builds a throwaway `ail migrate-modes` +subcommand (parse → map `Implicit↦Own`, keep explicit `Own`/`Borrow` +→ print explicit → write back) and unit-tests it without touching the +corpus. Task 4 is the atomic cutover: run the migration tool over the +whole `.ail` corpus, hand-fix the read-only-heap params the +now-universal linearity check flags as over-consuming, then delete the +variant + all its compile sites (compiler-driven), add the parser +bare-slot reject, reset the five hash pins, flip the leak pin, update +both affected contracts, and remove the throwaway subcommand. + +**Tech Stack:** `ailang-core` (`ast.rs` schema, `primitives.rs` +`is_value_type`), `ailang-surface` (`parse.rs` slot grammar, `print.rs` +slot printer), `ailang-check` (`lib.rs` signature checks + `CheckError` +registry, `linearity.rs`/`uniqueness.rs` activation gate), `ail` +(throwaway migration subcommand), the `.ail` corpus, the design ledger +contracts `0002`/`0008`. + +--- + +## Recon corrections folded into this plan + +The spec's enumeration drifted from the tree; the authoritative +figures the plan executes against (verified by `plan-recon`, +2026-06-01): + +- **Kernel migration path:** the spec/issue cite + `crates/ailang-kernel/src/kernel_stub/source.ail` — that path does + **not exist** (kernel_stub retired in raw-buf.4 per CLAUDE.md). The + live kernel-tier source is `crates/ailang-kernel/src/raw_buf/source.ail`. +- **Hash pins: FIVE, not two.** The spec named + `crates/ailang-core/tests/hash_pin.rs` and + `crates/ailang-surface/tests/prelude_module_hash_pin.rs`. Three more + carry fn-type-bearing hex pins that the mode-serialisation change + shifts: `crates/ailang-core/tests/embed_export_hash_stable.rs:32`, + `crates/ail/tests/eq_ord_e2e.rs:139`, + `crates/ail/tests/mono_hash_stability.rs` (the `eq__`/`compare__`/ + `show__` block, `:63-68,:107-110`). +- **Second contract.** The spec's acceptance criterion 7 names only + `design/contracts/0008-memory-model.md`. `design/contracts/0002-data-model.md` + also documents the `"implicit"` JSON form and `implicit ≡ own`, and is + drift-anchored by `design_schema_drift.rs:design_md_anchors_every_parammode_variant`. + The honesty rule forces it to update in the same iteration. **Both + contracts update.** +- **Counts:** ~261 example fixtures carry `(fn-type` slots (spec said + ~208); `fn_implicit` has 16 call sites + 1 def = 17 references (spec + said 16). The compiler is the authoritative enumerator for the + synthesis-site `Own` migration; do not hand-count. +- **Lambda annotations are NOT moded slots.** `parse_lam` + (`parse.rs:1518`) reads `(typed name type)` params and `(ret type)` + via `parse_type()`, not `parse_param_with_mode`. The bare-slot reject + (Task 4) therefore hits `(fn-type …)` slots only; lambda type + annotations stay bare and are untouched by the migration. + +## Files this plan creates or modifies + +- Create: `examples/borrow_return_reject.ail` — RED fixture, borrow-return reject (Task 1) +- Create: `examples/borrow_value_reject.ail` — RED fixture, borrow-over-value reject (Task 2) +- Create: `examples/bare_slot_reject.ail` — RED fixture, parser bare-slot reject (Task 4) +- Create: `examples/own_return_provenance_reject.ail` (+ `_let`, `_ctor` variants) — already-green `consume-while-borrowed` regression pins (Task 4) +- Create: `examples/ownership_total.ail` — post-cutover authoring-surface GREEN fixture (Task 4) +- Modify: `crates/ailang-check/src/lib.rs` — two new `CheckError` variants + `code()` entries + signature-check wiring (`:2240`); the ~50 `ret_mode: ParamMode::Implicit` synthesis literals → `Own` (Task 4) +- Modify: `crates/ailang-core/src/ast.rs:778-953` — `ParamMode` enum, `Type::Fn` serde, `fn_implicit`→`fn_owned`, helper deletion, `PartialEq` (Task 4) +- Modify: `crates/ailang-surface/src/parse.rs:1180-1222` — bare-slot reject + elision deletion (Task 4) +- Modify: `crates/ailang-surface/src/print.rs:357-360,:408` — delete `Implicit` arm (Task 4) +- Modify: `crates/ailang-codegen/src/{drop.rs:467-478,lambda.rs:164,lib.rs}` — `Implicit`→`Own` synthesis + comment (Task 4) +- Modify: `crates/ailang-core/src/{desugar.rs,pretty.rs}` — synthesis literals → `Own` (Task 4) +- Modify: `crates/ailang-prose/src/lib.rs:456,…` — delete `Implicit` arm + synthesis literals (Task 4) +- Modify: `crates/ailang-check/src/{linearity.rs:356,385,reuse_shape.rs:110,uniqueness.rs}` — dead activation-gate arm collapse (Task 4) +- Modify: `examples/*.ail` (261), `examples/prelude.ail`, `crates/ailang-kernel/src/raw_buf/source.ail` — corpus migration (Task 4) +- Modify: the five hash-pin test files (Task 4) +- Modify: `examples/rc_let_implicit_returning_app.ail` + `crates/ail/tests/print_no_leak_pin.rs` — leak flip (Task 4) +- Modify: `crates/ailang-core/tests/{schema_coverage.rs,design_schema_drift.rs}` — delete `ParamModeImplicit` tag + exemplar (Task 4) +- Modify: `design/contracts/0008-memory-model.md`, `design/contracts/0002-data-model.md` — binary-model prose (Task 4) +- Create (throwaway, removed in Task 4): `ail migrate-modes` subcommand in `crates/ail/src/main.rs` (Task 3) +- Test: `crates/ail/tests/migrate_modes.rs` — migration-tool unit test (Task 3, removed in Task 4) + +--- + +## Task 1: New check — borrow-return rejection + +`(ret (borrow T))` becomes a check error. Independent of `Implicit`; +the tree stays green and this task is independently committable. + +**Files:** +- Create: `examples/borrow_return_reject.ail` +- Modify: `crates/ailang-check/src/lib.rs` (`CheckError` enum ~`:404`, `code()` ~`:837`, signature check ~`:2275`) +- Test: `crates/ail/tests/mode_signature_rejects.rs` (new, CLI-boundary E2E) + +- [ ] **Step 1: Write the RED fixture** + +Create `examples/borrow_return_reject.ail`: + +```ail +(module borrow_return_reject + + (data Box + (doc "Heap cell holding one Int.") + (ctor Box (con Int))) + + (fn peek + (doc "MUST FAIL post-cutover: borrow-return is refcount-invisible and can outlive its source; re-enabling needs the escape axis.") + (type + (fn-type + (params (own (con Box))) + (ret (borrow (con Box))))) + (params b) + (body b))) +``` + +- [ ] **Step 2: Write the failing test (CLI-boundary, the project's reject-pin pattern)** + +Create `crates/ail/tests/mode_signature_rejects.rs` — modelled verbatim +on `crates/ail/tests/raw_buf_new_type_arg_pin.rs` (run `ail check` on +the fixture, assert non-zero exit + stderr carries the code): + +```rust +//! Signature-level mode rejects added by spec 0062: borrow-return +//! (`(ret (borrow T))`) and borrow-over-value (`(borrow value-type)`). +//! CLI-boundary E2E (the project's reject-pin pattern): the diagnostic +//! is the observable exit behaviour of `ail check`. +use std::path::{Path, PathBuf}; +use std::process::Command; + +fn repo_root() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")).parent().unwrap().parent().unwrap().to_path_buf() +} + +fn check_rejects_with(fixture: &str, code: &str) { + let path = repo_root().join("examples").join(fixture); + let out = Command::new(env!("CARGO_BIN_EXE_ail")) + .arg("check").arg(&path).output().expect("ail check spawn"); + assert!(!out.status.success(), + "expected `ail check {fixture}` to REJECT, but it passed: stdout={}", + String::from_utf8_lossy(&out.stdout)); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!(stderr.contains(code), "expected code `{code}`, got: {stderr}"); +} + +/// `(ret (borrow T))` is rejected with code `borrow-return-not-permitted`. +#[test] +fn borrow_return_is_rejected() { + check_rejects_with("borrow_return_reject.ail", "borrow-return-not-permitted"); +} +``` + +- [ ] **Step 3: Run the test to verify it fails** + +Run: `cargo test -p ail --test mode_signature_rejects borrow_return_is_rejected` +Expected: FAIL — today the fixture checks clean (no return check exists), +so `ail check` exits 0 and the `!out.status.success()` assert fires. + +- [ ] **Step 4: Add the `CheckError` variant** + +In `crates/ailang-check/src/lib.rs`, in `pub enum CheckError` (after the +last variant `Internal(_)`'s neighbours — place next to the other +signature rejects), add: + +```rust + /// A fn-type return slot is `(borrow T)`. Borrow-returns are + /// refcount-invisible and can outlive their source; re-enabling + /// them needs the escape/liveness axis (out of scope, spec 0062 + /// §"Out of scope"). Code: `borrow-return-not-permitted`. + #[error("borrow-return not permitted for `{0}`: a (borrow …) return is refcount-invisible and can outlive its source; this language version forbids it (the escape/liveness axis that would make it sound is not yet built)")] + BorrowReturnNotPermitted(String), +``` + +- [ ] **Step 5: Register the code** + +In `fn code(&self)`, add before `CheckError::Internal(_) => "internal",`: + +```rust + CheckError::BorrowReturnNotPermitted(_) => "borrow-return-not-permitted", +``` + +- [ ] **Step 6: Fire the check at the fn signature** + +In `check_def` (`crates/ailang-check/src/lib.rs`), the fn signature is +destructured at `:2240`: + +```rust + let (param_tys, ret_ty, declared_effs) = match &inner_ty { + Type::Fn { params, ret, effects, .. } => { + (params.clone(), (**ret).clone(), effects.clone()) + } +``` + +Change the pattern to bind the modes, and after the existing +`check_type_well_formed(&ret_ty, &env)?;` line (`:2275`) add the +reject. First, widen the destructure: + +```rust + let (param_tys, param_modes, ret_ty, ret_mode, declared_effs) = match &inner_ty { + Type::Fn { params, param_modes, ret, ret_mode, effects } => { + (params.clone(), param_modes.clone(), (**ret).clone(), *ret_mode, effects.clone()) + } + other => { + return Err(CheckError::FnTypeRequired( + f.name.clone(), + ailang_core::pretty::type_to_string(other), + )); + } + }; +``` + +Then immediately after `check_type_well_formed(&ret_ty, &env)?;`: + +```rust + // spec 0062: borrow-returns are refcount-invisible — forbidden in + // this language version (the escape/liveness axis is unbuilt). + if matches!(ret_mode, ParamMode::Borrow) { + return Err(CheckError::BorrowReturnNotPermitted(f.name.clone())); + } +``` + +> Ensure `ParamMode` is in scope in `lib.rs` (it is — `param_modes` +> are already referenced elsewhere in the file). If the widened +> destructure makes `param_modes`/`ret_mode` unused warnings appear +> before Task 2 lands, prefix with `_` and unprefix in Task 2 Step 4. + +- [ ] **Step 7: Run the test to verify it passes** + +Run: `cargo build -p ail && cargo test -p ail --test mode_signature_rejects borrow_return_is_rejected` +Expected: PASS + +- [ ] **Step 8: Confirm no corpus fixture regresses** + +Run: `cargo build -p ail && python3 bench/check.py` +Expected: 0 regressions (no checked-in fixture has a `(ret (borrow …))` +— the spec asserts none survive, and `consume-while-borrowed` already +rejects the body shapes that would force one). + +--- + +## Task 2: New signature reject — borrow-over-value + +`(borrow value-type)` becomes a check error, fired on the signature. +Independent of `Implicit`; tree stays green; independently committable. + +**Files:** +- Create: `examples/borrow_value_reject.ail` +- Modify: `crates/ailang-check/src/lib.rs` (`CheckError` enum, `code()`, signature check) +- Test: `crates/ail/tests/mode_signature_rejects.rs` (extend) + +- [ ] **Step 1: Confirm the corpus has no borrow-over-value today** + +Run: `git grep -nE '\(borrow \(con (Int|Bool|Float|Unit)\)' examples crates/ailang-kernel` +Expected: no matches (if any match, that fixture must be re-moded to +`(own …)` as part of this task before the check can land green — note +it in the implement report). + +- [ ] **Step 2: Write the RED fixture** + +Create `examples/borrow_value_reject.ail`: + +```ail +(module borrow_value_reject + + (fn ignore + (doc "MUST FAIL post-cutover: borrow over a value type is meaningless.") + (type + (fn-type + (params (borrow (con Int))) + (ret (own (con Int))))) + (params n) + (body 0))) +``` + +- [ ] **Step 3: Extend the test** + +Append to `crates/ail/tests/mode_signature_rejects.rs`: + +```rust +/// `(borrow value-type)` is rejected with code `borrow-over-value`. +#[test] +fn borrow_over_value_is_rejected() { + check_rejects_with("borrow_value_reject.ail", "borrow-over-value"); +} +``` + +- [ ] **Step 4: Run the test to verify it fails** + +Run: `cargo test -p ail --test mode_signature_rejects borrow_over_value_is_rejected` +Expected: FAIL — today the fixture checks clean. + +- [ ] **Step 5: Add the `CheckError` variant + code** + +In `pub enum CheckError`, add: + +```rust + /// A fn-type slot is `(borrow V)` where `V` is an unboxed value + /// type (`Int`/`Bool`/`Float`/`Unit`). Borrow is meaningless over + /// a value type — it has no refcount and is copied by value + /// (model §3.2). Code: `borrow-over-value`. + #[error("borrow over value type in `{def}`: `{ty}` is an unboxed value type and cannot be borrowed; use `(own {ty})`")] + BorrowOverValueType { def: String, ty: String }, +``` + +In `fn code(&self)`, add before `CheckError::Internal(_)`: + +```rust + CheckError::BorrowOverValueType { .. } => "borrow-over-value", +``` + +- [ ] **Step 6: Fire the check at the fn signature** + +In `check_def`, immediately after the borrow-return check added in +Task 1 Step 6, add (this uses the `param_modes`/`param_tys` bound in +Task 1; unprefix them if Task 1 prefixed with `_`): + +```rust + // spec 0062: borrow over an unboxed value type is meaningless. + // Fired on the signature, before body dataflow. + for (ty, mode) in param_tys.iter().zip(param_modes.iter()) { + if matches!(mode, ParamMode::Borrow) { + if let Type::Con { name, args } = ty { + if args.is_empty() && ailang_core::primitives::is_value_type(name) { + return Err(CheckError::BorrowOverValueType { + def: f.name.clone(), + ty: name.clone(), + }); + } + } + } + } + // ret slot: a borrow ret is already rejected above, so a + // borrow-over-value ret cannot reach here. +``` + +- [ ] **Step 7: Run the test to verify it passes** + +Run: `cargo build -p ail && cargo test -p ail --test mode_signature_rejects` +Expected: PASS (both tests). + +- [ ] **Step 8: Full check-suite gate** + +Run: `cargo build -p ail && python3 bench/check.py && python3 bench/compile_check.py` +Expected: 0 regressions. (Confirms no corpus fixture borrows a value +type today — the Step 1 grep already proved this.) + +--- + +## Task 3: Throwaway migration tool — `ail migrate-modes` + +A parse → `Implicit↦Own` → print-explicit → write-back pass, run over +the corpus in Task 4. `Own`/`Borrow` are preserved verbatim. This is +semantically invisible today (`PartialEq` treats `Implicit == Own`, +`ast.rs:mode_eq`), so the migrated corpus still typechecks identically +— but it materialises the modes so the post-cutover parser (which +rejects bare slots) accepts the sources. Throwaway: removed in Task 4 +once `Implicit` is deleted (the subcommand would not compile). + +**Files:** +- Modify: `crates/ail/src/main.rs` (add `MigrateModes` subcommand) +- Test: `crates/ail/tests/migrate_modes.rs` (new) + +- [ ] **Step 1: Write the failing tool test** + +Create `crates/ail/tests/migrate_modes.rs`: + +```rust +//! Throwaway migration-tool test (spec 0062). Asserts the +//! parse→Implicit↦Own→print pass materialises bare slots as `(own …)` +//! and leaves explicit `(borrow …)` untouched. Deleted in the cutover. +use ailang_surface::{parse, print}; +use ailang_core::ast::ParamMode; + +/// Re-implements the tool's core transform for the unit test so the +/// assertion does not depend on the CLI I/O wrapper. +fn migrate_text(src: &str) -> String { + let mut m = parse(src).expect("parse"); + ailang_core::ast::for_each_fn_type_mut(&mut m, &mut |params_len, pm, rm| { + pm.resize(params_len, ParamMode::Own); + for x in pm.iter_mut() { + if matches!(x, ParamMode::Implicit) { *x = ParamMode::Own; } + } + if matches!(rm, ParamMode::Implicit) { *rm = ParamMode::Own; } + }); + print(&m) +} + +#[test] +fn bare_slot_becomes_own_borrow_preserved() { + let src = "(module m\n (fn f\n (doc \"d\")\n (type (fn-type (params (con Int) (borrow (con Int))) (ret (con Int))))\n (params x y)\n (body x)))\n"; + let out = migrate_text(src); + assert!(out.contains("(params (own (con Int)) (borrow (con Int)))"), "got: {out}"); + assert!(out.contains("(ret (own (con Int)))"), "got: {out}"); +} +``` + +> `ailang_surface::parse` (`parse.rs:125`, `-> Result`) +> and `ailang_surface::print` (`print.rs:17`, `-> String`) are the +> verified public entry points. `for_each_fn_type_mut` is introduced in +> Step 2. + +- [ ] **Step 2: Add the AST fn-type walker** + +In `crates/ailang-core/src/ast.rs`, add a public mutator that visits +every `Type::Fn` reachable from a module's defs (signatures incl. +`Forall` bodies, and nested fn-types inside param/ret/arg types). The +callback receives the param count, a `&mut Vec`, and a +`&mut ParamMode`: + +```rust +/// Visit every `Type::Fn` in `m`, letting `f` rewrite its modes. +/// `f(params_len, param_modes, ret_mode)`. Used by the throwaway +/// `migrate-modes` tool (spec 0062); has no other caller and is +/// removed if the migration machinery is retired. +pub fn for_each_fn_type_mut( + m: &mut Module, + f: &mut impl FnMut(usize, &mut Vec, &mut ParamMode), +) { + fn walk_ty(t: &mut Type, f: &mut impl FnMut(usize, &mut Vec, &mut ParamMode)) { + match t { + Type::Fn { params, param_modes, ret, ret_mode, .. } => { + let n = params.len(); + for p in params.iter_mut() { walk_ty(p, f); } + walk_ty(ret, f); + f(n, param_modes, ret_mode); + } + Type::Con { args, .. } => { for a in args.iter_mut() { walk_ty(a, f); } } + Type::Forall { body, .. } => walk_ty(body, f), + Type::Var { .. } => {} + } + } + for def in m.defs.iter_mut() { + if let Def::Fn(fd) = def { + walk_ty(&mut fd.ty, f); + } + } +} +``` + +> The implementer confirms the `Module`/`Def`/`FnDef` field names +> (`m.defs`, `Def::Fn(fd)`, `fd.ty`) against the actual `ast.rs`; the +> recon-confirmed shape is `Def::Fn(f) => f.ty` (`lib.rs:1427`). + +- [ ] **Step 3: Run the tool test to verify it fails** + +Run: `cargo test -p ail --test migrate_modes` +Expected: FAIL — `for_each_fn_type_mut` is new; before Step 2 it does +not compile, after Step 2 the test should compile and pass. (If it +passes immediately after Step 2, that is the GREEN; the RED was the +compile failure pinning the missing walker.) + +- [ ] **Step 4: Add the throwaway CLI subcommand** + +In `crates/ail/src/main.rs`, add a `MigrateModes { path: PathBuf }` +arm to `enum Cmd` and a handler that reads the file, runs the same +transform as `migrate_text` (factored into a shared fn or duplicated — +this is throwaway), and writes the printed result back in place: + +```rust + /// THROWAWAY (spec 0062): rewrite every bare fn-type slot in a + /// `.ail` file as `(own …)`, preserving explicit `(own)`/`(borrow)`. + /// Removed in the Implicit-deletion cutover. + MigrateModes { path: std::path::PathBuf }, +``` + +Handler (in the match on `Cmd`): + +```rust + Cmd::MigrateModes { path } => { + let src = std::fs::read_to_string(&path)?; + let mut m = ailang_surface::parse(&src)?; + ailang_core::ast::for_each_fn_type_mut(&mut m, &mut |n, pm, rm| { + pm.resize(n, ailang_core::ast::ParamMode::Own); + for x in pm.iter_mut() { + if matches!(x, ailang_core::ast::ParamMode::Implicit) { + *x = ailang_core::ast::ParamMode::Own; + } + } + if matches!(rm, ailang_core::ast::ParamMode::Implicit) { + *rm = ailang_core::ast::ParamMode::Own; + } + }); + std::fs::write(&path, ailang_surface::print(&m))?; + Ok(()) + } +``` + +> Match the handler's error type / `Ok(())` shape to the sibling arms +> in `main.rs`; the recon confirms `enum Cmd` at `main.rs:63`. + +- [ ] **Step 5: Build the tool** + +Run: `cargo build -p ail` +Expected: 0 errors. `target/debug/ail migrate-modes ` now exists. + +- [ ] **Step 6: Full-suite gate (no corpus touched yet)** + +Run: `cargo test --workspace` +Expected: green — Task 3 is purely additive; no corpus file or schema +changed. + +--- + +## Task 4: The atomic cutover + +Everything that cannot land except together: run the migration over the +corpus, delete the variant + all compile sites, parser reject, hash +resets, leak flip, contract updates, drift-pin updates, new fixtures. +A deleted variant makes the whole workspace fail to compile until every +site is migrated, and the parser reject breaks every bare slot until +the corpus is migrated — so all of it is one task with a single green +gate at the end. The compiler is the authoritative site enumerator. + +**Files:** all under "Files this plan creates or modifies" tagged +(Task 4), plus removal of the Task 3 throwaway. + +### Phase A — migrate the corpus (Implicit still present, tree green) + +- [ ] **Step 1: Run the migration tool over the whole corpus** + +Run: +``` +cargo build -p ail +for f in (find examples -name '*.ail') examples/prelude.ail crates/ailang-kernel/src/raw_buf/source.ail + ./target/debug/ail migrate-modes $f +end +``` +(fish syntax; the implementer adapts to the available shell. The +`find` already includes `examples/prelude.ail`, so the explicit repeat +is harmless — dedupe if preferred.) +Expected: every `.ail` file rewritten with explicit modes on every +fn-type slot; bare slots gone. + +- [ ] **Step 2: Verify the migrated corpus parses and round-trips** + +Run: `cargo build -p ail && python3 bench/check.py` +Expected: 0 regressions. (Sources are now explicit `own`/`borrow`; +bare slots are still legal under the current parser, so anything the +tool missed still parses — but `check.py` must stay green. The +round-trip invariant is enforced by the build deriving JSON via +`parse`.) + +- [ ] **Step 3: Activate the strict check early via the migration, fix over-consuming params** + +Migrating a fn to explicit modes turns on the (today gated-off) +strict linearity check for it — exactly the universal activation #56 +hardened. A bare heap param the tool set to `(own …)` that the body +only reads, and which a caller passes while retaining, now trips +`consume-while-borrowed` / `use-after-consume`. + +Run: `cargo test --workspace 2>&1 | grep -iE 'consume-while-borrowed|use-after-consume|over-strict' ` +For each flagged fn: change the offending param's `(own …)` to +`(borrow …)` in its `.ail` source (the `suggested_mode: "borrow"` +diagnostic names the param). Re-run until the grep is empty. +Expected (final): no linearity errors; the corpus encodes the derived +modes (consumed ⇒ own, read-only-heap ⇒ borrow, value ⇒ own). + +> This is the spec's "derived from the existing uniqueness/consume +> analysis … reviewed by the orchestrator" — the tool drafts blanket +> `own`, the universal check flags the read-only-heap params, and the +> fix is mechanical and check-gated. The orchestrator reviews the full +> mode diff before commit (the derivation is a drafting aid, not a +> surviving default). + +### Phase B — delete the variant (compiler-driven site set) + +- [ ] **Step 4: Edit `ParamMode` and `Type::Fn` serde in `ast.rs`** + +In `crates/ailang-core/src/ast.rs`: + +Replace the `Type::Fn` field attributes (`:780`, `:783`) — drop the +elision: + +```rust + Fn { + params: Vec, + param_modes: Vec, + ret: Box, + ret_mode: ParamMode, + #[serde(default)] + effects: Vec, + }, +``` + +Replace `fn fn_implicit` (`:837`) with `fn_owned`: + +```rust + /// Build a `Type::Fn` with every parameter mode and the return + /// mode set to `ParamMode::Own`. The synthesis form for every + /// typechecker / desugar / codegen site that builds a fn-type; + /// `Own` is correct by construction (spec 0062 Data flow: the old + /// typechecker made `Implicit ≡ Own`, so synthesised fn-types were + /// already semantically `Own`). + pub fn fn_owned(params: Vec, ret: Type, effects: Vec) -> Type { + let n = params.len(); + Type::Fn { + params, + param_modes: vec![ParamMode::Own; n], + ret: Box::new(ret), + ret_mode: ParamMode::Own, + effects, + } + } +``` + +Replace the `ParamMode` enum (`:860`) — drop `Default` + `Implicit`: + +```rust +/// Per-parameter / return mode marker on a [`Type::Fn`]. Full +/// contract lives in `design/contracts/0008-memory-model.md`. +/// Ownership has no default: every fn-type slot carries an explicit +/// `Own` or `Borrow` (spec 0062). +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "lowercase")] +pub enum ParamMode { + /// `(own T)` — caller transfers ownership; callee consumes. + Own, + /// `(borrow T)` — caller retains ownership; callee may not consume. + Borrow, +} +``` + +Delete `impl ParamMode { fn is_implicit }` (`:872-878`), `fn all_implicit` +(`:880-887`), `fn mode_eq` (`:889-901`), and `fn mode_slices_eq` +(`:903-919`). + +In `impl PartialEq for Type`, replace the `Type::Fn` arm's mode +comparison (`:946-947`): + +```rust + ap == bp + && ar == br + && apm == bpm + && arm == brm + && { + let mut a = ae.clone(); + let mut b = be.clone(); + a.sort(); + b.sort(); + a == b + } +``` + +- [ ] **Step 5: Compiler-driven migration of all remaining sites** + +Run: `cargo build --workspace 2>&1 | rg 'ParamMode::Implicit|fn_implicit|mode_eq|all_implicit|is_implicit|mode_slices_eq'` + +Apply the deterministic decision rule to every reported site (no +judgement calls): + +- `ret_mode: ParamMode::Implicit` / `param_modes: vec![ParamMode::Implicit; n]` + / `.insert(_, ParamMode::Implicit)` — a **synthesis** site → replace + `Implicit` with `Own`. +- `.unwrap_or(ParamMode::Implicit)` — modes are always present now → + the `.unwrap_or(...)`/`.get(i).copied().unwrap_or(...)` becomes a + direct index (`param_modes[i]`) or `.unwrap_or(ParamMode::Own)` if a + fallback is structurally still needed; prefer the direct index where + the length invariant (`param_modes.len() == params.len()`) holds. +- `matches!(m, ParamMode::Implicit)` in an **activation gate** + (`linearity.rs:356`, `reuse_shape.rs:110`) — the `any(Implicit)` + disjunct is now always false → delete that disjunct (gate reduces to + its other condition, e.g. `params.is_empty()`). +- `ParamMode::Own | ParamMode::Implicit => …` match arm + (`linearity.rs:385`) → collapse to `ParamMode::Own => …`. +- `ParamMode::Implicit => write_type(out, t)` (printer `print.rs:360`, + prose `lib.rs:456`) → delete the arm (the `match mode` is now + exhaustive over `{Own, Borrow}`). +- `fn_implicit(` callers (17 references) → `fn_owned(`. +- `mode_eq` / `mode_slices_eq` callers → already handled in Step 4 + (only caller was `PartialEq`). + +Repeat `cargo build --workspace` until 0 errors. +Expected (final): `cargo build --workspace` 0 errors, and +`git grep -nE 'ParamMode::Implicit|fn_implicit|is_implicit|all_implicit|mode_eq|mode_slices_eq' crates/` is empty (acceptance criterion 1). + +- [ ] **Step 6: Parser — reject bare slots, delete elision** + +In `crates/ailang-surface/src/parse.rs`, replace the bare fallthrough +in `parse_param_with_mode` (`:1220-1221`): + +```rust + // bare type in a fn-type slot is no longer permitted (spec 0062): + // every slot must carry (own …) or (borrow …). + let tok = self.peek().cloned(); + Err(self.error_at(tok, "fn-type slot requires a mode: write (own T) or (borrow T)")) +``` + +> The implementer uses the crate's actual `ParseError` constructor +> (the helper the sibling parse errors in this file already use); the +> load-bearing behaviour is "bare slot → `Err`", verified by Step 12's +> fixture. + +In `parse_fn_type`, delete the all-Implicit elision (`:1180-1187`) — +store `param_modes` directly: + +```rust + Ok(Type::Fn { + params, + ret: Box::new(ret), + effects, + param_modes, + ret_mode, + }) +``` + +- [ ] **Step 7: Printer — drop the `Implicit` arm** + +In `crates/ailang-surface/src/print.rs`, `write_fn_type_slot` (`:357`) +becomes exhaustive over `{Own, Borrow}` (Step 5 already deleted the +`Implicit` arm); change the `param_modes.get(i).copied().unwrap_or(ParamMode::Implicit)` +at `:408` to a direct index `param_modes[i]` (length invariant holds +post-cutover). + +- [ ] **Step 8: Delete the `ParamModeImplicit` drift tag + exemplar** + +- `crates/ailang-core/tests/schema_coverage.rs:70,114,345` — delete the + `VariantTag::ParamModeImplicit` enum value and its exhaustive-`match` + arm so the coverage test no longer expects an `"implicit"` form. +- `crates/ailang-core/tests/design_schema_drift.rs:385,392` — delete the + `"implicit"` exemplar row and the `match` arm that asserts it + serialises and is doc-anchored. + +### Phase C — pins, fixtures, contracts + +- [ ] **Step 9: Reset all five hash pins** + +For each pin, regenerate the expected hex from the migrated module and +re-assert (do not hand-edit blindly — recompute): + +- `crates/ailang-core/tests/hash_pin.rs` — `sum`, `IntList`, and `:257`/`:266`/`:275`. +- `crates/ailang-surface/tests/prelude_module_hash_pin.rs:50`. +- `crates/ailang-core/tests/embed_export_hash_stable.rs:32`. +- `crates/ail/tests/eq_ord_e2e.rs:139`. +- `crates/ail/tests/mono_hash_stability.rs:63-68,107-110`. + +Procedure per pin: run the test, read the `assertion failed: left == right` +actual value, paste the new hex into the pin, re-run. + +Run: `cargo test --workspace 2>&1 | rg 'hash|pin' ` until the pin tests pass. +Expected: each pin holds the post-migration hash; this is the one-time +corpus-wide reset (spec §6, "the single irreversible step"). + +- [ ] **Step 10: Flip the leak pin** + +- `examples/rc_let_implicit_returning_app.ail` — its return is now + `(own …)` (migrated in Phase A). Rewrite the file header and the + property-3 assertion from "Implicit leaks by design" / `live=1` to + "own-return frees correctly" / `live=0`. +- `crates/ail/tests/print_no_leak_pin.rs` — change the pinned + `AILANG_RC_STATS` expectation for this fixture from `live=1` to + `live=0`; update the doc comment (`:26`) that mentions + `ParamMode::Implicit`. + +Run: `cargo test -p ail --test print_no_leak_pin` +Expected: PASS with `live=0` (acceptance criterion 5). + +- [ ] **Step 11: Add the regression-pin + authoring-surface fixtures** + +Create these (each verified to `ail check` at the stated exit code — +see "Spec fixture parse-gate" below): + +`examples/own_return_provenance_reject.ail` (exit 1, `consume-while-borrowed`): +```ail +(module own_return_provenance_reject + (data Box + (doc "Heap cell holding one Int.") + (ctor Box (con Int))) + (fn passthrough + (doc "Already rejected today (consume-while-borrowed): own-return aliases a borrowed binder.") + (type + (fn-type + (params (borrow (con Box))) + (ret (own (con Box))))) + (params b) + (body b))) +``` + +`examples/own_return_provenance_let.ail` (exit 1) — body `(let y b y)`; +`examples/own_return_provenance_ctor.ail` (exit 1) — adds +`(data Wrap (doc "Wraps a Box.") (ctor Wrap (con Box)))` and body +`(term-ctor Wrap Wrap b)` with ret `(own (con Wrap))` (regime A). + +`examples/ownership_total.ail` (exit 0) — the post-cutover +authoring-surface module verbatim from spec 0062 §"User-facing" +(`list_length` borrows, `sum_list` owns, `main` builds `[1,2,3]`). + +Add a test asserting each provenance fixture still exits 1 under the +post-cutover check (extend `crates/ail/tests/mode_signature_rejects.rs`, +reusing the `check_rejects_with` helper from Task 1 Step 2): + +```rust +/// The own-return-provenance / regime-A shapes stay rejected by +/// `consume-while-borrowed` after the schema deletion (spec 0062 +/// already-green pins — these are NOT new checks). +#[test] +fn own_return_provenance_still_rejected() { + for f in ["own_return_provenance_reject.ail", + "own_return_provenance_let.ail", + "own_return_provenance_ctor.ail"] { + check_rejects_with(f, "consume-while-borrowed"); + } +} +``` + +- [ ] **Step 12: Add the parser bare-slot RED fixture + test** + +Create `examples/bare_slot_reject.ail`: +```ail +(module bare_slot_reject + + (fn id + (doc "MUST FAIL post-cutover: bare `(con Int)` slot carries no mode.") + (type + (fn-type + (params (con Int)) + (ret (con Int)))) + (params x) + (body x))) +``` + +Add a parser test (in `crates/ailang-surface/tests/`) asserting this +source now fails to **parse**: + +```rust +#[test] +fn bare_fn_type_slot_is_a_parse_error() { + let src = include_str!("../../../examples/bare_slot_reject.ail"); + assert!(ailang_surface::parse(src).is_err(), "bare slot must not parse"); +} +``` + +> A CLI-boundary variant is also acceptable (assert `ail check +> bare_slot_reject.ail` exits non-zero with a parse-error stderr) if +> the implementer prefers consistency with the other reject pins; the +> load-bearing behaviour is "bare slot → error". + +Also extend the round-trip test suite with a case proving a previously +round-tripping bare-slot input now fails to parse (spec Testing +§"Round-trip invariant"). + +- [ ] **Step 13: Update both contracts** + +`design/contracts/0008-memory-model.md`: + +Replace `:57-59`: +``` +`Own` and `Borrow` are the two modes; every fn-type slot carries one +explicitly. Ownership has no default — there is no bare/unannotated +mode (spec 0062 deleted the legacy `Implicit` state). +``` + +Replace `:62-65`: +``` +JSON canonical form: `param_modes` and `ret_mode` are always present +(one mode per slot). The pre-0062 elision (skipping all-`Implicit` +vectors for hash stability) is gone with the variant; the +corpus-wide hash reset that accompanied the deletion is a one-time +event recorded in `git log`. +``` + +Replace the `:249-251` bullet (Iter B): +``` + param itself. `Borrow` parameters are skipped: `Borrow` retains the + caller's ownership by contract. (There is no `Implicit` parameter + any longer — every param is `Own` or `Borrow`.) +``` + +Replace the `:260` clause (Iter A): +``` + the dec — only `Own`-mode scrutinees enable it; a `Borrow` scrutinee + would let the arm dec memory the caller still references. +``` + +Replace the `:297` clause (ret_mode): +``` + holds a view, not an own ref). Every `Term::App` callee now carries + an explicit `Own`/`Borrow` `ret_mode`; an `Own`-returning call is + trackable for scope-close drop, a `Borrow`-returning call is not + (and is in any case rejected at the signature — borrow-returns are + out of scope, spec 0062). +``` + +`design/contracts/0002-data-model.md`: + +Replace the comment `:272-273`: +``` +// `paramModes` and `retMode` are always present (one mode per slot). +// Full mode contract lives in contracts/0008-memory-model.md. +``` + +Replace the `ParamMode` block `:297-302`: +``` +"own" — (own T) — caller transfers ownership; callee consumes. +"borrow" — (borrow T) — caller retains ownership; callee may not consume. +``` +and the trailing prose (`:302-…`): +``` +Every fn-type slot carries `own` or `borrow`; ownership has no default +(spec 0062 deleted the legacy `implicit` state). The full mode contract +(codegen consequences, the over-strict-mode lint, the `Suppress` +mechanism) lives in [memory model](0008-memory-model.md); the four +language-design preconditions that make RC sound live in +[language constraints](0015-language-constraints.md). +``` + +### Phase D — remove throwaway, final gate + +- [ ] **Step 14: Remove the throwaway migration tool** + +Delete the `MigrateModes` arm + handler from `crates/ail/src/main.rs`, +delete `crates/ail/tests/migrate_modes.rs`, and delete +`for_each_fn_type_mut` from `ast.rs` (it has no other caller). (It +references `ParamMode::Implicit` and would not compile anyway.) + +- [ ] **Step 15: Final workspace gate** + +Run: `cargo build --workspace && cargo test --workspace` +Expected: 0 errors, all tests green (acceptance criterion 6). + +- [ ] **Step 16: Regression scripts + grep-clean gate** + +Run: +``` +python3 bench/check.py +python3 bench/compile_check.py +python3 bench/cross_lang.py +git grep -nE 'ParamMode::Implicit|fn_implicit|is_implicit|all_implicit|mode_eq|mode_slices_eq' crates/ +git grep -nE 'ParamModeImplicit' crates/ +``` +Expected: 0 regressions on all three scripts; both greps empty +(acceptance criteria 1). + +--- + +## Spec fixture parse-gate (planner self-review item 9 attestation) + +Every surface-language fixture inlined above was run through +`ail check` against current HEAD (2026-06-01, `target/debug/ail`): + +```text +ownership_total.ail : exit 0 ok (36 symbols) +borrow_return_reject.ail : exit 0 (legal today; check error post-cutover) +borrow_value_reject.ail : exit 0 (legal today; sig error post-cutover) +bare_slot_reject.ail : exit 0 (legal today; parse error post-cutover) +own_return_provenance_reject.ail : exit 1 [consume-while-borrowed] passthrough: `b` … +own_return_provenance_let.ail : exit 1 [consume-while-borrowed] passthrough: `b` … +own_return_provenance_ctor.ail : exit 1 [consume-while-borrowed] escape: `b` … (regime A) +``` + +All seven match the spec's claimed exit codes. The migration-tool unit +test fixture (Task 3 Step 1) is a Rust string literal, not a corpus +fixture, and is exercised by `cargo test -p ail --test migrate_modes`. + +## Commit shape (orchestrator note, not an implement step) + +Tasks 1, 2, and 3 each leave a green, independent tree and may be +committed separately before the cutover (`feat(check): borrow-return +reject`, `feat(check): borrow-over-value reject`, `chore: throwaway +mode-migration tool`). Task 4 is the single irreversible cutover commit +(`feat: delete ParamMode::Implicit — binary ownership modes (#55)`) +carrying the one-time hash reset. main only ever advances on a green +tree; nothing half-migrated is committed. +``` diff --git a/docs/specs/0062-eliminate-implicit-mode.md b/docs/specs/0062-eliminate-implicit-mode.md index 11d9112..c8cbf49 100644 --- a/docs/specs/0062-eliminate-implicit-mode.md +++ b/docs/specs/0062-eliminate-implicit-mode.md @@ -1,7 +1,11 @@ # Eliminate the Implicit ownership default — Design Spec **Date:** 2026-06-01 -**Status:** Draft — awaiting user spec review +**Status:** Approved (user, 2026-06-01). 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; +all are return/let/ctor consume positions, untouched by #56). **Authors:** orchestrator + Claude ## Goal