Issues

• [V4b] A real register allocator in Lean (removes regalloc2)

  scopework-package
  eth-act/clifv#57 · Filter by author kevaundray opened on Oct 5, 2026

• kevaundray: current work and intentions

  eth-act/clifv#52 · Filter by author kevaundray opened on Oct 5, 2026

• Compiler agreement: daily reports

  eth-act/clifv#46 · Filter by author codygunton opened on Oct 5, 2026
  1

• codygunton: current work and intentions

  eth-act/clifv#44 · Filter by author codygunton opened on Oct 5, 2026

• [T7] Trusted base: normalize.py, clif-data-export (frontend-side tools)

  trusted-basework-package
  eth-act/clifv#43 · Filter by author kevaundray opened on Oct 4, 2026

• [T6] Trusted base: Lean.ofReduceBool/native_decide in the fixed proofs (bv_decide certificates, encoder facts)

  trusted-basework-package
  eth-act/clifv#42 · Filter by author kevaundray opened on Oct 4, 2026

• [T5] Trusted base: Clif.run fidelity (Cranelift interpreter + native runs)

  trusted-basework-package
  eth-act/clifv#41 · Filter by author kevaundray opened on Oct 4, 2026

• [T4] Trusted base: Arm model fidelity (ASL-derived, qemu co-simulation)

  trusted-basework-package
  eth-act/clifv#40 · Filter by author kevaundray opened on Oct 4, 2026

• [T3] Trusted base: std/musl contracts: compile std through cargo fv (-Zbuild-std)

  trusted-basework-package
  eth-act/clifv#39 · Filter by author kevaundray opened on Oct 4, 2026

• [T2] Trusted base: Atomics on a single-core model (ldar/stlr plain, exclusive store always succeeds, dmb no-op)

  trusted-basework-package
  eth-act/clifv#38 · Filter by author kevaundray opened on Oct 4, 2026

• [T1] Trusted base: TLS: TLSDESC hook vs lld's local-exec rewrite

  trusted-basework-package
  eth-act/clifv#37 · Filter by author kevaundray opened on Oct 4, 2026

• [S12] SIMD

  scopework-package
  eth-act/clifv#36 · Filter by author kevaundray opened on Oct 4, 2026

• [S11] Floats (f32/f64 in Clif.run, Arm FP instructions co-simulated, rules + proofs, FP register class in checkAlloc/V4)

  scopework-package
  eth-act/clifv#35 · Filter by author kevaundray opened on Oct 4, 2026

• [S10] Unwinding: landing pads, LSDA, .eh_frame, try_call's exceptional edge

  scopework-package
  eth-act/clifv#34 · Filter by author kevaundray opened on Oct 4, 2026

• [S9] Trapping helpers (__*ti3 division by zero) and traps inside program callees

  scopework-package
  eth-act/clifv#33 · Filter by author kevaundray opened on Oct 4, 2026

• [S8] return_call; recursion through a pointer; a function calling itself under its own name; indirect callees with stack-passed or sret params

  scopework-package
  eth-act/clifv#32 · Filter by author kevaundray opened on Oct 4, 2026

• [S7] vmctx/sarg parameters; sret return register (x0 holds the pointer)

  scopework-package
  eth-act/clifv#31 · Filter by author kevaundray opened on Oct 4, 2026

• [S6] A decidable Pre for legalisation (noSelf, defs, ids) so check is provably redundant on InScope

  scopework-package
  eth-act/clifv#30 · Filter by author kevaundray opened on Oct 4, 2026

• [S5] Stack-passed arguments of call_indirect/try_call_indirect (≤ 8 register params today)

  scopework-package
  eth-act/clifv#29 · Filter by author kevaundray opened on Oct 4, 2026

• [S4] i128 gaps: umulhi/smulhi, try_call, overflow ops, atomics, stack-passed i128, i128 indirect signatures, try_call_indirect

  scopework-package
  eth-act/clifv#28 · Filter by author kevaundray opened on Oct 4, 2026

• [S3] Whole-program refinement of the original i128 source program

  scopework-package
  eth-act/clifv#27 · Filter by author kevaundray opened on Oct 4, 2026

• [S2] Legalisation + optimisation composed; legalised functions in the linking theorem

  scopework-package
  eth-act/clifv#26 · Filter by author kevaundray opened on Oct 4, 2026

• [S1] Optimiser with call_indirect and try_call/try_call_indirect

  scopework-package
  eth-act/clifv#25 · Filter by author kevaundray opened on Oct 4, 2026

• [M1] Mid-end validators: completeness (optional, quality only)

  scopework-package
  eth-act/clifv#24 · Filter by author kevaundray opened on Oct 4, 2026

• [R9] Mid-end rule proofs: skeleton (18 rules left)

  rule-proofswork-package
  eth-act/clifv#23 · Filter by author kevaundray opened on Oct 4, 2026