From 5df3164178dcf224ff331fb57236b02c37575e49 Mon Sep 17 00:00:00 2001
From: robert <robujsph2001@gmail.com>
Date: Sun, 3 May 2026 03:37:05 +0000
Subject: [PATCH 1/2] feat(Boole): add verified queue examples

---
 .../Boole/examples/circular_queue.lean        | 141 +++++++++++++++++
 .../Boole/examples/deque_array_based.lean     | 144 ++++++++++++++++++
 .../Boole/examples/queue_array_based.lean     | 124 +++++++++++++++
 .../Boole/examples/stack_array_based.lean     |  10 +-
 lake-manifest.json                            |  90 +++++------
 lakefile.toml                                 |  12 +-
 lean-toolchain                                |   2 +-
 7 files changed, 464 insertions(+), 59 deletions(-)
 create mode 100644 Cslib/Languages/Boole/examples/circular_queue.lean
 create mode 100644 Cslib/Languages/Boole/examples/deque_array_based.lean
 create mode 100644 Cslib/Languages/Boole/examples/queue_array_based.lean

diff --git a/Cslib/Languages/Boole/examples/circular_queue.lean b/Cslib/Languages/Boole/examples/circular_queue.lean
new file mode 100644
index 000000000..5d37d5929
--- /dev/null
+++ b/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 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 `(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
diff --git a/Cslib/Languages/Boole/examples/deque_array_based.lean b/Cslib/Languages/Boole/examples/deque_array_based.lean
new file mode 100644
index 000000000..3a9f947c3
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/deque_array_based.lean
@@ -0,0 +1,144 @@
+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;
+};
+
+// 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
+
+example : Strata.smtVCsCorrect dequeArrayPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/queue_array_based.lean b/Cslib/Languages/Boole/examples/queue_array_based.lean
new file mode 100644
index 000000000..34a752084
--- /dev/null
+++ b/Cslib/Languages/Boole/examples/queue_array_based.lean
@@ -0,0 +1,124 @@
+import Strata.MetaVerifier
+
+------------------------------------------------------------
+namespace Strata
+
+-- CLRS Chapter 10: Queues (array implementation).
+--
+-- This version models a bounded, non-circular FIFO queue.  The queue contents
+-- occupy indices `head .. tail - 1`; `head == tail` means empty.  Unlike a
+-- circular-buffer implementation, this example does not wrap `head` or `tail`
+-- modulo the capacity.  That keeps the arithmetic simple and focuses the
+-- verification on global variables, `modifies` clauses, and `old(...)`
+-- postconditions.
+private def queueArrayPgm :=
+#strata
+program Boole;
+
+type Array := Map int int;
+
+// Global queue storage, capacity, and head/tail pointers.
+//
+// Valid live elements are stored in Q[head], Q[head + 1], ..., Q[tail - 1].
+// The next enqueue writes at Q[tail].  The next dequeue reads from Q[head].
+var Q    : Array;
+var n    : int;
+var head : int;
+var tail : int;
+
+// Initialize an empty queue with capacity `cap`.
+procedure QueueInit(cap : int) returns ()
+spec
+{
+  requires cap >= 0;
+  modifies n;
+  modifies head;
+  modifies tail;
+  ensures n == cap;
+  ensures head == 0;
+  ensures tail == 0;
+}
+{
+  n := cap;
+  head := 0;
+  tail := 0;
+};
+
+// Return whether the queue is empty.
+//
+// The postconditions state both directions of the Boolean result:
+// if `b` is true then the queue is empty, and if the queue is empty then `b`
+// is true.  Together these characterize `b` as `(head == tail)`.
+procedure QueueEmpty() returns (b : bool)
+spec
+{
+  ensures (b ==> head == tail);
+  ensures (head == tail ==> b);
+}
+{
+  if (head == tail) {
+    b := true;
+  } else {
+    b := false;
+  }
+};
+
+// Add `x` to the back of the queue.
+//
+// Preconditions require a well-formed, non-full queue segment:
+// `0 <= head <= tail < n`.  The `modifies` clause records that this operation
+// changes the queue array and the tail pointer, but not the head pointer or
+// capacity.  The postconditions use `old(...)` to relate the post-state to the
+// pre-state:
+// * `tail` advances by one;
+// * the old tail slot now stores `x`;
+// * all previously live elements are preserved.
+procedure Enqueue(x : int) returns ()
+spec
+{
+  requires 0 <= head;
+  requires head <= tail;
+  requires tail < n;
+  modifies Q;
+  modifies tail;
+
+  ensures tail == old(tail) + 1;
+  ensures Q[old(tail)] == x;
+  ensures (
+    ∀ i:int .
+      old(head) <= i && i < old(tail) ==> Q[i] == old(Q[i])
+  );
+}
+{
+  Q := Q[tail := x];
+  tail := tail + 1;
+};
+
+// Remove and return the front element of the queue.
+//
+// The non-empty precondition `head < tail` guarantees that `Q[head]` is a live
+// element.  Dequeue changes only the head pointer: the array contents and tail
+// are not modified.  The returned value is the element that was at the old head,
+// and the post-state head advances by one.
+procedure Dequeue() returns (x : int)
+spec
+{
+  requires head < tail;
+  modifies head;
+
+  ensures head == old(head) + 1;
+  ensures x == old(Q[old(head)]);
+  ensures head <= tail;
+}
+{
+  x := Q[head];
+  head := head + 1;
+};
+
+#end
+
+example : Strata.smtVCsCorrect queueArrayPgm := by
+  gen_smt_vcs
+  all_goals grind
+
+end Strata
diff --git a/Cslib/Languages/Boole/examples/stack_array_based.lean b/Cslib/Languages/Boole/examples/stack_array_based.lean
index ad337b5a9..07779e133 100644
--- a/Cslib/Languages/Boole/examples/stack_array_based.lean
+++ b/Cslib/Languages/Boole/examples/stack_array_based.lean
@@ -1,5 +1,4 @@
 import Strata.MetaVerifier
-import Smt
 
 ------------------------------------------------------------
 namespace Strata
@@ -107,9 +106,6 @@ spec
 
 #end
 
--- will verify once pr in Strata is merged
--- #eval Strata.Boole.verify "cvc5" stackArrayPgm
-
--- example : Strata.smtVCsCorrect stackArrayPgm := by
---   gen_smt_vcs
---   all_goals (smt +mono)
+example : Strata.smtVCsCorrect stackArrayPgm := by
+  gen_smt_vcs
+  all_goals grind
diff --git a/lake-manifest.json b/lake-manifest.json
index 7e3fb0017..263471f09 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,61 +1,41 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/ufmg-smite/lean-smt",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "2be8f61e7ae296b7e700fccc29672caa2a090b07",
-   "name": "smt",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "boole",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/strata-org/Strata",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "e3c375fad6ad42e91b13ebb8d09ea0077fcf9ba2",
-   "name": "Strata",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover-community/mathlib4",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
+   "rev": "5e932f97dd25535344f80f9dd8da3aab83df0fe6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.29.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/abdoo8080/lean-cvc5.git",
+  {"url": "https://github.com/ufmg-smite/lean-smt",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0cfacc8dc13402ccb737b17e96ea6c012d5ef866",
-   "name": "cvc5",
+   "rev": "7d1d8239e78daa5197f9a71948776c4627049f5f",
+   "name": "smt",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "0cfacc8",
-   "inherited": true,
+   "inputRev": "main",
+   "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/abdoo8080/lean-auto.git",
+  {"url": "https://github.com/strata-org/Strata",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0828adf8462833fec839a0506c5db8ee10d55e87",
-   "name": "auto",
+   "rev": "f714237cba5c0d67a066344e3bc71e73a8ef965b",
+   "name": "Strata",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
+   "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "48d5698bc464786347c1b0d859b18f938420f060",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
+   "rev": "4dd0959c44d1af0462bd604d0f87c5781307d709",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
+   "inputRev": "v0.0.95+lean-v4.29.1",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
+   "rev": "7152850e7b216a0d409701617721b6e469d34bf6",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -105,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "756e3321fd3b02a85ffda19fef789916223e578c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,11 +105,31 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
+   "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.29.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/abdoo8080/lean-cvc5.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "4ecae27437dc9ae97500fcdbbc9ccb771852004d",
+   "name": "cvc5",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "4ecae27",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/lean-auto.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5c4433f6047a918a85439b2d6ab8cd2639621110",
+   "name": "auto",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5c4433f",
    "inherited": true,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.lean"}],
  "name": "cslib",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 9817cf391..262694cee 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -13,11 +13,6 @@ weak.linter.pythonStyle = false
 weak.linter.checkInitImports = false
 weak.linter.allScriptsDocumented = false
 
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-rev = "v4.27.0"
-
 [[require]]
 name = "Strata"
 git = "https://github.com/strata-org/Strata"
@@ -26,7 +21,12 @@ rev = "main"
 [[require]]
 name = "smt"
 git = "https://github.com/ufmg-smite/lean-smt"
-rev = "boole"
+rev = "main"
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "v4.29.1"
 
 [[lean_lib]]
 name = "Cslib"
diff --git a/lean-toolchain b/lean-toolchain
index 5249182c0..05a063ac3 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.29.1
\ No newline at end of file

From 96bb95079cc5bd985037bb4a54deeecd47c3a31a Mon Sep 17 00:00:00 2001
From: robert <robujsph2001@gmail.com>
Date: Mon, 4 May 2026 20:39:42 +0000
Subject: [PATCH 2/2] docs(Boole): explain circular queue successor helper

---
 Cslib/Languages/Boole/examples/circular_queue.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/Boole/examples/circular_queue.lean b/Cslib/Languages/Boole/examples/circular_queue.lean
index 5d37d5929..90a61d61f 100644
--- a/Cslib/Languages/Boole/examples/circular_queue.lean
+++ b/Cslib/Languages/Boole/examples/circular_queue.lean
@@ -16,7 +16,13 @@ program Boole;
 
 type Array := Map int int;
 
-// `NextIndex(i, n)` is `(i + 1) mod n`, axiomatized without using `mod`.
+// `NextIndex(i, n)` is the usual circular-buffer successor:
+// `if i + 1 == n then 0 else i + 1`.
+//
+// It is axiomatized here because both obvious executable encodings currently
+// get in the way of this small example: `mod` is not yet convenient in these
+// VCs, and the direct Boole if/else form triggers an integer-valued `ite`
+// elaboration issue in the generated VCs.
 function NextIndex(i : int, n : int) : int;
 
 axiom (∀ i : int, n : int ::