diff options
| -rw-r--r-- | TODO.md | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -153,7 +153,7 @@ and pushed there. - x86-64 direct o3-to-o3 calls merged (`rcall_x64` / `rfinish_x64`, e765c3d). `make check` 214/0; icon regression 14/0; jit_x64 vs interp on o3* 17/17; o3_caller_replace and o3direct ok. post-rcall fib on x86-64 jit (ms/iter min): plain 0.54, o3 0.35 (o3 was 0.92 before direct calls). - trees/sieve baseline on x86-64 jit after rcall, before allocator change (ms/iter min): trees plain new/free 2.88, o3 new/free 4.13, o3 arena 0.09; sieve plain 6.96, o3 checked 0.64, o3 raw 0.61. (older llvm note was plain 9.2 / o3 12.0.) - allocator: o3 now uses `new_k` (size-class free lists) like plain code; `new_k`/`recycle_leaf` skip the o3 arg-fatten path. after: trees plain 2.78, o3 new/free 2.71, o3 arena 0.15. still open: emit the freelist pop/push as native code inside a compiled region (today every `new_k` still leaves via a normal call). -- prover gaps (work/prover): rebase onto main, fix lafact_keep after call-loops and proven_p across enclosing loops; bounds_prover / explain_prover land with test.sh checks. still open from the overnight queue: find_replace hardening and remaining TODO items. +- prover gaps merged (75f9ddb + c8cdee8): len/cross-array/fixed-new/affine proofs; proven_p checks enclosing loops; explain_prover reordered so call-loops come last (lafacts stay cleared after a may-free body). make check 217/0. still open from the overnight queue: find_replace hardening, native freelist inline inside compiled regions, remaining TODO items. ### how the work is organized - start with `ONBOARD.md` (reading order and exact commands), then |