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/bounds_prover.zc | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/programs/bounds_prover.zc (limited to 'tests/programs/bounds_prover.zc') 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; +} -- cgit v1.2.3