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.

3 files changed, 16 insertions, 0 deletions

diff --git a/tests/programs/bounds_prover.expected b/tests/programs/bounds_prover.expected
new file mode 100644
index 0000000..f5e92fa
--- /dev/null
+++ b/tests/programs/bounds_prover.expected
@@ -0,0 +1,4 @@
+28
+36
+0 1 2 3 4 5 6 zy: index 6 out of range (length 6)
+  at <stdin>:17 in main
diff --git a/tests/programs/explain_prover.expected b/tests/programs/explain_prover.expected
new file mode 100644
index 0000000..c43c72d
--- /dev/null
+++ b/tests/programs/explain_prover.expected
@@ -0,0 +1,9 @@
+{"version":1}
+{"file":"<eval>","line":18,"col":42,"end_line":18,"end_col":45,"fn":"main","kind":"index","loop_depth":1,"reason":"bound-not-invariant","fix":"the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"}
+{"file":"<eval>","line":22,"col":51,"end_line":22,"end_col":54,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
+{"file":"<eval>","line":26,"col":62,"end_line":26,"end_col":65,"fn":"main","kind":"pointer","loop_depth":2,"reason":"pointer-may-be-freed","fix":"the loop body calls something that might free or resize the block; move the call out of the loop"}
+{"file":"<eval>","line":27,"col":71,"end_line":27,"end_col":74,"fn":"main","kind":"pointer","loop_depth":2,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
+{"file":"<eval>","line":30,"col":46,"end_line":30,"end_col":49,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
+{"file":"<eval>","line":34,"col":81,"end_line":34,"end_col":92,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":35,"col":70,"end_line":35,"end_col":81,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":36,"col":59,"end_line":36,"end_col":70,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
diff --git a/tests/test.sh b/tests/test.sh
index 70e12b9..6992c0d 100755
--- a/tests/test.sh
+++ b/tests/test.sh
@@ -235,6 +235,9 @@ ABC" "$l o3 lifts byte loads and stores"
 	chk "$($vm < tests/programs/bounds_body.zc 2>&1 | head -1)" "zy: index -2999 out of range (length 4)" "$l a body that moves the loop index keeps the check"
 	chk "$($vm < tests/programs/bounds_ptr.zc 2>&1 | head -3 | cut -c1-9)" $'120\n240\nzy: index' "$l a pointer from rt.new(n): proved, hoisted, or kept when the body calls"
 	chk "$($vm --explain-checks < tests/programs/explain_checks.zc | md5sum)" "$(md5sum < tests/programs/explain_checks.expected)" "$l --explain-checks lists the kept checks (format v1)"
+	chk "$($vm < tests/programs/bounds_prover.zc 2>&1 | head -5)" $'28\n36\n0 1 2 3 4 5 6 zy: index 6 out of range (length 6)\n  at <stdin>:17 in main' "$l loop prover: len, cross-array and affine proofs; a too-long constant bound still faults"
+	chk "$($vm --explain-checks < tests/programs/explain_prover.zc | md5sum)" "$(md5sum < tests/programs/explain_prover.expected)" "$l --explain-checks for the prover cases (proved lines absent, kept lines present)"
+	chk "$($vm < tests/programs/explain_prover.zc)" "1204" "$l explain_prover runs and prints its checksum"
 	chk "$($vm --explain-checks a/b.zc < tests/programs/bounds.zc | head -1)" '{"version":1}' "$l --explain-checks starts with the version line"
 	chk "$($vm < tests/programs/zc0unbounded.zc)" "42" "$l unbounded in the unit, a prefix and a statement"
 	local r; r=$(bash tests/runerr.sh "$vm" tests/errors | tail -1)