From 282e21ea63f677dc6cc67191650105e09a36171b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 Jan 2017 17:32:10 +0100
Subject: [PATCH] Update the heap construction to use the state interpretation.
---
theories/lang/adequacy.v | 29 +-
theories/lang/derived.v | 6 +-
theories/lang/heap.v | 348 ++++++------------
theories/lang/lifting.v | 256 ++++++++-----
theories/lang/memcpy.v | 7 +-
theories/lang/new_delete.v | 14 +-
theories/lang/proofmode.v | 42 +--
theories/typing/bool.v | 8 +-
theories/typing/borrow.v | 8 +-
theories/typing/cont.v | 8 +-
theories/typing/function.v | 16 +-
theories/typing/int.v | 8 +-
theories/typing/own.v | 6 +-
theories/typing/programs.v | 42 +--
theories/typing/soundness.v | 12 +-
theories/typing/type.v | 2 +-
theories/typing/type_sum.v | 22 +-
theories/typing/unsafe/cell.v | 4 +-
theories/typing/unsafe/refcell/ref_code.v | 10 +-
theories/typing/unsafe/refcell/refcell_code.v | 28 +-
20 files changed, 406 insertions(+), 470 deletions(-)
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 2534ddfd..7a401f61 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -1,31 +1,32 @@
-From iris.program_logic Require Export hoare adequacy.
+From iris.program_logic Require Export adequacy weakestpre.
From iris.algebra Require Import auth.
From lrust.lang Require Export heap.
From lrust.lang Require Import proofmode notation.
Set Default Proof Using "Type".
-Class heapPreG Σ := HeapPreG {
- heap_preG_ownP :> ownPPreG lrust_lang Σ;
- heap_preG_heap :> inG Σ (authR heapUR);
- heap_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
+Class lrustPreG Σ := HeapPreG {
+ lrust_preG_irig :> invPreG Σ;
+ lrust_preG_heap :> inG Σ (authR heapUR);
+ lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
}.
-Definition heapΣ : gFunctors :=
- #[ownPΣ state;
+Definition lrustΣ : gFunctors :=
+ #[invΣ;
GFunctor (constRF (authR heapUR));
GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
+Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
Proof. solve_inG. Qed.
-Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
- (∀ `{heapG Σ}, {{ heap_ctx }} e {{ v, ⌜φ v⌠}}) →
+Definition lrust_adequacy Σ `{lrustPreG Σ} e σ φ :
+ (∀ `{lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌠}}) →
adequate e σ φ.
Proof.
- intros Hwp; eapply (ownP_adequacy Σ _). iIntros (?) "Hσ".
+ intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (own_alloc (◠to_heap σ)) as (vγ) "Hvγ".
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. }
iMod (own_alloc (◠(∅ : heap_freeableUR))) as (fγ) "Hfγ"; first done.
- set (Hheap := HeapG _ _ _ _ vγ fγ).
- iMod (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ, ∅; by iFrame|].
- iApply (Hwp _). by rewrite /heap_ctx.
+ set (Hheap := HeapG _ _ _ vγ fγ).
+ iModIntro. iExists heap_ctx. iSplitL.
+ { iExists ∅. by iFrame. }
+ iApply (Hwp (LRustG _ _ Hheap)).
Qed.
diff --git a/theories/lang/derived.v b/theories/lang/derived.v
index a84188b1..716569b2 100644
--- a/theories/lang/derived.v
+++ b/theories/lang/derived.v
@@ -18,7 +18,7 @@ Notation Newlft := (Lit LitUnit) (only parsing).
Notation Endlft := Skip (only parsing).
Section derived.
-Context `{ownPG lrust_lang Σ}.
+Context `{lrustG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
@@ -119,9 +119,9 @@ Proof.
destruct (bool_decide_reflect (n1 = n2)); [rewrite Hl //|rewrite Hg //];
clear Hl Hg; iApply wp_bin_op_pure; subst.
- intros. apply BinOpEqTrue. constructor.
- - iNext; iIntros (?? Heval). inversion_clear Heval. done. by inversion H.
+ - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
- intros. apply BinOpEqFalse. by constructor.
- - iNext; iIntros (?? Heval). inversion_clear Heval. by inversion H. done.
+ - iNext; iIntros (?? Heval). by inversion_clear Heval; inv_lit.
Qed.
(* TODO : wp_eq for locations, if needed. *)
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index c48e4b1c..b5c53cd3 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -1,14 +1,14 @@
From Coq Require Import Min.
+From iris.prelude Require Import coPset.
From iris.algebra Require Import cmra_big_op gmap frac agree.
From iris.algebra Require Import csum excl auth.
-From iris.base_logic Require Import big_op lib.invariants lib.fractional.
+From iris.base_logic Require Import big_op lib.fractional.
+From iris.base_logic Require Export lib.own.
From iris.proofmode Require Export tactics.
-From lrust.lang Require Export lifting.
+From lrust.lang Require Export lang.
Set Default Proof Using "Type".
Import uPred.
-Definition heapN : namespace := nroot .@ "heap".
-
Definition lock_stateR : cmraT :=
csumR (exclR unitC) natR.
@@ -19,7 +19,6 @@ Definition heap_freeableUR : ucmraT :=
gmapUR block (prodR fracR (gmapR Z (exclR unitC))).
Class heapG Σ := HeapG {
- heapG_ownP_inG :> ownPG lrust_lang Σ;
heap_inG :> inG Σ (authR heapUR);
heap_freeable_inG :> inG Σ (authR heap_freeableUR);
heap_name : gname;
@@ -32,7 +31,7 @@ Definition to_heap : state → heapUR :=
fmap (λ v, (1%Qp, to_lock_stateR (v.1), to_agree (v.2))).
Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
∀ blk qs, hF !! blk = Some qs →
- qs.2 ≠∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
+ qs.2 ≠∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
Section definitions.
Context `{heapG Σ}.
@@ -61,17 +60,13 @@ Section definitions.
Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
seal_eq heap_freeable_aux.
- Definition heap_inv : iProp Σ :=
- (∃ (σ:state) hF, ownP σ ∗ own heap_name (◠to_heap σ)
- ∗ own heap_freeable_name (◠hF)
- ∗ ⌜heap_freeable_rel σ hFâŒ)%I.
- Definition heap_ctx : iProp Σ := inv heapN heap_inv.
-
- Global Instance heap_ctx_persistent : PersistentP heap_ctx.
- Proof. apply _. Qed.
+ Definition heap_ctx (σ:state) : iProp Σ :=
+ (∃ hF, own heap_name (◠to_heap σ)
+ ∗ own heap_freeable_name (◠hF)
+ ∗ ⌜heap_freeable_rel σ hFâŒ)%I.
End definitions.
-Typeclasses Opaque heap_ctx heap_mapsto heap_freeable heap_mapsto_vec.
+Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
Instance: Params (@heap_mapsto) 4.
Instance: Params (@heap_freeable) 5.
@@ -92,13 +87,9 @@ Notation "†{ q } l … n" := (heap_freeable l q n)
(at level 20, q at level 50, format "†{ q } l … n") : uPred_scope.
Notation "†l … n" := (heap_freeable l 1 n) (at level 20) : uPred_scope.
-Section heap.
- Context {Σ : gFunctors}.
- Implicit Types P Q : iProp Σ.
+Section to_heap.
Implicit Types σ : state.
- Implicit Types E : coPset.
- (** Allocation *)
Lemma to_heap_valid σ : ✓ to_heap σ.
Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
@@ -112,8 +103,13 @@ Section heap.
Lemma to_heap_delete σ l : to_heap (delete l σ) = delete l (to_heap σ).
Proof. by rewrite /to_heap fmap_delete. Qed.
+End to_heap.
+Section heap.
Context `{heapG Σ}.
+ Implicit Types P Q : iProp Σ.
+ Implicit Types σ : state.
+ Implicit Types E : coPset.
(** General properties of mapsto and freeable *)
Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
@@ -179,8 +175,7 @@ Section heap.
- revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
{ rewrite !heap_mapsto_vec_nil. iIntros "_"; auto. }
rewrite !heap_mapsto_vec_cons. iIntros "[[Hv1 Hvl1] [Hv2 Hvl2]]".
- iDestruct (IH (shift_loc l 1) with "[Hvl1 Hvl2]") as "[% $]";
- subst; first by iFrame.
+ iDestruct (IH (shift_loc l 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
rewrite (inj_iff (:: vl2)).
iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
iSplit; first done. iFrame.
@@ -206,7 +201,7 @@ Section heap.
l ↦∗{q}: Φ1 -∗ (∀ vl, Φ1 vl -∗ Φ2 vl) -∗ l ↦∗{q}: Φ2.
Proof.
iIntros "Hm Hwand". iDestruct "Hm" as (vl) "[Hm HΦ]". iExists vl.
- iFrame "Hm". iApply "Hwand". done.
+ iFrame "Hm". by iApply "Hwand".
Qed.
Lemma heap_mapsto_vec_combine l q vl :
@@ -338,7 +333,7 @@ Section heap.
Qed.
(** Weakest precondition *)
- Lemma heap_alloc_vs σ l vl:
+ Lemma heap_alloc_vs σ l vl :
(∀ m : Z, σ !! shift_loc l m = None) →
own heap_name (◠to_heap σ)
==∗ own heap_name (◠to_heap (init_mem l vl σ))
@@ -358,31 +353,29 @@ Section heap.
rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
Qed.
- Lemma wp_alloc E n:
- ↑heapN ⊆ E → 0 < n →
- {{{ heap_ctx }}} Alloc (Lit $ LitInt n) @ E
- {{{ l vl, RET LitV $ LitLoc l; ⌜n = length vl⌠∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
+ Lemma heap_alloc σ l n vl :
+ 0 < n →
+ (∀ m, σ !! shift_loc l m = None) →
+ Z.of_nat (length vl) = n →
+ heap_ctx σ ==∗
+ heap_ctx (init_mem l vl σ) ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl.
Proof.
- iIntros (???) "#Hinv HΦ". rewrite /heap_ctx /heap_inv.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iApply (wp_alloc_pst with "[$Hσ]")=> //.
- iNext. iIntros (l σ') "(% & #Hσσ' & Hσ')".
- iDestruct "Hσσ'" as %(vl & HvlLen & Hvl).
+ intros ?? HvlLen; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
assert (vl ≠[]) by (intros ->; simpl in *; lia).
- iMod (heap_alloc_vs with "[$Hvalσ]") as "[Hvalσ' Hmapsto]"; first done.
+ iMod (heap_alloc_vs _ _ vl with "[$Hvalσ]") as "[Hvalσ Hmapsto]"; first done.
iMod (own_update _ (â— hF) with "HhF") as "[HhF Hfreeable]".
{ apply auth_update_alloc,
(alloc_singleton_local_update _ (l.1) (1%Qp, inter (l.2) (Z.to_nat n))).
- eauto using heap_freeable_rel_None.
- split. done. apply inter_valid. }
- iMod ("Hclose" with "[Hσ' Hvalσ' HhF]") as "_".
- - iNext. iExists σ', _. subst σ'. iFrame. iPureIntro.
- rewrite HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem.
- - rewrite heap_freeable_eq /heap_freeable_def. iApply "HΦ".
- iSplitR; first auto. iFrame. by rewrite heap_mapsto_vec_combine.
+ iModIntro. iSplitL "Hvalσ HhF".
+ { iExists _. iFrame. iPureIntro.
+ rewrite -HvlLen Nat2Z.id. auto using heap_freeable_rel_init_mem. }
+ rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
+ iFrame.
Qed.
- Lemma heap_free_vs l vl σ :
+ Lemma heap_free_vs σ l vl :
own heap_name (◠to_heap σ) ∗ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
{[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]})
==∗ own heap_name (◠to_heap (free_mem l (length vl) σ)).
@@ -403,15 +396,14 @@ Section heap.
setoid_rewrite <-shift_loc_assoc. apply IH.
Qed.
- Lemma wp_free E (n:Z) l vl :
- ↑heapN ⊆ E → n = length vl →
- {{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
- Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
- {{{ RET LitV LitUnit; True }}}.
+ Lemma heap_free σ l vl (n : Z) :
+ n = length vl →
+ heap_ctx σ -∗ l ↦∗ vl -∗ †l…(length vl)
+ ==∗ ⌜0 < n⌠∗ ⌜∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)⌠∗
+ heap_ctx (free_mem l (Z.to_nat n) σ).
Proof.
- iIntros (???Φ) "(#Hinv & >Hmt & >Hf) HΦ". rewrite /heap_ctx /heap_inv.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose". iDestruct "REL" as %REL.
- rewrite heap_freeable_eq /heap_freeable_def.
+ iDestruct 1 as (hF) "(Hvalσ & HhF & REL)"; iDestruct "REL" as %REL.
+ iIntros "Hmt Hf". rewrite heap_freeable_eq /heap_freeable_def.
iDestruct (own_valid_2 with "HhF Hf") as % [Hl Hv]%auth_valid_discrete_2.
move: Hl=> /singleton_included [[q qs] [/leibniz_equiv_iff Hl Hq]].
apply (Some_included_exclusive _ _) in Hq as [=<-<-]%leibniz_equiv; last first.
@@ -419,18 +411,16 @@ Section heap.
assert (vl ≠[]).
{ intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
assert (0 < n) by (subst n; by destruct vl).
- iApply (wp_free_pst _ σ with "[$Hσ]"). by auto.
- { intros i. subst n. eauto using heap_freeable_is_Some. }
- iNext. iIntros "Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
+ iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
{ rewrite heap_mapsto_vec_combine //. iFrame. }
iMod (own_update_2 with "HhF Hf") as "HhF".
{ apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
- iMod ("Hclose" with "[-HΦ]") as "_"; last by iApply "HΦ".
- iNext. iExists _, _. subst. rewrite Nat2Z.id. iFrame.
+ iModIntro; subst. repeat iSplit; eauto using heap_freeable_is_Some.
+ iExists _. subst. rewrite Nat2Z.id. iFrame.
eauto using heap_freeable_rel_free_mem.
Qed.
- Lemma heap_mapsto_lookup l ls q v σ:
+ Lemma heap_mapsto_lookup σ l ls q v :
own heap_name (◠to_heap σ) -∗
own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
⌜∃ n' : nat,
@@ -448,7 +438,7 @@ Section heap.
by exists O. eauto. exists O. by rewrite Nat.add_0_r.
Qed.
- Lemma heap_mapsto_lookup_1 l ls v σ:
+ Lemma heap_mapsto_lookup_1 σ l ls v :
own heap_name (◠to_heap σ) -∗
own heap_name (◯ {[ l := (1%Qp, to_lock_stateR ls, to_agree v) ]}) -∗
⌜σ !! l = Some (ls, v)âŒ.
@@ -463,210 +453,94 @@ Section heap.
destruct ls, ls''; rewrite ?Nat.add_0_r; naive_solver.
Qed.
- Lemma wp_read_sc E l q v :
- ↑heapN ⊆ E →
- {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
- {{{ RET v; l ↦{q} v }}}.
- Proof.
- iIntros (??) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
- iApply (wp_read_sc_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
- iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
- iNext. iExists σ, hF. iFrame. eauto.
- Qed.
-
Lemma heap_read_vs σ n1 n2 nf l q v:
σ !! l = Some (RSt (n1 + nf), v) →
- own heap_name (◠to_heap σ) ∗ heap_mapsto_st (RSt n1) l q v
+ own heap_name (◠to_heap σ) -∗ heap_mapsto_st (RSt n1) l q v
==∗ own heap_name (◠to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
∗ heap_mapsto_st (RSt n2) l q v.
Proof.
- intros Hσv. rewrite -!own_op to_heap_insert.
+ intros Hσv. apply uPred.wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update.
{ by rewrite /to_heap lookup_fmap Hσv. }
apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
apply nat_local_update; lia.
Qed.
- Lemma wp_read_na E l q v :
- ↑heapN ⊆ E →
- {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
- {{{ RET v; l ↦{q} v }}}.
- Proof.
- iIntros (??Φ) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iApply (wp_read_na1_pst E).
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
- iMod (heap_read_vs _ 0 1 with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
- iModIntro. iExists σ, n, v. iFrame. iSplit; [done|]. iIntros "!> Hσ".
- iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
- { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
- iModIntro. clear dependent n σ hF.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
- iApply (wp_read_na2_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
- iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
+ Lemma heap_read σ l q v :
+ heap_ctx σ -∗ l ↦{q} v -∗ ∃ n, ⌜σ !! l = Some (RSt n, v)âŒ.
+ Proof.
+ iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
+ rewrite heap_mapsto_eq.
+ iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ Qed.
+
+ Lemma heap_read_1 σ l v :
+ heap_ctx σ -∗ l ↦ v -∗ ⌜σ !! l = Some (RSt 0, v)âŒ.
+ Proof.
+ iDestruct 1 as (hF) "(Hσ & HhF & REL)". iIntros "Hmt".
+ rewrite heap_mapsto_eq.
+ iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
+ Qed.
+
+ Lemma heap_read_na σ l q v :
+ heap_ctx σ -∗ l ↦{q} v ==∗ ∃ n,
+ ⌜σ !! l = Some (RSt n, v)⌠∗
+ heap_ctx (<[l:=(RSt (S n), v)]> σ) ∗
+ ∀ σ2, heap_ctx σ2 ==∗ ∃ n2, ⌜σ2 !! l = Some (RSt (S n2), v)⌠∗
+ heap_ctx (<[l:=(RSt n2, v)]> σ2) ∗ l ↦{q} v.
+ Proof.
+ iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
+ rewrite heap_mapsto_eq.
+ iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ iMod (heap_read_vs _ 0 1 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+ iModIntro. iExists n; iSplit; [done|]. iSplitL "HhF Hσ".
+ { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
+ clear dependent n σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
+ iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ iMod (heap_read_vs _ 1 0 with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+ iExists n; iModIntro; iSplit; [done|]. iFrame "Hmt".
+ iExists hF. iFrame. eauto using heap_freeable_rel_stable.
Qed.
Lemma heap_write_vs σ st1 st2 l v v':
σ !! l = Some (st1, v) →
- own heap_name (◠to_heap σ) ∗ heap_mapsto_st st1 l 1%Qp v
+ own heap_name (◠to_heap σ) -∗ heap_mapsto_st st1 l 1%Qp v
==∗ own heap_name (◠to_heap (<[l:=(st2, v')]> σ))
∗ heap_mapsto_st st2 l 1%Qp v'.
Proof.
- intros Hσv. rewrite -!own_op to_heap_insert.
+ intros Hσv. apply uPred.wand_intro_r. rewrite -!own_op to_heap_insert.
eapply own_update, auth_update, singleton_local_update.
{ by rewrite /to_heap lookup_fmap Hσv. }
apply exclusive_local_update. by destruct st2.
Qed.
- Lemma wp_write_sc E l e v v' :
- ↑heapN ⊆ E → to_val e = Some v →
- {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
- {{{ RET LitV LitUnit; l ↦ v }}}.
- Proof.
- iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
- iApply (wp_write_sc_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
- iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
- Qed.
-
- Lemma wp_write_na E l e v v' :
- ↑heapN ⊆ E → to_val e = Some v →
- {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
- {{{ RET LitV LitUnit; l ↦ v }}}.
- Proof.
- iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iApply (wp_write_na1_pst E).
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
- iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod (fupd_intro_mask' (E∖↑heapN) ∅) as "Hclose'"; first set_solver.
- iModIntro. iExists σ, v'. iSplit; [done|]. iIntros "{$Hσ} !> Hσ".
- iMod "Hclose'" as "_". iMod ("Hclose" with "[Hσ Hvalσ HhF]") as "_".
- { iNext. iExists _, _. iFrame. eauto using heap_freeable_rel_stable. }
- iModIntro. clear dependent σ hF.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
- iApply (wp_write_na2_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
- iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
- Qed.
-
- Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
- ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 → z1 ≠zl →
- {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitInt zl) }}}
- CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
- {{{ RET LitV $ LitInt 0; l ↦{q} (LitV $ LitInt zl) }}}.
- Proof.
- iIntros (? <-%of_to_val ??) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "Hvalσ Hv") as %[n Hσl].
- iApply (wp_cas_pst with "[$Hσ]"); eauto.
- { right. by constructor. }
- { inversion 1. done. }
- iNext. iIntros ([|]).
- { iIntros "[Heq _]". iDestruct "Heq" as %Heq. inversion Heq. done. }
- iIntros "[_ Hσ]". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
- Qed.
-
- Lemma wp_cas_int_suc E l z1 e2 lit2 :
- ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 →
- {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
- CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
- {{{ RET LitV $ LitInt 1; l ↦ LitV lit2 }}}.
- Proof.
- iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
- iApply (wp_cas_pst with "[$Hσ]"); eauto.
- { left. by constructor. }
- iNext. iIntros ([|]); last first.
- { iIntros "[Hneq _]". iDestruct "Hneq" as %Hneq. inversion Hneq. done. }
- iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
- Qed.
-
- Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
- ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 → l1 ≠l' →
- {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
- CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
- {{{ RET LitV $ LitInt 0;
- l ↦{q} (LitV $ LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
- Proof.
- iIntros (? <-%of_to_val ??) "(#Hinv & >Hl & >Hl' & >Hl1) HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup with "Hvalσ Hl") as %[n Hσl].
- iDestruct (heap_mapsto_lookup with "Hvalσ Hl'") as %[n' Hσl'].
- iDestruct (heap_mapsto_lookup with "Hvalσ Hl1") as %[n1 Hσl1].
- iApply (wp_cas_pst with "[$Hσ]"); eauto.
- { right. by constructor. }
- { inversion 1; subst; (by destruct (σ !! l1)) || by destruct (σ !! l'). }
- iNext. iIntros ([|]).
- { iIntros "[Heq _]". iDestruct "Heq" as %Heq. inversion Heq; subst.
- done. by destruct (σ !! l1). by destruct (σ !! l'). }
- iIntros "[_ Hσ]". iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
- iNext. iExists _, hF. by iFrame.
- Qed.
-
- Lemma wp_cas_loc_suc E l l1 e2 lit2 :
- ↑heapN ⊆ E → to_val e2 = Some $ LitV lit2 →
- {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc l1) }}}
- CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
- {{{ RET LitV $ LitInt 1; l ↦ LitV lit2 }}}.
- Proof.
- iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
- iApply (wp_cas_pst with "[$Hσ]"); eauto.
- { left. by constructor. }
- iNext. iIntros ([|]); last first.
- { iIntros "[Hneq _]". iDestruct "Hneq" as %Hneq. inversion Hneq. done. }
- iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
- Qed.
-
- Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
- ↑heapN ⊆ E → to_val e2 = Some $ LitV $ LitLoc l2 →
- {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc ll) }}}
- CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
- {{{ b, RET LitV $ lit_of_bool b;
- if b is true then l ↦ LitV (LitLoc l2)
- else ⌜l1 ≠ll⌠∗ l ↦ LitV (LitLoc ll) }}}.
- Proof.
- iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
- rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
- iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
- iDestruct (heap_mapsto_lookup_1 with "Hvalσ Hv") as %?.
- iApply (wp_cas_pst with "[$Hσ]"); eauto.
- { destruct (decide (l1 = ll)) as [->|Hne].
- - left. by constructor.
- - right. by constructor. }
- iNext. iIntros ([|]).
- - iIntros "[_ Hσ]". iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
- iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
- - iIntros "[Hneq Hσ]". iDestruct "Hneq" as %Hneq. inversion_clear Hneq.
- iMod ("Hclose" with "[-Hv HΦ]"); last by iApply ("HΦ" $! false); iFrame.
- iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
+ Lemma heap_write σ l v v' :
+ heap_ctx σ -∗ l ↦ v ==∗ heap_ctx (<[l:=(RSt 0, v')]> σ) ∗ l ↦ v'.
+ Proof.
+ iDestruct 1 as (hF) "(Hσ & HhF & %)". iIntros "Hmt".
+ rewrite heap_mapsto_eq.
+ iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; auto.
+ iMod (heap_write_vs with "Hσ Hmt") as "[Hσ $]"; first done.
+ iModIntro. iExists _. iFrame. eauto using heap_freeable_rel_stable.
+ Qed.
+
+ Lemma heap_write_na σ l v v' :
+ heap_ctx σ -∗ l ↦ v ==∗
+ ⌜σ !! l = Some (RSt 0, v)⌠∗
+ heap_ctx (<[l:=(WSt, v)]> σ) ∗
+ ∀ σ2, heap_ctx σ2 ==∗ ⌜σ2 !! l = Some (WSt, v)⌠∗
+ heap_ctx (<[l:=(RSt 0, v')]> σ2) ∗ l ↦ v'.
+ Proof.
+ iDestruct 1 as (hF) "(Hσ & HhF & %)"; iIntros "Hmt".
+ rewrite heap_mapsto_eq.
+ iDestruct (heap_mapsto_lookup_1 with "Hσ Hmt") as %?; eauto.
+ iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+ iModIntro. iSplit; [done|]. iSplitL "HhF Hσ".
+ { iExists hF. iFrame. eauto using heap_freeable_rel_stable. }
+ clear dependent σ hF. iIntros (σ2). iDestruct 1 as (hF) "(Hσ & HhF & %)".
+ iDestruct (heap_mapsto_lookup with "Hσ Hmt") as %[n Hσl]; eauto.
+ iMod (heap_write_vs with "Hσ Hmt") as "[Hσ Hmt]"; first done.
+ iModIntro; iSplit; [done|]. iFrame "Hmt".
+ iExists hF. iFrame. eauto using heap_freeable_rel_stable.
Qed.
End heap.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index b8f0cab8..5df8261f 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -1,16 +1,32 @@
-From iris.program_logic Require Export weakestpre ownp.
+From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting.
-From lrust.lang Require Export lang.
+From lrust.lang Require Export lang heap.
From lrust.lang Require Import tactics.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
Local Hint Extern 0 (head_reducible _ _) => do_head_step eauto 2.
+Hint Constructors lit_neq lit_eq.
-(* TODO : as for heap_lang, directly use a global heap invariant. *)
+Class lrustG Σ := LRustG {
+ lrustG_invG : invG Σ;
+ lrustG_gen_heapG :> heapG Σ
+}.
+
+Instance lrustG_irisG `{lrustG Σ} : irisG lrust_lang Σ := {
+ iris_invG := lrustG_invG;
+ state_interp := heap_ctx
+}.
+Global Opaque iris_invG.
+
+Ltac inv_lit :=
+ repeat match goal with
+ | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
+ | H : lit_neq _ ?x ?y |- _ => inversion H; clear H; simplify_eq/=
+ end.
Section lifting.
-Context `{ownPG lrust_lang Σ}.
+Context `{lrustG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types ef : option expr.
@@ -24,121 +40,177 @@ Lemma wp_bindi {E e} Ki Φ :
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
-(** Base axioms for core primitives of the language: Stateful reductions. *)
-Lemma wp_alloc_pst E σ n:
+Lemma wp_alloc E n:
0 < n →
- {{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
- {{{ l σ', RET LitV $ LitLoc l;
- ⌜∀ m, σ !! (shift_loc l m) = None⌠∗
- ⌜∃ vl, n = length vl ∧ init_mem l vl σ = σ'⌠∗
- ownP σ' }}}.
+ {{{ True }}} Alloc (Lit $ LitInt n) @ E
+ {{{ l vl, RET LitV $ LitLoc l; ⌜n = length vl⌠∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
Proof.
- iIntros (? Φ) "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
- iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
- rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
+ iIntros (? Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ !>"; iSplit; first by auto.
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+ iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
+ iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
Qed.
-Lemma wp_free_pst E σ l n :
- 0 < n →
- (∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)) →
- {{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
- {{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
+Lemma wp_free E (n:Z) l vl :
+ n = length vl →
+ {{{ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
+ Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
+ {{{ RET LitV LitUnit; True }}}.
Proof.
- iIntros (???) "HP HΦ". iApply (ownP_lift_atomic_head_step _ σ); eauto.
- iFrame "HP". iNext. iIntros (v2 σ2 ef) "% HP". inv_head_step.
- rewrite big_sepL_nil right_id. by iApply "HΦ".
+ iIntros (? Φ) "[>Hmt >Hf] HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ".
+ iMod (heap_free _ _ _ n with "Hσ Hmt Hf") as "(% & % & Hσ)"=>//.
+ iModIntro; iSplit; first by auto.
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+ iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
Qed.
-Lemma wp_read_sc_pst E σ l n v :
- σ !! l = Some (RSt n, v) →
- {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ RET v; ownP σ }}}.
+Lemma wp_read_sc E l q v :
+ {{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
+ {{{ RET v; l ↦{q} v }}}.
Proof.
- iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
- by intros; inv_head_step; eauto using to_of_val.
- rewrite big_sepL_nil right_id; iFrame.
+ iIntros (?) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+ iModIntro; iSplit=> //. iFrame. rewrite to_of_val. iFrame. by iApply "HΦ".
Qed.
-Lemma wp_read_na2_pst E σ l n v :
- σ !! l = Some(RSt $ S n, v) →
- {{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
- {{{ RET v; ownP (<[l:=(RSt n, v)]>σ) }}}.
+Lemma wp_read_na E l q v :
+ {{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
+ {{{ RET v; l ↦{q} v }}}.
Proof.
- iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
- by intros; inv_head_step; eauto using to_of_val.
- rewrite big_sepL_nil right_id; iFrame.
+ iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1) "Hσ".
+ iMod (heap_read_na with "Hσ Hv") as (n) "(% & Hσ & Hσclose)".
+ iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
+ iModIntro. iFrame "Hσ". iSplit; [|by iApply big_sepL_nil].
+ clear dependent σ1 n.
+ iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step. rewrite to_of_val /=.
+ iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
-Lemma wp_read_na1_pst E l Φ :
- (|={E,∅}=> ∃ σ n v, ⌜σ !! l = Some(RSt $ n, v)⌠∧
- ▷ ownP σ ∗
- ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
- WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }})) -∗
- WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
+Lemma wp_write_sc E l e v v' :
+ to_val e = Some v →
+ {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
+ {{{ RET LitV LitUnit; l ↦ v }}}.
Proof.
- iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
- iMod "HΦP" as (σ n v) "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
- iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
- rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
+ iIntros (<-%of_to_val Φ) ">Hv HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+ iMod (heap_write _ _ _ v with "Hσ Hv") as "[Hσ Hv]".
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
+ iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
-Lemma wp_write_sc_pst E σ l v v' :
- σ !! l = Some (RSt 0, v') →
- {{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
- {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
+Lemma wp_write_na E l e v v' :
+ to_val e = Some v →
+ {{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
+ {{{ RET LitV LitUnit; l ↦ v }}}.
Proof.
- iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
- by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
+ iIntros (<-%of_to_val Φ) ">Hv HΦ".
+ iApply wp_lift_head_step; auto. iIntros (σ1) "Hσ".
+ iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
+ iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
+ iModIntro. iFrame "Hσ". iSplit; [|by iApply big_sepL_nil].
+ clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (e2 σ2 efs Hstep) "!>"; inv_head_step.
+ iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
Qed.
-Lemma wp_write_na2_pst E σ l v v' :
- σ !! l = Some(WSt, v') →
- {{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
- {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
+Lemma wp_cas_int_fail E l q z1 e2 lit2 zl :
+ to_val e2 = Some (LitV lit2) → z1 ≠zl →
+ {{{ ▷ l ↦{q} LitV (LitInt zl) }}}
+ CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+ {{{ RET LitV $ LitInt 0; l ↦{q} LitV (LitInt zl) }}}.
Proof.
- iIntros (??) "?HΦ". iApply ownP_lift_atomic_det_head_step; eauto.
- by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
+ iIntros (<-%of_to_val ? Φ) ">Hv HΦ".
+ iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hv") as %[n ?].
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
+ iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
-Lemma wp_write_na1_pst E l v Φ :
- (|={E,∅}=> ∃ σ v', ⌜σ !! l = Some(RSt 0, v')⌠∧
- ▷ ownP σ ∗
- ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
- WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }})) -∗
- WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
+Lemma wp_cas_suc E l lit1 e2 lit2 :
+ to_val e2 = Some (LitV lit2) → lit1 ≠LitUnit →
+ {{{ ▷ l ↦ LitV lit1 }}}
+ CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
+ {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
Proof.
- iIntros "HΦP". iApply (ownP_lift_head_step E); auto.
- iMod "HΦP" as (σ v') "(%&HΦ&HP)". iModIntro. iExists σ. iSplit. done. iFrame.
- iNext. iIntros (e2 σ2 ef) "% HΦ". inv_head_step.
- rewrite big_sepL_nil right_id. iApply ("HP" with "HΦ").
+ iIntros (<-%of_to_val ? Φ) ">Hv HΦ".
+ iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+ iModIntro; iSplit; first (destruct lit1; by eauto).
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; [inv_lit|].
+ iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+ iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
Qed.
-Lemma wp_cas_pst E n σ l e1 lit1 lit2 litl :
- to_val e1 = Some $ LitV lit1 →
- σ !! l = Some (RSt n, LitV litl) →
- (lit_eq σ lit1 litl ∨ lit_neq σ lit1 litl) →
- (lit_eq σ lit1 litl → n = 0%nat) →
- {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (Lit lit2) @ E
- {{{ b, RET LitV $ lit_of_bool b;
- if b is true then ⌜lit_eq σ lit1 litl⌠∗ ownP (<[l:=(RSt 0, LitV lit2)]>σ)
- else ⌜lit_neq σ lit1 litl⌠∗ ownP σ }}}.
+Lemma wp_cas_int_suc E l z1 e2 lit2 :
+ to_val e2 = Some (LitV lit2) →
+ {{{ ▷ l ↦ LitV (LitInt z1) }}}
+ CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
+ {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof. intros ?. by apply wp_cas_suc. Qed.
+
+Lemma wp_cas_loc_suc E l l1 e2 lit2 :
+ to_val e2 = Some (LitV lit2) →
+ {{{ ▷ l ↦ LitV (LitLoc l1) }}}
+ CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+ {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
+Proof. intros ?. by apply wp_cas_suc. Qed.
+
+Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 lit2 l' vl' :
+ to_val e2 = Some (LitV lit2) → l1 ≠l' →
+ {{{ ▷ l ↦{q} LitV (LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
+ CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+ {{{ RET LitV (LitInt 0);
+ l ↦{q} LitV (LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
Proof.
- iIntros (?%of_to_val ? Hdec Hn ?) "HP HΦ". subst.
- iApply ownP_lift_atomic_head_step; eauto.
- { destruct Hdec as [Heq|Hneq].
- - specialize (Hn Heq). subst. do 3 eexists. by eapply CasSucS.
- - do 3 eexists. by eapply CasFailS. }
- iFrame. iNext. iIntros (e2 σ2 efs Hs) "Ho".
- inv_head_step; rewrite big_sepL_nil right_id.
- - iApply ("HΦ" $! false). eauto.
- - iApply ("HΦ" $! true). eauto.
- - exfalso. refine (_ (Hn _)); last done. intros. omega.
+ iIntros (<-%of_to_val ? Φ) "(>Hl & >Hl' & >Hl1) HΦ".
+ iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iDestruct (heap_read with "Hσ Hl") as %[nl ?].
+ iDestruct (heap_read with "Hσ Hl'") as %[nl' ?].
+ iDestruct (heap_read with "Hσ Hl1") as %[nl1 ?].
+ iModIntro; iSplit; first by eauto.
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; inv_lit.
+ iModIntro; iSplit=> //. iFrame. iApply "HΦ"; iFrame.
+Qed.
+
+Lemma wp_cas_loc_nondet E l l1 e2 l2 ll :
+ to_val e2 = Some (LitV $ LitLoc l2) →
+ {{{ ▷ l ↦ LitV (LitLoc ll) }}}
+ CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
+ {{{ b, RET LitV (lit_of_bool b);
+ if b is true then l ↦ LitV (LitLoc l2)
+ else ⌜l1 ≠ll⌠∗ l ↦ LitV (LitLoc ll) }}}.
+Proof.
+ iIntros (<-%of_to_val Φ) ">Hv HΦ".
+ iApply wp_lift_atomic_head_step_no_fork; auto.
+ iIntros (σ1) "Hσ". iDestruct (heap_read_1 with "Hσ Hv") as %?.
+ iModIntro; iSplit; first (destruct (decide (ll = l1)) as [->|]; by eauto).
+ iNext; iIntros (v2 σ2 efs Hstep); inv_head_step; last lia.
+ - inv_lit. iModIntro; iSplit; [done|]; iFrame "Hσ".
+ iApply "HΦ"; simpl; auto.
+ - iMod (heap_write with "Hσ Hv") as "[$ Hv]".
+ iModIntro; iSplit; [done|]. iApply "HΦ"; iFrame.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
{{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
Proof.
- iIntros (?) "?HΦ". iApply ownP_lift_pure_det_head_step; eauto.
+ iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto. iNext.
rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
Qed.
@@ -150,10 +222,11 @@ Lemma wp_rec E e f xl erec erec' el Φ :
subst_l (f::xl) (e::el) erec = Some erec' →
▷ WP erec' @ E {{ Φ }} -∗ WP App e el @ E {{ Φ }}.
Proof.
- iIntros (-> ???) "?". iApply ownP_lift_pure_det_head_step; subst; eauto.
+ iIntros (-> ???) "?". iApply wp_lift_pure_det_head_step; subst; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
Qed.
+(* TODO: wp_eq for locations, if needed.
Lemma wp_bin_op_heap E σ op l1 l2 l' :
bin_op_eval σ op l1 l2 l' →
{{{ ▷ ownP σ }}} BinOp op (Lit l1) (Lit l2) @ E
@@ -164,14 +237,15 @@ Proof.
inv_head_step; rewrite big_sepL_nil right_id.
iApply "HΦ". eauto.
Qed.
+*)
Lemma wp_bin_op_pure E op l1 l2 l' :
(∀ σ, bin_op_eval σ op l1 l2 l') →
{{{ True }}} BinOp op (Lit l1) (Lit l2) @ E
{{{ l'' σ, RET LitV l''; ⌜bin_op_eval σ op l1 l2 l''⌠}}}.
Proof.
- iIntros (? Φ) "HΦ". iApply ownP_lift_pure_head_step; eauto.
- { intros. inv_head_step. done. }
+ iIntros (? Φ) "HΦ". iApply wp_lift_pure_head_step; eauto.
+ { intros. by inv_head_step. }
iNext. iIntros (e2 efs σ Hs).
inv_head_step; rewrite big_sepL_nil right_id.
rewrite -wp_value //. iApply "HΦ". eauto.
@@ -182,7 +256,7 @@ Lemma wp_case E i e el Φ :
el !! (Z.to_nat i) = Some e →
▷ WP e @ E {{ Φ }} -∗ WP Case (Lit $ LitInt i) el @ E {{ Φ }}.
Proof.
- iIntros (??) "?". iApply ownP_lift_pure_det_head_step; eauto.
+ iIntros (??) "?". iApply wp_lift_pure_det_head_step; eauto.
by intros; inv_head_step; eauto. iNext. rewrite big_sepL_nil. by iFrame.
Qed.
End lifting.
diff --git a/theories/lang/memcpy.v b/theories/lang/memcpy.v
index 0506e6d5..e735915c 100644
--- a/theories/lang/memcpy.v
+++ b/theories/lang/memcpy.v
@@ -21,14 +21,13 @@ Notation "e1 <-{ n ',Σ' i } ! e2" :=
(at level 80, n, i at next level,
format "e1 <-{ n ,Σ i } ! e2") : expr_scope.
-Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q (n : Z):
- ↑heapN ⊆ E →
+Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
Z.of_nat (length vl1) = n → Z.of_nat (length vl2) = n →
- {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
+ {{{ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
#l1 <-{n} !#l2 @ E
{{{ RET #(); l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
Proof.
- iIntros (? Hvl1 Hvl2 Φ) "(#Hinv & Hl1 & Hl2) HΦ".
+ iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index d6a43c54..8c70b067 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -16,27 +16,27 @@ Definition delete : val :=
Global Opaque delete.
Section specs.
- Context `{heapG Σ}.
+ Context `{lrustG Σ}.
Lemma wp_new E n:
- ↑heapN ⊆ E → 0 ≤ n →
- {{{ heap_ctx }}} new [ #n ] @ E
+ 0 ≤ n →
+ {{{ True }}} new [ #n ] @ E
{{{ l vl, RET LitV $ LitLoc l;
⌜n = length vl⌠∗ (†l…(Z.to_nat n) ∨ ⌜n = 0âŒ) ∗ l ↦∗ vl }}}.
Proof.
- iIntros (? ? Φ) "#Hinv HΦ". wp_lam. wp_op; intros ?.
+ iIntros (? Φ) "HΦ". wp_lam. wp_op; intros ?.
- wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l vl as "H↦" "H†". iApply "HΦ". iFrame. auto.
Qed.
Lemma wp_delete E (n:Z) l vl :
- ↑heapN ⊆ E → n = length vl →
- {{{ heap_ctx ∗ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0âŒ) }}}
+ n = length vl →
+ {{{ l ↦∗ vl ∗ (†l…(length vl) ∨ ⌜n = 0âŒ) }}}
delete [ #n; #l] @ E
{{{ RET LitV LitUnit; True }}}.
Proof.
- iIntros (? ? Φ) "(#Hinv & H↦ & [H†|%]) HΦ";
+ iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
Qed.
End specs.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 43aae5c7..50ffa607 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -138,13 +138,13 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
end.
Section heap.
-Context `{heapG Σ}.
+Context `{lrustG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (iResUR Σ).
Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
- (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → 0 < n →
+ 0 < n →
IntoLaterNEnvs 1 Δ Δ' →
(∀ l vl, n = length vl → ∃ Δ'',
envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
@@ -152,7 +152,7 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
(Δ'' ⊢ Φ (LitV $ LitLoc l))) →
Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
Proof.
- intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
+ intros ?? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
rewrite -always_and_sep_l. apply and_intro; first done.
rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l;
apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
@@ -162,7 +162,7 @@ Proof.
Qed.
Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
- (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → n = length vl →
+ n = length vl →
IntoLaterNEnvs 1 Δ Δ' →
envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
envs_delete i1 false Δ' = Δ'' →
@@ -172,47 +172,43 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
(Δ''' ⊢ Φ (LitV LitUnit)) →
Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
- intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
- eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
- apply and_intro; first done.
+ intros -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
+ eapply wand_apply; first exact:wp_free; simpl.
rewrite into_laterN_env_sound -!later_sep; apply later_mono.
- do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True -fupd_intro.
+ do 2 (rewrite envs_lookup_sound' //).
+ by rewrite HΔ wand_True -fupd_intro -assoc.
Qed.
Lemma tac_wp_read Δ Δ' E i l q v o Φ :
- (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
+ o = Na1Ord ∨ o = ScOrd →
IntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
(Δ' ⊢ Φ v) →
Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
Proof.
- intros ??[->| ->]???.
+ intros [->| ->] ???.
- rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
- rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
- rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
- rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
rewrite -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
to_val e = Some v' →
- (Δ ⊢ heap_ctx) → ↑heapN ⊆ E → o = Na1Ord ∨ o = ScOrd →
+ o = Na1Ord ∨ o = ScOrd →
IntoLaterNEnvs 1 Δ Δ' →
envs_lookup i Δ' = Some (false, l ↦ v)%I →
envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
(Δ'' ⊢ Φ (LitV LitUnit)) →
Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
Proof.
- intros ???[->| ->]????.
+ intros ? [->| ->] ????.
- rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
- rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
- rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
- rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id -fupd_intro. by apply later_mono, sep_mono_r, wand_mono.
Qed.
@@ -235,9 +231,7 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
match eval hnf in e' with Alloc _ => wp_bind_core K end)
|fail 1 "wp_alloc: cannot find 'Alloc' in" e];
eapply tac_wp_alloc with _ H Hf;
- [iAssumption || fail "wp_alloc: cannot find heap_ctx"
- |solve_ndisj
- |try fast_done
+ [try fast_done
|apply _
|first [intros l vl ? | fail 1 "wp_alloc:" l "or" vl "not fresh"];
eexists; split;
@@ -258,9 +252,7 @@ Tactic Notation "wp_free" :=
match eval hnf in e' with Free _ _ => wp_bind_core K end)
|fail 1 "wp_free: cannot find 'Free' in" e];
eapply tac_wp_free;
- [iAssumption || fail "wp_free: cannot find heap_ctx"
- |solve_ndisj
- |try fast_done
+ [try fast_done
|apply _
|let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
@@ -282,9 +274,7 @@ Tactic Notation "wp_read" :=
match eval hnf in e' with Read _ _ => wp_bind_core K end)
|fail 1 "wp_read: cannot find 'Read' in" e];
eapply tac_wp_read;
- [iAssumption || fail "wp_read: cannot find heap_ctx"
- |solve_ndisj
- |(right; fast_done) || (left; fast_done) ||
+ [(right; fast_done) || (left; fast_done) ||
fail "wp_read: order is neither Na2Ord nor ScOrd"
|apply _
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -304,8 +294,6 @@ Tactic Notation "wp_write" :=
eapply tac_wp_write;
[let e' := match goal with |- to_val ?e' = _ => e' end in
wp_done || fail "wp_write:" e' "not a value"
- |iAssumption || fail "wp_write: cannot find heap_ctx"
- |solve_ndisj
|(right; fast_done) || (left; fast_done) ||
fail "wp_write: order is neither Na2Ord nor ScOrd"
|apply _
diff --git a/theories/typing/bool.v b/theories/typing/bool.v
index c1f228b0..eecf25ec 100644
--- a/theories/typing/bool.v
+++ b/theories/typing/bool.v
@@ -26,7 +26,7 @@ Section typing.
Lemma type_bool_instr (b : Datatypes.bool) E L :
typed_instruction_ty E L [] #b bool.
Proof.
- iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
+ iAlways. iIntros (tid qE) "_ $ $ $ _". wp_value.
rewrite tctx_interp_singleton tctx_hasty_val. by destruct b.
Qed.
@@ -43,12 +43,12 @@ Section typing.
typed_body E L C T e1 → typed_body E L C T e2 →
typed_body E L C T (if: p then e1 else e2).
Proof.
- iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
+ iIntros (Hp He1 He2) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
iIntros ([[| |[|[]|]]|]) "_ H1"; try iDestruct "H1" as "[]";
(iApply wp_case; [done..|iNext]).
- - iApply (He2 with "HEAP LFT Htl HE HL HC HT").
- - iApply (He1 with "HEAP LFT Htl HE HL HC HT").
+ - iApply (He2 with "LFT Htl HE HL HC HT").
+ - iApply (He1 with "LFT Htl HE HL HC HT").
Qed.
End typing.
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index 6ff47693..1ea3d962 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -47,7 +47,7 @@ Section borrow.
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◠&uniq{κ} own_ptr n ty] (!p) (&uniq{κ} ty).
Proof.
- iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+ iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[Htok Hclose]"; first set_solver.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
@@ -80,7 +80,7 @@ Section borrow.
lctx_lft_alive E L κ →
typed_instruction_ty E L [p ◠&shr{κ} own_ptr n ty] (!p) (&shr{κ} ty).
Proof.
- iIntros (Hκ) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+ iIntros (Hκ) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
@@ -108,7 +108,7 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◠&uniq{κ} &uniq{κ'} ty] (!p) (&uniq{κ} ty).
Proof.
- iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL Hp".
+ iIntros (Hκ Hincl) "!#". iIntros (tid qE) "#LFT $ HE HL Hp".
rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
@@ -145,7 +145,7 @@ Section borrow.
lctx_lft_alive E L κ → lctx_lft_incl E L κ κ' →
typed_instruction_ty E L [p ◠&shr{κ} &uniq{κ'} ty] (!p) (&shr{κ} ty).
Proof.
- iIntros (Hκ Hincl) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+ iIntros (Hκ Hincl) "!# * #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
iPoseProof (Hincl with "[#] [#]") as "Hincl".
{ by iApply elctx_interp_persist. } { by iApply llctx_interp_persist. }
iMod (Hκ with "HE HL") as (q) "[[Htok1 Htok2] Hclose]"; first set_solver.
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 7e579382..48d94ceb 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -13,7 +13,7 @@ Section typing.
tctx_incl E L T (T' (list_to_vec args)) →
typed_body E L C T (k (of_val <$> args)).
Proof.
- iIntros (HC Hincl) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
+ iIntros (HC Hincl) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
iSpecialize ("HC" with "HE []"); first done.
rewrite -{3}(vec_to_list_of_list args). iApply ("HC" with "Htl HL HT").
@@ -26,15 +26,15 @@ Section typing.
typed_body E L1 (k â—cont(L1, T') :: C) (T' args) (subst_v (kb::argsb) (k:::args) econt)) →
typed_body E L2 C T (e2 cont: kb argsb := econt).
Proof.
- iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". iApply wp_let'.
+ iIntros (Hc1 Hc2 He2 Hecont) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT". iApply wp_let'.
{ simpl. rewrite decide_left. done. }
- iModIntro. iApply (He2 with "HEAP LFT Htl HE HL [HC] HT"). clear He2.
+ iModIntro. iApply (He2 with "LFT Htl HE HL [HC] HT"). clear He2.
iIntros "HE". iLöb as "IH". iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply ("HC" with "HE").
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
- iNext. iApply (Hecont with "HEAP LFT Htl HE HL [HC] HT").
+ iNext. iApply (Hecont with "LFT Htl HE HL [HC] HT").
by iApply "IH".
Qed.
End typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 84625161..4749eb98 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -31,7 +31,7 @@ Section fn.
Proof.
intros ?? Htys ?? Hty. unfold fn. f_equiv. rewrite st_dist_unfold /=.
f_contractive=>tid vl. unfold typed_body.
- do 12 f_equiv. f_contractive. do 18 f_equiv.
+ do 12 f_equiv. f_contractive. do 17 f_equiv.
- rewrite !cctx_interp_singleton /=. do 5 f_equiv.
rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat f_equiv. apply Hty.
by rewrite (ty_size_proper_d _ _ _ (Hty _)).
@@ -77,10 +77,10 @@ Section typing.
intros HE Htys Hty. apply subtype_simple_type=>//= _ vl.
iIntros "#LFT #HE0 #HL0 Hf". iDestruct "Hf" as (fb kb xb e ?) "[% [% #Hf]]". subst.
iExists fb, kb, xb, e, _. iSplit. done. iSplit. done. iNext.
- rewrite /typed_body. iIntros "* !# * #HEAP _ Htl HE HL HC HT".
+ rewrite /typed_body. iIntros "* !# * _ Htl HE HL HC HT".
iDestruct (elctx_interp_persist with "HE") as "#HEp".
iMod (HE with "HE0 HL0 HE") as (qE') "[HE' Hclose]". done.
- iApply ("Hf" with "HEAP LFT Htl HE' HL [HC Hclose] [HT]").
+ iApply ("Hf" with "LFT Htl HE' HL [HC Hclose] [HT]").
- iIntros "HE'". unfold cctx_interp. iIntros (elt) "Helt".
iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
iMod ("Hclose" with "HE'") as "HE".
@@ -172,7 +172,7 @@ Section typing.
T)
(call: p ps → k).
Proof.
- iIntros (HE) "!# * #HEAP #LFT Htl HE HL HC".
+ iIntros (HE) "!# * #LFT Htl HE HL HC".
rewrite tctx_interp_cons tctx_interp_app. iIntros "(Hf & Hargs & HT)".
wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = kâŒ):::
@@ -193,7 +193,7 @@ Section typing.
{ rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::k:::vl)) //. }
iNext. iSpecialize ("Hf" $! x k vl).
iMod (HE with "HE HL") as (q') "[HE' Hclose]"; first done.
- iApply ("Hf" with "HEAP LFT Htl HE' [] [HC Hclose HT]").
+ iApply ("Hf" with "LFT Htl HE' [] [HC Hclose HT]").
+ by rewrite /llctx_interp big_sepL_nil.
+ iIntros "HE'". iApply fupd_cctx_interp. iMod ("Hclose" with "HE'") as "[HE HL]".
iSpecialize ("HC" with "HE"). iModIntro. iIntros (y) "IN".
@@ -267,13 +267,13 @@ Section typing.
(subst_v (fb :: BNamed "return" :: argsb) (f ::: k ::: args) e)) →
typed_instruction_ty E L T (funrec: fb argsb := e) (fn E' tys ty).
Proof.
- iIntros (Hc Hbody) "!# * #HEAP #LFT $ $ $ #HT". iApply wp_value.
+ iIntros (Hc Hbody) "!# * #LFT $ $ $ #HT". iApply wp_value.
{ simpl. rewrite ->(decide_left Hc). done. }
rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
{ simpl. rewrite decide_left. done. }
iExists fb, _, argsb, e, _. iSplit. done. iSplit. done. iNext. clear qE.
- iIntros (x k args) "!#". iIntros (tid' qE) "_ _ Htl HE HL HC HT'".
- iApply (Hbody with "HEAP LFT Htl HE HL HC").
+ iIntros (x k args) "!#". iIntros (tid' qE) "_ Htl HE HL HC HT'".
+ iApply (Hbody with "LFT Htl HE HL HC").
rewrite tctx_interp_cons tctx_interp_app. iFrame "HT' IH".
by iApply sendc_change_tid.
Qed.
diff --git a/theories/typing/int.v b/theories/typing/int.v
index d4384fe9..fc156b3c 100644
--- a/theories/typing/int.v
+++ b/theories/typing/int.v
@@ -25,7 +25,7 @@ Section typing.
Lemma type_int_instr (z : Z) E L :
typed_instruction_ty E L [] #z int.
Proof.
- iAlways. iIntros (tid qE) "_ _ $ $ $ _". wp_value.
+ iAlways. iIntros (tid qE) "_ $ $ $ _". wp_value.
by rewrite tctx_interp_singleton tctx_hasty_val.
Qed.
@@ -40,7 +40,7 @@ Section typing.
Lemma type_plus_instr E L p1 p2 :
typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 + p2) int.
Proof.
- iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1").
iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
@@ -61,7 +61,7 @@ Section typing.
Lemma type_minus_instr E L p1 p2 :
typed_instruction_ty E L [p1 â— int; p2 â— int] (p1 - p2) int.
Proof.
- iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1").
iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
@@ -82,7 +82,7 @@ Section typing.
Lemma type_le_instr E L p1 p2 :
typed_instruction_ty E L [p1 ◠int; p2 ◠int] (p1 ≤ p2) bool.
Proof.
- iAlways. iIntros (tid qE) "_ _ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
+ iAlways. iIntros (tid qE) "_ $ $ $". rewrite tctx_interp_cons tctx_interp_singleton.
iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1").
iIntros ([[]|]) "_ H1"; try iDestruct "H1" as "[]".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index ebb7114c..361c1679 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -197,8 +197,8 @@ Section typing.
let n' := Z.to_nat n in
typed_instruction_ty E L [] (new [ #n ]%E) (own_ptr n' (uninit n')).
Proof.
- intros. iAlways. iIntros (tid q) "#HEAP #LFT $ $ $ _".
- iApply (wp_new with "HEAP"); try done. iModIntro.
+ intros. iAlways. iIntros (tid q) "#LFT $ $ $ _".
+ iApply wp_new; first done. iModIntro.
iIntros (l vl) "(% & H†& Hlft)". subst. rewrite tctx_interp_singleton tctx_hasty_val.
iNext. rewrite freeable_sz_full Z2Nat.id //. iFrame.
iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
@@ -231,7 +231,7 @@ Section typing.
Z.of_nat (ty.(ty_size)) = n →
typed_instruction E L [p ◠box ty] (delete [ #n; p])%E (λ _, []).
Proof.
- iIntros (<-) "!#". iIntros (tid eq) "#HEAP #LFT $ $ $ Hp". rewrite tctx_interp_singleton.
+ iIntros (<-) "!#". iIntros (tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown";
try iDestruct "Hown" as "[]". iDestruct "Hown" as "[H↦∗: >H†]".
iDestruct "H↦∗:" as (vl) "[>H↦ Hown]". rewrite tctx_interp_nil.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index b0b14236..aa24794b 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -10,7 +10,7 @@ Section typing.
(* This is an iProp because it is also used by the function type. *)
Definition typed_body (E : elctx) (L : llctx) (C : cctx) (T : tctx)
(e : expr) : iProp Σ :=
- (□ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+ (□ ∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
elctx_interp E qE -∗ llctx_interp L 1 -∗
(elctx_interp E qE -∗ cctx_interp tid C) -∗ tctx_interp tid T -∗
WP e {{ _, cont_postcondition }})%I.
@@ -35,9 +35,9 @@ Section typing.
(typed_body E L).
Proof.
intros C1 C2 HC T1 T2 HT e ? <-. iIntros "#H !#".
- iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
+ iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (HT with "LFT HE HL HT") as "(HE & HL & HT)".
- iApply ("H" with "HEAP LFT Htl HE HL [HC] HT").
+ iApply ("H" with "LFT Htl HE HL [HC] HT").
iIntros "HE". by iApply (HC with "LFT HC").
Qed.
@@ -49,7 +49,7 @@ Section typing.
(** Instruction *)
Definition typed_instruction (E : elctx) (L : llctx)
(T1 : tctx) (e : expr) (T2 : val → tctx) : iProp Σ :=
- (□ ∀ tid qE, heap_ctx -∗ lft_ctx -∗ na_own tid ⊤ -∗
+ (□ ∀ tid qE, lft_ctx -∗ na_own tid ⊤ -∗
elctx_interp E qE -∗ llctx_interp L 1 -∗ tctx_interp tid T1 -∗
WP e {{ v, na_own tid ⊤ ∗ elctx_interp E qE ∗
llctx_interp L 1 ∗ tctx_interp tid (T2 v) }})%I.
@@ -92,10 +92,10 @@ Section typing_rules.
typed_body ((κ1 ⊑ κ2) :: (κ2 ⊑ κ1) :: E) L C T e →
typed_body E ((κ1 ⊑ [κ2]%list) :: L) C T e.
Proof.
- iIntros (He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
+ iIntros (He) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
- iApply (He with "HEAP LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
+ iApply (He with "LFT Htl [Hκ1 Hκ2 HE] HL [HC] HT").
- rewrite /elctx_interp !big_sepL_cons. by iFrame.
- rewrite /elctx_interp !big_sepL_cons. iIntros "(_ & _ & HE)".
iApply "HC". done.
@@ -107,11 +107,11 @@ Section typing_rules.
(∀ v : val, typed_body E L C (T2 v ++ T) (subst' xb v e')) →
typed_body E L C (T1 ++ T) (let: xb := e in e').
Proof.
- iIntros (Hc He He') "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT". rewrite tctx_interp_app.
+ iIntros (Hc He He') "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT". rewrite tctx_interp_app.
iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[HE HL HT1 Htl]").
- { iApply (He with "HEAP LFT Htl HE HL HT1"). }
+ { iApply (He with "LFT Htl HE HL HT1"). }
iIntros (v) "/= (Htl & HE & HL & HT2)". iApply wp_let; first wp_done.
- iModIntro. iApply (He' with "HEAP LFT Htl HE HL HC [HT2 HT]").
+ iModIntro. iApply (He' with "LFT Htl HE HL HC [HT2 HT]").
rewrite tctx_interp_app. by iFrame.
Qed.
@@ -136,10 +136,10 @@ Section typing_rules.
(∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
typed_body E L C T (Newlft ;; e).
Proof.
- iIntros (Hc He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HC HT".
+ iIntros (Hc He) "!#". iIntros (tid qE) "#LFT Htl HE HL HC HT".
iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
set (κ' := foldr (∪) static κs). wp_seq.
- iApply (He (κ' ∪ Λ) with "HEAP LFT Htl HE [HL Htk] HC HT").
+ iApply (He (κ' ∪ Λ) with "LFT Htl HE [HL Htk] HC HT").
rewrite /llctx_interp big_sepL_cons. iFrame "HL".
iExists Λ. iSplit; first done. iFrame. done.
Qed.
@@ -150,18 +150,18 @@ Section typing_rules.
Closed [] e → UnblockTctx κ T1 T2 →
typed_body E L C T2 e → typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
Proof.
- iIntros (Hc Hub He) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
+ iIntros (Hc Hub He) "!#". iIntros (tid qE) "#LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
iSpecialize ("Hend" with "Htok"). wp_bind Endlft.
iApply (wp_fupd_step with "Hend"); try done. wp_seq.
- iIntros "#Hdead !>". wp_seq. iApply (He with "HEAP LFT Htl HE HL HC >").
+ iIntros "#Hdead !>". wp_seq. iApply (He with "LFT Htl HE HL HC >").
iApply (Hub with "[] HT"). simpl in *. subst κ. rewrite -lft_dead_or. auto.
Qed.
Lemma type_path_instr {E L} p ty :
typed_instruction_ty E L [p â— ty] p ty.
Proof.
- iIntros "!# * _ _ $$$ ?". rewrite tctx_interp_singleton.
+ iIntros "!# * _ $$$ ?". rewrite tctx_interp_singleton.
iApply (wp_hasty with "[-]"). done. iIntros (v) "_ Hv".
rewrite tctx_interp_singleton. iExists v. iFrame. by rewrite eval_path_of_val.
Qed.
@@ -179,7 +179,7 @@ Section typing_rules.
typed_write E L ty1 ty ty1' →
typed_instruction E L [p1 ◠ty1; p2 ◠ty] (p1 <- p2) (λ _, [p1 ◠ty1']%TC).
Proof.
- iIntros (Hwrt) "!#". iIntros (tid qE) "#HEAP #LFT $ HE HL".
+ iIntros (Hwrt) "!#". iIntros (tid qE) "#LFT $ HE HL".
rewrite tctx_interp_cons tctx_interp_singleton. iIntros "[Hp1 Hp2]".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "_ Hown2".
@@ -205,7 +205,7 @@ Section typing_rules.
ty.(ty_size) = 1%nat → typed_read E L ty1 ty ty1' →
typed_instruction E L [p ◠ty1] (!p) (λ v, [p ◠ty1'; v ◠ty]%TC).
Proof.
- iIntros (Hsz Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL Hp".
+ iIntros (Hsz Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL Hp".
rewrite tctx_interp_singleton. wp_bind p. iApply (wp_hasty with "Hp").
iIntros (v) "% Hown".
iMod (Hread with "[] LFT Htl HE HL Hown") as
@@ -232,14 +232,14 @@ Section typing_rules.
Lemma type_memcpy_iris E qE L qL tid ty ty1 ty1' ty2 ty2' (n : Z) p1 p2 :
Z.of_nat (ty.(ty_size)) = n →
typed_write E L ty1 ty ty1' -∗ typed_read E L ty2 ty ty2' -∗
- {{{ heap_ctx ∗ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
+ {{{ lft_ctx ∗ na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
tctx_elt_interp tid (p1 ◠ty1) ∗ tctx_elt_interp tid (p2 ◠ty2) }}}
(p1 <-{n} !p2)
{{{ RET #(); na_own tid ⊤ ∗ elctx_interp E qE ∗ llctx_interp L qL ∗
tctx_elt_interp tid (p1 ◠ty1') ∗ tctx_elt_interp tid (p2 ◠ty2') }}}.
Proof.
iIntros (<-) "#Hwrt #Hread !#".
- iIntros (Φ) "(#HEAP & #LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
+ iIntros (Φ) "(#LFT & Htl & [HE1 HE2] & [HL1 HL2] & [Hp1 Hp2]) HΦ".
wp_bind p1. iApply (wp_hasty with "Hp1"). iIntros (v1) "% Hown1".
wp_bind p2. iApply (wp_hasty with "Hp2"). iIntros (v2) "% Hown2".
iMod ("Hwrt" with "[] LFT HE1 HL1 Hown1")
@@ -247,7 +247,7 @@ Section typing_rules.
iMod ("Hread" with "[] LFT Htl HE2 HL2 Hown2")
as (l2 vl2 q2) "(% & Hl2 & Hown2 & Hcl2)"; first done.
iDestruct (ty_size_eq with "Hown2") as "#>%". subst v1 v2. iApply wp_fupd.
- iApply (wp_memcpy with "[$HEAP $Hl1 $Hl2]"); first done; try congruence; [].
+ iApply (wp_memcpy with "[$Hl1 $Hl2]"); try congruence; [].
iNext. iIntros "[Hl1 Hl2]". iApply ("HΦ" with ">"). rewrite !tctx_hasty_val' //.
iMod ("Hcl1" with "[Hl1 Hown2]") as "($ & $ & $)".
{ iExists _. iFrame. }
@@ -260,8 +260,8 @@ Section typing_rules.
typed_instruction E L [p1 â— ty1; p2 â— ty2] (p1 <-{n} !p2)
(λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
- iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#HEAP #LFT Htl HE HL HT".
- iApply (type_memcpy_iris with "[] [] [$HEAP $LFT $Htl $HE $HL HT]"); try done.
+ iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL HT".
+ iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
(* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
{ iPoseProof Hwrt as "Hwrt". done. }
{ iPoseProof Hread as "Hread". done. }
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index d67353e0..c6f7e7b4 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -9,14 +9,14 @@ From lrust.typing Require Import typing.
Set Default Proof Using "Type".
Class typePreG Σ := PreTypeG {
- type_heapG :> heapPreG Σ;
+ type_heapG :> lrustPreG Σ;
type_lftG :> lftPreG Σ;
type_preG_na_invG :> na_invG Σ;
type_frac_borrowG :> frac_borG Σ
}.
Definition typeΣ : gFunctors :=
- #[heapΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
+ #[lrustΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
Proof. solve_inG. Qed.
@@ -36,11 +36,11 @@ Section type_soundness.
cut (adequate (main [exit_cont]%E) ∅ (λ _, True)).
{ split. by eapply adequate_nonracing.
intros. by eapply (adequate_safe (main [exit_cont]%E)). }
- apply: heap_adequacy=>?.
- iIntros "!# #HEAP". iMod lft_init as (?) "#LFT". done.
+ apply: lrust_adequacy=>?.
+ iMod lft_init as (?) "#LFT". done.
iMod na_alloc as (tid) "Htl". set (Htype := TypeG _ _ _ _ _).
wp_bind (of_val main). iApply (wp_wand with "[Htl]").
- iApply (Hmain _ $! tid 1%Qp with "HEAP LFT Htl [] [] []").
+ iApply (Hmain _ $! tid 1%Qp with "LFT Htl [] [] []").
{ by rewrite /elctx_interp big_sepL_nil. }
{ by rewrite /llctx_interp big_sepL_nil. }
{ by rewrite tctx_interp_nil. }
@@ -51,7 +51,7 @@ Section type_soundness.
destruct x; try done.
iApply (wp_rec _ _ _ _ _ _ [exit_cont]%E); [done| |by simpl_subst|iNext].
{ repeat econstructor. apply to_of_val. }
- iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "HEAP LFT Htl HE HL []");
+ iApply ("Hmain" $! () exit_cont [#] tid 1%Qp with "LFT Htl HE HL []");
last by rewrite tctx_interp_nil.
iIntros "_". rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
inv_vec args. iIntros (x) "_ /=". by wp_lam.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 6a45388f..1ef9e656 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -6,7 +6,7 @@ From lrust.typing Require Import lft_contexts.
Set Default Proof Using "Type".
Class typeG Σ := TypeG {
- type_heapG :> heapG Σ;
+ type_heapG :> lrustG Σ;
type_lftG :> lftG Σ;
type_na_invG :> na_invG Σ;
type_frac_borrowG :> frac_borG Σ
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index a0eae973..3df1f459 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -15,7 +15,7 @@ Section case.
typed_body E L C ((p ◠own_ptr n (sum tyl)) :: T) e) tyl el →
typed_body E L C ((p â— own_ptr n (sum tyl)) :: T) (case: !p of el).
Proof.
- iIntros (Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+ iIntros (Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp";
try iDestruct "Hp" as "[]". iDestruct "Hp" as "[H↦ Hf]".
@@ -30,7 +30,7 @@ Section case.
destruct (tyl !! i) as [ty|] eqn:EQty; last iDestruct "Hown" as ">[]".
edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
- destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
+ destruct Hety as [Hety|Hety]; iApply (Hety with "LFT Hna HE HL HC");
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
- iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
@@ -61,7 +61,7 @@ Section case.
typed_body E L C ((p ◠&uniq{κ}sum tyl) :: T) e) tyl el →
typed_body E L C ((p ◠&uniq{κ}sum tyl) :: T) (case: !p of el).
Proof.
- iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+ iIntros (Halive Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
iMod (Halive with "HE HL") as (q) "[Htok Hclose]". done.
@@ -86,7 +86,7 @@ Section case.
iFrame. iExists _, _, _. iSplit. by auto.
rewrite /= -EQlen !app_length EQlenvl' EQlenvl'2 nth_lookup EQty /=. auto. }
iMod ("Hclose" with "Htok") as "[HE HL]".
- iApply (Hety with "HEAP LFT Hna HE HL HC").
+ iApply (Hety with "LFT Hna HE HL HC").
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
- iMod ("Hclose'" with "[H↦i H↦vl' H↦vl'' Hown] []") as "[Hb Htok]";
[|by iIntros "!>$"|].
@@ -94,7 +94,7 @@ Section case.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_app -EQlen. iFrame. iNext.
iExists i, vl', vl''. rewrite nth_lookup EQty. auto. }
iMod ("Hclose" with "Htok") as "[HE HL]".
- iApply (Hety with "HEAP LFT Hna HE HL HC").
+ iApply (Hety with "LFT Hna HE HL HC").
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //. iFrame.
Qed.
@@ -114,7 +114,7 @@ Section case.
typed_body E L C ((p ◠&shr{κ}sum tyl) :: T) e) tyl el →
typed_body E L C ((p ◠&shr{κ}sum tyl) :: T) (case: !p of el).
Proof.
- iIntros (Halive Hel) "!#". iIntros (tid qE) "#HEAP #LFT Hna HE HL HC HT". wp_bind p.
+ iIntros (Halive Hel) "!#". iIntros (tid qE) "#LFT Hna HE HL HC HT". wp_bind p.
rewrite tctx_interp_cons. iDestruct "HT" as "[Hp HT]".
iApply (wp_hasty with "Hp"). iIntros ([[]|] Hv) "Hp"; try iDestruct "Hp" as "[]".
iDestruct "Hp" as (i) "[#Hb Hshr]".
@@ -126,7 +126,7 @@ Section case.
wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
iMod ("Hclose'" with "[$H↦i $H↦vl'']") as "Htok".
iMod ("Hclose" with "Htok") as "[HE HL]".
- destruct Hety as [Hety|Hety]; iApply (Hety with "HEAP LFT Hna HE HL HC");
+ destruct Hety as [Hety|Hety]; iApply (Hety with "LFT Hna HE HL HC");
rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame.
iExists _. rewrite ->nth_lookup, EQty. auto.
Qed.
@@ -146,7 +146,7 @@ Section case.
tyl !! i = Some ty →
typed_instruction E L [p1 ◠ty1; p2 ◠ty] (p1 <-{Σ i} p2) (λ _, [p1 ◠ty2]%TC).
Proof.
- iIntros (Hw Hty) "!# * #HEAP #LFT $ HE HL Hp".
+ iIntros (Hw Hty) "!# * #LFT $ HE HL Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
@@ -185,7 +185,7 @@ Section case.
typed_write E L ty1 (sum tyl) ty2 →
typed_instruction E L [p ◠ty1] (p <-{Σ i} ()) (λ _, [p ◠ty2]%TC).
Proof.
- iIntros (Hty Hw) "!# * #HEAP #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
+ iIntros (Hty Hw) "!# * #LFT $ HE HL Hp". rewrite tctx_interp_singleton.
wp_bind p. iApply (wp_hasty with "Hp"). iIntros (v Hv) "Hty".
iMod (Hw with "[] LFT HE HL Hty") as (l vl) "(H & H↦ & Hw)". done.
simpl. destruct vl as [|? vl]; iDestruct "H" as %[[= Hlen] ->].
@@ -215,7 +215,7 @@ Section case.
typed_instruction E L [p1 â— ty1; p2 â— ty2]
(p1 <-{ty.(ty_size),Σ i} !p2) (λ _, [p1 ◠ty1'; p2 ◠ty2']%TC).
Proof.
- iIntros (Hty Hw Hr) "!# * #HEAP #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
+ iIntros (Hty Hw Hr) "!# * #LFT Htl [HE1 HE2] [HL1 HL2] Hp".
rewrite tctx_interp_cons tctx_interp_singleton.
iDestruct "Hp" as "[Hp1 Hp2]". iDestruct (closed_hasty with "Hp1") as "%".
iDestruct (closed_hasty with "Hp2") as "%". wp_bind p1.
@@ -233,7 +233,7 @@ Section case.
rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
iDestruct (ty_size_eq with "Hty") as "#>%".
- iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦vl1 $H↦2]"); [done| |lia|].
+ iApply wp_fupd. iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [|lia|].
{ rewrite take_length. lia. }
iNext; iIntros "[H↦vl1 H↦2]".
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 6bae5c4d..878c6ba0 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -151,7 +151,7 @@ Section typing.
(T2 := λ _, [d ◠&shr{α} cell ty;
x â— box (uninit ty.(ty_size))]%TC); try solve_typing; [|].
{ (* The core of the proof: Showing that the assignment is safe. *)
- iAlways. iIntros (tid qE) "#HEAP #LFT Htl HE $".
+ iAlways. iIntros (tid qE) "#LFT Htl HE $".
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iIntros "[#Hshr Hx]". rewrite {1}/elctx_interp big_opL_singleton /=.
destruct d as [[]|]; try iDestruct "Hshr" as "[]".
@@ -161,7 +161,7 @@ Section typing.
iDestruct ("Hown") as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%".
iDestruct (ty_size_eq with "Hown'") as "#>%".
- iApply wp_fupd. iApply (wp_memcpy with "[$HEAP $H↦ $H↦']"); [done||lia..|].
+ iApply wp_fupd. iApply (wp_memcpy with "[$H↦ $H↦']"); [done||lia..|].
iNext. iIntros "[H↦ H↦']". rewrite {1}/elctx_interp big_opL_singleton /=.
iMod ("Hclose" with "[H↦ Hown'] Htl") as "[$ $]".
{ iExists vl'. by iFrame. }
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 0819a6cc..97284a3b 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -29,7 +29,7 @@ Section ref_functions.
Proof.
apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
- iIntros "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
@@ -73,7 +73,7 @@ Section ref_functions.
wp_bind (new [ #2])%E. iApply wp_new; [done..|]. iNext. iIntros (lr ?) "(%&?&Hlr)".
iAssert (lx' ↦∗{qlx'} [ #lv; #lrc])%I with "[H↦1 H↦2]" as "H↦".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
- wp_let. wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hlr $H↦]"); [done..|].
+ wp_let. wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hlr $H↦]"); [done..|].
iIntros "!>[Hlr H↦]". wp_seq.
iMod ("Hcloseα2" with "[$H◯] Hna") as "[Hα2 Hna]".
iMod ("Hcloseδ" with "[H↦lrc H◠Hν1 INV] Hna") as "[Hδ Hna]".
@@ -83,7 +83,7 @@ Section ref_functions.
iAssert (elctx_interp [☀ α; ☀ β] qE) with "[Hα1 Hα2 Hβ]" as "HE".
{ rewrite /elctx_interp big_sepL_cons big_sepL_singleton. iFrame. }
iApply (type_delete _ _
- [ x ◠box (uninit 1); #lr ◠box(ref β ty)]%TC with "HEAP LFT Hna HE HL Hk");
+ [ x ◠box (uninit 1); #lr ◠box(ref β ty)]%TC with "LFT Hna HE HL Hk");
[solve_typing..| |]; first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
rewrite /= freeable_sz_full. iFrame. iExists _. iFrame. iExists _, _, _, _, _.
@@ -109,7 +109,7 @@ Section ref_functions.
Proof.
apply type_fn; [apply _..|]. move=>/= [α β] ret arg. inv_vec arg=>x. simpl_subst.
eapply type_deref; [solve_typing..|by apply read_own_move|done|]=>x'.
- iIntros "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']".
destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
@@ -123,7 +123,7 @@ Section ref_functions.
iAssert (elctx_interp [☀ α; ☀ β; α ⊑ β] qE) with "[Hα Hβ Hαβ]" as "HE".
{ rewrite /elctx_interp 2!big_sepL_cons big_sepL_singleton. by iFrame. }
iApply (type_letalloc_1 (&shr{α}ty) _
- [ x ◠box (uninit 1); #lv ◠&shr{α}ty]%TC with "HEAP LFT Hna HE HL Hk");
+ [ x ◠box (uninit 1); #lv ◠&shr{α}ty]%TC with "LFT Hna HE HL Hk");
[solve_typing..| |]; first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
iFrame. iApply (ty_shr_mono with "LFT [] Hshr"). by iApply lft_incl_glb. }
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index c78ea6a4..faf8ef0d 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -25,7 +25,7 @@ Section refcell_functions.
Proof.
apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
eapply type_new; [solve_typing..|].
- iIntros (r) "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hr Hx]".
@@ -36,10 +36,10 @@ Section refcell_functions.
iDestruct "Hr" as "[Hr↦ >SZ]". destruct vl' as [|]; iDestruct "SZ" as %[=].
rewrite heap_mapsto_vec_cons. iDestruct "Hr↦" as "[Hr↦0 Hr↦1]". wp_op.
rewrite shift_loc_0. wp_write. wp_op. iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
- wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦1 $Hx↦]"); [done||lia..|].
+ wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hr↦1 $Hx↦]"); [done||lia..|].
iIntros "!> [Hr↦1 Hx↦]". wp_seq.
iApply (type_delete _ _ [ #lx â— box (uninit (ty_size ty)); #lr â— box (refcell ty)]%TC
- with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
+ with "LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //=. iFrame.
iSplitL "Hx↦".
- iExists _. rewrite uninit_own. auto.
@@ -60,7 +60,7 @@ Section refcell_functions.
Proof.
apply type_fn; [apply _..|]. move=>/= _ ret arg. inv_vec arg=>x. simpl_subst.
eapply type_new; [solve_typing..|].
- iIntros (r) "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (r) "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try iDestruct "Hx" as "[]".
@@ -70,10 +70,10 @@ Section refcell_functions.
iDestruct "Hr" as (vl') "Hr". rewrite uninit_own heap_mapsto_vec_cons.
iDestruct "Hr" as "[Hr↦ >%]". iDestruct "Hx↦" as "[Hx↦0 Hx↦1]". wp_op.
iDestruct "Hx" as "[% Hx]". iDestruct (ty.(ty_size_eq) with "Hx") as %Hsz.
- wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$HEAP $Hr↦ $Hx↦1]"); [done||lia..|].
+ wp_bind (_ <-{_} !_)%E. iApply (wp_memcpy with "[$Hr↦ $Hx↦1]"); [done||lia..|].
iIntros "!> [Hr↦ Hx↦1]". wp_seq.
iApply (type_delete _ _ [ #lx â— box (uninit (S (ty_size ty))); #lr â— box ty]%TC
- with "HEAP LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
+ with "LFT Hna HE HL Hk [-]"); [solve_typing..| |]; last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iSplitR "Hr↦ Hx".
- iExists (_::_). rewrite heap_mapsto_vec_cons uninit_own -Hsz. iFrame. auto.
@@ -93,7 +93,7 @@ Section refcell_functions.
Proof.
apply type_fn; [apply _..|]. move=>/= α ret arg. inv_vec arg=>x. simpl_subst.
eapply type_deref; [solve_typing..|by eapply read_own_move|done|]=>x'. simpl_subst.
- iIntros "!# * #HEAP #LFT Hna HE HL HC HT".
+ iIntros "!# * #LFT Hna HE HL HC HT".
rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "[Hx Hx']". destruct x' as [[|lx'|]|]; try iDestruct "Hx'" as "[]".
iAssert (&{α} (∃ (z : Z), lx' ↦ #z ∗ ⌜-1 ≤ zâŒ) ∗
@@ -109,7 +109,7 @@ Section refcell_functions.
iDestruct "Hx" as (vl) "[Hx↦ Hx]". rewrite uninit_own. wp_op.
iApply (type_assign _ _ _ _
[ #lx ◠box (uninit 1); #(shift_loc lx' 1) ◠&uniq{α}ty]%TC
- with "HEAP LFT Hna HE HL HC [-]");
+ with "LFT Hna HE HL HC [-]");
[solve_typing..|by apply write_own| |]; last first.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //. iFrame.
iNext. iExists _. rewrite uninit_own. iFrame. }
@@ -148,7 +148,7 @@ Section refcell_functions.
eapply (type_jump [_]); solve_typing. }
eapply type_new; [solve_typing..|]=>r. simpl_subst.
eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
- iIntros (x') "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "(Hx & Hx' & Hr)".
destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
@@ -163,7 +163,7 @@ Section refcell_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_assign_unit [ref α ty; unit] _ _ _ _
[ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3) ]%TC
- with "HEAP LFT Hna HE HL Hk");
+ with "LFT Hna HE HL Hk");
[solve_typing..|by eapply write_own|done| |]; first last.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
simpl. eapply (type_jump [_]); solve_typing.
@@ -208,7 +208,7 @@ Section refcell_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [ref α ty; unit] _ _ _ _ _ _ _ _
[ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3); #lref ◠box (ref α ty)]%TC
- with "HEAP LFT Hna HE HL Hk");
+ with "LFT Hna HE HL Hk");
[solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
@@ -251,7 +251,7 @@ Section refcell_functions.
eapply (type_jump [_]); solve_typing. }
eapply type_new; [solve_typing..|]=>r. simpl_subst.
eapply type_deref; [solve_typing..|apply read_own_copy, _|done|].
- iIntros (x') "!# * #HEAP #LFT Hna HE HL Hk HT". simpl_subst.
+ iIntros (x') "!# * #LFT Hna HE HL Hk HT". simpl_subst.
rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
iDestruct "HT" as "(Hx & Hx' & Hr)".
destruct x' as [[|lx|]|]; try iDestruct "Hx'" as "[]".
@@ -274,7 +274,7 @@ Section refcell_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_memcpy [refmut α ty; unit] _ _ _ _ _ _ _ _
[ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3); #lref ◠box (refmut α ty)]%TC
- with "HEAP LFT Hna HE HL Hk");
+ with "LFT Hna HE HL Hk");
[solve_typing..|by eapply write_own|by eapply read_own_move|done|done| |];
first last.
{ rewrite 2!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame.
@@ -288,7 +288,7 @@ Section refcell_functions.
{ rewrite {1}/elctx_interp big_sepL_singleton /=. iApply "Hclose". by iFrame. }
iApply (type_sum_assign_unit [refmut α ty; unit] _ _ _ _
[ x ◠box (&shr{α}(refcell ty)); r ◠box (uninit 3) ]%TC
- with "HEAP LFT Hna HE HL Hk");
+ with "LFT Hna HE HL Hk");
[solve_typing..|by eapply write_own|done| |]; first last.
{ rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
simpl. eapply (type_jump [_]); solve_typing.
--
GitLab