fix(#932): --proven-safe must never elide against a floor it invented (SECURITY)

crates/synth-cli/src/main.rs

@@ -3328,7 +3328,32 @@ fn compile_all_exports(
     // (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);
+    // #932 (CRITICAL/SECURITY): this was
+    //     all_memories.first().map(|m| m.initial_bytes()).unwrap_or(0)
+    // and `unwrap_or(0)` turned "no floor can be established" into "the floor
+    // is 0 bytes". An IMPORTED memory is not in `all_memories` (imports land in
+    // `all_imports`), so for `(import "env" "memory" (memory 1))` the derived
+    // floor was 0 — and then:
+    //
+    //   memory_min_bytes = 0     -> ACCEPTED, 2 udf guards -> 0   (STRIPPED)
+    //   memory_min_bytes = 65536 -> REFUSED, guards kept          (the TRUTH)
+    //
+    // i.e. the fail-closed contract INVERTED: the honest document was rejected
+    // and the vacuous one stripped real guards, with synth printing "proved 1
+    // access site in-bounds against the 0 B floor" — self-refuting, since no
+    // access is in bounds of a zero-byte memory. An imported memory is real at
+    // run time, so that is an unguarded access at an attacker-controlled offset.
+    //
+    // A floor synth cannot ESTABLISH is now `None`, and `None` REFUSES. Absence
+    // of evidence is never evidence of safety — the same rule the rest of this
+    // seam already states and this line quietly broke.
+    //
+    // FOLLOW-UP (named, not silent): an imported memory declares its own
+    // minimum, but the decoder discards it (`TypeRef::Memory(_)` ->
+    // `ImportKind::Memory`), so the truthful document still cannot be accepted
+    // for imported memory — it is REFUSED, which is safe but not yet useful.
+    // Carrying the declared minimum through is tracked on #932.
+    let proven_safe_module_min_bytes: Option<u32> = all_memories.first().map(|m| m.initial_bytes());
     let proven_safe_ingest: Option<synth_core::proven_safe::ProvenSafeIngest> =
         proven_safe.as_ref().map(|path| {
             let module_bytes: &[u8] = sbom_wasm_bytes.as_deref().unwrap_or(&[]);
@@ -3338,8 +3363,29 @@ fn compile_all_exports(
                     path.display()
                 );
             }
-            let r =
-                synth_core::proven_safe::ingest(path, module_bytes, proven_safe_module_min_bytes);
+            let Some(min_bytes) = proven_safe_module_min_bytes else {
+                // #932: no DEFINED memory, so no floor synth can stand behind.
+                // The computed hash is reported even on this refusal: a
+                // consumer debugging a rejected document should not have to
+                // provoke a DIFFERENT refusal to learn what synth hashed, and
+                // #932's own regression test needs it to construct a document
+                // that reaches the floor check rather than dying at the hash.
+                eprintln!(
+                    "warning: --proven-safe {}: this module defines no linear memory \
+                     (an imported memory declares its minimum elsewhere, which synth \
+                     does not yet carry), so NO memory floor can be established; NO \
+                     bounds guard is elided (fail closed). This compile's module \
+                     hashes to {}.",
+                    path.display(),
+                    synth_core::proven_safe::hex_sha256(module_bytes)
+                );
+                return synth_core::proven_safe::ProvenSafeIngest::refused(
+                    "no linear memory is DEFINED by this module, so no memory floor \
+                     can be established; refusing rather than validating verdicts \
+                     against a 0 B floor (#932)",
+                );
+            };
+            let r = synth_core::proven_safe::ingest(path, module_bytes, min_bytes);
             for d in &r.diagnostics {
                 eprintln!("warning: proven-safe: {d}");
             }
@@ -4271,7 +4317,11 @@ fn compile_all_exports(
             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,
+            // #932: an attestation is only reached on an ACCEPTED ingest, and
+            // acceptance now requires an ESTABLISHED floor — so this cannot be
+            // the old invented 0. The `unwrap_or(0)` here is unreachable by
+            // construction; it is not a fallback.
+            memory_min_bytes: proven_safe_module_min_bytes.unwrap_or(0),
             declared_memory_min_bytes: ing.declared_memory_min_bytes,
             safety_bounds: safety_bounds.as_str().to_string(),
             accepted: ing.accepted,

crates/synth-cli/tests/proven_safe_imported_memory_932.rs

@@ -0,0 +1,211 @@
+//! #932 (CRITICAL/SECURITY) — `--proven-safe` must never elide against a floor
+//! it invented.
+//!
+//! For a module whose memory is IMPORTED, the derived floor was
+//! `all_memories.first().map(..).unwrap_or(0)` = **0**, because imported
+//! memories live in `imports`, not `memories`. Measured on v0.55.0:
+//!
+//! | claimed `memory_min_bytes` | verdict  | bounds guards |
+//! |---|---|---|
+//! | baseline, no `--proven-safe` | —        | present |
+//! | `0`     (vacuous)            | ACCEPTED | **STRIPPED** |
+//! | `65536` (the truth)          | REFUSED  | present |
+//!
+//! The fail-closed contract inverted: the honest document rejected, the vacuous
+//! one stripping real guards, while synth printed "proved 1 access site
+//! in-bounds against the 0 B floor" — self-refuting, since no access is in
+//! bounds of a zero-byte memory. An imported memory is real at run time, so
+//! that is an unguarded access at an attacker-controlled offset.
+//!
+//! # Why this test exists in this shape
+//!
+//! The #901 differential that gated the original feature used a module with a
+//! **declared** memory, so the imported shape was never exercised and the
+//! validator only ever saw the case it was written against — the v0.53 lesson
+//! that a validator tests the shape it was written against. This pins the
+//! SHAPE, not just the symptom.
+
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+fn synth() -> PathBuf {
+    PathBuf::from(env!("CARGO_BIN_EXE_synth"))
+}
+
+fn workdir(tag: &str) -> PathBuf {
+    let d = std::env::temp_dir().join(format!("synth-932-{tag}"));
+    std::fs::create_dir_all(&d).expect("temp dir");
+    d
+}
+
+/// Bytes of machine code, from synth's OWN stdout (`Total code size: N bytes`).
+///
+/// NOT from disassembly. The first version counted `udf` mnemonics in
+/// `synth disasm` output; it passed on macOS and returned ZERO on the ubuntu
+/// runner, failing both tests with "fixture must emit guards, got 0". That is a
+/// lesson already recorded in this repo and violated anyway: **disassembly TEXT
+/// is host-dependent — read structure, not rendering.** It also traded an
+/// `llvm-objdump` host dependency for a worse one.
+///
+/// Code size is synth's own number, identical on every host, and it moves for
+/// exactly the reason under test: eliding a bounds guard REMOVES instructions
+/// (measured on the declared-memory fixture: 24 B guarded, 8 B elided).
+fn code_size(stdout: &str) -> usize {
+    stdout
+        .split("Total code size:")
+        .nth(1)
+        .and_then(|s| s.split_whitespace().next())
+        .and_then(|n| n.parse().ok())
+        .unwrap_or_else(|| panic!("no 'Total code size:' in synth stdout:\n{stdout}"))
+}
+
+/// Compile and return `(code_size_bytes, stderr)`.
+fn compile(dir: &Path, wasm: &Path, out: &str, verdicts: Option<&Path>) -> (usize, String) {
+    let obj = dir.join(out);
+    let mut c = Command::new(synth());
+    c.args([
+        "compile",
+        wasm.to_str().unwrap(),
+        "-b",
+        "arm",
+        "--target",
+        "cortex-m4",
+        "--safety-bounds",
+        "software",
+        "--all-exports",
+        "--relocatable",
+        "-o",
+        obj.to_str().unwrap(),
+    ]);
+    if let Some(v) = verdicts {
+        c.args(["--proven-safe", v.to_str().unwrap()]);
+    }
+    let o = c.output().expect("run synth compile");
+    assert!(
+        o.status.success(),
+        "compile failed: {}",
+        String::from_utf8_lossy(&o.stderr)
+    );
+    (
+        code_size(&String::from_utf8_lossy(&o.stdout)),
+        String::from_utf8_lossy(&o.stderr).to_string(),
+    )
+}
+
+/// The sha256 synth computes over the bytes it hands to the DECODER, scraped
+/// from synth's own diagnostic.
+///
+/// This matters more than it looks. The first version of this test used a dummy
+/// hash, so every compile was refused at the HASH gate and the guards survived
+/// for a reason unrelated to #932 — mutating the fix away did NOT fail the
+/// test. Making the hash CORRECT is what leaves the floor check as the only
+/// thing that can refuse.
+fn actual_module_sha256(dir: &Path, wat: &Path) -> String {
+    let probe = dir.join("probe_hash.json");
+    std::fs::write(
+        &probe,
+        format!(
+            r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{}",
+                 "memory_min_bytes":65536,"proven_safe":[]}}"#,
+            "0".repeat(64)
+        ),
+    )
+    .expect("write probe");
+    let (_sz, stderr) = compile(dir, wat, "probe.o", Some(&probe));
+    stderr
+        .split("hashes to ")
+        .nth(1)
+        .and_then(|s| s.split(['.', ' ', '\n']).next())
+        .map(|s| s.trim().to_string())
+        .unwrap_or_else(|| panic!("could not scrape the module hash from:\n{stderr}"))
+}
+
+fn verdict_doc(dir: &Path, name: &str, sha: &str, claimed: u64) -> PathBuf {
+    let v = dir.join(name);
+    std::fs::write(
+        &v,
+        format!(
+            r#"{{"schema":"scry/safe-accesses/v1","module_sha256":"{sha}",
+                 "memory_min_bytes":{claimed},
+                 "proven_safe":[{{"func":0,"pc":1,"op":"i32.load","width":4}}]}}"#
+        ),
+    )
+    .expect("write verdicts");
+    v
+}
+
+const IMPORTED: &str = r#"(module
+  (import "env" "memory" (memory 1))
+  (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a))))
+"#;
+
+const DECLARED: &str = r#"(module
+  (memory 1)
+  (func (export "probe") (param $a i32) (result i32) (i32.load (local.get $a))))
+"#;
+
+/// THE SECURITY PROPERTY. A module whose floor synth cannot establish must keep
+/// every guard — whatever the document claims.
+#[test]
+fn imported_memory_never_elides_against_an_invented_floor() {
+    let dir = workdir("imported");
+    let wat = dir.join("imp.wat");
+    std::fs::write(&wat, IMPORTED).expect("write wat");
+
+    let (baseline, _) = compile(&dir, &wat, "base.o", None);
+    // Non-vacuity: with no code there is nothing to elide and the comparisons
+    // below would pass over an empty set forever.
+    assert!(
+        baseline > 0,
+        "fixture must emit code without --proven-safe, got {baseline} bytes"
+    );
+    let sha = actual_module_sha256(&dir, &wat);
+
+    // The VACUOUS claim (0) and the TRUTHFUL one (65536) must BOTH leave the
+    // code untouched: synth cannot establish this module's floor, and absence
+    // of evidence is not evidence of safety.
+    for claimed in [0u64, 65536] {
+        let v = verdict_doc(&dir, &format!("verdicts_{claimed}.json"), &sha, claimed);
+        let (size, stderr) = compile(&dir, &wat, &format!("out_{claimed}.o"), Some(&v));
+        assert_eq!(
+            size, baseline,
+            "claimed floor {claimed}: code SHRANK {baseline} -> {size} bytes, i.e. \
+             guards were elided for a module whose floor synth cannot establish. \
+             That is #932 — an unguarded access at an attacker-controlled \
+             offset. stderr:\n{stderr}"
+        );
+        assert!(
+            !stderr.contains("0 B floor"),
+            "synth must never report proving anything 'against the 0 B floor' — \
+             no access is in bounds of a zero-byte memory. stderr:\n{stderr}"
+        );
+    }
+}
+
+/// The feature must still WORK where a floor genuinely exists, or the fix above
+/// is indistinguishable from deleting it.
+#[test]
+fn declared_memory_still_elides_on_a_truthful_document() {
+    let dir = workdir("declared");
+    let wat = dir.join("decl.wat");
+    std::fs::write(&wat, DECLARED).expect("write wat");
+
+    let (baseline, _) = compile(&dir, &wat, "base.o", None);
+    assert!(baseline > 0, "fixture must emit code, got {baseline} bytes");
+    let sha = actual_module_sha256(&dir, &wat);
+
+    let v = verdict_doc(&dir, "v.json", &sha, 65536);
+    let (size, stderr) = compile(&dir, &wat, "out.o", Some(&v));
+
+    assert!(
+        !stderr.contains("no linear memory"),
+        "a DECLARED memory establishes a floor — the #932 refusal must not fire \
+         here. stderr:\n{stderr}"
+    );
+    assert!(
+        size < baseline,
+        "the feature must still ELIDE where a floor genuinely exists, else the \
+         #932 fix is indistinguishable from deleting it: baseline {baseline}, \
+         got {size}. stderr:\n{stderr}"
+    );
+}

crates/synth-core/src/proven_safe.rs

@@ -140,6 +140,15 @@ pub struct ProvenSafeIngest {
 }
 
 impl ProvenSafeIngest {
+    /// A refusal the CALLER establishes, for a gate that cannot be checked
+    /// inside this module. #932: the memory floor is derived by the CLI from
+    /// the decoded module, so "no floor could be established" is refusable only
+    /// out there — and it must refuse, not fall back to a `0` floor, because
+    /// every verdict validated against a zero-byte floor is vacuous.
+    pub fn refused(reason: impl Into<String>) -> Self {
+        Self::refuse(reason)
+    }
+
     /// A refusal: nothing trusted, one named reason.
     fn refuse(reason: impl Into<String>) -> Self {
         let reason = reason.into();