From fe43cc41876ffdb3e714de8efc8a2907d456b5db Mon Sep 17 00:00:00 2001 From: zinc Date: Thu, 15 Oct 2026 05:23:36 +0330 Subject: 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. --- tests/programs/bounds_prover.expected | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/programs/bounds_prover.expected (limited to 'tests/programs/bounds_prover.expected') 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 :17 in main -- cgit v1.2.3