From 3e5c7aba4f1844306f38882374f88afc45f51d3a Mon Sep 17 00:00:00 2001
From: Abhinav Peri <abhinavperi16@gmail.com>
Date: Wed, 3 Dec 2025 23:45:44 -0600
Subject: [PATCH] adding public tests

---
 proofs/pascal_triangle.dfy    |  7 +++++++
 proofs/prefix_sum.dfy         | 31 +++++++++++++++++++++++++++++++
 testcases/pascal_triangle.dfy |  8 ++++++++
 testcases/prefix_sum.dfy      |  6 ++++++
 4 files changed, 52 insertions(+)
 create mode 100644 proofs/pascal_triangle.dfy
 create mode 100644 proofs/prefix_sum.dfy
 create mode 100644 testcases/pascal_triangle.dfy
 create mode 100644 testcases/prefix_sum.dfy

diff --git a/proofs/pascal_triangle.dfy b/proofs/pascal_triangle.dfy
new file mode 100644
index 0000000..aa13d80
--- /dev/null
+++ b/proofs/pascal_triangle.dfy
@@ -0,0 +1,7 @@
+include "../testcases/pascal_triangle.dfy"
+
+lemma {:induction false} combination_symmetry(n: nat, k: nat)
+    requires k <= n
+    ensures combination(n, k) == combination(n, n - k)
+{
+}
\ No newline at end of file
diff --git a/proofs/prefix_sum.dfy b/proofs/prefix_sum.dfy
new file mode 100644
index 0000000..5cb8c94
--- /dev/null
+++ b/proofs/prefix_sum.dfy
@@ -0,0 +1,31 @@
+include "../testcases/prefix_sum.dfy"
+
+// --- tiny helpers ----------------------------------------------------------
+
+lemma sum_seq_append(a: seq<int>, b: seq<int>)
+  ensures sum_seq(a + b) == sum_seq(a) + sum_seq(b)
+  decreases a
+{
+
+}
+
+
+// snoc means appending one element to the end of a sequence
+// prefix[0..i+1] = prefix[0..i] + [arr[i]]
+// use the append lemma above
+lemma sum_seq_prefix_snoc(arr: seq<int>, i: int)
+  requires 0 <= i < |arr|
+  ensures  sum_seq(arr[0..i+1]) == sum_seq(arr[0..i]) + arr[i]
+{
+
+}
+
+// Write out the algorithm for a prefix sum. Use the lemma above
+// to prove that your algorithm creates the next element in the prefix sum.
+
+method prefix_sum_impl(arr: seq<int>) returns (out: seq<int>)
+  ensures |out| == |arr|
+  ensures forall i :: 0 <= i < |arr| ==> out[i] == sum_seq(arr[0..i+1])
+{
+
+}
\ No newline at end of file
diff --git a/testcases/pascal_triangle.dfy b/testcases/pascal_triangle.dfy
new file mode 100644
index 0000000..ef671fe
--- /dev/null
+++ b/testcases/pascal_triangle.dfy
@@ -0,0 +1,8 @@
+function {:induction false} combination(n: nat, k: nat): (result: nat)
+    requires k <= n
+    decreases n, k
+{
+    if k == 0 || k == n then 1
+    else if k > n then 0
+    else combination(n - 1, k - 1) + combination(n - 1, k)
+}
\ No newline at end of file
diff --git a/testcases/prefix_sum.dfy b/testcases/prefix_sum.dfy
new file mode 100644
index 0000000..846d9d9
--- /dev/null
+++ b/testcases/prefix_sum.dfy
@@ -0,0 +1,6 @@
+// --- spec used in proofs ---------------------------------------------------
+function {:induction false} sum_seq(s: seq<int>): int
+  decreases s
+{
+  if |s| == 0 then 0 else s[0] + sum_seq(s[1..])
+}