Initial commit

.gitignore

+*.vo
+*.vio
+*.v.d
+*.glob
+*.cache
+*.aux
+\#*\#
+.\#*
+*~
+*.bak
+Makefile.coq
+Makefile.coq.conf
+.coq-native/
+build-dep

.gitlab-ci.yml

+image: ralfjung/opam-ci:latest
+
+variables:
+  CPU_CORES: "9"
+
+.template: &template
+  tags:
+  - fp-timing
+  script:
+  # prepare
+  - . build/opam-ci.sh $OPAM_PINS
+  - env | egrep '^(CI_BUILD_REF|CI_RUNNER)' > build-env.txt
+  # build
+  - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
+  - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
+  - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
+  - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - opamroot/
+  only:
+  - master
+  - /^ci/
+
+build-coq.8.7:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.7.dev   coq-mathcomp-ssreflect version dev"
+  except:
+  - triggers
+
+build-coq.8.6.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.1"
+    VALIDATE: "1"
+  artifacts:
+    paths:
+    - build-time.txt
+    - build-env.txt
+  except:
+  - triggers
+
+build-iris.dev:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.1   coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
+  only:
+  - triggers

Makefile

+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	+@make -f Makefile.coq $@
+
+all: Makefile.coq
+	+@make -f Makefile.coq all
+.PHONY: all
+
+clean: Makefile.coq
+	+@make -f Makefile.coq clean
+	find theories \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
+	rm -f Makefile.coq
+.PHONY: clean
+
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
+# filename, so we do some file gymnastics.
+Makefile.coq: _CoqProject Makefile awk.Makefile
+	coq_makefile -f _CoqProject -o Makefile.coq
+	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
+
+# Install build-dependencies
+build-dep/opam: opam Makefile
+	# Creating the build-dep package.
+	@mkdir -p build-dep
+	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
+	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+
+build-dep: build-dep/opam phony
+	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything.
+	@# Upgrading is needed in case the pin already exists, but the builddep package changed.
+	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
+	  echo "# Pinning build-dep package." && \
+	  opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	  echo "# Updating build-dep package." && \
+	  opam upgrade "$$BUILD_DEP_PACKAGE"
+
+# Some files that do *not* need to be forwarded to Makefile.coq
+Makefile: ;
+_CoqProject: ;
+awk.Makefile: ;
+opam: ;
+
+# Phony wildcard targets
+phony: ;
+.PHONY: phony

README.md

+# IRIS EXAMPLES
+
+Some example verification demonstrating the use of Iris.
+
+## Prerequisites
+
+This version is known to compile with:
+
+ - Coq 8.6.1
+ - Ssreflect 1.6.1
+ - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
+
+The easiest way to install the correct versions of the dependencies is through
+opam.  Once you got opam set up, just run `make build-dep` to install the right
+versions of the dependencies.  When the dependencies change (e.g., a newer
+version of Iris is needed), just run `make build-dep` again.
+
+Alternatively, you can manually determine the required Iris commit by consulting
+the `opam.pins` file.
+
+## Building Instructions
+
+Run `make` to build the full development.
+
+## For Developers: How to update the Iris dependency
+
+- Do the change in Iris, push it.
+- In iris-atomic, change opam.pins to point to the new commit.
+- Run "make build-dep" (in iris-example) to install the new version of Iris.
+- You may have to do "make clean" as Coq will likely complain about .vo file
+  mismatches.

_CoqProject

+-Q theories iris_examples
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+theories/barrier/proof.v
+theories/barrier/specification.v
+theories/barrier/barrier.v
+theories/barrier/protocol.v

awk.Makefile

+# awk program that patches the Makefile generated by Coq.
+
+# Detect the name this project will be installed under.
+/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
+# Wow, POSIX awk is really broken.  I mean, isn't it supposed to be a text processing language?
+# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
+# we can just split the string at '/' here.
+	split($0, PIECES, /\//);
+	PROJECT=PIECES[2];
+}
+
+# Patch the uninstall target to work properly, and to also uninstall stale files.
+# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
+# This (and the section above) can be removed once we no longer support Coq 8.6.
+/^uninstall: / {
+	print "uninstall:";
+	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
+	getline;
+	next
+}
+
+# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
+# that the .vio files are up-to-date, and (b) only schedule vio2vo for those
+# files where the .vo is *older* than the .vio.
+/^vio2vo:/ {
+	print "quick2vo:";
+	print "\t@make -j $(J) quick"
+	print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
+	print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
+	print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
+	print ".PHONY: quick2vo"
+}
+
+# This forwards all unchanged lines
+1

build/opam-ci.sh

