Update docs: EasyCrypt/easycrypt@a31182f

Author: github-actions[bot]

refman/.buildinfo

@@ -0,0 +1,4 @@
+# Sphinx build info version 1
+# This file records the configuration used when building these files. When it is not found, a full rebuild will be done.
+config: 8e2a85eab20f98fda0352a8ff14ae838
+tags: 645f666f9bcd5a90fca523b33c5a78b7

refman/_sources/index.rst.txt

@@ -0,0 +1,7 @@
+EasyCrypt reference manual
+========================================================================
+
+.. toctree::
+   :maxdepth: 2
+
+   tactics

refman/_sources/tactics.rst.txt

@@ -0,0 +1,8 @@
+Proof tactics reference
+========================================================================
+
+.. toctree::
+   :maxdepth: 1
+   :glob:
+
+   tactics/*

refman/_sources/tactics/skip.rst.txt

@@ -0,0 +1,95 @@
+========================================================================
+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.
+
+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.
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+In Hoare logic
+------------------------------------------------------------------------
+
+.. ecproof::
+   :title: Hoare logic example
+
+   require import AllCore.
+
+   module M = {
+     proc f(x : int) = {
+       return x;
+     }
+   }.
+
+   pred p : int.
+   pred q : int.
+
+   lemma L : hoare[M.f : p x ==> q res].
+   proof.
+     proc. (*$*) skip.
+   abort.
+
+------------------------------------------------------------------------
+In Relational Hoare logic
+------------------------------------------------------------------------
+
+In the relational Hoare logic setting, the `skip`` tactic applies only
+when both programs are empty, in which case it reduces the relational
+judgment to obligations on the preconditions and postconditions alone.
+
+.. ecproof::
+   :title: Relational Hoare logic example
+
+   require import AllCore.
+
+   module M = {
+     proc f(x : int) = {
+       return x;
+     }
+   }.
+
+   pred p : int & int.
+   pred q : int & int.
+
+   lemma L : equiv[M.f ~ M.f : p x{1} x{2} ==> q res{1} res{2}].
+   proof.
+     proc. (*$*) skip.
+   abort.
+
+------------------------------------------------------------------------
+In Probabilistic Hoare logic
+------------------------------------------------------------------------
+
+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.
+
+.. ecproof::
+   :title: Probabilistic Hoare logic example
+
+   require import AllCore.
+
+   module M = {
+     proc f(x : int) = {
+       return x;
+     }
+   }.
+
+   pred p : int.
+   pred q : int.
+
+   lemma L : phoare[M.f : p x ==> q res] >= (1%r / 2%r).
+   proof.
+     proc. (*$*) skip.
+   abort.

refman/_sphinx_design_static/design-tabs.js

@@ -0,0 +1,101 @@
+// @ts-check
+
+// Extra JS capability for selected tabs to be synced
+// The selection is stored in local storage so that it persists across page loads.
+
+/**
+ * @type {Record<string, HTMLElement[]>}
+ */
+let sd_id_to_elements = {};
+const storageKeyPrefix = "sphinx-design-tab-id-";
+
+/**
+ * Create a key for a tab element.
+ * @param {HTMLElement} el - The tab element.
+ * @returns {[string, string, string] | null} - The key.
+ *
+ */
+function create_key(el) {
+  let syncId = el.getAttribute("data-sync-id");
+  let syncGroup = el.getAttribute("data-sync-group");
+  if (!syncId || !syncGroup) return null;
+  return [syncGroup, syncId, syncGroup + "--" + syncId];
+}
+
+/**
+ * Initialize the tab selection.
+ *
+ */
+function ready() {
+  // Find all tabs with sync data
+
+  /** @type {string[]} */
+  let groups = [];
+
+  document.querySelectorAll(".sd-tab-label").forEach((label) => {
+    if (label instanceof HTMLElement) {
+      let data = create_key(label);
+      if (data) {
+        let [group, id, key] = data;
+
+        // add click event listener
+        // @ts-ignore
+        label.onclick = onSDLabelClick;
+
+        // store map of key to elements
+        if (!sd_id_to_elements[key]) {
+          sd_id_to_elements[key] = [];
+        }
+        sd_id_to_elements[key].push(label);
+
+        if (groups.indexOf(group) === -1) {
+          groups.push(group);
+          // Check if a specific tab has been selected via URL parameter
+          const tabParam = new URLSearchParams(window.location.search).get(
+            group
+          );
+          if (tabParam) {
+            console.log(
+              "sphinx-design: Selecting tab id for group '" +
+                group +
+                "' from URL parameter: " +
+                tabParam
+            );
+            window.sessionStorage.setItem(storageKeyPrefix + group, tabParam);
+          }
+        }
+
+        // Check is a specific tab has been selected previously
+        let previousId = window.sessionStorage.getItem(
+          storageKeyPrefix + group
+        );
+        if (previousId === id) {
+          // console.log(
+          //   "sphinx-design: Selecting tab from session storage: " + id
+          // );
+          // @ts-ignore
+          label.previousElementSibling.checked = true;
+        }
+      }
+    }
+  });
+}
+
+/**
+ *  Activate other tabs with the same sync id.
+ *
+ * @this {HTMLElement} - The element that was clicked.
+ */
+function onSDLabelClick() {
+  let data = create_key(this);
+  if (!data) return;
+  let [group, id, key] = data;
+  for (const label of sd_id_to_elements[key]) {
+    if (label === this) continue;
+    // @ts-ignore
+    label.previousElementSibling.checked = true;
+  }
+  window.sessionStorage.setItem(storageKeyPrefix + group, id);
+}
+
+document.addEventListener("DOMContentLoaded", ready, false);

