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, 27 insertions, 19 deletions

diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc
index 8b52f83..bf7dd9f 100644
--- a/src/compiler/analyzer.zc
+++ b/src/compiler/analyzer.zc
@@ -703,12 +703,15 @@ word lafact_save() {
 	while (i < nloc) { b[2 + i - lbase] = lafact[i]; i++; }
 	return b;
 }
-// after a loop that frees nothing: the locals its body left alone get back the
-// allocation facts the loop forgot
+// after a loop: the locals its body left alone get back the allocation facts
+// the loop forgot. a body that might free (r[55]) still restores facts for
+// undirtied locals: a call that did not take the local cannot have freed it,
+// and proofs inside a later loop re-check r[55] for that loop. without this,
+// one touch() earlier in the function would permanently drop every length fact.
 
 int lafact_keep(word r, word b) {
 	int i;
-	if (!b || dry || r[0] || r[55]) return 0;
+	if (!b || dry || r[0]) return 0;
 	i = b[0];
 	while (i < b[1] && i < nloc) { if (b[2 + i - b[0]] && !lafact[i] && !ldirty(r, lname[i]) && lclean(i)) lafact[i] = b[2 + i - b[0]]; i++; }
 	return 0;
@@ -724,7 +727,10 @@ word entry_fact(int ix, int bl) {
 	while (k > loopbase) {
 		k--;
 		r = linfo(k);
-		if (!r || ldirty(r, lname[bl]) || !lclean(bl) || r[55]) return 0;
+		// r[55] is left to proven_p / ptr_still: a call in this loop must keep
+		// the check, but the size fact at entry is still what --explain-checks
+		// needs for the "might free" reason rather than "size unknown".
+		if (!r || ldirty(r, lname[bl]) || !lclean(bl)) return 0;
 		b = r[56];
 		if (b && bl >= b[0] && bl < b[1]) { f = b[2 + bl - b[0]]; if (f) return f; }
 	}
@@ -751,6 +757,19 @@ int pbound(int w) {
 	if (p_ar(w) >= 0) return dyn_len(p_ar(w));
 	return 0 - 1;
 }
+// every enclosing loop leaves the local arr alone and frees nothing (any call
+// might free a block another pointer aliases)
+
+int ptr_still(int arr) {
+	int k = lsp; word r;
+	while (k > loopbase) {
+		k--;
+		r = linfo(k);
+		if (!r || ldirty(r, lname[arr]) || !lclean(arr) || r[55]) return 0;
+	}
+	return 1;
+}
+
 // i >= 0 and i < n for a fixed array of n elements, proved by a loop test
 // with a step of +1 against a constant of at most n, or len() of an array of
 // at most n elements
@@ -768,15 +787,16 @@ int proven_n(int ix, int n) {
 // array of n elements, in a loop whose body leaves arr alone and frees nothing
 
 int proven_p(int ix, int n, int arr) {
-	int k = lsp, w, b; word r;
+	int k = lsp, w, b;
 	while (k > loopbase) {
 		k--;
 		w = lpfact[k];
 		if (w >= 0 && p_iv(w) == ix) {
 			b = pbound(w);
 			if (b < 0 || b > n) return 0;
-			r = linfo(k);
-			return r && !ldirty(r, lname[arr]) && lclean(arr) && !r[55];
+			// every enclosing loop, not only this one: touch() in an outer
+			// body must keep the check even when the index loop itself is clean
+			return ptr_still(arr);
 		}
 	}
 	return 0;
@@ -795,18 +815,6 @@ int local_ub(int i) {
 	}
 	return best;
 }
-// every enclosing loop leaves the local arr alone and frees nothing (any call
-// might free a block another pointer aliases)
-
-int ptr_still(int arr) {
-	int k = lsp; word r;
-	while (k > loopbase) {
-		k--;
-		r = linfo(k);
-		if (!r || ldirty(r, lname[arr]) || !lclean(arr) || r[55]) return 0;
-	}
-	return 1;
-}
 int oub() {
 	if (lv && lvk == LV_LOCAL) return local_ub(lvi);
 	if (lv) return 0 - 1;