+#!/bin/bash
+set -e
+## This script installs the build dependencies for CI builds.
+function run_and_print() {
+    echo "$ $@"
+    "$@"
+}
+
+# Prepare OPAM configuration
+export OPAMROOT="$(pwd)/opamroot"
+export OPAMJOBS="$((2*$CPU_CORES))"
+export OPAM_EDITOR="$(which false)"
+
+# Make sure we got a good OPAM.
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
+eval `opam conf env`
+
+# Make sure the pin for the builddep package is not stale.
+run_and_print make build-dep/opam
+
+# Update repositories
+if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
+    # last update was more than a day ago
+    run_and_print opam update
+else
+    # only update iris-dev, and only if it already exists
+    if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
+fi
+# Make sure we got the right set of repositories registered
+if echo "$@" | fgrep "dev"; then
+    # We are compiling against a dev version of something.  Get ourselves the dev repositories.
+    test -d "$OPAMROOT/repo/coq-extra-dev" || run_and_print opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
+    test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+else
+    # No dev version, make sure we do not have the dev repositories.
+    test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
+    test -d "$OPAMROOT/repo/coq-core-dev" && run_and_print opam repo remove coq-core-dev
+fi
+test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+echo
+
+# We really want to run all of the following in one opam transaction, but due to opam limitations,
+# that is not currently possible.
+
+# Install fixed versions of some dependencies.
+echo
+while (( "$#" )); do # while there are arguments left
+    PACKAGE="$1" ; shift
+    KIND="$1" ; shift
+    VERSION="$1" ; shift
+
+    # Check if the pin is already set
+    read -a PIN <<< $(opam pin list | (egrep "^$PACKAGE[. ]"))
+    if [[ "${PIN[1]}" == "$KIND" && "${PIN[2]}" == "$VERSION" ]]; then
+        echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
+    else
+        echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
+        run_and_print opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
+    fi
+done
+
+# Upgrade cached things.
+echo
+echo "[opam-ci] Upgrading opam"
+run_and_print opam upgrade -y
+
+# Install build-dependencies.
+echo
+echo "[opam-ci] Installing build-dependencies"
+make build-dep OPAMFLAGS=-y
+
+# done
+echo
+coqc -v

opam

+opam-version: "1.2"
+name: "coq-iris-examples"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+homepage: "http://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/FP/iris-examples/issues"
+dev-repo: "https://gitlab.mpi-sws.org/FP/iris-examples.git"
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
+depends: [
+  "coq-iris" { (= "dev.2017-10-19.0") | (= "dev") }
+]

theories/barrier/barrier.v

+From iris.heap_lang Require Export notation.
+Set Default Proof Using "Type".
+
+Definition newbarrier : val := λ: <>, ref #false.
+Definition signal : val := λ: "x", "x" <- #true.
+Definition wait : val :=
+  rec: "wait" "x" := if: !"x" then #() else "wait" "x".

theories/barrier/proof.v

