consume scry invariant JSON (scry-invariants/v1) for constant-fold / bounds-check elision / devirtualization

[avrabe]

Why

scry v0.6.0 (FEAT-008) publishes a stable, versioned JSON-schema contract describing the abstract invariants it proves about a Wasm module. This is the analyzer→optimizer half of the loop: scry proves, loom acts. This issue is loom's half — ingesting that JSON to strengthen transformation preconditions.

Mirrors the scry↔meld contract pattern (scry DD-002 / meld#192): the producing repo publishes + validates the schema; the consuming repo implements consumption separately.

The contract scry publishes

• Schema: contracts/scry-invariants-v1.schema.json in the scry repo — JSON Schema draft 2020-12, $id: https://pulseengine.eu/scry-invariants/v1, additionalProperties: false.
• Doc: docs/invariant-schema-v1.md — full WIT→JSON field mapping + worked examples.
• Stability: scry's crates/scry-host-tests/tests/contract.rs validates every representative bundle against the schema and asserts malformed bundles are rejected, so the contract won't silently drift.

What loom should consume

Per-instruction abstract invariants keyed by (func-index, pc), plus a resolved call graph and per-function summaries. Three transforms each invariant kind unlocks:

scry invariant	loom transform
singleton interval (lo == hi) on an instruction result	constant-fold the computation to i32.const lo
in-region load (region-pointer with offset interval proven within memory.size)	elide the bounds check on that load
singleton call-edge target set (sound, per scry FEAT-006)	devirtualize call_indirect → direct call

Suggested loom-side shape

1. A --consume-invariants <scry.json> flag on loom's optimize entry point.
2. Validate the input against scry-invariants-v1.schema.json before trusting it (reject on schema mismatch — never act on an unvalidated invariant; an unsound invariant would make loom's transform unsound).
3. Index the invariants by (func-index, pc); attach to loom's IR.
4. Gate each invariant-dependent transform on the matching invariant being present AND the soundness tag being sound.
5. The existing Z3 translation-validation pass remains the backstop: even if a scry invariant were wrong, loom's pre/post-optimization equivalence check catches a miscompile. (Defense-in-depth: scry's soundness + loom's translation validation are independent gates.)

Falsification

This integration is wrong if loom applies an invariant-dependent transform (e.g. bounds-check elision) on the basis of a scry invariant, AND loom's Z3 translation-validation then fails on the result — i.e. scry told loom something false that loom acted on. That would be a soundness bug in either scry's analysis or loom's invariant-matching; the translation-validation gate makes it observable rather than silent.

Cross-references

• scry v0.6.0 release: https://github.com/pulseengine/scry/releases/tag/v0.6.0
• scry FEAT-008 + REQ-004 (machine-consumable annotations for loom): scry artifacts/requirements.yaml
• Not blocking any scry release — scry's half is shipped and stable.

🤖 Generated with Claude Code