Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 21 additions & 24 deletions BUILD.bazel
Original file line number Diff line number Diff line change
@@ -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",
)
55 changes: 1 addition & 54 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
7 changes: 0 additions & 7 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 0 additions & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ members = [
"crates/scry-provenance",
"crates/scry-taint",
"crates/scry-octagon",
"crates/scry-interval",
"crates/scry-host-tests",
]

Expand Down
22 changes: 8 additions & 14 deletions composition.wac
Original file line number Diff line number Diff line change
@@ -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;
31 changes: 9 additions & 22 deletions crates/scry-analyzer/BUILD.bazel
Original file line number Diff line number Diff line change
@@ -1,29 +1,24 @@
"""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")
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
Expand All @@ -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",
],
)
8 changes: 0 additions & 8 deletions crates/scry-analyzer/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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" }
84 changes: 2 additions & 82 deletions crates/scry-analyzer/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -169,97 +169,17 @@ 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
// `ComponentOrigin` type above; conversion between the two is a trivial
// 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).
Expand Down
Loading
Loading