From c26398031436ea69e7d122fd2fe4ed7ea1e9f7d2 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 3 Feb 2026 17:44:25 +0100 Subject: [PATCH 1/4] document the `proc` tactic --- doc/tactics/proc.rst | 373 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 373 insertions(+) create mode 100644 doc/tactics/proc.rst diff --git a/doc/tactics/proc.rst b/doc/tactics/proc.rst new file mode 100644 index 000000000..0449d661a --- /dev/null +++ b/doc/tactics/proc.rst @@ -0,0 +1,373 @@ +======================================================================== +Tactic: ``proc`` +======================================================================== + +The ``proc`` tactic applies to program-logic goals where the procedure(s) +under consideration are referred to by name rather than content. It is +typically the first tactic applied when reasoning about procedure calls +or top level program logic statements. + +There are two variants of the ``proc`` tactic, depending on whether the +procedure(s) in question are abstract (i.e., declared but not defined) +or concrete (i.e., defined with a body of code). + +The abstract variant is a bit different for probabilistic relational +Hoare logic compared to the other program logics, so we describe it +separately. + +------------------------------------------------------------------------ +Variant: Concrete procedure(s) +------------------------------------------------------------------------ + +.. admonition:: Syntax + + ``proc`` + +The ``proc`` tactic, when applied to concrete procedures, unfolds the +procedure definition(s) at hand, replacing the procedure call(s) +with the body(ies) of the corresponding procedure(s). The proof goal is +then updated accordingly. + +.. ecproof:: + :title: Hoare logic example + + require import AllCore. + + module M = { + proc f(x : int) = { + x <- x + 1; + x <- x * 2; + return x; + } + }. + + pred p : int. + pred q : int. + + lemma L : hoare[M.f : p x ==> q res]. + proof. + (*$*) proc. + abort. + +.. ecproof:: + :title: Probabilistic relational Hoare logic example + + require import AllCore. + + module M1 = { + proc f(x : int) = { + x <- x + 1; + x <- x * 2; + return x; + } + }. + + module M2 = { + proc f(x : int) = { + x <- x * 10; + x <- x - 3; + return x; + } + }. + + pred p : int & int. + pred q : int & int. + + lemma L : equiv[M1.f ~ M2.f : p x{1} x{2} ==> q res{1} res{2}]. + proof. + (*$*) proc. + abort. + +------------------------------------------------------------------------ +Variant: Abstract procedure (non-relational) +------------------------------------------------------------------------ + +.. admonition:: Syntax + + ``proc {formulaI}`` + +Here, ``{formulaI}`` is an invariant that should be preserved by the +procedure. The invariant can refer to global variables not being modified +by the procedure. To ensure that variables of interest cannot be modified, +it may be necessary to add restrictions to the module type of the abstract procedure, specifying which globals are not accessed. + +The tactic, when applied to abstract procedures, generates a proof +obligation that the invariant holds initially (i.e., it is implied by the +precondition) and another that the invariant is sufficient to ensure the +postcondition. For every module argument to the abstract procedure, an +additional proof obligation is generated to ensure that every procedure in +the module argument preserves the invariant. + +The probabilistic Hoare logic variant only works when the invariant is +guaranteed to hold with probability 1. Therefore it requires the initial +bound to be 1 and generates an additional proof obligation requiring that +losslessness of procedures of the module arguments implies losslessness +of the procedure under consideration. + +.. ecproof:: + :title: Hoare logic example with abstract procedure + + require import AllCore. + + module type OT = { + proc g1(): int + proc g2(x: int): unit + }. + + module type MT (O: OT) = { + proc f(x : int): int + }. + + module O = { + var y: int + proc g1() = { + y <- y+1; + return y; + } + + proc g2(x: int) = { + } + }. + + pred p : int. + pred q : int. + pred inv : int. + + lemma L (M <: MT {-O}): hoare[M(O).f : p x ==> q res]. + proof. + (*$*) proc (inv O.y). + - admit. + - admit. + - admit. + abort. + +.. ecproof:: + :title: Probabilistic Hoare logic example with abstract procedure + + require import AllCore. + + module type OT = { + proc g1(): int + proc g2(x: int): unit + }. + + module type MT (O: OT) = { + proc f(x : int): int + }. + + module O = { + var y: int + proc g1() = { + y <- y+1; + return y; + } + + proc g2(x: int) = { + } + }. + + + pred p : int. + pred q : int. + pred inv : int. + + lemma L (M <: MT {-O}): phoare[M(O).f : p x ==> q res] = 1%r. + proof. + (*$*) proc (inv O.y). + - admit. + - admit. + - admit. + - admit. + abort. + +.. ecproof:: + :title: Expectation Hoare logic example with abstract procedure + + require import AllCore Xreal. + + module type OT = { + proc g1(): int + proc g2(x: int): unit + }. + + module type MT (O: OT) = { + proc f(x : int): int + }. + + module O = { + var y: int + proc g1() = { + y <- y+1; + return y; + } + + proc g2(x: int) = { + } + }. + + + op p : int -> xreal. + op q : int -> xreal. + op inv : int -> xreal. + + lemma L (M <: MT {-O}): ehoare[M(O).f : p x ==> q res]. + proof. + (*$*) proc (inv O.y). + - admit. + - admit. + - admit. + abort. + + +------------------------------------------------------------------------ +Variant: Abstract procedure (relational) +------------------------------------------------------------------------ + +The relational variant of the ``proc`` tactic for abstract procedures +requires both procedures to be the same, though their module arguments +may differ. + +.. admonition:: Syntax + + ``proc {formulaB}? {formulaI} {formulaJ}?`` + +Here: + +- ``{formulaI}`` is a two-sided invariant that should be preserved by the + pair of procedures. +- ``{formulaB}`` is an optional formula representing a bad event on the + right side after which the invariant need no longer hold. +- ``{formulaJ}`` is an optional formula representing the invariant after + the bad event has occurred. This is optional even if ``{formulaB}`` is + provided; in which case the invariant is taken to be ``true`` after the + bad event. + +The tactic can be thought of as keeping both procedures in sync using +``{formulaI}`` until the bad event ``{formulaB}`` occurs on the right +side, after which they are no longer kept in sync. Instead ``{formulaJ}`` +is then preserved by the left and right procedures individually, no matter +the order in which the two sides make progress. + +When only ``{formulaI}`` is provided, the tactic works similarly to the +non-relational variants, generating proof obligations to ensure that +the invariant, equality of the globals of the module containing the +procedure and equality of arguments holds and that equality of the +globals, result and the invariant suffices to ensure the postcondition. +For every procedure of every module argument to the abstract procedure +an additional proof obligation is generated to ensure that the procedure +pairs of the module arguments on the left and right preserve the invariant +and yield equal results when called on equal arguments. + +.. ecproof:: + :title: Simple Probabilistic Relational Hoare logic example + + require import AllCore. + + module type OT = { + proc g1(): int + proc g2(x: int): unit + }. + + module type MT (O: OT) = { + proc f(x : int): int + }. + + module O1 = { + var y: int + proc g1() = { + y <- y+1; + return y; + } + + proc g2(x: int) = { + } + }. + module O2 = { + var y: int + proc g1() = { + return y; + } + + proc g2(x: int) = { + y <- y-1; + } + }. + + pred p : int & int. + pred q : int & int. + pred inv : int & int. + + lemma L (M <: MT {-O1, -O2}): equiv[M(O1).f ~ M(O2).f: p x{1} x{2} ==> q res{1} res{2}]. + proof. + (*$*) proc (inv O1.y{1} O2.y{2}). + - admit. + - admit. + - admit. + abort. + +When ``{formulaB}`` and ``{formulaJ}`` are provided, the equality of +arguments, results, globals and ``{formulaI}`` obligations are modified to +only hold/need to hold conditional on the bad event not having occurred on +the right side. When the bad event has occurred, we instead require that +``{formulaJ}`` holds without any additional equality requirements. Since +the behavior of the two sides is no longer synchronized after the bad +event, an obligation is generated to ensure that the procedure is lossless +when the procedures in its module arguments are lossless, to avoid the +weights diverging after the bad event. + +For every procedure of every module argument to the abstract procedure on +the left, an additional proof obligation is generated to ensure that the +when the bad event has happened and ``{formulaJ}`` holds for some right +memory, then it is guaranteed to still hold for that right memory after +running the procedure of the argument on the left. Similarly, for every +procedure of every module argument to the abstract procedure on the right, +an additional proof obligation is generated to ensure that when the bad +event has happened and ``{formulaJ}`` holds for some left memory, then the +bad event on the right and the two-sided invariant ``{formulaJ}`` is +guaranteed to still hold for the left memory after running the procedure +of the argument on the right. + +If you want the bad event to be on the left side instead, you can swap the +two programs using the ``sym`` tactic before applying ``proc``. + +.. ecproof:: + :title: Probabilistic Relational Hoare logic example with bad event + + require import AllCore. + + module type OT = { + proc g(): unit + }. + + module type MT (O: OT) = { + proc f(x : int): int + }. + + module O1 = { + var y: int + proc g() = { + y <- y+1; + } + }. + module O2 = { + var y: int + proc g() = { + y <- y-1; + } + }. + + pred p : int & int. + pred q : int & int. + pred inv : int & int. + pred bad : int. + pred inv2 : int & int. + + lemma L (M <: MT {-O1, -O2}): equiv[M(O1).f ~ M(O2).f: p x{1} x{2} ==> q res{1} res{2}]. + proof. + (*$*) proc (bad O2.y) (inv O1.y{1} O2.y{2}) (inv2 O1.y{1} O2.y{2}). + - admit. + - admit. + - admit. + - admit. + - admit. + abort. \ No newline at end of file From c6d59cf953aa2c6629e82f32ea388a967ebd9fa4 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 3 Feb 2026 18:33:53 +0100 Subject: [PATCH 2/4] [documentation]: proc: add local TOC --- doc/tactics/proc.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/doc/tactics/proc.rst b/doc/tactics/proc.rst index 0449d661a..a5bfb2a2b 100644 --- a/doc/tactics/proc.rst +++ b/doc/tactics/proc.rst @@ -15,6 +15,9 @@ The abstract variant is a bit different for probabilistic relational Hoare logic compared to the other program logics, so we describe it separately. +.. contents:: + :local: + ------------------------------------------------------------------------ Variant: Concrete procedure(s) ------------------------------------------------------------------------ From 253750af69bf3c056d2c6c6127c30ee32bb396d5 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 3 Feb 2026 18:36:15 +0100 Subject: [PATCH 3/4] [documentation]: proc: do not use pre&post opt. args I prefer to expand the 3 possible syntax. --- doc/tactics/proc.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/tactics/proc.rst b/doc/tactics/proc.rst index a5bfb2a2b..f157a70ab 100644 --- a/doc/tactics/proc.rst +++ b/doc/tactics/proc.rst @@ -232,7 +232,9 @@ may differ. .. admonition:: Syntax - ``proc {formulaB}? {formulaI} {formulaJ}?`` + - ``proc {formulaI}`` + - ``proc {formulaB} {formulaI}`` + - ``proc {formulaB} {formulaI} {formulaJ}`` Here: From 5155dc41f04c624128caa895dade981f6f0daeec Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 6 Feb 2026 12:30:29 +0100 Subject: [PATCH 4/4] Add comments to admits --- doc/tactics/proc.rst | 41 +++++++++++++++++++++++------------------ 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/doc/tactics/proc.rst b/doc/tactics/proc.rst index f157a70ab..a412a963c 100644 --- a/doc/tactics/proc.rst +++ b/doc/tactics/proc.rst @@ -139,9 +139,10 @@ of the procedure under consideration. lemma L (M <: MT {-O}): hoare[M(O).f : p x ==> q res]. proof. (*$*) proc (inv O.y). - - admit. - - admit. - - admit. + - admit. (* Invariant holds initially *) + - admit. (* Invariant implies postcondition *) + - admit. (* Procedure g1 preserves invariant *) + (* Procedure g2 preserves invariant *) abort. .. ecproof:: @@ -177,10 +178,11 @@ of the procedure under consideration. lemma L (M <: MT {-O}): phoare[M(O).f : p x ==> q res] = 1%r. proof. (*$*) proc (inv O.y). - - admit. - - admit. - - admit. - - admit. + - admit. (* Invariant holds initially *) + - admit. (* Invariant implies postcondition *) + - admit. (* Losslessness of M(O).f *) + - admit. (* Procedure g1 preserves invariant *) + (* Procedure g2 preserves invariant *) abort. .. ecproof:: @@ -216,9 +218,10 @@ of the procedure under consideration. lemma L (M <: MT {-O}): ehoare[M(O).f : p x ==> q res]. proof. (*$*) proc (inv O.y). - - admit. - - admit. - - admit. + - admit. (* Invariant holds initially *) + - admit. (* Invariant implies postcondition *) + - admit. (* Procedure g1 preserves invariant *) + (* Procedure g2 preserves invariant *) abort. @@ -305,9 +308,10 @@ and yield equal results when called on equal arguments. lemma L (M <: MT {-O1, -O2}): equiv[M(O1).f ~ M(O2).f: p x{1} x{2} ==> q res{1} res{2}]. proof. (*$*) proc (inv O1.y{1} O2.y{2}). - - admit. - - admit. - - admit. + - admit. (* Invariant holds initially *) + - admit. (* Invariant implies postcondition *) + - admit. (* Procedure g1 preserves invariant *) + (* Procedure g2 preserves invariant *) abort. When ``{formulaB}`` and ``{formulaJ}`` are provided, the equality of @@ -370,9 +374,10 @@ two programs using the ``sym`` tactic before applying ``proc``. lemma L (M <: MT {-O1, -O2}): equiv[M(O1).f ~ M(O2).f: p x{1} x{2} ==> q res{1} res{2}]. proof. (*$*) proc (bad O2.y) (inv O1.y{1} O2.y{2}) (inv2 O1.y{1} O2.y{2}). - - admit. - - admit. - - admit. - - admit. - - admit. + - admit. (* Connecting precondition to invariants *) + - admit. (* Connecting invariants to postcondition *) + - admit. (* Losslessness of M(O).f *) + - admit. (* Relating O1.g and O2.g during synchronization *) + - admit. (* Behaviour of O1.g after bad event *) + (* Behaviour of O2.g after bad event *) abort. \ No newline at end of file