97% of real-world modules hit unsoundness-fallback, only 18% of memory-touching modules fully provable — operator ranking, and 579 fallbacks that name no operator

[avrabe]

Running the released analyzer over a real-world corpus, 97% of modules hit
unsoundness-fallback and only 18% of memory-touching modules have all their accesses
provable. Posting the operator ranking behind that, since it is a directly actionable priority
list — and one diagnostic-quality issue that makes the largest bucket unusable.

This is not a soundness complaint. scry behaved correctly on every probe I ran: it widens to top,
it refuses to prove what it cannot, and it announces every fallback through a dedicated severity.
The question here is purely how much of that value is reachable on real code today.

Measured on scry-3.2.4-wasm32-wasip2.wasm (release asset) via
wasmtime run --invoke 'analyze([...], {...})'.

Coverage on real-world modules

Corpus: 906 artifacts (toolchain output from this org's repos + components pulled from
wasm.directory). 530 are core modules; 468 fit within the ~150 KB that the --invoke argv path
allows.

analysed (ok):                        281
analyzer error:                        82      (uncharacterised — empty stderr in my capture)
crash:                                  2      (filed separately)
timed out at 60s:                     103      (timing only, shared machine — not a defect claim)

modules with a memory access:         122
  of those, ALL accesses provable:     22      (18%)
modules hitting unsoundness-fallback: 272 of 281   (97%)

The mechanism is what makes the fallback rate matter: each unmodelled operator degrades that
function's locals to top, so everything downstream in the function becomes unprovable. One
i32.and early in a function can cost every subsequent access in it.

The operator ranking

From scry's own fallback diagnostics, aggregated across the corpus:

count	operator
579	<unsupported> — scry does not name it (see below)
433	i32.and
203	select
151	unreachable
61	nop
46	i32.or
41	i32.xor
40	i32.shl
25	i32.shr_s
12	i32.shr_u
3	drop

Three clusters stand out, in what looks like decreasing value-per-effort:

1. The trivial ones — nop, drop, unreachable (215 combined). These have no effect on
   locals at all (unreachable makes the rest of the block dead). Modelling them as identity
   should be nearly free and immediately stops poisoning the functions that contain them.
2. The bitwise/shift family — and, or, xor, shl, shr_s, shr_u (597 combined). A
   coherent group, and the one that matters most for bounds work specifically: i32.and with a
   constant mask is the idiom producers emit to constrain an address, so it is exactly the
   operator whose absence blocks the bounds proofs synth's --proven-safe wants. Interval
   analysis of and against a constant mask gives a tight bound directly.
3. select (203). Needs a join of the two arms, more work than the above but standard.

For context on (2): I probed the boundary behaviour by hand and scry is byte-exact on constant
addresses — it proves i32.load at 65532 (last byte 65535, fits) and refuses 65533 (last byte
65536, overruns by one) against a 64 KiB region. The precision is there; i32.and is what stops
it being reachable on real code, where addresses are masked rather than constant.

The <unsupported> placeholder — 579 fallbacks that name nothing

The largest bucket is not an operator. scry emits the literal string:

severity: unsoundness-fallback, func-index: 0, pc: 3,
message: "unsupported operator at v0.2 AC#1: <unsupported> — locals degraded to top"

So for the majority of fallbacks a consumer is told that analysis degraded but not what
caused it. That makes the diagnostic non-actionable in exactly the cases where it would be most
useful, and it is presumably a cheap fix — the operator is known at the point the fallback is
raised. Naming it would also turn this whole ranking into something scry can report about itself
rather than something that has to be reconstructed from outside.

Why this ranking is worth having

synth's --proven-safe consumes proven-safe access sites to elide bounds guards (synth#901/#932);
scry's roadmap FEAT-069 is the producer. On today's numbers that channel would carry proofs for
roughly one in five memory-touching modules, and the single operator most responsible is the
constant-mask idiom that address-bounding code is written in. Modelling clusters (1) and (2) looks
like it would move that number substantially for a modest amount of work.

Happy to re-run the corpus against a branch and report the delta — the harness is scripted and the
comparison is cheap.

[avrabe]

The <unsupported> half is fixed in #127. The operator ranking is the more valuable part of this issue and I'm treating it separately — see below.

The 579 placeholders

You called it as "presumably a cheap fix — the operator is known at the point the fallback is raised." It was cheaper than that: the fix already existed and was wired to the wrong surface.

op_report_name() falls back to the operator's Debug variant name precisely so an unsupported op is still identified, and it was already used for the gap records. The fallback diagnostic used the lower-level op_name(), which returns the literal <unsupported> for anything outside a short hardcoded list. So at one pc, the gap named the operator and the diagnostic didn't — two surfaces disagreeing about the same event. One word.

I've recorded it as a REQ-017 defect rather than a cosmetic one. "No silent ⊤" isn't met by a record that announces a degradation without identifying its cause — and an unnameable fallback is marginally better than silence for a human but worse for an agent, which can't ask a follow-up question. Your point that this "would turn the ranking into something scry can report about itself" is exactly right and is the reason it's classed that way.

On the ranking

Not in v3.2.5 — naming ≠ modelling, and I don't want the release note to imply otherwise. Two notes for when it is scheduled:

Your cluster (2) may be cheaper than it looks. scry already ships a known-bits × interval-guarded congruence domain (scry-sai-bits, FEAT-037) that models and/or/xor/shl/shr over wrapping ints, including the constant-mask idiom you identified. It runs as a separate straight-line pass feeding bit_facts; the main interpreter's operator table is what falls back. So this looks closer to wiring an existing domain into the fixpoint than to building one — I haven't confirmed the effort, but it changes the estimate enough to be worth saying before anyone budgets it.

Your (1) → (2) → (3) ordering matches my read. unreachable is the one to watch: modelling it as identity would be wrong (the rest of the block is dead, not unchanged), so it belongs with select in effort terms even though it sits in the trivial cluster by count.

Yes please to the re-run offer. A before/after on the same corpus is the only honest way to state what the modelling work bought, and a number you produced independently is worth more than one I produce. Related: #128 is the first of your 82 analyzer errors with a name and a minimal public reproducer.

[avrabe]

v3.2.5 is out — the <unsupported> half of this issue ships in it. Leaving this issue open for the operator ranking, which is the substantive part and isn't in this release.

Verified against the published artifact rather than a local build: scry-3.2.5-wasm32-wasip2.wasm on the crash shape from #125 returns ok(...), where scry-3.2.4-wasm32-wasip2.wasm gives wasm trap: unreachable instruction executed.

Fixed at two sites, not one — after the first I grepped every op_name call rather than assuming the reported one was the only one, and the taint pass had the same defect. Its trigger is an unmodelled operator, so it was printing the placeholder for precisely the population it describes. A third site is safe (op_name covers block/loop/if).

Two things you may want to know before re-running the corpus:

• The artifact misreports its own version (SCRY_VERSION is a hardcoded literal — the shipped 3.2.5 component reports itself as 3.2.4 #133). The shipped 3.2.5 component emits "scry 3.2.4 — ..." from a hardcoded literal the bump missed. Doesn't affect analysis, but if you key anything off that string, it'll lie to you.
• func.wast: Internal("i32 binop with single operand") — operand-stack underflow, unmasked by the #125 fix #128 is the first of your 82 analyzer errors with a name and a public reproducer.

The re-run offer stands as the most useful next thing here — a before/after on your corpus is the only honest way to state what the operator modelling buys, and a number you produce independently is worth more than one I produce. The fallback ranking should now be readable directly from scry's own diagnostics rather than reconstructed.