From 08fd5dc4cb6d939c26f3acccebca82dddef8f293 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 27 Jun 2026 08:23:51 +0200 Subject: [PATCH] test(vcr-mem): pin scry 2.5.0 FEAT-039 open-world reachability soundness (#383, #242) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Issue-hunt pass external signal: scry v2.5.0 released (seen set was v2.3.0). Both new minors are no-API-change updates — v2.4.0 (FEAT-038) models memory.size/grow; v2.5.0 (FEAT-039) is a SOUNDNESS fix to `reachable_from_exports`, the exact "sound superset" synth's VCR-MEM-001 layer-1 shadow-stack pruning consumes. Triaged + validated: - Bumped the lockfile scry-sai-core 2.3.0 -> 2.5.0; the consumed surface (max_stack_bytes / function_summaries[].recursive / reachable_from_exports) is unchanged, so scry_proves_msgq_shadow_stack_budget_383 stays GREEN — the "2.x transparent" claim is tested on 2.5.0, not just asserted. - NEW scry_reachable_superset_is_open_world_sound_383_feat039: pins the FEAT-039 property synth depends on. A function reachable ONLY via an escaped funcref (exported funcref table, never called in-module) MUST be in the superset — under scry <=2.4.0 it was dropped, so pruning the complement would under-reserve a genuinely-reachable function's shadow stack. The closed-world contrast (same func index pruned when escape-free) keeps it non-vacuous and makes it discriminate: it would FAIL on pre-FEAT-039 scry. A future scry regression now reddens synth's gate instead of silently re-introducing the under-reservation. Frozen-safe — scry stays a DEV-dependency (no production pull, no codegen); frozen anchors 3/3 green, fmt + clippy clean. Co-Authored-By: Claude Opus 4.8 --- Cargo.lock | 24 +++--- crates/synth-cli/Cargo.toml | 8 +- .../tests/scry_shadow_stack_budget.rs | 79 ++++++++++++++++++- 3 files changed, 93 insertions(+), 18 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0688b6c..56b3480 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1799,15 +1799,15 @@ dependencies = [ [[package]] name = "scry-sai-bits" -version = "2.3.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99220601aa017b9d725d825837f01db2b1c3044b06ebe2eb5bd150161e650b1d" +checksum = "a749c9b7f213d76bcd20a00caed41c7365bb0e044f0d7e407cd0561ac4d6f8f0" [[package]] name = "scry-sai-core" -version = "2.3.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23c112b0ff57cf790e5b7c5077929c91639b4dc4a97929c0df4180d14f2a460d" +checksum = "cf1a9e14700890ba8812cfee5ae59e9d4c7e44434694c8617721ca35ed9b043d" dependencies = [ "scry-sai-bits", "scry-sai-interval", @@ -1820,27 +1820,27 @@ dependencies = [ [[package]] name = "scry-sai-interval" -version = "2.3.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83eac224c75f13bb39c244ad5615a7fc1a4e25203fe8ea31450155f0a865dc46" +checksum = "486d13ed454c233a42cfcf804a35c1a09a5ab2f8ad3b0169f2f601e4e3627f36" [[package]] name = "scry-sai-octagon" -version = "2.3.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7c7b4e8221a882a18638ae9ee4b82bcea3717d2dca82150ac969f4219d4cf645" +checksum = "86ef476091d53c8cc6ced2bbc5d302ec983b328366aa988230c6d2204f4c24b6" [[package]] name = "scry-sai-provenance" -version = "2.3.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "16b21313e6683a03b557c794d1925b0979005e298be0a0ead1e7d676b8b29ad6" +checksum = "b19071e291644ddb6017e3926eb13c8a6188857461592b6cb732b3cbe2df5926" [[package]] name = "scry-sai-taint" -version = "2.3.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7006fa9dcb6e57b90fff10a014f68bab20a294f0ed8e4a9f17d0e4160ceabf17" +checksum = "b255301d93308b14f235da0b53844042d3f73f2f1433411ee29051a3530e782f" [[package]] name = "semver" diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml index c9b7588..472786d 100644 --- a/crates/synth-cli/Cargo.toml +++ b/crates/synth-cli/Cargo.toml @@ -73,6 +73,10 @@ gimli = { version = "0.33", default-features = false, features = ["read", "std"] # but synth's consumed surface (call_graph / function_summaries / stack_usage / # reachable_from_exports / operand_stack) is unchanged and additive-only, so the # bump is transparent here. See scry#63 / scry v2.0.0. Empirically re-verified -# against scry v2.3.0 (2026-06-27, lockfile bumped) — scry_shadow_stack_budget -# stays GREEN, so the "transparent" claim is tested, not just asserted. +# against scry v2.3.0 then v2.5.0 (2026-06-27, lockfile bumped) — +# scry_shadow_stack_budget stays GREEN, so the "transparent" claim is tested, not +# just asserted. v2.4.0 (FEAT-038) models memory.size/grow; v2.5.0 (FEAT-039) +# makes reachable_from_exports sound in the open world (escaped funcref) — the +# superset synth's shadow-stack pruning relies on; pinned by +# scry_reachable_superset_is_open_world_sound_383_feat039. scry-sai-core = "2.0" diff --git a/crates/synth-cli/tests/scry_shadow_stack_budget.rs b/crates/synth-cli/tests/scry_shadow_stack_budget.rs index c5c2a1a..a47fb5c 100644 --- a/crates/synth-cli/tests/scry_shadow_stack_budget.rs +++ b/crates/synth-cli/tests/scry_shadow_stack_budget.rs @@ -3,12 +3,22 @@ //! Proves, in CI against the REAL gust-family module, that synth can obtain a //! SOUND worst-case shadow-stack budget from scry (`scry-sai-core`, the crates.io //! library finalized in scry#51 / scry PR #53). First validated on v1.12, then -//! across the SCPV v3 major bump (v2.x); re-verified GREEN on **scry v2.3.0** -//! (2026-06-27) — the consumed surface (`stack_usage.max_stack_bytes`, +//! across the SCPV v3 major bump (v2.x); re-verified GREEN on **scry v2.3.0** then +//! **v2.5.0** (2026-06-27) — the consumed surface (`stack_usage.max_stack_bytes`, //! `function_summaries[].recursive`, `reachable_from_exports`) is unchanged, so //! the "2.x bump is transparent" claim in `Cargo.toml` is empirically backed, not -//! just asserted. This is the layer-2 "proof the budget is sufficient" half of -//! #383 — the half scry owns: +//! just asserted. scry v2.4.0/v2.5.0 are behavioral-precision + soundness updates +//! with no API/contract change: v2.4.0 models `memory.size`/`grow` (FEAT-038); +//! v2.5.0 (FEAT-039) makes `reachable_from_exports` sound in the OPEN world — a +//! function reachable only via an ESCAPED funcref (exported table / exported +//! funcref global / passed to an import) is no longer dropped. That value is +//! exactly the "sound superset" synth's layer-1 shadow-stack pruning relies on: +//! under <=2.4.0 such a module could prune a genuinely-reachable function and +//! UNDER-reserve. `scry_reachable_superset_is_open_world_sound_383_feat039` below +//! pins that soundness property in synth's CI (with a closed-world dead-function +//! contrast so it is non-vacuous), so a future scry regression of FEAT-039 reddens +//! synth's gate rather than silently re-introducing the under-reservation. This is +//! the layer-2 "proof the budget is sufficient" half of #383 — the half scry owns: //! //! - layer-1 (synth-side): the ELF `.bss` retarget mechanics that consume the //! budget — still silicon-gated on gale's `--stack-first` answer. @@ -72,3 +82,64 @@ fn scry_proves_msgq_shadow_stack_budget_383() { "reachable_from_exports is the sound superset synth prunes against" ); } + +/// VCR-MEM-001 (#383) — pin scry v2.5.0's FEAT-039 open-world soundness fix for +/// the `reachable_from_exports` superset synth's layer-1 shadow-stack pruning +/// consumes. A function reachable ONLY via an escaped funcref (here: present in +/// an EXPORTED funcref table, never called in-module) is host-dispatchable, so it +/// MUST be in the sound superset — under scry <=2.4.0 it was wrongly omitted, and +/// pruning the complement would drop a genuinely-reachable function and +/// UNDER-reserve its shadow stack. Wiring this into synth's CI means a future scry +/// regression of FEAT-039 reddens synth's gate instead of silently re-introducing +/// the under-reservation. The closed-world dead-function contrast keeps the test +/// non-vacuous: it proves the superset still PRUNES (it is not trivially "all"). +#[test] +fn scry_reachable_superset_is_open_world_sound_383_feat039() { + let cfg = || AnalysisConfig { + widening_threshold: None, + emit_diagnostics: false, + taint_policy: None, + }; + + // ESCAPE: func 1 is only in an exported funcref table — never called by the + // exported `main`. Host code can `call_indirect` it through the table. + let escaping = wat::parse_str( + r#"(module + (table (export "t") 1 funcref) + (elem (i32.const 0) 1) + (func (export "main")) + (func (result i32) i32.const 7))"#, + ) + .expect("valid wat"); + let r = analyze(escaping, cfg()).expect("scry analyzes the escaping module"); + assert!( + r.reachable_from_exports.contains(&1), + "FEAT-039: a function in an EXPORTED funcref table is host-dispatchable ⇒ \ + must be in the sound superset synth prunes against (got {:?}) — under \ + scry <=2.4.0 this was dropped and synth would under-reserve", + r.reachable_from_exports + ); + + // CONTRAST (non-vacuity): a closed, escape-free module — func 1 is neither + // exported, called, nor address-taken, so the superset still PRUNES it. If + // this stopped holding, the superset would be trivially "everything" and the + // escape assertion above would prove nothing. + let closed = wat::parse_str( + r#"(module + (func (export "main")) + (func (result i32) i32.const 7))"#, + ) + .expect("valid wat"); + let r2 = analyze(closed, cfg()).expect("scry analyzes the closed module"); + assert!( + r2.reachable_from_exports.contains(&0), + "the exported root is reachable (got {:?})", + r2.reachable_from_exports + ); + assert!( + !r2.reachable_from_exports.contains(&1), + "a non-exported, uncalled, address-not-taken function MUST be pruned in a \ + closed escape-free module — else the superset is vacuously 'all' (got {:?})", + r2.reachable_from_exports + ); +}