scry-bits (known-bits × congruence reduced product; transfers and/or/xor/not/shl/shr/add/sub/mul, crates/scry-bits/src/lib.rs) proves transfer soundness only by exhaustive γ-sweep at w=8 (const W=8) because 32/64-bit enumeration is infeasible. The soundness obligation ∀ x∈γ(a),y∈γ(b): op(x,y)∈γ(f#(a,b)) for a concrete abstract input is a single QF_BV UNSAT query.
Proposal: discharge it with ordeal at the real analysis widths (32/64), emitting a portable cert.recheck() certificate bindable as DO-333 abstract-interpretation evidence — Z3-free, directly advancing #95's "reference oracle / adversarial independence" ask. Every op is in ordeal's fragment as-is; known-bits/congruence γ is a QF_BV mask/modulus predicate.
Enabler: the equivalence & soundness toolkit — ordeal roadmap pulseengine/ordeal#66 (v0.12.0). Boundary: validates soundness per concrete abstract input (literals ⇒ QF_BV); ∀-all-abstract-states and the lattice/join laws are quantified (stay in Verus). scry-float is FP — OUT.
scry-bits(known-bits × congruence reduced product; transfersand/or/xor/not/shl/shr/add/sub/mul,crates/scry-bits/src/lib.rs) proves transfer soundness only by exhaustive γ-sweep at w=8 (const W=8) because 32/64-bit enumeration is infeasible. The soundness obligation∀ x∈γ(a),y∈γ(b): op(x,y)∈γ(f#(a,b))for a concrete abstract input is a single QF_BV UNSAT query.Proposal: discharge it with ordeal at the real analysis widths (32/64), emitting a portable
cert.recheck()certificate bindable as DO-333 abstract-interpretation evidence — Z3-free, directly advancing #95's "reference oracle / adversarial independence" ask. Every op is in ordeal's fragment as-is; known-bits/congruence γ is a QF_BV mask/modulus predicate.Enabler: the equivalence & soundness toolkit — ordeal roadmap pulseengine/ordeal#66 (v0.12.0). Boundary: validates soundness per concrete abstract input (literals ⇒ QF_BV); ∀-all-abstract-states and the lattice/join laws are quantified (stay in Verus).
scry-floatis FP — OUT.