Issues

31,210 transforms found and discarded across 215 real-world modules — 73% dropped by a greedy cost rule BEFORE verification, not by proving power (data + an open challenge)

#348

· avrabe opened

on Aug 21, 2026

loom optimize does not finish in 300s on a 584KB meld-fused module — 97/100 real-world components blocked; a LARGER, denser ordinary module completes in 39s

#347

· avrabe opened

on Aug 20, 2026

loom optimize drops the data count section while keeping memory.init — exits 0 with '✅ Optimization complete!' and emits a module that fails validation

#346

· avrabe opened

on Aug 20, 2026

optimize_module applies the #196 element-section guard; the CLI pipeline does not — the library and the binary optimize differently

#345

· avrabe opened

on Aug 20, 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

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

Navigation Menu

Uh oh!

All issues

31,210 transforms found and discarded across 215 real-world modules — 73% dropped by a greedy cost rule BEFORE verification, not by proving power (data + an open challenge)

loom optimize does not finish in 300s on a 584KB meld-fused module — 97/100 real-world components blocked; a LARGER, denser ordinary module completes in 39s

loom optimize drops the data count section while keeping memory.init — exits 0 with '✅ Optimization complete!' and emits a module that fails validation

optimize_module applies the #196 element-section guard; the CLI pipeline does not — the library and the binary optimize differently

reconstruct_component corrupts components that nest core modules inside a ComponentSection

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

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

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

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

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

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

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

Uh oh!

Search results