Update docs: EasyCrypt/easycrypt@c3a0bf3

Author: github-actions[bot]

refman/_sources/tactics/if.rst.txt

@@ -0,0 +1,234 @@
+========================================================================
+Tactic: ``if``
+========================================================================
+
+In EasyCrypt, the ``if`` tactic is a way of reasoning about program(s)
+that use conditionals. When a program begins with an if statement,
+execution will follow one path if the condition is ``true`` and another
+path if it is ``false``. The tactic says that to prove the program is
+correct, you must consider both cases: you assume the condition holds
+and show that the *then* branch establishes the desired result, and you
+assume the condition does not hold and show that the *else* branch
+establishes the same result. EasyCrypt allows you to apply this rule
+only when the program starts with an if, so the proof can split immediately
+from the initial state.If the conditional appears deeper in the code, you
+can first use the seq tactic (or another tactic such as sp that eliminates
+the earlier statements) to separate the preceding statements from the
+conditional.
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Variant: ``if`` (HL)
+------------------------------------------------------------------------
+
+.. ecproof::
+   :title: Hoare logic example
+
+   require import AllCore.
+
+   module M = {
+     proc f(x : int) = {
+       var y : int;
+
+       if (x < 0) {
+         y <- -x;
+       } else {
+         y <- x;
+       }
+
+       return y;
+     }
+   }.
+
+   pred p : glob M.
+
+   lemma L : hoare[M.f : p (glob M) ==> 0 <= res].
+   proof.
+     proc.
+     (*$*) if.
+     (* First goal: (x < 0) holds *)
+     - wp. skip. smt().
+     (* Second goal: (x < 0) does not hold *)
+     - wp. skip. smt().
+   qed.
+
+------------------------------------------------------------------------
+Variant: ``if`` (pRHL)
+------------------------------------------------------------------------
+
+In probabilistic relational Hoare logic, the ``if`` tactic is applied
+in a lock-step manner, meaning that the two programs being compared must
+proceed through the conditional in sync. This requires that their guards
+evaluate to the same boolean value in the related states, so that either
+both programs take the *then* branch or both take the *else* branch.
+
+As a result, using the ``if`` tactic involves establishing that the two
+conditions are equal under the current relational invariant before
+splitting into the two synchronized cases. 
+
+Although synchronization ensures both guards take the same value, the
+implementation splits only on the left guard (rather than explicitly
+stating both are true or both are false).
+
+.. ecproof::
+   :title: Relational Hoare logic example (2-sided)
+
+   require import AllCore.
+   
+   module M = {
+     proc f(x : int) = {
+       var y : int;
+   
+       if (x < 0) {
+         y <- -x;
+       } else {
+         y <- x;
+       }
+   
+       return y;
+     }
+   }.
+   
+   lemma L : equiv[M.f ~ M.f: x{1} = x{2} ==> res{1} = res{2}].
+   proof.
+     proc.
+     (*$*) if.
+     (* First goal: we prove that the guards are in sync. *)
+     - smt().
+     (* First goal: (x < 0) holds *)
+     - wp; skip. smt().
+     (* Second goal: (x < 0) does not hold *)
+     - wp; skip. smt().
+   qed.
+
+
+------------------------------------------------------------------------
+Variant: ``if {side}`` (pRHL)
+------------------------------------------------------------------------
+
+In the one-sided ``if`` tactic used in pRHL, the user specifies whether
+the conditional reasoning should be applied to the left or the right
+program. The tactic then performs a case analysis only on the ``if``
+statement at the top of that chosen program, generating separate goals
+for the ``true`` and ``false`` branches on that side. Unlike the lock-step
+relational ``if`` tactic, no synchronization of guards is required, and
+the other program is not constrained to take the same branch or even to
+have a similar structure.
+
+.. ecproof::
+   :title: Relational Hoare logic example (1-sided)
+
+   require import AllCore.
+   
+   module M = {
+     proc f(x : int) = {
+       var y : int;
+   
+       if (x < 0) {
+         y <- -x;
+       } else {
+         y <- x;
+       }
+   
+       return y;
+     }
+   
+     proc g(x : int) = {
+       return `|x|;
+     }
+   }.
+   
+   lemma L : equiv[M.f ~ M.g: x{1} = x{2} ==> res{1} = res{2}].
+   proof.
+     proc.
+     (*$*) if{1}.
+     (* First goal: (x < 0) holds (left program) *)
+     - wp; skip. smt().
+     (* Second goal: (x < 0) does not hold (left program) *)
+     - wp; skip. smt().
+   qed.
+
+------------------------------------------------------------------------
+Variant: ``if`` (pHL)
+------------------------------------------------------------------------
+
+In probabilistic Hoare logic, the ``if`` tactic behaves much like in
+standard Hoare logic, except that the postcondition is expressed in terms
+of a probability bound. Since the if statement is the first command of
+the program, its guard is evaluated immediately in the initial state and
+therefore deterministically takes either the ``true`` or the ``false``
+value, with probability 1. As a result, the program execution splits into
+one of the two branches without introducing any additional probabilistic
+choice at the level of control flow, and the probability bound is preserved
+by reasoning separately about each branch under the corresponding
+assumption on the guard.
+
+.. ecproof::
+   :title: Probabilistic Hoare logic example
+
+   require import AllCore.
+   
+   module M = {
+     proc f(x : int) = {
+       var y : int;
+   
+       if (x < 0) {
+         y <- -x;
+       } else {
+         y <- x;
+       }
+   
+       return y;
+     }
+   }.
+   
+   lemma L : phoare[M.f : true ==> 0 <= res] = 1%r.
+   proof.
+     proc.
+     (*$*) if.
+     (* First goal: (x < 0) holds *)
+     - wp; skip. smt().
+     (* Second goal: (x < 0) does not hold *)
+     - wp; skip. smt().
+   qed.
+
+------------------------------------------------------------------------
+Variant: ``if`` (eHL)
+------------------------------------------------------------------------
+
+In expectation Hoare logic, the ``if`` tactic behaves similarly to standard
+Hoare logic. Two subgoals are generated, where the pre-expection is additionally
+guarded by the branch condition and its negation, respectively. This naturally
+splits the goal of proving the upper-bound into two cases along the control
+flow.
+
+.. ecproof::
+   :title: Expectation Hoare logic example
+
+   require import AllCore Xreal.
+
+   module M = {
+     proc f(x : int) = {
+       var y : int;
+   
+       if (x < 0) {
+         y <- -x;
+       } else {
+         y <- x;
+       }
+   
+       return y;
+     }
+   }.
+
+   lemma L : ehoare[M.f : 0%xr ==> (!(0 <= res))%xr].
+   proof.
+     proc.
+     (*$*) if.
+     (* First goal: (x < 0) holds *)
+     - wp; skip. smt().
+     (* Second goal: (x < 0) does not hold *)
+     - wp; skip. smt().
+   qed.

refman/index.html

@@ -78,6 +78,7 @@ <h1>EasyCrypt reference manual<a class="headerlink" href="#easycrypt-reference-m
 <div class="toctree-wrapper compound">
 <ul>
 <li class="toctree-l1"><a class="reference internal" href="tactics.html">Proof tactics reference</a><ul>
+<li class="toctree-l2"><a class="reference internal" href="tactics/if.html">Tactic: <code class="docutils literal notranslate"><span class="pre">if</span></code></a></li>
 <li class="toctree-l2"><a class="reference internal" href="tactics/skip.html">Tactic: <cite>skip</cite></a></li>
 </ul>
 </li>

refman/objects.inv

@@ -23,7 +23,7 @@
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="genindex.html" />
     <link rel="search" title="Search" href="search.html" />
-    <link rel="next" title="Tactic: skip" href="tactics/skip.html" />
+    <link rel="next" title="Tactic: if" href="tactics/if.html" />
     <link rel="prev" title="EasyCrypt reference manual" href="index.html" /> 
 </head>
 
@@ -48,6 +48,7 @@
         </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
               <ul class="current">
 <li class="toctree-l1 current"><a class="current reference internal" href="#">Proof tactics reference</a><ul>
+<li class="toctree-l2"><a class="reference internal" href="tactics/if.html">Tactic: <code class="docutils literal notranslate"><span class="pre">if</span></code></a></li>
 <li class="toctree-l2"><a class="reference internal" href="tactics/skip.html">Tactic: <cite>skip</cite></a></li>
 </ul>
 </li>
@@ -81,6 +82,7 @@
 <h1>Proof tactics reference<a class="headerlink" href="#proof-tactics-reference" title="Link to this heading"></a></h1>
 <div class="toctree-wrapper compound">
 <ul>
+<li class="toctree-l1"><a class="reference internal" href="tactics/if.html">Tactic: <code class="docutils literal notranslate"><span class="pre">if</span></code></a></li>
 <li class="toctree-l1"><a class="reference internal" href="tactics/skip.html">Tactic: <cite>skip</cite></a></li>
 </ul>
 </div>
@@ -91,7 +93,7 @@ <h1>Proof tactics reference<a class="headerlink" href="#proof-tactics-reference"
           </div>
           <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
         <a href="index.html" class="btn btn-neutral float-left" title="EasyCrypt reference manual" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
-        <a href="tactics/skip.html" class="btn btn-neutral float-right" title="Tactic: skip" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
+        <a href="tactics/if.html" class="btn btn-neutral float-right" title="Tactic: if" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
     </div>
 
   <hr/>