wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, affine i*n+k); unbuilt and untestedwork/prover

2 files changed, 59 insertions, 0 deletions

diff --git a/tests/programs/bounds_prover.zc b/tests/programs/bounds_prover.zc
new file mode 100644
index 0000000..1b3e3ca
--- /dev/null
+++ b/tests/programs/bounds_prover.zc
@@ -0,0 +1,19 @@
+namespace;
+include rt;
+
+// the new loop proofs drop checks that cannot fail and keep the ones that can:
+// the last loop runs one past a block of 6 and has to fault there.
+int main() {
+	int i, k, s = 0;
+	fixed int[?] a = rt.new(fixed int[?], 8);
+	fixed int[?] m = rt.new(fixed int[?], 16);
+	fixed int[?] c = rt.new(fixed int[?], 6);
+	for (i = 0; i < len(a); i++) a[i] = i;
+	for (i = 0; i < len(a); i++) s = s + a[i];
+	rt.put_n(s); rt.put_c(10);
+	for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) m[i * 4 + k] = i * k;
+	s = 0; for (i = 0; i < len(m); i++) s = s + m[i];
+	rt.put_n(s); rt.put_c(10);
+	for (i = 0; i < 7; i++) { rt.put_n(i); rt.put_c(32); c[i] = i; }
+	return 0;
+}
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;
+}