Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

.gitlab-ci.yml

+image: coq:8.5
+
+buildjob:
+  tags:
+  - coq
+  script:
+  - make -j9

barrier/barrier.v

@@ -126,6 +126,9 @@ End barrier_proto.
    the module into our namespaces. But Coq doesn't seem to support that...?? *)
 Import barrier_proto.
 
+(* The functors we need. *)
+Definition barrierFs := stsF sts `::` agreeF `::` pnil.
+
 (** Now we come to the Iris part of the proof. *)
 Section proof.
   Context {Σ : iFunctorG} (N : namespace).

barrier/client.v

 From barrier Require Import barrier.
+From program_logic Require Import auth sts saved_prop hoare ownership.
 (* FIXME This needs to be imported even though barrier exports it *)
 From heap_lang Require Import notation.
 Import uPred.
@@ -17,9 +18,7 @@ Section client.
     heapN ⊥ N → heap_ctx heapN ⊑ || client {{ λ _, True }}.
   Proof.
     intros ?. rewrite /client.
-    (* FIXME: wp (eapply newchan_spec with (P:=True%I)). *)
-    wp_focus (newchan _).
-    rewrite -(newchan_spec N heapN True%I) //.
+    ewp eapply (newchan_spec N heapN True%I); last done.
     apply sep_intro_True_r; first done.
     apply forall_intro=>l. apply wand_intro_l. rewrite right_id.
     wp_let. etrans; last eapply wait_spec.
@@ -27,3 +26,21 @@ Section client.
   Qed.
 
 End client.
+
+Section ClosedProofs.
+  Definition Σ : iFunctorG := heapF .:: barrierFs .++ endF.
+  Notation iProp := (iPropG heap_lang Σ).
+
+  Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
+  Proof.
+    apply ht_alt. rewrite (heap_alloc ⊤ (ndot nroot "Barrier")); last first.
+    { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
+      move=>? _. exact I. }
+    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
+    rewrite -(client_safe (nroot .: "Heap" ) (nroot .: "Barrier" )) //.
+    (* This, too, should be automated. *)
+    apply ndot_ne_disjoint. discriminate.
+  Qed.
+
+  Print Assumptions client_safe_closed.
+End ClosedProofs.

heap_lang/heap.v

@@ -8,6 +8,7 @@ Import uPred.
    predicates over finmaps instead of just ownP. *)
 
 Definition heapRA := mapRA loc (exclRA (leibnizC val)).