refman/_sphinx_design_static/sphinx-design.min.css

@@ -0,0 +1,123 @@
+/* Compatability shim for jQuery and underscores.js.
+ *
+ * Copyright Sphinx contributors
+ * Released under the two clause BSD licence
+ */
+
+/**
+ * small helper function to urldecode strings
+ *
+ * See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL
+ */
+jQuery.urldecode = function(x) {
+    if (!x) {
+        return x
+    }
+    return decodeURIComponent(x.replace(/\+/g, ' '));
+};
+
+/**
+ * small helper function to urlencode strings
+ */
+jQuery.urlencode = encodeURIComponent;
+
+/**
+ * This function returns the parsed url parameters of the
+ * current request. Multiple values per key are supported,
+ * it will always return arrays of strings for the value parts.
+ */
+jQuery.getQueryParameters = function(s) {
+    if (typeof s === 'undefined')
+        s = document.location.search;
+    var parts = s.substr(s.indexOf('?') + 1).split('&');
+    var result = {};
+    for (var i = 0; i < parts.length; i++) {
+        var tmp = parts[i].split('=', 2);
+        var key = jQuery.urldecode(tmp[0]);
+        var value = jQuery.urldecode(tmp[1]);
+        if (key in result)
+            result[key].push(value);
+        else
+            result[key] = [value];
+    }
+    return result;
+};
+
+/**
+ * highlight a given string on a jquery object by wrapping it in
+ * span elements with the given class name.
+ */
+jQuery.fn.highlightText = function(text, className) {
+    function highlight(node, addItems) {
+        if (node.nodeType === 3) {
+            var val = node.nodeValue;
+            var pos = val.toLowerCase().indexOf(text);
+            if (pos >= 0 &&
+                !jQuery(node.parentNode).hasClass(className) &&
+                !jQuery(node.parentNode).hasClass("nohighlight")) {
+                var span;
+                var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg");
+                if (isInSVG) {
+                    span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
+                } else {
+                    span = document.createElement("span");
+                    span.className = className;
+                }
+                span.appendChild(document.createTextNode(val.substr(pos, text.length)));
+                node.parentNode.insertBefore(span, node.parentNode.insertBefore(
+                    document.createTextNode(val.substr(pos + text.length)),
+                    node.nextSibling));
+                node.nodeValue = val.substr(0, pos);
+                if (isInSVG) {
+                    var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
+                    var bbox = node.parentElement.getBBox();
+                    rect.x.baseVal.value = bbox.x;
+                    rect.y.baseVal.value = bbox.y;
+                    rect.width.baseVal.value = bbox.width;
+                    rect.height.baseVal.value = bbox.height;
+                    rect.setAttribute('class', className);
+                    addItems.push({
+                        "parent": node.parentNode,
+                        "target": rect});
+                }
+            }
+        }
+        else if (!jQuery(node).is("button, select, textarea")) {
+            jQuery.each(node.childNodes, function() {
+                highlight(this, addItems);
+            });
+        }
+    }
+    var addItems = [];
+    var result = this.each(function() {
+        highlight(this, addItems);
+    });
+    for (var i = 0; i < addItems.length; ++i) {
+        jQuery(addItems[i].parent).before(addItems[i].target);
+    }
+    return result;
+};
+
+/*
+ * backward compatibility for jQuery.browser
+ * This will be supported until firefox bug is fixed.
+ */
+if (!jQuery.browser) {
+    jQuery.uaMatch = function(ua) {
+        ua = ua.toLowerCase();
+
+        var match = /(chrome)[ \/]([\w.]+)/.exec(ua) ||
+            /(webkit)[ \/]([\w.]+)/.exec(ua) ||
+            /(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) ||
+            /(msie) ([\w.]+)/.exec(ua) ||
+            ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) ||
+            [];
+
+        return {
+            browser: match[ 1 ] || "",
+            version: match[ 2 ] || "0"
+        };
+    };
+    jQuery.browser = {};
+    jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true;
+}