Issues

falcon f32 path residual after #708: f32.store + f32.abs + f32.copysign + mixed f32/int params + f32-across-call + local.set still skip (20 of falcon's 31 --relocatable skips)

#719

· avrabe opened

on Jul 11, 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

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

Beyond parity: proof-carrying specialization + optimal-alloc to BEAT LLVM (0.7× target)

#494

· avrabe opened

on Jun 25, 2026

perf: consecutive const-address stores re-materialize the linear-memory base every time

#468

· avrabe opened

on Jun 24, 2026

dissolve: bind passed-through embedder import `cabi-arena-realloc` to the native TCB arena allocator

#418

· avrabe opened

on Jun 22, 2026

Multi-memory structural isolation: lower N wasm memories to N distinct native bases (memidx-through-IR, cross-memory ops, expose base/size for MPU/PMP)

#406

· avrabe opened

on Jun 21, 2026

Design question: multi-memory → distinct native regions (MPU-protectable) vs single shared memory — which isolation model for the dissolved library-OS?

#404

· avrabe opened

on Jun 21, 2026

MC/DC source-to-object traceability: synth's branch folding/splitting changes the decision set witness measures on wasm

#396

· avrabe opened

on Jun 20, 2026

Emit DWARF in the ARM/RISC-V ELF — synth drops debug info; bare-metal output is not source-debuggable

#394

· avrabe opened

on Jun 20, 2026

Codegen: close the 3.9× size gap vs LLVM on the gust hot path (regalloc + addressing-mode folding)

#390

· avrabe opened

on Jun 20, 2026

scry

#290

· avrabe opened

on Jun 10, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

falcon f32 path residual after #708: f32.store + f32.abs + f32.copysign + mixed f32/int params + f32-across-call + local.set still skip (20 of falcon's 31 --relocatable skips)

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

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

Beyond parity: proof-carrying specialization + optimal-alloc to BEAT LLVM (0.7× target)

perf: consecutive const-address stores re-materialize the linear-memory base every time

dissolve: bind passed-through embedder import `cabi-arena-realloc` to the native TCB arena allocator

Multi-memory structural isolation: lower N wasm memories to N distinct native bases (memidx-through-IR, cross-memory ops, expose base/size for MPU/PMP)

Design question: multi-memory → distinct native regions (MPU-protectable) vs single shared memory — which isolation model for the dissolved library-OS?

MC/DC source-to-object traceability: synth's branch folding/splitting changes the decision set witness measures on wasm

Emit DWARF in the ARM/RISC-V ELF — synth drops debug info; bare-metal output is not source-debuggable

Codegen: close the 3.9× size gap vs LLVM on the gust hot path (regalloc + addressing-mode folding)

scry

Uh oh!

Search results