Commit f24fd7c3 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'nclose_subseteq' into 'master'

Use notation N @⊆ E to avoid ambiguity.

Since `nclose : namespace → coPset` is declared as a coercion, the notation `nclose N ⊆ E` was pretty printed as `N ⊆ E`. However, `N ⊆ E` could not be typechecked because type checking goes from left to right, and as such would look for an instance `SubsetEq namespace`, which causes the right hand side to be ill-typed.

See merge request !24
parents 608e347c 9bf8b8ba
Pipeline #3047 passed with stage
in 10 minutes and 26 seconds
......@@ -6,7 +6,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
## Iris 3.0 (unfinished)
* There now is a deprecation process. The modules `*.deprecated`
contains deprecated notations and definitions that are provided for
contain deprecated notations and definitions that are provided for
backwards compatibility and will be removed in a future version of Iris.
* View shifts are radically simplified to just internalize frame-preserving
updates. Weakestpre is defined inside the logic, and invariants and view
......@@ -22,6 +22,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Changed notation for embedding Coq assertions into Iris. The new notation
is ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope.
(The old notations are provided in `base_logic.deprecated`.)
* Up-closure of namespaces is now a notation (↑) instead of a coercion.
* With invariants and the physical state being handled in the logic, there
is no longer any reason to demand the CMRA unit to be discrete.
* The language can now fork off multiple threads at once.
......
......@@ -128,10 +128,10 @@ Section auth.
Qed.
Lemma auth_open E N γ a :
nclose N E
auth_ctx γ N f φ auth_own γ a ={E,EN}= t,
N E
auth_ctx γ N f φ auth_own γ a ={E,EN}= t,
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={EN,E}= auth_own γ b.
(f t, a) ~l~> (f u, b) φ u ={EN,E}= auth_own γ b.
Proof.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
......
......@@ -105,7 +105,7 @@ Proof.
Qed.
Lemma box_delete E f P Q γ :
nclose N E
N E
f !! γ = Some false
slice N γ Q box N f P ={E}= P',
(P (Q P')) box N (delete γ f) P'.
......@@ -125,7 +125,7 @@ Proof.
Qed.
Lemma box_fill E f γ P Q :
nclose N E
N E
f !! γ = Some false
slice N γ Q Q box N f P ={E}= box N (<[γ:=true]> f) P.
Proof.
......@@ -144,7 +144,7 @@ Proof.
Qed.
Lemma box_empty E f P Q γ :
nclose N E
N E
f !! γ = Some true
slice N γ Q box N f P ={E}= Q box N (<[γ:=false]> f) P.
Proof.
......@@ -164,7 +164,7 @@ Proof.
Qed.
Lemma box_fill_all E f P :
nclose N E
N E
box N f P P ={E}= box N (const true <$> f) P.
Proof.
iIntros (?) "[H HP]"; iDestruct "H" as (Φ) "[#HeqP Hf]".
......@@ -181,7 +181,7 @@ Proof.
Qed.
Lemma box_empty_all E f P :
nclose N E
N E
map_Forall (λ _, (true =)) f
box N f P ={E}= P box N (const false <$> f) P.
Proof.
......
......@@ -50,8 +50,7 @@ Section proofs.
iMod (inv_alloc N _ (P own γ 1%Qp)%I with "[HP]"); eauto.
Qed.
Lemma cinv_cancel E N γ P :
nclose N E cinv N γ P cinv_own γ 1 ={E}= P.
Lemma cinv_cancel E N γ P : N E cinv N γ P cinv_own γ 1 ={E}= P.
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
......@@ -59,8 +58,8 @@ Section proofs.
Qed.
Lemma cinv_open E N γ p P :
nclose N E
cinv N γ P cinv_own γ p ={E,EN}= P cinv_own γ p ( P ={EN,E}= True).
N E
cinv N γ P cinv_own γ p ={E,EN}= P cinv_own γ p ( P ={E∖↑N,E}= True).
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose".
......
......@@ -6,7 +6,7 @@ Import uPred.
(** Derived forms and lemmas about them. *)
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i nclose N ownI i P)%I.
( i, i N ownI i P)%I.
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
Definition inv {Σ i} := proj1_sig inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
......@@ -30,8 +30,8 @@ Proof. rewrite inv_eq /inv; apply _. Qed.
Lemma inv_alloc N E P : P ={E}= inv N P.
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
iMod (ownI_alloc ( nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
- intros Ef. exists (coPpick (nclose N coPset.of_gset Ef)).
iMod (ownI_alloc ( N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
- intros Ef. exists (coPpick ( N coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
......@@ -41,19 +41,19 @@ Proof.
Qed.
Lemma inv_open E N P :
nclose N E inv N P ={E,EN}= P ( P ={EN,E}= True).
N E inv N P ={E,E∖↑N}= P ( P ={E∖↑N,E}= True).
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
iIntros "(Hw & [HE $] & $) !> !>".
iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
Qed.
Lemma inv_open_timeless E N P `{!TimelessP P} :
nclose N E inv N P ={E,EN}= P (P ={EN,E}= True).
N E inv N P ={E,E∖↑N}= P (P ={E∖↑N,E}= True).
Proof.
iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto.
......
......@@ -16,10 +16,11 @@ Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux.
Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N).
Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed.
Coercion nclose := proj1_sig nclose_aux.
Instance nclose : UpClose namespace coPset := proj1_sig nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux.
Infix ".@" := ndot (at level 19, left associativity) : C_scope.
Notation "N .@ x" := (ndot N x)
(at level 19, left associativity, format "N .@ x") : C_scope.
Notation "(.@)" := ndot (only parsing) : C_scope.
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 nclose N2.
......@@ -27,53 +28,55 @@ Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ⊥ nclose N2.
Section namespace.
Context `{Countable A}.
Implicit Types x y : A.
Implicit Types N : namespace.
Implicit Types E : coPset.
Global Instance ndot_inj : Inj2 (=) (=) (=) (@ndot A _ _).
Proof. intros N1 x1 N2 x2; rewrite !ndot_eq=> ?; by simplify_eq. Qed.
Lemma nclose_nroot : nclose nroot = .
Lemma nclose_nroot : nroot = .
Proof. rewrite nclose_eq. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose N : encode N nclose N.
Lemma encode_nclose N : encode N N.
Proof.
rewrite nclose_eq.
by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _).
Qed.
Lemma nclose_subseteq N x : nclose (N .@ x) nclose N.
Lemma nclose_subseteq N x : N.@x (N : coPset).
Proof.
intros p; rewrite nclose_eq /nclose !ndot_eq !elem_coPset_suffixes.
intros [q ->]. destruct (list_encode_suffix N (ndot_def N x)) as [q' ?].
{ by exists [encode x]. }
by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Qed.
Lemma nclose_subseteq' E N x : nclose N E nclose (N .@ x) E.
Lemma nclose_subseteq' E N x : N E N.@x E.
Proof. intros. etrans; eauto using nclose_subseteq. Qed.
Lemma ndot_nclose N x : encode (N .@ x) nclose N.
Lemma ndot_nclose N x : encode (N.@x) N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_infinite N : ¬set_finite (nclose N).
Lemma nclose_infinite N : ¬set_finite ( N : coPset).
Proof. rewrite nclose_eq. apply coPset_suffixes_infinite. Qed.
Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y.
Lemma ndot_ne_disjoint N x y : x y N.@x N.@y.
Proof.
intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
intros [qx ->] [qy Hqy].
revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
Qed.
Lemma ndot_preserve_disjoint_l N E x : nclose N E nclose (N .@ x) E.
Lemma ndot_preserve_disjoint_l N E x : N E N.@x E.
Proof. intros. pose proof (nclose_subseteq N x). set_solver. Qed.
Lemma ndot_preserve_disjoint_r N E x : E nclose N E nclose (N .@ x).
Lemma ndot_preserve_disjoint_r N E x : E N E N.@x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma ndisj_subseteq_difference N E F :
E nclose N E F E F nclose N.
Lemma ndisj_subseteq_difference N E F : E N E F E F N.
Proof. set_solver. Qed.
End namespace.
(* The hope is that registering these will suffice to solve most goals
of the form [N1 ⊥ N2] and those of the form [N1 ⊆ E ∖ N2 ∖ .. ∖ Nn]. *)
of the form [N1 ⊥ N2] and those of the form [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]. *)
Hint Resolve ndisj_subseteq_difference : ndisj.
Hint Extern 0 (_ _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj.
......
......@@ -117,10 +117,10 @@ Section sts.
Proof. by apply sts_accS. Qed.
Lemma sts_openS E N γ S T :
nclose N E
sts_ctx γ N φ sts_ownS γ S T ={E,EN}= s,
N E
sts_ctx γ N φ sts_ownS γ S T ={E,EN}= s,
s S φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
......@@ -135,9 +135,9 @@ Section sts.
Qed.
Lemma sts_open E N γ s0 T :
nclose N E
sts_ctx γ N φ sts_own γ s0 T ={E,EN}= s,
N E
sts_ctx γ N φ sts_own γ s0 T ={E,EN}= s,
sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof. by apply sts_openS. Qed.
End sts.
......@@ -16,7 +16,7 @@ Section defs.
own tid (CoPset E, ).
Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, i nclose N
( i, i N
inv tlN (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I.
End defs.
......@@ -57,8 +57,8 @@ Section proofs.
iMod (own_empty (prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
{ apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i nclose N)).
intros Ef. exists (coPpick (nclose N coPset.of_gset Ef)).
apply (gset_disj_alloc_empty_updateP_strong' (λ i, i N)).
intros Ef. exists (coPpick ( N coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
......@@ -70,14 +70,14 @@ Section proofs.
Qed.
Lemma tl_inv_open tid tlE E N P :
nclose tlN tlE nclose N E
tl_inv tid N P tl_own tid E ={tlE}= P tl_own tid (E N)
( P tl_own tid (E N) ={tlE}= tl_own tid E).
tlN tlE N E
tl_inv tid N P tl_own tid E ={tlE}= P tl_own tid (E∖↑N)
( P tl_own tid (E∖↑N) ={tlE}= tl_own tid E).
Proof.
rewrite /tl_inv. iIntros (??) "#Htlinv Htoks".
iDestruct "Htlinv" as (i) "[% Hinv]".
rewrite {1 4}(union_difference_L (nclose N) E) //.
rewrite {1 5}(union_difference_L {[i]} (nclose N)) ?tl_own_union; [|set_solver..].
rewrite {1 4}(union_difference_L (N) E) //.
rewrite {1 5}(union_difference_L {[i]} (N)) ?tl_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
iInv tlN as "[[$ >Hdis]|>Htoki2]" "Hclose".
- iMod ("Hclose" with "[Htoki]") as "_"; first auto.
......
......@@ -69,13 +69,13 @@ Proof.
Qed.
Lemma vs_inv N E P Q R :
nclose N E inv N R ( R P ={E nclose N}=> R Q) P ={E}=> Q.
N E inv N R ( R P ={E∖↑N}=> R Q) P ={E}=> Q.
Proof.
iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
by iApply "Hclose".
Qed.
Lemma vs_alloc N P : P ={N}=> inv N P.
Lemma vs_alloc N P : P ={N}=> inv N P.
Proof. iIntros "!# HP". by iApply inv_alloc. Qed.
End vs.
......@@ -121,7 +121,7 @@ Section heap.
(** Weakest precondition *)
Lemma wp_alloc E e v :
to_val e = Some v nclose heapN E
to_val e = Some v heapN E
{{{ heap_ctx }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof.
iIntros (<-%of_to_val ? Φ) "#Hinv HΦ". rewrite /heap_ctx.
......@@ -135,7 +135,7 @@ Section heap.
Qed.
Lemma wp_load E l q v :
nclose heapN E
heapN E
{{{ heap_ctx l {q} v }}} Load (Lit (LitLoc l)) @ E
{{{ RET v; l {q} v }}}.
Proof.
......@@ -148,7 +148,7 @@ Section heap.
Qed.
Lemma wp_store E l v' e v :
to_val e = Some v nclose heapN E
to_val e = Some v heapN E
{{{ heap_ctx l v' }}} Store (Lit (LitLoc l)) e @ E
{{{ RET LitV LitUnit; l v }}}.
Proof.
......@@ -164,7 +164,7 @@ Section heap.
Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 nclose heapN E
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 heapN E
{{{ heap_ctx l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool false); l {q} v' }}}.
Proof.
......@@ -177,7 +177,7 @@ Section heap.
Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 nclose heapN E
to_val e1 = Some v1 to_val e2 = Some v2 heapN E
{{{ heap_ctx l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool true); l v2 }}}.
Proof.
......
......@@ -162,7 +162,7 @@ Proof.
Qed.
Lemma recv_split E l P1 P2 :
nclose N E recv l (P1 P2) ={E}= recv l P1 recv l P2.
N E recv l (P1 P2) ={E}= recv l P1 recv l P2.
Proof.
rename P1 into R1; rename P2 into R2. rewrite {1}/recv /barrier_ctx.
iIntros (?). iDestruct 1 as (γ P Q i) "(#(%&Hh&Hsts)&Hγ&#HQ&HQR)".
......
......@@ -14,7 +14,7 @@ Lemma barrier_spec (N : namespace) :
{{ v, l : loc, v = #l recv l P send l P }})
( l P, {{ send l P P }} signal #l {{ _, True }})
( l P, {{ recv l P }} wait #l {{ _, P }})
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, recv l (P Q) ={N}=> recv l P recv l Q)
( l P Q, (P - Q) recv l P - recv l Q).
Proof.
intros HN.
......
......@@ -14,7 +14,7 @@ Implicit Types Δ : envs (iResUR Σ).
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
to_val e = Some v
(Δ heap_ctx) nclose heapN E
(Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
......@@ -29,7 +29,7 @@ Proof.
Qed.
Lemma tac_wp_load Δ Δ' E i l q v Φ :
(Δ heap_ctx) nclose heapN E
(Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
(Δ' Φ v)
......@@ -43,7 +43,7 @@ Qed.
Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
to_val e = Some v'
(Δ heap_ctx) nclose heapN E
(Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
......@@ -58,7 +58,7 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx) nclose heapN E
(Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' Φ (LitV (LitBool false)))
......@@ -72,7 +72,7 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx) nclose heapN E
(Δ heap_ctx) heapN E
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
......
......@@ -726,6 +726,8 @@ End disjoint_list.
Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B.
Class UpClose A B := up_close : A B.
Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
(** * Monadic operations *)
(** We define operational type classes for the monadic operations bind, join
......
......@@ -12,7 +12,7 @@ Section LiftingTests.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E :
nclose heapN E heap_ctx WP heap_e @ E {{ v, v = #2 }}.
heapN E heap_ctx WP heap_e @ E {{ v, v = #2 }}.
Proof.
iIntros (HN) "#?". rewrite /heap_e.
wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
......@@ -23,7 +23,7 @@ Section LiftingTests.
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E :
nclose heapN E heap_ctx WP heap_e2 @ E {{ v, v = #2 }}.
heapN E heap_ctx WP heap_e2 @ E {{ v, v = #2 }}.
Proof.
iIntros (HN) "#?". rewrite /heap_e2.
wp_alloc l. wp_let. wp_alloc l'. wp_let.
......
......@@ -90,7 +90,7 @@ Section iris.
Implicit Types P Q : iProp Σ.
Lemma demo_8 N E P Q R :
nclose N E
N E
(True - P - inv N Q - True - R) P - Q ={E}= R.
Proof.
iIntros (?) "H HP HQ".
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment