doc-vs-source sweep: 30 mechanically-verified disagreements, 4 of them possible defects (not doc staleness)

[avrabe]

Two scanners over disjoint surfaces, both instructed to report the disagreement and never rule on which side is right. That framing was load-bearing: of this release's three known instances the resolution differed each time (doc wrong / code wrong / fixture wrong), so a scanner assuming "code wins" would have mis-filed two of three.

Examined ~930 claims mechanically. 30 genuine disagreements (~500 Rust doc comments → 20; ~430 prose claims → 10). Two already fixed in #945. This issue carries the rest.

---

TIER 1 — possible DEFECTS, need investigation before anything is edited

These are not assumed to be code bugs. Each is a claim the code appears to contradict in a way that would matter if the doc is the intended contract.

A. VFP encoder precondition holds for only ONE of the two selectors

arm_encoder.rs:7286 states "The SELECTOR guarantees dm is a dead temp, never a pinned param/local home (it copies a home into a fresh D-temp first)."

select_with_stack genuinely implements that copy (instruction_selector.rs:4505). select_default does not — it allocates from a bare round-robin counter with no home/liveness test (:7784, alloc_vfp_dreg :6020), and grep -c vfp_home over its body returns 0.

--relocatable forces select_default (per #197). If the encoder's overlapping VCVT write can land on a live f64 home there, this is a miscompile, not a doc bug.

B. "never S0" — index 0 is admitted

arm_encoder.rs:7280 / :7221: the 32-bit result stages through an S-alias "never S0, which may hold an unrelated live value (the #615 class)". The only guard is if dm_num > 7; encode_sreg(0) is S0, D0 is reachable (next_vfp_dreg: 0), and the encoder's own test records vmov s0, r3. Same #615 class the comment invokes.

C. --volatile-segment moves bytes while documented as inert

main.rs:471: "PHASE 1 = plumbing only … the emitted bytes are unchanged whether or not the flag is passed."

Measured by the scanner on scripts/repro/volatile_segment_543.wat, no SYNTH_* set: 196 B without the flag, 234 B with --volatile-segment 0x100:16. The Phase-2 back-off is already wired (arm_backend.rs:1432 const-CSE skipped when the list is non-empty; optimizer_bridge.rs:3213 base-CSE). The frozen-byte gates never exercise the flag, so nothing catches this.

D. WCET loop SP-tracking claims exhaustiveness over a wildcard

wcet_loops.rs:1036: "Exhaustive over every rd-carrying op the priced instruction set can contain." The match ends _ => false (:1089), and eight priced rd-carrying ops have no arm (I64SetCond, I64SetCondZ, I64Clz, I64Ctz, I64Popcnt, Str, Strb, Strh).

Those eight do not write SP, so the WCET bound is not currently wrong — but the stated tripwire does not exist: a new ArmOp that does write SP compiles fine and silently reads false. The parenthetical also says I64Popcnt is a whole-function LoopedExpansion decline; op_cost prices it.

---

TIER 2 — stale rationale on a live exclusion (safe today, wrong reason)

where	claim	source
wcet.rs:77	"the audited expansions push at most 3 registers, so this holds with margin"	PUSH {R0-R3} (0xB40F, 4 regs) is in the priced I64Rotl/I64Rotr arms. CEIL_PER_HALFWORD = 5 then holds exactly (1+4), not with margin — and it is a claims.yaml-pinned soundness constant
validator_pattern.rs:94	i64 div/rem excluded because "synth lowers 64-bit division to a runtime-library call (__aeabi_ldivmod)"	The encoder expands them inline (arm_encoder.rs:5646, 64-round loop). grep -rn '__aeabi' crates/ finds only comments. Four ops are excluded from translation validation on a rationale that does not describe the lowering
static_data_addr.rs:83	"AArch64: N/A — every memory op loud-declines at selection"	aarch64/selector.rs:2186+ lowers I32Load/Store, I64Load/Store, the 8/16-bit variants. Premise false since #851
alloc_validator.rs:56	"on RV every op_dest == None op is control-flow / system / label / call"	Sb/Sh/Sw are None and none of those four. Conclusion survives (stores write no register) but on a different argument than the one written
selector.rs:1498 (RV)	"alloc_temp must never hand any of them out"	The exhaustion path returns self.temps[0] — by construction one of them (:1556). Safe only via the alloc_exhausted decline the doc omits

---

TIER 3 — docs that UNDERSTATE what ships

Every one makes synth look less capable than it is. That is why none was noticed.

• aarch64/selector.rs:35 lists call_indirect, float rounding, f32/f64 load/store, i64→float converts as "deliberately still declined (loud-skip)" — all have real lowerings in the same file's shipped match. Same class in riscv/selector.rs:10 (br_table, cross-function calls listed out-of-scope, both lowered).
• instruction_selector.rs:5037 — "the 40 Rocq-proved rules"; the shipped table has 50, including nine i64 ops the enumeration omits.
• instruction_selector.rs:2285 — "phase 1 has no VFP spilling, so an f32 expression deeper than the register file loud-skips its function". GI-FPU-002 + RA tail is now the ONLY gate between the falcon cascade and the M7 — 5 entry-point symbols; phase-2 D-register pressure is new in v0.52 (inline-f64 #869 lowering) #881 shipped spilling and arm_backend.rs:686 retries with no env gate. The stale wording is also baked into a user-visible error string (:2296).
• aarch64/selector.rs:272 — select_typed_cf says loop/if/br_table are "declined by name"; all three are lowered (:1679, :1779, :1802). The same wrapper hardcodes MemBounds::Unchecked (:301) while MemBounds' own doc says "there is no silent default".
• main.rs:4538 — --shadow-stack-size: "a Some here is an honest Err, never a silent no-op". The surgery is implemented (:5031, :5210); a compile with --shadow-stack-size 4096 exits 0 and shrinks .bss to 4240 B.
• CLAUDE.md:150 — WasmCert pinned at "phases 1+2, 19 ops, 49 Qed"; actual 104 Qed, phase 3, 41 ops. The file that instructs every agent working here.
• README.md:284 — names 6 i64 ops as an "op-level-only residual"; coq/STATUS.md and the .v file both record it CLOSED.
• coq/STATUS.md — CI-gated headline 591 Qed, hand-maintained table totals 585, two rows understate their files (ArmSemantics 8 vs 14, VcrSelRules 42 vs 52), five .v files missing from the table entirely.
• VcrSelRules.v:16 — "the 40 Qed themselves are the divergence gate"; there are 50.
• CorrectnessI32.v:4 — "29 Qed"; 31 (29 theorems + 2 helper lemmas).
• FEATURE_MATRIX.md:72 — WasmCert bridge described as i32-only while carrying the i32+i64 count.
• docs/status/PROJECT_STATUS.md — ~10 releases stale and pinned by nothing: 291 Qed (actual 591), 16 crates (18, omitting both RISC-V and AArch64 backends), "no bulk memory" while GI-MEM-002 is verified, "no multi-memory" while SYNTH-MATRIX-MULTI-MEMORY is pinned and green, Z3 named as the default validator (ordeal since v0.27). Its own Last updated date is wrong.
• docs/status/POC_ACHIEVEMENTS.md:26 — "R0-R12" allocatable; the Verus spec allows R0-R8 (contracts.rs:45).
• gale-integration.yaml:584 — cites map_operator; git log -S shows the symbol never existed (it is convert_operator).

---

The mechanism, and why no gate sees it

Most of Tier 3 is one thing: a machine-derived number moves while the hand-written sentence beside it does not. claim_check.py pins ~43 claims and re-derives counts; everything else drifts freely. It checks prose against prose — it passed 43/43 over a European-decimal-separator typo I introduced hours earlier.

Nothing in the repo checks prose against behaviour. That is the seam all 30 findings live in.

Both scanners recorded what they checked and found consistent, so this is not re-scanned: 57 CI job names, 6 Bazel targets, 20 SYNTH_* env vars incl. every default-on claim, 132 implemented/verified artifact blocks' file references, 100 Rust symbols, the frozen anchors, ORACLE_WIRING's ratchet floors (deliberately floors, not current counts — not a disagreement), and wcet.rs:119's *"EXHAUSTIVE with NO wildcard"` which genuinely holds.

Nothing here is edited yet. Tier 1 needs investigation first — deciding which side is right is the work, and doing it wrong in either direction is how a real defect gets papered over.

[avrabe]

Two more, found incidentally — and one of them is the interesting kind

Not from the scan: I hit these while fixing #931, in the RV32 selector code the
br reconciliation touches. Both are fixed in #947; recording them here so
the next pass over this list doesn't re-derive them, and because the second is a
shape the scan's method would have missed.

(a) A comment that is simply false. live_regs in
crates/synth-backend-riscv/src/selector.rs:

Every vstack entry is a temp register (locals/params are always copied into a
fresh temp by lower_local_get)

lower_local_get does the opposite for a #472-promoted local — it aliases the
callee-saved s-register directly onto the vstack, "no load, no copy," and
says so in its own comment three hundred lines away. That aliasing is the whole
source of the promotion byte win. Ordinary staleness; corrected.

(b) An argument that is true but doesn't cover what it's cited for. The
aliasing at lower_local_get is justified by:

Sound because (a) any op consuming this value allocates a fresh dst … so the
s-reg is never clobbered by a consumer

That holds for every consumer that existed when it was written. A br edge is a
consumer that writes back into its operand — it donates the value's register
to the target frame, and the frame's end writes that register on the
fallthrough path. For br $l (local.get $x) that would clobber $x itself.

What actually prevents it is a rule in a different pass: promotion requires
all_depth0, and br exists only at depth ≥ 1. So the code is sound, by a fact
its own soundness argument never mentions and which nothing tied to it.

This is worth separating from category (a) in this issue's taxonomy. (a) is a
doc that disagrees with its source. (b) is a doc that agrees with its source and
is still not load-bearing — the claim is locally true and globally insufficient.
No prose-vs-prose check finds those, and neither would a doc-vs-source diff:
both halves read correct. It took writing a new consumer to expose it.

#947 guards it locally rather than borrowing soundness from the other pass, and
adds promotion_stays_depth0_or_931_guard_goes_live so relaxing all_depth0
reports instead of silently miscompiling.

Suggest the scan's follow-up explicitly hunts category (b): soundness
arguments that enumerate cases ("any op that …", "every consumer …", "in all
cases we …"). An enumeration written against the code of its day is a claim with
an expiry date, and the expiry is silent.

[avrabe]

Tier 1 A and B — investigated. Both resolve to doc wrong, code safe, neither for the stated reason.

Method: compile and read the emitted instructions, rather than read the source.
Fixed in #945.

A — "the SELECTOR guarantees dm is a dead temp"

True of the selector the compiler actually uses. select_with_stack emits
the copy. Shipped output for (func (param f64) (result i32) (i32.trunc_f64_s (local.get 0)))
on cortex-m7dp --relocatable:

vmov r1, r2, d0      ; read the param out of its AAPCS-VFP home D0
vmov d1, r1, r2      ; ...into a fresh D-temp
vcvt.s32.f64 s2, d1  ; converts from the TEMP, staging into its own S2

select_default genuinely lacks it — alloc_vfp_dreg is a bare
(n + 1) % 16 with no liveness or home test, as reported.

But the reachability premise is wrong. The finding says "--relocatable
forces select_default (per #197)". #197 forces the direct selector, and
the direct selector is select_with_stack (arm_backend.rs:566).
Direct and default are different selectors; the names invite exactly this
conflation.

InstructionSelector::select isn't reachable from synth compile at all — its
only non-test caller in the tree is examples/compile_add.rs. So this is a
pub API that hands out no guarantee, not a compiled miscompile. Worth
saying out loud in the encoder, which #945 now does.

B — "never S0"

False, and reproducible in three lines:

(func (export "t") (result i32) (i32.trunc_f64_s (f64.const 3.7)))

→ vcvt.s32.f64 s0, d0

The staging register is S0. But the claim was also unnecessary: S0 is
dangerous only as an unrelated scratch, and S(2m) is always the low half of
dm itself — which A's dead-temp precondition already covers. So the sentence
was both wrong and load-bearing-looking, which is the worse combination.
Removed rather than patched.

The class this belongs to — worth adding to the taxonomy

A and B are not "doc contradicts source". They are a soundness argument that
is locally true and cites the wrong reason:

• B names a guard (never S0) that does not exist, in place of the one that
  does (dm is dead).
• A names "the SELECTOR" where two selectors exist and only one complies.

Both halves read correct in isolation, so neither a prose-vs-prose check nor a
doc-vs-source diff finds them. What exposes them is writing a new consumer
— which is also how the same pattern turned up in #931/#947, where
lower_local_get's "any op consuming this value allocates a fresh dst" was
true of every consumer that existed when it was written, and a br edge is a
consumer that writes back.

Suggest the follow-up scan hunts this shape explicitly: soundness rationales
that quantify over cases — "any op that…", "every consumer…", "the selector
guarantees…", "in all cases…". An enumeration written against the code of its
day is a claim with a silent expiry date. Three instances in two days.

Remaining Tier 1: C (--volatile-segment moves bytes, 196 → 234 B — the
one with a measured behavioural delta, so likeliest to be a real defect) and
D (WCET SP wildcard — stated tripwire absent, bound not currently wrong).

[avrabe]

Tier 1 C — investigated. Doc wrong, code right and already gated.

Reproduced, then isolated the mechanism. scripts/repro/volatile_segment_543.wat,
--cortex-m on cortex-m4, scrubbed env so no ambient SYNTH_* leaks in:

levers	flag-off	flag-on
CSE default	36 B	74 B	differs
SYNTH_CONST_CSE=0 SYNTH_BASE_CSE=0	98 B	98 B	same

The second row is what makes the first interpretable: with the CSE levers
already off the flag changes nothing, so the +38 B is exactly the aliasing
back-off and not some other effect. (Your 196→234 was a different
invocation — same +38.)

Phase 2 is not only implemented, it is gated, by three tests in
crates/synth-cli/tests/volatile_segment_phase2_543.rs:
base_cse_honors_volatile_window_543,
const_cse_declines_wholesale_under_volatile_543, and
volatile_gates_are_identity_when_no_range_marked_543.

So the byte-gate gap in the finding ("the frozen-byte gates never exercise the
flag, so nothing catches this") is narrower than it looked — the frozen anchors
don't, but a dedicated suite does. What nothing checked was the --help
string, which is not any gate's input.

Doc corrected in #945.

Why this one mattered more than its tier suggests

Nearly every stale doc in this issue understates what ships — that is stated
as the reason none was noticed, and it is also why they are cheap. This one
inverts: it told users a flag that doubles code size was free plumbing. The
safe-sounding reading ("mark generously, it's only plumbing") is the expensive
action, on parts where flash is the binding constraint.

Suggest that when triaging the rest, direction of error is the priority
axis, not tier: a doc that undersells a shipped feature costs a missed
opportunity; a doc that undersells a cost changes what someone does. By that
axis the remaining highest-value item is Tier 2's validator_pattern.rs:94 —
four i64 ops excluded from translation validation on a rationale
(__aeabi_ldivmod) that does not describe the lowering. Wrong reason,
exclusion consequence: if the real reason doesn't hold, those ops should be
validated and currently aren't.

Tier 1 status

• A — doc wrong (named the wrong guarantor), code safe. Fixed docs(#945): correct a false claim we wrote, and stop a gate passing on nothing #945.
• B — doc wrong (never S0 is false AND unnecessary), code safe. Fixed docs(#945): correct a false claim we wrote, and stop a gate passing on nothing #945.
• C — doc wrong (claimed inert), code right and gated. Fixed docs(#945): correct a false claim we wrote, and stop a gate passing on nothing #945.
• D — WCET SP wildcard. Not yet investigated; the finding already concedes
  the bound is not currently wrong, so it is a missing tripwire rather than a
  defect.