A correct div-by-zero fix is invisible: br_if on i32.eqz gives a disequality, which an interval cannot hold

[avrabe]

Found while closing FEAT-064 AC3 (PR #164). Reporting separately because the
consequence is consumer-facing, not just a precision number.

The behaviour

Take the canonical repair for a div-by-zero — branch away when the divisor is zero:

(func $d (param i32) (result i32) (local $r i32)
  block
    local.get 0
    i32.eqz
    br_if 0        ;; divisor == 0 -> leave, $r stays 0
    i32.const 10
    local.get 0
    i32.div_s
    local.set $r
  end
  local.get $r)

This is a genuine, semantics-preserving fix. It opens no new region and adds no
second i32.div_s, so obligation identity is untouched — measured: same site_key,
byte-identical obligation_ids before and after.

And div-by-zero still fires afterwards.

Mechanism

Not a bug in the guard recogniser — it fires correctly. try_guard_brif maps
(I32Eqz, BrIf) → GuardOp::Eq with c = 0:

• taken edge (divisor == 0) → refines to [0,0]. Correct, and useless: the
  division is on the other edge.
• fall-through edge licenses divisor != 0 → refine_interval returns the
  interval unchanged, and states the reason in the code itself:

(GuardOp::Eq, false) | (GuardOp::Ne, true) => return iv, // ≠ c: no interval

A disequality is a hole in the middle of a range. An interval lattice cannot
represent one. The transfer is sound — it simply carries no information for exactly
the fact the fix establishes.

Why it's worth its own issue

REQ-021 gates an AI agent on scry's verdict over its own edit. Under this behaviour, an
agent that fixes the bug correctly is told the obligation still stands. The
fix-verify loop cannot converge, and the gate is actively punishing the correct repair —
a false alarm, not a missing feature.

Measured across five guard shapes

fix shape	site identity	fix visible?
br_if out of a pre-existing block	survives (ids identical)	no — disequality
select-based guard	survives	no — select is unsupported-op
if/else, folded (if (result i32) …)	moves	no — region havoc'd
if/else, statement form	moves	no — region havoc'd
divisor → constant	survives	not a fix — deletes the parameter's role

Note the if/else rows lose both identity and precision (the region is havoc'd, with
an honest UnmodeledControlFlow gap per REQ-017). Only the br_if and select rows
keep identity — those are where a fix could become adjudicable.

Direction (FEAT-089, not yet a design)

Don't try to encode != 0 in the interval domain — the lattice genuinely cannot
hold it, and widening to disjunctions was already rejected for the bounds decision.
Instead carry a narrow predicate fact ("this local is known non-zero on this path") that
only the div/rem trap check consults — the same shape as FEAT-084's known-bits
reduction: a targeted fact feeding one decision, not a new general domain.

The soundness obligation is small and statable: the fact holds only on the fall-through
edge of a guard whose taken edge pins the local to zero, and must be invalidated by
any write to that local (local.set/local.tee, a clobbering call, a loop back-edge).
That invalidation is the first thing a clean-room should attack.

Also: signed-overflow at the same site must be unaffected — != 0 says nothing
about INT_MIN / -1, and both obligations sit at that one site.

Modelling select is a separate bounded slice; it's the shape where identity is already
free.

Not claimed

How common any of these shapes is in real fixes. Five hand-written fixtures, zero
observed repairs — this establishes which shapes behave how, not their prevalence.
The corpus in #126 could answer prevalence and hasn't been asked.

[avrabe]

Fixed in #183 (FEAT-089) — and the measurement afterwards is the more useful half.

The fix

A narrow predicate fact (nonzero_locals), established only on the fall-through edge of
an eqz-guard and consulted only by the div/rem trap check. Not an attempt to encode
≠ 0 in the interval lattice, which genuinely cannot hold a hole in a range.

Measured on the canonical repair (br_if out of a pre-existing block):

div-by-zero  before=1  after=0
proven-safe  before=1  after=2

The fix is now visible. div_s/div_u/rem_s/rem_u all consult it; signed-overflow
at the same pc is deliberately unaffected, since ≠ 0 says nothing about INT_MIN / -1.

Soundness was the first target

This makes scry emit PROVEN-SAFE where it previously did not, so a fact surviving a write
is a false proof. Every invalidation path is killed and pinned by a test: local.set,
local.tee, any call (deliberately conservative), loop back-edge, every fixpoint pass
start, block exit, havoc_region, degrade-to-⊤. Joins meet facts, never union.

Forcing the fact always-true kills 20 tests — including pre-existing FEAT-045/055/064/
065/077/087 ones, not just the new adversarial set.

What it does NOT do — two honest results

No change on a real module. scry_mcdc.wasm reports identical counts before and after
(21 div-by-zero PotentialTrap / 7 ProvenSafe / 62 proven-safe). LLVM emits constant
divisors there and the local.get; i32.eqz; br_if idiom precedes no division. The target
is the agent repair loop, not this corpus.

It does not unblock REQ-021. The adjudicator still returns uncertain, because
FEAT-065's discharged requires the function's operator shape unchanged — and adding
a guard changes the shape. That term exists to stop a cardinality-preserving delete+insert
being a false discharge, so the tension is real: the conjunct that prevents a false
discharge also blocks every genuine repair that adds a guard. A shape hash can't tell
"guard inserted" from "same-kind operator swapped".

That's now REQ-021's recorded blocker, with what would actually resolve it: a shape
comparison finer than a hash, or corroboration of the open→safe transition by content
rather than structure.

One thing found on the way

proven-safe advisories were colliding — two distinct facts at one pc (i32.div_s
proving both divide-by-zero-safe and overflow-safe) shared a single obligation_id.
Verified main vs branch: main gives 2 advisories with 1 distinct id; the branch gives 2.
The whole FEAT-064/077/087 identity arc missed it because every identity test targeted the
open-obligation side. Now keyed by the obligation code discharged; site_key and
group_key untouched.