From 87518f0368c41c05da9fe94effd34a5c299773e5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 8 Aug 2026 09:06:55 +0200 Subject: [PATCH] =?UTF-8?q?feat(T2):=20dissolve=20the=20Health=20Monitor?= =?UTF-8?q?=20=E2=80=94=20the=20isolation=20core=20moves=20onto=20the=20ve?= =?UTF-8?q?rified=20path?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 could not dissolve, nothing in the isolation core could. It dissolves. Bodies lifted VERBATIM from the Verus/Kani-verified plain/src: health_monitor.rs -> wasm 2401 B -> component 3956 B -> cortex-m3 object text 1054 data 0 bss 0 undefined: 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. Its Rocq theorem i32_const_correct is Admitted (false as stated for un-normalized operands; the supporting arithmetic is Qed). So neither half covers it, 29 times over. i32.and / i32.eqz / i32.sub verified + Qed covered by both i32.gt_s / i32.le_s / i32.le_u verified, no theorem covered by BIN-VERIFY only i32.const x29 SKIPPED + Admitted COVERED BY NEITHER Filed: synth#933 (the proof gap) and synth#935 (that the gap is invisible in the tool's own output -- a consumer cannot compute a denominator from `synth verify`). 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 commit would have recorded a false zero-gap claim. NOT established, stated in RESULTS.md rather than left to be assumed: the evidence-on-wasm set (witness MC/DC, scry, the REQ-OS-HM-001 oracles re-run against the WASM build) has not been produced for this artifact, so BIN-VERIFY shows the lowering is faithful but not that the wasm refines the proven Rust; nothing has executed the object; the switch (3 seams) and mpu_switch (1 seam) remain; and 7 exported predicates became 6 functions, presumed inlining, unconfirmed. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- benches/gust/drivers/hm-thin/Cargo.lock | 335 +++++++++++++++++++ benches/gust/drivers/hm-thin/Cargo.toml | 15 + benches/gust/drivers/hm-thin/RESULTS.md | 87 +++++ benches/gust/drivers/hm-thin/hm-thin-cm3.o | Bin 0 -> 2085 bytes benches/gust/drivers/hm-thin/src/lib.rs | 68 ++++ benches/gust/drivers/hm-thin/wit/gust-hm.wit | 15 + 6 files changed, 520 insertions(+) create mode 100644 benches/gust/drivers/hm-thin/Cargo.lock create mode 100644 benches/gust/drivers/hm-thin/Cargo.toml create mode 100644 benches/gust/drivers/hm-thin/RESULTS.md create mode 100644 benches/gust/drivers/hm-thin/hm-thin-cm3.o create mode 100644 benches/gust/drivers/hm-thin/src/lib.rs create mode 100644 benches/gust/drivers/hm-thin/wit/gust-hm.wit diff --git a/benches/gust/drivers/hm-thin/Cargo.lock b/benches/gust/drivers/hm-thin/Cargo.lock new file mode 100644 index 0000000..088e438 --- /dev/null +++ b/benches/gust/drivers/hm-thin/Cargo.lock @@ -0,0 +1,335 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "anyhow" +version = "1.0.104" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470" + +[[package]] +name = "bitflags" +version = "2.13.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b588b76d00fde79687d7646a9b5bdf3cc0f655e0bbd080335a95d7e96f3587da" + +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "foldhash" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" + +[[package]] +name = "gust-hm-thin" +version = "0.1.0" +dependencies = [ + "wit-bindgen", +] + +[[package]] +name = "hashbrown" +version = "0.15.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" +dependencies = [ + "foldhash", +] + +[[package]] +name = "hashbrown" +version = "0.17.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" + +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + +[[package]] +name = "id-arena" +version = "2.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" + +[[package]] +name = "indexmap" +version = "2.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" +dependencies = [ + "equivalent", + "hashbrown 0.17.1", + "serde", + "serde_core", +] + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "leb128fmt" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" + +[[package]] +name = "log" +version = "0.4.33" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ceec5bc11778974d1bcb055b18002eba7f4b3518b6a0081b3af5f21666da9ad" + +[[package]] +name = "memchr" +version = "2.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" + +[[package]] +name = "prettyplease" +version = "0.2.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" +dependencies = [ + "proc-macro2", + "syn 2.0.119", +] + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348" +dependencies = [ + "proc-macro2", + "quote", + "syn 3.0.3", +] + +[[package]] +name = "serde_json" +version = "1.0.151" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "syn" +version = "2.0.119" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "872831b642d1a07999a962a351ed35b955ea2cfc8f3862091e2a240a84f17297" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "3.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "53e9bae58849f64dfa4f5d5ae372c8341f7305f82a3868709269343628b659a3" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" + +[[package]] +name = "wasm-encoder" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319" +dependencies = [ + "leb128fmt", + "wasmparser", +] + +[[package]] +name = "wasm-metadata" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" +dependencies = [ + "anyhow", + "indexmap", + "wasm-encoder", + "wasmparser", +] + +[[package]] +name = "wasmparser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" +dependencies = [ + "bitflags", + "hashbrown 0.15.5", + "indexmap", + "semver", +] + +[[package]] +name = "wit-bindgen" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4e048f41ef90f0b5dd61f1059c35f5636252e56813bf616d0803aa3739867230" +dependencies = [ + "wit-bindgen-rust-macro", +] + +[[package]] +name = "wit-bindgen-core" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c15e7a56641cc9040480a26526a3229cbc4e8065adf98c9755d21c4c9b446c4c" +dependencies = [ + "anyhow", + "heck", + "wit-parser", +] + +[[package]] +name = "wit-bindgen-rust" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd81b0ae1ec492bfe91683f1da6db6492ebc682e72d4f2715619dba783b066ca" +dependencies = [ + "anyhow", + "heck", + "indexmap", + "prettyplease", + "syn 2.0.119", + "wasm-metadata", + "wit-bindgen-core", + "wit-component", +] + +[[package]] +name = "wit-bindgen-rust-macro" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "54e6ce04c549e7149b66a70d34fc5a2a01b374bf49ca61db65d16e3ae922866e" +dependencies = [ + "anyhow", + "prettyplease", + "proc-macro2", + "quote", + "syn 2.0.119", + "wit-bindgen-core", + "wit-bindgen-rust", +] + +[[package]] +name = "wit-component" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" +dependencies = [ + "anyhow", + "bitflags", + "indexmap", + "log", + "serde", + "serde_derive", + "serde_json", + "wasm-encoder", + "wasm-metadata", + "wasmparser", + "wit-parser", +] + +[[package]] +name = "wit-parser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" +dependencies = [ + "anyhow", + "id-arena", + "indexmap", + "log", + "semver", + "serde", + "serde_derive", + "serde_json", + "unicode-xid", + "wasmparser", +] + +[[package]] +name = "zmij" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" diff --git a/benches/gust/drivers/hm-thin/Cargo.toml b/benches/gust/drivers/hm-thin/Cargo.toml new file mode 100644 index 0000000..c001d4f --- /dev/null +++ b/benches/gust/drivers/hm-thin/Cargo.toml @@ -0,0 +1,15 @@ +[workspace] +[package] +name = "gust-hm-thin" +version = "0.1.0" +edition = "2021" +description = "T2 stage 2: the Verus/Kani-verified Health-Monitor value-domain predicates as a dissolvable wasm component. Bodies lifted VERBATIM from plain/src/health_monitor.rs. Zero seams, zero SRAM \u2014 the cheapest proof that the isolation core can move onto the dissolve path (REQ-OS-OBJVERIFY-001)." +[lib] +crate-type = ["cdylib", "rlib"] +[dependencies] +wit-bindgen = { version = "0.52", default-features = false, features = ["macros"] } +[profile.release] +panic = "abort" +opt-level = "s" +lto = true +codegen-units = 1 diff --git a/benches/gust/drivers/hm-thin/RESULTS.md b/benches/gust/drivers/hm-thin/RESULTS.md new file mode 100644 index 0000000..f554d83 --- /dev/null +++ b/benches/gust/drivers/hm-thin/RESULTS.md @@ -0,0 +1,87 @@ +# hm-thin — the isolation core, dissolved. And an honest coverage report + +**Date:** 2026-08-07 · **T2 / REQ-OS-OBJVERIFY-001 stage 2** · meld 0.41.3, loom 1.2.0, +synth 0.52.0 built with `--features verify` + +`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 could not dissolve, nothing in the +isolation core could. + +## It dissolves + + plain/src/health_monitor.rs (Verus + Kani verified — bodies lifted VERBATIM) + -> cargo wasm32 2 401 B + -> wasm-tools component new 3 956 B + -> meld fuse --memory shared + -> loom optimize --passes inline + -> synth compile --target cortex-m3 --all-exports --relocatable + + 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 is the failure mode, `hm-thin` genuinely has no seam to +preserve. It computes over scalars and returns. + +## BIN-VERIFY runs on it + + 6 functions · 8 rules verified · 0 failed · 0 unknown · 0 declined + rules: i32.and · i32.eqz · i32.gt_s · i32.le_s · i32.le_u · i32.sub + +## THIS IS NOT A ZERO-GAP RESULT, AND THE SUMMARY LOOKS LIKE ONE + +The line above reads as complete coverage. It is not, and the discrepancy is the +whole reason `REQ-OS-OBJVERIFY-001` defines its denominator as the **union** of +RULE-VERIFY and BIN-VERIFY rather than as whatever the tool prints. + +**The object contains 29 `i32.const`.** BIN-VERIFY classes Const as a register +operation and skips it *silently* — it is not in the verified list and not in a +declined list, because there is no declined list. So: + +| 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, by BIN-VERIFY only | +| **`i32.const`** (×29) | **skipped, unreported** | **`Admitted`** | **NO — neither half** | + +`i32_const_correct` is Admitted because it is false as stated for un-normalized +operands; the supporting arithmetic (`i32_const_large_reconstruct`, +`movw_movt_reconstruct_Z`) is `Qed`. Filed as **synth#933**. + +That the gap is invisible in the tool's own output is filed separately as +**synth#935** — a consumer cannot compute a coverage denominator from `synth verify`, +because it never reports the rules it declined. + +**So: zero-gap CANNOT be claimed for this object.** One rule, named, filed, and +appearing 29 times. + +## What this does establish + +- The construction works. Verified Rust lifted verbatim into a wasm component + dissolves to a native object, and translation validation runs on the result. +- The isolation core is **not** blocked on a rewrite. All three modules are already + thin-seam shaped; this one simply had no seam at all. +- Instruction selection, register allocation and scheduling for this object are now + performed by a compiler that carries obligations, instead of by LLVM. + +## What it does NOT establish + +- **Not the full evidence-on-wasm set.** `REQ-OS-OBJVERIFY-001` also requires witness + MC/DC with zero unresolved gap rows, scry's verdicts and gap report, and the + `REQ-OS-HM-001` oracles **re-run against the wasm build**. None of those has been + done for this artifact. Without them, BIN-VERIFY shows the lowering is faithful but + not that the wasm refines the Verus-proven Rust. +- **Not executed.** Nothing has run this object. +- **Not the switch.** `partition_switch` (3 seams) and `mpu_switch` (1 seam) are the + remaining stage-2 work; HM was chosen first precisely because it is the easy case. +- **7 exported predicates became 6 functions** in the object. Presumed inlining; + not yet confirmed, and stated here rather than left unnoticed. + +## Reproduce + + cd benches/gust/drivers/hm-thin && cargo build --release --target wasm32-unknown-unknown + wasm-tools component new target/wasm32-unknown-unknown/release/gust_hm_thin.wasm -o hm.component.wasm + meld fuse hm.component.wasm --memory shared -o hm.fused.wasm + loom optimize hm.fused.wasm --passes inline --attestation false -o hm.loom.wasm + synth compile hm.loom.wasm --target cortex-m3 --all-exports --relocatable -o hm-thin-cm3.o + synth verify hm.loom.wasm hm-thin-cm3.o # needs a --features verify build diff --git a/benches/gust/drivers/hm-thin/hm-thin-cm3.o b/benches/gust/drivers/hm-thin/hm-thin-cm3.o new file mode 100644 index 0000000000000000000000000000000000000000..7fdf9f15e6adbef0b3b3fdc0966ca36893b21d86 GIT binary patch literal 2085 zcmdT_&u<$=6nB;Mr45xy3UZ30MET)tnikR?=*Ea4LR2;U1GbYawT0`r@g@*1 zB%q>ls{{vxggAjX6j2ExFWJSU$ERz{73Wg^`ox0m*z=BMCMT2T zONCNtaV6&z7E9xc@6o%)>bH(D~eCGXvlbI`&7OvT)jG4J`E@S$%$#X||oy{pKZ&+;# zSna5OuWjgomag}^x=Ewmb?j?aTZEKPgRk4w)3;JzR7ITPB+Fam#|ITB=*L?$=EWmc zgq1Jk$7k15kE&vT25z%O9??XWErWFk#T9;@IE{FDkY7NHuaRp&hegABM~49&UOX9o z9@z0ecV~XsEBDmgEY;ivqvq!0HMeMLvgVRCC{N2D`)|v*{JupZAgAP4sfSgOpahM@ zsuyLCgqm>8jizg^o^7}bZ zOn3L2vgmz?%TD>?4SJy0X z(%>SaPBA$kNAMmU^5dIeHCz!iP%Kkf8KR{Lf z7cl+>whsJV2k*eHLaxHBg(ufL3H~VT3?}Pg{5Gu8!}u1ks>k>zV3nWoufQrlV*|Ci zB18$c8c~{Uh-kC3|FE;~cJ>kep9X72$id*B9&1&D{XDub5A$vU@3Nya6z?SP;bv_> zBVP>faSli)1G68KWBh+D(K5h`?CcD+8~|pX8lNMdt^lm!y@ECLm6huo@J=fLt8%=7 U^@&6K8xUXu^Vv8TPku-K1^=u>_5c6? literal 0 HcmV?d00001 diff --git a/benches/gust/drivers/hm-thin/src/lib.rs b/benches/gust/drivers/hm-thin/src/lib.rs new file mode 100644 index 0000000..f7913ec --- /dev/null +++ b/benches/gust/drivers/hm-thin/src/lib.rs @@ -0,0 +1,68 @@ +//! SPIKE — gust:hm thin-seam Health Monitor. +//! Bodies lifted VERBATIM from plain/src/health_monitor.rs (Verus+Kani verified). +#![no_std] +#[panic_handler] +fn ph(_: &core::panic::PanicInfo) -> ! { loop {} } + +// wit-bindgen's canonical-ABI glue must LINK against a global allocator; this world +// is scalar-only (u32/i32/bool in, bool out), so nothing ever calls it and a +// zero-state trapping allocator keeps the 0-SRAM property intact. Same construction +// as the thin-seam drivers. +use core::alloc::{GlobalAlloc, Layout}; +struct NoAlloc; +unsafe impl GlobalAlloc for NoAlloc { + unsafe fn alloc(&self, _: Layout) -> *mut u8 { core::ptr::null_mut() } + unsafe fn dealloc(&self, _: *mut u8, _: Layout) {} +} +#[global_allocator] +static ALLOC: NoAlloc = NoAlloc; + +wit_bindgen::generate!({ world: "hm-thin", path: "wit" }); + +mod hm { +pub fn fresh(age_ms: u32, limit_ms: u32) -> bool { + age_ms <= limit_ms +} + +pub fn plausible(value: i32, lo: i32, hi: i32) -> bool { + lo <= value && value <= hi +} + +pub fn innovation_ok(innov_abs: u32, k_sigma: u32) -> bool { + innov_abs <= k_sigma +} + +pub fn budget_ok(used_us: u32, budget_us: u32) -> bool { + used_us <= budget_us +} + +pub fn deadline_ok(lateness_us: u32) -> bool { + lateness_us == 0 +} + +pub fn heartbeat_ok(missed_beats: u32) -> bool { + missed_beats == 0 +} + +pub fn vote_ok(s0: i32, s1: i32, s2: i32, tol: i32) -> bool { + let t = tol as i64; + let d01 = s0 as i64 - s1 as i64; + let d02 = s0 as i64 - s2 as i64; + let d12 = s1 as i64 - s2 as i64; + let a01 = (if d01 >= 0 { d01 } else { -d01 }) <= t; + let a02 = (if d02 >= 0 { d02 } else { -d02 }) <= t; + let a12 = (if d12 >= 0 { d12 } else { -d12 }) <= t; + (a01 && a02) || (a01 && a12) || (a02 && a12) +}} + +struct P; +impl exports::gust::hm::detect::Guest for P { + fn fresh(a: u32, l: u32) -> bool { hm::fresh(a, l) } + fn plausible(v: i32, lo: i32, hi: i32) -> bool { hm::plausible(v, lo, hi) } + fn innovation_ok(i: u32, k: u32) -> bool { hm::innovation_ok(i, k) } + fn budget_ok(u: u32, b: u32) -> bool { hm::budget_ok(u, b) } + fn deadline_ok(l: u32) -> bool { hm::deadline_ok(l) } + fn heartbeat_ok(m: u32) -> bool { hm::heartbeat_ok(m) } + fn vote_ok(a: i32, b: i32, c: i32, t: i32) -> bool { hm::vote_ok(a, b, c, t) } +} +export!(P); diff --git a/benches/gust/drivers/hm-thin/wit/gust-hm.wit b/benches/gust/drivers/hm-thin/wit/gust-hm.wit new file mode 100644 index 0000000..4190cab --- /dev/null +++ b/benches/gust/drivers/hm-thin/wit/gust-hm.wit @@ -0,0 +1,15 @@ +package gust:hm@0.1.0; + +/// The Health-Monitor value-domain predicates — pure scalar logic, no seam. +/// Derived from plain/src/health_monitor.rs (Verus + Kani verified). +interface detect { + fresh: func(age-ms: u32, limit-ms: u32) -> bool; + plausible: func(value: s32, lo: s32, hi: s32) -> bool; + innovation-ok: func(innov-abs: u32, k-sigma: u32) -> bool; + budget-ok: func(used-us: u32, budget-us: u32) -> bool; + deadline-ok: func(lateness-us: u32) -> bool; + heartbeat-ok: func(missed-beats: u32) -> bool; + vote-ok: func(s0: s32, s1: s32, s2: s32, tol: s32) -> bool; +} + +world hm-thin { export detect; }