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

1 files changed, 19 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;
+}