From e724ddf8b576241458d1272988c2f2e5f5ddf12a Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 5 Nov 2016 21:59:26 +0100 Subject: [PATCH] Fix compilation with Iris 37cf94e2. --- F_mu/logrel.v | 4 +- F_mu_ref/logrel.v | 6 +-- F_mu_ref/rules.v | 10 ++--- F_mu_ref_conc/examples/counter.v | 18 ++++---- F_mu_ref_conc/examples/lock.v | 22 ++++----- F_mu_ref_conc/examples/stack/CG_stack.v | 40 ++++++++--------- F_mu_ref_conc/examples/stack/refinement.v | 8 ++-- F_mu_ref_conc/examples/stack/stack_rules.v | 42 ++++++++--------- F_mu_ref_conc/fundamental_binary.v | 6 +-- F_mu_ref_conc/logrel_binary.v | 8 ++-- F_mu_ref_conc/logrel_unary.v | 6 +-- F_mu_ref_conc/rules.v | 18 ++++---- F_mu_ref_conc/rules_binary.v | 52 +++++++++++----------- README.md | 4 +- prelude/base.v | 2 +- stlc/fundamental.v | 2 +- 16 files changed, 124 insertions(+), 124 deletions(-) diff --git a/F_mu/logrel.v b/F_mu/logrel.v index 7456402..4906023 100644 --- a/F_mu/logrel.v +++ b/F_mu/logrel.v @@ -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|]. diff --git a/F_mu_ref/logrel.v b/F_mu_ref/logrel.v index 405d6eb..92ee696 100644 --- a/F_mu_ref/logrel.v +++ b/F_mu_ref/logrel.v @@ -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|]. diff --git a/F_mu_ref/rules.v b/F_mu_ref/rules.v index 9db248d..b55980f 100644 --- a/F_mu_ref/rules.v +++ b/F_mu_ref/rules.v @@ -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Φ". diff --git a/F_mu_ref_conc/examples/counter.v b/F_mu_ref_conc/examples/counter.v index 1118e9d..09af940 100644 --- a/F_mu_ref_conc/examples/counter.v +++ b/F_mu_ref_conc/examples/counter.v @@ -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. diff --git a/F_mu_ref_conc/examples/lock.v b/F_mu_ref_conc/examples/lock.v index dc4d98b..ccb11bb 100644 --- a/F_mu_ref_conc/examples/lock.v +++ b/F_mu_ref_conc/examples/lock.v @@ -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. diff --git a/F_mu_ref_conc/examples/stack/CG_stack.v b/F_mu_ref_conc/examples/stack/CG_stack.v index 9cacc7f..8a96166 100644 --- a/F_mu_ref_conc/examples/stack/CG_stack.v +++ b/F_mu_ref_conc/examples/stack/CG_stack.v @@ -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. diff --git a/F_mu_ref_conc/examples/stack/refinement.v b/F_mu_ref_conc/examples/stack/refinement.v index 37650a5..de2c0fb 100644 --- a/F_mu_ref_conc/examples/stack/refinement.v +++ b/F_mu_ref_conc/examples/stack/refinement.v @@ -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. diff --git a/F_mu_ref_conc/examples/stack/stack_rules.v b/F_mu_ref_conc/examples/stack/stack_rules.v index ad0eabf..816801b 100644 --- a/F_mu_ref_conc/examples/stack/stack_rules.v +++ b/F_mu_ref_conc/examples/stack/stack_rules.v @@ -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. diff --git a/F_mu_ref_conc/fundamental_binary.v b/F_mu_ref_conc/fundamental_binary.v index 12e8b35..67a0e8a 100644 --- a/F_mu_ref_conc/fundamental_binary.v +++ b/F_mu_ref_conc/fundamental_binary.v @@ -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. diff --git a/F_mu_ref_conc/logrel_binary.v b/F_mu_ref_conc/logrel_binary.v index e1657c8..53a39bd 100644 --- a/F_mu_ref_conc/logrel_binary.v +++ b/F_mu_ref_conc/logrel_binary.v @@ -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|]. diff --git a/F_mu_ref_conc/logrel_unary.v b/F_mu_ref_conc/logrel_unary.v index 630b77e..e99ea75 100644 --- a/F_mu_ref_conc/logrel_unary.v +++ b/F_mu_ref_conc/logrel_unary.v @@ -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|]. diff --git a/F_mu_ref_conc/rules.v b/F_mu_ref_conc/rules.v index 4c48222..eb25dbf 100644 --- a/F_mu_ref_conc/rules.v +++ b/F_mu_ref_conc/rules.v @@ -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. diff --git a/F_mu_ref_conc/rules_binary.v b/F_mu_ref_conc/rules_binary.v index 7e2cc4c..130d37d 100644 --- a/F_mu_ref_conc/rules_binary.v +++ b/F_mu_ref_conc/rules_binary.v @@ -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 E ρ j K l q v' e1 v1 e2 v2: to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → v' ≠ v1 → - spec_ctx ρ ★ j ⤇ fill K (CAS (Loc l) e1 e2) ★ l ↦ₛ{q} v' - ={E}=★ j ⤇ fill K (#♭ false) ★ l ↦ₛ{q} v'. + spec_ctx ρ ∗ j ⤇ fill K (CAS (Loc l) e1 e2) ∗ l ↦ₛ{q} v' + ={E}=∗ j ⤇ fill K (#♭ false) ∗ l ↦ₛ{q} v'. Proof. iIntros (????) "(#Hinv & Hj & Hl)". rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. @@ -238,8 +238,8 @@ Section cfg. Lemma step_cas_suc E ρ j K l e1 v1 v1' e2 v2: to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → v1 = v1' → - spec_ctx ρ ★ j ⤇ fill K (CAS (Loc l) e1 e2) ★ l ↦ₛ v1' - ={E}=★ j ⤇ fill K (#♭ true) ★ l ↦ₛ v2. + spec_ctx ρ ∗ j ⤇ fill K (CAS (Loc l) e1 e2) ∗ l ↦ₛ v1' + ={E}=∗ j ⤇ fill K (#♭ true) ∗ l ↦ₛ v2. Proof. iIntros (????) "(#Hinv & Hj & Hl)"; subst. rewrite /spec_ctx /tpool_mapsto /heapS_mapsto. @@ -263,61 +263,61 @@ Section cfg. Lemma step_rec E ρ j K e1 e2 v : to_val e2 = Some v → nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (App (Rec e1) e2) - ={E}=★ j ⤇ fill K (e1.[Rec e1,e2/]). + spec_ctx ρ ∗ j ⤇ fill K (App (Rec e1) e2) + ={E}=∗ j ⤇ fill K (e1.[Rec e1,e2/]). Proof. intros ?; apply step_pure => σ; econstructor; eauto. Qed. Lemma step_tlam E ρ j K e : nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (TApp (TLam e)) ={E}=★ j ⤇ fill K e. + spec_ctx ρ ∗ j ⤇ fill K (TApp (TLam e)) ={E}=∗ j ⤇ fill K e. Proof. apply step_pure => σ; econstructor; eauto. Qed. Lemma step_Fold E ρ j K e v : to_val e = Some v → nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (Unfold (Fold e)) ={E}=★ j ⤇ fill K e. + spec_ctx ρ ∗ j ⤇ fill K (Unfold (Fold e)) ={E}=∗ j ⤇ fill K e. Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. Lemma step_fst E ρ j K e1 v1 e2 v2 : to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (Fst (Pair e1 e2)) ={E}=★ j ⤇ fill K e1. + spec_ctx ρ ∗ j ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ j ⤇ fill K e1. Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed. Lemma step_snd E ρ j K e1 v1 e2 v2 : to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (Snd (Pair e1 e2)) ={E}=★ j ⤇ fill K e2. + spec_ctx ρ ∗ j ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ j ⤇ fill K e2. Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed. Lemma step_case_inl E ρ j K e0 v0 e1 e2 : to_val e0 = Some v0 → nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (Case (InjL e0) e1 e2) - ={E}=★ j ⤇ fill K (e1.[e0/]). + spec_ctx ρ ∗ j ⤇ fill K (Case (InjL e0) e1 e2) + ={E}=∗ j ⤇ fill K (e1.[e0/]). Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. Lemma step_case_inr E ρ j K e0 v0 e1 e2 : to_val e0 = Some v0 → nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (Case (InjR e0) e1 e2) - ={E}=★ j ⤇ fill K (e2.[e0/]). + spec_ctx ρ ∗ j ⤇ fill K (Case (InjR e0) e1 e2) + ={E}=∗ j ⤇ fill K (e2.[e0/]). Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed. Lemma step_if_false E ρ j K e1 e2 : nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (If (#♭ false) e1 e2) ={E}=★ j ⤇ fill K e2. + spec_ctx ρ ∗ j ⤇ fill K (If (#♭ false) e1 e2) ={E}=∗ j ⤇ fill K e2. Proof. apply step_pure => σ; econstructor. Qed. Lemma step_if_true E ρ j K e1 e2 : nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (If (#♭ true) e1 e2) ={E}=★ j ⤇ fill K e1. + spec_ctx ρ ∗ j ⤇ fill K (If (#♭ true) e1 e2) ={E}=∗ j ⤇ fill K e1. Proof. apply step_pure => σ; econstructor. Qed. Lemma step_nat_binop E ρ j K op a b : nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (BinOp op (#n a) (#n b)) - ={E}=★ j ⤇ fill K (of_val (binop_eval op a b)). + spec_ctx ρ ∗ j ⤇ fill K (BinOp op (#n a) (#n b)) + ={E}=∗ j ⤇ fill K (of_val (binop_eval op a b)). Proof. apply step_pure => σ; econstructor. Qed. Lemma step_fork E ρ j K e : nclose specN ⊆ E → - spec_ctx ρ ★ j ⤇ fill K (Fork e) ={E}=★ ∃ j', j ⤇ fill K Unit ★ j' ⤇ e. + spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K Unit ∗ j' ⤇ e. Proof. iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto. iInv specN as (tp σ) ">[Hown %]" "Hclose". diff --git a/README.md b/README.md index 5b86894..316f3f0 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ This version is known to compile with: - - Coq 8.5pl1 + - Coq 8.5pl2 - Ssreflect 1.6 - Autosubst 1.5 - - Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/6cb76aaa + - Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/37cf94e2 diff --git a/prelude/base.v b/prelude/base.v index 34b16f9..d6203b9 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -30,7 +30,7 @@ Ltac properness := | |- (WP _ {{ _ }})%I ≡ (WP _ {{ _ }})%I => apply wp_proper =>? | |- (▷ _)%I ≡ (▷ _)%I => apply later_proper | |- (□ _)%I ≡ (□ _)%I => apply always_proper - | |- (_ ★ _)%I ≡ (_ ★ _)%I => apply sep_proper + | |- (_ ∗ _)%I ≡ (_ ∗ _)%I => apply sep_proper | |- (inv _ _)%I ≡ (inv _ _)%I => apply (contractive_proper _) end. diff --git a/stlc/fundamental.v b/stlc/fundamental.v index eb0ced7..50d19d4 100644 --- a/stlc/fundamental.v +++ b/stlc/fundamental.v @@ -16,7 +16,7 @@ Section typed_interp. Theorem fundamental Γ vs e τ : Γ ⊢ₜ e : τ → length Γ = length vs → - [★] zip_with interp Γ vs ⊢ ⟦ τ ⟧ₑ e.[env_subst vs]. + [∗] zip_with interp Γ vs ⊢ ⟦ τ ⟧ₑ e.[env_subst vs]. Proof. intros Htyped; revert vs. induction Htyped; iIntros (vs Hlen) "#Hctx /=". -- GitLab