Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • robbert/cmra_valid_elim
  • ralf/separable
  • robbert/mono_Z
  • ralf/Z
  • ralf/bi-persistently-emp
  • ralf/mono_Z
  • ci/robbert/big_op_binder
  • robbert/no_native_compute
  • simon/parametric-index
  • ci/robbert/set_solver_eauto
  • ralf/make
  • ci/msammler/nb_state
  • robbert/add_sub
  • ci/general-contractive
  • ralf/has-lc
  • robbert/has_lc_if
  • robbert/bi_cofe
  • robbert/bi_wand_notation
  • robbert/level
  • iris-4.0.0
  • iris-3.6.0
  • iris-3.5.0
  • iris-3.4.0
  • iris-3.3.0
  • iris-3.2.0
  • iris-3.1.0
  • iris-3.0.0
  • iris-2.0
  • iris-2.0-rc2
  • iris-2.0-rc1
  • iris-1.1
  • iris-1.0
  • hope-2015-coq-1
  • appendix-1.0.0
  • appendix-1
36 results
Compare
Forked from Iris / Iris
5314 commits behind the upstream repository.
user avatar
Define `fill` in terms of a `foldl` over `fill_item`.
Robbert Krebbers authored 
This has some advantages:

- Evaluation contexts behave like a proper "Huet's zipper", and thus:
  + We no longer need to reverse the list of evaluation context items in the
    `reshape_expr` tactic.
  + The `fill` function becomes tail-recursive.
- It gives rise to more definitional equalities in simulation proofs using
  binary logical relations proofs.

  In the case of binary logical relations, we simulate an expressions in some
  ambient context, i.e. `fill K e`. Now, whenever we reshape `e` by turning it
  into `fill K' e'`, we end up with `fill K (fill K' e')`. In order to use the
  rules for the expression that is being simulated, we need to turn
  `fill K (fill K' e')` into `fill K'' e'` for some `K'`. In case of the old
  `foldr`-based approach, we had to rewrite using the lemma `fill_app` to
  achieve that. However, in case of the old `foldl`-based `fill`, we have that
  `fill K (fill K' e')` is definitionally equal to `fill (K' ++ K) e'` provided
  that `K'` consists of a bunch of `cons`es (which is always the case, since we
  obtained `K'` by reshaping `e`).

Note that this change hardly affected `heap_lang`. Only the proof of
`atomic_correct` broke. I fixed this by proving a more general lemma
`ectxi_language_atomic` about `ectxi`-languages, which should have been there
in the first place.
6fc9c27e
History
user avatar 6fc9c27e
History
Name Last commit Last update
benchmark
build
docs
theories
.gitignore
.gitlab-ci.yml
CHANGELOG.md
CONTRIBUTING.md
LICENSE
LICENSE-CODE
LICENSE-DOCS
Makefile
ProofMode.md
README.md
_CoqProject
awk.Makefile
naming.txt
opam
opam.pins
README.md

IRIS COQ DEVELOPMENT

This is the Coq development of the Iris Project.

Prerequisites

This version is known to compile with:

  • Coq 8.6
  • Ssreflect 1.6.1
  • A development version of std++

The easiest way to install the correct versions of the dependencies is through opam. Coq packages are available on the coq-released repository, set up by the command:

opam repo add coq-released https://coq.inria.fr/opam/released

Once you got opam set up, just run make build-dep to install the right versions of the dependencies. When the dependencies change, just run make build-dep again.

If you need to work with Coq 8.5, please check out the iris-3.0 branch.

Building Instructions

Run make to build the full development.

Structure

  • The folder algebra contains the COFE and CMRA constructions as well as the solver for recursive domain equations.
  • The folder base_logic defines the Iris base logic and the primitive connectives. It also contains derived constructions that are entirely independent of the choice of resources.
    • The subfolder lib contains some generally useful derived constructions. Most importantly, it defines composeable dynamic resources and ownership of them; the other constructions depend on this setup.
  • The folder program_logic 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.
  • The folder proofmode 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 ProofMode.md.
  • The folder heap_lang defines the ML-like concurrent heap language
  • The folder tests contains modules we use to test our infrastructure. Users of the Iris Coq library should not depend on these modules; they may change or disappear without any notice.

Documentation

A LaTeX version of the core logic definitions and some derived forms is available in docs/iris.tex. A compiled PDF version of this document is available online.