feat(provenance): SCPV v3 fusion premises for scry (#313 inc 1)#314
Open
avrabe wants to merge 4 commits into
Open
feat(provenance): SCPV v3 fusion premises for scry (#313 inc 1)#314avrabe wants to merge 4 commits into
avrabe wants to merge 4 commits into
Conversation
Reworks the `component-provenance` section to the converged binary SCPV v3 wire format (scry#63) and emits the two fusion-unique optimization premises that feed scry's sound abstract interpreter: - bounded_memory: no memory.grow in the fused core (memory_probe). - closed_world: all cross-component imports internalised; no residual import in a non-host namespace (conservative — unknown namespace ⇒ false). Why binary, why now: meld emitted JSON, scry-provenance decodes binary SCPV — the boundary never actually connected (BadMagic → provenance=None). Per DD-002 scry owns the format; converged on binary-canonical so scry's DO-333 trusted decoder stays lean/no_std (extend its SCPV reader, no JSON parser), and the one-time encoder swap lands on meld (untrusted host). meld's richer schema (sha256 binding, code_range, String component_id via length-prefix) ports into SCPV v3; premises live in the fixed header. meld does NOT compute value-ranges/const-args/dead-params — those are scry's analysis (scry-interval/scry-analyze-core), fed by these premises, for synth. SR-45 (sw-req, derives-from SYS-4) + SWV-45. Oracle: 9 provenance unit tests (codec round-trip both premises, header layout pinned, host-namespace classification) + v3_fusion_premises_present_on_real_fusion golden assertion; 439 lib tests green, clippy clean, rivet validate PASS. DWARF path unaffected (reads the in-memory struct, not the section bytes). Producer side of #313; scry consumer side tracked in scry#63. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
LS-N verification gate✅ 57/57 approved LS entries verified
Approved Failed LS entries(none) Missing regression tests(none) Updated automatically by |
Mythos delta-pass (auto)✅ NO FINDINGS across 1 Tier-5 file(s)
Auto-run via |
…314) Mythos delta-pass finding on the new SCPV v3 decoder: `from_bytes` read the entry count as a bare untrusted wire u32 and called `Vec::with_capacity(count)` unbounded — a crafted `component-provenance` section with count=u32::MAX forces a ~190 GiB allocation that aborts the process on memory-constrained hosts (containers/CI cgroups). Fix: cap the pre-allocation at the maximum entries the remaining bytes could hold (min entry = 13 bytes); the loop's bounded `take` still errors cleanly on genuine truncation. Regression PoC: from_bytes_huge_count_does_not_overallocate (count=u32::MAX + no entry bytes → Err, not OOM). 10 provenance tests green, clippy clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…#314) Second Mythos delta-pass finding: `is_host_import_namespace` used `starts_with("wasi")`, an over-broad prefix classifying a cross-component namespace like `wasi_auth_component` as host — so `fused_is_closed_world` returned true even when a real inter-component import edge survived, OVER- ASSERTING the `closed_world` premise (unsound; scry relies on it). Fix: precise host matching — exact `wasi_snapshot_preview1`/`wasi_unstable`/`env` + reserved `wasi:` and `pulseengine:async` prefixes; else non-host ⇒ closed_world stays conservatively false. Regression: a `wasi`-prefixed component namespace is non-host; `wasi:io/streams` stays host. 10 provenance tests green, clippy clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…hos #314) Third Mythos finding flagged `env` as another non-spec-reserved host namespace; the deeper issue is that ANY host allowlist is an over-assertion risk for a soundness premise (no namespace string is spec-guaranteed host). Stop patching the allowlist and make closed_world provably sound: true iff the fused module has zero imports (a tautology — no imports ⇒ no import edge ⇒ no inter-component escape — that cannot be over-asserted). Conservative (a module with host/WASI imports reports false); precise host-aware classification needs meld's resolution-state and is a follow-up — the SCPV v3 field already carries it. bounded_memory unchanged. 10 provenance unit tests + the real-fusion golden assertion (closed_world == zero-imports) green, clippy clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
github-actions
Bot
added
the
mythos-pass-done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Producer side of #313 (expose fusion facts for loom/synth specialization), inc 1. Pairs with scry#63 (consumer-side format).
What
Reworks the
component-provenancesection to the converged binary SCPV v3 wire format and emits the two fusion-unique optimization premises that feed scry's sound abstract interpreter:bounded_memory— nomemory.growin the fused core (fixed linear memory).closed_world— all cross-component import edges internalised; no residual import in a non-host namespace (conservative — unknown namespace ⇒false, never over-asserted).Why binary, why now
meld emitted JSON; scry-provenance decodes binary SCPV → the boundary never actually connected (
BadMagic→provenance=None, a dead feature). Per DD-002 scry owns the format; we converged (scry#63) on binary-canonical so scry's DO-333 trusted decoder stays lean/no_std(extend its SCPV reader, no JSON parser in the trusted base), and the one-time encoder swap lands on meld (untrusted host). meld's richer schema (sha256 binding,code_range, Stringcomponent_idvia length-prefix) ports into v3; premises live in the fixed header.Scope discipline
meld does not compute value-ranges / const-args / dead-params — that's scry's analysis (
scry-interval/scry-analyze-core), fed by these premises, for synth. inc 2+ is scry's, not meld's.Verification
derives-from SYS-4) + SWV-45.(bounded,closed)combos; header byte-layout pinned to scry#63; host-namespace classification (wasi/env/no-imports ⇒ closed; component-instance import ⇒ not closed).v3_fusion_premises_present_on_real_fusion: a real wac-composed fusion emitsSCPVmagic withclosed_world=trueandbounded_memory = !uses(memory.grow).rivet validatePASS. DWARF path unaffected (reads the in-memory struct, not the section bytes).Refs #313, scry#63.
🤖 Generated with Claude Code