Update docs: EasyCrypt/easycrypt@1d3318e

Author: github-actions[bot]

refman/.buildinfo

@@ -2,21 +2,21 @@
 Tactic: `skip`
 ========================================================================
 
-The `skip` tactic applies to program-logic goals where the program(s) under
-consideration are empty. In this situation, program execution performs
-no computation and produces no state changes.
+The ``skip`` tactic applies to program-logic goals where the program(s)
+under consideration are empty. In this situation, program execution
+performs no computation and produces no state changes.
 
-Applying `skip` eliminates the program component of the goal and reduces
+Applying ``skip`` eliminates the program component of the goal and reduces
 the proof obligation to a pure logical goal. Concretely, the remaining
 task is to prove that the precondition implies the postcondition.
 
-The `skip` tactic does not attempt to solve this logical obligation itself.
+The ``skip`` tactic does not attempt to solve this logical obligation itself.
 
 .. contents::
    :local:
 
 ------------------------------------------------------------------------
-In Hoare logic
+Variant: ``skip`` (Hoare logic)
 ------------------------------------------------------------------------
 
 .. ecproof::
@@ -39,7 +39,7 @@ In Hoare logic
    abort.
 
 ------------------------------------------------------------------------
-In Relational Hoare logic
+Variant: ``skip`` (Relational Hoare logic)
 ------------------------------------------------------------------------
 
 In the relational Hoare logic setting, the `skip`` tactic applies only
@@ -66,14 +66,14 @@ judgment to obligations on the preconditions and postconditions alone.
    abort.
 
 ------------------------------------------------------------------------
-In Probabilistic Hoare logic
+Variant: ``skip`` (Probabilistic Hoare logic)
 ------------------------------------------------------------------------
 
-In the probabilistic Hoare logic setting, applying `skip` generates an
+In the probabilistic Hoare logic setting, applying ``skip`` generates an
 additional proof obligation compared to the pure Hoare case. Besides the
 logical implication between the precondition and the postcondition, one
 must also prove that the probability weight of the empty program, namely
-`1%r`, satisfies the bound specified in the judgment.
+``1%r``, satisfies the bound specified in the judgment.
 
 .. ecproof::
    :title: Probabilistic Hoare logic example

refman/_sources/tactics/skip.rst.txt

@@ -48,9 +48,9 @@
               <ul class="current">
 <li class="toctree-l1 current"><a class="reference internal" href="../tactics.html">Proof tactics reference</a><ul class="current">
 <li class="toctree-l2 current"><a class="current reference internal" href="#">Tactic: <cite>skip</cite></a><ul>
-<li class="toctree-l3"><a class="reference internal" href="#in-hoare-logic">In Hoare logic</a></li>
-<li class="toctree-l3"><a class="reference internal" href="#in-relational-hoare-logic">In Relational Hoare logic</a></li>
-<li class="toctree-l3"><a class="reference internal" href="#in-probabilistic-hoare-logic">In Probabilistic Hoare logic</a></li>
+<li class="toctree-l3"><a class="reference internal" href="#variant-skip-hoare-logic">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Hoare logic)</a></li>
+<li class="toctree-l3"><a class="reference internal" href="#variant-skip-relational-hoare-logic">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Relational Hoare logic)</a></li>
+<li class="toctree-l3"><a class="reference internal" href="#variant-skip-probabilistic-hoare-logic">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Probabilistic Hoare logic)</a></li>
 </ul>
 </li>
 </ul>
@@ -84,30 +84,30 @@
 
   <section id="tactic-skip">
 <h1>Tactic: <cite>skip</cite><a class="headerlink" href="#tactic-skip" title="Link to this heading"></a></h1>
-<p>The <cite>skip</cite> tactic applies to program-logic goals where the program(s) under
-consideration are empty. In this situation, program execution performs
-no computation and produces no state changes.</p>
-<p>Applying <cite>skip</cite> eliminates the program component of the goal and reduces
+<p>The <code class="docutils literal notranslate"><span class="pre">skip</span></code> tactic applies to program-logic goals where the program(s)
+under consideration are empty. In this situation, program execution
+performs no computation and produces no state changes.</p>
+<p>Applying <code class="docutils literal notranslate"><span class="pre">skip</span></code> eliminates the program component of the goal and reduces
 the proof obligation to a pure logical goal. Concretely, the remaining
 task is to prove that the precondition implies the postcondition.</p>
-<p>The <cite>skip</cite> tactic does not attempt to solve this logical obligation itself.</p>
+<p>The <code class="docutils literal notranslate"><span class="pre">skip</span></code> tactic does not attempt to solve this logical obligation itself.</p>
 <nav class="contents local" id="contents">
 <ul class="simple">
-<li><p><a class="reference internal" href="#in-hoare-logic" id="id1">In Hoare logic</a></p></li>
-<li><p><a class="reference internal" href="#in-relational-hoare-logic" id="id2">In Relational Hoare logic</a></p></li>
-<li><p><a class="reference internal" href="#in-probabilistic-hoare-logic" id="id3">In Probabilistic Hoare logic</a></p></li>
+<li><p><a class="reference internal" href="#variant-skip-hoare-logic" id="id1">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Hoare logic)</a></p></li>
+<li><p><a class="reference internal" href="#variant-skip-relational-hoare-logic" id="id2">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Relational Hoare logic)</a></p></li>
+<li><p><a class="reference internal" href="#variant-skip-probabilistic-hoare-logic" id="id3">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Probabilistic Hoare logic)</a></p></li>
 </ul>
 </nav>
-<section id="in-hoare-logic">
-<h2><a class="toc-backref" href="#id1" role="doc-backlink">In Hoare logic</a><a class="headerlink" href="#in-hoare-logic" title="Link to this heading"></a></h2>
+<section id="variant-skip-hoare-logic">
+<h2><a class="toc-backref" href="#id1" role="doc-backlink">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Hoare logic)</a><a class="headerlink" href="#variant-skip-hoare-logic" title="Link to this heading"></a></h2>
 
 <div class="proofnav-sphinx">
   <div id="proofnav-0" class="proofnav-mount"></div>
   <script type="application/json" id="proofnav-0-data">{"source":"require import AllCore.\n\nmodule M = {\n  proc f(x : int) = {\n    return x;\n  }\n}.\n\npred p : int.\npred q : int.\n\nlemma L : hoare[M.f : p x ==> q res].\nproof.\n  proc. skip.\nabort.\n","sentenceEnds":[23,80,95,109,148,155,163,169,176],"sentences":[{"goals":[],"message":""},{"goals":[],"message":""},{"goals":[],"message":"info: added predicate p : int -> bool"},{"goals":[],"message":"info: added predicate q : int -> bool"},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\npre = p arg\n\n    M.f \n\npost = q res\n"],"message":""},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\npre = p arg\n\n    M.f \n\npost = q res\n"],"message":""},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x : int}\n\npre = p x\n\n\npost = q x\n"],"message":""},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\nforall &hr, p x{hr} => q x{hr}\n"],"message":""},{"goals":[],"message":""}],"initialSentence":6,"title":"Hoare logic example"}</script>
 </div>
 </section>
-<section id="in-relational-hoare-logic">
-<h2><a class="toc-backref" href="#id2" role="doc-backlink">In Relational Hoare logic</a><a class="headerlink" href="#in-relational-hoare-logic" title="Link to this heading"></a></h2>
+<section id="variant-skip-relational-hoare-logic">
+<h2><a class="toc-backref" href="#id2" role="doc-backlink">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Relational Hoare logic)</a><a class="headerlink" href="#variant-skip-relational-hoare-logic" title="Link to this heading"></a></h2>
 <p>In the relational Hoare logic setting, the <cite>skip`</cite> tactic applies only
 when both programs are empty, in which case it reduces the relational
 judgment to obligations on the preconditions and postconditions alone.</p>
