feat(Boole): add verified algorithm examples

Cslib/Languages/Boole/examples/euclid_gcd.lean

@@ -0,0 +1,75 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Euclid's algorithm for GCD, with a spec stated via a helper function/predicate.
+--
+-- We use the subtraction-based variant of Euclid's algorithm to avoid `mod`, which currently
+-- tends to produce large verification conditions.
+--
+-- Divisibility/maximality are stated as axioms about `GCDSpec`.
+private def euclidGcdPgm : Strata.Program :=
+#strata
+program Boole;
+
+function GCDSpec(a : int, b : int) : int;
+function Divides(d : int, a : int) : bool;
+
+// Subtraction-based Euclid facts for `GCDSpec`.
+axiom (forall x : int :: GCDSpec(x, x) == x);
+axiom (forall x : int, y : int :: x > y && y > 0 ==> GCDSpec(x, y) == GCDSpec(x - y, y));
+axiom (forall x : int, y : int :: y > x && x > 0 ==> GCDSpec(x, y) == GCDSpec(x, y - x));
+
+// Spec helper: divisibility and maximality properties of the computed `d`.
+// The key idea is that callers can assume `free ensures` without having to verify them here.
+procedure GCDProperties(a : int, b : int, d : int) returns ()
+spec
+{
+  requires d == GCDSpec(a, b);
+  free ensures Divides(d, a) && Divides(d, b);
+  free ensures forall e : int :: (e >= 0 && Divides(e, a) && Divides(e, b)) ==> e <= d;
+}
+{};
+
+procedure EuclidGCD(a : int, b : int) returns (d : int)
+spec
+{
+  requires a > 0;
+  requires b > 0;
+  ensures d == GCDSpec(a, b);
+  ensures Divides(d, a) && Divides(d, b);
+  ensures forall e : int :: (e >= 0 && Divides(e, a) && Divides(e, b)) ==> e <= d;
+}
+{
+  var x : int;
+  var y : int;
+
+  x := a;
+  y := b;
+
+  while (x != y)
+    invariant x > 0
+    invariant y > 0
+    invariant GCDSpec(x, y) == GCDSpec(a, b)
+  {
+    if (x > y) {
+      x := x - y;
+    } else {
+      y := y - x;
+    }
+  }
+
+  d := x;
+
+  // Discharge the divisibility/maximality postconditions via the spec helper.
+  call GCDProperties(a, b, d);
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect euclidGcdPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata

Cslib/Languages/Boole/examples/insertion_sort.lean

@@ -0,0 +1,103 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- CLRS Chapter 1: Insertion Sort
+-- Pseudo-code adapted from CLRS book (3rd edition), page 18
+
+-- Pseudo-code:
+-- INSERTION-SORT(A)
+-- 1  for j = 2 to A.length
+-- 2      key = A[j]
+-- 3      // Insert A[j] into the sorted sequence A[1..j-1]
+-- 4      i = j - 1
+-- 5      while i > 0 and A[i] > key
+-- 6          A[i + 1] = A[i]
+-- 7          i = i - 1
+-- 8      A[i + 1] = key
+
+private def insertionSortPgm :=
+#strata
+program Boole;
+
+// An "array of ints" is a map from int to int
+type Array := Map int int;
+
+// Global array we'll sort
+var A : Array;
+var n : int; // length of A
+
+// Add axiom for length of A
+// function array_length(a: Array) : int { n }
+// axiom (array_length(A) == n);
+// [FEATURE REQUEST] Support native arrays
+
+
+procedure InsertionSort() returns ()
+spec
+{
+  modifies A;
+  // Adjacent-order formulation of sortedness (simpler VCs than ∀ i j, ...).
+  ensures forall k:int ::
+    0 <= k && k < n - 1 ==> A[k] <= A[k + 1];
+  // [FEATURE REQUEST] Support for Lean 4-style quantifiers
+  // -- ∀ k: int, 0 ≤ k ∧ k < n - 1 → A[k] ≤ A[k + 1]
+}
+{
+  var i : int;
+  var j : int;
+  var key : int;
+
+  if (n > 1) {
+    // CLRS-style insertion sort (0-based):
+    // for i = 1 to n-1
+    // [FEATURE REQUEST] For loop construct
+    i := 1;
+    while (i < n)
+      invariant 1 <= i && i <= n
+      invariant (
+        forall k:int ::
+          0 <= k && k < i - 1 ==> A[k] <= A[k + 1]
+      )
+    {
+      key := A[i];
+      j := i - 1;
+
+      // We do one shift outside the loop so that, inside the loop,
+      // the prefix `A[0..i]` is sorted (with `key` stored separately).
+      if (A[j] > key) {
+        A := A[j + 1 := A[j]];
+        j := j - 1;
+
+        while (j >= 0 && A[j] > key)
+          invariant -1 <= j && j < i
+          invariant (
+            forall k:int ::
+              0 <= k && k < i ==> A[k] <= A[k + 1]
+          )
+          invariant (
+            forall k:int :: j < k && k <= i ==> A[k] > key
+          )
+        {
+          A := A[j + 1 := A[j]];
+          j := j - 1;
+        }
+      }
+
+      A := A[j + 1 := key];
+      i := i + 1;
+    }
+  }
+};
+#end
+
+-- Optional: run the SMT-based pipeline if `cvc5` is on your `PATH`.
+-- Note: use `#eval!` if your dependency graph contains `sorry`.
+-- #eval! Strata.Boole.verify "cvc5" insertionSortPgm
+
+example : Strata.smtVCsCorrect insertionSortPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata

Cslib/Languages/Boole/examples/linear_search.lean

@@ -0,0 +1,45 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Linear search: return an index where `A[idx] == x`, or `-1` if not found.
+private def linearSearchPgm : Strata.Program :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+procedure LinearSearch(A : Array, n : int, x : int) returns (idx : int)
+spec
+{
+  requires n >= 0;
+  ensures (idx == -1 ==> forall k:int :: 0 <= k && k < n ==> A[k] != x);
+  ensures (idx != -1 ==> 0 <= idx && idx < n && A[idx] == x);
+}
+{
+  var i : int;
+
+  i := 0;
+  idx := -1;
+
+  while (i < n && idx == -1)
+    invariant 0 <= i && i <= n
+    invariant (idx == -1 ==> forall k:int :: 0 <= k && k < i ==> A[k] != x)
+    invariant (idx != -1 ==> 0 <= idx && idx < i && A[idx] == x)
+  {
+    if (A[i] == x) {
+      idx := i;
+    }
+    i := i + 1;
+  }
+};
+#end
+
+set_option maxHeartbeats 500000 in
+example : Strata.smtVCsCorrect linearSearchPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
+

Cslib/Languages/Boole/examples/prefix_sums.lean

@@ -0,0 +1,50 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Prefix sums.
+--
+-- Intended spec: `S[i] = Σ_{k<i} A[k]`. In Boole, we encode the summation via an
+-- uninterpreted function with recursive axioms.
+private def prefixSumsPgm : Strata.Program :=
+#strata
+program Boole;
+
+// Sum of the first `i` elements: `PrefixSum(A, i) = Σ_{k<i} A[k]`.
+function PrefixSum(A : Map int int, i : int) : int;
+
+axiom (forall A : Map int int :: PrefixSum(A, 0) == 0);
+axiom (forall A : Map int int, i : int ::
+  i > 0 ==> PrefixSum(A, i) == PrefixSum(A, i - 1) + A[i - 1]);
+
+procedure PrefixSums(A : Map int int, n : int) returns (S : Map int int)
+spec
+{
+  requires n >= 0;
+  ensures forall i : int :: 0 <= i && i <= n ==> S[i] == PrefixSum(A, i);
+}
+{
+  var i : int;
+
+  // Initialize S[0] = 0.
+  S := S[0 := 0];
+
+  i := 0;
+  while (i < n)
+    invariant 0 <= i && i <= n
+    invariant forall k : int :: 0 <= k && k <= i ==> S[k] == PrefixSum(A, k)
+  {
+    // Step: S[i+1] = S[i] + A[i].
+    S := S[i + 1 := S[i] + A[i]];
+    i := i + 1;
+  }
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect prefixSumsPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata

Cslib/Languages/Boole/examples/selection_sort.lean

@@ -0,0 +1,76 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- Selection sort.
+--
+-- This example uses a lightweight sortedness spec:
+--   `∀ k, 0 ≤ k ∧ k < n-1 → A[k] ≤ A[k+1]`
+-- instead of `∀ i j, i ≤ j → A[i] ≤ A[j]`, because it tends to generate
+-- simpler verification conditions.
+private def selectionSortPgm : Strata.Program :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+var A : Array;
+var n : int;
+
+procedure SelectionSort() returns ()
+spec
+{
+  modifies A;
+  // Adjacent-order sortedness.
+  ensures forall k:int :: 0 <= k && k < n - 1 ==> A[k] <= A[k + 1];
+}
+{
+  var i : int;
+  var j : int;
+  var m : int;
+  var tmp : int;
+
+  if (n > 1) {
+    i := 0;
+
+    while (i < n - 1)
+      invariant 0 <= i && i <= n - 1
+      // Prefix `A[0..i]` is sorted.
+      invariant forall k:int :: 0 <= k && k < i ==> A[k] <= A[k + 1]
+      // Every element already placed in the prefix is <= every element remaining in the suffix.
+      invariant forall p:int, q:int :: 0 <= p && p < i && i <= q && q < n ==> A[p] <= A[q]
+    {
+      m := i;
+      j := i + 1;
+
+      // Find an index `m` holding a minimum of `A[i..n-1]`.
+      while (j < n)
+        invariant i <= m && m < n
+        invariant i < j && j <= n
+        invariant forall k:int :: i <= k && k < j ==> A[m] <= A[k]
+      {
+        if (A[j] < A[m]) {
+          m := j;
+        }
+        j := j + 1;
+      }
+
+      if (m != i) {
+        tmp := A[i];
+        A := A[i := A[m]];
+        A := A[m := tmp];
+      }
+
+      i := i + 1;
+    }
+  }
+};
+#end
+
+set_option maxHeartbeats 1000000 in
+example : Strata.smtVCsCorrect selectionSortPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata