From 900c59c4d72c692e0bb8e0d3a28cc52547e58c9b Mon Sep 17 00:00:00 2001 From: zinc Date: Wed, 14 Oct 2026 20:46:17 +0330 Subject: wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, affine i*n+k); unbuilt and untested --- tests/programs/explain_prover.zc | 40 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 tests/programs/explain_prover.zc (limited to 'tests/programs/explain_prover.zc') diff --git a/tests/programs/explain_prover.zc b/tests/programs/explain_prover.zc new file mode 100644 index 0000000..14486b5 --- /dev/null +++ b/tests/programs/explain_prover.zc @@ -0,0 +1,40 @@ +namespace; +include rt; + +// the loop prover, case by case: each "kept" line must stay in zy --explain-checks +// and each "proved" line must not. run, it prints one checksum. +int touch() { return 0; } +int[16] sq; +int main() { + int i, j, k, s = 0, n = 4; + fixed int[?] a = rt.new(fixed int[?], 8); + fixed int[?] b = rt.new(fixed int[?], 10); + fixed int[?] c = rt.new(fixed int[?], 6); + fixed int[?] m = rt.new(fixed int[?], 16); + fixed int[?] m15 = rt.new(fixed int[?], 15); + int* p = rt.new(16); + // 1. i < len(a) in the test + for (i = 0; i < len(a); i++) a[i] = i; // proved + for (i = 0; i < len(a); i++) { s = s + a[i]; i = i + 0; } // kept: the body moves i + // 2. len(a) bounds another array of known length + for (i = 0; i < len(a); i++) s = s + b[i]; // proved: 8 <= 10 + for (i = 0; i < len(a); i++) s = s + sq[i]; // proved: 8 <= 16 + for (i = 0; i < len(a); i++) if (i < 6) s = s + c[i]; // kept: 6 < 8 + // 3. a pointer of constant size at depth 2 and 3 + for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) p[j] = j; // proved + for (i = 0; i < 2; i++) for (k = 0; k < 2; k++) for (j = 0; j < 16; j++) s = s + p[j]; // proved + for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) { s = s + p[j]; touch(); } // kept: the body calls + for (i = 0; i < 2; i++) { touch(); for (j = 0; j < 16; j++) s = s + p[j]; } // kept: the outer body calls + // 4. new(fixed int[?], n) with a constant n + for (i = 0; i < 6; i++) s = s + c[i]; // proved + for (i = 0; i < 7; i++) if (i < 6) s = s + c[i]; // kept: 7 > 6 + // 5. i * n + k into exactly n * n + for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) m[i * 4 + k] = i + k; // proved + for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) s = s + p[i * 4 + k]; // proved + for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) if (i * 4 + k < 15) s = s + m15[i * 4 + k]; // kept: 15 < 16 + for (i = 0; i < 4; i++) for (k = 0; k < 5; k++) if (k < 4) s = s + m[i * 4 + k]; // kept: k < 5 + for (i = 0; i < n; i++) for (k = 0; k < n; k++) s = s + m[i * n + k]; // kept: n is a variable + rt.put_n(s); rt.put_c(10); + rt.free(d*a); rt.free(d*b); rt.free(d*c); rt.free(d*m); rt.free(d*m15); rt.free(p); + return 0; +} -- cgit v1.2.3