feat(Boole): Bring Boole sandbox to Lean 4.29 and add queue examples

.github/workflows/lean_action_ci.yml

@@ -14,14 +14,24 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
-      - name: Set TEST_ARGS manually
-        run: |
-          echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV
-        shell: bash
       - uses: leanprover/lean-action@v1
         with:
-          build-args: "--wfail --iofail"
-          test-args: "--wfail --iofail"
+          build: false
+          test: false
+          lint: false
+      - name: Set up cvc5
+        run: |
+          lake update cvc5
+          lake build @cvc5
+          cvc5_bin="$(find .lake/packages/cvc5 -maxdepth 5 -type f -name cvc5 -path '*/bin/cvc5' -print -quit)"
+          test -n "$cvc5_bin"
+          echo "$(dirname "$cvc5_bin")" >> "$GITHUB_PATH"
+      - name: Build
+        run: lake build --wfail --iofail
+      - name: Test
+        run: lake test --wfail --iofail
+      - name: Lint
+        run: lake lint
       - name: "lake exe mk_all --check"
         run: |
           set -e

Cslib/Languages/Boole/examples/circular_queue.lean

@@ -0,0 +1,141 @@
+import StrataBoole.MetaVerifier
+import Smt
+
+------------------------------------------------------------
+namespace Strata
+
+-- Circular-buffer queue.
+--
+-- The queue is represented by an array `Q`, a capacity `n`, a head pointer, a
+-- tail pointer, and a live element count.  Unlike `queue_array_based.lean`,
+-- `head` and `tail` wrap back to zero when they reach the capacity.  We model
+-- that wraparound with a small `NextIndex` function instead of `mod`, so the
+-- verification conditions remain simple arithmetic plus map-update reasoning.
+private def circularQueuePgm :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+// `NextIndex(i, n)` is the usual circular-buffer successor:
+// `if i + 1 == n then 0 else i + 1`.
+//
+function NextIndex(i : int, n : int) : int {
+  if i + 1 == n then 0 else i + 1
+}
+
+var Q     : Array;
+var n     : int;
+var head  : int;
+var tail  : int;
+var count : int;
+
+// Initialize an empty circular queue.
+procedure CircularQueueInit(cap : int) returns ()
+spec
+{
+  requires cap > 0;
+  modifies n;
+  modifies head;
+  modifies tail;
+  modifies count;
+
+  ensures n == cap;
+  ensures head == 0;
+  ensures tail == 0;
+  ensures count == 0;
+}
+{
+  n := cap;
+  head := 0;
+  tail := 0;
+  count := 0;
+};
+
+// Return whether the circular queue is empty.
+procedure CircularQueueEmpty() returns (b : bool)
+spec
+{
+  ensures (b ==> count == 0);
+  ensures (count == 0 ==> b);
+}
+{
+  if (count == 0) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Return whether the circular queue is full.
+procedure CircularQueueFull() returns (b : bool)
+spec
+{
+  ensures (b ==> count == n);
+  ensures (count == n ==> b);
+}
+{
+  if (count == n) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Add `x` at the current tail position and advance the tail pointer, wrapping
+// to zero when the insertion occurs at the last array slot.
+procedure CircularEnqueue(x : int) returns ()
+spec
+{
+  requires n > 0;
+  requires 0 <= head && head < n;
+  requires 0 <= tail && tail < n;
+  requires 0 <= count && count < n;
+  modifies Q;
+  modifies tail;
+  modifies count;
+
+  ensures count == old(count) + 1;
+  ensures Q[old(tail)] == x;
+  ensures 0 <= tail && tail < n;
+  ensures (
+    ∀ i:int .
+      0 <= i && i < n && i != old(tail) ==> Q[i] == old(Q[i])
+  );
+}
+{
+  Q := Q[tail := x];
+  tail := NextIndex(tail, n);
+  count := count + 1;
+};
+
+// Remove and return the current head element, then advance the head pointer
+// with the same wraparound convention.
+procedure CircularDequeue() returns (x : int)
+spec
+{
+  requires n > 0;
+  requires 0 <= head && head < n;
+  requires 0 <= tail && tail < n;
+  requires 0 < count && count <= n;
+  modifies head;
+  modifies count;
+
+  ensures x == old(Q[old(head)]);
+  ensures count == old(count) - 1;
+  ensures 0 <= head && head < n;
+}
+{
+  x := Q[head];
+  head := NextIndex(head, n);
+  count := count - 1;
+};
+
+#end
+
+theorem circularQueuePgm_smtVCsCorrect :
+    Strata.smtVCsCorrectBoole circularQueuePgm := by
+  gen_smt_vcs_boole
+  all_goals (first | smt +mono | omega | trivial | grind)
+
+end Strata

Cslib/Languages/Boole/examples/deque_array_based.lean

@@ -0,0 +1,146 @@
+import StrataBoole.MetaVerifier
+import Smt
+
+------------------------------------------------------------
+namespace Strata
+
+-- Array-backed double-ended queue.
+--
+-- A deque supports insertion and removal at both ends.  This example uses a
+-- bounded, non-circular array model: live elements occupy indices
+-- `front .. back - 1`, with `front == back` meaning empty.  The front can move
+-- left and the back can move right, so `PushFront` requires spare space before
+-- `front` and `PushBack` requires spare space after `back`.
+--
+-- The circular-buffer queue example covers wraparound behavior separately.
+-- Keeping this deque non-circular makes the specifications direct and lets the
+-- example focus on four endpoint operations, `old(...)`, and frame properties.
+private def dequeArrayPgm :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+var D     : Array;
+var n     : int;
+var front : int;
+var back  : int;
+
+// Initialize an empty deque.  Starting both endpoints at `start` leaves room
+// to grow in either direction if `0 < start < cap`.
+procedure DequeInit(cap : int, start : int) returns ()
+spec
+{
+  requires cap > 0;
+  requires 0 <= start && start <= cap;
+  modifies n;
+  modifies front;
+  modifies back;
+
+  ensures n == cap;
+  ensures front == start;
+  ensures back == start;
+}
+{
+  n := cap;
+  front := start;
+  back := start;
+};
+
+// Return whether the deque has no live elements.
+procedure DequeEmpty() returns (b : bool)
+spec
+{
+  ensures (b ==> front == back);
+  ensures (front == back ==> b);
+}
+{
+  if (front == back) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Add `x` to the back of the deque.
+procedure PushBack(x : int) returns ()
+spec
+{
+  requires 0 <= front && front <= back;
+  requires back < n;
+  modifies D;
+  modifies back;
+
+  ensures back == old(back) + 1;
+  ensures D[old(back)] == x;
+  ensures (
+    ∀ i:int .
+      old(front) <= i && i < old(back) ==> D[i] == old(D[i])
+  );
+}
+{
+  D := D[back := x];
+  back := back + 1;
+};
+
+// Remove and return the last element of the deque.
+procedure PopBack() returns (x : int)
+spec
+{
+  requires front < back;
+  modifies back;
+
+  ensures back == old(back) - 1;
+  ensures x == old(D[old(back) - 1]);
+  ensures front <= back;
+}
+{
+  back := back - 1;
+  x := D[back];
+};
+
+// Add `x` to the front of the deque.
+procedure PushFront(x : int) returns ()
+spec
+{
+  requires 0 < front && front <= back;
+  requires back <= n;
+  modifies D;
+  modifies front;
+
+  ensures front == old(front) - 1;
+  ensures D[front] == x;
+  ensures (
+    ∀ i:int .
+      old(front) <= i && i < old(back) ==> D[i] == old(D[i])
+  );
+}
+{
+  front := front - 1;
+  D := D[front := x];
+};
+
+// Remove and return the first element of the deque.
+procedure PopFront() returns (x : int)
+spec
+{
+  requires front < back;
+  modifies front;
+
+  ensures front == old(front) + 1;
+  ensures x == old(D[old(front)]);
+  ensures front <= back;
+}
+{
+  x := D[front];
+  front := front + 1;
+};
+
+#end
+
+theorem dequeArrayPgm_smtVCsCorrect :
+    Strata.smtVCsCorrectBoole dequeArrayPgm := by
+  gen_smt_vcs_boole
+  all_goals (first | smt +mono | omega | trivial | grind)
+
+end Strata