loom's empirical independence is already strong and Conrad-aligned: the wasm-opt differential (an independent optimizer as oracle) and EMI mutation (input-mutation meta-oracle) are exactly the reference-oracle and meta-oracle moves — keep them.
The approach gap is on the deductive side, and it's a vacuity risk: the Rocq 'proofs' lean on stub axioms. Correctness.v's master theorem rests on Axiom term_instr_bijection … := True; FusedOptimization.v on ~10 assumed wasm-semantics axioms (exec_call, trivial_call_nop, …). An Axiom := True standing in for the load-bearing lemma is the spec-side twin of a green verifier on a vacuous spec — the proof passes because it constrains nothing.
First step: treat every semantic Axiom in proofs/ as a tracked debt with a discharge plan (define + prove, or demote the claim to what the Z3 translation-validation actually establishes). The Z3 validator's own documented soundness gaps (return-value-only equivalence, discarded branch conditions, void auto-pass — docs/analysis/z3-status.md) belong on the same ledger. Generation move, longer-term: derive the Rocq simplify model from the ISLE rules that are the implementation, so the model can't diverge from the rewrite it proves.
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).
loom's empirical independence is already strong and Conrad-aligned: the wasm-opt differential (an independent optimizer as oracle) and EMI mutation (input-mutation meta-oracle) are exactly the reference-oracle and meta-oracle moves — keep them.
The approach gap is on the deductive side, and it's a vacuity risk: the Rocq 'proofs' lean on stub axioms.
Correctness.v's master theorem rests onAxiom term_instr_bijection … := True;FusedOptimization.von ~10 assumed wasm-semantics axioms (exec_call,trivial_call_nop, …). AnAxiom := Truestanding in for the load-bearing lemma is the spec-side twin of a green verifier on a vacuous spec — the proof passes because it constrains nothing.First step: treat every semantic
Axiominproofs/as a tracked debt with a discharge plan (define + prove, or demote the claim to what the Z3 translation-validation actually establishes). The Z3 validator's own documented soundness gaps (return-value-only equivalence, discarded branch conditions, void auto-pass —docs/analysis/z3-status.md) belong on the same ledger. Generation move, longer-term: derive the Rocqsimplifymodel from the ISLE rules that are the implementation, so the model can't diverge from the rewrite it proves.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).