@@ -117,13 +117,13 @@ <h2><a class="toc-backref" href="#id2" role="doc-backlink">In Relational Hoare l
   <script type="application/json" id="proofnav-1-data">{"source":"require import AllCore.\n\nmodule M = {\n  proc f(x : int) = {\n    return x;\n  }\n}.\n\npred p : int & int.\npred q : int & int.\n\nlemma L : equiv[M.f ~ M.f : p x{1} x{2} ==> q res{1} res{2}].\nproof.\n  proc. skip.\nabort.\n","sentenceEnds":[23,80,101,121,184,191,199,205,212],"sentences":[{"goals":[],"message":""},{"goals":[],"message":""},{"goals":[],"message":"info: added predicate p : int -> int -> bool"},{"goals":[],"message":"info: added predicate q : int -> int -> bool"},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\npre = p arg{1} arg{2}\n\n    M.f ~ M.f \n\npost = q res{1} res{2}\n"],"message":""},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\npre = p arg{1} arg{2}\n\n    M.f ~ M.f \n\npost = q res{1} res{2}\n"],"message":""},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\n&1 (left ) : {x : int} [programs are in sync]\n&2 (right) : {x : int}\n\npre = p x{1} x{2}\n\n\npost = q x{1} x{2}\n"],"message":""},{"goals":["Type variables: <none>\n\n------------------------------------------------------------------------\nforall &1 &2, p x{1} x{2} => q x{1} x{2}\n"],"message":""},{"goals":[],"message":""}],"initialSentence":6,"title":"Relational Hoare logic example"}</script>
 </div>
 </section>
-<section id="in-probabilistic-hoare-logic">
-<h2><a class="toc-backref" href="#id3" role="doc-backlink">In Probabilistic Hoare logic</a><a class="headerlink" href="#in-probabilistic-hoare-logic" title="Link to this heading"></a></h2>
-<p>In the probabilistic Hoare logic setting, applying <cite>skip</cite> generates an
+<section id="variant-skip-probabilistic-hoare-logic">
+<h2><a class="toc-backref" href="#id3" role="doc-backlink">Variant: <code class="docutils literal notranslate"><span class="pre">skip</span></code> (Probabilistic Hoare logic)</a><a class="headerlink" href="#variant-skip-probabilistic-hoare-logic" title="Link to this heading"></a></h2>
+<p>In the probabilistic Hoare logic setting, applying <code class="docutils literal notranslate"><span class="pre">skip</span></code> generates an
 additional proof obligation compared to the pure Hoare case. Besides the
 logical implication between the precondition and the postcondition, one
 must also prove that the probability weight of the empty program, namely
-<cite>1%r</cite>, satisfies the bound specified in the judgment.</p>
+<code class="docutils literal notranslate"><span class="pre">1%r</span></code>, satisfies the bound specified in the judgment.</p>
 
 <div class="proofnav-sphinx">
   <div id="proofnav-2" class="proofnav-mount"></div>