The initial import of files

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
+	"$(COQBIN)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

_CoqProject

+-Q theories iris_c
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+
+theories/lib/env.v
+theories/lib/flock.v
+theories/c_translation/monad.v
+theories/c_translation/translation.v
\ No newline at end of file

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

theories/c_translation/monad.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac.
+From iris.base_logic.lib Require Import fractional.
+From iris_c.lib Require Import env flock.
+
+(* M A := ref (list loc) → Mutex → A *)
+
+(* A → M A *)
+Definition a_ret : val := λ: "a" <> <>, "a".
+
+(* (A → M B) → M A → M B *)
+Definition a_bind : val := λ: "f" "x" "env" "l",
+  let: "a" := "x" "env" "l" in
+  "f" "a" "env" "l".
+
+(* M A → A *)
+Definition a_run : val := λ: "x",
+  let: "env" := ref (newset #()) in
+  let: "l" := newlock #() in
+  "x" "env" "l".
+
+(* M A → M A *)
+Definition a_atomic : val := λ: "x" "env" "l",
+  acquire "l";;
+  let: "k" := newlock #() in
+  let: "a" := "x" "env" "k" in
+  release "l";;
+  "a".
+
+(* (ref (list loc) → A) → M A *)
+Definition a_atomic_env : val := λ: "f" "env" "l",
+  acquire "l";;
+  let: "a" := "f" "env" in
+  release "l";;
+  "a".
+
+(* M A → M B → M (A * B) *)
+Definition a_par : val := λ: "x" "y" "env" "l",
+  "x" "env" "l" ||| "y" "env" "l".
+
+Definition amonadN := nroot .@ "amonad".
+
+Section a_wp.
+  Context `{heapG Σ, lockG Σ, spawnG Σ}.
+
+  Definition awp (e : expr)
+      (R : iProp Σ) (Φ : val → iProp Σ) : iProp Σ :=
+    (∀ (γ : gname) (π : frac) (env : val) (l : val),
+      is_flock γ π false l (env_inv env ∗ R) -∗
+      WP e env l {{ v,
+        Φ v ∗ is_flock γ π false l (env_inv env ∗ R) }}
+    )%I.
+
+  Lemma awp_ret e R Φ :
+    WP e {{ Φ }} -∗ awp (a_ret e) R Φ.
+  Proof.
+    iIntros "Hwp" (γ π env l) "Hlock".
+    rewrite /a_ret. wp_bind e.
+    iApply (wp_wand with "Hwp"); iIntros (v) "HΦ /=".
+    do 3 wp_lam. iFrame.
+  Qed.
+
+  (* Use [IntoVal] everywhere *)
+  Lemma awp_bind (f v : val) R Φ :
+    awp v R (λ w, awp (f w) R Φ) -∗ awp (a_bind f v) R Φ.
+  Proof.
+    iIntros "Hwp" (γ π env l) "Hlock".
+    rewrite /a_bind /=. do 4 wp_lam.
+    wp_bind (v env l).
+    iApply (wp_wand with "[Hwp Hlock]"); first by iApply "Hwp".
+    iIntros (w) "[Hwp Hlock]". wp_let. by iApply "Hwp".
+  Qed.
+
+  Lemma awp_run (v : val) R Φ :
+    R -∗ awp v R (λ w, R -∗ Φ w) -∗
+    WP a_run v {{ Φ }}.
+  Proof.
+    iIntros "HR Hwp". rewrite /a_run /=. wp_let.
+(*
+    wp_apply (newlock_cancel_spec R with "[$]").
+    iIntros (k γ') "Hlock". wp_let. iApply wp_fupd.
+    iApply (wp_wand with "[Hwp Hlock]"); first by iApply "Hwp".
+    iIntros (w) "[HΦ Hlock]".
+    iMod (cancel_lock with "Hlock") as "HR".
+    by iApply "HΦ".
+  Qed.
+*) Admitted.
+
+  Lemma awp_atomic (v : val) R Φ :
+    (R -∗ ∃ R', R' ∗ awp v R' (λ w, R' -∗ R ∗ Φ w)) -∗
+    awp (a_atomic v) R Φ.
+  Proof.
+    iIntros "Hwp" (γ π env l) "Hlock1".
+    rewrite /a_atomic /=. do 3 wp_let.
+    wp_apply (acquire_cancel_spec with "[$]").
+    iIntros "[Hlock1 [Henv HR]] /=". wp_seq.
+    iDestruct ("Hwp" with "HR") as (R') "[HR' Hwp]".
+    wp_apply (newlock_cancel_spec (env_inv env ∗ R')%I with "[$Henv $HR']").
+    iIntros (k γ') "Hlock2". wp_let. wp_bind (v env k).
+    iApply (wp_wand with "[Hwp Hlock2]"); first by iApply "Hwp".
+    iIntros (w) "[HR Hlock2]". wp_let.
+    iMod (cancel_lock with "Hlock2") as "[Henv HR']".
+    iDestruct ("HR" with "HR'") as "[HR HΦ]".
+    wp_apply (release_cancel_spec with "[$Hlock1 $Henv $HR]").
+    iIntros "Hlock1". wp_seq. iFrame.
+  Qed.
+
+  Lemma awp_atomic_env (v : val) R Φ :
+    (∀ env, env_inv env -∗ R -∗
+      WP v env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗
+    awp (a_atomic_env v) R Φ.
+  Proof.
+    iIntros "Hwp" (γ π env l) "Hlock".
+    rewrite /a_atomic_env /=. do 3 wp_lam.
+    wp_apply (acquire_cancel_spec with "[$]").
+    iIntros "[Hlock1 [Henv HR]] /=". wp_seq.
+    iDestruct ("Hwp" with "Henv HR") as "Hwp".
+    wp_apply (wp_wand with "Hwp").
+    iIntros (w) "[Henv [HR HΦ]]". wp_let.
+    wp_apply (release_cancel_spec with "[$Hlock1 $Henv $HR]").
+    iIntros "Hlock". wp_seq. iFrame.
+  Qed.
+
+  Lemma awp_par (v1 v2 : val) R (Ψ1 Ψ2 Φ : val → iProp Σ) :
+    awp v1 R Ψ1 -∗
+    awp v2 R Ψ2 -∗
+    ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗
+    awp (a_par v1 v2) R Φ.
+  Proof.
+    iIntros "Hwp1 Hwp2 HΦ" (γ π env l) "[Hlock1 Hlock2]".
+    rewrite /a_par /=. do 4 wp_lam.
+    iApply (par_spec (λ v, Ψ1 v ∗ is_flock γ _ false l _)%I
+                     (λ v, Ψ2 v ∗ is_flock γ _ false l _)%I
+      with "[Hwp1 Hlock1] [Hwp2 Hlock2]").
+    - wp_lam. by iApply "Hwp1".
+    - wp_lam. by iApply "Hwp2".
+    - iNext. iIntros (w1 w2) "[[HΨ1 $] [HΨ2 $]]".
+      iApply ("HΦ" with "[$] [$]").
+  Qed.
+End a_wp.

theories/c_translation/translation.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac.
+From iris.base_logic.lib Require Import fractional.
+From iris_c.lib Require Import env flock.
+From iris_c.c_translation Require Import monad.
+
+
+Definition a_store : val := λ: "x1" "x2",
+  a_bind (λ: "vv",
+    a_atomic_env (λ: "env",
+      "env" <- set_add (!"env") (!(Fst "vv")) ;;
+      Fst "vv" <- Snd "vv" ;;
+      Snd "vv"
+    )
+  ) (a_par "x1" "x2").
+
+Definition a_load : val := λ: "x",
+  a_bind (λ: "v",
+    a_atomic_env (λ: "env",
+      assert (set_member (!"env") "v" = #false);;
+      !"v"
+    )
+  ) "x".
+
+Definition a_un_op (op : un_op) : val := λ: "x",
+  a_bind (λ: "v", UnOp op "v") "x".
+
+Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
+  a_bind (λ: "vv",
+    BinOp op (Fst "vv") (Snd "vv")
+  ) (a_par "x1" "x2").
+
+(* M () *)
+(* The eta expansion is used to turn it into a value *)
+Definition a_seq : val := λ: "env",
+  a_atomic_env (λ: "env",
+    "env" <- newset #()
+  ) "env".

theories/lib/env.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac.
+From iris.base_logic.lib Require Import fractional.
+
+
+(* Make mutable versions *)
+Fixpoint is_list (hd : val) (xs : list val) : Prop :=
+  match xs with
+  | [] => hd = NONEV
+  | x :: xs => ∃ hd', hd = SOMEV (x,hd') ∧ is_list hd' xs
+  end.
+Definition is_set (hd : val) (X : gset val) : Prop :=
+  ∃ l : list val, is_list hd l ∧ NoDup l ∧ of_list l ≡ X.
+
+Definition is_set_mut `{heapG Σ} (v : val) (X : gset val) : iProp Σ :=
+  (∃ (l : loc) hd,
+    ⌜ v = #l ⌝ ∗ l ↦ hd ∗ ⌜ is_set hd X ⌝)%I.
+
+Definition newset : val := λ: <>, NONEV.
+Definition set_member : val :=
+  rec: "member" "x" "xs" :=
+    match: "xs" with
+      NONE => #false
+    | SOME "p" => if: Fst "p" = "x" then #true else "member" "x" (Snd "p")
+    end.
+Definition set_add : val := λ: "x" "xs",
+  if: set_member "x" "xs"
+  then assert #false
+  else SOME ("x", "xs").
+
+  Definition env_inv `{heapG Σ} (env : val) : iProp Σ :=
+    (∃ X, is_set_mut env X)%I.
\ No newline at end of file

theories/lib/flock.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.heap_lang Require Import spin_lock assert par.
+From iris.algebra Require Import frac.
+From iris.base_logic.lib Require Import fractional.
+
+Section flock.
+  Context `{heapG Σ, lockG Σ, spawnG Σ}.
+
+  Definition is_flock (γ : gname) (π : frac) (b : bool)
+             (l : val) (R : iProp Σ) : iProp Σ.
+  Admitted.
+
+  Lemma is_flock_op γ π1 π2 lk R :
+    is_flock γ (π1 + π2) false lk R ⊣⊢
+      is_flock γ π1 false lk R ∗ is_flock γ π2 false lk R.
+  Proof. Admitted.
+
+  Global Instance is_flock_fractional γ lk R :
+    Fractional (λ π, is_flock γ π false lk R).
+  Proof. intros p q. apply is_flock_op. Qed.
+  Global Instance is_flock_as_fractional γ π lk R :
+    AsFractional (is_flock γ π false lk R) (λ π, is_flock γ π false lk R) π.
+  Proof. split. done. apply _. Qed.
+
+  Lemma newlock_cancel_spec (R : iProp Σ):
+    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_flock γ 1 false lk R }}}.
+  Proof. Admitted.
+
+  Lemma acquire_cancel_spec γ π lk R :
+    {{{ is_flock γ π false lk R }}} acquire lk
+    {{{ RET #(); is_flock γ π true lk R ∗ R }}}.
+  Proof. Admitted.
+
+  Lemma release_cancel_spec γ π lk R :
+    {{{ is_flock γ π true lk R ∗ R }}} release lk
+    {{{ RET #(); is_flock γ π false lk R }}}.
+  Proof. Admitted.
+
+  Lemma cancel_lock γ lk R :
+    is_flock γ 1 false lk R ={⊤}=∗ R.
+  Proof. Admitted.
+
+
+End flock.