"git-rts@gitlab.mpi-sws.org:tchajed/iris.git" did not exist on "1f5898582d842fe69e14acabe034fa933e979253"

Forked from Iris / Iris

6285 commits behind the upstream repository.

Iris 3.0: invariants and weakest preconditions encoded in the logic.

Robbert Krebbers authored 8 years ago

This commit features:

- A simpler model. The recursive domain equation no longer involves a triple
  containing invariants, physical state and ghost state, but just ghost state.
  Invariants and physical state are encoded using (higher-order) ghost state.

- (Primitive) view shifts are formalized in the logic and all properties about
  it are proven in the logic instead of the model. Instead, the core logic
  features only a notion of raw view shifts which internalizing performing frame
  preserving updates.

- A better behaved notion of mask changing view shifts. In particular, we no
  longer have side-conditions on transitivity of view shifts, and we have a
  rule for introduction of mask changing view shifts |={E1,E2}=> P with
  E2 ⊆ E1 which allows to postpone performing a view shift.

- The weakest precondition connective is formalized in the logic using Banach's
  fixpoint. All properties about the connective are proven in the logic instead
  of directly in the model.

- Adequacy is proven in the logic and uses a primitive form of adequacy for
  uPred that only involves raw views shifts and laters.

Some remarks:

- I have removed binary view shifts. I did not see a way to describe all rules
  of the new mask changing view shifts using those.
- There is no longer the need for the notion of "frame shifting assertions" and
  these are thus removed. The rules for Hoare triples are thus also stated in
  terms of primitive view shifts.

TODO:

- Maybe rename primitive view shift into something more sensible
- Figure out a way to deal with closed proofs (see the commented out stuff in
  tests/heap_lang and tests/barrier_client).

1f589858

History

1f589858 8 years ago

History

Name	Last commit	Last update
algebra
benchmark
docs
heap_lang
prelude
program_logic
proofmode
tests
.gitignore
.gitlab-ci.yml
CHANGELOG.md
LICENSE
Makefile
ProofMode.md
README.md
_CoqProject
naming.txt

README.md

IRIS COQ DEVELOPMENT

This is the Coq development of the Iris Project.

Prerequisites

This version is known to compile with:

Coq 8.5pl2
Ssreflect 1.6

For development, better make sure you have a version of Ssreflect that includes commit be724937 (no such version has been released so far, you will have to fetch the development branch yourself). Iris compiles fine even without this patch, but proof bullets will only be in 'strict' (enforcing) mode with the fixed version of Ssreflect.

Building Instructions

Run the following command to build the full development:

make

The development can then be installed as the Coq user contribution iris by running:

make install

Structure

The folder prelude contains an extended "Standard Library" by Robbert Krebbers http://robbertkrebbers.nl/thesis.html.
The folder algebra contains the COFE and CMRA constructions as well as the solver for recursive domain equations.
The folder program_logic builds the semantic domain of Iris, defines and verifies primitive view shifts and weakest preconditions, and builds some language-independent derived constructions (e.g., STSs).
The folder heap_lang defines the ML-like concurrent heap language
- The subfolder lib contains a few derived constructions within this language, e.g., parallel composition. Most notable here s lib/barrier, the implementation and proof of a barrier as described in http://doi.acm.org/10.1145/2818638.
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 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.