feat(mir): admit heap-owning tuple fields in functional-record-update carry

[gertybotbot]

Closes the fail-closed NYI in #2207 for heap-owning tuple fields.

What changed

sound_carry in the functional-record-update carry pre-flight now admits
ty_is_heap_owning_tuple. No new recursive carry spine is authored.

The protection comes from derive_owned_record_drop_allowed, not the tuple-binding
prover: the tuple-typed RecordFieldLoad destination is recognised as a heap-owning
field binder, and its escape into the result's RecordInit excludes the consumed base
root from RecordInPlace. The result therefore receives the tuple's complete nested
drop obligation without the base releasing it a second time.

The functional change is 4 lines in hew-mir/src/lower/expr.rs; the rest is tests and
the soundness comment at the carry gate.

Verification

Suites at head 42ca548ee:

• cargo test -p hew-cli --test funcupdate_consume_semantics — 49 passed / 0 failed
• cargo test -p hew-mir — 565 passed / 0 failed
• cargo fmt --all -- --check — rc=0

Six widened shapes accept and run clean, including the full scope implied by the tuple
predicate:

• tuple nested in tuple (string, (string, i64))
• tuple of tuples ((string, i64), (string, i64))
• tuple carrying a Vec (Vec<string>, i64)
• tuple carrying an owned record (Inner, i64)
• tuple carrying an Option payload (Option<Inner>, i64)
• tuple carrying a user-enum payload (Payload, i64)

The Linux allocator checks used glibc's
MALLOC_CHECK_=3 MALLOC_PERTURB_=165; Guard Malloc + MallocScribble is the
authoritative Darwin oracle and was independently verified in review.

No per-frame leak on the collection-bearing shape. The sweep stayed flat across
50k/100k/200k frames: 56800 / 56928 / 56976 KB maxRSS.

Bounded on both sides

Bare Option<Inner> and bare heap-payload enum fields remain fail-closed. An Option
or enum nested inside the admitted tuple transfer boundary is covered by explicit
fixtures. Closure and handle families also remain fail-closed.

A tuple with no heap fields ((i64, i64)) still rejects with the NYI. That is a
coverage gap, not a soundness one (a plain-scalar tuple is trivially bit-copyable), and
it is pinned by a named test. Lifting it is a separate follow-up.

Scope

This PR lifts heap-owning tuple fields, including their recursively owned payloads.
Direct/bare Option and enum fields, handles, and closures remain untouched.

Refs #2207

[gertybotbot]

CI update at head 6c14269c: both defects I introduced are fixed, and the one remaining failure looks unrelated to this PR.

Fixed — Clippy & format now passes (was the cargo fmt --check failure), and the E0061 break is gone (upstream added a 4th &LifecycleRegistry param to ty_is_heap_owning_tuple after I branched; rebased and now passing &self.lifecycle_registry). All Linux build/test/shard jobs pass.

Remaining failure, and I do not believe it is mine: Build & test (macOS arm64), step 15, job 94094963485 — 13066 tests run: 13065 passed, 1 failed. The failure is hew-cli::wasi_run_e2e native_actor_periodic_timer_reaches_quiescence (wasi_run_e2e.rs:788, "the native periodic handler never fired").

Why I read it as a timing flake:

• Disjoint blast radius. This PR is a 4-line sound_carry widening in hew-mir plus tests. The failing assertion is about a runtime periodic timer firing before shutdown drain.
• The shape is a race, not a miscompile. The program exited 0 and printed spawned and done but not tick 1 — the handler simply never ran before quiescence. A wrong carry decision would corrupt or crash, not skip a timer tick.
• The relevant runtime fix is already in this branch. 3a0bfb5fa fix(runtime): quiesce periodic timers before shutdown drain is an ancestor of this head, so this looks like residual jitter under macOS-runner load.
• Not reproducible locally: passes, and 12/12 consecutive runs green.

I do not have re-run rights (gh run rerun --failed → "Must have admin rights to Repository"), so I cannot clear it myself — a re-run from someone with upstream access would confirm. Linux gates is still pending, so this is not a green verdict yet.

[slepp]

The lowering change itself held up under everything I threw at it — Guard-Malloc with scribble/guard-edges, a 100k-iteration reassign-loop carry, and 50k/100k/200k frame sweeps with zero RSS slope. Two things need addressing before this can land:

1. Admitted scope is wider than the stated scope. ty_is_heap_owning_tuple is a pure shape predicate (Tuple(_) + any drop obligation), so the carry now also admits a tuple containing an Option payload (record O { maybe: (Option<Inner>, i64), tag: string }) and a tuple containing a heap-payload user enum — both pass hew check today, while the bare-field forms are still rejected. The description says Option/enum are untouched, and there's no fixture or soundness argument for either newly admitted family. My probes for both ran clean under the malloc oracles, so I don't have evidence of unsoundness — but they need fixtures and a stated argument, or the predicate needs narrowing to what the PR argues for.

2. The soundness comment names a prover that doesn't run on this path. derive_tuple_composite_drop_allowed's candidate set is tuple bindings; in these fixtures the carried tuple is a record field, never a binding, so that prover has no candidate. What actually protects the base is derive_owned_record_drop_allowed's escape rule — the tuple-typed RecordFieldLoad dest counts as heap-owning and its escape into the result's RecordInit drops the base root from RecordInPlace. The mechanism is real; the committed explanation attributes it to the wrong prover. Please repoint the comment at the escape rule.

One smaller note: MALLOC_CHECK_/MALLOC_PERTURB_ are glibc-only, so it's worth stating the platform in the test plan — the suite's own module doc names Guard-Malloc + MallocScribble as the authoritative oracle, and that's what I verified with.

The (i64, i64) conservative-reject follow-up you propose sounds right; happy to see that as a separate PR.

[gertybotbot]

Addressed both requested changes at 42ca548ee:

• Corrected the soundness explanation in the carry gate, test docs, and PR body: the protecting mechanism is derive_owned_record_drop_allowed recognizing the tuple-typed field-load destination as a heap-owning binder, then excluding the consumed base when that binder escapes into RecordInit.
• Added executed fixtures for the full admitted predicate scope: tuple-contained Option<Inner> and tuple-contained heap-payload user enum. Bare Option/enum fields remain fail-closed.
• Clarified that MALLOC_CHECK_/MALLOC_PERTURB_ are the Linux/glibc check and Guard Malloc + MallocScribble is the Darwin oracle.

Local verification at that head: funcupdate_consume_semantics 49/0, hew-mir 565/0, and cargo fmt --check rc=0.

[slepp]

The current head is green, and the requested scope and soundness corrections are present in 42ca548ee. I consider the code ready for a fresh review verdict; the existing changes-requested state is the remaining gate.