v0.2 plan: real interval-domain fixpoint + Verus/Rocq toolchain + region memory

[avrabe]

Umbrella issue tracking the v0.2 cycle. Three feature artifacts in the rivet graph already type the work; this issue exists as a contributor entry-point.

v0.2 scope (typed in artifacts/requirements.yaml)

FEAT-001 acceptance criterion #1 — real interval-domain fixpoint

The v0.1.0 scaffold returns a hardcoded invariant bundle. v0.2 ships:

• wasmparser integration to walk the input Wasm module.
• A fixpoint engine that propagates interval invariants through arithmetic instructions.
• Per-program-point invariants emitted in the on-disk JSON schema declared at https://pulseengine.eu/scry-invariants/v1.

FEAT-001 acceptance criterion #3 — host wasmtime test harness

• New crate crates/scry-host-tests/ (cargo, native, depends on wasmtime-wasi).
• Loads the built bazel-bin/scry.wasm, invokes analyzer.analyze via the WIT bindings, asserts the returned intervals over-approximate concrete execution of the input.
• Promotes CI's currently-placeholder Clippy + Test jobs to real cargo runs.

FEAT-005 — region-based linear-memory model

• CRAB-style region tracking in the wasm-lattice crate.
• Per-region offset intervals (not collapsed into one giant interval).
• Property-based soundness tests on the region × interval product domain.

FEAT-012 — wire Verus + Rocq into the Bazel build

• Add rules_verus (commit a49f72ef per synth) + rules_rocq_rust (commit 090b875c6 per synth) to MODULE.bazel.
• Add nix_repo config for hermetic Rocq.
• proofs/verus/ with the join-commutativity theorem on the interval domain.
• proofs/rocq/ with the ⊑-reflexivity theorem on the interval lattice.
• New CI job rocq-proofs (continue-on-error: true per the loom pattern).

Why these and not others

The v0.2 cycle picks features that lift the scaffold's known limitations (per the v0.1.0 CHANGELOG "Known limitations" section). It does NOT include witness MC/DC, sigil signing of analyzer attestations (FEAT-004), or Component Model AI (FEAT-002) — those depend on the v0.2 work landing first.

Falsification

v0.2 is wrong if, after these features land, the scry CLI's interval invariants are ever observed to exclude a concrete value that the program actually computed for a given input. The host wasmtime test harness from FEAT-001 AC#3 is the mechanical falsifier — every test run that hits the analyzer is a chance to refute the soundness claim.

Cross-repo dependency status

• pulseengine/meld#192 — component-provenance custom section. Not blocking v0.2; needed for v0.7 (FEAT-002 — Component Model AI).

🤖 Generated with Claude Code