From 54d8f0c6603ef25dd9664312ece496d932293515 Mon Sep 17 00:00:00 2001 From: Brummel Date: Tue, 2 Jun 2026 15:51:35 +0200 Subject: [PATCH] docs(contracts): record the leak-class branch-param drop gate (#63) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Audit of the #63 leg-3 cycle flagged ledger drift: 0008-memory-model.md enumerated the Own-param drop gates as a closed set, but the leak-class branch-param fall-through drop now ships in codegen with no home in the contract. Per the honesty-rule (a contract describes the actual present state), reconcile it. Adds the fourth gate with its three soundness guards — disjointness from the fn-return dec (partition by aggregate: ==0 vs >=1), no-use-after-free (the use-after-consume rejection makes an aggregate>=1 param dead past the construct), and the heap-RC-ADT type precondition (field_drop_call != ailang_rc_dec; closure/static-Str/Var params are skipped to avoid a static-constant underflow). Notes that the pre-tail-call Own-param dec now shares the per-branch model (gate-source = MArm.consume) and updates the binder-name-injectivity precondition to cover the per-branch consume maps carried on MArm / MTerm::If and correlated by the traversal-order cursor. The accepted heap-capturing-closure-in-leak-class leak (soundness over completeness) is recorded in the backlog as Brummel/AILang#67. refs #63 --- design/contracts/0008-memory-model.md | 49 ++++++++++++++++++++++++--- 1 file changed, 44 insertions(+), 5 deletions(-) diff --git a/design/contracts/0008-memory-model.md b/design/contracts/0008-memory-model.md index 6d78f30..ebcfee9 100644 --- a/design/contracts/0008-memory-model.md +++ b/design/contracts/0008-memory-model.md @@ -279,12 +279,51 @@ emit drop calls: the requirement that every ptr-typed slot in the active ctor's pattern is in `moved_slots[scrutinee]`. +- **Leak-class branch-param drop.** When a `match`-arm or + `if`-branch falls through (no tail-call) and an `Own`, ptr-typed + parameter is LIVE on that branch (its per-branch consume is `0`) + but CONSUMED on a sibling branch (per-fn aggregate + `consume_count >= 1`), it is dec'd at that branch's close, before + the `br` to the join — never at the join, which is a merge point + that cannot tell the consumed path from the live one. Three guards + make this sound: + - *Disjointness from the fn-return dec.* The fn-return Own-param + dec above owns the `aggregate == 0` class (live on every path); + this gate owns the `aggregate >= 1` class. The predicates are + mutually exclusive, so no param is dropped twice — the fn-return + dec is left unchanged and no tail-position analysis is required. + - *No use-after-free.* An `aggregate >= 1` param is provably dead + past the branch construct: the checker rejects use-after-consume + (`use-after-consume`), so a param consumed on any branch cannot + be used afterwards. The per-branch drop is therefore + path-terminal regardless of whether the construct sits in tail + position. + - *Heap-RC-ADT type precondition.* The drop fires only for a param + whose static type resolves to a real per-type heap drop fn + (`field_drop_call != "ailang_rc_dec"`). Closure (`Type::Fn`), + static-`Str`, and `Type::Var` params route to the bare + `ailang_rc_dec`, which would underflow on a static closure-pair / + static-`Str` constant (`.rodata`, no rc-header); they are + skipped. A heap-capturing closure in this exact position leaks + rather than double-frees — soundness is preferred over + completeness (tracked in the backlog). + + The pre-tail-call Own-param dec (the drop of an `Own` param a + tail-call arm neither forwards nor consumes) shares this + per-branch model: its gate-source is the per-arm `consume_count` + (`MArm.consume`), which for an `aggregate == 0` param is identical + to the old aggregate gate. + **Per-fn binder-name injectivity (a precondition of every gate -above).** All three drop gates read `consume_count` from the -uniqueness side-table keyed by `(def_name, binder_name)`. Codegen -looks up by the binder's source name and must resolve the binding it -means — so within one `def_name`, every `binder_name` must denote -exactly one binding. The desugar pass guarantees this: it +above).** Every drop gate reads `consume_count` from the uniqueness +side-table keyed by `(def_name, binder_name)`; the two per-branch +gates (leak-class drop, pre-tail-call Own-param dec) additionally read +the per-branch consume map carried on `MArm.consume` / +`MTerm::If.{then,else}_consume`, correlated to the MIR branch nodes by +a traversal-order lock-step cursor in `lower_to_mir` (the AST carries +no node id). Codegen looks up by the binder's source name and must +resolve the binding it means — so within one `def_name`, every +`binder_name` must denote exactly one binding. The desugar pass guarantees this: it alpha-renames any binder whose name shadows an enclosing binding to a fresh `$` (`ailang-core::desugar`), so a shadow-rebind idiom like `(let buf (new…) (let buf (set buf…) … (get buf)))` becomes