diff --git a/benches/gust/drivers/mpu-thin/Cargo.lock b/benches/gust/drivers/mpu-thin/Cargo.lock new file mode 100644 index 0000000..11cdf99 --- /dev/null +++ b/benches/gust/drivers/mpu-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-mpu-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/mpu-thin/Cargo.toml b/benches/gust/drivers/mpu-thin/Cargo.toml new file mode 100644 index 0000000..6d4e179 --- /dev/null +++ b/benches/gust/drivers/mpu-thin/Cargo.toml @@ -0,0 +1,15 @@ +[workspace] +[package] +name = "gust-mpu-thin" +version = "0.1.0" +edition = "2021" +description = "T2 stage 2: the Verus/Kani-verified I-ISO region-programming core as a dissolvable wasm component. Bodies lifted VERBATIM from plain/src/mpu_switch.rs + mpu.rs. ONE native atom (mpu-write) as a typed component import." +[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/mpu-thin/RESULTS.md b/benches/gust/drivers/mpu-thin/RESULTS.md new file mode 100644 index 0000000..0e5c56d --- /dev/null +++ b/benches/gust/drivers/mpu-thin/RESULTS.md @@ -0,0 +1,92 @@ +# mpu-thin — the I-ISO core dissolved, and a real SRAM constraint + +**Date:** 2026-08-08 · **T2 / REQ-OS-OBJVERIFY-001 stage 2** · meld 0.41.3, loom 1.2.0, +synth 0.52.0 (`--features verify` build for BIN-VERIFY) + +Second isolation-core module onto the dissolve path, after `hm-thin`. Unlike HM this +one has a seam — the single `mpu_write(rnr, rbar, rasr)` atom — so it tests the part +that matters: does the seam survive the dissolve, and what does the module actually +cost in RAM? + +## It dissolves, and the seam survives exactly + + plain/src/mpu_switch.rs + mpu.rs (Verus + Kani verified — lifted VERBATIM) + -> wasm 7 120 B -> component 8 464 B + -> meld fuse --memory shared -> loom optimize -> synth compile + + undefined symbols: [ mpu-write ] + +One atom, exactly as declared. Nothing undeclared crept in; nothing was swallowed. +Lifted verbatim: `size_field`, `rasr_for`, `RegionTable` (+ `new`, +`program_partition`, `switch_to_partition`, `try_add_region`, `covers_addr`), +`apply_program`, `emit_write`, and from `mpu.rs` the `is_power_of_two` / +`validate_region` helpers and `MIN_REGION_SIZE`. + +## THE FOOTPRINT — and why the first number was wrong + +Compiled the way `hm-thin` was, the object reports: + + text 3614 data 0 bss 0 + +**That is true and misleading.** Without `--native-pointer-abi` the linear memory is +not reserved in the object at all — the embedder supplies it — and this module +declares **17 wasm pages (1 088 KB)**. Reporting "zero SRAM" for it would have been +wrong by a factor of 136 on an 8 KB part. + +With the shadow-stack re-base the OS-node builds already use (#383): + +| `--shadow-stack-size` | text | data | bss | **SRAM of 8 192** | +|---|---|---|---|---| +| **2048** (OS-node standard) | 3744 | 636 | 2688 | **3 324 B — 40.6%** | +| 1024 | 3744 | 636 | 1664 | 2 300 B — 28.1% | +| 512 | 3744 | 636 | 1152 | 1 788 B — 21.8% | + +synth's own log: `sp_init 1048576 -> 2048, reservation 1049216 -> 2688 B (post-link +oracle: stack/static disjoint, all reservation accesses in-range)`. The 640 B delta +above the shadow stack is static data — the 320-byte `RegionTable` plus panic strings. + +**The committed object is the 2048 build.** + +### The constraint this surfaces + +At the standard budget **this one module takes 40.6% of the STM32F100RB's RAM**. The +isolation core is three modules, and a system needs the OS and the application too. +Either the shadow-stack budget comes down for this module, or the F100 does not host +a multi-partition configuration. That is a finding for the partition work, not a +detail of this file. + +And the budget is **asserted, not proven** — the same `2048 of 8192` gap already +recorded against `REQ-OS-OBJVERIFY-001`. scry computes the depth; wiring it is the +open step. + +## BIN-VERIFY + + 7 functions run · 7 rules verified · 0 failed · 0 unknown + rules: i32.add · i32.and · i32.eq · i32.eqz · i32.gt_u · i32.ne + 20 LRAT-certified I64 expansions + 3 functions with no computational rules + +**Not a zero-gap result.** The object contains **356 `i32.const`**, skipped by +BIN-VERIFY as a register operation and `Admitted` in Rocq (`i32_const_correct`) — so +neither half covers it. synth#933 (the proof gap), synth#935 (that the gap is +invisible in the tool's output). More than ten times HM's 29 occurrences. + +## What this does NOT establish + +- **No evidence-on-wasm.** No witness MC/DC, no scry, and the `REQ-OS-ISO-001` + oracles have not been re-run against the wasm build. BIN-VERIFY shows the lowering + is faithful, not that the wasm refines the Verus-proven Rust. +- **Not executed.** Nothing has run this object, on silicon or under Renode. +- **The seam is still native.** `mpu_write` remains trusted platform code, including + its barrier-pairing contract. What moved is the region-programming *policy*. +- **`partition_switch` (3 seams) remains** — the last stage-2 module. + +## Reproduce + + cd benches/gust/drivers/mpu-thin && cargo build --release --target wasm32-unknown-unknown + wasm-tools component new target/wasm32-unknown-unknown/release/gust_mpu_thin.wasm -o mpu.component.wasm + meld fuse mpu.component.wasm --memory shared -o mpu.fused.wasm + loom optimize mpu.fused.wasm --passes inline --attestation false -o mpu.loom.wasm + synth compile mpu.loom.wasm --target cortex-m3 --all-exports --relocatable \ + --native-pointer-abi --shadow-stack-size 2048 -o mpu-thin-cm3.o + synth verify mpu.loom.wasm mpu-thin-cm3.o # needs a --features verify build diff --git a/benches/gust/drivers/mpu-thin/mpu-thin-cm3.o b/benches/gust/drivers/mpu-thin/mpu-thin-cm3.o new file mode 100644 index 0000000..dc4e1ef Binary files /dev/null and b/benches/gust/drivers/mpu-thin/mpu-thin-cm3.o differ diff --git a/benches/gust/drivers/mpu-thin/src/lib.rs b/benches/gust/drivers/mpu-thin/src/lib.rs new file mode 100644 index 0000000..c68dd4a --- /dev/null +++ b/benches/gust/drivers/mpu-thin/src/lib.rs @@ -0,0 +1,329 @@ +//! SPIKE — gust:mpu thin-seam I-ISO region-programming core. +//! Bodies lifted VERBATIM from plain/src/mpu_switch.rs (Verus+Kani verified). +//! The single native atom `mpu_write` arrives as a WIT-typed component import. +#![no_std] +#[panic_handler] +fn ph(_: &core::panic::PanicInfo) -> ! { loop {} } + +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: "mpu-thin", path: "wit", generate_all }); + +mod mpu { +pub const MIN_REGION_SIZE: u32 = 32; +pub fn is_power_of_two(n: u32) -> bool { + let result = n > 0 && (n & (n - 1)) == 0; + result +} + +pub fn validate_region(base: u32, size: u32) -> bool { + if size == 0 { + return false; + } + let power_of_two = (size & (size - 1)) == 0; + let min_size = size >= MIN_REGION_SIZE; + let aligned = (base & (size - 1)) == 0; + let no_overflow = base.checked_add(size).is_some(); + power_of_two && min_size && aligned && no_overflow +} +} + +mod iso { + use crate::mpu::MIN_REGION_SIZE; + // the seam: what was `unsafe extern "C" fn mpu_write` is now a typed import + pub fn mpu_write(rnr: u32, rbar: u32, rasr: u32) { + crate::gust::mpu::regs::mpu_write(rnr, rbar, rasr); + } + pub const MAX_PARTITIONS: usize = 4; + + pub const MAX_REGIONS: usize = 8; + + pub const TABLE_SLOTS: usize = 32; + + pub const SEQ_LEN: usize = 10; + + pub const REQUIRED_DREGION: u32 = 8; + + pub const MPU_CTRL_ID: u32 = 0xFFFF_FFFF; + + pub const MPU_CTRL_ENABLE: u32 = 1; + + pub const MPU_CTRL_DISABLE: u32 = 0; + + #[derive(Clone, Copy)] + pub struct MpuWrite { + /// Region number (RNR), or `MPU_CTRL_ID` for the trailing enable. + pub rnr: u32, + /// Region base address register value (RBAR). + pub rbar: u32, + /// Region attribute and size register value (RASR), or the MPU_CTRL + /// value for the trailing enable write. + pub rasr: u32, + } + + #[derive(Clone, Copy)] + pub struct ProgramSeq { + pub w: [MpuWrite; SEQ_LEN], + } + + pub struct RegionTable { + pub base: [u32; TABLE_SLOTS], + pub size: [u32; TABLE_SLOTS], + pub enabled: [bool; TABLE_SLOTS], + pub writable: [bool; TABLE_SLOTS], + } + + pub fn size_field(size: u32) -> u32 { + if size == 32 { + 4 + } else if size == 64 { + 5 + } else if size == 128 { + 6 + } else if size == 256 { + 7 + } else if size == 512 { + 8 + } else if size == 1024 { + 9 + } else if size == 2048 { + 10 + } else if size == 4096 { + 11 + } else if size == 8192 { + 12 + } else if size == 16384 { + 13 + } else if size == 32768 { + 14 + } else if size == 65536 { + 15 + } else if size == 131072 { + 16 + } else if size == 262144 { + 17 + } else if size == 524288 { + 18 + } else if size == 1048576 { + 19 + } else if size == 2097152 { + 20 + } else if size == 4194304 { + 21 + } else if size == 8388608 { + 22 + } else if size == 16777216 { + 23 + } else if size == 33554432 { + 24 + } else if size == 67108864 { + 25 + } else if size == 134217728 { + 26 + } else if size == 268435456 { + 27 + } else if size == 536870912 { + 28 + } else if size == 1073741824 { + 29 + } else if size == 2147483648 { + 30 + } else { + 0 + } + } + + pub fn rasr_for(size: u32, writable: bool) -> u32 { + let f = size_field(size); + let ap: u32 = if writable { 3 } else { 6 }; + 1u32 + 2u32 * f + 0x0100_0000u32 * ap + } + + fn emit_write(w: &MpuWrite) { + unsafe { mpu_write(w.rnr, w.rbar, w.rasr) }; + } + + pub fn apply_program(seq: &ProgramSeq) { + let mut i: usize = 0; + while i < SEQ_LEN { + emit_write(&seq.w[i]); + i += 1; + } + } + + impl RegionTable { + /// An all-disabled table (the deny-everything baseline). Real + /// deployments construct their static per-partition configuration as + /// a constant and discharge `table_inv` at build time. + pub fn new() -> RegionTable { + RegionTable { + base: [0u32; TABLE_SLOTS], + size: [0u32; TABLE_SLOTS], + enabled: [false; TABLE_SLOTS], + writable: [false; TABLE_SLOTS], + } + } + /// Compute the exact register-write sequence for switching the MPU to + /// partition `part` — the verified heart of I-ISO. See the module + /// header for P1–P4. + pub fn program_partition(&self, part: u32) -> ProgramSeq { + let mut out = ProgramSeq { + w: [MpuWrite { + rnr: 0, + rbar: 0, + rasr: 0, + }; SEQ_LEN], + }; + out.w[0] = MpuWrite { + rnr: MPU_CTRL_ID, + rbar: 0, + rasr: MPU_CTRL_DISABLE, + }; + let mut r: usize = 0; + while r < MAX_REGIONS { + let i = (part as usize) * MAX_REGIONS + r; + if self.enabled[i] { + let rasr = rasr_for(self.size[i], self.writable[i]); + out.w[r + 1] = MpuWrite { + rnr: r as u32, + rbar: self.base[i], + rasr, + }; + } else { + out.w[r + 1] = MpuWrite { + rnr: r as u32, + rbar: 0, + rasr: 0, + }; + } + r += 1; + } + out.w[MAX_REGIONS + 1] = MpuWrite { + rnr: MPU_CTRL_ID, + rbar: 0, + rasr: MPU_CTRL_ENABLE, + }; + out + } + /// Program the MPU for partition `part`: compute the verified + /// sequence, then emit it through the trusted seam — the one call a + /// partition switch makes. The computation and the emission loop are + /// verified; only the single register store is trusted. + pub fn switch_to_partition(&self, part: u32) { + let seq = self.program_partition(part); + apply_program(&seq); + } + /// Verified table builder: add region request (`base`, `size`, + /// `writable`) to partition `part`'s FIRST free slot. + /// + /// Rejects (returns `false`, table proven unchanged — B2) when: + /// * `part` is out of range (defensive: keeps the stripped exec + /// builder total — no panic on any input), + /// * `size` is not a power of two >= `MIN_REGION_SIZE` (32) — the + /// same characterisation `crate::mpu::validate_region` enforces, + /// reusing the verified `crate::mpu::is_power_of_two`, + /// * `base` is not `size`-aligned, + /// * `base + size` wraps the address space (the U-6 bound), + /// * the request OVERLAPS an enabled region already granted to + /// `part` (THE isolation-bearing check), or + /// * all of `part`'s region slots are occupied. + /// + /// On acceptance the resulting table is proven to still satisfy + /// `table_inv` (B1) — in particular the new region is well-formed and + /// disjoint from every other enabled region of `part` — so a caller + /// building exclusively through `new()` + `try_add_region` cannot + /// construct an isolation-violating table, and `program_partition`'s + /// precondition holds on the result by construction. + pub fn try_add_region( + &mut self, + part: u32, + base: u32, + size: u32, + writable: bool, + ) -> bool { + if part >= MAX_PARTITIONS as u32 { + return false; + } + if !crate::mpu::is_power_of_two(size) { + return false; + } + if size < MIN_REGION_SIZE { + return false; + } + if base % size != 0 { + return false; + } + if base.checked_add(size).is_none() { + return false; + } + let mut r: usize = 0; + while r < MAX_REGIONS { + let i = (part as usize) * MAX_REGIONS + r; + if self.enabled[i] { + if !(base + size <= self.base[i] || self.base[i] + self.size[i] <= base) + { + return false; + } + } + r += 1; + } + let mut f: usize = 0; + while f < MAX_REGIONS { + let i = (part as usize) * MAX_REGIONS + f; + if !self.enabled[i] { + self.base[i] = base; + self.size[i] = size; + self.writable[i] = writable; + self.enabled[i] = true; + return true; + } + f += 1; + } + false + } + /// Exec mirror of `covers`, proven equivalent: does some enabled + /// region of partition `part` contain `addr`? Post-strip this is the + /// plain runtime query for what the builder granted (and the + /// Kani-checkable form of `covers`). + pub fn covers_addr(&self, part: u32, addr: u32) -> bool { + let mut r: usize = 0; + while r < MAX_REGIONS { + let i = (part as usize) * MAX_REGIONS + r; + if self.enabled[i] && self.base[i] <= addr + && addr - self.base[i] < self.size[i] + { + return true; + } + r += 1; + } + false + } + }} + +// One instance owns the table — the exec-provider construction. +static mut TABLE: Option = None; +fn table() -> &'static mut iso::RegionTable { + unsafe { + if TABLE.is_none() { TABLE = Some(iso::RegionTable::new()); } + TABLE.as_mut().unwrap() + } +} + +struct P; +impl exports::gust::mpu::iso::Guest for P { + fn size_field(size: u32) -> u32 { iso::size_field(size) } + fn rasr_for(size: u32, writable: bool) -> u32 { iso::rasr_for(size, writable) } + fn try_add_region(part: u32, base: u32, size: u32, writable: bool) -> bool { + table().try_add_region(part, base, size, writable) + } + fn covers_addr(part: u32, addr: u32) -> bool { table().covers_addr(part, addr) } + fn switch_to_partition(part: u32) { table().switch_to_partition(part) } +} +export!(P); diff --git a/benches/gust/drivers/mpu-thin/wit/gust-mpu.wit b/benches/gust/drivers/mpu-thin/wit/gust-mpu.wit new file mode 100644 index 0000000..d364256 --- /dev/null +++ b/benches/gust/drivers/mpu-thin/wit/gust-mpu.wit @@ -0,0 +1,25 @@ +package gust:mpu@0.1.0; + +/// The one native atom: write one MPU register triple. rnr < MAX_REGIONS programs +/// RNR/RBAR/RASR; rnr == 0xFFFFFFFF writes MPU_CTRL from `rasr`. Barrier pairing is +/// the platform layer's trusted contract — see plain/src/mpu_switch.rs. +interface regs { + mpu-write: func(rnr: u32, rbar: u32, rasr: u32); +} + +/// The verified region-programming core. Table state lives in this component +/// instance — exactly one instance may own it, the exec-provider construction. +interface iso { + /// RASR SIZE field for a byte size (pure). + size-field: func(size: u32) -> u32; + /// Full RASR word for a size + writability (pure). + rasr-for: func(size: u32, writable: bool) -> u32; + /// Add a region to a partition's slot set; false if it does not fit. + try-add-region: func(part: u32, base: u32, size: u32, writable: bool) -> bool; + /// Does partition `part` cover `addr` in an enabled region? + covers-addr: func(part: u32, addr: u32) -> bool; + /// Program the incoming partition's regions through the seam, in order. + switch-to-partition: func(part: u32); +} + +world mpu-thin { import regs; export iso; }