scry's soundness is honestly 'stated against the Wasm operational semantics and tracked toward mechanized proof against WasmCert-Coq.' Two approach moves close the gap the honest way:
- Spec-as-executable-oracle: import WasmCert-Coq now, as a differential. Rather than transcribing the Wasm semantics by hand (
WrapAdd.v models two's-complement wrap by hand), make WasmCert-Coq the external ground truth the transfer functions are checked against — the same way a verified interpreter is run against real engines. That turns 'sound vs the official semantics' from a prose claim into a mechanical differential.
- Generation: emit the Rocq/Verus lattice model from
scry-interval/wasm-lattice. Today Soundness.v and join_proofs.rs are hand-transcribed mirrors of the production Rust in the same γ-style — a mirror that drifts fools both provers identically. Generate the abstract model from the shipped crate (or the crate from the model) so the mirror can't drift.
The concrete-vs-abstract wasmtime oracle (soundness.rs, skip removed in FEAT-015) is already the reference-oracle move — extend it.
Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).
scry's soundness is honestly 'stated against the Wasm operational semantics and tracked toward mechanized proof against WasmCert-Coq.' Two approach moves close the gap the honest way:
WrapAdd.vmodels two's-complement wrap by hand), make WasmCert-Coq the external ground truth the transfer functions are checked against — the same way a verified interpreter is run against real engines. That turns 'sound vs the official semantics' from a prose claim into a mechanical differential.scry-interval/wasm-lattice. TodaySoundness.vandjoin_proofs.rsare hand-transcribed mirrors of the production Rust in the same γ-style — a mirror that drifts fools both provers identically. Generate the abstract model from the shipped crate (or the crate from the model) so the mirror can't drift.The concrete-vs-abstract wasmtime oracle (
soundness.rs, skip removed in FEAT-015) is already the reference-oracle move — extend it.Part of a verification-approach sweep (direction, not a defect): prefer generation over checking (a single source emits the artifacts, so drift becomes unrepresentable), use independence adversarially (run a second mechanisation to hunt spec bugs rather than shelving it), and invest reference oracles (one artifact everything else differential-tests against).