document proc*

doc/tactics/proc.rst

@@ -1,19 +1,20 @@
 ========================================================================
-Tactic: ``proc``
+Tactic: `proc`
 ========================================================================
 
-The ``proc`` tactic applies to program-logic goals where the procedure(s)
+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 
+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.
+separately. When one of the two procedures is abstract and the other is
+concrete the :ref:`proc* <procstar-tactic>` tactic can be used instead.
 
 .. contents::
    :local:
@@ -24,9 +25,9 @@ Variant: Concrete procedure(s)
 
 .. admonition:: Syntax
 
-  ``proc``
+  `proc`
 
-The ``proc`` tactic, when applied to concrete procedures, unfolds the 
+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.
@@ -87,9 +88,9 @@ Variant: Abstract procedure (non-relational)
 
 .. admonition:: Syntax
 
-  ``proc {formulaI}``
+  `proc {formulaI}`
 
-Here, ``{formulaI}`` is an invariant that should be preserved by the 
+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.
@@ -229,34 +230,34 @@ of the procedure under consideration.
 Variant: Abstract procedure (relational)
 ------------------------------------------------------------------------
 
-The relational variant of the ``proc`` tactic for abstract procedures
+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 {formulaI}``
-  - ``proc {formulaB} {formulaI}``
-  - ``proc {formulaB} {formulaI} {formulaJ}``
+  - `proc {formulaI}`
+  - `proc {formulaB} {formulaI}`
+  - `proc {formulaB} {formulaI} {formulaJ}`
 
 Here: 
 
-- ``{formulaI}`` is a two-sided invariant that should be preserved by the
+- `{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 
+- `{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 
+- `{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}`` 
+`{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 
+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 
@@ -314,30 +315,30 @@ and yield equal results when called on equal arguments.
      (* Procedure g2 preserves invariant *)
    abort.
 
-When ``{formulaB}`` and ``{formulaJ}`` are provided, the equality of 
-arguments, results, globals and ``{formulaI}`` obligations are modified to 
+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 
+`{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 
+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 
+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``.
+two programs using the `sym` tactic before applying `proc`.
 
 .. ecproof::
    :title: Probabilistic Relational Hoare logic example with bad event

doc/tactics/procstar.rst

@@ -0,0 +1,68 @@
+.. _procstar-tactic:
+========================================================================
+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 replaces the procedure(s) with a statement calling that procedure.
+This is useful, for example, when the goal is relational, but one of
+the two procedures is abstract, while the other is concrete.
+In that case no variant of `proc` can be applied, but `proc*` can,
+after which things like inlining the concrete procedure can be
+used to make progress.
+
+.. admonition:: Syntax
+
+  `proc*`
+
+.. 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.