Skip to content

R
ReLoC-v1
Commit e724ddf8 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Fix compilation with Iris 37cf94e2.

parent 7ab22ba1
Hide whitespace changes
Inline Side-by-side
Showing with 124 additions and 124 deletions
F_mu/logrel.v
View file @ e724ddf8
......@@ -72,7 +72,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(length Γ = length vs ★ [★] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
(length Γ = length vs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
......@@ -154,7 +154,7 @@ Section logrel.
Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ [].
Proof. iIntros ""; iSplit; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ★ ⟦ Γ ⟧* Δ vs.
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
Proof.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
......
F_mu_ref/logrel.v
View file @ e724ddf8
......@@ -61,7 +61,7 @@ Section logrel.
Qed.
Program Definition interp_ref_inv (l : loc) : D -n> iProp Σ := λne τi,
(∃ v, l ↦ v ★ τi v)%I.
(∃ v, l ↦ v ∗ τi v)%I.
Solve Obligations with solve_proper.
Program Definition interp_ref
......@@ -84,7 +84,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(length Γ = length vs ★ [★] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
(length Γ = length vs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
......@@ -168,7 +168,7 @@ Section logrel.
Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ [].
Proof. iIntros ""; iSplit; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ★ ⟦ Γ ⟧* Δ vs.
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
Proof.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
......
F_mu_ref/rules.v
View file @ e724ddf8
......@@ -87,13 +87,13 @@ Section lang_rules.
Proof. by rewrite /to_heap -fmap_insert. Qed.
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
Proof.
by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
l ↦{q1} v1 ★ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
......@@ -103,7 +103,7 @@ Section lang_rules.
rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
Qed.
Lemma heap_mapsto_op_split l q v : (l ↦{q} v)%I ≡ (l ↦{q/2} v ★ l ↦{q/2} v)%I.
Lemma heap_mapsto_op_split l q v : (l ↦{q} v)%I ≡ (l ↦{q/2} v ∗ l ↦{q/2} v)%I.
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
......@@ -151,7 +151,7 @@ Section lang_rules.
Lemma wp_load E l q v :
nclose heapN ⊆ E →
{{{ heap_ctx ★ ▷ l ↦{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦{q} v }}}.
{{{ heap_ctx ∗ ▷ l ↦{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦{q} v }}}.
Proof.
iIntros (? Φ) "[#Hinv >Hl] HΦ".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
......@@ -163,7 +163,7 @@ Section lang_rules.
Lemma wp_store E l v' e v :
to_val e = Some v → nclose heapN ⊆ E →
{{{ heap_ctx ★ ▷ l ↦ v' }}} Store (Loc l) e @ E
{{{ heap_ctx ∗ ▷ l ↦ v' }}} Store (Loc l) e @ E
{{{ RET UnitV; l ↦ v }}}.
Proof.
iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
......
F_mu_ref_conc/examples/counter.v
View file @ e724ddf8
......@@ -60,8 +60,8 @@ Section CG_Counter.
Lemma steps_CG_increment E ρ j K x n:
nclose specN ⊆ E →
spec_ctx ρ ★ x ↦ₛ (#nv n) ★ j ⤇ fill K (App (CG_increment (Loc x)) Unit)
⊢ |={E}=> j ⤇ fill K (Unit) ★ x ↦ₛ (#nv (S n)).
spec_ctx ρ ∗ x ↦ₛ (#nv n) ∗ j ⤇ fill K (App (CG_increment (Loc x)) Unit)
⊢ |={E}=> j ⤇ fill K (Unit) ∗ x ↦ₛ (#nv (S n)).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_increment.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......@@ -120,9 +120,9 @@ Section CG_Counter.
Lemma steps_CG_locked_increment E ρ j K x n l :
nclose specN ⊆ E →
spec_ctx ρ ★ x ↦ₛ (#nv n) ★ l ↦ₛ (#♭v false)
★ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K Unit ★ x ↦ₛ (#nv S n) ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ x ↦ₛ (#nv n) ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K Unit ∗ x ↦ₛ (#nv S n) ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]".
iMod (steps_with_lock
......@@ -160,9 +160,9 @@ Section CG_Counter.
Lemma steps_counter_read E ρ j K x n :
nclose specN ⊆ E →
spec_ctx ρ ★ x ↦ₛ (#nv n)
★ j ⤇ fill K (App (counter_read (Loc x)) Unit)
⊢ |={E}=> j ⤇ fill K (#n n) ★ x ↦ₛ (#nv n).
spec_ctx ρ ∗ x ↦ₛ (#nv n)
∗ j ⤇ fill K (App (counter_read (Loc x)) Unit)
⊢ |={E}=> j ⤇ fill K (#n n) ∗ x ↦ₛ (#nv n).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold counter_read.
iMod (step_rec _ _ j K _ Unit with "[Hj]") as "Hj"; eauto.
......@@ -282,7 +282,7 @@ Section CG_Counter.
iApply wp_wand_l; iSplitR; [iIntros (v) "Hv"; iExact "Hv"|].
iApply (wp_alloc with "[]"); trivial; iFrame "#"; iNext; iIntros (cnt) "Hcnt /=".
(* establishing the invariant *)
iAssert ((∃ n, l ↦ₛ (#♭v false) ★ cnt ↦ᵢ (#nv n) ★ cnt' ↦ₛ (#nv n) )%I)
iAssert ((∃ n, l ↦ₛ (#♭v false) ∗ cnt ↦ᵢ (#nv n) ∗ cnt' ↦ₛ (#nv n) )%I)
with "[Hl Hcnt Hcnt']" as "Hinv".
{ iExists _. by iFrame. }
iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
......
F_mu_ref_conc/examples/lock.v
View file @ e724ddf8
......@@ -79,8 +79,8 @@ Section proof.
Lemma steps_newlock E ρ j K :
nclose specN ⊆ E →
spec_ctx ρ ★ j ⤇ fill K newlock
⊢ |={E}=> ∃ l, j ⤇ fill K (Loc l) ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ j ⤇ fill K newlock
⊢ |={E}=> ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec Hj]".
by iMod (step_alloc _ _ j K with "[Hj]") as "Hj"; eauto.
......@@ -90,8 +90,8 @@ Section proof.
Lemma steps_acquire E ρ j K l :
nclose specN ⊆ E →
spec_ctx ρ ★ l ↦ₛ (#♭v false) ★ j ⤇ fill K (App acquire (Loc l))
⊢ |={E}=> j ⤇ fill K Unit ★ l ↦ₛ (#♭v true).
spec_ctx ρ ∗ l ↦ₛ (#♭v false) ∗ j ⤇ fill K (App acquire (Loc l))
⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#♭v true).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold acquire.
iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto. done.
......@@ -109,8 +109,8 @@ Section proof.
Lemma steps_release E ρ j K l b:
nclose specN ⊆ E →
spec_ctx ρ ★ l ↦ₛ (#♭v b) ★ j ⤇ fill K (App release (Loc l))
⊢ |={E}=> j ⤇ fill K Unit ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ l ↦ₛ (#♭v b) ∗ j ⤇ fill K (App release (Loc l))
⊢ |={E}=> j ⤇ fill K Unit ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec [Hl Hj]]". unfold release.
iMod (step_rec _ _ j K with "[Hj]") as "Hj"; eauto; try done.
......@@ -125,11 +125,11 @@ Section proof.
Lemma steps_with_lock E ρ j K e l P Q v w:
nclose specN ⊆ E →
(∀ f, e.[f] = e) (* e is a closed term *) →
(∀ K', spec_ctx ρ ★ P ★ j ⤇ fill K' (App e (of_val w))
⊢ |={E}=> j ⤇ fill K' (of_val v) ★ Q) →
spec_ctx ρ ★ P ★ l ↦ₛ (#♭v false)
★ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w))
⊢ |={E}=> j ⤇ fill K (of_val v) ★ Q ★ l ↦ₛ (#♭v false).
(∀ K', spec_ctx ρ ∗ P ∗ j ⤇ fill K' (App e (of_val w))
⊢ |={E}=> j ⤇ fill K' (of_val v) ∗ Q) →
spec_ctx ρ ∗ P ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (with_lock e (Loc l)) (of_val w))
⊢ |={E}=> j ⤇ fill K (of_val v) ∗ Q ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE H1 H2) "[#Hspec [HP [Hl Hj]]]".
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......
F_mu_ref_conc/examples/stack/CG_stack.v
View file @ e724ddf8
......@@ -79,8 +79,8 @@ Section CG_Stack.
Lemma steps_CG_push E ρ j K st v w :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ v ★ j ⤇ fill K (App (CG_push (Loc st)) (of_val w))
⊢ |={E}=> j ⤇ fill K Unit ★ st ↦ₛ FoldV (InjRV (PairV w v)).
spec_ctx ρ ∗ st ↦ₛ v ∗ j ⤇ fill K (App (CG_push (Loc st)) (of_val w))
⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)).
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......@@ -134,9 +134,9 @@ Section CG_Stack.
Lemma steps_CG_locked_push E ρ j K st w v l :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ v ★ l ↦ₛ (#♭v false)
★ j ⤇ fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w))
⊢ |={E}=> j ⤇ fill K Unit ★ st ↦ₛ FoldV (InjRV (PairV w v)) ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w))
⊢ |={E}=> j ⤇ fill K Unit ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false).
Proof.
intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
iMod (steps_with_lock
......@@ -175,9 +175,9 @@ Section CG_Stack.
Lemma steps_CG_pop_suc E ρ j K st v w :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ FoldV (InjRV (PairV w v)) ★
spec_ctx ρ ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗
j ⤇ fill K (App (CG_pop (Loc st)) Unit)
⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ★ st ↦ₛ v.
⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v.
Proof.
intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......@@ -218,9 +218,9 @@ Section CG_Stack.
Lemma steps_CG_pop_fail E ρ j K st :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ FoldV (InjLV UnitV) ★
spec_ctx ρ ∗ st ↦ₛ FoldV (InjLV UnitV) ∗
j ⤇ fill K (App (CG_pop (Loc st)) Unit)
⊢ |={E}=> j ⤇ fill K (InjL Unit) ★ st ↦ₛ FoldV (InjLV UnitV).
⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV).
Proof.
iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
......@@ -278,9 +278,9 @@ Section CG_Stack.
Lemma steps_CG_locked_pop_suc E ρ j K st v w l :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ FoldV (InjRV (PairV w v)) ★ l ↦ₛ (#♭v false)
★ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ★ st ↦ₛ v ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ st ↦ₛ FoldV (InjRV (PairV w v)) ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K (InjR (of_val w)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iMod (steps_with_lock _ _ j K _ _ _ _ (InjRV w) UnitV _ _
......@@ -293,9 +293,9 @@ Section CG_Stack.
Lemma steps_CG_locked_pop_fail E ρ j K st l :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ FoldV (InjLV UnitV) ★ l ↦ₛ (#♭v false)
★ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K (InjL Unit) ★ st ↦ₛ FoldV (InjLV UnitV) ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ fill K (InjL Unit) ∗ st ↦ₛ FoldV (InjLV UnitV) ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
iMod (steps_with_lock _ _ j K _ _ _ _ (InjLV UnitV) UnitV _ _
......@@ -341,9 +341,9 @@ Section CG_Stack.
Lemma steps_CG_snap E ρ j K st v l :
nclose specN ⊆ E →
spec_ctx ρ ★ st ↦ₛ v ★ l ↦ₛ (#♭v false)
★ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ (fill K (of_val v)) ★ st ↦ₛ v ★ l ↦ₛ (#♭v false).
spec_ctx ρ ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false)
∗ j ⤇ fill K (App (CG_snap (Loc st) (Loc l)) Unit)
⊢ |={E}=> j ⤇ (fill K (of_val v)) ∗ st ↦ₛ v ∗ l ↦ₛ (#♭v false).
Proof.
iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
iMod (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _
......@@ -407,7 +407,7 @@ Section CG_Stack.
Lemma steps_CG_iter E ρ j K f v w :
nclose specN ⊆ E →
spec_ctx ρ
★ j ⤇ fill K (App (CG_iter (of_val f))
∗ j ⤇ fill K (App (CG_iter (of_val f))
(Fold (InjR (Pair (of_val w) (of_val v)))))
⊢ |={E}=>
j ⤇ fill K
......@@ -441,7 +441,7 @@ Section CG_Stack.
Lemma steps_CG_iter_end E ρ j K f :
nclose specN ⊆ E →
spec_ctx ρ ★ j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
spec_ctx ρ ∗ j ⤇ fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
⊢ |={E}=> j ⤇ fill K Unit.
Proof.
iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
......
F_mu_ref_conc/examples/stack/refinement.v
View file @ e724ddf8
......@@ -73,10 +73,10 @@ Section Stack_refinement.
iFrame "Hls". iLeft. iSplit; trivial.
}
iAssert ((∃ istk v h, (stack_owns h)
★ stk' ↦ₛ v
★ stk ↦ᵢ (FoldV (LocV istk))
★ StackLink τi (LocV istk, v)
★ l ↦ₛ (#♭v false)
∗ stk' ↦ₛ v
∗ stk ↦ᵢ (FoldV (LocV istk))
∗ StackLink τi (LocV istk, v)
∗ l ↦ₛ (#♭v false)
)%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
{ iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". }
iMod (inv_alloc stackN with "[Hinv]") as "#Hinv"; trivial.
......
F_mu_ref_conc/examples/stack/stack_rules.v
View file @ e724ddf8
......@@ -28,13 +28,13 @@ Section Rules.
Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : uPred_scope.
Lemma stack_mapsto_dup l v : l ↦ˢᵗᵏ v ⊢ l ↦ˢᵗᵏ v ★ l ↦ˢᵗᵏ v.
Lemma stack_mapsto_dup l v : l ↦ˢᵗᵏ v ⊢ l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ v.
Proof.
by rewrite /stack_mapsto /auth_own -own_op -auth_frag_op -stackR_self_op.
Qed.
Lemma stack_mapstos_agree l v w:
l ↦ˢᵗᵏ v ★ l ↦ˢᵗᵏ w ⊢ l ↦ˢᵗᵏ v ★ l ↦ˢᵗᵏ w ∧ v = w.
l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ⊢ l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ∧ v = w.
Proof.
iIntros "H".
rewrite -own_op.
......@@ -46,10 +46,10 @@ Section Rules.
Qed.
Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
(∃ l w, v.1 = LocV l ★ l ↦ˢᵗᵏ w ★
(∃ l w, v.1 = LocV l ∗ l ↦ˢᵗᵏ w ∗
((w = InjLV UnitV ∧ v.2 = FoldV (InjLV UnitV)) ∨
(∃ y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) ★
v.2 = FoldV (InjRV (PairV y2 z2)) ★ Q (y1, y2) ★ ▷ P(z1, z2))))%I.
(∃ y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) ∗
v.2 = FoldV (InjRV (PairV y2 z2)) ∗ Q (y1, y2) ∗ ▷ P(z1, z2))))%I.
Solve Obligations with solve_proper.
Global Instance StackLink_pre_contractive Q : Contractive (StackLink_pre Q).
......@@ -65,17 +65,17 @@ Section Rules.
Lemma StackLink_unfold Q v :
StackLink Q v ≡ (∃ l w,
v.1 = LocV l ★ l ↦ˢᵗᵏ w ★
v.1 = LocV l ∗ l ↦ˢᵗᵏ w ∗
((w = InjLV UnitV ∧ v.2 = FoldV (InjLV UnitV)) ∨
(∃ y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
★ v.2 = FoldV (InjRV (PairV y2 z2))
★ Q (y1, y2) ★ ▷ @StackLink Q (z1, z2))))%I.
∗ v.2 = FoldV (InjRV (PairV y2 z2))
∗ Q (y1, y2) ∗ ▷ @StackLink Q (z1, z2))))%I.
Proof. by rewrite {1}/StackLink fixpoint_unfold. Qed.
Global Opaque StackLink. (* So that we can only use the unfold above. *)
Lemma StackLink_dup (Q : D) v `{∀ vw, PersistentP (Q vw)} :
StackLink Q v ⊢ StackLink Q v ★ StackLink Q v.
StackLink Q v ⊢ StackLink Q v ∗ StackLink Q v.
Proof.
iIntros "H". iLöb as "Hlat" forall (v). rewrite StackLink_unfold.
iDestruct "H" as (l w) "[% [Hl Hr]]"; subst.
......@@ -174,14 +174,14 @@ Section Rules.
Definition stack_owns (h : stackUR) :=
(own stack_name (● h)
★ [★ map] l ↦ v ∈ h, match v with
∗ [∗ map] l ↦ v ∈ h, match v with
| DecAgree v' => l ↦ᵢ v'
| _ => True
end)%I.
Lemma stack_owns_alloc E h l v :
stack_owns h ★ l ↦ᵢ v
⊢ |={E}=> stack_owns (<[l := DecAgree v]> h) ★ l ↦ˢᵗᵏ v.
stack_owns h ∗ l ↦ᵢ v
⊢ |={E}=> stack_owns (<[l := DecAgree v]> h) ∗ l ↦ˢᵗᵏ v.
Proof.
iIntros "[[Hown Hall] Hl]".
iDestruct (own_valid _ with "Hown") as "#Hvalid".
......@@ -209,13 +209,13 @@ Section Rules.
Qed.
Lemma stack_owns_open h l v :
stack_owns h ★ l ↦ˢᵗᵏ v
stack_owns h ∗ l ↦ˢᵗᵏ v
⊢ own stack_name (● h)
★ ([★ map] l ↦ v ∈ delete l h,
∗ ([∗ map] l ↦ v ∈ delete l h,
match v with
| DecAgree v' => l ↦ᵢ v'
| DecAgreeBot => True
end) ★ l ↦ᵢ v ★ l ↦ˢᵗᵏ v.
end) ∗ l ↦ᵢ v ∗ l ↦ˢᵗᵏ v.
Proof.
iIntros "[[Hown Hall] Hl]".
unfold stack_mapsto, auth_own.
......@@ -231,12 +231,12 @@ Section Rules.
Lemma stack_owns_close h l v :
own stack_name (● h)
★ ([★ map] l ↦ v ∈ delete l h,
∗ ([∗ map] l ↦ v ∈ delete l h,
match v with
| DecAgree v' => l ↦ᵢ v'
| DecAgreeBot => True
end)
★ l ↦ᵢ v ★ l ↦ˢᵗᵏ v ⊢ stack_owns h ★ l ↦ˢᵗᵏ v.
∗ l ↦ᵢ v ∗ l ↦ˢᵗᵏ v ⊢ stack_owns h ∗ l ↦ˢᵗᵏ v.
Proof.
iIntros "[Hown [Hall [Hl Hl']]]".
unfold stack_mapsto, auth_own.
......@@ -256,8 +256,8 @@ Section Rules.
Qed.
Lemma stack_owns_open_close h l v :
stack_owns h ★ l ↦ˢᵗᵏ v
⊢ l ↦ᵢ v ★ (l ↦ᵢ v -★ (stack_owns h ★ l ↦ˢᵗᵏ v)).
stack_owns h ∗ l ↦ˢᵗᵏ v
⊢ l ↦ᵢ v ∗ (l ↦ᵢ v -∗ (stack_owns h ∗ l ↦ˢᵗᵏ v)).
Proof.
iIntros "[Howns Hls]".
iDestruct (stack_owns_open with "[Howns Hls]") as "[Hh [Hm [Hl Hls]]]".
......@@ -267,7 +267,7 @@ Section Rules.
Qed.
Lemma stack_owns_later_open_close h l v :
▷ stack_owns h ★ l ↦ˢᵗᵏ v
⊢ ▷ (l ↦ᵢ v ★ (l ↦ᵢ v -★ (stack_owns h ★ l ↦ˢᵗᵏ v))).
▷ stack_owns h ∗ l ↦ˢᵗᵏ v
⊢ ▷ (l ↦ᵢ v ∗ (l ↦ᵢ v -∗ (stack_owns h ∗ l ↦ˢᵗᵏ v))).
Proof. iIntros "H". by iNext; iApply stack_owns_open_close. Qed.
End Rules.
F_mu_ref_conc/fundamental_binary.v
View file @ e724ddf8
......@@ -37,9 +37,9 @@ Section fundamental.
(* Put all quantifiers at the outer level *)
Lemma bin_log_related_alt {Γ e e' τ} : Γ ⊨ e ≤log≤ e' : τ → ∀ Δ vvs ρ j K,
env_PersistentP Δ →
heapI_ctx ★ spec_ctx ρ ★ ⟦ Γ ⟧* Δ vvs ★ j ⤇ fill K (e'.[env_subst (vvs.*2)])
heapI_ctx ∗ spec_ctx ρ ∗ ⟦ Γ ⟧* Δ vvs ∗ j ⤇ fill K (e'.[env_subst (vvs.*2)])
⊢ WP e.[env_subst (vvs.*1)] {{ v, ∃ v',
j ⤇ fill K (of_val v') ★ interp τ Δ (v, v') }}.
j ⤇ fill K (of_val v') ∗ interp τ Δ (v, v') }}.
Proof.
iIntros (Hlog Δ vvs ρ j K ?) "(#Hh & #Hs & HΓ & Hj)".
iApply (Hlog with "[HΓ] *"); iFrame; eauto.
......@@ -303,7 +303,7 @@ Section fundamental.
iApply wp_fupd. iApply (wp_alloc with "[]"); auto.
iIntros "!>"; iIntros (l) "Hl'".
iMod (inv_alloc (logN .@ (l,l')) _ (∃ w : val * val,
l ↦ᵢ w.1 ★ l' ↦ₛ w.2 ★ interp τ Δ w)%I with "[Hl Hl']") as "HN"; eauto.
l ↦ᵢ w.1 ∗ l' ↦ₛ w.2 ∗ interp τ Δ w)%I with "[Hl Hl']") as "HN"; eauto.
{ iNext; iExists (v, v'); by iFrame. }
iModIntro; iExists (LocV l'). iFrame "Hj". iExists (l, l'); eauto.
Qed.
......
F_mu_ref_conc/logrel_binary.v
View file @ e724ddf8
......@@ -33,7 +33,7 @@ Section logrel.
Definition interp_expr (τi : listC D -n> D) (Δ : listC D)
(ee : expr * expr) : iProp Σ := (∀ j K,
j ⤇ fill K (ee.2) →
WP ee.1 {{ v, ∃ v', j ⤇ fill K (of_val v') ★ τi Δ (v, v') }})%I.
WP ee.1 {{ v, ∃ v', j ⤇ fill K (of_val v') ∗ τi Δ (v, v') }})%I.
Global Instance interp_expr_ne n :
Proper (dist n ==> dist n ==> (=) ==> dist n) interp_expr.
Proof. solve_proper. Qed.
......@@ -101,7 +101,7 @@ Section logrel.
Qed.
Program Definition interp_ref_inv (ll : loc * loc) : D -n> iProp Σ := λne τi,
(∃ vv, ll.1 ↦ᵢ vv.1 ★ ll.2 ↦ₛ vv.2 ★ τi vv)%I.
(∃ vv, ll.1 ↦ᵢ vv.1 ∗ ll.2 ↦ₛ vv.2 ∗ τi vv)%I.
Solve Obligations with solve_proper.
Program Definition interp_ref
......@@ -127,7 +127,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vvs : list (val * val)) : iProp Σ :=
(length Γ = length vvs ★ [★] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
(length Γ = length vvs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vvs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Class env_PersistentP Δ :=
......@@ -217,7 +217,7 @@ Section logrel.
Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ [].
Proof. iIntros ""; iSplit; auto. Qed.
Lemma interp_env_cons Δ Γ vvs τ vv :
⟦ τ :: Γ ⟧* Δ (vv :: vvs) ⊣⊢ ⟦ τ ⟧ Δ vv ★ ⟦ Γ ⟧* Δ vvs.
⟦ τ :: Γ ⟧* Δ (vv :: vvs) ⊣⊢ ⟦ τ ⟧ Δ vv ∗ ⟦ Γ ⟧* Δ vvs.
Proof.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
......
F_mu_ref_conc/logrel_unary.v
View file @ e724ddf8
......@@ -63,7 +63,7 @@ Section logrel.
Qed.
Program Definition interp_ref_inv (l : loc) : D -n> iProp Σ := λne τi,
(∃ v, l ↦ᵢ v ★ τi v)%I.
(∃ v, l ↦ᵢ v ∗ τi v)%I.
Solve Obligations with solve_proper.
Program Definition interp_ref
......@@ -88,7 +88,7 @@ Section logrel.
Definition interp_env (Γ : list type)
(Δ : listC D) (vs : list val) : iProp Σ :=
(length Γ = length vs ★ [★] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
(length Γ = length vs ∗ [∗] zip_with (λ τ, ⟦ τ ⟧ Δ) Γ vs)%I.
Notation "⟦ Γ ⟧*" := (interp_env Γ).
Definition interp_expr (τ : type) (Δ : listC D) (e : expr) : iProp Σ :=
......@@ -171,7 +171,7 @@ Section logrel.
Lemma interp_env_nil Δ : True ⊢ ⟦ [] ⟧* Δ [].
Proof. iIntros ""; iSplit; auto. Qed.
Lemma interp_env_cons Δ Γ vs τ v :
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ★ ⟦ Γ ⟧* Δ vs.
⟦ τ :: Γ ⟧* Δ (v :: vs) ⊣⊢ ⟦ τ ⟧ Δ v ∗ ⟦ Γ ⟧* Δ vs.
Proof.
rewrite /interp_env /= (assoc _ (⟦ _ ⟧ _ _)) -(comm _ (_ = _)%I) -assoc.
by apply sep_proper; [apply pure_proper; omega|].
......
F_mu_ref_conc/rules.v
View file @ e724ddf8
......@@ -87,13 +87,13 @@ Section lang_rules.
Proof. by rewrite /to_heap -fmap_insert. Qed.
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v : l ↦ᵢ{q1} v ★ l ↦ᵢ{q2} v ⊣⊢ l ↦ᵢ{q1+q2} v.
Lemma heap_mapsto_op_eq l q1 q2 v : l ↦ᵢ{q1} v ∗ l ↦ᵢ{q2} v ⊣⊢ l ↦ᵢ{q1+q2} v.
Proof.
by rewrite heapI_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
l ↦ᵢ{q1} v1 ★ l ↦ᵢ{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦ᵢ{q1+q2} v1.
l ↦ᵢ{q1} v1 ∗ l ↦ᵢ{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦ᵢ{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
......@@ -103,10 +103,10 @@ Section lang_rules.
rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
Qed.
Lemma heap_mapsto_op_split l q v : (l ↦ᵢ{q} v)%I ≡ (l ↦ᵢ{q/2} v ★ l ↦ᵢ{q/2} v)%I.
Lemma heap_mapsto_op_split l q v : (l ↦ᵢ{q} v)%I ≡ (l ↦ᵢ{q/2} v ∗ l ↦ᵢ{q/2} v)%I.
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
Lemma heap_mapsto_dup_invalid l v1 v2 : l ↦ᵢ v1 ★ l ↦ᵢ v2 ⊢ False.
Lemma heap_mapsto_dup_invalid l v1 v2 : l ↦ᵢ v1 ∗ l ↦ᵢ v2 ⊢ False.
Proof.
rewrite heap_mapsto_op heapI_mapsto_eq /heapI_mapsto_def auth_own_valid.
iIntros "[_ Hv]". iDestruct "Hv" as %Hv.
......@@ -177,7 +177,7 @@ Section lang_rules.
Lemma wp_load E l q v :
nclose heapN ⊆ E →
{{{ heapI_ctx ★ ▷ l ↦ᵢ{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}.
{{{ heapI_ctx ∗ ▷ l ↦ᵢ{q} v }}} Load (Loc l) @ E {{{ RET v; l ↦ᵢ{q} v }}}.
Proof.
iIntros (? Φ) "[#Hinv >Hl] HΦ".
rewrite /heapI_ctx heapI_mapsto_eq /heapI_mapsto_def.
......@@ -189,7 +189,7 @@ Section lang_rules.
Lemma wp_store E l v' e v :
to_val e = Some v → nclose heapN ⊆ E →
{{{ heapI_ctx ★ ▷ l ↦ᵢ v' }}} Store (Loc l) e @ E
{{{ heapI_ctx ∗ ▷ l ↦ᵢ v' }}} Store (Loc l) e @ E
{{{ RET UnitV; l ↦ᵢ v }}}.
Proof.
iIntros (<-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
......@@ -205,7 +205,7 @@ Section lang_rules.
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 →
{{{ heapI_ctx ★ ▷ l ↦ᵢ{q} v' }}} CAS (Loc l) e1 e2 @ E
{{{ heapI_ctx ∗ ▷ l ↦ᵢ{q} v' }}} CAS (Loc l) e1 e2 @ E
{{{ RET (BoolV false); l ↦ᵢ{q} v' }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ?? Φ) "[#Hinv >Hl] HΦ".
......@@ -218,7 +218,7 @@ Section lang_rules.
Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 → to_val e2 = Some v2 → nclose heapN ⊆ E →
{{{ heapI_ctx ★ ▷ l ↦ᵢ v1 }}} CAS (Loc l) e1 e2 @ E
{{{ heapI_ctx ∗ ▷ l ↦ᵢ v1 }}} CAS (Loc l) e1 e2 @ E
{{{ RET (BoolV true); l ↦ᵢ v2 }}}.
Proof.
iIntros (<-%of_to_val <-%of_to_val ? Φ) "[#Hinv >Hl] HΦ".
......@@ -297,7 +297,7 @@ Section lang_rules.
Qed.
Lemma wp_fork E e Φ :
▷ (|={E}=> Φ UnitV) ★ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
▷ (|={E}=> Φ UnitV) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) Unit [e]) //=; eauto.
- by rewrite later_sep -(wp_value_fupd _ _ Unit) // big_sepL_singleton.
......
F_mu_ref_conc/rules_binary.v
View file @ e724ddf8
......@@ -32,7 +32,7 @@ Section definitionsS.
own cfg_name (◯ ({[ j := Excl e ]}, ∅)).
Definition spec_inv (ρ : cfg lang) : iProp Σ :=
(∃ tp σ, own cfg_name (● (to_tpool tp, to_heap σ)) ★ ■ rtc step ρ (tp,σ))%I.
(∃ tp σ, own cfg_name (● (to_tpool tp, to_heap σ)) ∗ ■ rtc step ρ (tp,σ))%I.
Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
inv specN (spec_inv ρ).
......@@ -133,7 +133,7 @@ Section cfg.
Lemma step_pure E ρ j K e e' :
(∀ σ, head_step e σ e' σ []) →
nclose specN ⊆ E →
spec_ctx ρ ★ j ⤇ fill K e ={E}=★ j ⤇ fill K e'.
spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
Proof.
iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
......@@ -149,7 +149,7 @@ Section cfg.
Lemma step_alloc E ρ j K e v:
to_val e = Some v → nclose specN ⊆ E →
spec_ctx ρ ★ j ⤇ fill K (Alloc e) ={E}=★ ∃ l, j ⤇ fill K (Loc l) ★ l ↦ₛ v.
spec_ctx ρ ∗ j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
Proof.
iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
......@@ -171,8 +171,8 @@ Section cfg.
Lemma step_load E ρ j K l q v:
nclose specN ⊆ E →
spec_ctx ρ ★ j ⤇ fill K (Load (Loc l)) ★ l ↦ₛ{q} v
={E}=★ j ⤇ fill K (of_val v) ★ l ↦ₛ{q} v.
spec_ctx ρ ∗ j ⤇ fill K (Load (Loc l)) ∗ l ↦ₛ{q} v
={E}=∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
Proof.
iIntros (?) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
......@@ -192,8 +192,8 @@ Section cfg.
Lemma step_store E ρ j K l v' e v:
to_val e = Some v → nclose specN ⊆ E →
spec_ctx ρ ★ j ⤇ fill K (Store (Loc l) e) ★ l ↦ₛ v'
={E}=★ j ⤇ fill K Unit ★ l ↦ₛ v.
spec_ctx ρ ∗ j ⤇ fill K (Store (Loc l) e) ∗ l ↦ₛ v'
={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
......@@ -217,8 +217,8 @@ Section cfg.
Lemma step_cas_fail