From 19757480b707e7acf1cc2d79c38d7d2d235b6a8f Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 00:45:06 +0200 Subject: [PATCH] audit(0064/cutover): record shipped drop machinery + retire dead desugar arm MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cycle-close tidy for the #55 cutover (its audit drift-resolution). Architect drift review found the design ledger out of step with the codegen that the cutover shipped, plus two debt items; regression green (733 passed / 0 failed across the workspace). design/contracts/0008-memory-model.md — the Codegen contract described the drop-emission *gates* but not the drop machinery the cutover landed. Added three subsections recording the present state (honesty rule): - Per-monomorph drop fns for polymorphic ADTs (crates/ailang-codegen/ src/dropmono.rs: collect_drop_monos / DropAdtMeta, the suffix scheme, value-field-skip on the substituted field type). Ratified by alloc_rc_value_type_field_is_not_rc_dec_dropped. - String-literal rep promotion at owned drop sites (StrRep::Static→Heap on a Str literal flowing into an Own slot the callee drops; gated strictly on Own). Ratified by own_str_literal_arg_is_dropped_exactly_once. - Same-constructor arm grouping in match desugar (build_chain / build_ctor_group bind ctor fields once). Ratified by lit_pat_ctor_tail_drop_single_drop + lit_pat_nil_scrutinee_single_drop. crates/ailang-core/src/desugar.rs — build_chain routes every Ctor-head arm (including a length-1 run) through build_ctor_group, so desugar_one_arm's Pattern::Ctor arm was unreachable dead code duplicating the bind-once lowering. Replaced it with unreachable! naming the invariant, and corrected two stale doc comments (the module-header step 4 and the desugar_one_arm doc still described it as handling ctor arms, and mislabeled the Lit lowering as Term::Match — it is Term::If). Full workspace stayed green, confirming the arm was dead. crates/ailang-check/src/linearity.rs — renamed test implicit_fn_is_exempt → own_param_consumed_once_is_clean. Post-0062 there is no Implicit and no exemption; the test pins the ordinary single-Own-consume clean path. Did the desugar + linearity edits inline rather than via an agent: I had already loaded build_chain/build_ctor_group/desugar_one_arm to prove the arm dead, and a sub-agent would have redone the same reading. --- crates/ailang-check/src/linearity.rs | 8 +-- crates/ailang-core/src/desugar.rs | 72 ++++++++++----------------- design/contracts/0008-memory-model.md | 67 +++++++++++++++++++++++++ 3 files changed, 99 insertions(+), 48 deletions(-) diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index e769782..38b54cd 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -1897,10 +1897,12 @@ mod tests { ); } - /// All-Implicit fn → check is skipped, no diagnostics, even if the - /// body would trigger a use-after-consume under explicit modes. + /// A single `Own` param consumed exactly once (the body returns it) + /// is clean — no `over-strict-mode`, no use-after-consume. (Pre-0062 + /// this was the `Implicit`-exemption case; post-cutover there is no + /// `Implicit`, so it pins the ordinary single-consume path.) #[test] - fn implicit_fn_is_exempt() { + fn own_param_consumed_once_is_clean() { let m = Module { schema: ailang_core::SCHEMA.into(), name: "t".into(), diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index fdb1c91..becde37 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -37,17 +37,21 @@ //! arms returned a non-Unit type to carry a synthetic `_` arm //! dominating the terminator. The polymorphic `__unreachable__` //! removes that workaround. -//! 4. Each arm is lowered via `desugar_one_arm`: -//! - `Pattern::Wild` → arm body (catch-all; later arms are dropped). -//! - `Pattern::Var { name }` → `Let { name = scrutinee_var; body }`. -//! - `Pattern::Lit { lit }` → `Term::If { cond = (== s_var lit), -//! then = arm.body, else_ = fall_k }` (Iter 16c). After this +//! 4. `build_chain` lowers the arms head-first: +//! - A maximal run of consecutive arms sharing the head arm's outer +//! ctor + arity is lowered together via `build_ctor_group`: lift +//! each ctor field to a fresh var, emit ONE `Term::Match` over the +//! flat ctor pattern (binding the fields once) plus a wildcard +//! fall-through, and thread the bound vars through every arm's +//! sub-patterns via `wrap_sub`. Binding once keeps the ctor's +//! owned children under a single match scope (no re-match, no +//! re-drop). +//! - A non-ctor head (Wild/Var/Lit) is lowered via `desugar_one_arm`: +//! `Pattern::Wild` → arm body (catch-all; later arms are dropped); +//! `Pattern::Var { name }` → `Let { name = scrutinee_var; body }`; +//! `Pattern::Lit { lit }` → `Term::If { cond = (== s_var lit), +//! then = arm.body, else_ = fall_k }` (Iter 16c). After the Lit //! rewrite, no `Pattern::Lit` reaches typecheck or codegen. -//! - `Pattern::Ctor { ctor, fields }`: lift each field to a fresh -//! var, build a flat outer pattern, walk fields right-to-left -//! wrapping inner sub-patterns via `wrap_sub`. Emit a -//! `Term::Match` with two arms: the flat ctor and a wildcard -//! fall-through into the rest of the chain. //! //! `wrap_sub(fv, sub, body, fall_k)` recurses on `sub`: //! - `Var(n)` → `Let(n, Var(fv), body)`. @@ -1259,10 +1263,11 @@ impl Desugarer { } } - /// Lowers one arm into a term. Wild/Var arms drop the chain (the - /// arm matches everything); Lit and Ctor arms emit a `Term::Match` - /// with the desugared head pattern as the first arm and a - /// wildcard fall-through to `fall_k`. + /// Lowers one non-constructor arm into a term. Wild/Var arms drop + /// the chain (the arm matches everything); a Lit arm emits a + /// `Term::If` discriminating on `(== s_var lit)` with `fall_k` as + /// the else-branch. Ctor-head arms never reach here — `build_chain` + /// routes them through `build_ctor_group` (bind-once lowering). fn desugar_one_arm(&mut self, s_var: &Term, arm: &Arm, fall_k: Term) -> Term { match &arm.pat { Pattern::Wild => arm.body.clone(), @@ -1282,37 +1287,14 @@ impl Desugarer { else_: Box::new(fall_k), } } - Pattern::Ctor { ctor, fields } => { - // Lift each field to a fresh var; build the flat outer - // pattern, then walk right-to-left wrapping each inner - // sub-pattern via `wrap_sub` so the deepest field is - // matched first inside-out. - let fresh_vars: Vec = fields.iter().map(|_| self.fresh()).collect(); - let flat_fields: Vec = fresh_vars - .iter() - .map(|n| Pattern::Var { name: n.clone() }) - .collect(); - let mut inner = arm.body.clone(); - for (sub, fv) in fields.iter().zip(fresh_vars.iter()).rev() { - inner = self.wrap_sub(fv, sub, inner, &fall_k); - } - Term::Match { - scrutinee: Box::new(s_var.clone()), - arms: vec![ - Arm { - pat: Pattern::Ctor { - ctor: ctor.clone(), - fields: flat_fields, - }, - body: inner, - }, - Arm { - pat: Pattern::Wild, - body: fall_k, - }, - ], - } - } + // `build_chain` routes every Ctor-head arm — including a + // length-1 run — through `build_ctor_group`, whose bind-once + // lowering is the live path. `desugar_one_arm` therefore only + // ever sees Wild/Var/Lit heads. + Pattern::Ctor { .. } => unreachable!( + "build_chain routes Ctor-head arms through build_ctor_group; \ + desugar_one_arm sees only Wild/Var/Lit" + ), } } diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md index 22bdf46..1783c42 100644 --- a/design/contracts/0008-memory-model.md +++ b/design/contracts/0008-memory-model.md @@ -324,6 +324,73 @@ returns that are not `Type::Con` (e.g. unresolved type vars on a polymorphic call's pre-monomorphisation site; the monomorphised copies resolve to concrete drop fns). +#### Per-monomorph drop fns for polymorphic ADTs + +A polymorphic ADT (`Box a`, `Pair a b`) has no single correct +drop fn: a ctor field typed at a type-var lowers to `ptr` and is +`rc_dec`'d, but at a value-type instantiation (`Box Int`) that +field is an inline `i64`, so dec'ing it dereferences a scalar. +Codegen therefore emits **one drop fn per (polymorphic-ADT, +concrete instantiation)** and makes the dec-vs-skip decision on +the *substituted* field type: a value-type field +(`Int`/`Bool`/`Float`/`Unit`) is skipped (inline scalar, no RC); +a heap field is dec'd through its own per-monomorph drop symbol +so the cascade composes. + +The workspace-global collection lives in +`crates/ailang-codegen/src/dropmono.rs` (`collect_drop_monos`, +`DropAdtMeta`), built once before the per-module codegen loop and +shared by reference with every `Emitter`. Symbol naming: + +- A concrete-monomorphic ADT (declared `vars` empty: `IntList`, + `Ordering`) keeps its un-suffixed `drop__` / + `partial_drop__` symbol byte-for-byte (the `ir_snapshot` + goldens pin these). +- A polymorphic ADT instantiation gets a mono suffix mangled + exactly as `ailang_check::mono::mono_symbol_n` mangles fn + symbols (`drop__Pair__Int_Int`; compound args hash-route to + stay bounded). +- Intrinsic-storage types (`RawBuf`) are polymorphic but use the + flat intrinsic drop path and are NOT suffixed (their drop is + element-type independent; the golden pins `drop__RawBuf`). + +A drop fn and its call sites consult the same `DropAdtMeta` +(emission + manglers in `drop.rs`, call-site manglers in +`match_lower.rs`), so they always agree on the symbol — a +mismatch would be a link error. Ratified by +`alloc_rc_value_type_field_is_not_rc_dec_dropped` in +`crates/ail/tests/drop_value_field_no_segfault_pin.rs`. + +#### String-literal rep promotion at owned drop sites + +A `Str` literal carries a `StrRep`: `Static` (header-less rodata +constant) or `Heap` (rc-headered owned slab). An `Own`-mode drop +path emits `ailang_rc_dec` on the value; dec'ing a +`StrRep::Static` reads `payload - 8` (the length field) as a fake +refcount and `free()`s a static address — a segfault. Codegen +therefore promotes a `Str` literal that flows into an `Own` slot +the callee will drop from `Static` to `Heap` (codegen then emits +`ailang_str_clone` → refcount 1, and the single dec is sound). +The promotion is gated **strictly on `Own`**: a `Borrow` slot +fires no `rc_dec`, so a borrow-position literal stays +`StrRep::Static` (no spurious clone). +`crates/ailang-check/src/lower_to_mir.rs` applies this at four +sites — the `Term::App` owned-arg site (`is_str_ty` + `Own`) and +the loop-carried seed/tail/recur sites of a `Str`-returning loop +body. Ratified by `own_str_literal_arg_is_dropped_exactly_once` +in `crates/ail/tests/e2e.rs`. + +#### Same-constructor arm grouping in match desugar + +`crates/ailang-core/src/desugar.rs` groups consecutive match +arms that share a head constructor (`build_chain` / +`build_ctor_group`) into a single match over that constructor's +fields, binding the fields once. This keeps a literal sub-pattern +(`(Cons (pat-lit K) _)`) from re-matching — and re-dropping — the +same owned scrutinee tail across the literal-discriminating arms. +Ratified by `lit_pat_ctor_tail_drop_single_drop` and +`lit_pat_nil_scrutinee_single_drop` in `crates/ail/tests/e2e.rs`. + #### Arg-position policy for compound AST nodes The uniqueness and linearity passes walk arguments of compound