prover: len/cross-array/fixed-new/affine proofs; keep facts past call loops

Rebased the prover WIP onto main. lafact_keep restores undirtied allocation
facts even when the loop body might free (so a later touch() no longer drops
every length fact). proven_p uses ptr_still so an outer call keeps the check.
entry_fact still supplies the size for the "might free" explain reason.
bounds_prover.zc and explain_prover.zc land with test.sh coverage.

1 files changed, 1 insertions, 0 deletions

diff --git a/TODO.md b/TODO.md
index d59947f..57083c3 100644
--- a/TODO.md
+++ b/TODO.md
@@ -153,6 +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.
 
 ### how the work is organized
 - start with `ONBOARD.md` (reading order and exact commands), then