Executable plan for the second of two iterations delivering spec 0060's
mir.3 row. A focused recon (the anon-temp gate + the per-arg mode
sources) established two refinements to the spec sketch, both locked in
the plan:
1. module_def_ail_types is deleted in mir.3b, not mir.5. A grep proved
self.module_def_ail_types has exactly ONE reader — the emit_call
anon-temp borrow-slot drop gate. The own-param drop reads param_modes
from the def's own f.ty, not this table. So switching that gate onto
MArg.mode leaves the table dead; deleting it now is the clean move.
mir.5's "last re-derivation residue" shrinks to element-type/Term::New.
2. MArg.mode is filled for App args only; MTerm::Let.mode is not filled.
Only App args have a real per-arg mode source (the callee
Type::Fn.param_modes). Do/Ctor/Recur args have no per-arg mode
(EffectOpSig/Ctor.fields/loop-binders carry none) -> stay Owned
default. Let.mode has no source (ast::Term::Let has no mode field)
and no consumer (the let-drop gate reads consume, not Let.mode) ->
stays Owned.
Safety property (recon-confirmed on the #43 anon-temp witness): MArg.mode
is filled from the same callee fn-type the gate read from the table, so
the drop fires identically. For (app RawBuf.get (app RawBuf.set …) 0),
RawBuf.get's param 0 is borrow -> args[0].mode = Borrow, exactly the
value module_def_ail_types yielded.
Four tasks: (1) producer fills App-arg MArg.mode via a param_mode_at
helper; (2) codegen gate reads arg.mode + delete module_def_ail_types
(field + construction + threading, compiler-completeness-checked);
(3) producer pin (App arg mode == Borrow) + the live=0 anon-temp
acceptance (raw_buf_owned_drop_balances_rc_stats); (4) record the
refinements in spec 0060. No new .ail fixture (reuses raw_buf_drop_min.ail).
Brummel
0bd7f47fad