+Definition heapF := authF heapRA.
 
 Class heapG Σ := HeapG {
   heap_inG : inG heap_lang Σ (authRA heapRA);
@@ -20,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl.
 Definition of_heap : heapRA → state := omap (maybe Excl).
 
 Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
-  auth_own heap_name {[ l := Excl v ]}.
+  auth_own heap_name ({[ l := Excl v ]} : heapRA).
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
   ownP (of_heap h).
 Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
@@ -103,7 +104,7 @@ Section heap.
     P ⊑ || Alloc e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
-    trans (|={E}=> auth_own heap_name ∅ ★ P)%I.
+    trans (|={E}=> auth_own heap_name (∅ : heapRA) ★ P)%I.
     { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
     apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
       with N heap_name ∅; simpl; eauto with I.

heap_lang/tests.v

@@ -63,8 +63,6 @@ Section LiftingTests.
   Proof.
     wp_lam. wp_op=> ?; wp_if.
     - wp_op. wp_op.
-      (* TODO: Can we use the wp tactic again here? It seems that the tactic fails if there
-         are goals being generated. That should not be the case. *)
       ewp apply FindPred_spec; last omega.
       wp_op. by replace (n - 1) with (- (-n + 2 - 1)) by omega.
     - by ewp apply FindPred_spec; eauto with omega.
@@ -78,18 +76,15 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  Definition Σ : iFunctorG := λ _, authF (constF heapRA).
+  Definition Σ : iFunctorG := heapF .:: endF.
   Notation iProp := (iPropG heap_lang Σ).
 
-  Instance: authG heap_lang Σ heapRA.
-  Proof. split; try apply _. by exists 1%nat. Qed.
-
-  Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
+  Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
   Proof.
     apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
   Qed.
 
-  Print Assumptions heap_e_hoare.
+  Print Assumptions heap_e_closed.
 End ClosedProofs.

heap_lang/wp_tactics.v

@@ -190,6 +190,7 @@ Tactic Notation "wp" ">" tactic(tac) :=
   end.
 Tactic Notation "wp" tactic(tac) := (wp> tac); [wp_strip_later|..].
 
-(* In case the precondition does not match *)
+(* In case the precondition does not match.
+   TODO: Have one tactic unifying wp and ewp. *)
 Tactic Notation "ewp" tactic(tac) := wp (etrans; [|tac]).
 Tactic Notation "ewp" ">" tactic(tac) := wp> (etrans; [|tac]).

prelude/functions.v

@@ -29,3 +29,43 @@ Section functions.
   Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
 
 End functions.
+
+(** "Cons-ing" of functions from nat to T *)
+(* Coq's standard lists are not universe polymorphic. Hence we have to re-define them. Ouch.
+   TODO: If we decide to end up going with this, we should move this elsewhere. *)
+Polymorphic Inductive plist {A : Type} : Type :=
+| pnil : plist
+| pcons: A → plist → plist.
+Arguments plist : clear implicits.
+
+Polymorphic Fixpoint papp {A : Type} (l1 l2 : plist A) : plist A :=
+  match l1 with
+  | pnil => l2
+  | pcons a l => pcons a (papp l l2)
+  end.
+
+(* TODO: Notation is totally up for debate. *)
+Infix "`::`" := pcons (at level 60, right associativity) : C_scope.
+Infix "`++`" := papp (at level 60, right associativity) : C_scope.
+
+Polymorphic Definition fn_cons {T : Type} (t : T) (f: nat → T) : nat → T :=
+  λ n, match n with
+       | O => t
+       | S n => f n
+       end.
+
+Polymorphic Fixpoint fn_mcons {T : Type} (ts : plist T) (f : nat → T) : nat → T :=
+  match ts with
+  | pnil => f
+  | pcons t ts => fn_cons t (fn_mcons ts f)
+  end.
+
+(* TODO: Notation is totally up for debate. *)
+Infix ".::" := fn_cons (at level 60, right associativity) : C_scope.
+Infix ".++" := fn_mcons (at level 60, right associativity) : C_scope.
+
+Polymorphic Lemma fn_mcons_app {T : Type} (ts1 ts2 : plist T) f :
+  (ts1 `++` ts2) .++ f = ts1 .++ (ts2 .++ f).
+Proof.
+  induction ts1; simpl; eauto. congruence.
+Qed.

program_logic/auth.v

@@ -9,6 +9,13 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
   auth_timeless (a : A) :> Timeless a;
 }.
 
+(* TODO: This shadows algebra.auth.authF. *)
+Definition authF (A : cmraT) := constF (authRA A).
+
+Instance authG_inGF (A : cmraT) `{CMRAIdentity A} `{∀ a : A, Timeless a}
+         `{inGF Λ Σ (authF A)} : authG Λ Σ A.
+Proof. split; try apply _. move:(@inGF_inG Λ Σ (authF A)). auto. Qed.
+
 Section definitions.
   Context `{authG Λ Σ A} (γ : gname).
   (* TODO: Once we switched to RAs, it is no longer necessary to remember that a

program_logic/ghost_ownership.v

+From prelude Require Export functions.
 From algebra Require Export iprod.
 From program_logic Require Export pviewshifts.
 From program_logic Require Import ownership.
@@ -144,3 +145,22 @@ Proof.
   apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
 Qed.
 End global.
+
+(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
+   the functor breaks badly because Coq is unable to infer the correct
+   typeclasses, it does not unfold the functor. *)
+Class inGF (Λ : language) (Σ : gid → iFunctor) (F : iFunctor) := InGF {
+  inGF_id : gid;
+  inGF_prf : F = Σ inGF_id;
+}.
+
+Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
+Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.
+
+Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
+Proof. exists 0. done. Qed.
+
+Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
+Proof. exists (S inGF_id). apply inGF_prf. Qed.
+
+Definition endF : gid → iFunctor := const (constF unitRA).

program_logic/namespaces.v

@@ -7,19 +7,22 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
 Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
+Infix ".:" := ndot (at level 19, left associativity) : C_scope.
+Notation "(.:)" := ndot : C_scope.
+
 Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
 Lemma nclose_nroot : nclose nroot = ⊤.
 Proof. by apply (sig_eq_pi _). Qed.
 Lemma encode_nclose N : encode N ∈ nclose N.
 Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
-Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N.
+Lemma nclose_subseteq `{Countable A} N x : nclose (N .: x) ⊆ nclose N.
 Proof.
   intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
-  destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
+  destruct (list_encode_suffix N (N .: x)) as [q' ?]; [by exists [encode x]|].
   by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
 Qed.
-Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N.
+Lemma ndot_nclose `{Countable A} N x : encode (N .: x) ∈ nclose N.
 Proof. apply nclose_subseteq with x, encode_nclose. Qed.
 
 Instance ndisjoint : Disjoint namespace := λ N1 N2,
@@ -33,16 +36,16 @@ Section ndisjoint.
   Global Instance ndisjoint_comm : Comm iff ndisjoint.
   Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
 
-  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → ndot N x ⊥ ndot N y.
-  Proof. intros Hxy. exists (ndot N x), (ndot N y); naive_solver. Qed.
+  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N .: x ⊥ N .: y.
+  Proof. intros Hxy. exists (N .: x), (N .: y); naive_solver. Qed.
 
-  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → ndot N1 x ⊥ N2.
+  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .: x ⊥ N2.
   Proof.
     intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
     split_and?; try done; []. by apply suffix_of_cons_r.
   Qed.
 
-  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ ndot N2 x .
+  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 .: x .
   Proof. rewrite ![N1 ⊥ _]comm. apply ndot_preserve_disjoint_l. Qed.
 
   Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ∩ nclose N2 = ∅.

program_logic/saved_prop.v

@@ -5,6 +5,9 @@ Import uPred.
 Notation savedPropG Λ Σ :=
   (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
 
+Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
+Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed.
+
 Definition saved_prop_own `{savedPropG Λ Σ}
     (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
   own γ (to_agree (Next (iProp_unfold P))).

program_logic/sts.v

@@ -8,6 +8,12 @@ Class stsG Λ Σ (sts : stsT) := StsG {
 }.
 Coercion sts_inG : stsG >-> inG.
 
+Definition stsF (sts : stsT) := constF (stsRA sts).
+
+Instance stsG_inGF sts `{Inhabited (sts.state sts)}
+         `{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts.
+Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed.
+
 Section definitions.
   Context `{i : stsG Λ Σ sts} (γ : gname).
   Import sts.