From 9dc1dc39b737768e99df27b5a3a3c871c8a30ba1 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 2 Feb 2026 22:13:57 +0100 Subject: [PATCH 1/3] [documentation]: document `while` tactic --- doc/tactics/while.rst | 132 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 132 insertions(+) create mode 100644 doc/tactics/while.rst diff --git a/doc/tactics/while.rst b/doc/tactics/while.rst new file mode 100644 index 0000000000..d7d32ff4b1 --- /dev/null +++ b/doc/tactics/while.rst @@ -0,0 +1,132 @@ +======================================================================== +Tactic: ``while`` +======================================================================== + +The ``while`` tactic applies to program-logic goals where the next +statement to reason about is a ``while`` loop. + +Applying ``while`` replaces the original goal with proof obligations that let +you reason about the loop via an invariant (and, in some variants, a +termination variant). Intuitively, you prove that the invariant is preserved +by one iteration of the loop, and you then use the invariant to justify what +follows once the loop condition becomes false. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Variant: Hoare logic +------------------------------------------------------------------------ + +.. admonition:: Syntax + + ``while ({formula})`` + +The formula is a loop invariant. It may reference variables of the program. + +Applying this form of ``while`` generates (at least) the following goals: + +- **Preservation goal (one iteration):** assuming the invariant holds and the + loop condition is true, executing the loop body re-establishes the invariant. + +- **Exit/continuation goal:** you must show that the invariant holds when the + loop is entered, and that when the loop condition becomes false, the + invariant is strong enough to derive the desired postcondition. + +.. ecproof:: + :title: Hoare logic example + + require import AllCore. + + module M = { + proc sumsq(n : int) : int = { + var x, i; + x <- 0; + i <- 0; + while (i < n) { + x <- x + (i + 1); + i <- i + 1; + } + return x; + } + }. + + lemma ex_while_hl (n : int) : + hoare [M.sumsq : 0 <= n ==> 0 <= res]. + proof. + proc. + (*$*) while (0 <= i <= n /\ 0 <= x). + - admit. + - admit. + qed. + +------------------------------------------------------------------------ +Variant: Probabilistic relational Hoare logic (one-sided) +------------------------------------------------------------------------ + +.. admonition:: Syntax + + ``while {side} {formula} {expr}`` + +Here `{formula}` is a relational invariant, and `{expr}` is an integer-valued +termination variant. This variant applies when the designated program by +``{side}`` ends with a `while` loop. + +Applying this form of ``while`` generates two main goals: + +- **Loop-body goal (designated side):** assuming the invariant holds and the + loop condition is true, executing the loop body re-establishes the + invariant and decreases the variant. + +- **Remaining relational goal:** the loop is removed from the designated + program, and the postcondition is strengthened with the invariant together + with pure logical conditions connecting loop exit to the desired + postcondition. + +.. ecproof:: + :title: Relational example (shape) + + require import AllCore. + + module M = { + proc sumsq(n : int) : int = { + var x, i; + x <- 0; + i <- 0; + while (i < n) { + x <- x + (i + 1); + i <- i + 1; + } + return x; + } + }. + + lemma ex_while_prhl : + equiv [ M.sumsq ~ M.sumsq : ={n} ==> res{1} = res{2} ]. + proof. + proc. + (*$*) while{1} (true) (0). + - admit. + - admit. + qed. + +------------------------------------------------------------------------ +Variant: Probabilistic Hoare logic +------------------------------------------------------------------------ + +.. admonition:: Syntax + + ``while {formula} {expr}`` + +Here ``{formula}`` is an invariant and ``{expr}`` is an integer termination +variant. + +At a high level, this variant generates obligations analogous to the +designated relational case, but for a single program: + +- a probabilistic goal for the loop body showing preservation of the + invariant and strict progress of the variant, and + +- a remaining goal for the code before the loop, whose postcondition is + strengthened with the invariant plus pure logical conditions that connect + loop exit to the desired postcondition. From 47800cccc0e585f911bfb39b2441bb091730307f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Dupressoir?= Date: Sat, 21 Feb 2026 13:57:55 +0000 Subject: [PATCH 2/3] stack some simple edits --- doc/tactics/while.rst | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/doc/tactics/while.rst b/doc/tactics/while.rst index d7d32ff4b1..978525a420 100644 --- a/doc/tactics/while.rst +++ b/doc/tactics/while.rst @@ -7,9 +7,9 @@ statement to reason about is a ``while`` loop. Applying ``while`` replaces the original goal with proof obligations that let you reason about the loop via an invariant (and, in some variants, a -termination variant). Intuitively, you prove that the invariant is preserved -by one iteration of the loop, and you then use the invariant to justify what -follows once the loop condition becomes false. +termination variant). Intuitively, you prove that the invariant is initially +true, is preserved by one iteration of the loop, and you then use the invariant +to justify what follows once the loop condition becomes false. .. contents:: :local: @@ -22,7 +22,9 @@ Variant: Hoare logic ``while ({formula})`` -The formula is a loop invariant. It may reference variables of the program. +The formula is a loop invariant that must hold whenever the loop condition is +evaluated (at the start of each iteration). It may reference variables of the +program. Applying this form of ``while`` generates (at least) the following goals: @@ -69,14 +71,14 @@ Variant: Probabilistic relational Hoare logic (one-sided) ``while {side} {formula} {expr}`` Here `{formula}` is a relational invariant, and `{expr}` is an integer-valued -termination variant. This variant applies when the designated program by +termination variant. This variant applies when the program designated by ``{side}`` ends with a `while` loop. Applying this form of ``while`` generates two main goals: - **Loop-body goal (designated side):** assuming the invariant holds and the loop condition is true, executing the loop body re-establishes the - invariant and decreases the variant. + invariant and decreases the variant with probability 1. - **Remaining relational goal:** the loop is removed from the designated program, and the postcondition is strengthened with the invariant together From 0370468c0b808b0de955908878f89c3b2456d4fd Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 27 Feb 2026 13:01:46 +0100 Subject: [PATCH 3/3] add phoare (<=) bound variant --- doc/tactics/while.rst | 116 ++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 113 insertions(+), 3 deletions(-) diff --git a/doc/tactics/while.rst b/doc/tactics/while.rst index 978525a420..9a0992fbb3 100644 --- a/doc/tactics/while.rst +++ b/doc/tactics/while.rst @@ -113,14 +113,82 @@ Applying this form of ``while`` generates two main goals: qed. ------------------------------------------------------------------------ -Variant: Probabilistic Hoare logic +Variant: Probabilistic Hoare logic with (<=) bound ------------------------------------------------------------------------ .. admonition:: Syntax - ``while {formula} {expr}`` + `while {formula}` -Here ``{formula}`` is an invariant and ``{expr}`` is an integer termination +Here `{formula}` is a loop invariant. + +This variant essentially proceeds by coinduction on the number of iterations. +A non-trivial application of this variant relies on the probability bound +depending on variables being modified by the loop. This can be achieved +by using `conseq` to change the bound. + +The generated goals are as follows: + +- An induction step, where you need to show that adding one more iteration + before a statement preserving the invariant with the bound also preserves + the invariant with the bound. + +- A case where you show that the invariant holds to start with, + and that the bound becomes `1%r` when the loop condition becomes false. + +.. ecproof:: + :title: Probabilistic Hoare logic example (shape) + + require import AllCore DBool. + + module M = { + proc p() = { + var r, f; + r <- false; + f <- false; + while (!r && !f) { + f <$ {0,1}; + r <$ {0,1}; + } + return r && !f; + } + }. + + lemma L: phoare[M.p: true==> res] <= (1%r/3%r). + proof. + proc. + sp. + conseq (: : <= (if (!f) then (if (!r) then (1%r/3%r) else 1%r) else 0%r)). + - smt(). + (*$*) while true. + - move => IH. + conseq (: true ==> _: <= (1%r/3%r)). + + smt(). + seq 1: f (1%r/2%r) 0%r (1%r/2%r) (2%r/3%r) => //. + + seq 1: true _ 0%r 0%r _ f => //. + * auto. + conseq IH. + smt(). + + rnd; auto; rewrite dboolE => //. + seq 1: r (1%r/2%r) 1%r (1%r/2%r) (1%r/3%r) (!f) => //. + + auto. + + rnd; auto; rewrite dboolE => //. + + rnd; auto; rewrite dboolE => //. + conseq IH. + smt(). + auto. + smt(). + qed. + +------------------------------------------------------------------------ +Variant: Probabilistic Hoare logic with strict variant +------------------------------------------------------------------------ + +.. admonition:: Syntax + + `while {formula} {expr}` + +Here `{formula}` is an invariant and `{expr}` is an integer termination variant. At a high level, this variant generates obligations analogous to the @@ -132,3 +200,45 @@ designated relational case, but for a single program: - a remaining goal for the code before the loop, whose postcondition is strengthened with the invariant plus pure logical conditions that connect loop exit to the desired postcondition. + +.. ecproof:: + require import AllCore DBool. + + module M = { + proc p(b, e) = { + var r; + r <- 1; + while (0 < e) { + r <- r * b; + e <- e - 1; + } + return r; + } + }. + + lemma L b' e': 0<=e' => b' <> 0 => + phoare[M.p: (b, e) = (b', e') ==> res = b'^e'] = 1%r. + proof. + move => e_ge0 b_ne0. + proc. + sp. + (*$*) while (r = b^(e'-e) /\ b = b' /\ 0 <= e <= e') e. + - move => z. + auto. + smt(expr_pred). + auto. + smt(expr_pred expr0). + qed. + + +------------------------------------------------------------------------ +Variant: Probabilistic Hoare logic with non-strict variant +------------------------------------------------------------------------ + +.. admonition:: Syntax + + `while {formula} {expr1} {expr2} {prob}` + +Here `{formula}` is an invariant, `{expr1}` and `{expr2}` are integer +termination variants, and `{prob}` is a probability threshold. +