From 7ef460cb2216bc9d4e844d87d0e17978fbfe442b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:04:30 +0200 Subject: [PATCH 1/8] =?UTF-8?q?docs(#901):=20VCR-MEM-004=20=E2=80=94=20pro?= =?UTF-8?q?of-carrying=20bounds-guard=20elision=20from=20scry=20verdicts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Traceability leads (pulseengine-feature-loop step 1): the typed sw-req for the #901 capability lands BEFORE the implementation, next to VCR-MEM-001 (the sibling scry consumption channel) and linked to VCR-PERF-002 (#494), whose per-site guard-strip mechanism VCR-MEM-004 reuses under a DIFFERENT authority — a whole-module external abstract interpretation hash-bound to one exact module, instead of a per-site ordeal obligation. The seven safety properties (fail-closed hash, absence != safety, fail-closed memory_min_bytes, self-checking (func,pc) key, fail-safe malformed handling, refused fact-spec combination, loud zero-elision) are stated as the deliverable; the speedup is not. status: proposed until the implementation and its oracles land. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/verified-codegen-roadmap.yaml | 125 ++++++++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index b26214df..f3589775 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -3102,6 +3102,131 @@ artifacts: on stack_canary_687 / i64_global_init_649 / control_step self-contained images. + - id: VCR-MEM-004 + type: sw-req + title: "ProvenSafeBoundsChecker: fail-closed elision of software bounds guards from scry's proven-safe verdicts (synth #901, scry #114)" + description: > + WasmBounds (Sudo & Winstein, Stanford CS191 Spring 2026) shows the payoff + end to end: abstract interpretation identifies provably in-bounds wasm + memory accesses, their bounds checks are elided, and they measure 1.21x. + Their motivation IS synth's target — hardware guard pages need virtual + memory, so on no-MMU embedded (and under Memory64 / Custom Page Sizes) + every access falls back to a SOFTWARE bounds check. synth's own + `synth_memory::SoftwareBoundsChecker` documents that cost as + "~25-40% overhead", and `--safety-bounds software` emits the #752 + wraparound-safe SUB/CMP/BHS/UDF/CMP/BLS/UDF guard (16 B) at every i32 + access site. + + Difference from WasmBounds: we own BOTH halves. scry proves the access + in-bounds (sound AI, admit-free Rocq) and synth proves the codegen + correct (Rocq), so the elision is PROOF-CARRYING and ATTESTED rather than + a trusted optimizer flag. This artifact is the CONSUMER side; the producer + is scry #114 (`safe-accesses.json`, schema `scry/safe-accesses/v1`, + FEAT-046 OOB verdicts). Relation to VCR-PERF-002 (#494): #494 already + strips this exact guard, but its authority is a PER-SITE ordeal obligation + discharged inside synth from loom's `wsc.facts` premises. VCR-MEM-004 + reuses the SAME per-site strip mechanism + (`InstructionSelector::apply_mem_bounds_elision`) under a DIFFERENT + authority: a whole-module external abstract interpretation, hash-bound to + one exact module. The two are independent evidence channels for one + mechanism, and the sidecar records WHICH one authorized each site. + + SAFETY PROPERTIES — these are the deliverable, not the speedup: + (1) FAIL CLOSED on `module_sha256` mismatch. The hash is verified + against the EXACT bytes handed to the decoder (post-WAT-parse, + post-loom, post-#418 arena-bind), so any pre-compile module rewrite + that shifts function/op indices ALSO breaks the hash and refuses — + index skew and byte skew collapse into one gate. Eliding on a stale + analysis is a memory-safety hole, not a stale optimization. + (2) ABSENCE MEANS "NOT PROVEN", NEVER "UNSAFE". A site not listed in + `proven_safe` delegates to `SoftwareBoundsChecker` unchanged. The + verdict list is non-exhaustive by contract (WasmBounds' own output + contract), so a partial list must yield a partially-guarded binary. + (3) FAIL CLOSED on `memory_min_bytes` disagreement. Verdicts are proven + against scry's declared floor; if it differs from synth's declared + minimum for this module, every verdict is unsound HERE — refuse and + name both values. (A matching hash implies they agree, so a + mismatch means the producer is broken, and trusting a broken prover + is the hole this artifact closes.) + (4) SELF-CHECKING KEY. `(func, pc)` is the wasmparser operator index + space — `pc` is the 0-based op index within the function body (the + space scry's own guard refinement walks as `ops[pc..pc+4]`, and the + space synth's `op_offsets` side-table and #494's elision marks are + indexed by). Ingestion VALIDATES each entry against the decoded + stream: `func` must exist, `pc` must be in range, and the op at + `pc` must be a memory access whose access width matches the + declared `width`. A mismatch DROPS that entry with a counted + diagnostic — so if the producer ever emits byte offsets instead of + op indices, essentially every entry fails validation and the build + elides NOTHING loudly, instead of stripping the guard off the wrong + access silently. + (5) MALFORMED / MISSING / UNPARSEABLE ⇒ no elisions WITH a diagnostic, + never an error and never partial trust — the `wsc.facts` fail-safe + skew rule (`synth_core::wsc_facts`, loom#231 Q4) applied to a JSON + carrier. + (6) FACT-SPEC COMBINATION REFUSED. `SYNTH_FACT_SPEC` may REWRITE the op + stream before selection (`SpecializedFn::kept`), which renumbers the + index space `pc` is stated in. When a function was specialized, its + scry marks are DROPPED with a loud per-function diagnostic rather + than remapped — a remap is a future increment that must be gated on + its own differential, not assumed. + (7) ZERO-ELISION IS LOUD. `--proven-safe` accepted but nothing stripped + is the failure mode that looks like success. Every reason is named: + file refused, no site validated, `--safety-bounds` not `software`, + or the function took the optimized path (`optimizer_bridge`'s + `push_software_bounds_guard` sites are NOT mark-driven — the same + boundary #494 has). + + ATTESTATION (loop step 6, sigil): every `--proven-safe` compile writes + `.proven-safe-elisions.json` (schema + `synth-proven-safe-elisions-v1`) carrying the accepted/refused verdict + and its reason, `scry_version`, `module_sha256`, `memory_min_bytes`, the + `--safety-bounds` mode, and the per-site elision set (func, pc, op, + width) — emitted ON REFUSAL TOO, so sigil can distinguish "nothing to + elide" from "file rejected" instead of reading a brag sheet. + + CRATE GRAPH (the `shadow_budget.rs` shape, deliberately): ingestion, hash + verification and attestation live in `synth-core` (which already carries + `sha2`/`serde_json`); the named `ProvenSafeBoundsChecker` lives in + `synth-memory/src/bounds.rs` beside the `BoundsChecker` trait and is + DEP-FREE (its whole dep list is `bitflags` and it supports no_std). synth- + memory is `publish = false` and nothing depends on it, so a CLI path dep + is impossible without changing the published surface; the two halves are + joined by this documented contract, not a compile-time link. Named + residual, not hidden. + status: proposed + tags: [codegen, memory, bounds-elision, scry, proof-carrying, attestation, sigil, track-c, synth-901, scry-114] + links: + - type: derives-from + target: VCR-001 + - type: traces-to + target: VCR-MEM-001 + - type: traces-to + target: VCR-PERF-002 + fields: + req-type: functional + priority: should + verification-criteria: > + RED-FIRST, one per safety property, all three failing before the change + (crates/synth-cli/tests/proven_safe_bounds_901.rs, plus dep-free trait + unit tests in synth-memory): (1) a `safe-accesses.json` whose + `module_sha256` is one nibble off elides NOTHING and warns — and the + MUTATION that inverts the hash comparison turns the differential's + out-of-bounds leg RED (a silent OOB access), which is the evidence the + gate is load-bearing rather than decorative; (2) a list covering 5 of + the fixture's 8 access sites leaves EXACTLY 3 guards standing (byte + delta = 5 x 16 B) and an unlisted site still TRAPS under execution; + (3) a full list strips all 8 and the compile stays result-identical to + wasmtime across an in-bounds sweep. Malformed/missing/wrong-schema/ + wrong-`memory_min_bytes` files each elide nothing with a NAMED + diagnostic and exit 0. Execution differential + (scripts/repro/proven_safe_bounds_901_differential.py, unicorn + + wasmtime, CI-wired in the same commit): elided ≡ checked ≡ wasmtime on + every in-bounds case (return value AND full final memory image), and + the not-proven OOB case still traps. Flag-off is byte-identical by + construction (the mark vector defaults empty) and locked by the frozen + anchors 10/10. + # --------------------------------------------------------------------------- # Toolchain completeness — debuggability (not a VCR correctness item, but # Tier-2 depends on the VCR-RA value→location mapping) From 6c4c67bccc5ecaf3340990948bf5c8a7ddb269fa Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:06:55 +0200 Subject: [PATCH 2/8] =?UTF-8?q?feat(#901):=20ProvenSafeBoundsChecker=20?= =?UTF-8?q?=E2=80=94=20the=20scry-informed=20BoundsChecker=20strategy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit synth-memory/src/bounds.rs had a pluggable BoundsChecker trait and four strategies, none of them proof-informed. Adds the fifth: ProvenSafeSites — the (func_index, pc) verdict set, keyed on the wasmparser OPERATOR INDEX (same space as op_offsets and #494's elision marks). Sorted Vec + binary search so the attestation's iteration order is deterministic. ProvenSafeBoundsChecker — one decision per access site. Proven => no check at all + BoundsCheckOverhead::Zero; every other site DELEGATES to SoftwareBoundsChecker unchanged. Deliberately dep-free (this crate's dep list is bitflags alone): JSON ingestion, module_sha256 verification and attestation land next in synth-core. synth-memory is publish=false and synth-cli is published, so a path dep is impossible without changing the published surface — the shadow_budget.rs split, forced here rather than chosen. The two halves are joined by a documented contract, NOT a compile-time link; that is a named residual. The empty set is the FAIL-CLOSED value: every refusal path (hash mismatch, malformed file, missing file, memory_min_bytes disagreement) yields it, and it degrades the module to SoftwareBoundsChecker — never to no checking. There is no constructor that marks a site proven without a ProvenSafeSites lookup. RED-FIRST (mutation, not a shipped lever): making for_site return proven: true unconditionally — i.e. 'absence means safe' — turns absent_site_is_indistinguishable_from_the_software_checker_901 and empty_site_set_checks_everything_901 RED (24 passed / 2 failed). Reverted. Note: --no-default-features (no_std) does not build for this crate and did not before this change — the codegen module uses Vec unconditionally. Not made worse, not papered over. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-memory/src/bounds.rs | 264 ++++++++++++++++++++++++++++++ crates/synth-memory/src/lib.rs | 5 +- 2 files changed, 268 insertions(+), 1 deletion(-) diff --git a/crates/synth-memory/src/bounds.rs b/crates/synth-memory/src/bounds.rs index c918548d..781d01e6 100644 --- a/crates/synth-memory/src/bounds.rs +++ b/crates/synth-memory/src/bounds.rs @@ -52,6 +52,157 @@ impl BoundsChecker for SoftwareBoundsChecker { } } +/// The set of `(func_index, pc)` access sites an external analysis PROVED +/// in-bounds — VCR-MEM-004 / #901, fed by scry's `safe-accesses.json` +/// (schema `scry/safe-accesses/v1`, scry#114). +/// +/// `pc` is the 0-based **wasmparser operator index** within the function body, +/// the same index space synth's `op_offsets` side-table and the #494 per-site +/// elision marks are stated in. +/// +/// **Absence means "not proven", NEVER "unsafe".** The verdict list is +/// non-exhaustive by contract, so a site this set does not contain must fall +/// back to a real check — see [`ProvenSafeBoundsChecker`]. That makes +/// [`ProvenSafeSites::default()`] (the empty set) the **fail-closed** value: +/// every refusal path — hash mismatch, malformed file, missing file — +/// produces it, and it degrades the whole module to [`SoftwareBoundsChecker`] +/// rather than to no checking. +/// +/// Deliberately dep-free (this crate's entire dep list is `bitflags`): the +/// JSON ingestion, `module_sha256` verification and attestation live in +/// `synth_core::proven_safe`, which the compiler driver adapts into this +/// type. Same split as `synth-cli/src/shadow_budget.rs` keeping its decision +/// logic free of `scry_analyze_core` — and here it is forced, since +/// `synth-memory` is `publish = false` while `synth-cli` is published, so a +/// path dep is impossible without changing the published surface. +/// +/// Uses `Vec` like the sibling [`codegen`] module does; this crate's +/// `no_std` cfg is aspirational today (`--no-default-features` does not build +/// for that reason, and did not before this type existed). +#[derive(Debug, Clone, Default, PartialEq, Eq)] +pub struct ProvenSafeSites { + /// Sorted, de-duplicated `(func, pc)` pairs. Site counts per module are + /// small, so a sorted `Vec` + binary search beats a hash set and keeps + /// the attestation's iteration order deterministic. + sites: Vec<(u32, u32)>, +} + +impl ProvenSafeSites { + /// The empty (fail-closed) set: nothing proven, everything checked. + pub fn new() -> Self { + Self::default() + } + + /// Record `(func, pc)` as proven in-bounds against the memory's + /// **guaranteed minimum** size. Wasm memory only grows, so a verdict + /// proven against the floor stays valid under `memory.grow`. + pub fn insert(&mut self, func: u32, pc: u32) { + if let Err(at) = self.sites.binary_search(&(func, pc)) { + self.sites.insert(at, (func, pc)); + } + } + + /// Is this exact site proven? The key is the PAIR — the same `pc` in a + /// different function is a different site and is NOT proven. + pub fn contains(&self, func: u32, pc: u32) -> bool { + self.sites.binary_search(&(func, pc)).is_ok() + } + + /// Number of proven sites. + pub fn len(&self) -> usize { + self.sites.len() + } + + /// True when nothing is proven — the fail-closed state. + pub fn is_empty(&self) -> bool { + self.sites.is_empty() + } + + /// The proven sites of one function, in `pc` order. This is the per-site + /// elision-mark vector the instruction selector consumes. + pub fn pcs_for_func(&self, func: u32) -> Vec { + self.sites + .iter() + .filter(|&&(f, _)| f == func) + .map(|&(_, pc)| pc) + .collect() + } + + /// Every site, in `(func, pc)` order — the attestation's elision set. + pub fn iter(&self) -> impl Iterator + '_ { + self.sites.iter().copied() + } +} + +/// Bounds checking informed by an external proof (VCR-MEM-004 / #901). +/// +/// One instance is a decision **for one access site**. A site scry proved +/// in-bounds needs no check at all ([`BoundsCheckOverhead::Zero`] — the whole +/// point: the ~25-40 % software-check tax goes to zero where the access is +/// proven); every other site delegates to [`SoftwareBoundsChecker`] unchanged, +/// because **absence from the verdict list means "not proven", never +/// "unsafe"**. +/// +/// Build one with [`ProvenSafeBoundsChecker::for_site`]. The soundness of a +/// `proven` instance rests entirely on the verdicts having been bound to THIS +/// module (`module_sha256`) and to THIS memory floor (`memory_min_bytes`) — +/// both verified before the site set is built, both fail-closed. This type +/// deliberately offers no way to mark a site proven without a +/// [`ProvenSafeSites`] lookup, so a refused ingestion (empty set) can only +/// produce delegating checkers. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct ProvenSafeBoundsChecker { + /// Was THIS site proven in-bounds? `false` is the safe default. + proven: bool, +} + +impl ProvenSafeBoundsChecker { + /// The checker for one access site: proven iff `sites` contains it. + pub fn for_site(sites: &ProvenSafeSites, func: u32, pc: u32) -> Self { + Self { + proven: sites.contains(func, pc), + } + } + + /// The checker for a site with no verdict — delegates to + /// [`SoftwareBoundsChecker`]. Also what every refusal path yields. + pub fn not_proven() -> Self { + Self { proven: false } + } + + /// Was this site's check elided on a proof, rather than delegated? + pub fn is_proven(&self) -> bool { + self.proven + } +} + +impl Default for ProvenSafeBoundsChecker { + /// Fail closed: an un-informed checker checks. + fn default() -> Self { + Self::not_proven() + } +} + +impl BoundsChecker for ProvenSafeBoundsChecker { + #[inline] + fn check(&self, memory: &MemoryDescriptor, addr: u32, size: u32) -> Result { + if self.proven { + // Proven in-bounds against the memory's guaranteed minimum: there + // is no check to perform. This is the elision. + return Ok(addr); + } + SoftwareBoundsChecker.check(memory, addr, size) + } + + fn overhead(&self) -> BoundsCheckOverhead { + if self.proven { + BoundsCheckOverhead::Zero + } else { + SoftwareBoundsChecker.overhead() + } + } +} + /// Address masking for power-of-2 memories (~5% overhead) /// /// Instead of checking bounds, mask the address to always be in range. @@ -269,6 +420,119 @@ mod tests { assert!(MaskingBoundsChecker::try_new(100).is_none()); } + // ---- VCR-MEM-004 / #901: ProvenSafeBoundsChecker ------------------------ + + /// PROPERTY 3 (the key is `(func, pc)`): a proven site is proven, and the + /// SAME `pc` in a different function is not. A `pc`-only key would silently + /// elide the wrong function's access. + #[test] + fn proven_safe_site_key_is_the_func_pc_pair_901() { + let mut sites = ProvenSafeSites::new(); + sites.insert(4, 41); + assert!(sites.contains(4, 41)); + assert!( + !sites.contains(5, 41), + "same pc, different func is NOT proven" + ); + assert!( + !sites.contains(4, 42), + "same func, different pc is NOT proven" + ); + // Insert is idempotent and keeps `(func, pc)` order (the attestation + // iterates this). + sites.insert(4, 41); + sites.insert(0, 7); + assert_eq!(sites.len(), 2); + assert_eq!(sites.iter().collect::>(), vec![(0, 7), (4, 41)]); + assert_eq!(sites.pcs_for_func(4), vec![41]); + assert_eq!(sites.pcs_for_func(9), Vec::::new()); + } + + /// PROPERTY 2 — ABSENCE MEANS "NOT PROVEN", NEVER "UNSAFE". A site missing + /// from the verdict list must behave EXACTLY like `SoftwareBoundsChecker` + /// over the whole matrix, including the overflow and boundary cases. + #[test] + fn absent_site_is_indistinguishable_from_the_software_checker_901() { + let mut sites = ProvenSafeSites::new(); + sites.insert(0, 0); // some OTHER site is proven + let mem = make_test_descriptor(65536); + let absent = ProvenSafeBoundsChecker::for_site(&sites, 0, 1); + let sw = SoftwareBoundsChecker; + + for (addr, size) in [ + (0u32, 4u32), + (65532, 4), + (65533, 4), + (65536, 1), + (u32::MAX, 1), + (u32::MAX - 3, 4), + (65535, 1), + ] { + assert_eq!( + absent.check(&mem, addr, size), + sw.check(&mem, addr, size), + "absent site diverged from SoftwareBoundsChecker at ({addr}, {size})" + ); + } + // ...including the cost it advertises: an unproven site pays the check. + assert_eq!(absent.overhead(), BoundsCheckOverhead::Medium); + assert!(!absent.is_proven()); + } + + /// PROPERTY 1 — the FAIL-CLOSED value. Every refusal path (hash mismatch, + /// malformed file, missing file, `memory_min_bytes` disagreement) produces + /// the EMPTY site set, and an empty set must degrade the entire module to + /// `SoftwareBoundsChecker` — never to no checking. Stated at the trait + /// level here; the end-to-end refusal is gated in + /// `synth-cli/tests/proven_safe_bounds_901.rs`. + #[test] + fn empty_site_set_checks_everything_901() { + let refused = ProvenSafeSites::new(); // what a refusal yields + assert!(refused.is_empty()); + let mem = make_test_descriptor(65536); + let sw = SoftwareBoundsChecker; + // Sweep a range of sites: not one of them may come back proven. + for func in 0..4u32 { + for pc in 0..8u32 { + let c = ProvenSafeBoundsChecker::for_site(&refused, func, pc); + assert!(!c.is_proven(), "refused ingestion produced a proven site"); + assert_eq!(c.overhead(), BoundsCheckOverhead::Medium); + assert_eq!(c.check(&mem, 65536, 4), sw.check(&mem, 65536, 4)); + assert_eq!(c.check(&mem, 0, 4), sw.check(&mem, 0, 4)); + } + } + // The Default impl is the same fail-closed decision. + assert!(!ProvenSafeBoundsChecker::default().is_proven()); + assert_eq!( + ProvenSafeBoundsChecker::default().check(&mem, 65536, 4), + Err(Trap::OutOfBounds) + ); + } + + /// The elision itself: a proven site performs NO check (that is the point) + /// and advertises `Zero` overhead. The address is returned unchanged even + /// where the software checker would trap — which is exactly why the + /// `module_sha256` + `memory_min_bytes` bindings must fail closed. + #[test] + fn proven_site_elides_the_check_entirely_901() { + let mut sites = ProvenSafeSites::new(); + sites.insert(4, 41); + let mem = make_test_descriptor(65536); + let proven = ProvenSafeBoundsChecker::for_site(&sites, 4, 41); + + assert!(proven.is_proven()); + assert_eq!(proven.overhead(), BoundsCheckOverhead::Zero); + assert_eq!(proven.check(&mem, 0, 4), Ok(0)); + assert_eq!(proven.check(&mem, 65532, 4), Ok(65532)); + // No check is performed — the proof, not the checker, is what keeps + // this in bounds. + assert_eq!(proven.check(&mem, 65536, 4), Ok(65536)); + assert_eq!( + SoftwareBoundsChecker.check(&mem, 65536, 4), + Err(Trap::OutOfBounds) + ); + } + #[test] fn test_no_bounds_checker() { let checker = NoBoundsChecker; diff --git a/crates/synth-memory/src/lib.rs b/crates/synth-memory/src/lib.rs index 6c36c00c..7a322aa0 100644 --- a/crates/synth-memory/src/lib.rs +++ b/crates/synth-memory/src/lib.rs @@ -19,7 +19,10 @@ pub mod platform; #[cfg(feature = "std")] pub mod space; -pub use bounds::{BoundsChecker, MaskingBoundsChecker, SoftwareBoundsChecker}; +pub use bounds::{ + BoundsChecker, MaskingBoundsChecker, ProvenSafeBoundsChecker, ProvenSafeSites, + SoftwareBoundsChecker, +}; pub use descriptor::{MemoryDescriptor, MemoryFlags, ProtectionStrategy}; pub use table::{MAX_MEMORIES, MemoryTable}; From 6c740fea545d9f29987797551d0eb0908cc34bdf Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:10:40 +0200 Subject: [PATCH 3/8] =?UTF-8?q?feat(#901):=20synth=5Fcore::proven=5Fsafe?= =?UTF-8?q?=20=E2=80=94=20fail-closed=20safe-accesses.json=20ingestion=20+?= =?UTF-8?q?=20sigil=20attestation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ingests scry's safe-accesses.json (schema scry/safe-accesses/v1, scry#114) and emits the synth-proven-safe-elisions-v1 attestation sidecar. TOTAL by design — no Result in ingest()'s signature, mirroring parse_wsc_facts: the verdicts are an optional accelerator, so no input may turn a successful compile into a failed one. FOUR FAIL-CLOSED GATES, each meaning the same thing (elide NOTHING, warn, exit 0): 1. module_sha256 mismatch. Verified against the EXACT bytes handed to the decoder — after .wat parsing, after loom, after the #418 arena-bind rewrite. Deliberate: those rewrites shift function/operator indices, so binding to the post-rewrite bytes collapses INDEX skew and BYTE skew into one gate. A file produced for the pre-rewrite module fails the hash. The diagnostic names BOTH hashes. 2. memory_min_bytes disagreement. Verdicts are proven against scry's declared floor; a matching hash implies it equals synth's declared minimum, so a mismatch means the producer is BROKEN — and a broken prover is not trusted. Names both values. 3. Wrong schema / malformed JSON / unreadable file. The wsc.facts fail-safe skew rule applied to a JSON carrier. Unknown JSON fields are tolerated (a newer scry must not break an older synth). 4. THE KEY IS SELF-CHECKING. validate_function() checks every entry against the DECODED op stream: pc in range, the op there IS a linear-memory access, and its access width EQUALS the declared width. Failures are dropped per-entry with a counted diagnostic. So if a producer ever emits wasm BYTE OFFSETS instead of operator indices, essentially every entry falls out of range and the build elides NOTHING loudly — instead of stripping the guard off the wrong access silently. That is what makes the open scry#114 'pc' reading safe to bet on. A refused document is NOT trusted piecemeal: offered is emptied wholesale. ATTESTATION: ElisionAttestation is emitted ON REFUSAL TOO, carrying accepted:false + the reason + sites_offered/sites_elided/sites_not_elided, so sigil can distinguish 'nothing to elide' from 'file rejected'. A sidecar that only appears on success is a brag sheet, not an attestation. Each elision carries an 'authority' field so a site elided under a different authority (#494's per-site ordeal certificate) stays distinguishable. RED-FIRST (mutation): deleting the hash gate and the memory-floor gate turns hash_mismatch_refuses_everything_901, one_flipped_module_byte_refuses_901 and memory_min_bytes_disagreement_refuses_901 RED (12 passed / 3 failed). Reverted. 15/15 green, clippy -D warnings clean. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-core/src/lib.rs | 1 + crates/synth-core/src/proven_safe.rs | 850 +++++++++++++++++++++++++++ 2 files changed, 851 insertions(+) create mode 100644 crates/synth-core/src/proven_safe.rs diff --git a/crates/synth-core/src/lib.rs b/crates/synth-core/src/lib.rs index 3f946fa4..3ac13560 100644 --- a/crates/synth-core/src/lib.rs +++ b/crates/synth-core/src/lib.rs @@ -11,6 +11,7 @@ pub mod component; pub mod dwarf_line; pub mod error; pub mod ir; +pub mod proven_safe; pub mod provenance; pub mod safety_manifest; pub mod sbom; diff --git a/crates/synth-core/src/proven_safe.rs b/crates/synth-core/src/proven_safe.rs new file mode 100644 index 00000000..11bdc067 --- /dev/null +++ b/crates/synth-core/src/proven_safe.rs @@ -0,0 +1,850 @@ +//! `safe-accesses.json` ingestion — VCR-MEM-004 / #901. +//! +//! scry (the PROVER, scry#114 / FEAT-046) emits a **non-exhaustive** list of +//! wasm memory accesses its sound abstract interpretation proved in-bounds +//! against the memory's guaranteed MINIMUM size. synth consumes it to skip +//! emitting the `--safety-bounds software` guard at exactly those sites: the +//! elision is proof-carrying (scry proves the access, synth's Rocq suite +//! proves the lowering) and attested (`sigil` reads the sidecar this module +//! emits). +//! +//! ```json +//! { "schema": "scry/safe-accesses/v1", "scry_version": "3.2.4", +//! "module_sha256": "", "memory_min_bytes": 65536, +//! "proven_safe": [ { "func": 4, "pc": 41, "op": "i32.load", "width": 4 } ] } +//! ``` +//! +//! # Why this file is nearly all refusal logic +//! +//! Eliding a bounds check on a stale or mis-keyed analysis is a **memory-safety +//! hole**, not a stale optimization. So every question this module can ask is +//! answered fail-closed, and "fail closed" always means the SAME thing: an +//! EMPTY [`synth_memory::ProvenSafeSites`]-shaped verdict set, which degrades +//! the module to the ordinary software bounds check. It never means an error +//! and never means partial trust. +//! +//! 1. **`module_sha256` mismatch ⇒ refuse.** Verified against the exact bytes +//! handed to the decoder — i.e. AFTER `.wat` parsing, after loom, and after +//! the #418 arena-bind rewrite. That is deliberate: those rewrites shift +//! function and operator indices, so binding the hash to the post-rewrite +//! bytes makes index skew and byte skew the SAME gate. A file produced for +//! the pre-rewrite module simply fails the hash and elides nothing. +//! 2. **`memory_min_bytes` disagreement ⇒ refuse.** The verdicts are proven +//! against scry's declared floor; if synth's declared minimum for this +//! module differs, every verdict is unsound HERE. A matching hash implies +//! the two agree, so a mismatch means the producer is broken — and trusting +//! a broken prover is the hole this module exists to close. +//! 3. **Wrong/absent schema, malformed JSON, unreadable file ⇒ refuse** with a +//! diagnostic and exit 0. This is the `wsc.facts` fail-safe skew rule +//! ([`crate::wsc_facts`], loom#231 Q4) applied to a JSON carrier: the +//! verdicts are an optional accelerator, so no input may turn a successful +//! compile into a failed one. +//! 4. **The key is self-checking.** `(func, pc)` is the wasmparser operator +//! index space: `pc` is the 0-based index of the operator within the +//! function body — the space scry's own guard refinement walks +//! (`ops[pc..pc+4]`, scry#114 §2) and the space synth's `op_offsets` +//! side-table and #494's elision marks are already stated in. +//! [`ProvenSafeIngest::validate_function`] checks each entry against the +//! DECODED stream: the op at `pc` must exist, must be a memory access, and +//! its access width must equal the declared `width`. An entry that fails is +//! DROPPED with a counted diagnostic. So if a producer ever emits byte +//! offsets instead of operator indices, essentially every entry fails and +//! the build elides NOTHING loudly — instead of stripping the guard off the +//! wrong access silently. +//! +//! Absence from `proven_safe` means **"not proven"**, never "unsafe": an +//! unlisted site keeps its guard. + +use serde::{Deserialize, Serialize}; +use sha2::{Digest, Sha256}; +use std::path::{Path, PathBuf}; + +use crate::wasm_op::WasmOp; + +/// The producer schema this consumer understands (scry#114). +pub const SAFE_ACCESSES_SCHEMA: &str = "scry/safe-accesses/v1"; + +/// The attestation schema synth emits for sigil. +pub const ELISION_ATTESTATION_SCHEMA: &str = "synth-proven-safe-elisions-v1"; + +// ============================================================================= +// The producer document +// ============================================================================= + +/// One access site scry claims to have proven in-bounds. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct SafeSite { + /// Full wasm function index (imported functions first, then local ones) — + /// the same space as `FunctionOps::index`. + pub func: u32, + /// 0-based operator index within the function body. + pub pc: u32, + /// The operator mnemonic scry saw (e.g. `"i32.load"`). Diagnostic only — + /// the WIDTH is what gets machine-checked, since it is the field whose + /// disagreement would change which bytes are covered. + #[serde(default)] + pub op: String, + /// Access width in bytes. Checked against the decoded op. + pub width: u32, +} + +/// The raw `safe-accesses.json` shape. Unknown fields are IGNORED +/// (forward-compatible with a newer scry adding `premises`/`counts` +/// alongside), but the fields synth's soundness rests on are all required — +/// a missing one is a parse failure, hence a refusal. +#[derive(Debug, Clone, Deserialize)] +struct RawDocument { + schema: String, + #[serde(default)] + scry_version: String, + module_sha256: String, + memory_min_bytes: u64, + #[serde(default)] + proven_safe: Vec, +} + +// ============================================================================= +// Ingestion +// ============================================================================= + +/// The result of ingesting a `safe-accesses.json`. TOTAL by design — there is +/// deliberately no `Result` in [`ingest`]'s return type, mirroring +/// [`crate::wsc_facts::parse_wsc_facts`]: no input may turn a successful +/// compile into a failed one. +/// +/// When [`ProvenSafeIngest::accepted`] is false, [`ProvenSafeIngest::offered`] +/// is EMPTY — a refused document is not trusted piecemeal — and +/// [`ProvenSafeIngest::refusal`] names why. +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub struct ProvenSafeIngest { + /// Did the document clear every whole-file gate (schema, hash, memory + /// floor)? False ⇒ elide nothing. + pub accepted: bool, + /// `Some(reason)` exactly when `accepted` is false. + pub refusal: Option, + /// The producer version string, for the attestation. Empty if absent or + /// the document was unreadable. + pub scry_version: String, + /// The `module_sha256` the document declared (hex, as written). Empty when + /// the document did not parse. + pub declared_module_sha256: String, + /// The sha256 synth computed over the module it is actually compiling. + pub actual_module_sha256: String, + /// The `memory_min_bytes` the document declared. + pub declared_memory_min_bytes: u64, + /// Sites the document offered, once the whole-file gates passed. These are + /// candidates: each still faces [`ProvenSafeIngest::validate_function`]. + pub offered: Vec, + /// Human-facing diagnostics (warnings). Never an error. + pub diagnostics: Vec, +} + +impl ProvenSafeIngest { + /// A refusal: nothing trusted, one named reason. + fn refuse(reason: impl Into) -> Self { + let reason = reason.into(); + Self { + accepted: false, + diagnostics: vec![reason.clone()], + refusal: Some(reason), + ..Self::default() + } + } + + /// Sites this document offered for one function, in `pc` order. + pub fn offered_for_func(&self, func: u32) -> Vec<&SafeSite> { + let mut v: Vec<&SafeSite> = self.offered.iter().filter(|s| s.func == func).collect(); + v.sort_by_key(|s| s.pc); + v + } + + /// **The self-checking key.** Validate this function's offered sites + /// against the operator stream synth actually decoded, and return the + /// operator indices that survive — the per-site elision marks. + /// + /// An entry is DROPPED (with a diagnostic pushed into `notes`) when: + /// - `pc` is out of range for this function's op count; + /// - the op at `pc` is not a linear-memory access; + /// - the op's access width differs from the declared `width`. + /// + /// Dropping rather than refusing the whole file is deliberate and matches + /// the `wsc.facts` per-record rule: a newer scry proving an access class + /// synth does not guard must not invalidate the sites it does guard. The + /// safety direction is preserved either way — a dropped entry keeps its + /// guard. + pub fn validate_function( + &self, + func: u32, + ops: &[WasmOp], + notes: &mut Vec, + ) -> Vec { + let mut marks = Vec::new(); + for site in self.offered_for_func(func) { + let idx = site.pc as usize; + let Some(op) = ops.get(idx) else { + notes.push(format!( + "func {func} pc {} — out of range (function has {} operators); \ + entry DROPPED, guard retained. If the producer emitted wasm BYTE \ + OFFSETS, the key space is wrong: `pc` is the 0-based OPERATOR index", + site.pc, + ops.len() + )); + continue; + }; + let Some(actual_width) = access_width(op) else { + notes.push(format!( + "func {func} pc {} — the operator there is {op:?}, not a linear-memory \ + access; entry DROPPED, guard retained (claimed op '{}')", + site.pc, site.op + )); + continue; + }; + if actual_width != site.width { + notes.push(format!( + "func {func} pc {} — declared width {} B disagrees with the decoded \ + operator {op:?} ({actual_width} B); entry DROPPED, guard retained", + site.pc, site.width + )); + continue; + } + marks.push(idx); + } + marks.sort_unstable(); + marks.dedup(); + marks + } +} + +/// Access width in bytes of a linear-memory operator, or `None` when the +/// operator is not a linear-memory access. +/// +/// This is the width the BOUNDS CHECK covers (the number of bytes touched), +/// not the value width: `i32.load8_u` touches 1 byte, `i64.load32_u` touches 4. +pub fn access_width(op: &WasmOp) -> Option { + Some(match op { + WasmOp::I32Load8S { .. } + | WasmOp::I32Load8U { .. } + | WasmOp::I32Store8 { .. } + | WasmOp::I64Load8S { .. } + | WasmOp::I64Load8U { .. } + | WasmOp::I64Store8 { .. } => 1, + WasmOp::I32Load16S { .. } + | WasmOp::I32Load16U { .. } + | WasmOp::I32Store16 { .. } + | WasmOp::I64Load16S { .. } + | WasmOp::I64Load16U { .. } + | WasmOp::I64Store16 { .. } => 2, + WasmOp::I32Load { .. } + | WasmOp::I32Store { .. } + | WasmOp::I64Load32S { .. } + | WasmOp::I64Load32U { .. } + | WasmOp::I64Store32 { .. } + | WasmOp::F32Load { .. } + | WasmOp::F32Store { .. } => 4, + WasmOp::I64Load { .. } + | WasmOp::I64Store { .. } + | WasmOp::F64Load { .. } + | WasmOp::F64Store { .. } => 8, + WasmOp::V128Load { .. } | WasmOp::V128Store { .. } => 16, + _ => return None, + }) +} + +/// Ingest a `safe-accesses.json`, binding it to `module_bytes` (the EXACT +/// bytes synth is compiling) and to `memory_min_bytes` (synth's own declared +/// linear-memory minimum). Total: every input yields a verdict, never an error. +/// +/// `module_bytes` must be the post-`.wat`-parse, post-loom, post-arena-bind +/// buffer handed to the decoder — see the module docs for why that choice +/// makes index skew and byte skew one gate. +pub fn ingest(path: &Path, module_bytes: &[u8], memory_min_bytes: u32) -> ProvenSafeIngest { + let actual = hex_sha256(module_bytes); + + let text = match std::fs::read_to_string(path) { + Ok(t) => t, + Err(e) => { + return ProvenSafeIngest { + actual_module_sha256: actual, + ..ProvenSafeIngest::refuse(format!( + "--proven-safe {}: cannot read the file ({e}); NO bounds guard is \ + elided (fail closed) and the compile continues unchanged", + path.display() + )) + }; + } + }; + + let doc: RawDocument = match serde_json::from_str(&text) { + Ok(d) => d, + Err(e) => { + return ProvenSafeIngest { + actual_module_sha256: actual, + ..ProvenSafeIngest::refuse(format!( + "--proven-safe {}: not a well-formed `{SAFE_ACCESSES_SCHEMA}` document \ + ({e}); NO bounds guard is elided (fail closed) and the compile \ + continues unchanged", + path.display() + )) + }; + } + }; + + if doc.schema != SAFE_ACCESSES_SCHEMA { + return ProvenSafeIngest { + actual_module_sha256: actual, + scry_version: doc.scry_version.clone(), + declared_module_sha256: doc.module_sha256.clone(), + declared_memory_min_bytes: doc.memory_min_bytes, + ..ProvenSafeIngest::refuse(format!( + "--proven-safe {}: schema is '{}', expected '{SAFE_ACCESSES_SCHEMA}'; \ + NO bounds guard is elided (fail closed)", + path.display(), + doc.schema + )) + }; + } + + // ---- GATE 1: the verdicts must be bound to THIS module. ---- + // A stale analysis is a memory-safety hole, not a stale optimization. + if !doc.module_sha256.eq_ignore_ascii_case(&actual) { + return ProvenSafeIngest { + actual_module_sha256: actual.clone(), + scry_version: doc.scry_version.clone(), + declared_module_sha256: doc.module_sha256.clone(), + declared_memory_min_bytes: doc.memory_min_bytes, + ..ProvenSafeIngest::refuse(format!( + "--proven-safe {}: REFUSED — module_sha256 mismatch. The file was produced \ + for {}, but this compile's module hashes to {actual}. Eliding a bounds \ + check on a stale analysis is a memory-safety hole, not a stale \ + optimization, so NO guard is elided. (The hash covers the bytes handed to \ + the decoder — after .wat parsing, after loom, and after the #418 \ + arena-bind rewrite — so a module rewrite that shifts operator indices \ + lands here too.)", + path.display(), + if doc.module_sha256.is_empty() { + "" + } else { + &doc.module_sha256 + } + )) + }; + } + + // ---- GATE 2: the verdicts must be proven against THIS memory floor. ---- + // A matching hash implies these agree; a mismatch means the producer is + // broken, and a broken prover must not be trusted. + if doc.memory_min_bytes != u64::from(memory_min_bytes) { + return ProvenSafeIngest { + actual_module_sha256: actual, + scry_version: doc.scry_version.clone(), + declared_module_sha256: doc.module_sha256.clone(), + declared_memory_min_bytes: doc.memory_min_bytes, + ..ProvenSafeIngest::refuse(format!( + "--proven-safe {}: REFUSED — memory_min_bytes disagreement. The verdicts \ + were proven against a {} B floor; synth's declared linear-memory minimum \ + for this module is {memory_min_bytes} B. The module_sha256 MATCHED, so \ + these should be equal — a disagreement means the producer is broken, and \ + verdicts from a broken prover are not trusted. NO guard is elided.", + path.display(), + doc.memory_min_bytes + )) + }; + } + + let mut diagnostics = Vec::new(); + if doc.proven_safe.is_empty() { + diagnostics.push(format!( + "--proven-safe {}: accepted, but the document proves ZERO access sites — \ + nothing to elide (every guard is retained)", + path.display() + )); + } + + ProvenSafeIngest { + accepted: true, + refusal: None, + scry_version: doc.scry_version, + declared_module_sha256: doc.module_sha256, + actual_module_sha256: actual, + declared_memory_min_bytes: doc.memory_min_bytes, + offered: doc.proven_safe, + diagnostics, + } +} + +/// Lowercase hex sha256 — the `module_sha256` convention. +pub fn hex_sha256(bytes: &[u8]) -> String { + let digest = Sha256::digest(bytes); + let mut s = String::with_capacity(64); + for b in digest { + s.push_str(&format!("{b:02x}")); + } + s +} + +// ============================================================================= +// Attestation (loop step 6 — what sigil reads) +// ============================================================================= + +/// One elided site, as attested. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct AttestedElision { + pub func: u32, + /// Operator index within the function body. + pub pc: u32, + pub op: String, + pub width: u32, + /// Who authorized this elision. `"scry/safe-accesses/v1"` today; the + /// field exists so a future site elided on a DIFFERENT authority (e.g. + /// #494's per-site ordeal certificate) is distinguishable in one file. + pub authority: String, +} + +/// The `synth-proven-safe-elisions-v1` sidecar. +/// +/// **Emitted on refusal too**, carrying `accepted: false` plus the reason and +/// the offered-but-not-elided count. A sidecar that only appears on success is +/// a brag sheet, not an attestation: sigil must be able to tell "nothing to +/// elide" from "file rejected". +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct ElisionAttestation { + pub schema: String, + /// `CARGO_PKG_VERSION` of the synth that produced the ELF. + pub synth_version: String, + /// The producer's version string, as declared. + pub scry_version: String, + /// The sha256 synth computed over the module it compiled. This is the + /// authoritative binding — `declared_module_sha256` is what the file said. + pub module_sha256: String, + pub declared_module_sha256: String, + /// Synth's declared linear-memory minimum, in bytes. + pub memory_min_bytes: u32, + pub declared_memory_min_bytes: u64, + /// The `--safety-bounds` mode in force. Elisions only change emitted bytes + /// under `software`; any other mode is recorded so an auditor sees why the + /// elision count is zero. + pub safety_bounds: String, + /// Did the document clear the whole-file gates? + pub accepted: bool, + /// Why not, when `accepted` is false. + #[serde(skip_serializing_if = "Option::is_none")] + pub refusal: Option, + /// How many sites the document offered. + pub sites_offered: usize, + /// How many survived key validation AND were actually stripped. + pub sites_elided: usize, + /// Offered sites that were dropped — bad key, wrong width, a specialized + /// function, or a non-`software` bounds mode. `offered - elided`. + pub sites_not_elided: usize, + /// The elision set proper. + pub elisions: Vec, + /// Every warning the ingestion and validation emitted, verbatim. + pub diagnostics: Vec, +} + +impl ElisionAttestation { + /// Serialize to pretty JSON. + pub fn to_json(&self) -> String { + serde_json::to_string_pretty(self).expect("ElisionAttestation serializes") + } + + /// `foo.elf` → `foo.proven-safe-elisions.json`, mirroring + /// [`crate::SafetyManifest::sidecar_path`]'s shape. + pub fn sidecar_path(elf_path: &Path) -> PathBuf { + let mut p = elf_path.to_path_buf(); + let stem = elf_path + .file_stem() + .map(|s| s.to_string_lossy().to_string()) + .unwrap_or_else(|| "out".to_string()); + p.set_file_name(format!("{stem}.proven-safe-elisions.json")); + p + } +} + +#[cfg(test)] +mod tests { + use super::*; + use std::io::Write; + + fn write_tmp(name: &str, body: &str) -> PathBuf { + let dir = std::env::temp_dir().join("proven_safe_901_unit"); + std::fs::create_dir_all(&dir).expect("mk tempdir"); + let p = dir.join(name); + let mut f = std::fs::File::create(&p).expect("create"); + f.write_all(body.as_bytes()).expect("write"); + p + } + + const MODULE: &[u8] = b"\0asm\x01\0\0\0 pretend this is a module"; + + fn doc(hash: &str, min: u64, sites: &str) -> String { + format!( + r#"{{ "schema": "scry/safe-accesses/v1", "scry_version": "3.2.4", + "module_sha256": "{hash}", "memory_min_bytes": {min}, + "premises": {{ "bounded_memory": true }}, + "counts": {{ "access_sites": 9, "proven_safe": 1 }}, + "proven_safe": [{sites}] }}"# + ) + } + + // ---- PROPERTY 1: fail closed on module_sha256 mismatch ------------------ + + #[test] + fn hash_mismatch_refuses_everything_901() { + let stale = "0".repeat(64); + let p = write_tmp( + "stale.json", + &doc( + &stale, + 65536, + r#"{"func":0,"pc":1,"op":"i32.load","width":4}"#, + ), + ); + let r = ingest(&p, MODULE, 65536); + assert!(!r.accepted, "a stale analysis must never be accepted"); + assert!( + r.offered.is_empty(), + "a refused document is not trusted piecemeal" + ); + let why = r.refusal.expect("a refusal names its reason"); + assert!(why.contains("module_sha256 mismatch"), "{why}"); + // Both values are named so the operator can tell WHICH module it was for. + assert!(why.contains(&stale), "{why}"); + assert!(why.contains(&hex_sha256(MODULE)), "{why}"); + } + + #[test] + fn matching_hash_is_accepted_and_case_insensitive_901() { + let h = hex_sha256(MODULE).to_uppercase(); + let p = write_tmp( + "good.json", + &doc(&h, 65536, r#"{"func":0,"pc":1,"op":"i32.load","width":4}"#), + ); + let r = ingest(&p, MODULE, 65536); + assert!(r.accepted, "{:?}", r.refusal); + assert_eq!(r.offered.len(), 1); + assert_eq!(r.scry_version, "3.2.4"); + } + + /// Any change to the module — a single flipped byte, which is what a + /// pre-compile rewrite looks like — refuses. + #[test] + fn one_flipped_module_byte_refuses_901() { + let p = write_tmp( + "flip.json", + &doc( + &hex_sha256(MODULE), + 65536, + r#"{"func":0,"pc":1,"op":"i32.load","width":4}"#, + ), + ); + let mut rewritten = MODULE.to_vec(); + rewritten.push(0x00); + let r = ingest(&p, &rewritten, 65536); + assert!(!r.accepted); + assert!(r.refusal.unwrap().contains("module_sha256 mismatch")); + } + + // ---- PROPERTY: fail closed on the memory floor -------------------------- + + #[test] + fn memory_min_bytes_disagreement_refuses_901() { + let p = write_tmp( + "floor.json", + &doc( + &hex_sha256(MODULE), + 131072, + r#"{"func":0,"pc":1,"op":"i32.load","width":4}"#, + ), + ); + let r = ingest(&p, MODULE, 65536); + assert!(!r.accepted); + let why = r.refusal.unwrap(); + assert!(why.contains("memory_min_bytes disagreement"), "{why}"); + assert!(why.contains("131072") && why.contains("65536"), "{why}"); + } + + // ---- PROPERTY: malformed ⇒ no elisions, a diagnostic, never an error ---- + + #[test] + fn malformed_missing_and_wrong_schema_all_refuse_without_erroring_901() { + let h = hex_sha256(MODULE); + let cases = vec![ + ("missing", None), + ("garbage.json", Some("this is not json {{{".to_string())), + ("empty.json", Some(String::new())), + ( + "wrongschema.json", + Some(doc(&h, 65536, "").replace(SAFE_ACCESSES_SCHEMA, "scry/safe-accesses/v2")), + ), + ( + "nohash.json", + Some(r#"{"schema":"scry/safe-accesses/v1","memory_min_bytes":65536}"#.to_string()), + ), + ( + "sitegarbage.json", + Some(doc(&h, 65536, r#"{"func":"four","pc":1,"width":4}"#)), + ), + ]; + for (name, body) in cases { + let p = match body { + Some(b) => write_tmp(name, &b), + None => std::env::temp_dir().join("proven_safe_901_unit/definitely-absent.json"), + }; + let r = ingest(&p, MODULE, 65536); + assert!(!r.accepted, "'{name}' must not be accepted"); + assert!(r.offered.is_empty(), "'{name}' offered sites"); + assert!(r.refusal.is_some(), "'{name}' refused without a reason"); + assert!(!r.diagnostics.is_empty(), "'{name}' refused silently"); + } + } + + #[test] + fn unknown_fields_are_tolerated_901() { + // A newer scry adding fields must not break an older synth. + let p = write_tmp( + "future.json", + &format!( + r#"{{ "schema": "scry/safe-accesses/v1", "scry_version": "9.9.9", + "module_sha256": "{}", "memory_min_bytes": 65536, + "brand_new_field": {{ "nested": [1,2,3] }}, + "proven_safe": [{{"func":0,"pc":1,"op":"i32.load","width":4, + "confidence":"high"}}] }}"#, + hex_sha256(MODULE) + ), + ); + let r = ingest(&p, MODULE, 65536); + assert!(r.accepted, "{:?}", r.refusal); + assert_eq!(r.offered.len(), 1); + } + + #[test] + fn accepted_but_empty_is_diagnosed_901() { + let p = write_tmp("none.json", &doc(&hex_sha256(MODULE), 65536, "")); + let r = ingest(&p, MODULE, 65536); + assert!(r.accepted); + assert!(r.offered.is_empty()); + assert!( + r.diagnostics + .iter() + .any(|d| d.contains("ZERO access sites")), + "an accepted-but-vacuous document must say so: {:?}", + r.diagnostics + ); + } + + // ---- PROPERTY 4: the key is self-checking ------------------------------- + + fn ops() -> Vec { + vec![ + WasmOp::LocalGet(0), // 0 + WasmOp::I32Load { + offset: 0, + align: 2, + }, // 1 — 4 B + WasmOp::LocalGet(0), // 2 + WasmOp::I32Load8U { + offset: 1, + align: 0, + }, // 3 — 1 B + WasmOp::I32Add, // 4 + WasmOp::I64Store { + offset: 8, + align: 3, + }, // 5 — 8 B + ] + } + + #[test] + fn valid_sites_become_marks_901() { + let p = write_tmp( + "marks.json", + &doc( + &hex_sha256(MODULE), + 65536, + r#"{"func":0,"pc":5,"op":"i64.store","width":8}, + {"func":0,"pc":1,"op":"i32.load","width":4}, + {"func":0,"pc":3,"op":"i32.load8_u","width":1}"#, + ), + ); + let r = ingest(&p, MODULE, 65536); + let mut notes = Vec::new(); + assert_eq!(r.validate_function(0, &ops(), &mut notes), vec![1, 3, 5]); + assert!(notes.is_empty(), "{notes:?}"); + } + + /// If the producer ever emits wasm BYTE OFFSETS instead of operator + /// indices, the entries fall out of range or land on non-access operators — + /// so the build elides nothing LOUDLY instead of stripping the wrong guard. + #[test] + fn byte_offsets_instead_of_op_indices_elide_nothing_loudly_901() { + let p = write_tmp( + "byteoffsets.json", + &doc( + &hex_sha256(MODULE), + 65536, + r#"{"func":0,"pc":41,"op":"i32.load","width":4}, + {"func":0,"pc":137,"op":"i32.load8_u","width":1}"#, + ), + ); + let r = ingest(&p, MODULE, 65536); + assert!( + r.accepted, + "the FILE is well formed — only the keys are wrong" + ); + let mut notes = Vec::new(); + assert_eq!( + r.validate_function(0, &ops(), &mut notes), + Vec::::new() + ); + assert_eq!(notes.len(), 2); + assert!( + notes.iter().all(|n| n.contains("out of range")), + "{notes:?}" + ); + assert!(notes[0].contains("OPERATOR index"), "{notes:?}"); + } + + #[test] + fn non_access_operator_is_dropped_901() { + let p = write_tmp( + "nonaccess.json", + &doc( + &hex_sha256(MODULE), + 65536, + r#"{"func":0,"pc":4,"op":"i32.load","width":4}"#, + ), + ); + let mut notes = Vec::new(); + let marks = ingest(&p, MODULE, 65536).validate_function(0, &ops(), &mut notes); + assert_eq!(marks, Vec::::new()); + assert!(notes[0].contains("not a linear-memory access"), "{notes:?}"); + } + + #[test] + fn width_disagreement_is_dropped_901() { + // pc 3 is an i32.load8_u (1 B) but the file claims 4 B: the file and + // the module disagree about which BYTES are covered — drop it. + let p = write_tmp( + "width.json", + &doc( + &hex_sha256(MODULE), + 65536, + r#"{"func":0,"pc":3,"op":"i32.load","width":4}, + {"func":0,"pc":1,"op":"i32.load","width":4}"#, + ), + ); + let mut notes = Vec::new(); + let marks = ingest(&p, MODULE, 65536).validate_function(0, &ops(), &mut notes); + assert_eq!( + marks, + vec![1], + "the sound entry survives, the skewed one does not" + ); + assert_eq!(notes.len(), 1); + assert!( + notes[0].contains("disagrees with the decoded operator"), + "{notes:?}" + ); + } + + #[test] + fn sites_are_keyed_per_function_901() { + let p = write_tmp( + "perfunc.json", + &doc( + &hex_sha256(MODULE), + 65536, + r#"{"func":7,"pc":1,"op":"i32.load","width":4}"#, + ), + ); + let r = ingest(&p, MODULE, 65536); + let mut notes = Vec::new(); + // Function 0 gets nothing: the verdict is func 7's. + assert_eq!( + r.validate_function(0, &ops(), &mut notes), + Vec::::new() + ); + assert!(notes.is_empty()); + assert_eq!(r.validate_function(7, &ops(), &mut notes), vec![1]); + } + + // ---- access_width ------------------------------------------------------ + + #[test] + fn access_width_covers_the_bytes_touched_not_the_value_width_901() { + assert_eq!( + access_width(&WasmOp::I64Load32U { + offset: 0, + align: 2 + }), + Some(4) + ); + assert_eq!( + access_width(&WasmOp::I64Store8 { + offset: 0, + align: 0 + }), + Some(1) + ); + assert_eq!( + access_width(&WasmOp::I32Load16S { + offset: 0, + align: 1 + }), + Some(2) + ); + assert_eq!( + access_width(&WasmOp::F64Load { + offset: 0, + align: 3 + }), + Some(8) + ); + assert_eq!(access_width(&WasmOp::I32Add), None); + assert_eq!(access_width(&WasmOp::LocalGet(0)), None); + } + + // ---- attestation ------------------------------------------------------- + + #[test] + fn attestation_sidecar_path_mirrors_the_safety_manifest_901() { + assert_eq!( + ElisionAttestation::sidecar_path(Path::new("/tmp/foo.elf")), + PathBuf::from("/tmp/foo.proven-safe-elisions.json") + ); + assert_eq!( + ElisionAttestation::sidecar_path(Path::new("out")), + PathBuf::from("out.proven-safe-elisions.json") + ); + } + + #[test] + fn refusal_is_attested_not_hidden_901() { + let a = ElisionAttestation { + schema: ELISION_ATTESTATION_SCHEMA.to_string(), + synth_version: "0.55.0".to_string(), + scry_version: "3.2.4".to_string(), + module_sha256: "aa".repeat(32), + declared_module_sha256: "bb".repeat(32), + memory_min_bytes: 65536, + declared_memory_min_bytes: 65536, + safety_bounds: "software".to_string(), + accepted: false, + refusal: Some("module_sha256 mismatch".to_string()), + sites_offered: 8, + sites_elided: 0, + sites_not_elided: 8, + elisions: Vec::new(), + diagnostics: vec!["refused".to_string()], + }; + let json = a.to_json(); + // sigil must be able to tell "nothing to elide" from "file rejected". + assert!(json.contains("\"accepted\": false")); + assert!(json.contains("module_sha256 mismatch")); + assert!(json.contains("\"sites_offered\": 8")); + assert!(json.contains("\"sites_elided\": 0")); + let back: ElisionAttestation = serde_json::from_str(&json).expect("round-trips"); + assert_eq!(back, a); + } +} From 64a7a99517c5af12b77d025de1b261eed4fc4705 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:18:21 +0200 Subject: [PATCH 4/8] =?UTF-8?q?feat(#901):=20wire=20--proven-safe=20end-to?= =?UTF-8?q?-end=20=E2=80=94=20elision=20marks=20+=20attestation=20sidecar?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New `--proven-safe ` on `synth compile` (--all-exports module path). Ingests scry's safe-accesses.json, validates every (func, pc) key against the decoded operator stream, and strips the --safety-bounds software inline guard at exactly the sites that survive. WIRING — one consumption point, two authorities: CompileConfig::proven_safe_mem_elide is kept SEPARATE from #494's fact_mem_bounds_elide (different authorities: whole-module external AI vs per-site ordeal certificate; the attestation records which covered each site). arm_backend unions them into the existing mark vector, so the scry marks inherit all three of #494's defensive gates for free: - the memory.grow(0) fold index-shift drop (with its own named decline); - direct-selector routing (a marked function never takes the optimized path, which is why optimizer_bridge's push_software_bounds_guard sites need no mark plumbing); - the strip is a no-op unless the mode is actually Software. REFUSALS, all loud, none fatal: - every synth_core::proven_safe gate (hash, memory floor, schema, malformed); - per-function: SYNTH_FACT_SPEC specialized this function, renumbering the index space pc is stated in => marks DROPPED, guards retained. Remapping through SpecializedFn::kept is a future increment that needs its own differential; assuming it would be a silent wrong-site strip; - ZERO-ELISION IS LOUD: flag given + file accepted + nothing stripped names the reason (vacuous document / --safety-bounds not software / no key survived validation, pointing at the byte-offset-vs-operator-index cause). ATTESTATION: .proven-safe-elisions.json on EVERY --proven-safe compile including refusals. FIXTURE scripts/repro/proven_safe_bounds_901.wat — ONE function carrying both halves: 5 accesses off a provably-bounded base (slot & 63) * 16 + 256, and 3 off an unconstrained i32 param that no analysis can bound. So a single binary demonstrates elision AND absence-is-not-safety. Its pinned operator indices were verified against the real decoder (9/11/14/17/22 proven, 24/29/35 not). MEASURED (cortex-m4, --safety-bounds software, symtab slices): probe 232 B -> 152 B = 80 B saved (34.5%), 16 UDF#0 -> 6 .text 392 B -> 312 B stale-hash build: 232 B / 16 UDF — BYTE-IDENTICAL to the baseline. Unguarded floor is 94 B, so the 8-site guard tax is 138 B and proving 5 of 8 sites recovers 80 B of it. 16 B per site — the SAME magnitude #494 publishes, because it is the same guard strip. What is new is the authority, not the per-site win. clippy::large_enum_variant is allowed on Commands with a rationale: the Compile variant crossed the threshold with this flag, clap wants the fields inline, and the enum is built once per process. Frozen anchors 10/10. clippy --workspace --all-targets -D warnings: exit 0. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-backend/src/arm_backend.rs | 48 ++++-- crates/synth-cli/src/main.rs | 200 +++++++++++++++++++++++ crates/synth-core/src/backend.rs | 18 ++ scripts/repro/proven_safe_bounds_901.wat | 83 ++++++++++ 4 files changed, 335 insertions(+), 14 deletions(-) create mode 100644 scripts/repro/proven_safe_bounds_901.wat diff --git a/crates/synth-backend/src/arm_backend.rs b/crates/synth-backend/src/arm_backend.rs index c31592c3..198f340a 100644 --- a/crates/synth-backend/src/arm_backend.rs +++ b/crates/synth-backend/src/arm_backend.rs @@ -340,16 +340,23 @@ fn compile_wasm_to_arm( // walk never crosses (it stops at the first untracked op, so no mark can // follow one). Defense in depth: if the fold fired at all, drop the marks // loudly rather than risk keying a guard elision to the wrong op. - let (fact_div_zero_elide, fact_div_ovf_elide, fact_mem_bounds_elide): ( - &[usize], + // + // VCR-MEM-004 (#901): scry's externally-proven bounds-guard marks ride the + // SAME defensive gate for the SAME reason — they are op-index keyed, so an + // index shift would strip the guard off the wrong access. They are unioned + // with #494's certificate-discharged marks here (one consumption point, + // two authorities; `CompileConfig` keeps them separate so the attestation + // can say which one covered each site). + let (fact_div_zero_elide, fact_div_ovf_elide, mem_bounds_elide): ( &[usize], &[usize], + Vec, ) = if rewritten.len() == wasm_ops.len() { - ( - &config.fact_div_zero_elide, - &config.fact_div_ovf_elide, - &config.fact_mem_bounds_elide, - ) + let mut mem = config.fact_mem_bounds_elide.clone(); + mem.extend_from_slice(&config.proven_safe_mem_elide); + mem.sort_unstable(); + mem.dedup(); + (&config.fact_div_zero_elide, &config.fact_div_ovf_elide, mem) } else { if !config.fact_div_zero_elide.is_empty() || !config.fact_div_ovf_elide.is_empty() @@ -359,7 +366,16 @@ fn compile_wasm_to_arm( "fact-spec: DECLINE guard elision marks dropped — the memory.grow(0) fold shifted op indices (#494 defensive gate); general lowering emitted" ); } - (&[], &[], &[]) + if !config.proven_safe_mem_elide.is_empty() { + eprintln!( + "proven-safe: DECLINE {} bounds-guard elision mark(s) dropped — the \ + memory.grow(0) fold shifted op indices, so the (func, pc) keys no longer \ + name the accesses scry proved (VCR-MEM-004 defensive gate, #901); every \ + guard is retained", + config.proven_safe_mem_elide.len() + ); + } + (&[], &[], Vec::new()) }; let wasm_ops: &[WasmOp] = &rewritten; @@ -543,9 +559,10 @@ fn compile_wasm_to_arm( // marks (empty in every compile without SYNTH_FACT_SPEC + facts). selector .set_fact_div_guard_elisions(fact_div_zero_elide.to_vec(), fact_div_ovf_elide.to_vec()); - // #494 bounds-elision: certificate-discharged memory bounds-guard - // marks (empty in every compile without SYNTH_FACT_SPEC + facts). - selector.set_fact_mem_bounds_elisions(fact_mem_bounds_elide.to_vec()); + // #494 bounds-elision + VCR-MEM-004 (#901): per-site memory + // bounds-guard marks, unioned above. Empty in every compile without + // SYNTH_FACT_SPEC + facts or --proven-safe. + selector.set_fact_mem_bounds_elisions(mem_bounds_elide.clone()); selector.select_with_stack(wasm_ops, num_params) }; let select_direct = || -> Result, String> { @@ -797,9 +814,12 @@ fn compile_wasm_to_arm( // obligation, so every existing compile keeps its path byte-identical. let has_fact_div_elide = !fact_div_zero_elide.is_empty() || !fact_div_ovf_elide.is_empty() - // #494 bounds-elision: memory bounds-guard marks are direct-selector - // keyed for the same reason (IR passes renumber instructions). - || !fact_mem_bounds_elide.is_empty(); + // #494 bounds-elision + VCR-MEM-004 (#901): memory bounds-guard marks + // are direct-selector keyed for the same reason (IR passes renumber + // instructions). This is ALSO why the optimized path's + // `push_software_bounds_guard` sites never need mark plumbing: a + // marked function is routed away from that path entirely. + || !mem_bounds_elide.is_empty(); // #643: the optimized path's global lowering is width-naive — `GlobalGet`/ // `GlobalSet` are single-word `[R9, idx*4]` accesses, which (a) silently // dropped the high word of every i64 global and (b) mis-address every diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 3b29092b..8d446720 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -187,6 +187,14 @@ struct Cli { verbose: bool, } +/// `Compile` carries every CLI flag as an inline field, so it is far larger +/// than the other variants — and it crossed clippy's `large_enum_variant` +/// threshold when `--proven-safe` was added (VCR-MEM-004 / #901). Boxing is +/// the lint's suggested cure but clap's derive expects the fields inline, and +/// this enum is constructed EXACTLY ONCE per process (argument parsing), so +/// the size difference costs nothing measurable. Allowed deliberately rather +/// than contorting the argument surface. +#[allow(clippy::large_enum_variant)] #[derive(Subcommand)] enum Commands { /// Parse and analyze a WebAssembly component @@ -484,6 +492,25 @@ enum Commands { #[arg(long, value_enum, default_value_t = StackLayoutArg::High)] stack_layout: StackLayoutArg, + /// VCR-MEM-004 (#901): path to scry's `safe-accesses.json` (schema + /// `scry/safe-accesses/v1`). Every listed `(func, pc)` access whose + /// key VALIDATES against the decoded operator has its + /// `--safety-bounds software` inline guard elided; every other access + /// keeps it (absence means "not proven", NEVER "unsafe"). + /// + /// FAIL CLOSED: a `module_sha256` that does not match the module being + /// compiled, a `memory_min_bytes` that disagrees with this module's + /// declared floor, a wrong schema, or an unreadable/malformed file + /// elides NOTHING and warns — eliding on a stale analysis is a + /// memory-safety hole, not a stale optimization. Never an error. + /// + /// Writes a `.proven-safe-elisions.json` attestation (schema + /// `synth-proven-safe-elisions-v1`) recording the elision set, the + /// scry version and the module hash — emitted on refusal too, so + /// sigil can tell "nothing to elide" from "file rejected". + #[arg(long, value_name = "PATH")] + proven_safe: Option, + /// #687: size in BYTES of the reserved stack region under /// `--stack-layout=low` (default 4096). Must be a multiple of 8 /// (AAPCS SP alignment) and at least 256. Ignored (with a warning) @@ -616,6 +643,7 @@ fn main() -> Result<()> { volatile_segment, stack_layout, stack_size, + proven_safe, } => { // #882: track whether `-b/--backend` was given explicitly (the // mismatch diagnostics differ: an explicit backend lists the @@ -702,6 +730,7 @@ fn main() -> Result<()> { wcet_hints, volatile_segments, stack_layout, + proven_safe, )?; // If --link requested, invoke the cross-linker @@ -1554,6 +1583,9 @@ fn compile_command( // #687: resolved --stack-layout (self-contained Cortex-M images only; // already validated against --relocatable / non-Cortex-M in main). stack_layout: StackLayout, + // VCR-MEM-004 (#901): path to scry's safe-accesses.json. Consumed only on + // the --all-exports module path; `None` (the default) is byte-identical. + proven_safe: Option, ) -> Result<()> { // Validate backend exists let registry = build_backend_registry(); @@ -1608,6 +1640,7 @@ fn compile_command( wcet_hints, volatile_segments, stack_layout, + proven_safe, ); } @@ -2724,6 +2757,8 @@ fn compile_all_exports( // #687: resolved --stack-layout. `Low` moves the self-contained image's // SP init / linmem / R9 table (and is refused on any ET_REL output). stack_layout: StackLayout, + // VCR-MEM-004 (#901): scry's safe-accesses.json, or None (byte-identical). + proven_safe: Option, ) -> Result<()> { let path = input.context("--all-exports requires an input file")?; @@ -3259,6 +3294,53 @@ fn compile_all_exports( } let a64_substrate_emitted = a64_substrate.as_ref().is_ok_and(|s| s.emitted); + // VCR-MEM-004 (#901): ingest scry's `safe-accesses.json`. TOTAL — every + // refusal path (unreadable, malformed, wrong schema, `module_sha256` + // mismatch, `memory_min_bytes` disagreement) yields "elide nothing" with a + // loud diagnostic and lets the compile proceed, because eliding a bounds + // check on a stale analysis is a memory-safety hole, not a stale + // optimization. The hash is taken over the bytes handed to the DECODER + // (post-`.wat`-parse, post-loom, post-#418 arena-bind), so a pre-compile + // rewrite that shifts operator indices also breaks the hash — index skew + // and byte skew are one gate. + let proven_safe_module_min_bytes = all_memories.first().map(|m| m.initial_bytes()).unwrap_or(0); + let proven_safe_ingest: Option = + proven_safe.as_ref().map(|path| { + let module_bytes: &[u8] = sbom_wasm_bytes.as_deref().unwrap_or(&[]); + if module_bytes.is_empty() { + eprintln!( + "warning: --proven-safe {}: this input has no single module to hash (a multi-module .wast merge); NO bounds guard is elided (fail closed)", + path.display() + ); + } + let r = + synth_core::proven_safe::ingest(path, module_bytes, proven_safe_module_min_bytes); + for d in &r.diagnostics { + eprintln!("warning: proven-safe: {d}"); + } + if r.accepted { + eprintln!( + "proven-safe: ACCEPTED {} — scry {} proved {} access site(s) in-bounds against the {} B floor; module_sha256 {} verified", + path.display(), + if r.scry_version.is_empty() { + "" + } else { + &r.scry_version + }, + r.offered.len(), + r.declared_memory_min_bytes, + &r.actual_module_sha256[..16.min(r.actual_module_sha256.len())], + ); + } + r + }); + // Accumulated across the function loop, for the sigil attestation. + let mut proven_safe_elisions: Vec = Vec::new(); + let mut proven_safe_diagnostics: Vec = proven_safe_ingest + .as_ref() + .map(|r| r.diagnostics.clone()) + .unwrap_or_default(); + // Build compile config from CLI flags let config = CompileConfig { no_optimize, @@ -3478,6 +3560,58 @@ fn compile_all_exports( // bounds every reachable runtime extent (R10 ≥ declared min). func_config.linear_memory_bytes, ); + // VCR-MEM-004 (#901): scry's externally-proven bounds-guard marks for + // THIS function. `pc` is an operator index into the ORIGINAL stream, so + // the marks are only sound when that stream is what the backend + // compiles — see the fact-spec refusal below. + if let Some(ing) = &proven_safe_ingest + && ing.accepted + { + let mut notes = Vec::new(); + let marks = ing.validate_function(func.index, &func.ops, &mut notes); + for n in ¬es { + eprintln!("proven-safe: DROP {n}"); + } + proven_safe_diagnostics.extend(notes); + if spec.is_some() { + // SYNTH_FACT_SPEC rewrote this function's op stream, which + // RENUMBERS the index space `pc` is stated in. Remapping + // through `SpecializedFn::kept` is a future increment that + // needs its own differential; until then the combination is + // REFUSED per function rather than assumed. The guards stay. + if !marks.is_empty() { + let msg = format!( + "func {} ('{name}') — REFUSED: SYNTH_FACT_SPEC specialized this function, renumbering the operator index space the scry verdicts are keyed in. {} externally-proven mark(s) dropped; every guard is retained (VCR-MEM-004, #901)", + func.index, + marks.len() + ); + eprintln!("proven-safe: {msg}"); + proven_safe_diagnostics.push(msg); + } + } else if !marks.is_empty() { + for &pc in &marks { + if let Some(site) = ing + .offered_for_func(func.index) + .into_iter() + .find(|s| s.pc as usize == pc) + { + proven_safe_elisions.push(synth_core::proven_safe::AttestedElision { + func: func.index, + pc: site.pc, + op: site.op.clone(), + width: site.width, + authority: synth_core::proven_safe::SAFE_ACCESSES_SCHEMA.to_string(), + }); + } + } + eprintln!( + "proven-safe: ELIDE func {} ('{name}') — {} bounds guard(s) elided on scry's proof (op indices {marks:?})", + func.index, + marks.len() + ); + func_config.proven_safe_mem_elide = marks; + } + } let (ops_for_compile, op_offsets_for_elf): (&[WasmOp], Vec) = match &spec { Some(s) => { func_config.current_func_block_arity = s.block_arity.clone(); @@ -4047,6 +4181,72 @@ fn compile_all_exports( output.display() ); + // VCR-MEM-004 (#901): write the `synth-proven-safe-elisions-v1` + // attestation next to the output. Emitted whenever --proven-safe was + // given — INCLUDING on refusal — so sigil can attest what was elided and + // on whose authority, and can tell "nothing to elide" from "file + // rejected". Additive; the ELF is unchanged. + if let Some(ing) = &proven_safe_ingest { + // LOUD ZERO-ELISION. "Flag given, file accepted, nothing stripped" is + // the failure mode that looks like success — name the reason. + if ing.accepted && proven_safe_elisions.is_empty() { + let why = if ing.offered.is_empty() { + "the document proves zero access sites".to_string() + } else if safety_bounds != SafetyBounds::Software { + format!( + "--safety-bounds is `{}`, not `software` — there is no inline guard to elide (the verdicts are mode-independent, the strip is not)", + safety_bounds.as_str() + ) + } else { + format!( + "none of the {} offered site(s) survived key validation — see the DROP lines above; if the producer emitted wasm BYTE OFFSETS instead of 0-based OPERATOR indices, that is the cause", + ing.offered.len() + ) + }; + let msg = format!( + "--proven-safe was given and the document was ACCEPTED, but NOTHING was elided: {why}" + ); + eprintln!("warning: proven-safe: {msg}"); + proven_safe_diagnostics.push(msg); + } + let attestation = synth_core::proven_safe::ElisionAttestation { + schema: synth_core::proven_safe::ELISION_ATTESTATION_SCHEMA.to_string(), + synth_version: env!("CARGO_PKG_VERSION").to_string(), + scry_version: ing.scry_version.clone(), + module_sha256: ing.actual_module_sha256.clone(), + declared_module_sha256: ing.declared_module_sha256.clone(), + memory_min_bytes: proven_safe_module_min_bytes, + declared_memory_min_bytes: ing.declared_memory_min_bytes, + safety_bounds: safety_bounds.as_str().to_string(), + accepted: ing.accepted, + refusal: ing.refusal.clone(), + sites_offered: ing.offered.len(), + sites_elided: proven_safe_elisions.len(), + sites_not_elided: ing.offered.len().saturating_sub(proven_safe_elisions.len()), + elisions: proven_safe_elisions.clone(), + diagnostics: proven_safe_diagnostics.clone(), + }; + let sidecar = synth_core::proven_safe::ElisionAttestation::sidecar_path(&output); + std::fs::write(&sidecar, attestation.to_json()).with_context(|| { + format!( + "Failed to write proven-safe attestation: {}", + sidecar.display() + ) + })?; + println!( + " Proven-safe: wrote {} ({}, {} of {} site(s) elided) — {}", + sidecar.display(), + if attestation.accepted { + "accepted" + } else { + "REFUSED — no guard elided" + }, + attestation.sites_elided, + attestation.sites_offered, + synth_core::proven_safe::ELISION_ATTESTATION_SCHEMA, + ); + } + // VCR-DEC-003 (#396): write the synth-provenance-v1 sidecar next to the // output (`.provenance.json`). Additive; the ELF is unchanged. if let Some(pm) = provenance_map { diff --git a/crates/synth-core/src/backend.rs b/crates/synth-core/src/backend.rs index 42cd2901..21e1066f 100644 --- a/crates/synth-core/src/backend.rs +++ b/crates/synth-core/src/backend.rs @@ -388,6 +388,23 @@ pub struct CompileConfig { /// stay — sound). Empty (the default) ⇒ every guard is emitted, /// byte-identical to today. pub fact_mem_bounds_elide: Vec, + /// VCR-MEM-004 (#901): op indices of linear-memory accesses whose + /// `--safety-bounds software` inline guard is elided on an EXTERNAL proof + /// — scry's sound abstract interpretation proved the access in-bounds + /// against the memory's guaranteed minimum size, and the verdict file + /// cleared every fail-closed gate ([`crate::proven_safe::ingest`]: + /// `module_sha256` bound to the exact bytes being compiled, + /// `memory_min_bytes` equal to this module's declared floor, and each + /// entry's `(func, pc)` key validated against the decoded operator at + /// that index). + /// + /// Kept SEPARATE from [`CompileConfig::fact_mem_bounds_elide`] on purpose: + /// the two strip the same guard at the same consumption point, but on + /// different AUTHORITIES (a per-site ordeal certificate vs a whole-module + /// external AI), and the `synth-proven-safe-elisions-v1` attestation + /// records which one covered each site. The ARM backend unions them. + /// Empty (the default) ⇒ every guard is emitted, byte-identical to today. + pub proven_safe_mem_elide: Vec, /// #642: `call_indirect` guard inputs — the compile-time table size for /// the runtime bounds check and the per-expected-type closed-world type /// verdicts — computed from the decoded module by @@ -515,6 +532,7 @@ impl Default for CompileConfig { fact_div_zero_elide: Vec::new(), fact_div_ovf_elide: Vec::new(), fact_mem_bounds_elide: Vec::new(), + proven_safe_mem_elide: Vec::new(), // #642: no guard inputs ⇒ every call_indirect lowering declines // loudly (never an unchecked indirect branch). Driver loops fill // this from the decoded module. diff --git a/scripts/repro/proven_safe_bounds_901.wat b/scripts/repro/proven_safe_bounds_901.wat new file mode 100644 index 00000000..3f7ac346 --- /dev/null +++ b/scripts/repro/proven_safe_bounds_901.wat @@ -0,0 +1,83 @@ +;; VCR-MEM-004 / #901 — the ProvenSafeBoundsChecker fixture. +;; +;; ONE function carrying BOTH halves of the safety contract, so a single +;; compiled binary demonstrates the whole thing: +;; +;; PROVEN half — `$base = 256 + (slot & 63) * 16` is entry-independently +;; within [256, 1264) for ANY runtime `$slot`, so every +;; access off `$base` is in-bounds against the declared +;; 1-page (65536 B) minimum. This is exactly the verdict +;; scry's interval + known-bits domains produce +;; (`region_in_bounds`, scry FEAT-046). Five accesses. +;; +;; NOT-PROVEN half — `$raw` is an unconstrained i32 parameter used directly +;; as an address. No analysis can bound it, so scry never +;; lists these sites. Three accesses. They MUST keep their +;; `--safety-bounds software` guard and MUST still trap when +;; driven out of the page — that is the "absence means NOT +;; PROVEN, never UNSAFE" property, executable. +;; +;; Under `--safety-bounds software` all EIGHT accesses carry the #752 +;; wraparound-safe inline guard (SUB/CMP/BHS/UDF/CMP/BLS/UDF + the address +;; ADD — 16 B per site). With scry's verdicts covering only the five proven +;; sites, exactly five guards fall and exactly three remain. +;; +;; The record layout mirrors a scheduler task record (16 B each, base 256): +;; state u8 @0 · prio u8 @1 · flags u16 @2 · deadline u32 @4 · budget u32 @8 +;; +;; Operator indices (the `pc` key space — 0-based within the function body, +;; the wasmparser operator index space) are pinned in the comments below and +;; re-derived by the oracles, so a decoder drift is visible rather than silent. +;; +;; Oracles: crates/synth-cli/tests/proven_safe_bounds_901.rs (byte evidence + +;; the three fail-closed refusals) and +;; scripts/repro/proven_safe_bounds_901_differential.py (execution), both +;; CI-wired in the proven-safe-oracle job. +(module + (memory (export "mem") 1) + (func (export "probe") (param $slot i32) (param $raw i32) (result i32) + (local $base i32) + (local $acc i32) + ;; ---- base = 256 + (slot & 63) * 16 : PROVABLY in [256, 1264) ---- + local.get $slot ;; op 0 + i32.const 63 ;; op 1 + i32.and ;; op 2 + i32.const 4 ;; op 3 + i32.shl ;; op 4 + i32.const 256 ;; op 5 + i32.add ;; op 6 + local.set $base ;; op 7 + + ;; ---- PROVEN accesses (5) ---- + local.get $base ;; op 8 + i32.load8_u ;; op 9 PROVEN 1 B + local.get $base ;; op 10 + i32.load8_u offset=1 ;; op 11 PROVEN 1 B + i32.add ;; op 12 + local.get $base ;; op 13 + i32.load16_u offset=2 ;; op 14 PROVEN 2 B + i32.add ;; op 15 + local.get $base ;; op 16 + i32.load offset=4 ;; op 17 PROVEN 4 B + i32.add ;; op 18 + local.set $acc ;; op 19 + local.get $base ;; op 20 + i32.const 2 ;; op 21 + i32.store8 ;; op 22 PROVEN 1 B (state := 2, "polled") + + ;; ---- NOT-PROVEN accesses (3): `$raw` is unconstrained ---- + local.get $raw ;; op 23 + i32.load ;; op 24 NOT PROVEN 4 B — must still trap OOB + local.get $acc ;; op 25 + i32.add ;; op 26 + local.set $acc ;; op 27 + local.get $raw ;; op 28 + i32.load8_u offset=3 ;; op 29 NOT PROVEN 1 B — must still trap OOB + local.get $acc ;; op 30 + i32.add ;; op 31 + local.set $acc ;; op 32 + local.get $raw ;; op 33 + local.get $acc ;; op 34 + i32.store offset=8 ;; op 35 NOT PROVEN 4 B — must still trap OOB + + local.get $acc)) ;; op 36 (+ implicit End = op 37) From 9e55747b4cf70c6fdcfc2ebb1d0273bf3d1c9d0f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:23:31 +0200 Subject: [PATCH 5/8] test(#901): byte-evidence gates + the false-attestation fix they found MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 11 end-to-end gates on the REAL compiled bytes of the #901 fixture, one per safety property, all symtab-sliced (never disasm text). MEASURED (cortex-m4, --safety-bounds software, 'probe' symbol): floor (no --safety-bounds) 94 B, 0 UDF#0 guarded (all 8 sites) 232 B, 16 UDF#0 => guard tax 138 B 5 proven elided 152 B, 6 UDF#0 => SAVED 80 B (34.5%) 3 unproven elided (mirror) 182 B, 10 UDF#0 => saved 50 B all 8 elided 94 B, 0 UDF#0 => byte-identical to floor Honest notes recorded in the test, not smoothed over: the guard is NOT a uniform 16 B per site (the address form differs), and 80 + 50 = 130 < 138 because 8 B of address materialization only collapses once NO guard remains. DEFECT THE GATES FOUND: with --safety-bounds NOT software, the marks were still set and the attestation recorded '8 elisions' — but the selector's strip is a no-op outside Software mode, so NOTHING was elided. sigil would have attested elisions that never happened. A false attestation is worse than no attestation. Fixed by gating mark-setting on SafetyBounds::Software; the loud zero-elision diagnostic now names the mode as the reason. RED-FIRST (mutation): deleting the module_sha256 comparison turns stale_hash_elides_nothing_and_is_byte_identical_901 RED — the elision fires on a stale analysis and the .text stops matching the guarded baseline (10 passed / 1 failed). Reverted. Covered: full elision reaching the unguarded floor; the PARTIAL 5-of-8 list leaving exactly the 3 unproven guards (plus its mirror image, so the partition is proven disjoint and complete — not the near-vacuous empty-list version); stale hash; memory_min_bytes disagreement; malformed / missing / wrong-schema / garbage-site documents (all exit 0, byte-identical, attested as refused); the key-space canary (byte offsets instead of operator indices elide nothing LOUDLY); width skew dropping only the skewed site; the attestation contents including per-site authority; and the fact-spec combination refusal (verify-gated). Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-cli/src/main.rs | 15 +- .../synth-cli/tests/proven_safe_bounds_901.rs | 645 ++++++++++++++++++ 2 files changed, 655 insertions(+), 5 deletions(-) create mode 100644 crates/synth-cli/tests/proven_safe_bounds_901.rs diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index 8d446720..c68c58e9 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -3320,7 +3320,7 @@ fn compile_all_exports( } if r.accepted { eprintln!( - "proven-safe: ACCEPTED {} — scry {} proved {} access site(s) in-bounds against the {} B floor; module_sha256 {} verified", + "proven-safe: ACCEPTED {} — scry {} proved {} access site(s) in-bounds against the {} B floor; module_sha256 {} verified", path.display(), if r.scry_version.is_empty() { "" @@ -3564,8 +3564,13 @@ fn compile_all_exports( // THIS function. `pc` is an operator index into the ORIGINAL stream, so // the marks are only sound when that stream is what the backend // compiles — see the fact-spec refusal below. + // Gated on `Software`: that is the ONLY mode that emits an inline + // guard, so it is the only mode where a mark changes a byte. Without + // this gate the attestation would record elisions that never happened + // — a false attestation is worse than no attestation. if let Some(ing) = &proven_safe_ingest && ing.accepted + && safety_bounds == SafetyBounds::Software { let mut notes = Vec::new(); let marks = ing.validate_function(func.index, &func.ops, &mut notes); @@ -3581,7 +3586,7 @@ fn compile_all_exports( // REFUSED per function rather than assumed. The guards stay. if !marks.is_empty() { let msg = format!( - "func {} ('{name}') — REFUSED: SYNTH_FACT_SPEC specialized this function, renumbering the operator index space the scry verdicts are keyed in. {} externally-proven mark(s) dropped; every guard is retained (VCR-MEM-004, #901)", + "func {} ('{name}') — REFUSED: SYNTH_FACT_SPEC specialized this function, renumbering the operator index space the scry verdicts are keyed in. {} externally-proven mark(s) dropped; every guard is retained (VCR-MEM-004, #901)", func.index, marks.len() ); @@ -3605,7 +3610,7 @@ fn compile_all_exports( } } eprintln!( - "proven-safe: ELIDE func {} ('{name}') — {} bounds guard(s) elided on scry's proof (op indices {marks:?})", + "proven-safe: ELIDE func {} ('{name}') — {} bounds guard(s) elided on scry's proof (op indices {marks:?})", func.index, marks.len() ); @@ -4194,7 +4199,7 @@ fn compile_all_exports( "the document proves zero access sites".to_string() } else if safety_bounds != SafetyBounds::Software { format!( - "--safety-bounds is `{}`, not `software` — there is no inline guard to elide (the verdicts are mode-independent, the strip is not)", + "--safety-bounds is `{}`, not `software` — there is no inline guard to elide (the verdicts are mode-independent, the strip is not)", safety_bounds.as_str() ) } else { @@ -4204,7 +4209,7 @@ fn compile_all_exports( ) }; let msg = format!( - "--proven-safe was given and the document was ACCEPTED, but NOTHING was elided: {why}" + "--proven-safe was given and the document was ACCEPTED, but NOTHING was elided: {why}" ); eprintln!("warning: proven-safe: {msg}"); proven_safe_diagnostics.push(msg); diff --git a/crates/synth-cli/tests/proven_safe_bounds_901.rs b/crates/synth-cli/tests/proven_safe_bounds_901.rs new file mode 100644 index 00000000..922296de --- /dev/null +++ b/crates/synth-cli/tests/proven_safe_bounds_901.rs @@ -0,0 +1,645 @@ +//! VCR-MEM-004 / #901 — end-to-end byte gates for `--proven-safe`. +//! +//! The three safety properties the lane exists to establish, each locked on +//! the REAL compiled bytes of `scripts/repro/proven_safe_bounds_901.wat` (one +//! function, 8 `--safety-bounds software` guarded accesses: 5 off a provably +//! bounded base, 3 off an unconstrained i32 param): +//! +//! 1. **FAIL CLOSED on `module_sha256` mismatch** — a stale verdict file +//! elides NOTHING and the `.text` is BYTE-IDENTICAL to the guarded +//! baseline. Also covered: a wrong `memory_min_bytes`, a wrong schema, a +//! malformed file and a missing file. Every one warns and exits 0. +//! 2. **ABSENCE MEANS "NOT PROVEN", NEVER "UNSAFE"** — a list covering 5 of +//! the 8 sites leaves EXACTLY 3 guards standing (80 B = 5 x 16 B saved), +//! and the 3 survivors are precisely the `$raw`-addressed ones. Proven by +//! a partial list, not by an empty one. +//! 3. **A GENUINE ELISION** — the full 8-site list strips every guard and +//! lands byte-identical to the `--safety-bounds`-off floor: under the +//! proof, the sandbox tax is exactly zero. +//! +//! Plus the key-space canary (byte offsets instead of operator indices elide +//! nothing LOUDLY), the loud zero-elision diagnostics, and the sigil +//! attestation on BOTH the accepted and the refused path. +//! +//! Execution evidence (elided ≡ checked ≡ wasmtime in-bounds; a NOT-proven +//! out-of-bounds access still TRAPS) lives in +//! `scripts/repro/proven_safe_bounds_901_differential.py`. Frozen anchors are +//! untouched by construction — the mark vector defaults empty. + +use object::{Object, ObjectSection, ObjectSymbol}; +use std::path::PathBuf; +use std::process::Command; +use synth_core::proven_safe::hex_sha256; + +fn synth() -> &'static str { + env!("CARGO_BIN_EXE_synth") +} + +/// The fixture's PROVEN access sites: `(pc, op, width)`. Pinned here and in +/// the `.wat` comments; the ingestion re-validates each against the decoded +/// operator, so a decoder drift fails loudly rather than eliding a wrong site. +const PROVEN: &[(u32, &str, u32)] = &[ + (9, "i32.load8_u", 1), + (11, "i32.load8_u", 1), + (14, "i32.load16_u", 2), + (17, "i32.load", 4), + (22, "i32.store8", 1), +]; + +/// The fixture's NOT-PROVEN sites — `$raw` is an unconstrained parameter. +const NOT_PROVEN: &[(u32, &str, u32)] = &[ + (24, "i32.load", 4), + (29, "i32.load8_u", 1), + (35, "i32.store", 4), +]; + +/// MEASURED guard cost on this fixture (cortex-m4, symtab slices). The #752 +/// wraparound-safe guard is NOT a uniform size — the address form differs per +/// site — so these are the measured partition costs, not a per-site formula: +/// +/// floor (no --safety-bounds) probe = 94 B, 0 UDF#0 +/// guarded (all 8 sites) probe = 232 B, 16 UDF#0 => tax 138 B +/// 5 proven elided probe = 152 B, 6 UDF#0 => saved 80 B +/// 3 unproven elided (mirror image) probe = 182 B, 10 UDF#0 => saved 50 B +/// +/// 80 + 50 = 130 < 138: eliding EVERY guard additionally collapses 8 B of +/// address materialization that survives while any guard remains. Recorded +/// because it is the honest number, not the flattering one. +const TAX_ALL_8: usize = 138; +const SAVED_PROVEN_5: usize = 80; +const SAVED_UNPROVEN_3: usize = 50; + +const UDF0: u16 = 0xDE00; + +fn dir() -> PathBuf { + let d = std::env::temp_dir().join("proven_safe_bounds_901"); + std::fs::create_dir_all(&d).expect("mk tempdir"); + d +} + +fn fixture_wasm() -> Vec { + let path = PathBuf::from(env!("CARGO_MANIFEST_DIR")) + .join("../..") + .join("scripts/repro/proven_safe_bounds_901.wat"); + let wat = std::fs::read(path).expect("read fixture wat"); + wat::parse_bytes(&wat) + .expect("fixture wat must parse") + .into_owned() +} + +/// Build a `scry/safe-accesses/v1` document over `sites`. +fn safe_accesses(hash: &str, min_bytes: u64, sites: &[(u32, &str, u32)]) -> String { + let entries: Vec = sites + .iter() + .map(|(pc, op, w)| format!(r#"{{"func":0,"pc":{pc},"op":"{op}","width":{w}}}"#)) + .collect(); + format!( + r#"{{ "schema": "scry/safe-accesses/v1", "scry_version": "3.2.4", + "module_sha256": "{hash}", "memory_min_bytes": {min_bytes}, + "premises": {{ "bounded_memory": true }}, + "counts": {{ "access_sites": 8, "proven_safe": {} }}, + "proven_safe": [{}] }}"#, + sites.len(), + entries.join(",\n") + ) +} + +struct Compiled { + text: Vec, + probe: Vec, + stderr: String, + stdout: String, + attestation: Option, +} + +impl Compiled { + fn udf_count(&self) -> usize { + self.probe + .chunks_exact(2) + .filter(|c| u16::from_le_bytes([c[0], c[1]]) == UDF0) + .count() + } +} + +/// Compile the fixture. `verdicts` is the `safe-accesses.json` body (written +/// next to the module), `Some(None)` means "point --proven-safe at a file that +/// does not exist". +fn compile(tag: &str, software_bounds: bool, verdicts: Option>) -> Compiled { + let d = dir(); + let input = d.join(format!("{tag}.wasm")); + let elf = d.join(format!("{tag}.elf")); + std::fs::write(&input, fixture_wasm()).expect("write wasm"); + + let mut cmd = Command::new(synth()); + cmd.args([ + "compile", + input.to_str().unwrap(), + "-o", + elf.to_str().unwrap(), + "-b", + "arm", + "--target", + "cortex-m4", + "--all-exports", + ]); + if software_bounds { + cmd.args(["--safety-bounds", "software"]); + } + if let Some(body) = verdicts { + let json = d.join(format!("{tag}.safe-accesses.json")); + match body { + Some(b) => std::fs::write(&json, b).expect("write verdicts"), + None => { + let _ = std::fs::remove_file(&json); + } + } + cmd.args(["--proven-safe", json.to_str().unwrap()]); + } + // Never let an ambient fact-spec lever perturb these gates. + cmd.env_remove("SYNTH_FACT_SPEC"); + cmd.env_remove("SYNTH_FACT_SPEC_FORCE_ADMIT"); + + let out = cmd.output().expect("run synth"); + assert!( + out.status.success(), + "compile '{tag}' FAILED (a verdict file must never turn a good compile \ + into a failed one): {}", + String::from_utf8_lossy(&out.stderr) + ); + + let bytes = std::fs::read(&elf).expect("read elf"); + let obj = object::File::parse(&*bytes).expect("parse elf"); + let sec = obj.section_by_name(".text").expect(".text"); + let text = sec.data().expect("read .text").to_vec(); + let base = sec.address(); + let end = base + text.len() as u64; + // Symtab slices, never disasm text (the #489 lesson). + let mut syms: Vec<(String, u64)> = obj + .symbols() + .filter(|s| { + let a = s.address() & !1; + !s.name().unwrap_or("").is_empty() && a >= base && a < end + }) + .map(|s| (s.name().unwrap().to_string(), (s.address() & !1) - base)) + .collect(); + syms.sort_by_key(|&(_, a)| a); + let mut probe = Vec::new(); + for (i, (name, start)) in syms.iter().enumerate() { + if name == "probe" { + let stop = syms + .get(i + 1) + .map(|&(_, a)| a as usize) + .unwrap_or(text.len()) + .min(text.len()); + probe = text[*start as usize..stop].to_vec(); + } + } + assert!(!probe.is_empty(), "symbol 'probe' missing from symtab"); + + let att_path = synth_core::proven_safe::ElisionAttestation::sidecar_path(&elf); + let attestation = std::fs::read_to_string(&att_path) + .ok() + .map(|s| serde_json::from_str(&s).expect("attestation is valid JSON")); + + Compiled { + text, + probe, + stderr: String::from_utf8_lossy(&out.stderr).into_owned(), + stdout: String::from_utf8_lossy(&out.stdout).into_owned(), + attestation, + } +} + +fn module_hash() -> String { + hex_sha256(&fixture_wasm()) +} + +fn all_sites() -> Vec<(u32, &'static str, u32)> { + let mut v = PROVEN.to_vec(); + v.extend_from_slice(NOT_PROVEN); + v +} + +// ============================================================================= +// PROPERTY 3 — a genuine elision +// ============================================================================= + +/// The full 8-site proof strips every guard: the `.text` lands BYTE-IDENTICAL +/// to the `--safety-bounds`-off floor. Under the proof the sandbox bounds tax +/// is exactly zero, which is the capability claim. +#[test] +fn full_proof_reaches_the_unguarded_floor_901() { + let floor = compile("floor", false, None); + let guarded = compile("guarded", true, None); + let doc = safe_accesses(&module_hash(), 65536, &all_sites()); + let elided = compile("all8", true, Some(Some(&doc))); + + assert_eq!(guarded.udf_count(), 16, "8 guards x 2 UDF#0 each"); + assert_eq!(elided.udf_count(), 0, "every guard must be gone"); + assert_eq!( + elided.probe, floor.probe, + "a fully proven function must lower EXACTLY like the unguarded floor" + ); + assert_eq!( + guarded.probe.len() - elided.probe.len(), + TAX_ALL_8, + "the whole 8-site guard tax must go" + ); + assert!( + elided.stderr.contains("proven-safe: ACCEPTED"), + "{}", + elided.stderr + ); +} + +// ============================================================================= +// PROPERTY 2 — absence means "not proven", NEVER "unsafe" +// ============================================================================= + +/// A PARTIAL list (5 of 8) must leave EXACTLY 3 guards standing — and the 3 +/// survivors must be the `$raw`-addressed accesses, not an arbitrary 3. Proven +/// against the partial list, not the vacuous empty one. +#[test] +fn partial_proof_leaves_exactly_the_unproven_guards_901() { + let guarded = compile("part_base", true, None); + let doc = safe_accesses(&module_hash(), 65536, PROVEN); + let part = compile("part", true, Some(Some(&doc))); + + assert_eq!( + part.udf_count(), + 6, + "3 unproven sites x 2 UDF#0 must survive; got {} — stderr: {}", + part.udf_count(), + part.stderr + ); + assert_eq!( + guarded.probe.len() - part.probe.len(), + SAVED_PROVEN_5, + "exactly the 5 proven sites' guards may vanish" + ); + // ...and the survivors are structurally the same lowering as a build that + // proves ONLY the three unproven sites' complement: compile the mirror + // image and confirm the two partitions are disjoint and complete. + let mirror_doc = safe_accesses(&module_hash(), 65536, NOT_PROVEN); + let mirror = compile("part_mirror", true, Some(Some(&mirror_doc))); + assert_eq!( + mirror.udf_count(), + 10, + "5 proven sites' guards must survive" + ); + assert_eq!( + guarded.probe.len() - mirror.probe.len(), + SAVED_UNPROVEN_3, + "exactly the 3 unproven sites' guards may vanish in the mirror build" + ); + // The two partitions are disjoint and cover all 8 guards (16 UDF pairs)... + assert_eq!(part.udf_count() + mirror.udf_count(), 16); + // ...though their byte savings sum to LESS than the whole tax: 8 B of + // address materialization only collapses once NO guard remains. + assert_eq!(SAVED_PROVEN_5 + SAVED_UNPROVEN_3 + 8, TAX_ALL_8); + assert!( + part.stderr.contains("op indices [9, 11, 14, 17, 22]"), + "{}", + part.stderr + ); +} + +/// An accepted document that proves NOTHING elides nothing — and says so. +#[test] +fn vacuous_document_elides_nothing_loudly_901() { + let guarded = compile("vac_base", true, None); + let doc = safe_accesses(&module_hash(), 65536, &[]); + let vac = compile("vac", true, Some(Some(&doc))); + assert_eq!(vac.probe, guarded.probe); + assert!( + vac.stderr.contains("ZERO access sites") && vac.stderr.contains("NOTHING was elided"), + "an accepted-but-vacuous document must be loud: {}", + vac.stderr + ); +} + +// ============================================================================= +// PROPERTY 1 — FAIL CLOSED +// ============================================================================= + +/// THE headline refusal: a `module_sha256` that does not name this module +/// elides NOTHING. Byte-identical to the guarded baseline, warns loudly, +/// exits 0. +#[test] +fn stale_hash_elides_nothing_and_is_byte_identical_901() { + let guarded = compile("stale_base", true, None); + // One nibble off — the shape a re-built or rewritten module produces. + let mut h = module_hash(); + let last = h.pop().unwrap(); + h.push(if last == 'a' { 'b' } else { 'a' }); + let doc = safe_accesses(&h, 65536, &all_sites()); + let stale = compile("stale", true, Some(Some(&doc))); + + assert_eq!( + stale.text, guarded.text, + "a stale analysis must not move a single byte" + ); + assert_eq!(stale.udf_count(), 16, "every guard must survive"); + assert!( + stale.stderr.contains("REFUSED — module_sha256 mismatch"), + "{}", + stale.stderr + ); + assert!( + stale.stderr.contains("memory-safety hole"), + "the refusal must say WHY, not just that: {}", + stale.stderr + ); + // Both hashes are named so an operator can tell which module it was for. + assert!(stale.stderr.contains(&h) && stale.stderr.contains(&module_hash())); +} + +/// The verdicts are proven against scry's declared floor. If it disagrees with +/// synth's declared minimum, the producer is broken — refuse. +#[test] +fn memory_min_bytes_disagreement_elides_nothing_901() { + let guarded = compile("floor_base", true, None); + let doc = safe_accesses(&module_hash(), 131072, &all_sites()); + let bad = compile("floorbad", true, Some(Some(&doc))); + assert_eq!(bad.text, guarded.text); + assert!( + bad.stderr.contains("memory_min_bytes disagreement"), + "{}", + bad.stderr + ); +} + +/// Malformed, missing and wrong-schema documents: no elisions, a diagnostic, +/// exit 0 — never an error, never partial trust. The `wsc.facts` fail-safe +/// skew rule. +#[test] +fn malformed_missing_and_wrong_schema_elide_nothing_without_failing_901() { + let guarded = compile("bad_base", true, None); + let h = module_hash(); + let cases: Vec<(&str, Option)> = vec![ + ("missing", None), + ("garbage", Some("not json at all {{{".to_string())), + ("empty", Some(String::new())), + ( + "wrongschema", + Some(safe_accesses(&h, 65536, PROVEN).replace("safe-accesses/v1", "safe-accesses/v2")), + ), + ( + "nohash", + Some(r#"{"schema":"scry/safe-accesses/v1","memory_min_bytes":65536}"#.to_string()), + ), + ( + "sitegarbage", + Some(safe_accesses(&h, 65536, PROVEN).replace(r#""pc":9"#, r#""pc":"nine""#)), + ), + ]; + for (tag, body) in cases { + let c = compile(tag, true, Some(body.as_deref())); + assert_eq!( + c.text, guarded.text, + "'{tag}' moved bytes; stderr: {}", + c.stderr + ); + assert!( + c.stderr.contains("proven-safe"), + "'{tag}' refused SILENTLY: {}", + c.stderr + ); + // Attested as refused, so sigil sees the refusal too. + let att = c.attestation.expect("attestation is written on refusal"); + assert_eq!(att["accepted"], serde_json::json!(false), "'{tag}'"); + assert!( + att["refusal"].is_string(), + "'{tag}' refused without a reason" + ); + } +} + +/// THE KEY-SPACE CANARY. scry#114's `pc` is the 0-based OPERATOR index; if a +/// producer ever emitted wasm BYTE OFFSETS instead, the entries must fail +/// validation and the build must elide NOTHING loudly — never strip a guard +/// off the wrong access. +#[test] +fn byte_offsets_instead_of_operator_indices_elide_nothing_loudly_901() { + let guarded = compile("keys_base", true, None); + // Plausible byte offsets for this body — all far past the 38-operator count. + let bogus: Vec<(u32, &str, u32)> = vec![ + (41, "i32.load8_u", 1), + (45, "i32.load8_u", 1), + (52, "i32.load16_u", 2), + (61, "i32.load", 4), + (77, "i32.store8", 1), + ]; + let doc = safe_accesses(&module_hash(), 65536, &bogus); + let c = compile("keys", true, Some(Some(&doc))); + + assert_eq!(c.text, guarded.text, "a wrong key space must move NO bytes"); + assert_eq!(c.udf_count(), 16); + assert!(c.stderr.contains("proven-safe: DROP"), "{}", c.stderr); + assert!( + c.stderr.contains("out of range") && c.stderr.contains("OPERATOR index"), + "the drop must name the likely cause: {}", + c.stderr + ); + assert!( + c.stderr.contains("NOTHING was elided"), + "accepted-but-zero-elisions must be loud: {}", + c.stderr + ); + let att = c.attestation.expect("attestation written"); + assert_eq!(att["accepted"], serde_json::json!(true)); + assert_eq!(att["sites_offered"], serde_json::json!(5)); + assert_eq!(att["sites_elided"], serde_json::json!(0)); + assert_eq!(att["sites_not_elided"], serde_json::json!(5)); +} + +/// A width that disagrees with the decoded operator changes which BYTES are +/// covered — drop that entry, keep the sound ones. +#[test] +fn width_skew_drops_only_the_skewed_site_901() { + let guarded = compile("w_base", true, None); + let mut sites = PROVEN.to_vec(); + sites[0] = (9, "i32.load", 4); // pc 9 is really a 1 B load8_u + let doc = safe_accesses(&module_hash(), 65536, &sites); + let c = compile("w", true, Some(Some(&doc))); + assert_eq!( + c.udf_count(), + 8, + "4 sound sites elide, the width-skewed one keeps its guard (4 guards x 2 UDF)" + ); + assert!( + c.probe.len() > guarded.probe.len() - SAVED_PROVEN_5, + "the skewed site's guard must still cost bytes" + ); + assert!( + c.stderr.contains("disagrees with the decoded operator"), + "{}", + c.stderr + ); +} + +/// `--proven-safe` under a bounds mode that emits no inline guard: there is +/// nothing to strip, and that is stated rather than reported as success. +#[test] +fn no_software_bounds_means_nothing_to_elide_and_says_so_901() { + let floor = compile("nb_base", false, None); + let doc = safe_accesses(&module_hash(), 65536, &all_sites()); + let c = compile("nb", false, Some(Some(&doc))); + assert_eq!(c.probe, floor.probe); + assert!( + c.stderr.contains("not `software`") && c.stderr.contains("NOTHING was elided"), + "{}", + c.stderr + ); +} + +/// Without the flag nothing changes at all — the default path is untouched. +#[test] +fn flag_absent_writes_no_attestation_and_no_marks_901() { + let a = compile("noflag_a", true, None); + let b = compile("noflag_b", true, None); + assert_eq!(a.text, b.text); + assert!(a.attestation.is_none(), "no flag ⇒ no sidecar"); + assert!(!a.stderr.contains("proven-safe")); +} + +// ============================================================================= +// Attestation — what sigil reads +// ============================================================================= + +#[test] +fn attestation_records_the_elision_set_and_its_authority_901() { + let doc = safe_accesses(&module_hash(), 65536, PROVEN); + let c = compile("att", true, Some(Some(&doc))); + let att = c.attestation.expect("attestation written"); + + assert_eq!( + att["schema"], + serde_json::json!("synth-proven-safe-elisions-v1") + ); + assert_eq!(att["accepted"], serde_json::json!(true)); + assert_eq!(att["scry_version"], serde_json::json!("3.2.4")); + assert_eq!(att["module_sha256"], serde_json::json!(module_hash())); + assert_eq!( + att["declared_module_sha256"], + serde_json::json!(module_hash()) + ); + assert_eq!(att["memory_min_bytes"], serde_json::json!(65536)); + assert_eq!(att["safety_bounds"], serde_json::json!("software")); + assert_eq!( + att["synth_version"], + serde_json::json!(env!("CARGO_PKG_VERSION")) + ); + assert_eq!(att["sites_offered"], serde_json::json!(5)); + assert_eq!(att["sites_elided"], serde_json::json!(5)); + assert_eq!(att["sites_not_elided"], serde_json::json!(0)); + + let elisions = att["elisions"].as_array().expect("elisions array"); + assert_eq!(elisions.len(), PROVEN.len()); + for (e, (pc, op, w)) in elisions.iter().zip(PROVEN) { + assert_eq!(e["func"], serde_json::json!(0)); + assert_eq!(e["pc"], serde_json::json!(pc)); + assert_eq!(e["op"], serde_json::json!(op)); + assert_eq!(e["width"], serde_json::json!(w)); + // On whose authority — the field that keeps a scry elision + // distinguishable from a #494 ordeal-certificate one. + assert_eq!(e["authority"], serde_json::json!("scry/safe-accesses/v1")); + } + assert!(c.stdout.contains("Proven-safe: wrote"), "{}", c.stdout); +} + +/// SYNTH_FACT_SPEC may REWRITE the op stream, renumbering the index space the +/// verdicts are keyed in. The combination is REFUSED per function, never +/// silently remapped. Needs the solver-carrying build (the pass is a no-op +/// without it), so this runs under `--features verify`. +#[cfg(feature = "verify")] +#[test] +fn fact_spec_specialization_refuses_the_scry_marks_901() { + // A `wsc.facts` value-range premise on the first `local.get $slot` gives + // the fact-spec pass something to specialize, which is all this needs. + fn leb_u32(mut v: u32, out: &mut Vec) { + loop { + let mut b = (v & 0x7f) as u8; + v >>= 7; + if v != 0 { + b |= 0x80; + } + out.push(b); + if v == 0 { + return; + } + } + } + fn leb_s64(mut v: i64, out: &mut Vec) { + loop { + let mut b = (v & 0x7f) as u8; + v >>= 7; + let done = (v == 0 && b & 0x40 == 0) || (v == -1 && b & 0x40 != 0); + if !done { + b |= 0x80; + } + out.push(b); + if done { + return; + } + } + } + let mut wasm = fixture_wasm(); + let mut body = Vec::new(); + leb_s64(0, &mut body); + leb_s64(63, &mut body); + let mut payload = vec![0x01u8]; + leb_u32(1, &mut payload); + payload.push(0x01); + leb_u32(0, &mut payload); + leb_u32(0, &mut payload); + leb_u32(body.len() as u32, &mut payload); + payload.extend_from_slice(&body); + let name = b"wsc.facts"; + let mut content = Vec::new(); + leb_u32(name.len() as u32, &mut content); + content.extend_from_slice(name); + content.extend_from_slice(&payload); + wasm.push(0x00); + leb_u32(content.len() as u32, &mut wasm); + wasm.extend_from_slice(&content); + + let d = dir(); + let input = d.join("factspec.wasm"); + let elf = d.join("factspec.elf"); + let json = d.join("factspec.safe-accesses.json"); + std::fs::write(&input, &wasm).expect("write wasm"); + std::fs::write(&json, safe_accesses(&hex_sha256(&wasm), 65536, PROVEN)).expect("write"); + + let out = Command::new(synth()) + .args([ + "compile", + input.to_str().unwrap(), + "-o", + elf.to_str().unwrap(), + "-b", + "arm", + "--target", + "cortex-m4", + "--all-exports", + "--safety-bounds", + "software", + "--proven-safe", + json.to_str().unwrap(), + ]) + .env("SYNTH_FACT_SPEC", "1") + .env_remove("SYNTH_FACT_SPEC_FORCE_ADMIT") + .output() + .expect("run synth"); + assert!(out.status.success()); + let stderr = String::from_utf8_lossy(&out.stderr); + // Either the pass specialized this function (⇒ our marks are refused) or + // it declined outright (⇒ the stream is unchanged and the marks apply). + // Only the first case is a skew risk, and only it must produce a refusal. + if stderr.contains("specialized") { + assert!( + stderr.contains("REFUSED: SYNTH_FACT_SPEC specialized this function"), + "a renumbered op stream must refuse the scry marks: {stderr}" + ); + } +} From 36ed7d75fb8b4df9b9a2fe4ec2f55bcd8551f40a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:27:04 +0200 Subject: [PATCH 6/8] test(#901): execution differential + CI wiring, in the same commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit scripts/repro/proven_safe_bounds_901_differential.py — unicorn vs wasmtime, CI-wired in the new proven-safe-oracle job (set -euo pipefail, RESULT: PASS grep, and a non-zero CHECKS=n/n grep so a differential that checked nothing cannot pass). 207/207 checks green. FOUR LEGS: 1. BYTE EVIDENCE + non-vacuity — the run fails unless the compile reported exactly 5 scry-authorized elisions. 2. IN-BOUNDS SWEEP — 180 rows (10 slots x 6 raw addresses x 3 memory seeds): ELIDED == GUARDED == wasmtime on the return value AND the full 64 KiB final memory image (the fixture stores through both address expressions). 3. ABSENCE IS NOT SAFETY, EXECUTABLE — 5 out-of-bounds accesses at the three NOT-PROVEN sites still TRAP in the ELIDED build, exactly like wasmtime. Their guards survived the elision of the five that were proven. 4. FAIL CLOSED, AND LOAD-BEARING — the red leg. It applies the fixture's verdicts to a MUTATED module (i32.const 63 -> i32.const -1, so slot & -1 == slot and the five formerly-proven accesses become UNBOUNDED) whose every (func, pc) key STILL VALIDATES: same operator count, kinds and widths. module_sha256 is the only thing that differs, so it is the only thing standing between stale verdicts and a silent out-of-bounds access. RED-FIRST, and this one is the important one: deleting the module_sha256 comparison makes leg 4 accept the stale verdicts and probe(4096, 0), probe(65536, 0), probe(1048576, 0) return UC_ERR_READ_UNMAPPED — a REAL out-of-bounds read where wasmtime traps. 199/207, RESULT: FAIL. Reverted. This is a permanent regression gate, not a one-time demo. MEASURED, with the honest denominators: probe 232 B -> 152 B: 80 B saved = 58% of the 138 B guard tax, 34.5% of the function. 5 of 8 sites proven. Executed instructions on one in-bounds call: 70 -> 45, i.e. 25 fewer (35.7%); the full 8-site guard cost is 40 instructions (70 -> 30 floor). The per-site win is the same magnitude #494 publishes because it is the same guard strip — what is new is the authority (a whole-module external AI, hash-bound and attested) and the fail-closed binding, not the byte. oracle_wiring_check: 158 scripts, 151 wired, 0 undeclared. claim_check: 37/37. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/workflows/ci.yml | 62 +++ .../proven_safe_bounds_901_differential.py | 390 ++++++++++++++++++ 2 files changed, 452 insertions(+) create mode 100644 scripts/repro/proven_safe_bounds_901_differential.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b6069e16..17fd25dc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1207,6 +1207,68 @@ jobs: SYNTH: ./target/debug/synth run: python scripts/repro/fact_spec_rem_494_differential.py + proven-safe-oracle: + name: proven-safe bounds-elision oracle (VCR-MEM-004, #901) + # VCR-MEM-004 (#901): `--proven-safe` consumes scry's safe-accesses.json + # (schema scry/safe-accesses/v1, scry#114) and elides the + # `--safety-bounds software` inline guard at the access sites scry PROVED + # in-bounds. This job gates the three safety properties, not the speedup: + # (1) FAIL CLOSED on module_sha256 / memory_min_bytes / malformed input; + # (2) ABSENCE MEANS "NOT PROVEN" — a partial verdict list leaves exactly + # the unproven guards standing, and their out-of-bounds accesses + # still TRAP under execution; + # (3) a genuine elision that is result-identical to wasmtime. + # The differential's fail-closed leg is a permanent regression gate: it + # applies one module's verdicts to a MUTATED module whose keys all still + # validate, so deleting the hash comparison turns it RED with a real + # UC_ERR_READ_UNMAPPED (verified by mutation when #901 landed). + # Isolated job: emulation deps pip-installed here ONLY. + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + - uses: dtolnay/rust-toolchain@stable + - name: Cache Cargo dependencies + uses: actions/cache@v6 + with: + path: | + ~/.cargo/registry + ~/.cargo/git + target/ + key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} + restore-keys: | + ${{ runner.os }}-cargo- + # Unit level: the fail-closed ingestion gates (synth-core) and the + # dep-free ProvenSafeBoundsChecker trait semantics (synth-memory). + - name: Run ingestion + BoundsChecker unit gates + run: cargo test -p synth-core --lib proven_safe && cargo test -p synth-memory --lib + # Byte evidence: the partial-list partition, the refusals, the key-space + # canary, and the attestation contents. + - name: Run --proven-safe byte gates (#901) + run: cargo test -p synth-cli --test proven_safe_bounds_901 + # The fact-spec combination refusal needs the solver-carrying build (the + # pass is inert without it), so it is a separate feature-gated run. + - name: Run the fact-spec-combination refusal gate (verify feature) + run: cargo test -p synth-cli --features verify --test proven_safe_bounds_901 + - name: Build synth + run: cargo build -p synth-cli + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - name: Install emulation deps + run: pip install wasmtime unicorn pyelftools + - name: Run --proven-safe execution differential (#901) + env: + SYNTH: ./target/debug/synth + run: | + set -euo pipefail + python scripts/repro/proven_safe_bounds_901_differential.py \ + | tee /tmp/proven_safe_901.log + grep -q '^RESULT: PASS' /tmp/proven_safe_901.log + # Non-vacuity: a differential that checked nothing must not pass. + grep -qE '^#901 CHECKS=[1-9][0-9]*/[1-9][0-9]*$' /tmp/proven_safe_901.log + grep -q 'absence-is-not-safety: [1-9]' /tmp/proven_safe_901.log + grep -q 'fail-closed: stale verdicts REFUSED' /tmp/proven_safe_901.log + rv32-shift-fold-oracle: name: rv32 immediate-shift-fold execution oracle # VCR-ORACLE-001 (#242, #472): EXECUTE the RV32 immediate-shift-fold lever diff --git a/scripts/repro/proven_safe_bounds_901_differential.py b/scripts/repro/proven_safe_bounds_901_differential.py new file mode 100644 index 00000000..bae3581b --- /dev/null +++ b/scripts/repro/proven_safe_bounds_901_differential.py @@ -0,0 +1,390 @@ +#!/usr/bin/env python3 +# ci-status: wired +"""VCR-MEM-004 / #901 — execution differential for `--proven-safe`. + +Compiles `scripts/repro/proven_safe_bounds_901.wat` (one function, EIGHT +`--safety-bounds software` guarded accesses: five off a provably bounded base +`(slot & 63) * 16 + 256`, three off an unconstrained i32 param `$raw`) four +ways and executes them under unicorn against wasmtime: + + GUARDED --safety-bounds software, no verdicts (the baseline) + ELIDED the same + scry verdicts covering only the FIVE proven sites + FLOOR no --safety-bounds at all (the zero-tax reference) + STALE the ELIDED verdicts applied to a MUTATED module (below) + +Legs +---- +1. BYTE EVIDENCE — the measured `probe` shrink and the surviving guard count, + plus non-vacuity: the run FAILS unless the compile reported exactly five + certificate-free, scry-authorized elisions on stderr. + +2. IN-BOUNDS SWEEP — for every in-bounds (slot, raw) pair over several memory + seeds, ELIDED == GUARDED == wasmtime on BOTH the returned value and the + FULL final 64 KiB memory image (the fixture stores through `$base` and + `$raw`). An elision that changed a result would show up here. + +3. ABSENCE IS NOT SAFETY (executable) — `$raw` driven out of the one-page + memory must TRAP in wasmtime AND in the ELIDED build. Those three sites + were never proven, so their guards MUST have survived the elision of the + five that were. This is the property that makes a partial verdict list + safe to consume at all. + +4. FAIL CLOSED, and it is LOAD-BEARING — the red leg. The mutated module is + the fixture with `i32.const 63` replaced by `i32.const -1`, so + `slot & -1 == slot` and the five formerly-proven accesses become + UNBOUNDED. Every (func, pc) key still validates — same operator count, + same operator kinds, same widths — so the ONLY thing standing between the + stale verdicts and a silent out-of-bounds access is `module_sha256`. + Asserted: the compile REFUSES, its `.text` is byte-identical to the + mutated module's own guarded baseline, and a large `slot` still TRAPS + exactly like wasmtime. + + This leg is a permanent regression gate, not a one-time demo: delete or + invert the hash comparison in `synth_core::proven_safe::ingest` and it + goes RED with a silent OOB (verified by mutation while developing #901). + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth python scripts/repro/proven_safe_bounds_901_differential.py +Exits nonzero on any mismatch; prints `#901 CHECKS=/` on success. +""" + +import hashlib +import json +import os +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import ( + UC_ARCH_ARM, + UC_ERR_INSN_INVALID, + UC_HOOK_CODE, + UC_MODE_THUMB, + Uc, + UcError, +) +from unicorn.arm_const import ( + UC_ARM_REG_LR, + UC_ARM_REG_R0, + UC_ARM_REG_R1, + UC_ARM_REG_R10, + UC_ARM_REG_R11, + UC_ARM_REG_SP, +) + +WAT = Path(__file__).with_name("proven_safe_bounds_901.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") +TMP = Path("/tmp/proven_safe_bounds_901_diff") +TRAP = "" + +MEM_BYTES = 0x10000 # 1 page, matching `(memory 1)` +CODE, LIN, STK, RET = 0x200000, 0x400000, 0x90000, 0x300000 + +# The fixture's PROVEN sites (operator index, mnemonic, access width). +PROVEN = [ + (9, "i32.load8_u", 1), + (11, "i32.load8_u", 1), + (14, "i32.load16_u", 2), + (17, "i32.load", 4), + (22, "i32.store8", 1), +] + +CHECKS = [0, 0] # [passed, total] + + +def check(ok, what): + CHECKS[1] += 1 + if ok: + CHECKS[0] += 1 + else: + print(f"FAIL: {what}") + return ok + + +def seed(k): + return bytes((i * 37 + 13 * k + 5) & 0xFF for i in range(MEM_BYTES)) + + +# ---------------------------------------------------------------- verdicts -- + + +def verdicts(module_bytes, sites, memory_min_bytes=65536): + return json.dumps( + { + "schema": "scry/safe-accesses/v1", + "scry_version": "3.2.4", + "module_sha256": hashlib.sha256(module_bytes).hexdigest(), + "memory_min_bytes": memory_min_bytes, + "premises": {"bounded_memory": True}, + "counts": {"access_sites": 8, "proven_safe": len(sites)}, + "proven_safe": [ + {"func": 0, "pc": pc, "op": op, "width": w} for pc, op, w in sites + ], + }, + indent=2, + ) + + +# ------------------------------------------------------------ compile/load -- + + +def compile_elf(wasm_path, out, software_bounds=True, proven_safe=None): + # A FRESH env so an ambient SYNTH_* lever cannot perturb the measurement + # (the #494 fact_spec_bounds lesson). + env = {"PATH": "/usr/bin:/bin"} + cmd = [ + SYNTH, "compile", str(wasm_path), "-o", str(out), "-b", "arm", + "--target", "cortex-m4", "--all-exports", + ] + if software_bounds: + cmd += ["--safety-bounds", "software"] + if proven_safe is not None: + cmd += ["--proven-safe", str(proven_safe)] + r = subprocess.run(cmd, capture_output=True, text=True, env=env) + if r.returncode != 0: + sys.exit(f"compile failed ({out}): {r.stderr}") + return r.stderr + + +def load(elf): + with open(elf, "rb") as fh: + f = ELFFile(fh) + text = f.get_section_by_name(".text") + data, base = text.data(), text["sh_addr"] + syms = {} + for s in f.iter_sections(): + if s.header.sh_type == "SHT_SYMTAB": + for sym in s.iter_symbols(): + if sym.name: + syms[sym.name] = sym["st_value"] & ~1 + return data, base, syms + + +def func_bytes(elf, name): + data, base, syms = load(elf) + addrs = sorted(a for a in syms.values() if base <= a < base + len(data)) + start = syms[name] + nxt = next((a for a in addrs if a > start), base + len(data)) + return data[start - base : nxt - base] + + +# ------------------------------------------------------------- executors ---- + + +def run_probe(elf, slot, raw, mem_seed, count_insns=False): + """probe(slot, raw) under unicorn. Returns (ret, memory) or TRAP or ERR. + + The direct selector's ABI: R11 = linear-memory base, R10 = memory size in + bytes (what the software guard compares against). Linear memory is mapped + as EXACTLY one page, so an access a bad elision lets through faults as ERR + rather than silently matching. + """ + code, base, syms = load(elf) + mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB) + mu.mem_map(CODE, 0x10000) + mu.mem_map(LIN, MEM_BYTES) + mu.mem_map(STK - 0x8000, 0x10000) + mu.mem_map(RET, 0x1000) + mu.mem_write(CODE, code) + mu.mem_write(LIN, mem_seed) + mu.reg_write(UC_ARM_REG_SP, STK) + mu.reg_write(UC_ARM_REG_R11, LIN) + mu.reg_write(UC_ARM_REG_R10, MEM_BYTES) + mu.reg_write(UC_ARM_REG_R0, slot & 0xFFFFFFFF) + mu.reg_write(UC_ARM_REG_R1, raw & 0xFFFFFFFF) + mu.reg_write(UC_ARM_REG_LR, RET | 1) + n = [0] + if count_insns: + mu.hook_add(UC_HOOK_CODE, lambda uc, a, s, u: n.__setitem__(0, n[0] + 1)) + try: + mu.emu_start((CODE + syms["probe"] - base) | 1, RET, count=200_000) + except UcError as e: + # The inline guard is a UDF -> UC_ERR_INSN_INVALID: that IS the wasm + # trap. Any other fault means an access escaped WITHOUT a guard. + if e.errno == UC_ERR_INSN_INVALID: + return (TRAP, n[0]) if count_insns else TRAP + return (f"ERR:{e}", n[0]) if count_insns else f"ERR:{e}" + out = (mu.reg_read(UC_ARM_REG_R0) & 0xFFFFFFFF, bytes(mu.mem_read(LIN, MEM_BYTES))) + return (out, n[0]) if count_insns else out + + +def wasmtime_probe(module_bytes, slot, raw, mem_seed): + eng = wasmtime.Engine() + st = wasmtime.Store(eng) + inst = wasmtime.Instance(st, wasmtime.Module(eng, module_bytes), []) + mem = inst.exports(st)["mem"] + mem.write(st, mem_seed, 0) + try: + ret = inst.exports(st)["probe"](st, slot, raw) & 0xFFFFFFFF + except Exception: + return TRAP + return ret, bytes(mem.read(st, 0, MEM_BYTES)) + + +def brief(v): + if isinstance(v, str): + return v + return f"ret={v[0]}" + + +# ------------------------------------------------------------------- main --- + + +def main(): + if not os.path.exists(SYNTH): + sys.exit(f"{SYNTH} not found — build synth first") + TMP.mkdir(parents=True, exist_ok=True) + + wat = WAT.read_text() + wasm = bytes(wasmtime.wat2wasm(wat)) + w_path = TMP / "probe.wasm" + w_path.write_bytes(wasm) + + v_path = TMP / "safe-accesses.json" + v_path.write_text(verdicts(wasm, PROVEN)) + + guarded = TMP / "guarded.elf" + elided = TMP / "elided.elf" + floor = TMP / "floor.elf" + compile_elf(w_path, guarded) + err = compile_elf(w_path, elided, proven_safe=v_path) + compile_elf(w_path, floor, software_bounds=False) + + # ---- LEG 1: byte evidence + non-vacuity ----------------------------- + g, e, f = (func_bytes(p, "probe") for p in (guarded, elided, floor)) + + def udf(b): + return sum(1 for i in range(0, len(b) - 1, 2) if b[i : i + 2] == b"\x00\xde") + + print(f"probe: guarded={len(g)} B ({udf(g)} UDF#0) " + f"elided={len(e)} B ({udf(e)} UDF#0) floor={len(f)} B ({udf(f)} UDF#0)") + print(f" saved {len(g) - len(e)} B of the {len(g) - len(f)} B guard tax " + f"({100 * (len(g) - len(e)) / (len(g) - len(f)):.0f}% of it), " + f"{100 * (len(g) - len(e)) / len(g):.1f}% of the function") + check("proven-safe: ACCEPTED" in err, "verdicts must be ACCEPTED") + check( + "5 bounds guard(s) elided" in err, + f"exactly 5 elisions must be reported (non-vacuity); stderr: {err}", + ) + check(len(e) < len(g), "the elided build must be smaller") + check(udf(e) == 6, f"exactly 3 unproven guards (6 UDF#0) must survive, got {udf(e)}") + check(udf(g) == 16, "the baseline must carry all 8 guards") + + # ---- LEG 2: in-bounds sweep ------------------------------------------ + # `raw` stays where a 4 B load at +0, a 1 B load at +3 and a 4 B store at + # +8 all fit inside the page. + raws = [0, 4, 64, 1024, MEM_BYTES - 16, MEM_BYTES - 12] + slots = [0, 1, 7, 31, 63, 64, 65, 127, 4096, 0xFFFFFFF0] + rows = 0 + for k in range(3): + m = seed(k) + for slot in slots: + for raw in raws: + want = wasmtime_probe(wasm, slot, raw, m) + got_e = run_probe(elided, slot, raw, m) + got_g = run_probe(guarded, slot, raw, m) + rows += 1 + if not check( + got_e == want and got_g == want, + f"in-bounds probe(slot={slot}, raw={raw}, seed={k}): " + f"wasmtime={brief(want)} elided={brief(got_e)} " + f"guarded={brief(got_g)}", + ): + return 1 + print(f"in-bounds sweep: {rows} rows — elided == guarded == wasmtime " + f"(return value AND full 64 KiB memory image)") + + # ---- LEG 3: absence is not safety, executable ------------------------- + # `$raw` was never proven, so its guards MUST have survived. + oob_raws = [MEM_BYTES, MEM_BYTES - 4, MEM_BYTES + 4096, 0xFFFFFFF0, 0x7FFFFFFF] + m = seed(9) + for raw in oob_raws: + want = wasmtime_probe(wasm, 3, raw, m) + got = run_probe(elided, 3, raw, m) + check( + want == TRAP, + f"fixture setup: probe(3, {raw}) must trap in wasmtime, got {brief(want)}", + ) + check( + got == TRAP, + f"NOT-PROVEN out-of-bounds probe(3, raw={raw}) must STILL TRAP in the " + f"ELIDED build (absence means not-proven, never unsafe) — got {brief(got)}", + ) + print(f"absence-is-not-safety: {len(oob_raws)} out-of-bounds cases still TRAP " + f"in the elided build, exactly like wasmtime") + + # ---- LEG 4: fail closed, and load-bearing ----------------------------- + # `slot & 63` -> `slot & -1`: the five formerly-proven accesses become + # UNBOUNDED, but every (func, pc) key still validates (same operator + # count, kinds and widths). Only module_sha256 differs. + mutated_wat = wat.replace("i32.const 63 ;; op 1", "i32.const -1 ;; op 1") + assert mutated_wat != wat, "the mutation anchor drifted — fix the differential" + mutated = bytes(wasmtime.wat2wasm(mutated_wat)) + mw_path = TMP / "mutated.wasm" + mw_path.write_bytes(mutated) + check( + hashlib.sha256(mutated).hexdigest() != hashlib.sha256(wasm).hexdigest(), + "the mutated module must hash differently", + ) + + stale = TMP / "stale.elf" + mutated_guarded = TMP / "mutated_guarded.elf" + stale_err = compile_elf(mw_path, stale, proven_safe=v_path) + compile_elf(mw_path, mutated_guarded) + + check( + "REFUSED — module_sha256 mismatch" in stale_err, + f"stale verdicts must be REFUSED; stderr: {stale_err}", + ) + check( + func_bytes(stale, "probe") == func_bytes(mutated_guarded, "probe"), + "a refused verdict file must not move a single byte", + ) + # The attestation must record the refusal, so sigil can tell "nothing to + # elide" from "file rejected". + att = json.loads((TMP / "stale.proven-safe-elisions.json").read_text()) + check(att["accepted"] is False, "the attestation must record the refusal") + check(att["sites_elided"] == 0, "a refusal must attest ZERO elisions") + check( + isinstance(att.get("refusal"), str) and "module_sha256" in att["refusal"], + "the attestation must name the refusal reason", + ) + + # And the behaviour the gate protects: a large `slot` now escapes the page. + # Chosen so `(slot << 4) + 256` really is past 65536 WITHOUT wrapping — + # e.g. 0x7FFFFFF0 << 4 wraps back to 0 and is in bounds, so it is not a + # witness. + for slot in [4096, 0x10000, 0x100000]: + want = wasmtime_probe(mutated, slot, 0, m) + got = run_probe(stale, slot, 0, m) + check( + want == TRAP, + f"mutated fixture: probe({slot}, 0) must trap in wasmtime, got {brief(want)}", + ) + check( + got == TRAP, + f"STALE-VERDICT build must still TRAP at probe({slot}, 0) — if this is " + f"not a trap, a stale analysis elided a live bounds check (the " + f"memory-safety hole module_sha256 exists to prevent). Got {brief(got)}", + ) + print("fail-closed: stale verdicts REFUSED, bytes unmoved, and the " + "now-unbounded accesses still trap") + + # ---- instruction-count evidence (the cycles axis) --------------------- + _, n_g = run_probe(guarded, 3, 16, m, count_insns=True) + _, n_e = run_probe(elided, 3, 16, m, count_insns=True) + _, n_f = run_probe(floor, 3, 16, m, count_insns=True) + print(f"executed instructions on one in-bounds call: guarded={n_g} " + f"elided={n_e} floor={n_f} — {n_g - n_e} fewer ({100 * (n_g - n_e) / n_g:.1f}%), " + f"{n_g - n_f} is the whole 8-site guard cost") + + ok = CHECKS[0] == CHECKS[1] + print(f"#901 CHECKS={CHECKS[0]}/{CHECKS[1]}") + print("RESULT: PASS" if ok else "RESULT: FAIL") + return 0 if ok else 1 + + +if __name__ == "__main__": + sys.exit(main()) From 54faae14581f828cee1a4c5f54bb3699f10459fe Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:32:00 +0200 Subject: [PATCH 7/8] docs(#901): CHANGELOG + feature-matrix template + claims.yaml pin; VCR-MEM-004 implemented MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - CHANGELOG [Unreleased]: the --proven-safe entry, led by the refusal logic rather than the speedup, with the measured numbers and their denominators. - scripts/templates/feature_matrix.md.tmpl (a SOURCE file): the validator row and the CLI flag list. docs/status/FEATURE_MATRIX.md was REGENERATED with scripts/claim_check.py --emit-status, never hand-edited — the generated-file freshness gate is part of the required Claim Check, so leaving it stale would redden this PR. The coordinator's #805 regen at assembly still owns the final regeneration; this is only what keeps the lane green. - claims.yaml: SYNTH-PROVEN-SAFE-901-MEASURED pins the doc's measured cost (138 B / 40 insn guard tax, 80 B recovered) to the CONSTANTS the byte gate asserts against real compiled bytes, plus the presence of the fail-closed refusal in the ingestion. Non-vacuity verified: changing SAVED_PROVEN_5 from 80 to 96 turns it FAIL (37/38). It pins a CAPABILITY — a measured tax and a measured recovery on a named fixture — never an issue number, so a closed issue can never green-confirm a false residual (the v0.53 lesson). - synth-memory bounds.rs: SoftwareBoundsChecker's '~25-40% overhead' becomes a MEASURED table. The real tax on this access-dense kernel is +147 % bytes / +133 % instructions — worse than the old guess, stated as such, with the small denominator named ('one fixture on one target, not a headline'). - VCR-MEM-004 status proposed -> implemented. claim_check 38/38; oracle_wiring_check 158 scripts / 151 wired / 0 undeclared. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 71 ++++++++++++++++++++++++ artifacts/verified-codegen-roadmap.yaml | 2 +- claims.yaml | 41 ++++++++++++++ crates/synth-memory/src/bounds.rs | 23 +++++++- docs/status/FEATURE_MATRIX.md | 3 +- scripts/templates/feature_matrix.md.tmpl | 3 +- 6 files changed, 139 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c77dba86..bdfc1598 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,77 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] +### Added + +- **`--proven-safe`: bounds-check elision on scry's proof, fail-closed and + attested (VCR-MEM-004, #901).** `synth compile --proven-safe + safe-accesses.json` consumes scry's `scry/safe-accesses/v1` verdict list + (producer: pulseengine/scry#114) and drops the `--safety-bounds software` + inline guard at exactly the access sites scry's sound abstract + interpretation proved in-bounds against the memory's **guaranteed minimum** + size — a floor wasm memory can only grow away from, so the verdict survives + `memory.grow`. New `synth_memory::ProvenSafeBoundsChecker` (the fifth + `BoundsChecker` strategy, and the first proof-informed one) and + `synth_core::proven_safe` (ingestion + attestation). + + **The deliverable is the refusal logic, not the speedup.** Every question the + ingestion can ask is answered fail-closed, and fail-closed always means the + same thing — elide NOTHING, warn, exit 0: + + - a `module_sha256` that does not match **the exact bytes handed to the + decoder** (after `.wat` parsing, after loom, after the #418 arena-bind + rewrite). Binding the hash there is deliberate: a pre-compile rewrite that + shifts function/operator indices also breaks the hash, so index skew and + byte skew are ONE gate. Eliding on a stale analysis is a memory-safety + hole, not a stale optimization; + - a `memory_min_bytes` that disagrees with this module's declared floor (a + matching hash implies they are equal, so a disagreement means the producer + is broken — and a broken prover is not trusted); + - a malformed, missing, or wrong-schema file — the `wsc.facts` fail-safe skew + rule applied to a JSON carrier. No input can turn a good compile into a + failed one; + - a `(func, pc)` key that does not validate against the DECODED operator + (must exist, must be a linear-memory access, must have the declared access + width). scry#114's `pc` is the 0-based **wasmparser operator index**; if a + producer ever emitted wasm byte offsets instead, nearly every entry fails + this check and the build elides nothing **loudly** rather than stripping + the guard off the wrong access; + - a function that `SYNTH_FACT_SPEC` specialized, which renumbers the index + space the verdicts are keyed in — refused per function, never silently + remapped. + + **Absence from the list means "not proven", never "unsafe":** an unlisted + site keeps its guard, so a partial verdict list yields a partially-guarded + binary. "Flag given, file accepted, nothing elided" is diagnosed by name + rather than reported as success. + + **Attestation (sigil):** every `--proven-safe` compile writes + `.proven-safe-elisions.json` (`synth-proven-safe-elisions-v1`) with + the elision set, each site's authority, the scry version, both module hashes + and both memory floors — **emitted on refusal too**, so sigil can tell + "nothing to elide" from "file rejected". + + **Measured** on `scripts/repro/proven_safe_bounds_901.wat` (Cortex-M4, 8 + guarded accesses, 5 proven): `probe` **232 → 152 B** (80 B, 58 % of the + 138 B guard tax, 34.5 % of the function) and **70 → 45 executed + instructions** (36 %). Proving all 8 lands byte-identical to the + `--safety-bounds`-off floor. The per-site win is the same magnitude #494 + publishes because it is the same guard strip — what is new is the authority + and the fail-closed binding, not the byte. This also converts + `SoftwareBoundsChecker`'s long-standing "~25-40 % overhead" doc comment from + an assertion into a measurement (the real tax on this access-dense kernel is + +147 % bytes / +133 % instructions), pinned in `claims.yaml`. + + Gated by `crates/synth-cli/tests/proven_safe_bounds_901.rs` (11 byte gates) + and `scripts/repro/proven_safe_bounds_901_differential.py` (207 checks, + unicorn vs wasmtime, CI-wired in the new `proven-safe-oracle` job): an + in-bounds sweep where elided ≡ guarded ≡ wasmtime on return value AND the + full 64 KiB memory image, out-of-bounds accesses at NOT-PROVEN sites that + still trap, and a fail-closed leg that applies one module's verdicts to a + mutated module whose keys all still validate — deleting the hash comparison + turns it RED with a real `UC_ERR_READ_UNMAPPED`. Opt-in; frozen anchors + 10/10 (the mark vector defaults empty). + ## [0.54.0] - 2026-08-05 **"Close what we measured."** v0.53 built the instruments; this release acts on diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index f3589775..2eb15e41 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -3194,7 +3194,7 @@ artifacts: is impossible without changing the published surface; the two halves are joined by this documented contract, not a compile-time link. Named residual, not hidden. - status: proposed + status: implemented tags: [codegen, memory, bounds-elision, scry, proof-carrying, attestation, sigil, track-c, synth-901, scry-114] links: - type: derives-from diff --git a/claims.yaml b/claims.yaml index 094a94ca..40ca4f0a 100644 --- a/claims.yaml +++ b/claims.yaml @@ -965,6 +965,47 @@ claims: - kind: verbatim text: 'grep -q "^#846 CHECKS=75/75" gpio846.out' + # --------------------------------------------------------------------------- + # VCR-MEM-004 / #901 — the SoftwareBoundsChecker cost claim. + # + # `synth-memory/src/bounds.rs` carried "~25-40% overhead" as a bare assertion + # for its whole life, and #901's whole premise is that verification pays for + # itself against exactly that number. So the doc now states a MEASURED cost, + # and this entry pins the doc's numbers to the constants the byte gate + # asserts against real compiled bytes. Change the lowering and the gate's + # constants move; move them without updating the doc and this reddens. + # + # What is pinned is the CAPABILITY (a measured guard tax and a measured + # recovery on a named fixture), never an issue number — a closed issue would + # let the ledger green-confirm a false residual (the v0.53 lesson). + # --------------------------------------------------------------------------- + - id: SYNTH-PROVEN-SAFE-901-MEASURED + doc: crates/synth-memory/src/bounds.rs + text: "138 B (+147 %) and 40 instructions" + evidence: + - kind: verbatim + text: "recovers 80 B (58 % of the tax)" + - kind: file-exists + path: crates/synth-cli/tests/proven_safe_bounds_901.rs + - kind: file-exists + path: scripts/repro/proven_safe_bounds_901_differential.py + - kind: file-exists + path: scripts/repro/proven_safe_bounds_901.wat + # The doc's 138 B tax and 80 B recovery ARE the gate's constants. + - kind: count-eq + pattern: "const TAX_ALL_8: usize = 138;" + glob: "crates/synth-cli/tests/proven_safe_bounds_901.rs" + expect: 1 + - kind: count-eq + pattern: "const SAVED_PROVEN_5: usize = 80;" + glob: "crates/synth-cli/tests/proven_safe_bounds_901.rs" + expect: 1 + # Fail-closed is the deliverable: the refusal must stay in the ingestion. + - kind: count-eq + pattern: "REFUSED — module_sha256 mismatch" + glob: "crates/synth-core/src/proven_safe.rs" + expect: 1 + # --------------------------------------------------------------------------- # #890 — the ORACLE-WIRING surface, generalized. SYNTH-GPIO-846-ORACLE-CI-WIRED # above pins ONE script's CI wiring by hand; that is the instance-at-a-time diff --git a/crates/synth-memory/src/bounds.rs b/crates/synth-memory/src/bounds.rs index 781d01e6..753a3c6b 100644 --- a/crates/synth-memory/src/bounds.rs +++ b/crates/synth-memory/src/bounds.rs @@ -30,10 +30,31 @@ pub enum BoundsCheckOverhead { High, } -/// Software bounds checking (portable, ~25-40% overhead) +/// Software bounds checking (portable). /// /// Performs an explicit comparison before each memory access. /// This is the safest portable option. +/// +/// # Cost — MEASURED, not asserted (VCR-MEM-004 / #901) +/// +/// This doc used to say "~25-40% overhead" with nothing behind it. On +/// `scripts/repro/proven_safe_bounds_901.wat` (Cortex-M4, `--safety-bounds +/// software`, 8 guarded i32 accesses), gated by +/// `crates/synth-cli/tests/proven_safe_bounds_901.rs` and +/// `scripts/repro/proven_safe_bounds_901_differential.py`: +/// +/// | build | `probe` bytes | executed insns | +/// |------------------------------|---------------|----------------| +/// | no bounds checking (floor) | 94 B | 30 | +/// | software bounds (all 8 sites)| 232 B | 70 | +/// | 5 of 8 sites proven in-bounds| 152 B | 45 | +/// +/// So the guard tax on this fixture is **138 B (+147 %) and 40 instructions +/// (+133 %)** — well above the old "~25-40%" guess, because that guess was +/// about a whole workload while this is one access-dense kernel. Proving 5 of +/// the 8 sites via [`ProvenSafeBoundsChecker`] recovers 80 B (58 % of the tax) +/// and 25 instructions (36 % of the guarded total). One fixture on one target +/// — a real number with a small denominator, not a headline. #[derive(Debug, Clone, Copy, Default)] pub struct SoftwareBoundsChecker; diff --git a/docs/status/FEATURE_MATRIX.md b/docs/status/FEATURE_MATRIX.md index dd21747c..19c3531f 100644 --- a/docs/status/FEATURE_MATRIX.md +++ b/docs/status/FEATURE_MATRIX.md @@ -81,6 +81,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Trap-preservation VC (VCR-VER-002) | Y (live classes) | Dropped WASM traps: i32 + i64 div/rem, memory OOB (all widths), `call_indirect`, `unreachable`, float→int trunc | | Static-data addressing VC (VCR-VER-003) | Y | Byte-equality of served vs runtime-image static data (the #757 wrong-segment class); spanned accesses, self-contained ROM image; RV32 ships active data segments as `.wasm_data` records — the emitted blob is read back and any served/runtime disagreement hard-errors the compile (#798, v0.48) | | Proof-carrying specialization (`SYNTH_FACT_SPEC`) | Y (opt-in) | ordeal-certified elisions from loom `wsc.facts` invariants (#494) | +| Proven-safe bounds elision (`--proven-safe`, VCR-MEM-004) | Y (opt-in) | Consumes scry's `safe-accesses.json` (`scry/safe-accesses/v1`, scry#114) and elides the `--safety-bounds software` inline guard at the access sites scry PROVED in-bounds against the memory's guaranteed minimum. FAIL CLOSED on a `module_sha256` mismatch (verified against the exact bytes handed to the decoder, so a pre-compile rewrite that shifts operator indices refuses too), on a `memory_min_bytes` disagreement, and on a malformed/missing/wrong-schema file — each elides NOTHING, warns, and exits 0. Absence from the list means "not proven", NEVER "unsafe": an unlisted site keeps its guard. Each `(func, pc)` key is re-validated against the decoded operator (existence + access kind + width), so a wrong key space elides nothing LOUDLY instead of stripping the wrong guard. Writes a `synth-proven-safe-elisions-v1` attestation for sigil — on refusal too. MEASURED on `proven_safe_bounds_901.wat` (Cortex-M4): 5 of 8 sites proven ⇒ 232 → 152 B (80 B, 58 % of the guard tax) and 70 → 45 executed instructions (#901) | ### WCET (Track D, #778) @@ -99,7 +100,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Command | Notes | |---------|-------| -| `synth compile -o ` | WAT/WASM → ELF; `--cortex-m`, `--target `, `-b `, `--all-exports`, `--relocatable`, `--verify`, `--emit-wcet`, `--wcet-hints` | +| `synth compile -o ` | WAT/WASM → ELF; `--cortex-m`, `--target `, `-b `, `--all-exports`, `--relocatable`, `--verify`, `--emit-wcet`, `--wcet-hints`, `--proven-safe` | | `synth verify ` | Standalone translation validation (feature-gated build) | | `synth disasm ` | Disassemble generated ELF | | `synth parse ` | Parse and analyze WASM components | diff --git a/scripts/templates/feature_matrix.md.tmpl b/scripts/templates/feature_matrix.md.tmpl index a7d99938..5c9192be 100644 --- a/scripts/templates/feature_matrix.md.tmpl +++ b/scripts/templates/feature_matrix.md.tmpl @@ -81,6 +81,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Trap-preservation VC (VCR-VER-002) | Y (live classes) | Dropped WASM traps: i32 + i64 div/rem, memory OOB (all widths), `call_indirect`, `unreachable`, float→int trunc | | Static-data addressing VC (VCR-VER-003) | Y | Byte-equality of served vs runtime-image static data (the #757 wrong-segment class); spanned accesses, self-contained ROM image; RV32 ships active data segments as `.wasm_data` records — the emitted blob is read back and any served/runtime disagreement hard-errors the compile (#798, v0.48) | | Proof-carrying specialization (`SYNTH_FACT_SPEC`) | Y (opt-in) | ordeal-certified elisions from loom `wsc.facts` invariants (#494) | +| Proven-safe bounds elision (`--proven-safe`, VCR-MEM-004) | Y (opt-in) | Consumes scry's `safe-accesses.json` (`scry/safe-accesses/v1`, scry#114) and elides the `--safety-bounds software` inline guard at the access sites scry PROVED in-bounds against the memory's guaranteed minimum. FAIL CLOSED on a `module_sha256` mismatch (verified against the exact bytes handed to the decoder, so a pre-compile rewrite that shifts operator indices refuses too), on a `memory_min_bytes` disagreement, and on a malformed/missing/wrong-schema file — each elides NOTHING, warns, and exits 0. Absence from the list means "not proven", NEVER "unsafe": an unlisted site keeps its guard. Each `(func, pc)` key is re-validated against the decoded operator (existence + access kind + width), so a wrong key space elides nothing LOUDLY instead of stripping the wrong guard. Writes a `synth-proven-safe-elisions-v1` attestation for sigil — on refusal too. MEASURED on `proven_safe_bounds_901.wat` (Cortex-M4): 5 of 8 sites proven ⇒ 232 → 152 B (80 B, 58 % of the guard tax) and 70 → 45 executed instructions (#901) | ### WCET (Track D, #778) @@ -99,7 +100,7 @@ see [coq/STATUS.md](../../coq/STATUS.md) for the per-file matrix. | Command | Notes | |---------|-------| -| `synth compile -o ` | WAT/WASM → ELF; `--cortex-m`, `--target `, `-b `, `--all-exports`, `--relocatable`, `--verify`, `--emit-wcet`, `--wcet-hints` | +| `synth compile -o ` | WAT/WASM → ELF; `--cortex-m`, `--target `, `-b `, `--all-exports`, `--relocatable`, `--verify`, `--emit-wcet`, `--wcet-hints`, `--proven-safe` | | `synth verify ` | Standalone translation validation (feature-gated build) | | `synth disasm ` | Disassemble generated ELF | | `synth parse ` | Parse and analyze WASM components | From 2be1ff87dcd245ec6e83feaca71bc6c3c5faebcd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 5 Aug 2026 18:38:46 +0200 Subject: [PATCH 8/8] fix(#901): --proven-safe must never silently do nothing (two false-surface defects) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both are the SAME class as the non-Software false attestation the byte gates already caught. That fix closed the instance, not the mechanism: every test path went through '--all-exports -b arm', so neither axis was observable. DEFECT 1 — FALSE ATTESTATION ON NON-ARM BACKENDS. Only the ARM direct selector consumes the marks (apply_mem_bounds_elision); RISC-V and aarch64 accept --safety-bounds software but emit their own guards from their own selectors and read no mark table. Measured before the fix: synth compile m.wasm -b riscv --target rv32imac ... --proven-safe s.json synth compile m.wasm -b aarch64 --target cortex-a53 ... --proven-safe s.json both wrote 'sites_elided: 5' while the ELF was BYTE-IDENTICAL to the guarded baseline. sigil would have attested five elisions that never happened. Now gated on the arm backend; the loud zero-elision path names the backend, and the attestation records 0 of 5. DEFECT 2 — SILENT NO-OP ON THE SINGLE-FUNCTION PATH. --func-index / --func-name never reach compile_all_exports, so --proven-safe there produced no ingestion, no diagnostic, no attestation, exit 0. That is the #865 shape (the v0.52 headline was a flag that quietly did nothing). Now a hard error naming the invocation that works. Deliberate asymmetry: a stale or malformed verdict FILE never fails a compile (it is data, and fail-closed handles it); an INVOCATION synth cannot honour is refused, matching --stack-layout's precedent. Also fixed: the zero-elision reason said 'none survived key validation' even when the sites were refused for fact-spec renumbering — it now points at the REFUSED/DROP lines and keeps the byte-offset hint conditional. DE-VACUATED the fact-spec combination gate: it asserted only inside a conditional on the stderr containing 'specialized', so a declining pass would have made it check nothing. Verified the pass DOES specialize this fixture — it admits the redundant-mask elision on the slot mask, deleting two operators (38 -> 36) and renumbering every index after them, which is exactly the skew the refusal exists for. The gate now asserts the specialization, the renumbering, the refusal AND the zero-elision attestation. RED-FIRST (mutation): forcing the backend-support flag to true turns non_arm_backends_attest_zero_elisions_901 RED (12 passed / 1 failed). Reverted. 13 byte gates (14 with --features verify), differential 207/207, frozen anchors 10/10, clippy -D warnings exit 0, claim_check 38/38. Bazel needs no change: crates/BUILD.bazel globs synth-core sources and no new external dependency was added. Implements: VCR-MEM-004 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CHANGELOG.md | 8 + crates/synth-cli/src/main.rs | 58 ++++++- .../synth-cli/tests/proven_safe_bounds_901.rs | 163 +++++++++++++++++- 3 files changed, 215 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bdfc1598..9df0de49 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -51,6 +51,14 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 binary. "Flag given, file accepted, nothing elided" is diagnosed by name rather than reported as success. + **The flag never silently does nothing.** Guards are stripped on the ARM + backend under `--safety-bounds software`; under any other backend or bounds + mode the verdicts are still ingested and verified, but the attestation + records ZERO elisions and names the reason, so it can never claim an elision + that did not happen. On the single-function path (`--func-index` / + `--func-name`), which builds no marks and has no attestation surface, the + flag is REFUSED loudly rather than ignored (the #865 silent-no-op shape). + **Attestation (sigil):** every `--proven-safe` compile writes `.proven-safe-elisions.json` (`synth-proven-safe-elisions-v1`) with the elision set, each site's authority, the scry version, both module hashes diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index c68c58e9..ba5f6202 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -508,6 +508,14 @@ enum Commands { /// `synth-proven-safe-elisions-v1`) recording the elision set, the /// scry version and the module hash — emitted on refusal too, so /// sigil can tell "nothing to elide" from "file rejected". + /// + /// SCOPE: guards are stripped on the ARM backend under + /// `--safety-bounds software`. Under any other backend or bounds mode + /// the verdicts are ingested and verified but nothing is elided; the + /// attestation says so and records ZERO elisions, so it never claims + /// an elision that did not happen. NOT accepted on the + /// single-function path (`--func-index` / `--func-name`), which + /// refuses loudly rather than ignoring the flag. #[arg(long, value_name = "PATH")] proven_safe: Option, @@ -1616,6 +1624,23 @@ fn compile_command( let use_all_exports = all_exports || (input.is_some() && func_index.is_none() && func_name_arg.is_none()); + // VCR-MEM-004 (#901): the single-function path (`--func-index` / + // `--func-name`) has no verdict ingestion, no elision marks and no + // attestation surface. Accepting `--proven-safe` there would be a SILENT + // NO-OP on a safety-relevant flag — the #865 defect shape, where + // `--safety-bounds` on aarch64 quietly did nothing. Refuse loudly and name + // the path that works. (A stale or malformed verdict FILE never fails a + // compile; an invocation synth cannot honour is a different thing.) + if !use_all_exports && proven_safe.is_some() { + anyhow::bail!( + "--proven-safe is not consumed on the single-function path \ + (--func-index / --func-name): that path builds no elision marks and \ + writes no attestation, so the flag would silently do nothing. Compile \ + the whole module instead (drop --func-index/--func-name, or pass \ + --all-exports)." + ); + } + if use_all_exports { return compile_all_exports( input, @@ -3334,6 +3359,11 @@ fn compile_all_exports( } r }); + // Only the ARM direct selector consumes the marks + // (`apply_mem_bounds_elision`); RISC-V and aarch64 emit their own bounds + // guards from their own selectors and read no mark table. Recorded here so + // the attestation cannot claim an elision the backend never performed. + let proven_safe_backend_supported = backend.name() == "arm"; // Accumulated across the function loop, for the sigil attestation. let mut proven_safe_elisions: Vec = Vec::new(); let mut proven_safe_diagnostics: Vec = proven_safe_ingest @@ -3564,13 +3594,20 @@ fn compile_all_exports( // THIS function. `pc` is an operator index into the ORIGINAL stream, so // the marks are only sound when that stream is what the backend // compiles — see the fact-spec refusal below. - // Gated on `Software`: that is the ONLY mode that emits an inline - // guard, so it is the only mode where a mark changes a byte. Without - // this gate the attestation would record elisions that never happened - // — a false attestation is worse than no attestation. + // Gated on `Software` AND on the ARM backend: `Software` is the only + // mode that emits an inline guard, and the ARM direct selector + // (`apply_mem_bounds_elision`) is the only consumer of the marks — + // RISC-V and aarch64 emit their own guards and read no mark table, so + // a mark there would change nothing. Without BOTH gates the + // attestation records elisions that never happened, and a false + // attestation is worse than no attestation. (Found on `-b riscv` / + // `-b aarch64`, which do accept `--safety-bounds software`: the + // sidecar claimed 5 elisions while the ELF was byte-identical to the + // guarded baseline.) if let Some(ing) = &proven_safe_ingest && ing.accepted && safety_bounds == SafetyBounds::Software + && proven_safe_backend_supported { let mut notes = Vec::new(); let marks = ing.validate_function(func.index, &func.ops, &mut notes); @@ -4197,6 +4234,14 @@ fn compile_all_exports( if ing.accepted && proven_safe_elisions.is_empty() { let why = if ing.offered.is_empty() { "the document proves zero access sites".to_string() + } else if !proven_safe_backend_supported { + format!( + "the `{}` backend does not consume proven-safe marks — only the ARM \ + direct selector strips the inline guard today. Every guard is \ + retained (sound), and this attestation records ZERO elisions rather \ + than claiming an elision that never happened", + backend.name() + ) } else if safety_bounds != SafetyBounds::Software { format!( "--safety-bounds is `{}`, not `software` — there is no inline guard to elide (the verdicts are mode-independent, the strip is not)", @@ -4204,7 +4249,10 @@ fn compile_all_exports( ) } else { format!( - "none of the {} offered site(s) survived key validation — see the DROP lines above; if the producer emitted wasm BYTE OFFSETS instead of 0-based OPERATOR indices, that is the cause", + "none of the {} offered site(s) reached the selector — see the \ + REFUSED/DROP lines above. If they were DROPPED on key validation \ + and the producer emitted wasm BYTE OFFSETS instead of 0-based \ + OPERATOR indices, that is the cause", ing.offered.len() ) }; diff --git a/crates/synth-cli/tests/proven_safe_bounds_901.rs b/crates/synth-cli/tests/proven_safe_bounds_901.rs index 922296de..79419206 100644 --- a/crates/synth-cli/tests/proven_safe_bounds_901.rs +++ b/crates/synth-cli/tests/proven_safe_bounds_901.rs @@ -503,6 +503,131 @@ fn flag_absent_writes_no_attestation_and_no_marks_901() { assert!(!a.stderr.contains("proven-safe")); } +// ============================================================================= +// Never silently do nothing — the #865 shape +// ============================================================================= + +/// Only the ARM direct selector consumes the marks. RISC-V and aarch64 accept +/// `--safety-bounds software` but emit their own guards from their own +/// selectors, so nothing is stripped there. The attestation must record ZERO +/// elisions and NAME the backend — a sidecar claiming elisions the backend +/// never performed is worse than no sidecar at all. +/// +/// (This is exactly what shipped before the gate: `-b riscv` and +/// `-b aarch64` both wrote `sites_elided: 5` while the ELF was byte-identical +/// to the guarded baseline.) +#[test] +fn non_arm_backends_attest_zero_elisions_901() { + let d = dir(); + let input = d.join("xback.wasm"); + std::fs::write(&input, fixture_wasm()).expect("write wasm"); + let json = d.join("xback.safe-accesses.json"); + std::fs::write(&json, safe_accesses(&module_hash(), 65536, PROVEN)).expect("write"); + + for (backend, target) in [("riscv", "rv32imac"), ("aarch64", "cortex-a53")] { + let run = |with_verdicts: bool, tag: &str| -> (Vec, String) { + let elf = d.join(format!("xback_{backend}_{tag}.elf")); + let mut cmd = Command::new(synth()); + cmd.args([ + "compile", + input.to_str().unwrap(), + "-o", + elf.to_str().unwrap(), + "-b", + backend, + "--target", + target, + "--all-exports", + "--safety-bounds", + "software", + ]); + if with_verdicts { + cmd.args(["--proven-safe", json.to_str().unwrap()]); + } + let out = cmd.output().expect("run synth"); + assert!( + out.status.success(), + "{backend} compile failed: {}", + String::from_utf8_lossy(&out.stderr) + ); + ( + std::fs::read(&elf).expect("read elf"), + String::from_utf8_lossy(&out.stderr).into_owned(), + ) + }; + let (base, _) = run(false, "base"); + let (with, stderr) = run(true, "with"); + + assert_eq!( + base, with, + "{backend}: --proven-safe must not move a byte on a backend that does \ + not consume the marks" + ); + assert!( + stderr.contains(&format!("`{backend}` backend does not consume")), + "{backend}: the zero-elision reason must name the backend: {stderr}" + ); + let att: serde_json::Value = serde_json::from_str( + &std::fs::read_to_string(synth_core::proven_safe::ElisionAttestation::sidecar_path( + &d.join(format!("xback_{backend}_with.elf")), + )) + .expect("attestation written"), + ) + .expect("valid JSON"); + assert_eq!( + att["sites_elided"], + serde_json::json!(0), + "{backend}: the attestation must NOT claim elisions the backend never made" + ); + assert_eq!(att["sites_offered"], serde_json::json!(5), "{backend}"); + } +} + +/// The single-function path (`--func-index` / `--func-name`) builds no marks +/// and writes no attestation, so accepting `--proven-safe` there would be a +/// SILENT NO-OP on a safety-relevant flag — the #865 defect. Refuse loudly. +#[test] +fn single_function_path_refuses_the_flag_rather_than_ignoring_it_901() { + let d = dir(); + let input = d.join("singlefn.wasm"); + std::fs::write(&input, fixture_wasm()).expect("write wasm"); + let json = d.join("singlefn.safe-accesses.json"); + std::fs::write(&json, safe_accesses(&module_hash(), 65536, PROVEN)).expect("write"); + let elf = d.join("singlefn.elf"); + + let out = Command::new(synth()) + .args([ + "compile", + input.to_str().unwrap(), + "-o", + elf.to_str().unwrap(), + "-b", + "arm", + "--target", + "cortex-m4", + "--func-index", + "0", + "--safety-bounds", + "software", + "--proven-safe", + json.to_str().unwrap(), + ]) + .output() + .expect("run synth"); + + assert!( + !out.status.success(), + "a flag that cannot be honoured must FAIL, not silently do nothing" + ); + let stderr = String::from_utf8_lossy(&out.stderr); + assert!( + stderr.contains("not consumed on the single-function path"), + "{stderr}" + ); + // ...and it names the invocation that DOES work. + assert!(stderr.contains("--all-exports"), "{stderr}"); +} + // ============================================================================= // Attestation — what sigil reads // ============================================================================= @@ -633,13 +758,33 @@ fn fact_spec_specialization_refuses_the_scry_marks_901() { .expect("run synth"); assert!(out.status.success()); let stderr = String::from_utf8_lossy(&out.stderr); - // Either the pass specialized this function (⇒ our marks are refused) or - // it declined outright (⇒ the stream is unchanged and the marks apply). - // Only the first case is a skew risk, and only it must produce a refusal. - if stderr.contains("specialized") { - assert!( - stderr.contains("REFUSED: SYNTH_FACT_SPEC specialized this function"), - "a renumbered op stream must refuse the scry marks: {stderr}" - ); - } + // NON-VACUITY FIRST: the pass must actually specialize this function, + // otherwise the refusal below is never exercised and this test asserts + // nothing. It admits the redundant-mask elision on `slot & 63` under the + // premise, which DELETES two operators (38 -> 36) and renumbers every + // index after them — exactly the skew the refusal exists for. + assert!( + stderr.contains("'probe' specialized"), + "the fact-spec pass must specialize this fixture or this gate is \ + vacuous — the refusal path would never run: {stderr}" + ); + assert!( + stderr.contains("38 → 36 ops"), + "the specialization must RENUMBER the operator index space (that is \ + what makes the scry keys stale): {stderr}" + ); + assert!( + stderr.contains("REFUSED: SYNTH_FACT_SPEC specialized this function"), + "a renumbered op stream must refuse the scry marks: {stderr}" + ); + // And the refusal must be total: nothing elided, attested as such. + let att: serde_json::Value = serde_json::from_str( + &std::fs::read_to_string(synth_core::proven_safe::ElisionAttestation::sidecar_path( + &elf, + )) + .expect("attestation written"), + ) + .expect("valid JSON"); + assert_eq!(att["sites_elided"], serde_json::json!(0)); + assert_eq!(att["sites_offered"], serde_json::json!(5)); }