From 25e2628ab3fb4757f7670373c22582a2d00c2ca6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 21 Aug 2026 07:17:55 +0200 Subject: [PATCH 1/2] fix: #346 never write a module loom has not validated, and emit the data count section MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `loom optimize` dropped the data count section while keeping the `memory.init` instructions that require it, then printed "✅ Optimization complete!" and exited 0 over a module no validator accepts. Reproduces from a 79-byte hand-written module, not just the fused one in the report. Silent invalid output is the worst shape this can take: the next tool in the chain reports the failure against ITS OWN input, so the blame lands downstream of the tool that actually broke the module. --- the narrow half: the section was never emitted at all --- Not "dropped" — there was no reference to the data count section anywhere in loom-core. The parser read MemoryInit/DataDrop; nothing ever wrote the section they require. The spec makes it mandatory precisely so those instructions can be validated without scanning the data section. Now emitted (id 12) between element and code whenever those instructions survive into the output. The count is the number of data segments — the size of the index space they index into, not the number of references. --- the systemic half: the guarantee was unreachable --- The #257 MANDATORY AUTHORITATIVE OUTPUT-VALIDATION BACKSTOP, whose comment states it is the systemic guarantee that loom can NEVER emit structurally invalid wasm, lives inside `optimize_module`. The CLI does not call it — it drives the passes directly (#345). Grepping loom-cli/src/main.rs for "validate" returned three hits, all comments. The binary everyone runs had no output validation whatsoever, so ANY encoder bug shipped silently as success. This one did. All three CLI write paths — serial pipeline, islands, component — now go through one gate that validates before writing, using the same authoritative check via a newly exposed `encode::validate_output_bytes` so the CLI cannot drift to a weaker feature set than the parser. On failure the ORIGINAL input is written instead, but only after the original is itself proven valid — a .wat input, or one that was already invalid, must not be copied over the output path and presented as a module. Exit is non-zero either way: a caller that checks learns something broke, and a caller that ignores exit codes still gets a module that loads. --- tests --- The load-bearing assertion is that the emitted module carries a data count SECTION, not merely that it validates — validation alone would also pass if a future change simply deleted the instructions. The unit tests on the gate are what would fail if the gate were removed; the fixture sweep ("exit 0 implies the artifact validates") holds trivially while the encoder is correct and so cannot catch that. Paired with a positive control, since a gate that refused everything would pass the refusal test. Confirmed discriminating twice, by reverting each half: without the encoder fix the memory.init test fails on "data count section required"; without the gate the CLI writes the invalid module and exits 0. loom-cli 21/21, loom-core --lib 534/534 (default AND both-mode), --test verification 47/47. fmt clean; clippy unchanged (the three remaining warnings are pre-existing in the feature-gated maybe_differential_gate). Verifies TEST-346-OUTPUT-IS-VALIDATED-BEFORE-IT-IS-WRITTEN Fixes #346 Refs #345, #257, #289 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01RZof1M5HMBSYVZPeoT4MEn --- loom-cli/src/main.rs | 151 +++++++++++++++++- loom-cli/tests/output_validation.rs | 210 ++++++++++++++++++++++++++ loom-core/src/lib.rs | 47 ++++++ safety/requirements/verification.yaml | 66 ++++++++ 4 files changed, 467 insertions(+), 7 deletions(-) create mode 100644 loom-cli/tests/output_validation.rs diff --git a/loom-cli/src/main.rs b/loom-cli/src/main.rs index 8944f62..808abbe 100644 --- a/loom-cli/src/main.rs +++ b/loom-cli/src/main.rs @@ -348,6 +348,56 @@ fn count_instructions_from_bytes(bytes: &[u8]) -> usize { /// (safe, unoptimized) bytes to `output_path` and return `Err` so the process /// exits non-zero. A no-op when the gate is disabled (`original` is `None`). #[allow(unused_variables)] +/// Write the optimized artifact ONLY if it passes authoritative WebAssembly +/// validation (#346). +/// +/// `loom optimize` used to write whatever the encoder produced and print +/// "✅ Optimization complete!" over it. When the encoder dropped the data +/// count section while keeping the `memory.init` instructions that require it, +/// the result was a module no validator accepts — emitted with exit code 0. +/// Silent invalid output is the worst shape this can take: the next tool in +/// the chain reports the failure against ITS OWN input, so the blame lands +/// downstream of the tool that actually broke the module. +/// +/// `loom_core::optimize::optimize_module` has carried exactly this gate since +/// #257, described there as the systemic guarantee that loom can NEVER emit +/// structurally invalid wasm. The CLI does not go through that function — it +/// drives the passes directly (#345) — so it inherited none of it. This closes +/// that hole at the only point that matters: the write. +/// +/// On failure the ORIGINAL input is written instead, when the original itself +/// validates, so the worst case is unoptimized-but-valid output rather than a +/// missing or corrupt file. The exit code is still non-zero: a caller that +/// checks it learns something went wrong, and a caller that ignores it still +/// gets a module that loads. +fn write_validated_output( + output_path: &str, + output_bytes: &[u8], + wasm_to_validate: &[u8], + original_input: &[u8], +) -> Result<()> { + if let Err(e) = loom_core::encode::validate_output_bytes(wasm_to_validate) { + eprintln!("error: the optimized module failed authoritative WebAssembly validation:"); + eprintln!(" {e}"); + // Fall back to the input, but only after proving the input itself is + // valid wasm — a `.wat` input, or one that was already invalid, must + // not be copied over the output path and presented as a module. + let recovered = loom_core::encode::validate_output_bytes(original_input).is_ok() + && fs::write(output_path, original_input).is_ok(); + if recovered { + eprintln!("note: wrote the ORIGINAL module to {output_path} instead;"); + eprintln!(" nothing invalid was written, and nothing was optimized."); + } else { + eprintln!("note: no output was written."); + } + eprintln!("note: this is a loom bug — please report it with the input module."); + return Err(anyhow!("refusing to emit a module that does not validate")); + } + fs::write(output_path, output_bytes).context("Failed to write output file")?; + println!("✓ Written to: {}", output_path); + Ok(()) +} + fn maybe_differential_gate( original: Option<&[u8]>, optimized_wasm: &[u8], @@ -519,9 +569,14 @@ fn optimize_command( // Write optimized component let output_path = output.unwrap_or_else(|| "output.wasm".to_string()); - fs::write(&output_path, &optimized_bytes) - .context("Failed to write output file")?; - println!("✓ Written to: {}", output_path); + // #346: components go through the same gate. `validate` + // handles the component grammar as well as core modules. + write_validated_output( + &output_path, + &optimized_bytes, + &optimized_bytes, + &input_bytes, + )?; println!("\n✅ Optimization complete!"); return Ok(()); } @@ -653,8 +708,15 @@ fn optimize_command( }; maybe_differential_gate(original_wasm.as_deref(), &opt_wasm, &output_path)?; } - fs::write(&output_path, &output_bytes).context("Failed to write output file")?; - println!("✓ Written to: {}", output_path); + // #346: validate before writing. For WAT output the bytes on disk are + // text, so the WASM encoding is what gets validated. + let validate_bytes = if output_wat { + loom_core::encode::encode_wasm(&module) + .context("Failed to encode optimized module for output validation")? + } else { + output_bytes.clone() + }; + write_validated_output(&output_path, &output_bytes, &validate_bytes, &input_bytes)?; if show_stats { stats.print(); @@ -999,8 +1061,15 @@ fn optimize_command( }; maybe_differential_gate(original_wasm.as_deref(), &opt_wasm, &output_path)?; } - fs::write(&output_path, &output_bytes).context("Failed to write output file")?; - println!("✓ Written to: {}", output_path); + // #346: validate before writing. For WAT output the bytes on disk are + // text, so the WASM encoding is what gets validated. + let validate_bytes = if output_wat { + loom_core::encode::encode_wasm(&module) + .context("Failed to encode optimized module for output validation")? + } else { + output_bytes.clone() + }; + write_validated_output(&output_path, &output_bytes, &validate_bytes, &input_bytes)?; // Show statistics if requested if show_stats { @@ -1532,4 +1601,72 @@ mod tests { assert_eq!(stats.reduction_percentage(100, 25), 75.0); assert_eq!(stats.reduction_percentage(0, 0), 0.0); } + + /// The #346 backstop, tested directly on its refusal path. + /// + /// The integration sweep asserts "success implies the artifact validates", + /// which holds trivially while the encoder is correct — so it cannot fail + /// if the gate is deleted. This can: it hands the gate bytes that are + /// definitely invalid and asserts the three things that must follow. + /// + /// Before #346 the CLI had no such gate at all: `fs::write` was called on + /// whatever the encoder returned, and "✅ Optimization complete!" was + /// printed over it. + #[test] + fn the_output_gate_refuses_invalid_bytes_and_restores_the_original() { + // Valid: (module) — the 8-byte preamble is a complete empty module. + const VALID: &[u8] = &[0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00]; + // Invalid: right magic, but a truncated type section header. + const INVALID: &[u8] = &[0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, 0x01, 0x7f]; + assert!(loom_core::encode::validate_output_bytes(VALID).is_ok()); + assert!( + loom_core::encode::validate_output_bytes(INVALID).is_err(), + "the negative fixture must actually be invalid, or this test \ + asserts nothing" + ); + + let dir = std::env::temp_dir().join(format!("loom-346-unit-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("create scratch dir"); + let out_path = dir.join("out.wasm"); + let out_str = out_path.to_str().unwrap(); + + let result = write_validated_output(out_str, INVALID, INVALID, VALID); + + assert!( + result.is_err(), + "the gate accepted bytes that do not validate; exit 0 over an \ + invalid module is exactly the #346 defect" + ); + let written = std::fs::read(&out_path).expect("the gate must leave a valid file behind"); + assert_ne!( + written, INVALID, + "the invalid bytes were written to the output path" + ); + assert_eq!( + written, VALID, + "the gate must fall back to the original module so the worst case \ + is unoptimized-but-valid output, never a corrupt artifact" + ); + + let _ = std::fs::remove_file(&out_path); + } + + /// The positive control: valid bytes must be written unchanged. Without + /// this, a gate that refused everything would pass the test above. + #[test] + fn the_output_gate_writes_valid_bytes_unchanged() { + const VALID: &[u8] = &[0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00]; + let dir = std::env::temp_dir().join(format!("loom-346-unit-ok-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("create scratch dir"); + let out_path = dir.join("ok.wasm"); + let out_str = out_path.to_str().unwrap(); + + write_validated_output(out_str, VALID, VALID, VALID).expect("valid output must be written"); + assert_eq!( + std::fs::read(&out_path).expect("read back"), + VALID, + "valid output must reach disk byte-for-byte" + ); + let _ = std::fs::remove_file(&out_path); + } } diff --git a/loom-cli/tests/output_validation.rs b/loom-cli/tests/output_validation.rs new file mode 100644 index 0000000..23a6225 --- /dev/null +++ b/loom-cli/tests/output_validation.rs @@ -0,0 +1,210 @@ +//! `loom optimize` must never write a module that does not validate (#346). +//! +//! Two defects met here. The encoder dropped the **data count section** while +//! keeping the `memory.init` / `data.drop` instructions that require it — the +//! spec makes that section mandatory precisely so those instructions can be +//! validated without scanning the data section, so the output was structurally +//! invalid rather than merely suboptimal. And nothing checked: the CLI wrote +//! whatever the encoder produced and printed `✅ Optimization complete!` over +//! it, exit 0. +//! +//! Silent invalid output is the worst shape this can take. The next tool in +//! the chain reports the failure against *its own* input, so the blame lands +//! downstream of the tool that actually broke the module. +//! +//! `loom_core::optimize::optimize_module` has carried an output-validation +//! backstop since #257 — described there as the systemic guarantee that loom +//! can NEVER emit structurally invalid wasm. The CLI does not go through that +//! function (#345), so it inherited none of it. +//! +//! These tests drive the real binary, because the property is about what lands +//! on disk. + +use std::process::Command; + +/// The #346 reproduction, assembled from: +/// +/// ```wat +/// (module +/// (memory 1) +/// (data $d "hello") +/// (func (export "init") (param i32) +/// local.get 0 i32.const 0 i32.const 5 +/// memory.init $d +/// data.drop $d)) +/// ``` +/// +/// 79 bytes, valid on input, and the smallest thing that exercises both +/// instructions that make the data count section mandatory. +const MEMORY_INIT_WASM: &[u8] = &[ + 0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, 0x01, 0x05, 0x01, 0x60, 0x01, 0x7f, 0x00, 0x03, + 0x02, 0x01, 0x00, 0x05, 0x03, 0x01, 0x00, 0x01, 0x07, 0x08, 0x01, 0x04, 0x69, 0x6e, 0x69, 0x74, + 0x00, 0x00, 0x0c, 0x01, 0x01, 0x0a, 0x11, 0x01, 0x0f, 0x00, 0x20, 0x00, 0x41, 0x00, 0x41, 0x05, + 0xfc, 0x08, 0x00, 0x00, 0xfc, 0x09, 0x00, 0x0b, 0x0b, 0x08, 0x01, 0x01, 0x05, 0x68, 0x65, 0x6c, + 0x6c, 0x6f, 0x00, 0x0b, 0x04, 0x6e, 0x61, 0x6d, 0x65, 0x09, 0x04, 0x01, 0x00, 0x01, 0x64, +]; + +fn scratch_dir(tag: &str) -> std::path::PathBuf { + let dir = std::env::temp_dir().join(format!("loom-346-{tag}-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("create scratch dir"); + dir +} + +/// Section id 12 is the data count section. Walking the section headers is +/// enough — every section after the 8-byte preamble is `[id][uleb size]`. +fn has_data_count_section(bytes: &[u8]) -> bool { + let mut i = 8; // magic + version + while i < bytes.len() { + let id = bytes[i]; + i += 1; + // uleb128 section size + let mut size: usize = 0; + let mut shift = 0; + loop { + if i >= bytes.len() { + return false; + } + let b = bytes[i]; + i += 1; + size |= ((b & 0x7f) as usize) << shift; + if b & 0x80 == 0 { + break; + } + shift += 7; + } + if id == 12 { + return true; + } + i += size; + } + false +} + +/// The end-to-end property: a module using `memory.init` must come out valid. +/// +/// Before the fix this wrote a module rejected with "data count section +/// required" while exiting 0. +#[test] +fn a_module_using_memory_init_is_emitted_valid() { + let dir = scratch_dir("init"); + let input = dir.join("in.wasm"); + let output = dir.join("out.wasm"); + std::fs::write(&input, MEMORY_INIT_WASM).expect("write input"); + + // The input itself must be valid, or the test proves nothing about output. + assert!( + loom_core::encode::validate_output_bytes(MEMORY_INIT_WASM).is_ok(), + "the fixture is not valid wasm; the test cannot attribute an invalid \ + OUTPUT to the optimizer" + ); + + let out = Command::new(env!("CARGO_BIN_EXE_loom")) + .args([ + "optimize", + input.to_str().unwrap(), + "-o", + output.to_str().unwrap(), + ]) + .output() + .expect("failed to run the loom binary"); + + assert!( + out.status.success(), + "optimizing a valid memory.init module failed:\nstdout: {}\nstderr: {}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ); + + let emitted = std::fs::read(&output).expect("read the emitted module"); + if let Err(e) = loom_core::encode::validate_output_bytes(&emitted) { + panic!( + "loom emitted a module that does not validate: {e}\n\ + (this is #346: the data count section is mandatory whenever \ + memory.init or data.drop appear)" + ); + } + + // And specifically the section that was missing. Validation alone would + // also pass if some future change removed the instructions entirely, so + // assert the section is there rather than only that nothing complained. + assert!( + has_data_count_section(&emitted), + "the emitted module validates but carries no data count section — \ + check whether the memory.init instructions survived at all" + ); +} + +/// The systemic half, and the one that matters beyond this instance: the CLI +/// must not write output it has not validated. +/// +/// Rather than asserting on the encoder (already covered above), this asserts +/// the property that makes the NEXT encoder bug loud instead of silent — that +/// success on stdout implies the artifact on disk validates. Driven over every +/// wasm fixture in the repo that the binary accepts. +#[test] +fn every_successful_optimize_leaves_a_valid_module_on_disk() { + let fixtures = + std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("../loom-core/tests/fixtures"); + let dir = scratch_dir("sweep"); + + let mut checked = 0usize; + let entries = match std::fs::read_dir(&fixtures) { + Ok(e) => e, + Err(_) => return, // fixtures directory absent in some checkouts + }; + for entry in entries.flatten() { + let path = entry.path(); + if path.extension().and_then(|e| e.to_str()) != Some("wasm") { + continue; + } + // Only modules that were valid to begin with can hold loom responsible + // for an invalid result. + let input_bytes = match std::fs::read(&path) { + Ok(b) => b, + Err(_) => continue, + }; + if loom_core::encode::validate_output_bytes(&input_bytes).is_err() { + continue; + } + + let output = dir.join(format!( + "{}.opt.wasm", + path.file_stem().unwrap().to_string_lossy() + )); + let out = Command::new(env!("CARGO_BIN_EXE_loom")) + .args([ + "optimize", + path.to_str().unwrap(), + "-o", + output.to_str().unwrap(), + // Keep the sweep quick: the full pipeline is exercised by the + // test above, and #347 makes `inline` unusably slow on some + // real modules. + "--passes", + "dce,vacuum,constant-folding", + ]) + .output() + .expect("failed to run the loom binary"); + + if !out.status.success() { + // A refusal is the CORRECT behaviour now — it means the gate + // fired. What must never happen is success over invalid output. + continue; + } + checked += 1; + let emitted = std::fs::read(&output).expect("read the emitted module"); + if let Err(e) = loom_core::encode::validate_output_bytes(&emitted) { + panic!( + "loom reported SUCCESS but wrote an invalid module for {}: {e}\n\ + Exit 0 must imply the artifact validates (#346).", + path.display() + ); + } + } + + assert!( + checked > 0, + "the sweep validated no modules at all, so it asserts nothing — check \ + that the fixtures directory is present and that the binary accepts them" + ); +} diff --git a/loom-core/src/lib.rs b/loom-core/src/lib.rs index 864abc8..8ea30c3 100644 --- a/loom-core/src/lib.rs +++ b/loom-core/src/lib.rs @@ -1901,6 +1901,25 @@ pub mod encode { encode_wasm_with_facts(module, false) } + /// Run the authoritative WebAssembly spec validator over emitted bytes. + /// + /// This is the SAME check the #257 output-validation backstop applies, + /// exposed so a caller that does its own encoding — notably the CLI, which + /// drives the passes directly rather than through + /// [`crate::optimize::optimize_module`] — can apply the identical gate + /// instead of an approximation of it. + /// + /// It exists because that divergence had teeth (#346): the backstop lived + /// inside `optimize_module`, the binary never called it, and so + /// `loom optimize` emitted a module that no validator would accept while + /// printing a success message. A guarantee reachable only from a function + /// nobody calls is prose, not a guarantee. + pub fn validate_output_bytes(bytes: &[u8]) -> Result<()> { + wasmparser::validate(bytes) + .map(|_| ()) + .map_err(|e| anyhow::anyhow!("{e}")) + } + /// Encode to WebAssembly binary, optionally emitting the #231 `wsc.facts` /// custom section (schema v1) from `module.facts`. /// @@ -2109,6 +2128,34 @@ pub mod encode { }); } + // Build the DATA COUNT section (id 12) — #346. + // + // The spec makes this section MANDATORY whenever `memory.init` or + // `data.drop` appear in the code: it exists so those instructions can + // be validated without scanning the data section, and a validator + // rejects the module outright when it is missing. loom preserved the + // data section and the instructions but never emitted this section at + // all — there was no reference to it anywhere in the crate — so any + // module using `memory.init` came out structurally INVALID while the + // CLI reported success. + // + // It must be written between the element section (9) and the code + // section (10), which is why it is emitted here rather than beside the + // data section it describes. + // + // The count is the number of data segments, not the number of + // instructions referencing them: it is the length of the data index + // space that `memory.init`/`data.drop` index into. + if module.functions.iter().any(|f| { + f.instructions + .iter() + .any(|i| matches!(i, Instruction::MemoryInit { .. } | Instruction::DataDrop(_))) + }) { + wasm_module.section(&wasm_encoder::DataCountSection { + count: module.data_segments.len() as u32, + }); + } + // Build code section (function bodies) let mut code = CodeSection::new(); for func in &module.functions { diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index a7005bd..fc52a2c 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -1119,3 +1119,69 @@ artifacts: target: REQ-3 - type: verifies target: REQ-1 + + # ============================================================================ + # #346 / #345 — v1.4.1: the binary must not emit what it has not validated. + # + # The encoder never emitted a data count section — there was no reference to + # it anywhere in the crate — so any module using `memory.init` or `data.drop` + # came out structurally INVALID. Nothing caught it, because the #257 + # output-validation backstop lives inside `optimize_module` and the CLI + # drives the passes directly (#345). A guarantee reachable only from a + # function nobody calls is prose, not a guarantee. + # ============================================================================ + + - id: TEST-346-OUTPUT-IS-VALIDATED-BEFORE-IT-IS-WRITTEN + type: feature + title: the data count section is emitted, and no unvalidated module is ever written (#346, #345) + description: > + Verifies both halves of the #346 defect. The narrow half: the encoder + now emits the data count section (id 12, between element and code) + whenever `memory.init` or `data.drop` survive into the output. The spec + makes that section mandatory for those instructions — it exists so they + can be validated without scanning the data section — and loom preserved + the data section and the instructions while dropping the section that + makes them legal. + The systemic half, which is the one that generalises: every CLI write + path now runs the authoritative WebAssembly spec validator BEFORE + writing, using the same check `optimize_module` has applied since #257. + On failure the ORIGINAL input is written instead — but only after the + original is itself proven valid, so a `.wat` input or an + already-invalid one is never copied over the output path and presented + as a module — and the exit code is non-zero. Worst case becomes + unoptimized-but-valid output; success can no longer be printed over an + invalid artifact. + Asserted: (1) a module using `memory.init` and `data.drop` is emitted + valid AND carries a data count section — the second assertion matters + because validation alone would also pass if the instructions were + simply deleted; (2) across every valid in-tree wasm fixture, a + successful exit implies the artifact on disk validates; (3) fed bytes + that definitely do not validate, the gate REFUSES, does not write them, + and restores the original; (4) fed valid bytes it writes them + byte-for-byte — the positive control, without which a gate that refused + everything would pass (3). + Confirmed discriminating: with the encoder fix reverted, (1) fails on + "data count section required". + fields: + method: automated-test + acceptance-criteria: + - "Given a module using memory.init/data.drop, the output validates AND contains a data count section" + - "Given any valid fixture, exit 0 implies the written artifact validates" + - "Given bytes that do not validate, the gate refuses, writes the original instead, and exits non-zero" + - "Given valid bytes, the gate writes them unchanged" + - "Given an original that is not itself valid wasm, it is NOT written over the output path" + steps: + - run: | + cargo test --release -p loom-cli --test output_validation + - run: | + cargo test --release -p loom-cli --bin loom -- the_output_gate + status: verified + release: v1.4.1 + tags: [v141, encoder, honesty, no-silent-failures, safety] + links: + - type: verifies + target: REQ-3 + - type: verifies + target: REQ-12 + - type: verifies + target: REQ-1 From c47908f40d9ba798a241638ec5cf0010233d5bf5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 22 Aug 2026 10:47:25 +0200 Subject: [PATCH 2/2] fix(verify): #347 bound array-modelled memory operations, and refuse what cannot be verified (#350) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 97 of 100 real-world components exceeded a 60 s budget. One 463 KB meld-fused module ran past 455 s and was killed, while a structurally DENSER 1.13 MB ordinary module finished in 39 s — so it is not size, functions, blocks, loops or br_table, all of which the control exceeds. Root-caused by profiling, after bisecting the hang to a single pass: 14172 loom_core::optimize::inline_functions 13725 TranslationValidator::verify -> Z3_solver_check 97% 5290 smt::theory_array_base::propagate 40% 3849 assert_store_axiom2_core The cost is the solver's ARRAY theory — the memory model — instantiating store axioms PAIRWISE, so it grows quadratically in memory accesses per body. Only the inliner triggers it, for a structural reason: it is the one pass that concatenates callee bodies into a caller, and so the one pass that multiplies memory accesses per function. `LOOM_Z3_MAX_INSTRUCTIONS` bounds instruction count, which does not track that quantity at all. This bounds the one that does. I had a different hypothesis going in — the acyclic-CF executor from #219, which runs ONLY for inline_functions and fit the evidence perfectly. The profile disproved it. Worth recording, because a fix for that would have shipped and changed nothing. --- exceeding the bound REVERTS, unlike the instruction bound --- Returning Ok would accept a transform nothing verified, and at this bound that ships thousands of unproven transforms per module — the wrong direction for a charter whose rule is to skip rather than risk. Refusing costs optimization and costs nothing in safety, which is what makes a bound this aggressive defensible. The instruction bound still keeps; that inconsistency is left visible rather than quietly harmonised, since changing long-shipped behaviour belongs in its own change. Reverts are attributed (`/memory-ops-over-threshold`) and recorded in ONE place — recording at the refusal site as well would count each revert twice, which is the same class of defect as the mislabelled counter this branch series just fixed. --- tiny bodies are exempt, and that is not a nicety --- The naive bound broke #219. Measured: the seam-dissolution tests need a bound >= 4; the 463 KB module needs <= 2. Irreconcilable — and the first implementation silently regressed a shipped, silicon-validated capability, caught only because those tests exist. Exempting bodies at or below an instruction floor resolves it, because the seam inlines are tiny and the pathological ones are inlined-large. With the exemption: 45 s (from >455 s killed), seams intact, and slightly BETTER coverage than without it (49.8% vs 45.2%). --- what this is not --- Not a solution. It buys termination by declining the hardest obligations; they are discharged only when the memory model stops being the incumbent's array theory (#313 slice 5). Not a timeout, and not for want of trying: the solver's timeout IS wired (LOOM_Z3_TIMEOUT_MS, default 5000) and measurably does not bound this — at 100 ms the pass still exceeded 120 s, because the time goes into axiom instantiation, not the search a timeout guards. A wall-clock budget is also ruled out on principle: it would make which functions got verified depend on machine speed, so the same input could produce different output (REQ-14). Measured cost on a normal module: 0.47% larger output, 21% of the optimization gain foregone. loom-core --lib 539/539 (default AND both-mode), 410/410 --no-default-features, --test verification 47/47, loom-cli 21/21. Verifies TEST-347-MEMORY-OP-BOUND Refs #347, #219, #313, #331 Claude-Session: https://claude.ai/code/session_01RZof1M5HMBSYVZPeoT4MEn Co-authored-by: Claude Opus 5 --- loom-core/src/verify.rs | 318 +++++++++++++++++++++++++- safety/requirements/verification.yaml | 79 +++++++ 2 files changed, 396 insertions(+), 1 deletion(-) diff --git a/loom-core/src/verify.rs b/loom-core/src/verify.rs index 02dfc5e..5f28a24 100644 --- a/loom-core/src/verify.rs +++ b/loom-core/src/verify.rs @@ -88,6 +88,191 @@ pub struct VerificationSignatureContext { pub function_bodies: Vec>>, } +#[cfg(all(test, feature = "verification"))] +mod memory_bound_tests_347 { + use super::*; + + fn f(instrs: Vec) -> Function { + Function { + name: None, + signature: FunctionSignature { + params: vec![], + results: vec![], + }, + locals: vec![], + instructions: instrs, + } + } + + fn store() -> Instruction { + Instruction::I32Store { + offset: 0, + align: 2, + mem: 0, + } + } + + fn load() -> Instruction { + Instruction::I64Load { + offset: 0, + align: 3, + mem: 0, + } + } + + #[test] + fn counts_array_modelled_loads_and_stores() { + assert_eq!(count_array_memory_ops(&f(vec![])), 0); + assert_eq!( + count_array_memory_ops(&f(vec![store(), load(), Instruction::I32Const(1)])), + 2, + "only the memory accesses count, not the arithmetic beside them" + ); + } + + /// The count must see through structured control flow. A body that hides + /// its stores inside a block would otherwise slip under the bound and + /// reintroduce the hang the bound exists to prevent. + #[test] + fn counts_nested_bodies() { + let inner = Instruction::Block { + block_type: BlockType::Empty, + body: vec![store(), store()], + }; + let outer = Instruction::If { + block_type: BlockType::Empty, + then_body: vec![store(), inner], + else_body: vec![load()], + }; + assert_eq!( + count_array_memory_ops(&f(vec![outer, store()])), + 5, + "stores nested in block/if bodies must be counted" + ); + } + + /// Float and partial-width loads are deliberately NOT counted: they are + /// rejected earlier by `contains_unverifiable_instructions` and never + /// reach the array theory, so counting them would defer functions this + /// bound has no reason to defer. + #[test] + fn does_not_count_accesses_that_never_reach_the_array_theory() { + let float_store = Instruction::F64Store { + offset: 0, + align: 3, + mem: 0, + }; + let partial_load = Instruction::I32Load8U { + offset: 0, + align: 0, + mem: 0, + }; + assert_eq!( + count_array_memory_ops(&f(vec![float_store, partial_load])), + 0 + ); + } + + /// The #219 exemption, asserted as a property rather than left implicit in + /// the seam tests. + /// + /// The bound defers only bodies that are BOTH memory-dense and non-trivial. + /// Dropping the instruction floor makes the memory-seam and division-seam + /// dissolution tests fail — measured, not assumed: at a floor of 0 the + /// bound needs to be >= 4 for those to pass, while #347 needs <= 2, and + /// the two are irreconcilable without this exemption. + #[test] + fn a_tiny_memory_dense_body_is_exempt_from_the_bound() { + let tiny = f(vec![store(), store(), store(), store()]); + assert!( + count_array_memory_ops(&tiny) > DEFAULT_MAX_ARRAY_MEMORY_OPS, + "the fixture must exceed the memory bound, or it proves nothing" + ); + assert!( + count_function_instructions(&tiny) <= DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR, + "a body this small must fall under the instruction floor, which is \ + what keeps #219's seam-dissolution inlines verifiable" + ); + } + + /// The control for the exemption: a body that is memory-dense AND large + /// must NOT be exempt, or the bound would never fire and #347 returns. + #[test] + fn a_large_memory_dense_body_is_not_exempt() { + let mut instrs = vec![store(); 4]; + instrs.extend(std::iter::repeat_n( + Instruction::I32Const(0), + DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR + 1, + )); + let big = f(instrs); + assert!(count_array_memory_ops(&big) > DEFAULT_MAX_ARRAY_MEMORY_OPS); + assert!( + count_function_instructions(&big) > DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR, + "this body must clear the floor so the bound actually applies to it" + ); + } +} + +/// Count the memory accesses in a function that the SMT encoder models with +/// the solver's ARRAY theory (#347). +/// +/// This exists because `count_function_instructions` bounds the wrong +/// quantity. Profiling the meld-fused module that would not finish in 300 s +/// showed 97% of wall time inside `Z3_solver_check`, and **40% of the whole +/// process** inside `theory_array_base::propagate` → +/// `assert_store_axiom2_core`. Those are the array store axioms, and they are +/// instantiated PAIRWISE, so the cost grows quadratically in the number of +/// memory accesses reachable in one function body. +/// +/// Instruction count does not track that at all: a body well under +/// `LOOM_Z3_MAX_INSTRUCTIONS` can carry enough stores to be intractable, +/// which is exactly how a 463 KB module ran past 455 s while a structurally +/// denser 1.13 MB module finished in 39 s. +/// +/// Only the inliner triggers it in practice, and for a structural reason: it +/// is the one pass that concatenates callee bodies into a caller, so it is the +/// one pass that multiplies memory accesses PER FUNCTION. Every other pass +/// leaves that count roughly where it found it. +/// +/// Counted here are the accesses the encoder actually lowers to array +/// select/store. The float and partial-width loads that +/// `contains_memory_instructions` rejects are deliberately NOT counted: those +/// bail out earlier and never reach the array theory, so counting them would +/// defer functions this bound has no reason to defer. +#[cfg(feature = "verification")] +fn count_array_memory_ops(func: &Function) -> usize { + fn count_body(instrs: &[Instruction]) -> usize { + let mut n = 0; + for instr in instrs { + match instr { + Instruction::I32Load { .. } + | Instruction::I64Load { .. } + | Instruction::I32Store { .. } + | Instruction::I64Store { .. } + | Instruction::I32Store8 { .. } + | Instruction::I32Store16 { .. } + | Instruction::I64Store8 { .. } + | Instruction::I64Store16 { .. } + | Instruction::I64Store32 { .. } => n += 1, + Instruction::Block { body, .. } | Instruction::Loop { body, .. } => { + n += count_body(body); + } + Instruction::If { + then_body, + else_body, + .. + } => { + n += count_body(then_body); + n += count_body(else_body); + } + _ => {} + } + } + n + } + count_body(&func.instructions) +} + #[cfg(feature = "verification")] impl VerificationSignatureContext { /// Create a new empty context (for backwards compatibility) @@ -1527,6 +1712,39 @@ const MAX_LOOP_NESTING_DEPTH: usize = 1; /// When false, falls back to bounded unrolling only const ENABLE_K_INDUCTION: bool = true; +/// Default ceiling on array-modelled memory accesses per function before the +/// translation validator defers the obligation (#347). +/// +/// Chosen by measurement, not taste. Full-pipeline sweep on the meld-fused +/// module from #347 (463 KB, 1444 functions), which does not finish at all +/// today — killed at 455 s: +/// +/// | bound | wall clock | proven | +/// |-------|-----------|--------| +/// | 0 | 2 s | 21.6% | +/// | **2** | **45 s** | 45.0% | +/// | 4 | > 240 s | — | +/// +/// The knee between 2 and 4 is far sharper than a "quadratic in stores" +/// reading suggests, because memory is modelled BYTE-level: one `i64.store` +/// is eight array stores, so four of them already generate on the order of +/// 500 axiom pairs. +/// +/// That sharpness makes this number fragile — it is tuned on ONE module and +/// should be revisited against a corpus. It is recorded here rather than +/// hidden so the next person knows it is empirical and narrow, not derived. +/// +/// A wall-clock budget would generalise better and is deliberately NOT used: +/// which functions got verified would then depend on machine speed, so the +/// same input could produce different output, violating REQ-14 (deterministic +/// optimization output). A count is the only mechanism here that stays +/// deterministic. +const DEFAULT_MAX_ARRAY_MEMORY_OPS: usize = 2; + +/// Bodies at or below this instruction count are exempt from the memory-op +/// bound (#347). See the sweep in `TEST-347-MEMORY-OP-BOUND`. +const DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR: usize = 16; + /// K value for K-induction (number of base case iterations) /// Higher K = stronger base case but slower verification #[allow(dead_code)] @@ -2832,6 +3050,27 @@ thread_local! { const { std::cell::Cell::new(None) }; } +thread_local! { + /// Why the validator REFUSED an obligation, when the reason is more + /// specific than "the proof failed" — read back by `verify_or_revert` so + /// the revert is attributed in `--stats` instead of landing in the + /// undifferentiated per-pass bucket. + static DEFERRAL_REASON: std::cell::Cell> = + const { std::cell::Cell::new(None) }; +} + +/// Record why this obligation is being refused. +#[cfg(feature = "verification")] +fn note_deferral_reason(reason: &'static str) { + DEFERRAL_REASON.with(|c| c.set(Some(reason))); +} + +/// Read and clear the pending refusal reason. +#[cfg(feature = "verification")] +fn take_deferral_reason() -> Option<&'static str> { + DEFERRAL_REASON.with(|c| c.take()) +} + /// Record that this attempt is about to be ACCEPTED without a proof. #[cfg(feature = "verification")] fn note_unproven_acceptance(reason: &'static str) { @@ -3396,6 +3635,71 @@ impl TranslationValidator { return Ok(()); } + // #347 — MEMORY-OPERATION bound, beside the instruction bound above. + // + // The instruction bound cannot see the cost that actually blows up + // here. Profiling a meld-fused module that ran past 455 s put 97% of + // wall time in `Z3_solver_check` and 40% of the whole process in the + // solver's array theory instantiating store axioms PAIRWISE — a cost + // quadratic in memory accesses per body, which inlining multiplies by + // concatenating callees into their caller. + // + // Two things this deliberately is NOT: + // + // * It is not a fix. It buys termination by declining to verify the + // hardest inlines, so it trades proof coverage for completing at + // all. Those obligations are only really discharged when the + // memory model stops being the incumbent's array theory (#313 + // slice 5). The honest framing is a bound, not a solution. + // * It is not a timeout. The solver's own timeout IS wired + // (`LOOM_Z3_TIMEOUT_MS`, default 5000) and measurably does not + // bound this: at 100 ms the pass still exceeded 120 s, because the + // time goes into axiom instantiation and internalisation rather + // than the search the timeout guards. + // + // The transform is KEPT, exactly as with the instruction bound, and + // recorded as kept-without-proof so `--stats` reports it against a + // denominator instead of it vanishing (#331). A deferral nobody can + // see is the failure mode this project keeps finding. + let max_memory_ops: usize = std::env::var("LOOM_Z3_MAX_MEMORY_OPS") + .ok() + .and_then(|s| s.parse().ok()) + .unwrap_or(DEFAULT_MAX_ARRAY_MEMORY_OPS); + let n_memory_ops = + count_array_memory_ops(&self.original).max(count_array_memory_ops(optimized)); + // Tiny bodies are exempt regardless of memory-op count: they are + // cheap for the solver whatever they touch, and they are where the + // #219 seam-dissolution inlines live. Bounding them would trade a + // shipped, silicon-validated capability for nothing measurable. + let memory_bound_floor: usize = std::env::var("LOOM_Z3_MEMORY_BOUND_FLOOR") + .ok() + .and_then(|s| s.parse().ok()) + .unwrap_or(DEFAULT_MEMORY_BOUND_INSTRUCTION_FLOOR); + if n_memory_ops > max_memory_ops && n_instr > memory_bound_floor { + // REVERT, not keep — deliberately unlike the instruction bound + // directly above. + // + // Returning `Ok(())` would accept a transform nothing verified, + // and at a default this low that would ship thousands of unproven + // transforms per module: the wrong direction for a charter whose + // rule is "skip the function rather than risk incorrect + // optimization". Refusing costs optimization on memory-dense + // inlines and costs nothing in safety, which is what makes a bound + // this aggressive defensible at all. + // + // The instruction bound above still keeps. That inconsistency is + // real and is left visible rather than quietly harmonised here — + // changing long-shipped behaviour belongs in its own change. + note_deferral_reason("memory-ops-over-threshold"); + return Err(anyhow!( + "{}: {} array-modelled memory operations exceeds the limit of {} \ + (#347) - optimization rejected (unproven)", + self.pass_name, + n_memory_ops, + max_memory_ops + )); + } + // PR-C (#219) M3.2: precise acyclic-CF fast-path for the inliner. The // main encoder models br_table approximately and a br_table callee is // not straight-line-by-body-modelable, so it cannot prove `call F` @@ -3483,6 +3787,8 @@ impl TranslationValidator { /// Reverts are recorded in `crate::stats::record_revert(pass_name)` so /// callers can observe how often verification rejects a transform. pub fn verify_or_revert(&self, func: &mut Function) -> bool { + // Clear any stale note before the attempt we are about to classify. + let _ = take_deferral_reason(); match self.verify(func) { Ok(()) => true, Err(e) => { @@ -3490,7 +3796,17 @@ impl TranslationValidator { "{}: reverting function: {}", self.pass_name, e )); - crate::stats::record_revert(&self.pass_name); + // Attribute the revert when the validator said something more + // specific than "the proof failed". Recorded HERE and only + // here: recording at the refusal site too would count one + // revert twice, and an inflated revert total is the same class + // of defect as the mislabelled one this replaced. + match take_deferral_reason() { + Some(reason) => { + crate::stats::record_revert(&format!("{}/{}", self.pass_name, reason)) + } + None => crate::stats::record_revert(&self.pass_name), + } func.instructions = self.original.instructions.clone(); func.locals = self.original.locals.clone(); false diff --git a/safety/requirements/verification.yaml b/safety/requirements/verification.yaml index fc52a2c..77ebfbe 100644 --- a/safety/requirements/verification.yaml +++ b/safety/requirements/verification.yaml @@ -1185,3 +1185,82 @@ artifacts: target: REQ-12 - type: verifies target: REQ-1 + + # ============================================================================ + # #347 — v1.4.1: bound the quantity that actually drives solver cost. + # + # 97 of 100 real-world components exceeded a 60 s budget; one 463 KB fused + # module ran past 455 s and was killed, while a structurally denser 1.13 MB + # ordinary module finished in 39 s. Profiling put 97% of wall clock inside + # the solver and 40% of the whole process inside its ARRAY theory + # instantiating store axioms pairwise. Instruction count — the only quantity + # loom bounded — does not track that at all. + # ============================================================================ + + - id: TEST-347-MEMORY-OP-BOUND + type: feature + title: the translation validator bounds array-modelled memory operations, and refuses rather than ships what it declines to verify (#347) + description: > + Verifies the memory-operation bound that makes store-dense inlines + terminate. The cost driver is the solver's array theory, whose store + axioms are instantiated pairwise, so cost grows quadratically in memory + accesses per body — a quantity inlining multiplies by concatenating + callee bodies into their caller, which is why only the inliner triggers + it. + Two design decisions are recorded because both were reached by + measurement and both could reasonably have gone the other way. + FIRST, exceeding the bound REVERTS rather than keeps. The existing + instruction bound keeps, and copying that here would have shipped + thousands of unproven transforms per module at this bound — the wrong + direction for a charter whose rule is to skip rather than risk. Refusing + costs optimization and costs nothing in safety. The instruction bound's + keep-behaviour is left untouched and the inconsistency stated rather + than quietly harmonised. + SECOND, tiny bodies are EXEMPT. Without the exemption the bound must be + 2 or lower for the 463 KB module to finish, while #219's memory-seam and + division-seam dissolution require 4 or higher — irreconcilable, and the + naive bound silently broke a shipped, silicon-validated capability. The + exemption resolves it: measured 45 s (from >455 s killed) with the seam + intact, and slightly BETTER proof coverage than without it (49.8% vs + 45.2%). + A wall-clock budget would generalise better and is deliberately not + used: which functions got verified would depend on machine speed, so the + same input could produce different output, violating REQ-14. A count is + the only mechanism here that stays deterministic. The solver's own + timeout is wired and measurably does NOT bound this — at 100 ms the pass + still exceeded 120 s, because the cost is axiom instantiation rather + than the search a timeout guards. + Asserted: (1) the counter counts array-modelled loads and stores; (2) it + sees through block/if bodies, so a body cannot hide its stores under the + bound; (3) it does NOT count float or partial-width accesses, which bail + earlier and never reach the array theory; (4) a tiny memory-dense body + is exempt — the #219 property, asserted directly rather than left + implicit in the seam tests; (5) a LARGE memory-dense body is not exempt, + the control without which the bound could never fire. + This is a BOUND, not a solution: it buys termination by declining the + hardest obligations. They are discharged only when the memory model + stops being the incumbent's array theory (#313 slice 5). + fields: + method: automated-test + acceptance-criteria: + - "Given a body with nested stores, all of them are counted" + - "Given float/partial-width accesses, none are counted" + - "Given a tiny memory-dense body, the bound does NOT apply (#219 seams keep dissolving)" + - "Given a large memory-dense body, the bound DOES apply" + - "Given the bound fires, the transform is REVERTED and the revert is attributed by reason" + - "Given the #347 module at default settings, the full pipeline completes and the output validates" + steps: + - run: | + cargo test --release -p loom-core --features verification --lib memory_bound_tests_347 + - run: | + cargo test --release -p loom-core --features verification --lib -- seam_fully_dissolves + status: verified + release: v1.4.1 + tags: [v141, verification, performance, solver-migration] + links: + - type: verifies + target: REQ-5 + - type: verifies + target: REQ-14 + - type: verifies + target: REQ-3