havoc_region launders obligations: a typed block/if with an empty write set emits no trap check, no gap, no advisory

[avrabe]

The hole

havoc_region never interprets the region body, and it records a gap only when !written.is_empty() || region_has_call. So a typed region that writes no local and contains no call disappears with no record of any kind:

;; the divisor is still an unconstrained param — the obligation is LIVE
(module (func (export "b") (param i32) (result i32)
  (block (result i32) i32.const 10 local.get 0 i32.div_s)))

Measured: trap_checks.is_empty() && gaps.is_empty() && advisories.is_empty(). The bare (unwrapped) version reports a div-by-zero POTENTIAL-TRAP as expected. (if (result i32) …) behaves identically.

Why it matters beyond precision

This breaks the invariant REQ-017 exists to establish — "every place the analysis is conservative is recorded as data, never as silence." Here scry is maximally conservative (it interprets nothing) and says nothing at all. Three consequences:

1. The gap report is not complete. An assessor reading gaps as the scope boundary gets a region that was never analysed and never disclosed.
2. It is a one-line laundering vector. Wrapping a flagged expression in a typed block removes it from the report entirely — no understanding of any internal scheme required.
3. It promotes to a WRONG VERDICT in FEAT-065. The adjudicator (PR FEAT-065: scry adjudicates its own oracle (verify_against), conservative by construction #120, draft) reads "absent from the after-run" as removed-with-code — literally "the site no longer exists" — while the code is still there and the obligation still live. Found by adversarial review; recorded in DD-021's limitations as finding (3).

Fix

Emit a gap for every havoc'd region, unconditionally — drop the !written.is_empty() || region_has_call guard. The guard was added (correctly, for FEAT-043) to ensure a void call inside an if still recorded a gap; the lesson generalises: the reason to record a gap is that the region was not interpreted, not that it happened to write a local. An empty write set makes the region cheaper to havoc, not more analysed.

Until that lands, FEAT-065 must treat "site absent from a function that degraded or gained a havoc region" as uncertain rather than removed-with-code.

Relates: REQ-017 (gap reporting), FEAT-040 (gap records), FEAT-046 (OOB verdicts), DD-021 finding (3).