+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang.
+From iris.heap_lang.lib.barrier Require Export barrier.
+From stdpp Require Import functions.
+From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
+From iris.heap_lang Require Import proofmode.
+From iris.heap_lang.lib.barrier Require Import protocol.
+Set Default Proof Using "Type".
+
+(** The CMRAs/functors we need. *)
+Class barrierG Σ := BarrierG {
+  barrier_stsG :> stsG Σ sts;
+  barrier_savedPropG :> savedPropG Σ idCF;
+}.
+Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
+
+Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
+Proof. solve_inG. Qed.
+
+(** Now we come to the Iris part of the proof. *)
+Section proof.
+Context `{!heapG Σ, !barrierG Σ} (N : namespace).
+Implicit Types I : gset gname.
+
+Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
+  (∃ Ψ : gname → iProp Σ,
+    ▷ (P -∗ [∗ set] i ∈ I, Ψ i) ∗ [∗ set] i ∈ I, saved_prop_own i (Ψ i))%I.
+
+Coercion state_to_val (s : state) : val :=
+  match s with State Low _ => #false | State High _ => #true end.
+Arguments state_to_val !_ / : simpl nomatch.
+
+Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ :=
+  match s with State Low _ => P | State High _ => True%I end.
+Arguments state_to_prop !_ _ / : simpl nomatch.
+
+Definition barrier_inv (l : loc) (P : iProp Σ) (s : state) : iProp Σ :=
+  (l ↦ s ∗ ress (state_to_prop s P) (state_I s))%I.
+
+Definition barrier_ctx (γ : gname) (l : loc) (P : iProp Σ) : iProp Σ :=
+  sts_ctx γ N (barrier_inv l P).
+
+Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
+  (∃ γ, barrier_ctx γ l P ∗ sts_ownS γ low_states {[ Send ]})%I.
+
+Definition recv (l : loc) (R : iProp Σ) : iProp Σ :=
+  (∃ γ P Q i,
+    barrier_ctx γ l P ∗ sts_ownS γ (i_states i) {[ Change i ]} ∗
+    saved_prop_own i Q ∗ ▷ (Q -∗ R))%I.
+
+Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) :
+  PersistentP (barrier_ctx γ l P).
+Proof. apply _. Qed.
+
+(** Setoids *)
+Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
+Proof. solve_proper. Qed.
+Global Instance state_to_prop_ne s :
+  NonExpansive (state_to_prop s).
+Proof. solve_proper. Qed.
+Global Instance barrier_inv_ne n l :
+  Proper (dist n ==> eq ==> dist n) (barrier_inv l).
+Proof. solve_proper. Qed.
+Global Instance barrier_ctx_ne γ l : NonExpansive (barrier_ctx γ l).
+Proof. solve_proper. Qed. 
+Global Instance send_ne l : NonExpansive (send l).
+Proof. solve_proper. Qed.
+Global Instance recv_ne l : NonExpansive (recv l).
+Proof. solve_proper. Qed.
+
+(** Helper lemmas *)
+Lemma ress_split i i1 i2 Q R1 R2 P I :
+  i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
+  saved_prop_own i Q -∗ saved_prop_own i1 R1 -∗ saved_prop_own i2 R2 -∗
+  (Q -∗ R1 ∗ R2) -∗ ress P I -∗
+  ress P ({[i1;i2]} ∪ I ∖ {[i]}).
+Proof.
+  iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
+  iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
+  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
+  - iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
+    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
+    iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
+    iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
+    rewrite -assoc_L !big_opS_fn_insert'; [|abstract set_solver ..].
+    by iFrame.
+  - rewrite -assoc_L !big_opS_fn_insert; [|abstract set_solver ..]. eauto.
+Qed.
+
+(** Actual proofs *)
+Lemma newbarrier_spec (P : iProp Σ) :
+  {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
+Proof.
+  iIntros (Φ) "_ HΦ".
+  rewrite -wp_fupd /newbarrier /=. wp_seq. wp_alloc l as "Hl".
+  iApply ("HΦ" with "[> -]").
+  iMod (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
+  iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
+    as (γ') "[#? Hγ']"; eauto.
+  { iNext. rewrite /barrier_inv /=. iFrame.
+    iExists (const P). rewrite !big_opS_singleton /=. eauto. }
+  iAssert (barrier_ctx γ' l P)%I as "#?".
+  { done. }
+  iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
+    ∗ sts_ownS γ' low_states {[Send]})%I with "[> -]" as "[Hr Hs]".
+  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+    - set_solver.
+    - iApply (sts_own_weaken with "Hγ'");
+        auto using sts.closed_op, i_states_closed, low_states_closed;
+        abstract set_solver. }
+  iModIntro. iSplitL "Hr".
+  - iExists γ', P, P, γ. iFrame. auto.
+  - rewrite /send. auto.
+Qed.
+
+Lemma signal_spec l P :
+  {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}.
+Proof.
+  rewrite /signal /=.
+  iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_let.
+  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
+  destruct p; [|done]. wp_store.
+  iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
+  iMod ("Hclose" $! (State High I) (∅ : set token) with "[-]"); last done.
+  iSplit; [iPureIntro; by eauto using signal_step|].
+  rewrite /barrier_inv /ress /=. iNext. iFrame "Hl".
+  iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
+  iNext. iIntros "_"; by iApply "Hr".
+Qed.
+
+Lemma wait_spec l P:
+  {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
+Proof.
+  rename P into R.
+  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
+  iLöb as "IH". wp_rec. wp_bind (! _)%E.
+  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
+  wp_load. destruct p.
+  - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
+    { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
+    { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
+    iModIntro. wp_if.
+    iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
+  - (* a High state: the comparison succeeds, and we perform a transition and
+    return to the client *)
+    iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
+    iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
+    iAssert (▷ Ψ i ∗ ▷ [∗ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
+    { iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
+    iMod ("Hclose" $! (State High (I ∖ {[ i ]})) ∅ with "[HΨ' Hl Hsp]").
+    { iSplit; [iPureIntro; by eauto using wait_step|].
+      rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
+    iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
+    iModIntro. wp_if.
+    iApply "HΦ". iApply "HQR". by iRewrite "Heq".
+Qed.
+
+Lemma recv_split E l P1 P2 :
+  ↑N ⊆ E → recv l (P1 ∗ P2) ={E}=∗ recv l P1 ∗ recv l P2.
+Proof.
+  rename P1 into R1; rename P2 into R2.
+  iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
+  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
+    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
+  iMod (saved_prop_alloc_strong (R1: ∙%CF (iProp Σ)) I) as (i1) "[% #Hi1]".
+  iMod (saved_prop_alloc_strong (R2: ∙%CF (iProp Σ)) (I ∪ {[i1]}))
+    as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
+  rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
+  iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
+                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
+  { iSplit; first by eauto using split_step.
+    rewrite /barrier_inv /=. iNext. iFrame "Hl".
+    by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
+  iAssert (sts_ownS γ (i_states i1) {[Change i1]}
+    ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with "[> -]" as "[Hγ1 Hγ2]".
+  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
+    - abstract set_solver.
+    - iApply (sts_own_weaken with "Hγ");
+        eauto using sts.closed_op, i_states_closed.
+      abstract set_solver. }
+  iModIntro; iSplitL "Hγ1".
+  - iExists γ, P, R1, i1. iFrame; auto.
+  - iExists γ, P, R2, i2. iFrame; auto.
+Qed.
+
+Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2.
+Proof.
+  iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
+  iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
+  iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
+Qed.
+
+Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
+Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
+End proof.
+
+Typeclasses Opaque barrier_ctx send recv.

theories/barrier/protocol.v

+From iris.algebra Require Export sts.
+From iris.base_logic Require Import lib.own.
+From stdpp Require Export gmap.
+Set Default Proof Using "Type".
+
+(** The STS describing the main barrier protocol. Every state has an index-set
+    associated with it. These indices are actually [gname], because we use them
+    with saved propositions. *)
+Inductive phase := Low | High.
+Record state := State { state_phase : phase; state_I : gset gname }.
+Add Printing Constructor state.
+Inductive token := Change (i : gname) | Send.
+
+Global Instance stateT_inhabited: Inhabited state := populate (State Low ∅).
+Global Instance Change_inj : Inj (=) (=) Change.
+Proof. by injection 1. Qed.
+
+Inductive prim_step : relation state :=
+  | ChangeI p I2 I1 : prim_step (State p I1) (State p I2)
+  | ChangePhase I : prim_step (State Low I) (State High I).
+
+Definition tok (s : state) : set token :=
+  {[ t | ∃ i, t = Change i ∧ i ∉ state_I s ]} ∪
+  (if state_phase s is High then {[ Send ]} else ∅).
+Global Arguments tok !_ /.
+
+Canonical Structure sts := sts.STS prim_step tok.
+
+(* The set of states containing some particular i *)
+Definition i_states (i : gname) : set state := {[ s | i ∈ state_I s ]}.
+
+(* The set of low states *)
+Definition low_states : set state := {[ s | state_phase s = Low ]}.
+
+Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
+Proof.
+  split; first (intros [[] I]; set_solver).
+  (* If we do the destruct of the states early, and then inversion
+     on the proof of a transition, it doesn't work - we do not obtain
+     the equalities we need. So we destruct the states late, because this
+     means we can use "destruct" instead of "inversion". *)
+  intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
+  inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
+  destruct Htrans as [[] ??|]; done || set_solver.
+Qed.
+
+Lemma low_states_closed : sts.closed low_states {[ Send ]}.
+Proof.
+  split; first (intros [??]; set_solver).
+  intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
+  inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
+  destruct Htrans as [[] ??|]; done || set_solver.
+Qed.
+
+(* Proof that we can take the steps we need. *)
+Lemma signal_step I : sts.steps (State Low I, {[Send]}) (State High I, ∅).
+Proof. apply rtc_once. constructor; first constructor; set_solver. Qed.
+
+Lemma wait_step i I :
+  i ∈ I →
+  sts.steps (State High I, {[ Change i ]}) (State High (I ∖ {[ i ]}), ∅).
+Proof.
+  intros. apply rtc_once.
+  constructor; first constructor; [set_solver..|].
+  apply elem_of_equiv=>-[j|]; last set_solver.
+  destruct (decide (i = j)); set_solver.
+Qed.
+
+Lemma split_step p i i1 i2 I :
+  i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
+  sts.steps
+    (State p I, {[ Change i ]})
+    (State p ({[i1; i2]} ∪ I ∖ {[i]}), {[ Change i1; Change i2 ]}).
+Proof.
+  intros. apply rtc_once. constructor; first constructor.
+  - destruct p; set_solver.
+  - destruct p; set_solver.
+  - apply elem_of_equiv=> /= -[j|]; last set_solver.
+    set_unfold; rewrite !(inj_iff Change).
+    assert (Change j ∈ match p with Low => ∅ : set token | High => {[Send]} end ↔ False)
+      as -> by (destruct p; set_solver).
+    destruct (decide (i1 = j)) as [->|]; first naive_solver.
+    destruct (decide (i2 = j)) as [->|]; first naive_solver.