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/5] [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/5] 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/5] 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. + From 709a5d65dfbf17fcdece0c98d7dd6f5f9e8cdc26 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 27 Feb 2026 17:28:22 +0100 Subject: [PATCH 4/5] simple example for advanced while --- doc/tactics/while.rst | 65 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 64 insertions(+), 1 deletion(-) diff --git a/doc/tactics/while.rst b/doc/tactics/while.rst index 9a0992fbb3..f4c1c7d082 100644 --- a/doc/tactics/while.rst +++ b/doc/tactics/while.rst @@ -232,7 +232,7 @@ designated relational case, but for a single program: ------------------------------------------------------------------------ -Variant: Probabilistic Hoare logic with non-strict variant +Variant: Probabilistic Hoare logic with non-strict variant and `>=` or `=` bound ------------------------------------------------------------------------ .. admonition:: Syntax @@ -242,3 +242,66 @@ Variant: Probabilistic Hoare logic with non-strict variant Here `{formula}` is an invariant, `{expr1}` and `{expr2}` are integer termination variants, and `{prob}` is a probability threshold. +The tactic generates 6 goals + +- a goal that connects the precondition to the invariant + +- + +.. ecproof:: + :title: Example with `1%r` bound + require import AllCore DBool. + + module M = { + proc p(n) = { + var b, r; + r <- true; + while (0 < n) { + b <$ {0,1}; + if (b) { + n <- n-1; + } + } + return r; + } + }. + + lemma L: phoare[M.p: true ==> res] >= 1%r. + proof. + proc. + sp. + while r n n (1%r/2%r). + - trivial. + - trivial. + - smt(). + - move => wh. + seq 1: r => //. + + rnd. + auto. + smt(dboolE). + if. + + sp. + conseq wh. + smt(). + conseq wh. + smt(). + - conseq (: : >= 1%r). + seq 1: r => //. + + rnd. + auto. + smt(dboolE). + if. + + sp. + auto. + auto. + split. + - smt(). + move => z. + seq 1: (b /\ n = z) => //. + - rnd. + auto. + smt(dboolE). + rcondt 1 => //. + auto. + smt(). + qed. \ No newline at end of file From a2f41f8b523834fe462a74c690f9283ecde1115c Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 16 Mar 2026 19:43:33 +0100 Subject: [PATCH 5/5] document pHL variants of while tactic --- doc/tactics/while.rst | 177 ++++++++++++++++++++++++++++++------------ 1 file changed, 128 insertions(+), 49 deletions(-) diff --git a/doc/tactics/while.rst b/doc/tactics/while.rst index f4c1c7d082..bd45bc7636 100644 --- a/doc/tactics/while.rst +++ b/doc/tactics/while.rst @@ -235,73 +235,152 @@ designated relational case, but for a single program: Variant: Probabilistic Hoare logic with non-strict variant and `>=` or `=` bound ------------------------------------------------------------------------ +This variant only works on pHL goals whose body only contains a while loop. +It can be seen as a variation of the variant pHL with `>=` bounds +with some additional requirements to handle issues with termination. + .. admonition:: Syntax - `while {formula} {expr1} {expr2} {prob}` + `while {formula} {var} {varbd} {prob}` + +Here `{formula}` is an invariant, `{var}` is an integer +termination variant, `{varbd}` is an upper bound on the variant, +and `{prob}` is a lower bound on the probability that the variant decreases. + +Program variables used in `{varbd}` and `{prob}` need to be unmodified by the loop body. -Here `{formula}` is an invariant, `{expr1}` and `{expr2}` are integer -termination variants, and `{prob}` is a probability threshold. +Though this tactic can be used to prove non-`1%r` bounds, it only works with +almost certain termination. The bounds are proven using co-induction, +similarly to the variant of while for pHL with `>=` bounds. Using this +requires carefully setting up the precondition and bounds to facilitate this. The tactic generates 6 goals -- a goal that connects the precondition to the invariant +- A goal that connects the precondition to the invariant + +- A goal that handles the case where the loop is never entered, connecting + the bound of the pHL statement to both the precondition and postcondition. + +- A goal requiring that `{varbd}` bounds the variant from above, and that the loop + condition fails when the variant reaches 0. -- +- A goal requiring that the pHL holds from coinduction. + +- A goal requiring that the invariant is always preserved + +- A goal requiring that `{prob}` is positive and lower bounds the probability of + the variant decreasing. .. ecproof:: - :title: Example with `1%r` bound + :title: Rejection sample example require import AllCore DBool. - + module M = { - proc p(n) = { - var b, r; - r <- true; - while (0 < n) { - b <$ {0,1}; - if (b) { - n <- n-1; - } + proc rs(c: bool) = { + while (c) { + c <$ {0,1}; } - return r; } }. - - lemma L: phoare[M.p: true ==> res] >= 1%r. + + lemma L: phoare[M.rs: true ==> true] = 1%r. proof. proc. - sp. - while r n n (1%r/2%r). - - trivial. - - trivial. - - smt(). - - move => wh. - seq 1: r => //. - + rnd. - auto. - smt(dboolE). - if. - + sp. - conseq wh. - smt(). - conseq wh. + (*$*) while true (b2i c) 1 (1%r/2%r). + - (* Connecting precondition to invariant *) + done. + - (* Connecting precondition to pHL bound and postcondition + when the loop is never entered *) + done. + - (* Showing that 1 bounds the variant, and that the variant + reaching 0 means exiting the loop *) smt(). - - conseq (: : >= 1%r). - seq 1: r => //. - + rnd. - auto. + - (* Using coinduction to prove that the pHL bound is as desired *) + move => wH. + conseq (: : >= 1%r). + seq 1: true 1%r => //. + + auto => />. smt(dboolE). - if. - + sp. - auto. - auto. - split. + conseq wH. + - (* Showing that the invariant is preserved *) + auto; smt(dboolE). + (* Showing that the probabiliy bound on the variant decreasing + is exactly that *) + split. - smt(). move => z. - seq 1: (b /\ n = z) => //. - - rnd. - auto. - smt(dboolE). - rcondt 1 => //. - auto. - smt(). + rnd; skip => />. + smt(dboolE). + qed. + +The previous example is simpler and more well motivated, but does +not fully demonstrate the power of the tactic, which we demonstrate +with the following example. + +.. ecproof:: + require import AllCore DBool. + + module M = { + proc p(i: int, f: bool) = { + var c; + while (0 < i) { + c <$ {0,1}; + if (c) { + i <- i-1; + } else { + f <- false; + } + } + return f; + } + }. + + lemma L: phoare[M.p: 0 <= i /\ f==> res] = ((2%r)^(-i)). + proof. + proc. + exlim i => I. + conseq (: 0 <= i <= I ==> f: + = (if f then 2%r ^ -i else 0%r)) => //. + + smt(). + (*$*) while (i <= I) i I (1%r/2%r). + - (* Connecting precondition to invariant *) + done. + - (* Connecting precondition to pHL bound and postcondition + when the loop is never entered *) + smt(RField.expr0). + - (* Showing that I bounds the variant, and that the variant + reaching 0 means exiting the loop *) + smt(). + - (* Using coinduction to prove that the pHL bound is as desired *) + move => wH. + exlim i => i'. + seq 2: f (if f then 1%r/2%r else 0%r) + (2%r ^ (1-i')) _ 0%r + (0 <= i <= I /\ (f => i' = i + 1))=> //. + + auto. + smt(). + + wp. + rnd (fun c => c = true /\ f). + auto => /> &hr. + rewrite dboolE. + smt(). + + conseq wH. + * smt(). + smt(). + + conseq wH. + * smt(). + smt(). + rewrite (StdBigop.Bigreal.Num.Domain.exprD) // RField.expr1 => />. + smt(RField.unitrX). + - (* Showing that the invariant is preserved *) + auto; smt(dboolE). + (* Showing that the probabiliy bound on the variant decreasing + is exactly that *) + split. + - smt(). + move => z. + wp. + rnd. + auto => />. + smt(dboolE). qed. \ No newline at end of file