From 61063dd2f56e99ae9ef3c8071f4c3848fcf78b36 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Tue, 3 Feb 2026 08:25:24 +0100
Subject: [PATCH] [documentation]: document the `splitwhile` tactic

---
 doc/tactics/splitwhile.rst | 93 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 93 insertions(+)
 create mode 100644 doc/tactics/splitwhile.rst

diff --git a/doc/tactics/splitwhile.rst b/doc/tactics/splitwhile.rst
new file mode 100644
index 000000000..81b680a07
--- /dev/null
+++ b/doc/tactics/splitwhile.rst
@@ -0,0 +1,93 @@
+========================================================================
+Tactic: ``splitwhile`` Tactic
+========================================================================
+
+The ``splitwhile`` tactic applies to program-logic goals where the program
+contains a ``while`` loop.
+
+It belongs to a family of tactics that operate by rewriting the program
+into a semantically equivalent form. More precisely, given a loop of the
+form::
+
+  while (b) { c }
+
+applying ``splitwhile`` with a splitting condition ``S`` rewrites the loop
+into a structure where the execution is decomposed into two successive
+loops.
+
+In a nutshell, the original loop is split into:
+
+- a first loop that executes iterations only while both the loop guard
+  ``b`` and the splitting condition ``S`` hold,
+
+- followed by a second loop that executes the remaining iterations of the
+  original loop under the standard guard ``b``.
+
+Concretely, the loop is rewritten into an equivalent program of the shape::
+
+  while (b /\ S) { c };
+  while (b)      { c }
+
+This transformation allows the user to reason separately about an initial
+phase of the loop execution where ``S`` is maintained, and a second phase
+that accounts for the rest of the iterations.
+
+Since this is a semantic-preserving program transformation, ``splitwhile``
+can be used in any program component, independently of the surrounding
+logic (Hoare logic, probabilistic Hoare logic, relational logics, etc.).
+
+The splitting condition must be supplied explicitly; it is not inferred
+automatically.
+
+------------------------------------------------------------------------
+Syntax
+------------------------------------------------------------------------
+
+The general form of the tactic is:
+
+.. admonition:: Syntax
+
+  ``splitwhile {side}? {codepos} : ({expr})``
+
+Here:
+
+- ``{expr}`` is the splitting condition used to restrict the first phase of
+  the loop execution.
+
+- ``{codepos}`` specifies the position of the ``while`` loop in the program
+  that should be rewritten.
+
+- ``{side}`` is optional and is used in relational goals to specify on
+  which program the transformation should be applied (left or right). If
+  omitted, the tactic applies to the single program under consideration.
+
+The following example shows ``splitwhile`` on a Hoare goal. The program
+increments ``x`` until it reaches ``10``. We split the loop into two phases:
+an initial phase where ``x < 5`` holds, and then the remaining iterations.
+
+.. ecproof::
+
+   require import AllCore.
+
+   module M = {
+     proc up_to_10(x : int) : int = {
+       while (x < 10) {
+         x <- x + 1;
+       }
+       return x;
+     }
+   }.
+ 
+   lemma up_to_10_correct :
+     hoare [ M.up_to_10 : true ==> res = 10 ].
+   proof.
+     proc.
+     (*$*)
+     (* Split the loop at its position into:
+        while (x < 10 /\ x < 5) { x <- x + 1 };
+        while (x < 10)          { x <- x + 1 } *)
+     splitwhile 1 : (x < 5).
+ 
+     (* The goal is the same, but with the program rewritten. *)
+     admit.
+   qed.