README.html

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
  <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
  <meta http-equiv="Content-Style-Type" content="text/css" />
  <meta name="generator" content="pandoc" />
  <title></title>
  <style type="text/css">code{white-space: pre;}</style>
</head>
<body>
<h1 id="polaris-coq-development">POLARIS COQ DEVELOPMENT</h1>
<p>This is the Coq development of Polaris, an extension of the <a href="http://iris-project.org">Iris Project</a> to support probabilistic relational reasoning. The code includes commits from Iris up through Iris version 3.1.0. The following README is adapted in part from that of the original Iris development.</p>
<h2 id="prerequisites">Prerequisites</h2>
<p>This version is known to compile with the following opam packages:</p>
<ul>
<li>coq 8.8.2</li>
<li>coq-coquelicot 3.0.2</li>
<li>coq-mathcomp-ssreflect 1.7.0</li>
<li>coq-stdpp 1.1.0</li>
<li>coq-flocq 3.0.0</li>
<li>coq-interval 3.4.0</li>
<li>coq-bignums 8.8.0</li>
</ul>
<p>When building from source, we recommend to use opam (1.2.2 or newer) for installing dependencies. This requires adding the following repository:</p>
<pre><code>opam repo add coq-released https://coq.inria.fr/opam/released</code></pre>
<p>You then should be able to run <code>make build-dep</code> to get these dependencies installed.</p>
<p>Run <code>make -jN</code> to build the full development, where <code>N</code> is the number of your CPU cores. (WARNING: the examples can take a long time to build). If you do so, one of the files will print axioms used for a small example proof (see below for the list of axioms used in the development).</p>
<h2 id="clickable-html-correspondence-table">Clickable HTML Correspondence Table</h2>
<p>The files <a href="outline.html" class="uri">outline.html</a> and <a href="outline-diss.html" class="uri">outline-diss.html</a> provide a table giving a correspondence between definitions/theorems in the paper and the first author's dissertation (forthcoming) and their location in the Coq development, as suggested in the <a href="https://docs.google.com/document/d/18IOZR_-zFUDB-2KT-VSDTcl3suge_bSX2758W1kHm5o/edit#heading=h.632p0wk53q0m">Proof Artifact Guidelines</a> by Marianna Rapoport. Clickable links are given to spots in the HTML version of the development produced using coqdoc. These should be prebuilt in versions of this package built for artifact archival, but if they do not exist, you can create them by running <code>make html</code> after building the development.</p>
<h2 id="axioms">Axioms</h2>
<p>The following list of axioms is produced when executing the <code>Print Assumptions</code> command in <a href="theories/tests/prob_heap_lang.v" class="uri">theories/tests/prob_heap_lang.v</a>:</p>
<pre><code>Axioms:
up : R → Z
total_order_T : ∀ r1 r2 : R, {r1 &lt; r2} + {r1 = r2} + {r1 &gt; r2}
ClassicalEpsilon.constructive_indefinite_description : 
∀ (A : Type) (P : A → Prop), (∃ x : A, P x) → {x : A | P x}
completeness : ∀ E : R → Prop,
               bound E → (∃ x : R, E x) → {m : R | is_lub E m}
Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ P
archimed : ∀ r : R, IZR (up r) &gt; r ∧ IZR (up r) - r &lt;= 1
Rplus_opp_r : ∀ r : R, r + - r = 0
Rplus_lt_compat_l : ∀ r r1 r2 : R, r1 &lt; r2 → r + r1 &lt; r + r2
Rplus_comm : ∀ r1 r2 : R, r1 + r2 = r2 + r1
Rplus_assoc : ∀ r1 r2 r3 : R, r1 + r2 + r3 = r1 + (r2 + r3)
Rplus_0_l : ∀ r : R, 0 + r = r
Rplus : R → R → R
Ropp : R → R
Rmult_plus_distr_l : ∀ r1 r2 r3 : R, r1 * (r2 + r3) = r1 * r2 + r1 * r3
Rmult_lt_compat_l : ∀ r r1 r2 : R, 0 &lt; r → r1 &lt; r2 → r * r1 &lt; r * r2
Rmult_comm : ∀ r1 r2 : R, r1 * r2 = r2 * r1
Rmult_assoc : ∀ r1 r2 r3 : R, r1 * r2 * r3 = r1 * (r2 * r3)
Rmult_1_l : ∀ r : R, 1 * r = r
Rmult : R → R → R
Rlt_trans : ∀ r1 r2 r3 : R, r1 &lt; r2 → r2 &lt; r3 → r1 &lt; r3
Rlt_asym : ∀ r1 r2 : R, r1 &lt; r2 → ¬ r2 &lt; r1
Rlt : R → R → Prop
Rinv_l : ∀ r : R, r ≠ 0 → / r * r = 1
Rinv : R → R
R1_neq_R0 : 1 ≠ 0
R1 : R
R0 : R
R : Set</code></pre>
<p>With two exceptions, these axioms are all from the Coq standard library's axiomatization of the real numbers. The two exceptions are:</p>
<pre><code>ClassicalEpsilon.constructive_indefinite_description : 
∀ (A : Type) (P : A → Prop), (∃ x : A, P x) → {x : A | P x}
Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ P</code></pre>
<p>which are again from Coq's standard library, and are used for classical reasoning.</p>
<p>WARNING: If you try to compile this with Coq 8.8.1, it will list additional things as &quot;assumptions&quot; that are not assumptions at all. This is caused by a <a href="https://github.com/coq/coq/issues/8416">bug</a> in Coq.</p>
<h2 id="directory-structure">Directory Structure</h2>
<p>The development is divided into two main parts. The folder theories/ contains the the program logic formalization, while proba/theories/ contains a library for probability theory, and our formalization of the theory of indexed valuations.</p>
<h3 id="original-iris-files-and-outline">Original Iris Files and Outline</h3>
<ul>
<li>The folder <a href="theories/algebra">algebra</a> contains the COFE and CMRA constructions as well as the solver for recursive domain equations.</li>
<li>The folder <a href="theories/base_logic">base_logic</a> defines the Iris base logic and the primitive connectives. It also contains derived constructions that are entirely independent of the choice of resources.</li>
<li>The subfolder <a href="theories/base_logic/lib">lib</a> contains some generally useful derived constructions. Most importantly, it defines composeable dynamic resources and ownership of them; the other constructions depend on this setup.</li>
<li>The folder <a href="theories/program_logic">program_logic</a> specializes the base logic to build Iris, the program logic. This includes weakest preconditions that are defined for any language satisfying some generic axioms, and some derived constructions that work for any such language.</li>
<li>The folder <a href="theories/proofmode">proofmode</a> contains the Iris proof mode, which extends Coq with contexts for persistent and spatial Iris assertions. It also contains tactics for interactive proofs in Iris. Documentation can be found in <a href="ProofMode.md" class="uri">ProofMode.md</a>.</li>
<li>The folder <a href="theories/heap_lang">heap_lang</a> defines the ML-like concurrent heap language, extended with a primitive operation for sampling from Bernoulli distribution.</li>
<li>The subfolder <a href="theories/heap_lang/lib">lib</a> contains a few derived constructions within this language, e.g., parallel composition.</li>
</ul>
<h3 id="overview-of-probabilistic-extensions">Overview of Probabilistic Extensions</h3>
<ul>
<li><a href="theories/program_logic/prob_language.v">program_logic/prob_language.v</a> defines the generic structure of concurrent languages that we consider.</li>
<li><a href="theories/program_logic/prob_lifting.v">program_logic/prob_lifting.v</a> gives the generic proof rules for the new probabilistic extensions of weakest precondition.</li>
<li><a href="theories/heap_lang/adequacy.v">heap_lang/adequacy.v</a> instantiation of the generic soundness theorem for the particular language we consider in the paper. N.B.: in the paper, we state this theorem as if the indexed valuation interpretation of the concrete program <em>always</em> returned a non-empty list and always returned a value; to avoid having to make this term dependently typed to ensure this, here we simply return dummy values for the expectation function if the program is not terminated or if the list of threads is empty.</li>
<li><a href="theories/program_logic/prob_adequacy.v">program_logic/prob_adequacy.v</a> gives the soundness theorem for the probabilistic extensions (that is, the existence of an appropriate triple implies the existence of a coupling up to irrelevance), stated for a generic language.</li>
<li><a href="theories/tests/approx_counter/faa_approx_counter.v">tests/approx_counter/faa_approx_counter.v</a> develops the approximate counter example from the paper, along with the &quot;countTrue&quot; client and an additional client not discussed in the paper. faa_approx_counter_nomax.v and faa_approx_counter_arb.v contain the variations mentioned in section 4.3</li>
<li><a href="theories/tests/skiplist">tests/skiplist/</a> contains the skip list example and client.
<ul>
<li><a href="theories/tests/skiplist/code.v">code.v</a> gives the implementation of skip lists.</li>
<li><a href="theories/tests/skiplist/idxval.v">idxval.v</a> is the monadic model.</li>
<li><a href="theories/tests/skiplist/spec_bundled.v">spec_bundled.v</a> contains the Hoare triples for the skip list.</li>
<li><a href="theories/tests/skiplist/idxval_expected.v">idxval_expected.v</a> derives the upper bound on the expected values</li>
<li><a href="theories/tests/skiplist/client.v">client.v</a> contains a simple example client that uses these triples.</li>
</ul></li>
</ul>
<h3 id="library-for-probability">Library for Probability</h3>
<ul>
<li>The folder <a href="proba/theories/basic">basic</a> defines some lemmas missing from ssreflect that we found useful.</li>
<li>The folder <a href="proba/theories/prob">prob</a> contains a development of discrete probability theory</li>
<li>The folder <a href="proba/theories/measure">measure</a> contains a development of basic measure theory and Lebesgue integration(not used here).</li>
<li>The folder <a href="proba/theories/monad">monad</a> definition of probability distribution list monad</li>
<li>The folder <a href="proba/theories/idxval">idxval</a> contains results on the indexed valuation monad.
<ul>
<li><a href="proba/theories/idxval/irrel_equiv.v">irrel_equiv.v</a> gives the notion of non-deterministic couplings and its theory.</li>
<li><a href="proba/theories/idxval/extrema.v">extrema.v</a> defines expected values and extrema for indexed valuations and sets of them.</li>
</ul></li>
</ul>
<p>At some point this library will probably be split off and distributed as a separate project (parts of it have been already).</p>
</body>
</html>