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 `<name>$<n>` (`ailang-core::desugar`), so a shadow-rebind idiom
 like `(let buf (new…) (let buf (set buf…) … (get buf)))` becomes