diff --git a/BUILD.bazel b/BUILD.bazel index 52f2460..0abd3f4 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -1,33 +1,30 @@ """Top-level Bazel package for scry. -v1.1 (FEAT-013 / DD-011): the distributable `//:scry` is the -self-contained analyzer component itself, copied to the stable name -`scry.wasm`. Through v1.0 this was a `wac_compose` of the analyzer + -lattice components, but wac's `--import-dependencies` left the analyzer -as a root-level component import — a hollow ~2.6 KB shell wasmtime 45 -rejects ("root-level component imports are not supported"), so the -composed `analyze()` could never run (the v1.0.1 open finding). Now that -the analyzer links the abstract-domain algebra as Rust crate deps -(scry-interval / scry-taint / scry-octagon) it imports only WASI and -runs standalone, so the distributable is simply that component — no wac -composition needed. +The two component crates live under //crates/. The composed +distributable artifact is `//:scry` (produced by wac_compose). -The wasm-lattice component still builds and exports the `domain` -interface (the DD-008 / DD-004 cross-component dogfood), but it is no -longer part of the distributable or on the analyzer's execution path. +A meld_fuse-based dogfood variant lands at //:scry_fused in a +later milestone — that target exercises meld on scry's own build +artifacts, validating the meld fusion path on a real PulseEngine +component graph. For v0.1, wac_compose is enough to produce a +runnable component. """ +load("@rules_wasm_component//wac:defs.bzl", "wac_compose") + package(default_visibility = ["//visibility:public"]) -# The distributable: the self-contained analyzer component, copied to the -# stable filename `scry.wasm` that release.yml and the host harness -# (crates/scry-host-tests) read. The bare `scry_analyzer_component` label -# emits the core module (`_wasm_base.wasm`); the *packaged component* is -# the `_release` profile target, which emits `scry_analyzer_component.wasm` -# (~2.5 MB, analyzer embedded, WASI-only imports, validates). Copy that. -genrule( +# Compose the two scry components into a single distributable Wasm +# component. wac auto-wires the `pulseengine:wasm-lattice/domain` +# interface from the lattice component into the analyzer's matching +# import. The composed component exports the analyzer's `analyzer` +# interface as its main export. +wac_compose( name = "scry", - srcs = ["//crates/scry-analyzer:scry_analyzer_component_release"], - outs = ["scry.wasm"], - cmd = "cp $(location //crates/scry-analyzer:scry_analyzer_component_release) $@", + components = { + "//crates/wasm-lattice:wasm_lattice_component": "lattice", + "//crates/scry-analyzer:scry_analyzer_component": "analyzer", + }, + composition_file = "composition.wac", + profile = "release", ) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4cb4357..a86f1fe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,58 +7,6 @@ Versioning: [SemVer 2.0](https://semver.org/spec/v2.0.0.html). ## [Unreleased] -## [1.1.0] — 2026-05-30 - -Headline: **the shipped artifact is finally the real one.** v1.1 closes -the composition gap recorded as the v1.0.1 open finding (FEAT-013 / -DD-011): through v1.0 the composed `//:scry` was a ~4.6 KB hollow shell — -wac's `--import-dependencies` left both sub-components as root-level -component imports, which wasmtime 45 rejects, so `analyze()` could never -run and analyzer source never reached the shipped binary. v1.1 makes the -analyzer self-contained and executable. - -### Added / Changed - -- **`crates/scry-interval`** — new pure, zero-dep crate holding the - interval + region-memory algebra, extracted from `wasm-lattice` - (byte-identical transfer functions; soundness mechanized in - `proofs/rocq/Soundness.v` + `Region.v`). Same dual-compile pattern as - scry-octagon / scry-taint / scry-provenance. -- **Self-contained analyzer (FEAT-013 / DD-011).** The analyzer now links - the interval/region (scry-interval), taint (scry-taint), and octagon - (scry-octagon) algebra as Rust crate deps via a thin local `domain` - module, instead of importing `pulseengine:wasm-lattice/domain` over WIT. - The `scry` world drops the cross-component import (the `interval` record - is declared locally), so the analyzer component imports only WASI and - runs standalone. The wasm-lattice component still exports the same - `domain` interface (DD-008 dogfood), now off the analyzer's execution - path. `SCRY_VERSION` → 1.1.0. -- **`//:scry` is the analyzer component itself, not a `wac_compose`.** The - actual mechanism that closes the gap: `wac compose` (as the - `wac_compose` rule invokes it, with `--import-dependencies`) emits a - component that *imports* `pulseengine:scry` at the root rather than - embedding it — the hollow 2,669-byte shell wasmtime rejects. Since the - analyzer is now self-contained, `//:scry` is a `genrule` that copies the - `scry_analyzer_component` (2,510,923 bytes — analyzer embedded) to the - stable `scry.wasm` name release.yml and the host harness read. 0 - non-WASI imports, `wasm-tools validate` ok. -- **Live runnable gate (`feat013_live_analyze_gate`).** A no-skip host - test that loads the shipped component and invokes the live `analyze()` - on a real module — the process exits non-zero if it cannot run. Prior - to v1.1 it would have failed on the wasmtime root-level-import - rejection; it now passes. - -### Falsifiable kill-criterion - -Two binary properties, both now true (were both false through v1.0.1): -1. **AC#1** — a source edit to the analyzer changes the composed - artifact's SHA-256 (the version bump moved it off the frozen - `30f8d4e2…` hash that was identical across v0.9–v1.0.1). -2. **AC#2** — the live `analyze()` runs in wasmtime 45 on the shipped - `//:scry` (`feat013_live_analyze_gate`, no skip path, exit 0). -If either regresses, the gap has reopened. - - ## [1.0.1] — 2026-05-30 ### Fixed @@ -891,8 +839,7 @@ falsifier. See git history for pre-v0.1 work (initial scope-out + DD-002 closure in PR #2). -[Unreleased]: https://github.com/pulseengine/scry/compare/v1.1.0...HEAD -[1.1.0]: https://github.com/pulseengine/scry/releases/tag/v1.1.0 +[Unreleased]: https://github.com/pulseengine/scry/compare/v1.0.1...HEAD [1.0.1]: https://github.com/pulseengine/scry/releases/tag/v1.0.1 [1.0.0]: https://github.com/pulseengine/scry/releases/tag/v1.0.0 [0.9.0]: https://github.com/pulseengine/scry/releases/tag/v0.9.0 diff --git a/Cargo.lock b/Cargo.lock index 0c87ec3..4824e1b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1828,10 +1828,7 @@ name = "scry-analyzer" version = "0.1.0" dependencies = [ "bitflags", - "scry-interval", - "scry-octagon", "scry-provenance", - "scry-taint", "sha2", "wasmparser 0.247.0", ] @@ -1853,10 +1850,6 @@ dependencies = [ "wat", ] -[[package]] -name = "scry-interval" -version = "0.1.0" - [[package]] name = "scry-octagon" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index c360365..8ac36b2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -26,7 +26,6 @@ members = [ "crates/scry-provenance", "crates/scry-taint", "crates/scry-octagon", - "crates/scry-interval", "crates/scry-host-tests", ] diff --git a/composition.wac b/composition.wac index 06ca618..64ecf5f 100644 --- a/composition.wac +++ b/composition.wac @@ -1,19 +1,13 @@ -// WAC composition for scry. -// -// v1.1 (FEAT-013 / DD-011): the analyzer is self-contained — it links -// the interval/region/taint/octagon algebra as Rust crate deps instead -// of importing `pulseengine:wasm-lattice/domain` over WIT. So the -// composition is now just the analyzer itself: no lattice instantiation, -// no `domain` wiring. Its only imports are WASI, which flow through to -// the outer composed component's import list, so wasmtime can -// instantiate and run it (closing the v1.0.1 root-level-import finding). -// -// The wasm-lattice component still builds and exports `domain` (the -// DD-008 / DD-004 cross-component dogfood), but it is no longer on the -// analyzer's execution path, so it is not part of this composition. +// WAC composition for scry v0.1. +// Wires the lattice component's `domain` interface to the analyzer +// component's `domain` import; exports the analyzer's `analyzer` +// interface as the composed component's main export. Other imports +// (WASI; auto-injected by wit-bindgen's runtime) flow through to +// the outer composed component's import list. package pulseengine:scry-composed@0.1.0; -let analyzer = new pulseengine:scry { ... }; +let lattice = new pulseengine:wasm-lattice { ... }; +let analyzer = new pulseengine:scry { domain: lattice.domain, ... }; export analyzer as main; diff --git a/crates/scry-analyzer/BUILD.bazel b/crates/scry-analyzer/BUILD.bazel index 5c8646e..a905f9b 100644 --- a/crates/scry-analyzer/BUILD.bazel +++ b/crates/scry-analyzer/BUILD.bazel @@ -1,12 +1,6 @@ -"""scry-analyzer — the scry abstract interpreter as a Wasm component. - -v1.1 (FEAT-013 / DD-011): self-contained. The interval/region/taint/ -octagon algebra is linked as Rust crate dependencies (scry-interval, -scry-taint, scry-octagon, scry-provenance), NOT imported over WIT, so -the composed component imports only WASI and runs standalone in -wasmtime — closing the v1.0.1 open finding. The wasm-lattice component -still exports the same `domain` interface (DD-008 dogfood), but it is no -longer on the analyzer's execution path. +"""scry-analyzer — the v0.1 interval-domain abstract interpreter as +a Wasm component. Imports the `pulseengine:wasm-lattice/domain` +interface from `//crates/wasm-lattice` (per DD-008's dogfood story). """ load("@rules_wasm_component//rust:defs.bzl", "rust_wasm_component_bindgen") @@ -14,16 +8,17 @@ load("@rules_wasm_component//wit:defs.bzl", "wit_library") package(default_visibility = ["//visibility:public"]) -# WIT interface this component exports. v1.1: no `deps` — the world no -# longer imports pulseengine:wasm-lattice (the `interval` record is -# declared locally in scry.wit), so wit-bindgen needs no cross-package -# resolution and the composed component carries no root-level component -# import for wasmtime to reject. +# WIT interface this component exports — declares the cross-package +# import of pulseengine:wasm-lattice via deps. The Bazel rule builds +# the proper `deps/` directory layout under bazel-bin so wit-bindgen +# can resolve `use pulseengine:wasm-lattice/domain@0.1.0` at codegen +# time. wit_library( name = "scry_analyzer_wit", package_name = "pulseengine:scry@0.1.0", srcs = ["wit/scry.wit"], world = "scry", + deps = ["//crates/wasm-lattice:wasm_lattice_wit"], ) # The Wasm component. The `_bindings` crate produced by the macro is @@ -50,13 +45,5 @@ rust_wasm_component_bindgen( # wasm32-wasip2 alongside this component; provides the # `component-provenance` section decode + projection lookup. "//crates/scry-provenance:scry_provenance", - # FEAT-013 (DD-011): the abstract-domain algebra as crate deps, - # replacing the WIT `pulseengine:wasm-lattice/domain` import so the - # analyzer is self-contained and executable. scry-interval is the - # interval+region domain (extracted from wasm-lattice); scry-taint - # the security-label domain; scry-octagon the relational domain. - "//crates/scry-interval:scry_interval", - "//crates/scry-taint:scry_taint", - "//crates/scry-octagon:scry_octagon", ], ) diff --git a/crates/scry-analyzer/Cargo.toml b/crates/scry-analyzer/Cargo.toml index 36eccfd..0f2a1b0 100644 --- a/crates/scry-analyzer/Cargo.toml +++ b/crates/scry-analyzer/Cargo.toml @@ -31,11 +31,3 @@ sha2 = { workspace = true } # //crates/scry-provenance:scry_provenance rust_library target; this # path entry keeps the cargo metadata coherent. scry-provenance = { path = "../scry-provenance" } - -# FEAT-013 (DD-011): abstract-domain algebra as crate deps, replacing the -# WIT `pulseengine:wasm-lattice/domain` import so the analyzer is -# self-contained and executable in wasmtime. Bazel wires the matching -# //crates/* rust_library targets; these path entries keep cargo coherent. -scry-interval = { path = "../scry-interval" } -scry-taint = { path = "../scry-taint" } -scry-octagon = { path = "../scry-octagon" } diff --git a/crates/scry-analyzer/src/lib.rs b/crates/scry-analyzer/src/lib.rs index 5d36fdc..a4c51dd 100644 --- a/crates/scry-analyzer/src/lib.rs +++ b/crates/scry-analyzer/src/lib.rs @@ -169,13 +169,7 @@ use scry_analyzer_component_bindings::exports::pulseengine::scry::analyzer::{ LocalInvariant, ProgramPoint, SecurityLabel, SoundnessTag, TaintFinding, TaintFindingKind, TaintPolicy, }; -// v1.1 (FEAT-013 / DD-011): the abstract-domain algebra is now a Rust -// crate dependency, not a WIT cross-component import. `domain` is a local -// module (defined below) that delegates to the pure scry-interval / -// scry-taint / scry-octagon crates and re-exports their types — so all -// existing `domain::*` call sites compile unchanged, but the analyzer no -// longer imports `pulseengine:wasm-lattice/domain` and runs standalone. -use domain::Interval; +use scry_analyzer_component_bindings::pulseengine::wasm_lattice::domain::{self, Interval}; // The pure meld<->scry boundary crate (DD-002 / FEAT-002): the binary // format of the `component-provenance` custom section plus the // projection lookup. Aliased to avoid colliding with the WIT-binding @@ -183,83 +177,9 @@ use domain::Interval; // field copy at the point we build the WIT `provenance` field. use scry_provenance::ComponentOrigin as ProvOrigin; -/// The abstract-domain interface the analyzer dispatches every transfer -/// function through. Through v1.0 this was the WIT-generated bindings for -/// the imported `pulseengine:wasm-lattice/domain` interface; as of v1.1 -/// (FEAT-013) it is a thin local module over the pure domain crates, so -/// the analyzer is self-contained and executable (DD-011). The surface -/// (types + free fns) is identical to the old WIT binding, so the ~44 -/// `domain::*` call sites are unchanged. -mod domain { - // The currency interval type is the WIT-generated `interval` record - // the analyzer's `abstract-value` / `region-pointer-payload` are - // built from. The pure `scry_interval::Interval` is field-identical - // but a distinct type, so we convert at each crate-call boundary - // (a trivial `{lo, hi}` copy). `Region` is never stored into an - // `abstract-value` (the analyzer synthesises it only for the - // bounds-check soundness story), so it can be the pure type directly. - pub use scry_analyzer_component_bindings::exports::pulseengine::scry::analyzer::Interval; - pub use scry_interval::Region; - pub use scry_taint::Label; - - #[inline] - fn to_pure(i: Interval) -> scry_interval::Interval { - scry_interval::Interval { lo: i.lo, hi: i.hi } - } - #[inline] - fn from_pure(i: scry_interval::Interval) -> Interval { - Interval { lo: i.lo, hi: i.hi } - } - - // ── Interval lattice + transfer functions ────────────────────── - pub fn top() -> Interval { - from_pure(scry_interval::top()) - } - pub fn constant_i32(c: i32) -> Interval { - from_pure(scry_interval::constant_i32(c)) - } - pub fn constant_i64(c: i64) -> Interval { - from_pure(scry_interval::constant_i64(c)) - } - pub fn join(a: Interval, b: Interval) -> Interval { - from_pure(scry_interval::join(to_pure(a), to_pure(b))) - } - pub fn i32_add(a: Interval, b: Interval) -> Interval { - from_pure(scry_interval::i32_add(to_pure(a), to_pure(b))) - } - pub fn i32_sub(a: Interval, b: Interval) -> Interval { - from_pure(scry_interval::i32_sub(to_pure(a), to_pure(b))) - } - pub fn i32_mul(a: Interval, b: Interval) -> Interval { - from_pure(scry_interval::i32_mul(to_pure(a), to_pure(b))) - } - - // ── Region-memory domain ─────────────────────────────────────── - pub fn region_create(region_id: u32) -> Region { - scry_interval::region_create(region_id) - } - pub fn region_offset(r: Region, delta: Interval) -> Region { - scry_interval::region_offset(r, to_pure(delta)) - } - - // ── Security-label (taint) domain ────────────────────────────── - pub fn label_bottom() -> Label { - scry_taint::bottom() - } - pub fn label_top() -> Label { - scry_taint::top() - } - pub fn label_leq(a: Label, b: Label) -> bool { - scry_taint::leq(a, b) - } - pub fn label_join(a: Label, b: Label) -> Label { - scry_taint::join(a, b) - } -} - struct Component; -const SCRY_VERSION: &str = "1.1.0"; +const SCRY_VERSION: &str = "1.0.1"; const INVARIANT_SCHEMA_URL: &str = "https://pulseengine.eu/scry-invariants/v1"; /// Default Wasm linear-memory page size (64 KiB). diff --git a/crates/scry-analyzer/wit/scry.wit b/crates/scry-analyzer/wit/scry.wit index 6b6f9ee..b8b14f1 100644 --- a/crates/scry-analyzer/wit/scry.wit +++ b/crates/scry-analyzer/wit/scry.wit @@ -1,34 +1,17 @@ // scry — sound abstract interpretation for WebAssembly. // -// v1.1 WIT world (FEAT-013 / DD-011). Hand-derived from spar/scry.aadl -// (see DD-010). Through v1.0 this world IMPORTED the `domain` interface -// from `pulseengine:wasm-lattice`; wac's `--import-dependencies` left -// that as a root-level component import, which wasmtime 45 rejects, so -// the composed `analyze()` could never run (the v1.0.1 open finding). -// -// v1.1 makes the analyzer self-contained: the interval/region algebra is -// now a Rust crate dependency (`scry-interval`), not a WIT import, so the -// `interval` type is declared locally here and the `scry` world imports -// only WASI — the component runs standalone in wasmtime. The wasm-lattice -// component still exports the same `domain` interface (delegating to the -// same pure crates), preserving the DD-008 / DD-004 cross-component -// dogfood as a demonstration, just no longer on the analyzer's execution -// path. +// v0.1 WIT world. Hand-derived from spar/scry.aadl (see DD-010). +// The `scry` world imports the `domain` interface from the +// `pulseengine:wasm-lattice` component (see DD-004 for the +// reusability rationale and DD-008 for the dogfood rationale of +// cross-component WIT). meld will fuse `wasm-lattice` and the +// `scry-analyzer` component into a single distributable artifact; +// callers see a single component exporting the `analyzer` interface. package pulseengine:scry@0.1.0; interface analyzer { - /// Closed interval over signed 64-bit integers (abstracts i32/i64 - /// Wasm values). Declared locally as of v1.1 (FEAT-013): structurally - /// identical to the interval the `scry-interval` crate and the - /// `pulseengine:wasm-lattice/domain` interface use; the analyzer - /// converts at the crate-call boundary. Bottom is encoded `{lo:1, - /// hi:0}`; consumers should test emptiness semantically, not by the - /// encoding. - record interval { - lo: s64, - hi: s64, - } + use pulseengine:wasm-lattice/domain@0.1.0.{interval}; /// Region-pointer carried as part of an `abstract-value`. /// Structurally equivalent to the wasm-lattice's `region` @@ -37,9 +20,10 @@ interface analyzer { /// through the WAC composition (which the v0.1.0 wac compose /// path does not yet handle cleanly for the new variant — /// see commit message for the validation issue). - /// Conversion to/from `scry-interval`'s `Region` is trivial - /// (same field shape) and is performed inside the analyzer - /// implementation when it dispatches to the `region-*` transfer ops. + /// Conversion to/from `pulseengine:wasm-lattice/domain.region` + /// is trivial (same field shape) and is performed inside the + /// analyzer implementation when it dispatches to the + /// `region-*` transfer ops. record region-pointer-payload { region-id: u32, offset: interval, @@ -391,10 +375,6 @@ interface analyzer { } world scry { - // v1.1 (FEAT-013): no cross-component import — the analyzer is - // self-contained (interval/region/taint/octagon algebra are Rust - // crate deps), so the only imports are WASI, injected by wit-bindgen. - // This is what lets wasmtime 45 instantiate the composed artifact and - // run analyze() (the v1.0.1 open finding, closed). + import pulseengine:wasm-lattice/domain@0.1.0; export analyzer; } diff --git a/crates/scry-host-tests/tests/soundness.rs b/crates/scry-host-tests/tests/soundness.rs index 5c38438..c29f58f 100644 --- a/crates/scry-host-tests/tests/soundness.rs +++ b/crates/scry-host-tests/tests/soundness.rs @@ -979,33 +979,3 @@ fn composed_component_loads() -> Result<()> { } } } - -/// FEAT-013 AC#2 — the runnable gate. **No skip path.** Loads the shipped -/// composed component and invokes the live `analyze()` on a real input -/// module; if the component cannot instantiate or `analyze()` cannot run, -/// the `?`/`expect` propagates and the process exits non-zero. Prior to -/// v1.1 this test would have failed on wasmtime's "root-level component -/// imports are not supported" (the v1.0.1 open finding); v1.1 makes the -/// analyzer self-contained so it runs. The exit code is the falsifier. -#[test] -fn feat013_live_analyze_gate() { - let comp_path = component_path(); - assert!( - comp_path.exists(), - "FEAT-013 gate: composed component missing at {} — run `bazel build //:scry`", - comp_path.display() - ); - let wat_path = fixtures_dir().join("fixture-01-constant-fold.wat"); - let wasm = wat::parse_file(&wat_path) - .unwrap_or_else(|e| panic!("compile {}: {e}", wat_path.display())); - let bundle = run_analyzer(&comp_path, &wasm) - .unwrap_or_else(|e| panic!("FEAT-013 gate: live analyze() must run: {e:#}")); - assert!( - !bundle.points.is_empty(), - "FEAT-013 gate: live analyze() returned an empty invariant bundle" - ); - eprintln!( - "FEAT013_GATE_OK live analyze() ran on the self-contained component: {} program points", - bundle.points.len() - ); -} diff --git a/crates/scry-interval/BUILD.bazel b/crates/scry-interval/BUILD.bazel deleted file mode 100644 index b1775f0..0000000 --- a/crates/scry-interval/BUILD.bazel +++ /dev/null @@ -1,25 +0,0 @@ -load("@rules_rust//rust:defs.bzl", "rust_library", "rust_test") - -# scry-interval — pure interval + region-memory abstract domain -# (FEAT-001/FEAT-005), extracted for the self-contained analyzer -# (FEAT-013, DD-011). Like scry-octagon/scry-taint/scry-provenance it is -# a dependency-free crate cross-compiled to wasm32-wasip2 (linked into -# the scry-analyzer component so analyze() runs standalone) AND native -# (the wasm-lattice component delegates to it; scry-host-tests falsifies -# it). - -rust_library( - name = "scry_interval", - srcs = ["src/lib.rs"], - crate_name = "scry_interval", - edition = "2024", - visibility = ["//visibility:public"], - tags = ["feat-013"], -) - -rust_test( - name = "scry_interval_test", - crate = ":scry_interval", - edition = "2024", - tags = ["feat-013"], -) diff --git a/crates/scry-interval/Cargo.toml b/crates/scry-interval/Cargo.toml deleted file mode 100644 index 00a1b3d..0000000 --- a/crates/scry-interval/Cargo.toml +++ /dev/null @@ -1,20 +0,0 @@ -[package] -name = "scry-interval" -description = "Pure interval + region-memory abstract domain for scry (FEAT-001/FEAT-005; extracted for the self-contained analyzer, FEAT-013)." -version.workspace = true -edition.workspace = true -license.workspace = true -repository.workspace = true -authors.workspace = true - -# Pure library, zero deps — mirrors scry-octagon / scry-taint / -# scry-provenance. Compiles to wasm32-wasip2 (linked directly into the -# self-contained scry-analyzer component, FEAT-013) AND natively (the -# wasm-lattice component delegates its WIT `domain` exports to it, and -# scry-host-tests falsifies it). The transfer functions are the same -# ones whose soundness is mechanized in proofs/rocq/Soundness.v + -# Region.v. -[lib] -path = "src/lib.rs" - -[dependencies] diff --git a/crates/scry-interval/src/lib.rs b/crates/scry-interval/src/lib.rs deleted file mode 100644 index 50baaa8..0000000 --- a/crates/scry-interval/src/lib.rs +++ /dev/null @@ -1,383 +0,0 @@ -//! scry-interval — the pure interval + region-memory abstract domain -//! for scry (FEAT-005 region, FEAT-001 interval; extracted for FEAT-013 -//! v1.1). -//! -//! ## Why this crate exists (FEAT-013 / DD-011) -//! -//! Through v1.0 the analyzer reached the interval/region algebra over a -//! WIT cross-component import (`pulseengine:wasm-lattice/domain`). That -//! import is exactly what made the composed `//:scry` a hollow ~4.6 KB -//! shell: wac's `--import-dependencies` leaves the lattice as a -//! *root-level component import*, which wasmtime 45 rejects -//! ("root-level component imports are not supported"), so `analyze()` -//! could never run and analyzer source never reached the shipped binary -//! (the v1.0.1 open finding). -//! -//! v1.1 closes that gap by making the algebra a *crate dependency* of -//! the analyzer instead of a WIT import: this crate holds the interval -//! and region operations as plain Rust, the analyzer calls them -//! directly, and the `import pulseengine:wasm-lattice/domain` line -//! leaves the scry world — so the analyzer component imports only WASI -//! and runs standalone. -//! -//! Same pure-crate-dual-compile pattern as [`scry-octagon`] / -//! [`scry-taint`] / [`scry-provenance`]: `#![no_std]`, zero deps, -//! compiles to `wasm32-wasip2` (linked into the analyzer) AND natively -//! (falsified by `scry-host-tests`). The `wasm-lattice` component keeps -//! delegating its WIT `domain` exports to this crate, so the two- -//! component dogfood (DD-008) still demonstrates cross-component WIT — -//! it is just no longer the analyzer's execution path. -//! -//! The transfer functions are byte-for-byte the ones shipped in -//! `wasm-lattice` through v1.0 (interval soundness mechanized in -//! `proofs/rocq/Soundness.v`; region soundness in `proofs/rocq/ -//! Region.v`), so this is a pure relocation, not a behaviour change. - -#![cfg_attr(not(test), no_std)] - -/// Closed interval over signed 64-bit integers (abstracts i32 and i64 -/// Wasm values). Bottom (empty) is any interval with `lo > hi`, -/// canonically `{ lo: 1, hi: 0 }`; top is the full i64 range. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub struct Interval { - pub lo: i64, - pub hi: i64, -} - -/// A pointer abstracted as `(region_id, offset)` — the v0.3 region -/// memory domain. Same `region_id` ⇒ necessarily aliased; different -/// `region_id` ⇒ the lattice is non-relational across them. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub struct Region { - pub region_id: u32, - pub offset: Interval, -} - -/// Bottom (empty) interval — the conventional encoding `{ lo: 1, hi: 0 }`. -pub const BOTTOM: Interval = Interval { lo: 1, hi: 0 }; - -/// Top interval — the full i64 range. -pub const TOP: Interval = Interval { - lo: i64::MIN, - hi: i64::MAX, -}; - -/// True iff `x` is bottom (empty), i.e. `lo > hi`. -#[inline] -pub fn is_bot(x: Interval) -> bool { - x.lo > x.hi -} - -/// Canonicalise `(lo, hi)` to an interval, collapsing `lo > hi` to BOTTOM. -#[inline] -pub fn canon(lo: i64, hi: i64) -> Interval { - if lo > hi { BOTTOM } else { Interval { lo, hi } } -} - -// ── Interval lattice + transfer functions ────────────────────────── -// Bodies are identical to the v0.1–v1.0 wasm-lattice impl. - -pub fn bottom() -> Interval { - BOTTOM -} - -pub fn top() -> Interval { - TOP -} - -pub fn is_bottom(x: Interval) -> bool { - is_bot(x) -} - -pub fn leq(a: Interval, b: Interval) -> bool { - if is_bot(a) { - return true; - } - if is_bot(b) { - return false; - } - b.lo <= a.lo && a.hi <= b.hi -} - -pub fn join(a: Interval, b: Interval) -> Interval { - if is_bot(a) { - return b; - } - if is_bot(b) { - return a; - } - Interval { - lo: a.lo.min(b.lo), - hi: a.hi.max(b.hi), - } -} - -pub fn meet(a: Interval, b: Interval) -> Interval { - if is_bot(a) || is_bot(b) { - return BOTTOM; - } - canon(a.lo.max(b.lo), a.hi.min(b.hi)) -} - -pub fn widen(a: Interval, b: Interval) -> Interval { - if is_bot(a) { - return b; - } - if is_bot(b) { - return a; - } - let lo = if b.lo < a.lo { i64::MIN } else { a.lo }; - let hi = if b.hi > a.hi { i64::MAX } else { a.hi }; - Interval { lo, hi } -} - -pub fn constant_i32(c: i32) -> Interval { - Interval { - lo: c as i64, - hi: c as i64, - } -} - -pub fn constant_i64(c: i64) -> Interval { - Interval { lo: c, hi: c } -} - -pub fn i32_add(a: Interval, b: Interval) -> Interval { - if is_bot(a) || is_bot(b) { - return BOTTOM; - } - let lo = a.lo.saturating_add(b.lo); - let hi = a.hi.saturating_add(b.hi); - if lo < i32::MIN as i64 || hi > i32::MAX as i64 { - TOP - } else { - Interval { lo, hi } - } -} - -pub fn i32_sub(a: Interval, b: Interval) -> Interval { - if is_bot(a) || is_bot(b) { - return BOTTOM; - } - let lo = a.lo.saturating_sub(b.hi); - let hi = a.hi.saturating_sub(b.lo); - if lo < i32::MIN as i64 || hi > i32::MAX as i64 { - TOP - } else { - Interval { lo, hi } - } -} - -pub fn i32_mul(a: Interval, b: Interval) -> Interval { - if is_bot(a) || is_bot(b) { - return BOTTOM; - } - let corners = [ - a.lo.saturating_mul(b.lo), - a.lo.saturating_mul(b.hi), - a.hi.saturating_mul(b.lo), - a.hi.saturating_mul(b.hi), - ]; - let lo = corners.iter().copied().min().unwrap(); - let hi = corners.iter().copied().max().unwrap(); - if lo < i32::MIN as i64 || hi > i32::MAX as i64 { - TOP - } else { - Interval { lo, hi } - } -} - -// ── Region-memory domain (FEAT-005) ───────────────────────────────── - -pub fn region_create(region_id: u32) -> Region { - Region { - region_id, - offset: Interval { lo: 0, hi: 0 }, - } -} - -pub fn region_offset(r: Region, delta: Interval) -> Region { - if is_bot(r.offset) || is_bot(delta) { - return Region { - region_id: r.region_id, - offset: BOTTOM, - }; - } - let lo = r.offset.lo.saturating_add(delta.lo); - let hi = r.offset.hi.saturating_add(delta.hi); - Region { - region_id: r.region_id, - offset: canon(lo, hi), - } -} - -pub fn region_leq(a: Region, b: Region) -> bool { - if a.region_id != b.region_id { - return is_bot(a.offset); - } - if is_bot(a.offset) { - return true; - } - if is_bot(b.offset) { - return false; - } - b.offset.lo <= a.offset.lo && a.offset.hi <= b.offset.hi -} - -pub fn region_join(a: Region, b: Region) -> Region { - if a.region_id != b.region_id { - return Region { - region_id: a.region_id, - offset: TOP, - }; - } - let off = if is_bot(a.offset) { - b.offset - } else if is_bot(b.offset) { - a.offset - } else { - Interval { - lo: a.offset.lo.min(b.offset.lo), - hi: a.offset.hi.max(b.offset.hi), - } - }; - Region { - region_id: a.region_id, - offset: off, - } -} - -pub fn region_meet(a: Region, b: Region) -> Region { - if a.region_id != b.region_id { - return Region { - region_id: a.region_id, - offset: BOTTOM, - }; - } - let off = if is_bot(a.offset) || is_bot(b.offset) { - BOTTOM - } else { - canon(a.offset.lo.max(b.offset.lo), a.offset.hi.min(b.offset.hi)) - }; - Region { - region_id: a.region_id, - offset: off, - } -} - -pub fn region_widen(a: Region, b: Region) -> Region { - if a.region_id != b.region_id { - return Region { - region_id: a.region_id, - offset: TOP, - }; - } - let off = if is_bot(a.offset) { - b.offset - } else if is_bot(b.offset) { - a.offset - } else { - let lo = if b.offset.lo < a.offset.lo { - i64::MIN - } else { - a.offset.lo - }; - let hi = if b.offset.hi > a.offset.hi { - i64::MAX - } else { - a.offset.hi - }; - Interval { lo, hi } - }; - Region { - region_id: a.region_id, - offset: off, - } -} - -#[cfg(test)] -mod tests { - use super::*; - - /// γ: does concrete `z` lie in the interval? - fn gamma(a: Interval, z: i64) -> bool { - !is_bot(a) && a.lo <= z && z <= a.hi - } - - #[test] - fn extrema() { - assert!(is_bot(BOTTOM)); - assert!(!is_bot(TOP)); - assert!(gamma(TOP, 0)); - assert!(gamma(TOP, i64::MAX)); - assert!(!gamma(BOTTOM, 0)); - } - - #[test] - fn constants_are_singletons() { - assert_eq!(constant_i32(42), Interval { lo: 42, hi: 42 }); - assert_eq!(constant_i64(-7), Interval { lo: -7, hi: -7 }); - } - - /// add soundness: za∈γ(a), zb∈γ(b) ⇒ za+zb ∈ γ(a⊞b), over a sweep. - #[test] - fn i32_add_is_sound() { - for alo in -8..=8 { - for ahi in alo..=8 { - for blo in -8..=8 { - for bhi in blo..=8 { - let a = Interval { lo: alo, hi: ahi }; - let b = Interval { lo: blo, hi: bhi }; - let r = i32_add(a, b); - for za in alo..=ahi { - for zb in blo..=bhi { - assert!(gamma(r, za + zb), "{a:?}+{b:?} missed {}", za + zb); - } - } - } - } - } - } - } - - #[test] - fn join_is_upper_bound() { - let a = Interval { lo: 1, hi: 3 }; - let b = Interval { lo: 7, hi: 9 }; - let j = join(a, b); - assert!(leq(a, j) && leq(b, j)); - assert!(gamma(j, 1) && gamma(j, 9)); - } - - #[test] - fn widen_terminates_upward() { - let a = Interval { lo: 0, hi: 3 }; - let b = Interval { lo: 0, hi: 5 }; - // hi grew → widen to +∞. - assert_eq!(widen(a, b).hi, i64::MAX); - // stable → unchanged. - assert_eq!(widen(a, a), a); - } - - #[test] - fn region_offset_shifts_within_region() { - let r = region_create(7); - let r = region_offset(r, constant_i32(100)); - assert_eq!(r.region_id, 7); - assert_eq!(r.offset, Interval { lo: 100, hi: 100 }); - } - - #[test] - fn distinct_regions_do_not_alias_under_leq() { - let a = Region { - region_id: 1, - offset: Interval { lo: 0, hi: 4 }, - }; - let b = Region { - region_id: 2, - offset: Interval { lo: 0, hi: 4 }, - }; - // a non-bottom region is not ⊑ a different-id region. - assert!(!region_leq(a, b)); - } -}