All issues

Mixed-width i32/i64 Select forces verification reverts: coverage loss is counted but not attributed, and the free verify entry point is panic-unsafe

#331

· avrabe opened

on Aug 13, 2026

reconstruct_component corrupts components that nest core modules inside a ComponentSection

#325

· avrabe opened

on Aug 12, 2026

#240's premise hook is inert: assume_max/assume_range have no non-test callers, so fits_below_bit can never fire

#323

· avrabe opened

on Aug 12, 2026

Retire Z3: migrate the core translation validator to ordeal and drop the C++ dependency

#313

· avrabe opened

on Aug 7, 2026

Canonical-ABI glue survives the dissolve: componentizing a scalar-only driver doubles .text, and cabi_realloc (x2) is never removed

#303

· avrabe opened

on Jul 30, 2026

Translation validation: verify refinement with traps as first-class state (Alive2 encoding), not value-equivalence + guards

#300

· avrabe opened

on Jul 28, 2026

Investigate: verify.rs opaque-float shared const name may unify distinct float ops (verifier soundness)

#283

· avrabe opened

on Jul 15, 2026

Adopt ordeal for certificate-checked optimization-rule verification (replace loom's own Z3 path)

#277

· avrabe opened

on Jul 11, 2026

approach: discharge the stub axioms so the Rocq proofs stop being vacuous (the differential + EMI legs are already right)

#271

· avrabe opened

on Jul 8, 2026

synth's requirements for a Z3 replacement — QF_BV one-shot validation; the static-link build is the real pain, not the solver

#246

· avrabe opened

on Jul 1, 2026

Carry Verus value-range/no-alias facts as IR premises + algebraic mid-end — feed synth's beat-LLVM specialization

#240

· avrabe opened

on Jun 25, 2026

Make components small: custom-section GC + component-level reachability GC + canon seam dissolution

#239

· avrabe opened

on Jun 25, 2026