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/test.sh | 3 +++ 1 file changed, 3 insertions(+) (limited to 'tests/test.sh') 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 :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) -- cgit v1.2.3