feat(Boole): add verified queue examples

Author: Robertboy18

Cslib/Languages/Boole/examples/circular_queue.lean

@@ -0,0 +1,141 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+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 encode
+-- wraparound with conditionals 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 `(i + 1) mod n`, axiomatized without using `mod`.
+function NextIndex(i : int, n : int) : int;
+
+axiom (∀ i : int, n : int ::
+  n > 0 && 0 <= i && i < n ==> 0 <= NextIndex(i, n) && NextIndex(i, n) < n);
+axiom (∀ n : int :: n > 0 ==> NextIndex(n - 1, n) == 0);
+axiom (∀ i : int, n : int ::
+  n > 0 && 0 <= i && i + 1 < n ==> NextIndex(i, n) == 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
+
+example : Strata.smtVCsCorrect circularQueuePgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata

Cslib/Languages/Boole/examples/deque_array_based.lean

@@ -0,0 +1,143 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+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;
+};
+
+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
+
+example : Strata.smtVCsCorrect dequeArrayPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata