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
Brummel
54d8f0c660