iGPS & iRSL - encoding of GPS and RSL in Iris
This repository contains the Coq development of iGPS and iRSL, which are variants of GPS and RSL in Iris.
The master branch is known to compile with:
- Coq 8.6
- Ssreflect 1.6.1
- Iris 3.0
The easiest way to build the development is to use OPAM.
Go to coq/ra and then
All the dependencies will be built and installed by OPAM before
the actual compilation of the development.
- The operational semantics is in
machine.v. The language is in
- The base logic is in the
basefolder. The model is in
base/ghosts.v. Each base rule is proven in a separate file.
- iRSL's main rules are in
rsl_instances.v. The model is in
- Non-atomic rules are in
- iGPS's rules are in the
gpsfolder. The model is in
- Examples are in the
tests/message_passing.vcontains a closed proof of MP without Iris statements.