Issues

thumb-2: --safety-bounds mask is a silent no-op for memory.copy/memory.fill — bulk memory emitted un-masked (identical to none) while safety-manifest still attests mask

#679

· avrabe opened

on Jul 9, 2026

--native-pointer-abi + --shadow-stack-size refuses wit-bindgen buffer node: inline linmem statics not down-shifted into .data (VCR-MEM-001 layer-2)

#678

· avrabe opened

on Jul 9, 2026

thumb-2: memory.copy/memory.fill clobber a local dest/src/len operand reused after the op (mutated in place as the loop pointer, no spill) — wild pointer / wrong result

#677

· avrabe opened

on Jul 9, 2026

call_indirect into a HETEROGENEOUS funcref table (mixed signatures) loud-declines — needs a runtime type-id check; the terminal layer of falcon's dispatch (20 funcs)

#676

· avrabe opened

on Jul 8, 2026

approach: generate the Rocq model from the shipped selector (close the 5-way divergence) + extend the certifying validator

#667

· avrabe opened

on Jul 8, 2026

thumb-2: parameter-bounded loop miscompiles — loop bound in a live param register (r0) clobbered by the induction increment, loop exits after 1 iteration

#663

· avrabe opened

on Jul 8, 2026

Internal (non-exported) func_N emitted as GLOBAL symbols → multiple-definition collision when co-linking two dissolved .o's

#656

· avrabe opened

on Jul 8, 2026

synth disasm decodes its own Cortex-M/thumb-2 output as A32 (garbage) — no thumb auto-detect, no .ARM.attributes

#637

· avrabe opened

on Jul 8, 2026

Make VFP f32/f64 reachable on the thumb-2 CLI path (Cortex-M4F) — encoder exists but decoder drops float ops; the M4F float frontier vs the new Cranelift arm32 backend

#619

· avrabe opened

on Jul 7, 2026

CI: self-hosted runner9 disk-full — Code Coverage failing with 'No space left on device' (will hit required jobs next)

#572

· avrabe opened

on Jul 2, 2026

Adopt ordeal (pure-Rust QF_BV) in synth-verify; demote Z3 to differential oracle, then drop static-link-z3

#553

· avrabe opened

on Jul 1, 2026

Feature challenge: add an aarch64 (host-native) backend so output runs and debugs natively on arm64 dev machines

#538

· avrabe opened

on Jun 30, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

thumb-2: --safety-bounds mask is a silent no-op for memory.copy/memory.fill — bulk memory emitted un-masked (identical to none) while safety-manifest still attests mask

--native-pointer-abi + --shadow-stack-size refuses wit-bindgen buffer node: inline linmem statics not down-shifted into .data (VCR-MEM-001 layer-2)

thumb-2: memory.copy/memory.fill clobber a local dest/src/len operand reused after the op (mutated in place as the loop pointer, no spill) — wild pointer / wrong result

call_indirect into a HETEROGENEOUS funcref table (mixed signatures) loud-declines — needs a runtime type-id check; the terminal layer of falcon's dispatch (20 funcs)

approach: generate the Rocq model from the shipped selector (close the 5-way divergence) + extend the certifying validator

thumb-2: parameter-bounded loop miscompiles — loop bound in a live param register (r0) clobbered by the induction increment, loop exits after 1 iteration

Internal (non-exported) func_N emitted as GLOBAL symbols → multiple-definition collision when co-linking two dissolved .o's

synth disasm decodes its own Cortex-M/thumb-2 output as A32 (garbage) — no thumb auto-detect, no .ARM.attributes

Make VFP f32/f64 reachable on the thumb-2 CLI path (Cortex-M4F) — encoder exists but decoder drops float ops; the M4F float frontier vs the new Cranelift arm32 backend

CI: self-hosted runner9 disk-full — Code Coverage failing with 'No space left on device' (will hit required jobs next)

Adopt ordeal (pure-Rust QF_BV) in synth-verify; demote Z3 to differential oracle, then drop static-link-z3

Feature challenge: add an aarch64 (host-native) backend so output runs and debugs natively on arm64 dev machines

Uh oh!

Search results