feat(T2): dissolve the Health Monitor — the isolation core moves onto the verified path

[avrabe]

REQ-OS-OBJVERIFY-001 needs the isolation core lowered by a compiler that carries per-rule obligations. health_monitor.rs is the cheapest possible first step: zero hardware seams, pure scalar predicates. If it couldn't dissolve, nothing in the isolation core could.

It dissolves

health_monitor.rs (Verus + Kani verified — bodies lifted VERBATIM)
  -> wasm 2 401 B -> component 3 956 B -> cortex-m3 object

text 1054   data 0   bss 0        undefined symbols: none

Zero SRAM, and correctly no undefined symbols — unlike the fused OS composite, where an empty undefined set means the seam was swallowed, hm-thin genuinely has no seam.

BIN-VERIFY runs on it: 6 functions, 8 rules verified, 0 failed, 0 unknown.

And it is NOT a zero-gap result, though the summary looks like one

The object contains 29 i32.const. BIN-VERIFY classes Const as a register operation and skips it silently — not in the verified list, not in a declined list, because there is no declined list.

rule	BIN-VERIFY	RULE-VERIFY (Rocq)	covered?
i32.and, i32.eqz, i32.sub	verified	Qed	yes, both halves
i32.gt_s, i32.le_s, i32.le_u	verified	no theorem exists	yes, BIN-VERIFY only
i32.const ×29	skipped, unreported	Admitted	NO — neither half

Filed: synth#933 (the proof gap — false as stated for un-normalized operands, supporting arithmetic is Qed) and synth#935 (that the gap is invisible in the tool's own output).

This is the union-denominator clause from #260 earning its place on the first object it was applied to. My first read of that summary was "zero declined, clean." The clause is what made me check the module, and the module had 29 of them. Written the old way, this PR would have recorded a false zero-gap claim.

What it establishes

• the construction works — verified Rust, lifted verbatim, dissolves and is translation-validated
• the isolation core is not blocked on a rewrite
• instruction selection, register allocation and scheduling for this object are now done by a compiler carrying obligations rather than by LLVM

What it does not

• the evidence-on-wasm set is absent — no witness MC/DC, no scry, and the REQ-OS-HM-001 oracles have not been re-run against the wasm build. So BIN-VERIFY shows the lowering is faithful, not that the wasm refines the proven Rust.
• nothing has executed the object
• partition_switch (3 seams) and mpu_switch (1 seam) remain
• 7 exported predicates became 6 functions — presumed inlining, unconfirmed, recorded rather than ignored

Stays out of the requirement's verified column: this is one module of three, with a named open gap and no evidence-on-wasm.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!