req(T2): state what object-code verification actually achieves — and what it needs

[avrabe]

REQ-OS-OBJVERIFY-001 claimed "the compiler is removed from the isolation trust argument BY CONSTRUCTION." Working the track showed that isn't what the construction delivers. The requirement now says what it does.

① Precondition — the object doesn't exist yet

The requirement presumed an object produced by a per-rule-obligation compiler. There is none: partition_switch / mpu_switch / health_monitor are compiled natively by LLVM and never enter the dissolve path. Moving them is the requirement.

The text records why that's tractable rather than a rewrite — all three are already thin-seam shaped: ~1 790 lines of scalar logic over four native atoms (ctx_save, region_swap, ctx_resume, mpu_write), no inline asm, no volatile, no raw pointers. Read out of the source, not assumed.

② The obligation — "zero gap" had no denominator

Now defined as the union of RULE-VERIFY and BIN-VERIFY: a rule BIN-VERIFY declines as non-computational counts as covered only if its RULE-VERIFY theorem is discharged.

③ What it achieves — rewritten, and this is the substantive change

rustc lowers Rust to wasm through LLVM, so dissolving doesn't remove LLVM — it moves it.

My first draft framed the residue as trusted LLVM. That was the wrong frame. LLVM is an untrusted producer whose output is verified rather than believed: the wasm carries MC/DC (witness), sound abstract interpretation (scry) and the executable oracles, then reaches machine code through a translation-validated compiler.

Qualification of LLVM is therefore not required — the classical alternative to qualifying a tool is verifying its output, which is what's claimed. Written so an assessor asking "what compiles the Rust to wasm?" meets an answer rather than a hole.

⑤ Evidence-on-wasm — the argument's price

③ holds only while the evidence is gathered, and today it isn't — witness has never been pointed at this OS (v0.6.0's notes say so). So the obligations are named and gated: witness MC/DC with zero unresolved gap rows, scry verdicts + gap report, and the SWITCH / ISO / HM oracles re-run against the wasm build.

That last clause is load-bearing. MC/DC and abstract interpretation establish properties of the wasm — they don't by themselves show it refines the Verus-proven Rust. A miscompile could yield wasm that is well-covered and sound-by-AI yet semantically different from the proven source.

④ Known open gap

i32_const_correct is Admitted in synth's Rocq development — false as stated for un-normalized operands, though the supporting arithmetic (i32_const_large_reconstruct, movw_movt_reconstruct_Z) is Qed. BIN-VERIFY declines i32.const as a register operation, so neither half covers it. 473 occurrences across 34 of 67 functions on the E2 composite. Filed synth#933.

Zero-gap cannot be claimed while it stands, and the requirement now says so where a release gate will see it.

Kill-criterion

Gains the case that was missing: if the object is not synth-lowered the obligation is INAPPLICABLE, not satisfied — otherwise "no mismatches reported" reads as passing when the pass cannot run at all.

Evidence behind this

Built synth from source with --features verify (no release binary ships it) and ran BIN-VERIFY on the E2 dissolved OS: 23/23 functions, 24 rules verified, 0 failed, 0 unknown, 20 LRAT-certified I64 expansions, zero problems. The machinery works; the gap is one named rule.

rivet validate: PASS, 333 warnings, unchanged.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!