Commit 53c9d30c authored by Ralf Jung's avatar Ralf Jung
Browse files

never genrealize without a !

parent 976a0602
Pipeline #15059 passed with stage
in 18 minutes and 36 seconds
......@@ -17,8 +17,8 @@ Definition lrustΣ : gFunctors :=
Instance subG_heapPreG {Σ} : subG lrustΣ Σ lrustPreG Σ.
Proof. solve_inG. Qed.
Definition lrust_adequacy Σ `{lrustPreG Σ} e σ φ :
( `{lrustG Σ}, True WP e {{ v, ⌜φ v }})
Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
( `{!lrustG Σ}, True WP e {{ v, ⌜φ v }})
adequate NotStuck e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
......
......@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
qs.2 i, is_Some (σ !! (blk, i)) is_Some (qs.2 !! i).
Section definitions.
Context `{heapG Σ}.
Context `{!heapG Σ}.
Definition heap_mapsto_st (st : lock_state)
(l : loc) (q : Qp) (v: val) : iProp Σ :=
......@@ -106,7 +106,7 @@ Section to_heap.
End to_heap.
Section heap.
Context `{heapG Σ}.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types σ : state.
Implicit Types E : coPset.
......
......@@ -91,7 +91,7 @@ Proof. rewrite /Closed. apply _. Qed.
Inductive val :=
| LitV (l : base_lit)
| RecV (f : binder) (xl : list binder) (e : expr) `{Closed (f :b: xl +b+ []) e}.
| RecV (f : binder) (xl : list binder) (e : expr) `{!Closed (f :b: xl +b+ []) e}.
Bind Scope val_scope with val.
......
......@@ -19,7 +19,7 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
(at level 80, n, i at next level,
format "e1 <-{ n ,Σ i } ! e2") : expr_scope.
Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Lemma wp_memcpy `{!lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n Z.of_nat (length vl2) = n
{{{ l1 ↦∗ vl1 l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
......
......@@ -13,7 +13,7 @@ Definition delete : val :=
else Free "n" "loc".
Section specs.
Context `{lrustG Σ}.
Context `{!lrustG Σ}.
Lemma wp_new E n:
0 n
......
......@@ -10,7 +10,7 @@ Definition swap : val :=
"p2" <- "x";;
"swap" ["p1" + #1 ; "p2" + #1 ; "len" - #1].
Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
Lemma wp_swap `{!lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
Z.of_nat (length vl1) = n Z.of_nat (length vl2) = n
{{{ l1 ↦∗ vl1 l2 ↦∗ vl2 }}}
swap [ #l1; #l2; #n] @ E
......
......@@ -11,7 +11,7 @@ Class lrustG Σ := LRustG {
lrustG_gen_heapG :> heapG Σ
}.
Instance lrustG_irisG `{lrustG Σ} : irisG lrust_lang Σ := {
Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
iris_invG := lrustG_invG;
state_interp σ κs _ := heap_ctx σ;
fork_post _ := True%I;
......@@ -61,7 +61,7 @@ Instance do_subst_vec xl (vsl : vec val (length xl)) e :
Proof. by rewrite /DoSubstL subst_v_eq. Qed.
Section lifting.
Context `{lrustG Σ}.
Context `{!lrustG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types e : expr.
Implicit Types ef : option expr.
......
......@@ -6,14 +6,14 @@ From iris.program_logic Require Import lifting.
Set Default Proof Using "Type".
Import uPred.
Lemma tac_wp_value `{lrustG Σ} Δ E Φ e v :
Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
IntoVal e v
envs_entails Δ (Φ v) envs_entails Δ (WP e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
Lemma tac_wp_pure `{lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
MaybeIntoLaterNEnvs n Δ Δ'
......@@ -38,7 +38,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| _ => fail "wp_pure: not a 'wp'"
end.
Lemma tac_wp_eq_loc `{lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i1 Δ' = Some (false, l1 {q1} v1)%I
envs_lookup i2 Δ' = Some (false, l2 {q2} v2)%I
......@@ -67,7 +67,7 @@ Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
Tactic Notation "wp_if" := wp_pure (If _ _ _).
Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
Lemma tac_wp_bind `{lrustG Σ} K Δ E Φ e :
Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I
envs_entails Δ (WP fill K e @ E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
......@@ -89,7 +89,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
end.
Section heap.
Context `{lrustG Σ}.
Context `{!lrustG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
......
......@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
(** Atomic persistent bors *)
(* TODO : update the TEX with the fact that we can choose the namespace. *)
Definition at_bor `{invG Σ, lftG Σ} κ N (P : iProp Σ) :=
Definition at_bor `{!invG Σ, !lftG Σ} κ N (P : iProp Σ) :=
( i, &{κ,i}P
(N ## lftN inv N (idx_bor_own 1 i)
N = lftN inv N ( q, idx_bor_own q i)))%I.
Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
Section atomic_bors.
Context `{invG Σ, lftG Σ} (P : iProp Σ) (N : namespace).
Context `{!invG Σ, !lftG Σ} (P : iProp Σ) (N : namespace).
Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
Proof. solve_proper. Qed.
......@@ -97,7 +97,7 @@ Section atomic_bors.
Qed.
End atomic_bors.
Lemma at_bor_acc_lftN `{invG Σ, lftG Σ} (P : iProp Σ) E κ :
Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ} (P : iProp Σ) E κ :
lftN E
lft_ctx - &at{κ,lftN}P ={E,E∖↑lftN}= P (P ={E∖↑lftN,E}= True)
[†κ] |={E∖↑lftN,E}=> True.
......
......@@ -7,13 +7,13 @@ Set Default Proof Using "Type".
Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
Definition frac_bor `{invG Σ, lftG Σ, frac_borG Σ} κ (φ : Qp iProp Σ) :=
Definition frac_bor `{!invG Σ, !lftG Σ, !frac_borG Σ} κ (φ : Qp iProp Σ) :=
( γ κ', κ κ' &at{κ',lftN} ( q, φ q own γ q
(q = 1%Qp q', (q + q' = 1)%Qp q'.[κ'])))%I.
Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
Section frac_bor.
Context `{invG Σ, lftG Σ, frac_borG Σ} (φ : Qp iProp Σ).
Context `{!invG Σ, !lftG Σ, !frac_borG Σ} (φ : Qp iProp Σ).
Implicit Types E : coPset.
Global Instance frac_bor_contractive κ n :
......@@ -112,7 +112,7 @@ Section frac_bor.
iApply "Hclose". iFrame. rewrite Hqκ'. by iFrame.
Qed.
Lemma frac_bor_acc E q κ `{Fractional _ φ} :
Lemma frac_bor_acc E q κ `{!Fractional φ} :
lftN E
lft_ctx - &frac{κ}φ - q.[κ] ={E}= q', φ q' ( φ q' ={E}= q.[κ]).
Proof.
......@@ -134,7 +134,7 @@ Section frac_bor.
Qed.
End frac_bor.
Lemma frac_bor_lft_incl `{invG Σ, lftG Σ, frac_borG Σ} κ κ' q:
Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ, !frac_borG Σ} κ κ' q:
lft_ctx - &frac{κ}(λ q', (q * q').[κ']) - κ κ'.
Proof.
iIntros "#LFT#Hbor". iApply lft_incl_intro. iAlways. iSplitR.
......
......@@ -23,7 +23,7 @@ Instance lft_inhabited : Inhabited lft := populate static.
Canonical lftC := leibnizC lft.
Section derived.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma bor_acc_atomic_cons E κ P :
......
......@@ -23,17 +23,17 @@ Module Type lifetime_sig.
Parameter static : lft.
Parameter lft_intersect : lft lft lft.
Parameter lft_ctx : `{invG, lftG Σ}, iProp Σ.
Parameter lft_ctx : `{!invG Σ, !lftG Σ}, iProp Σ.
Parameter lft_tok : `{lftG Σ} (q : Qp) (κ : lft), iProp Σ.
Parameter lft_dead : `{lftG Σ} (κ : lft), iProp Σ.
Parameter lft_tok : `{!lftG Σ} (q : Qp) (κ : lft), iProp Σ.
Parameter lft_dead : `{!lftG Σ} (κ : lft), iProp Σ.
Parameter lft_incl : `{invG, lftG Σ} (κ κ' : lft), iProp Σ.
Parameter bor : `{invG, lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
Parameter lft_incl : `{!invG Σ, !lftG Σ} (κ κ' : lft), iProp Σ.
Parameter bor : `{!invG Σ, !lftG Σ} (κ : lft) (P : iProp Σ), iProp Σ.
Parameter bor_idx : Type.
Parameter idx_bor_own : `{lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
Parameter idx_bor : `{invG, lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
Parameter idx_bor_own : `{!lftG Σ} (q : frac) (i : bor_idx), iProp Σ.
Parameter idx_bor : `{!invG Σ, !lftG Σ} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
(** Notation *)
Notation "q .[ κ ]" := (lft_tok q κ)
......@@ -47,7 +47,7 @@ Module Type lifetime_sig.
Infix "⊓" := lft_intersect (at level 40) : stdpp_scope.
Section properties.
Context `{invG, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
(** Instances *)
Global Declare Instance lft_inhabited : Inhabited lft.
......@@ -155,6 +155,6 @@ Module Type lifetime_sig.
Parameter lftΣ : gFunctors.
Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ lftPreG Σ.
Parameter lft_init : `{invG Σ, !lftPreG Σ} E, lftN E
Parameter lft_init : `{!invG Σ, !lftPreG Σ} E, lftN E
(|={E}=> _ : lftG Σ, lft_ctx)%I.
End lifetime_sig.
......@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
Set Default Proof Using "Type".
Section accessors.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
(* Helper internal lemmas *)
......
......@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma raw_bor_create E κ P :
......
......@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section borrow.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma bor_sep E κ P Q :
......
......@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section creation.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :
......
......@@ -79,7 +79,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
Definition to_borUR : gmap slice_name bor_state borUR := fmap ((1%Qp,) to_agree).
Section defs.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
([ mset] Λ κ, own alft_name ( {[ Λ := Cinl q ]}))%I.
......@@ -224,7 +224,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
idx_bor_own idx_bor raw_bor bor.
Section basic_properties.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
(* Unfolding lemmas *)
......
......@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section faking.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma ilft_create A I κ :
......
......@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Import uPred.
Section primitive.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :
......
......@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section reborrow.
Context `{invG Σ, lftG Σ}.
Context `{!invG Σ, !lftG Σ}.
Implicit Types κ : lft.
(* Notice that taking lft_inv for both κ and κ' already implies
......
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