From dc3ff29e295d5fdaa3756e49c8c13905281d8233 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 6 Mar 2019 22:46:57 +0100
Subject: [PATCH] fix merge + bump gpfsl
---
opam | 2 +-
theories/lang/adequacy.v | 32 --
theories/lang/heap.v | 548 -------------------------------
theories/lang/lang.v | 660 --------------------------------------
theories/lang/lifting.v | 377 ----------------------
theories/lang/proofmode.v | 259 ---------------
theories/lang/spawn.v | 2 +-
7 files changed, 2 insertions(+), 1878 deletions(-)
delete mode 100644 theories/lang/adequacy.v
delete mode 100644 theories/lang/heap.v
delete mode 100644 theories/lang/lang.v
delete mode 100644 theories/lang/lifting.v
delete mode 100644 theories/lang/proofmode.v
diff --git a/opam b/opam
index 9027351e..15107505 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-gpfsl" { (= "dev.2019-03-04.0.5f34e857") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2019-03-06.1.8f1c2d76") | (= "dev") }
]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
deleted file mode 100644
index 05315b8c..00000000
--- a/theories/lang/adequacy.v
+++ /dev/null
@@ -1,32 +0,0 @@
-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 lrustPreG Σ := HeapPreG {
- lrust_preG_irig :> invPreG Σ;
- lrust_preG_heap :> inG Σ (authR heapUR);
- lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
-}.
-
-Definition lrustΣ : gFunctors :=
- #[invΣ;
- GFunctor (constRF (authR heapUR));
- GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustPreG Σ.
-Proof. solve_inG. Qed.
-
-Definition lrust_adequacy Σ `{!lrustPreG Σ} e σ φ :
- (∀ `{!lrustG Σ}, True ⊢ WP e {{ v, ⌜φ v⌝ }}) →
- adequate NotStuck e σ (λ v _, φ v).
-Proof.
- 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γ).
- iModIntro. iExists (λ σ _, heap_ctx σ). iSplitL.
- { iExists ∅. by iFrame. }
- by iApply (Hwp (LRustG _ _ Hheap)).
-Qed.
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
deleted file mode 100644
index 38b14062..00000000
--- a/theories/lang/heap.v
+++ /dev/null
@@ -1,548 +0,0 @@
-From Coq Require Import Min.
-From stdpp Require Import coPset.
-From iris.algebra Require Import big_op gmap frac agree.
-From iris.algebra Require Import csum excl auth cmra_big_op.
-From iris.bi Require Import fractional.
-From iris.base_logic Require Export lib.own.
-From iris.proofmode Require Export tactics.
-From lrust.lang Require Export lang.
-Set Default Proof Using "Type".
-Import uPred.
-
-Definition lock_stateR : cmraT :=
- csumR (exclR unitC) natR.
-
-Definition heapUR : ucmraT :=
- gmapUR loc (prodR (prodR fracR lock_stateR) (agreeR valC)).
-
-Definition heap_freeableUR : ucmraT :=
- gmapUR block (prodR fracR (gmapR Z (exclR unitC))).
-
-Class heapG Σ := HeapG {
- heap_inG :> inG Σ (authR heapUR);
- heap_freeable_inG :> inG Σ (authR heap_freeableUR);
- heap_name : gname;
- heap_freeable_name : gname
-}.
-
-Definition to_lock_stateR (x : lock_state) : lock_stateR :=
- match x with RSt n => Cinr n | WSt => Cinl (Excl ()) end.
-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).
-
-Section definitions.
- Context `{!heapG Σ}.
-
- Definition heap_mapsto_st (st : lock_state)
- (l : loc) (q : Qp) (v: val) : iProp Σ :=
- own heap_name (◯ {[ l := (q, to_lock_stateR st, to_agree v) ]}).
-
- Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
- heap_mapsto_st (RSt 0) l q v.
- Definition heap_mapsto_aux : seal (@heap_mapsto_def). by eexists. Qed.
- Definition heap_mapsto := unseal heap_mapsto_aux.
- Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
- seal_eq heap_mapsto_aux.
-
- Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
- ([∗ list] i ↦ v ∈ vl, heap_mapsto (l +ₗ i) q v)%I.
-
- Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitC) :=
- match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
-
- Definition heap_freeable_def (l : loc) (q : Qp) (n: nat) : iProp Σ :=
- own heap_freeable_name (◯ {[ l.1 := (q, inter (l.2) n) ]}).
- Definition heap_freeable_aux : seal (@heap_freeable_def). by eexists. Qed.
- Definition heap_freeable := unseal heap_freeable_aux.
- Definition heap_freeable_eq : @heap_freeable = @heap_freeable_def :=
- seal_eq heap_freeable_aux.
-
- 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_mapsto heap_freeable heap_mapsto_vec.
-Instance: Params (@heap_mapsto) 4 := {}.
-Instance: Params (@heap_freeable) 5 := {}.
-
-Notation "l ↦{ q } v" := (heap_mapsto l q v)
- (at level 20, q at level 50, format "l ↦{ q } v") : bi_scope.
-Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : bi_scope.
-
-Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
- (at level 20, q at level 50, format "l ↦∗{ q } vl") : bi_scope.
-Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : bi_scope.
-
-Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
- (at level 20, q at level 50, format "l ↦∗{ q }: P") : bi_scope.
-Notation "l ↦∗: P " := (∃ vl, l ↦∗ vl ∗ P vl)%I
- (at level 20, format "l ↦∗: P") : bi_scope.
-
-Notation "†{ q } l … n" := (heap_freeable l q n)
- (at level 20, q at level 50, format "†{ q } l … n") : bi_scope.
-Notation "† l … n" := (heap_freeable l 1 n) (at level 20) : bi_scope.
-
-Section to_heap.
- Implicit Types σ : state.
-
- Lemma to_heap_valid σ : ✓ to_heap σ.
- Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
-
- Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
- Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
-
- Lemma to_heap_insert σ l x v :
- to_heap (<[l:=(x, v)]> σ)
- = <[l:=(1%Qp, to_lock_stateR x, to_agree v)]> (to_heap σ).
- Proof. by rewrite /to_heap fmap_insert. Qed.
-
- 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 : Timeless (l↦{q}v).
- Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
-
- Global Instance heap_mapsto_fractional l v: Fractional (λ q, l ↦{q} v)%I.
- Proof.
- intros p q.
- by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op agree_idemp.
- Qed.
- Global Instance heap_mapsto_as_fractional l q v:
- AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
- Proof. split. done. apply _. Qed.
-
- Global Instance heap_mapsto_vec_timeless l q vl : Timeless (l ↦∗{q} vl).
- Proof. rewrite /heap_mapsto_vec. apply _. Qed.
-
- Global Instance heap_mapsto_vec_fractional l vl: Fractional (λ q, l ↦∗{q} vl)%I.
- Proof.
- intros p q. rewrite /heap_mapsto_vec -big_sepL_sepL.
- by setoid_rewrite (fractional (Φ := λ q, _ ↦{q} _)%I).
- Qed.
- Global Instance heap_mapsto_vec_as_fractional l q vl:
- AsFractional (l ↦∗{q} vl) (λ q, l ↦∗{q} vl)%I q.
- Proof. split. done. apply _. Qed.
-
- Global Instance heap_freeable_timeless q l n : Timeless (†{q}l…n).
- Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
-
- Lemma heap_mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 ∗ l ↦{q2} v2 ⊢ ⌜v1 = v2⌝.
- Proof.
- rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
- eapply pure_elim; [done|]=> /auth_own_valid /=.
- rewrite op_singleton pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
- Qed.
-
- Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
- Proof. by rewrite /heap_mapsto_vec. Qed.
-
- Lemma heap_mapsto_vec_app l q vl1 vl2 :
- l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ (l +ₗ length vl1) ↦∗{q} vl2.
- Proof.
- rewrite /heap_mapsto_vec big_sepL_app.
- do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
- Qed.
-
- Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
- Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed.
-
- Lemma heap_mapsto_vec_cons l q v vl:
- l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ (l +ₗ 1) ↦∗{q} vl.
- Proof.
- by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
- Qed.
-
- Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
- length vl1 = length vl2 →
- l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ ⌜vl1 = vl2⌝ ∧ l ↦∗{q1+q2} vl1.
- Proof.
- intros Hlen%Forall2_same_length. apply (anti_symm (⊢)).
- - 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 (l +ₗ 1) with "[$Hvl1 $Hvl2]") as "[% $]"; subst.
- rewrite (inj_iff (:: vl2)).
- iDestruct (heap_mapsto_agree with "[$Hv1 $Hv2]") as %<-.
- iSplit; first done. iFrame.
- - by iIntros "[% [$ Hl2]]"; subst.
- Qed.
-
- Lemma heap_mapsto_pred_op l q1 q2 n (Φ : list val → iProp Σ) :
- (∀ vl, Φ vl -∗ ⌜length vl = n⌝) →
- l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, ⌜length vl = n⌝) ⊣⊢ l ↦∗{q1+q2}: Φ.
- Proof.
- intros Hlen. iSplit.
- - iIntros "[Hmt1 Hmt2]".
- iDestruct "Hmt1" as (vl) "[Hmt1 Hown]". iDestruct "Hmt2" as (vl') "[Hmt2 %]".
- iDestruct (Hlen with "Hown") as %?.
- iCombine "Hmt1" "Hmt2" as "Hmt". rewrite heap_mapsto_vec_op; last congruence.
- iDestruct "Hmt" as "[_ Hmt]". iExists vl. by iFrame.
- - iIntros "Hmt". iDestruct "Hmt" as (vl) "[[Hmt1 Hmt2] Hown]".
- iDestruct (Hlen with "Hown") as %?.
- iSplitL "Hmt1 Hown"; iExists _; by iFrame.
- Qed.
-
- Lemma heap_mapsto_pred_wand l q Φ1 Φ2 :
- 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". by iApply "Hwand".
- Qed.
-
- Lemma heap_mapsto_pred_iff_proper l q Φ1 Φ2 :
- □ (∀ vl, Φ1 vl ↔ Φ2 vl) -∗ □ (l ↦∗{q}: Φ1 ↔ l ↦∗{q}: Φ2).
- Proof.
- iIntros "#HΦ !#". iSplit; iIntros; iApply (heap_mapsto_pred_wand with "[-]"); try done; [|];
- iIntros; by iApply "HΦ".
- Qed.
-
- Lemma heap_mapsto_vec_combine l q vl :
- vl ≠ [] →
- l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
- {[l +ₗ i := (q, Cinr 0%nat, to_agree v)]}).
- Proof.
- rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
- by rewrite (big_opL_commute (Auth None)) big_opL_commute1 //.
- Qed.
-
- Global Instance heap_mapsto_pred_fractional l (P : list val → iProp Σ):
- (∀ vl, Persistent (P vl)) → Fractional (λ q, l ↦∗{q}: P)%I.
- Proof.
- intros p q q'. iSplit.
- - iIntros "H". iDestruct "H" as (vl) "[[Hown1 Hown2] #HP]".
- iSplitL "Hown1"; eauto.
- - iIntros "[H1 H2]". iDestruct "H1" as (vl1) "[Hown1 #HP1]".
- iDestruct "H2" as (vl2) "[Hown2 #HP2]".
- set (ll := min (length vl1) (length vl2)).
- rewrite -[vl1](firstn_skipn ll) -[vl2](firstn_skipn ll) 2!heap_mapsto_vec_app.
- iDestruct "Hown1" as "[Hown1 _]". iDestruct "Hown2" as "[Hown2 _]".
- iCombine "Hown1" "Hown2" as "Hown". rewrite heap_mapsto_vec_op; last first.
- { rewrite !firstn_length. subst ll.
- rewrite -!min_assoc min_idempotent min_comm -min_assoc min_idempotent min_comm. done. }
- iDestruct "Hown" as "[H Hown]". iDestruct "H" as %Hl. iExists (take ll vl1). iFrame.
- destruct (min_spec (length vl1) (length vl2)) as [[Hne Heq]|[Hne Heq]].
- + iClear "HP2". rewrite take_ge; last first.
- { rewrite -Heq /ll. done. }
- rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
- + iClear "HP1". rewrite Hl take_ge; last first.
- { rewrite -Heq /ll. done. }
- rewrite drop_ge; first by rewrite app_nil_r. by rewrite -Heq.
- Qed.
- Global Instance heap_mapsto_pred_as_fractional l q (P : list val → iProp Σ):
- (∀ vl, Persistent (P vl)) → AsFractional (l ↦∗{q}: P) (λ q, l ↦∗{q}: P)%I q.
- Proof. split. done. apply _. Qed.
-
- Lemma inter_lookup_Some i j (n : nat):
- i ≤ j < i+n → inter i n !! j = Excl' ().
- Proof.
- revert i. induction n as [|n IH]=>/= i; first lia.
- rewrite lookup_insert_Some. destruct (decide (i = j)); naive_solver lia.
- Qed.
- Lemma inter_lookup_None i j (n : nat):
- j < i ∨ i+n ≤ j → inter i n !! j = None.
- Proof.
- revert i. induction n as [|n IH]=>/= i; first by rewrite lookup_empty.
- rewrite lookup_insert_None. naive_solver lia.
- Qed.
- Lemma inter_op i n n' : inter i n ⋅ inter (i+n) n' ≡ inter i (n+n').
- Proof.
- intros j. rewrite lookup_op.
- destruct (decide (i ≤ j < i+n)); last destruct (decide (i+n ≤ j < i+n+n')).
- - by rewrite (inter_lookup_None (i+n) j n') ?inter_lookup_Some; try lia.
- - by rewrite (inter_lookup_None i j n) ?inter_lookup_Some; try lia.
- - by rewrite !inter_lookup_None; try lia.
- Qed.
- Lemma inter_valid i n : ✓ inter i n.
- Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
-
- Lemma heap_freeable_op_eq l q1 q2 n n' :
- †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
- Proof.
- by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
- op_singleton pair_op inter_op.
- Qed.
-
- (** Properties about heap_freeable_rel and heap_freeable *)
- Lemma heap_freeable_rel_None σ l hF :
- (∀ m : Z, σ !! (l +ₗ m) = None) → heap_freeable_rel σ hF →
- hF !! l.1 = None.
- Proof.
- intros FRESH REL. apply eq_None_not_Some. intros [[q s] [Hsne REL']%REL].
- destruct (map_choose s) as [i []%REL'%not_eq_None_Some]; first done.
- move: (FRESH (i - l.2)). by rewrite /shift_loc Zplus_minus.
- Qed.
-
- Lemma heap_freeable_is_Some σ hF l n i :
- heap_freeable_rel σ hF →
- hF !! l.1 = Some (1%Qp, inter (l.2) n) →
- is_Some (σ !! (l +ₗ i)) ↔ 0 ≤ i ∧ i < n.
- Proof.
- destruct l as [b j]; rewrite /shift_loc /=. intros REL Hl.
- destruct (REL b (1%Qp, inter j n)) as [_ ->]; simpl in *; auto.
- destruct (decide (0 ≤ i ∧ i < n)).
- - rewrite is_Some_alt inter_lookup_Some; lia.
- - rewrite is_Some_alt inter_lookup_None; lia.
- Qed.
-
- Lemma heap_freeable_rel_init_mem l h n σ:
- n ≠ O →
- (∀ m : Z, σ !! (l +ₗ m) = None) →
- heap_freeable_rel σ h →
- heap_freeable_rel (init_mem l n σ)
- (<[l.1 := (1%Qp, inter (l.2) n)]> h).
- Proof.
- move=> Hvlnil FRESH REL blk qs /lookup_insert_Some [[<- <-]|[??]].
- - split.
- { destruct n as [|n]; simpl in *; [done|]. apply: insert_non_empty. }
- intros i. destruct (decide (l.2 ≤ i ∧ i < l.2 + n)).
- + rewrite inter_lookup_Some // lookup_init_mem; naive_solver.
- + rewrite inter_lookup_None; last lia. rewrite lookup_init_mem_ne /=; last lia.
- replace (l.1,i) with (l +ₗ (i - l.2)) by (rewrite /shift_loc; f_equal; lia).
- by rewrite FRESH !is_Some_alt.
- - destruct (REL blk qs) as [? Hs]; auto.
- split; [done|]=> i. by rewrite -Hs lookup_init_mem_ne; last auto.
- Qed.
-
- Lemma heap_freeable_rel_free_mem σ hF n l :
- hF !! l.1 = Some (1%Qp, inter (l.2) n) →
- heap_freeable_rel σ hF →
- heap_freeable_rel (free_mem l n σ) (delete (l.1) hF).
- Proof.
- intros Hl REL b qs; rewrite lookup_delete_Some=> -[NEQ ?].
- destruct (REL b qs) as [? REL']; auto.
- split; [done|]=> i. by rewrite -REL' lookup_free_mem_ne.
- Qed.
-
- Lemma heap_freeable_rel_stable σ h l p :
- heap_freeable_rel σ h → is_Some (σ !! l) →
- heap_freeable_rel (<[l := p]>σ) h.
- Proof.
- intros REL Hσ blk qs Hqs. destruct (REL blk qs) as [? REL']; first done.
- split; [done|]=> i. rewrite -REL' lookup_insert_is_Some.
- destruct (decide (l = (blk, i))); naive_solver.
- Qed.
-
- (** Weakest precondition *)
- Lemma heap_alloc_vs σ l n :
- (∀ m : Z, σ !! (l +ₗ m) = None) →
- own heap_name (● to_heap σ)
- ==∗ own heap_name (● to_heap (init_mem l n σ))
- ∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
- {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]}).
- Proof.
- intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
- revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
- rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
- etrans; first apply (IH (l +ₗ 1)).
- { intros. by rewrite shift_loc_assoc. }
- rewrite shift_loc_0 -insert_singleton_op; last first.
- { rewrite -equiv_None big_opL_commute equiv_None big_opL_None=> l' v' ?.
- rewrite lookup_singleton_None -{2}(shift_loc_0 l). apply not_inj; lia. }
- rewrite to_heap_insert. setoid_rewrite shift_loc_assoc.
- apply alloc_local_update; last done. apply lookup_to_heap_None.
- rewrite lookup_init_mem_ne /=; last lia. by rewrite -(shift_loc_0 l) FRESH.
- Qed.
-
- Lemma heap_alloc σ l n :
- 0 < n →
- (∀ m, σ !! (l +ₗ m) = None) →
- heap_ctx σ ==∗
- heap_ctx (init_mem l (Z.to_nat n) σ) ∗ †l…(Z.to_nat n) ∗
- l ↦∗ repeat (LitV LitPoison) (Z.to_nat n).
- Proof.
- intros ??; iDestruct 1 as (hF) "(Hvalσ & HhF & %)".
- assert (Z.to_nat n ≠ O). { rewrite -(Nat2Z.id 0)=>/Z2Nat.inj. lia. }
- iMod (heap_alloc_vs _ _ (Z.to_nat n) 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. }
- iModIntro. iSplitL "Hvalσ HhF".
- { iExists _. iFrame. iPureIntro.
- auto using heap_freeable_rel_init_mem. }
- rewrite heap_freeable_eq /heap_freeable_def heap_mapsto_vec_combine //.
- iFrame. destruct (Z.to_nat n); done.
- Qed.
-
- Lemma heap_free_vs σ l vl :
- own heap_name (● to_heap σ) ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
- {[l +ₗ i := (1%Qp, Cinr 0%nat, to_agree v)]})
- ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
- Proof.
- rewrite -own_op. apply own_update, auth_update_dealloc.
- revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
- rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
- apply local_update_total_valid=> _ Hvalid _.
- assert (([^op list] k↦y ∈ vl,
- {[l +ₗ (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
- { move: (Hvalid l). rewrite lookup_op lookup_singleton.
- by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
- rewrite -insert_singleton_op //. etrans.
- { apply (delete_local_update _ _ l (1%Qp, Cinr 0%nat, to_agree v)).
- by rewrite lookup_insert. }
- rewrite delete_insert // -to_heap_delete delete_free_mem.
- setoid_rewrite <-shift_loc_assoc. apply IH.
- Qed.
-
- Lemma heap_free σ l vl (n : Z) :
- n = length vl →
- heap_ctx σ -∗ l ↦∗ vl -∗ †l…(length vl)
- ==∗ ⌜0 < n⌝ ∗ ⌜∀ m, is_Some (σ !! (l +ₗ m)) ↔ (0 ≤ m < n)⌝ ∗
- heap_ctx (free_mem l (Z.to_nat n) σ).
- Proof.
- 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.
- { move: (Hv (l.1)). rewrite Hl. by intros [??]. }
- assert (vl ≠ []).
- { intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
- assert (0 < n) by (subst n; by destruct vl).
- 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 _ _ _). }
- 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 :
- own heap_name (● to_heap σ) -∗
- own heap_name (◯ {[ l := (q, to_lock_stateR ls, to_agree v) ]}) -∗
- ⌜∃ n' : nat,
- σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v)⌝.
- Proof.
- iIntros "H● H◯".
- iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
- iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
- rewrite /to_heap lookup_fmap fmap_Some_equiv.
- move=> [[[ls'' v'] [?[[/=??]->]]]]; simplify_eq.
- move=> /Some_pair_included_total_2
- [/Some_pair_included [_ Hincl] /to_agree_included->].
- destruct ls as [|n], ls'' as [|n''],
- Hincl as [[[|n'|]|] [=]%leibniz_equiv]; subst.
- by exists O. eauto. exists O. by rewrite Nat.add_0_r.
- Qed.
-
- 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)⌝.
- Proof.
- iIntros "H● H◯".
- iDestruct (own_valid_2 with "H● H◯") as %[Hl?]%auth_valid_discrete_2.
- iPureIntro. move: Hl=> /singleton_included [[[q' ls'] dv]].
- rewrite /to_heap lookup_fmap fmap_Some_equiv.
- move=> [[[ls'' v'] [?[[/=??]->]]] Hincl]; simplify_eq.
- apply (Some_included_exclusive _ _) in Hincl as [? Hval]; last by destruct ls''.
- apply (inj to_agree) in Hval. fold_leibniz. subst.
- destruct ls, ls''; rewrite ?Nat.add_0_r; naive_solver.
- 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 (<[l:=(RSt (n2 + nf), v)]> σ))
- ∗ heap_mapsto_st (RSt n2) l q v.
- Proof.
- intros Hσv. apply 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 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 (<[l:=(st2, v')]> σ))
- ∗ heap_mapsto_st st2 l 1%Qp v'.
- Proof.
- intros Hσv. apply 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 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/lang.v b/theories/lang/lang.v
deleted file mode 100644
index c302a1c3..00000000
--- a/theories/lang/lang.v
+++ /dev/null
@@ -1,660 +0,0 @@
-From iris.program_logic Require Export language ectx_language ectxi_language.
-From stdpp Require Export strings.
-From stdpp Require Import gmap.
-Set Default Proof Using "Type".
-
-Open Scope Z_scope.
-
-(** Expressions and vals. *)
-Definition block : Set := positive.
-Definition loc : Set := block * Z.
-
-Bind Scope loc_scope with loc.
-Delimit Scope loc_scope with L.
-Open Scope loc_scope.
-
-Inductive base_lit : Set :=
-| LitPoison | LitLoc (l : loc) | LitInt (n : Z).
-Inductive bin_op : Set :=
-| PlusOp | MinusOp | LeOp | EqOp | OffsetOp.
-Inductive order : Set :=
-| ScOrd | Na1Ord | Na2Ord.
-
-Inductive binder := BAnon | BNamed : string → binder.
-Delimit Scope lrust_binder_scope with RustB.
-Bind Scope lrust_binder_scope with binder.
-
-Notation "[ ]" := (@nil binder) : lrust_binder_scope.
-Notation "a :: b" := (@cons binder a%RustB b%RustB)
- (at level 60, right associativity) : lrust_binder_scope.
-Notation "[ x1 ; x2 ; .. ; xn ]" :=
- (@cons binder x1%RustB (@cons binder x2%RustB
- (..(@cons binder xn%RustB (@nil binder))..))) : lrust_binder_scope.
-Notation "[ x ]" := (@cons binder x%RustB (@nil binder)) : lrust_binder_scope.
-
-Definition cons_binder (mx : binder) (X : list string) : list string :=
- match mx with BAnon => X | BNamed x => x :: X end.
-Infix ":b:" := cons_binder (at level 60, right associativity).
-Fixpoint app_binder (mxl : list binder) (X : list string) : list string :=
- match mxl with [] => X | b :: mxl => b :b: app_binder mxl X end.
-Infix "+b+" := app_binder (at level 60, right associativity).
-Instance binder_dec_eq : EqDecision binder.
-Proof. solve_decision. Defined.
-
-Instance set_unfold_cons_binder x mx X P :
- SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
-Proof.
- constructor. rewrite -(set_unfold (x ∈ X) P).
- destruct mx; rewrite /= ?elem_of_cons; naive_solver.
-Qed.
-Instance set_unfold_app_binder x mxl X P :
- SetUnfold (x ∈ X) P → SetUnfold (x ∈ mxl +b+ X) (BNamed x ∈ mxl ∨ P).
-Proof.
- constructor. rewrite -(set_unfold (x ∈ X) P).
- induction mxl as [|?? IH]; set_solver.
-Qed.
-
-Inductive expr :=
-| Var (x : string)
-| Lit (l : base_lit)
-| Rec (f : binder) (xl : list binder) (e : expr)
-| BinOp (op : bin_op) (e1 e2 : expr)
-| App (e : expr) (el : list expr)
-| Read (o : order) (e : expr)
-| Write (o : order) (e1 e2: expr)
-| CAS (e0 e1 e2 : expr)
-| Alloc (e : expr)
-| Free (e1 e2 : expr)
-| Case (e : expr) (el : list expr)
-| Fork (e : expr).
-
-Arguments App _%E _%E.
-Arguments Case _%E _%E.
-
-Fixpoint is_closed (X : list string) (e : expr) : bool :=
- match e with
- | Var x => bool_decide (x ∈ X)
- | Lit _ => true
- | Rec f xl e => is_closed (f :b: xl +b+ X) e
- | BinOp _ e1 e2 | Write _ e1 e2 | Free e1 e2 =>
- is_closed X e1 && is_closed X e2
- | App e el | Case e el => is_closed X e && forallb (is_closed X) el
- | Read _ e | Alloc e | Fork e => is_closed X e
- | CAS e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2
- end.
-
-Class Closed (X : list string) (e : expr) := closed : is_closed X e.
-Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
-Proof. rewrite /Closed. apply _. Qed.
-Instance closed_decision env e : Decision (Closed env e).
-Proof. rewrite /Closed. apply _. Qed.
-
-Inductive val :=
-| LitV (l : base_lit)
-| RecV (f : binder) (xl : list binder) (e : expr) `{!Closed (f :b: xl +b+ []) e}.
-
-Bind Scope val_scope with val.
-
-Definition of_val (v : val) : expr :=
- match v with
- | RecV f x e => Rec f x e
- | LitV l => Lit l
- end.
-
-Definition to_val (e : expr) : option val :=
- match e with
- | Rec f xl e =>
- if decide (Closed (f :b: xl +b+ []) e) then Some (RecV f xl e) else None
- | Lit l => Some (LitV l)
- | _ => None
- end.
-
-(** The state: heaps of vals*lockstate. *)
-Inductive lock_state :=
-| WSt | RSt (n : nat).
-Definition state := gmap loc (lock_state * val).
-
-(** Evaluation contexts *)
-Inductive ectx_item :=
-| BinOpLCtx (op : bin_op) (e2 : expr)
-| BinOpRCtx (op : bin_op) (v1 : val)
-| AppLCtx (e2 : list expr)
-| AppRCtx (v : val) (vl : list val) (el : list expr)
-| ReadCtx (o : order)
-| WriteLCtx (o : order) (e2 : expr)
-| WriteRCtx (o : order) (v1 : val)
-| CasLCtx (e1 e2: expr)
-| CasMCtx (v0 : val) (e2 : expr)
-| CasRCtx (v0 : val) (v1 : val)
-| AllocCtx
-| FreeLCtx (e2 : expr)
-| FreeRCtx (v1 : val)
-| CaseCtx (el : list expr).
-
-Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
- match Ki with
- | BinOpLCtx op e2 => BinOp op e e2
- | BinOpRCtx op v1 => BinOp op (of_val v1) e
- | AppLCtx e2 => App e e2
- | AppRCtx v vl el => App (of_val v) ((of_val <$> vl) ++ e :: el)
- | ReadCtx o => Read o e
- | WriteLCtx o e2 => Write o e e2
- | WriteRCtx o v1 => Write o (of_val v1) e
- | CasLCtx e1 e2 => CAS e e1 e2
- | CasMCtx v0 e2 => CAS (of_val v0) e e2
- | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
- | AllocCtx => Alloc e
- | FreeLCtx e2 => Free e e2
- | FreeRCtx v1 => Free (of_val v1) e
- | CaseCtx el => Case e el
- end.
-
-(** Substitution *)
-Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
- match e with
- | Var y => if bool_decide (y = x) then es else Var y
- | Lit l => Lit l
- | Rec f xl e =>
- Rec f xl $ if bool_decide (BNamed x ≠ f ∧ BNamed x ∉ xl) then subst x es e else e
- | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
- | App e el => App (subst x es e) (map (subst x es) el)
- | Read o e => Read o (subst x es e)
- | Write o e1 e2 => Write o (subst x es e1) (subst x es e2)
- | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
- | Alloc e => Alloc (subst x es e)
- | Free e1 e2 => Free (subst x es e1) (subst x es e2)
- | Case e el => Case (subst x es e) (map (subst x es) el)
- | Fork e => Fork (subst x es e)
- end.
-
-Definition subst' (mx : binder) (es : expr) : expr → expr :=
- match mx with BNamed x => subst x es | BAnon => id end.
-
-Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
- match xl, esl with
- | [], [] => Some e
- | x::xl, es::esl => subst' x es <$> subst_l xl esl e
- | _, _ => None
- end.
-Arguments subst_l _%RustB _ _%E.
-
-Definition subst_v (xl : list binder) (vsl : vec val (length xl))
- (e : expr) : expr :=
- Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
-Arguments subst_v _%RustB _ _%E.
-
-Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
- Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
-Proof.
- revert vsl. induction xl=>/= vsl; inv_vec vsl=>//=v vsl. by rewrite -IHxl.
-Qed.
-
-(** The stepping relation *)
-(* Be careful to make sure that poison is always stuck when used for anything
- except for reading from or writing to memory! *)
-Definition Z_of_bool (b : bool) : Z :=
- if b then 1 else 0.
-
-Definition lit_of_bool (b : bool) : base_lit :=
- LitInt $ Z_of_bool b.
-
-Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
-
-Notation "l +ₗ z" := (shift_loc l%L z%Z)
- (at level 50, left associativity) : loc_scope.
-
-Fixpoint init_mem (l:loc) (n:nat) (σ:state) : state :=
- match n with
- | O => σ
- | S n => <[l:=(RSt 0, LitV LitPoison)]>(init_mem (l +ₗ 1) n σ)
- end.
-
-Fixpoint free_mem (l:loc) (n:nat) (σ:state) : state :=
- match n with
- | O => σ
- | S n => delete l (free_mem (l +ₗ 1) n σ)
- end.
-
-Inductive lit_eq (σ : state) : base_lit → base_lit → Prop :=
-(* No refl case for poison *)
-| IntRefl z : lit_eq σ (LitInt z) (LitInt z)
-| LocRefl l : lit_eq σ (LitLoc l) (LitLoc l)
-(* Comparing unallocated pointers can non-deterministically say they are equal
- even if they are not. Given that our `free` actually makes addresses
- re-usable, this may not be strictly necessary, but it is the most
- conservative choice that avoids UB (and we cannot use UB as this operation is
- possible in safe Rust). See
- <https://internals.rust-lang.org/t/comparing-dangling-pointers/3019> for some
- more background. *)
-| LocUnallocL l1 l2 :
- σ !! l1 = None →
- lit_eq σ (LitLoc l1) (LitLoc l2)
-| LocUnallocR l1 l2 :
- σ !! l2 = None →
- lit_eq σ (LitLoc l1) (LitLoc l2).
-
-Inductive lit_neq : base_lit → base_lit → Prop :=
-| IntNeq z1 z2 :
- z1 ≠ z2 → lit_neq (LitInt z1) (LitInt z2)
-| LocNeq l1 l2 :
- l1 ≠ l2 → lit_neq (LitLoc l1) (LitLoc l2)
-| LocNeqNullR l :
- lit_neq (LitLoc l) (LitInt 0)
-| LocNeqNullL l :
- lit_neq (LitInt 0) (LitLoc l).
-
-Inductive bin_op_eval (σ : state) : bin_op → base_lit → base_lit → base_lit → Prop :=
-| BinOpPlus z1 z2 :
- bin_op_eval σ PlusOp (LitInt z1) (LitInt z2) (LitInt (z1 + z2))
-| BinOpMinus z1 z2 :
- bin_op_eval σ MinusOp (LitInt z1) (LitInt z2) (LitInt (z1 - z2))
-| BinOpLe z1 z2 :
- bin_op_eval σ LeOp (LitInt z1) (LitInt z2) (lit_of_bool $ bool_decide (z1 ≤ z2))
-| BinOpEqTrue l1 l2 :
- lit_eq σ l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool true)
-| BinOpEqFalse l1 l2 :
- lit_neq l1 l2 → bin_op_eval σ EqOp l1 l2 (lit_of_bool false)
-| BinOpOffset l z :
- bin_op_eval σ OffsetOp (LitLoc l) (LitInt z) (LitLoc $ l +ₗ z).
-
-Definition stuck_term := App (Lit $ LitInt 0) [].
-
-Inductive head_step : expr → state → list Empty_set → expr → state → list expr → Prop :=
-| BinOpS op l1 l2 l' σ :
- bin_op_eval σ op l1 l2 l' →
- head_step (BinOp op (Lit l1) (Lit l2)) σ [] (Lit l') σ []
-| BetaS f xl e e' el σ:
- Forall (λ ei, is_Some (to_val ei)) el →
- Closed (f :b: xl +b+ []) e →
- subst_l (f::xl) (Rec f xl e :: el) e = Some e' →
- head_step (App (Rec f xl e) el) σ [] e' σ []
-| ReadScS l n v σ:
- σ !! l = Some (RSt n, v) →
- head_step (Read ScOrd (Lit $ LitLoc l)) σ [] (of_val v) σ []
-| ReadNa1S l n v σ:
- σ !! l = Some (RSt n, v) →
- head_step (Read Na1Ord (Lit $ LitLoc l)) σ
- []
- (Read Na2Ord (Lit $ LitLoc l)) (<[l:=(RSt $ S n, v)]>σ)
- []
-| ReadNa2S l n v σ:
- σ !! l = Some (RSt $ S n, v) →
- head_step (Read Na2Ord (Lit $ LitLoc l)) σ
- []
- (of_val v) (<[l:=(RSt n, v)]>σ)
- []
-| WriteScS l e v v' σ:
- to_val e = Some v →
- σ !! l = Some (RSt 0, v') →
- head_step (Write ScOrd (Lit $ LitLoc l) e) σ
- []
- (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
- []
-| WriteNa1S l e v v' σ:
- to_val e = Some v →
- σ !! l = Some (RSt 0, v') →
- head_step (Write Na1Ord (Lit $ LitLoc l) e) σ
- []
- (Write Na2Ord (Lit $ LitLoc l) e) (<[l:=(WSt, v')]>σ)
- []
-| WriteNa2S l e v v' σ:
- to_val e = Some v →
- σ !! l = Some (WSt, v') →
- head_step (Write Na2Ord (Lit $ LitLoc l) e) σ
- []
- (Lit LitPoison) (<[l:=(RSt 0, v)]>σ)
- []
-| CasFailS l n e1 lit1 e2 lit2 litl σ :
- to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
- σ !! l = Some (RSt n, LitV litl) →
- lit_neq lit1 litl →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ [] (Lit $ lit_of_bool false) σ []
-| CasSucS l e1 lit1 e2 lit2 litl σ :
- to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
- σ !! l = Some (RSt 0, LitV litl) →
- lit_eq σ lit1 litl →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ
- []
- (Lit $ lit_of_bool true) (<[l:=(RSt 0, LitV lit2)]>σ)
- []
-(* A succeeding CAS has to detect concurrent non-atomic read accesses, and
- trigger UB if there is one. In lambdaRust, succeeding and failing CAS are
- not mutually exclusive, so it could happen that a CAS can both fail (and
- hence not be stuck) but also succeed (and hence be racing with a concurrent
- non-atomic read). In that case, we have to explicitly reduce to a stuck
- state; due to the possibility of failing CAS, we cannot rely on the current
- state being stuck like we could in a language where failing and succeeding
- CAS are mutually exclusive.
-
- This means that CAS is atomic (it always reducs to an irreducible
- expression), but not strongly atomic (it does not always reduce to a value).
-
- If there is a concurrent non-atomic write, the CAS itself is stuck: All its
- reductions are blocked. *)
-| CasStuckS l n e1 lit1 e2 lit2 litl σ :
- to_val e1 = Some $ LitV lit1 → to_val e2 = Some $ LitV lit2 →
- σ !! l = Some (RSt n, LitV litl) → 0 < n →
- lit_eq σ lit1 litl →
- head_step (CAS (Lit $ LitLoc l) e1 e2) σ
- []
- stuck_term σ
- []
-| AllocS n l σ :
- 0 < n →
- (∀ m, σ !! (l +ₗ m) = None) →
- head_step (Alloc $ Lit $ LitInt n) σ
- []
- (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ)
- []
-| FreeS n l σ :
- 0 < n →
- (∀ m, is_Some (σ !! (l +ₗ m)) ↔ 0 ≤ m < n) →
- head_step (Free (Lit $ LitInt n) (Lit $ LitLoc l)) σ
- []
- (Lit LitPoison) (free_mem l (Z.to_nat n) σ)
- []
-| CaseS i el e σ :
- 0 ≤ i →
- el !! (Z.to_nat i) = Some e →
- head_step (Case (Lit $ LitInt i) el) σ [] e σ []
-| ForkS e σ:
- head_step (Fork e) σ [] (Lit LitPoison) σ [e].
-
-(** Basic properties about the language *)
-Lemma to_of_val v : to_val (of_val v) = Some v.
-Proof.
- by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
-Qed.
-
-Lemma of_to_val e v : to_val e = Some v → of_val v = e.
-Proof.
- revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
-Qed.
-
-Instance of_val_inj : Inj (=) (=) of_val.
-Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
-
-Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
-Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
-
-Lemma fill_item_val Ki e :
- is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
-Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
-
-Lemma val_stuck e1 σ1 κ e2 σ2 ef :
- head_step e1 σ1 κ e2 σ2 ef → to_val e1 = None.
-Proof. destruct 1; naive_solver. Qed.
-
-Lemma head_ctx_step_val Ki e σ1 κ e2 σ2 ef :
- head_step (fill_item Ki e) σ1 κ e2 σ2 ef → is_Some (to_val e).
-Proof.
- destruct Ki; inversion_clear 1; decompose_Forall_hyps;
- simplify_option_eq; by eauto.
-Qed.
-
-Lemma list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2 :
- to_val e1 = None → to_val e2 = None →
- map of_val vl1 ++ e1 :: el1 = map of_val vl2 ++ e2 :: el2 →
- vl1 = vl2 ∧ el1 = el2.
-Proof.
- revert vl2; induction vl1; destruct vl2; intros H1 H2; inversion 1.
- - done.
- - subst. by rewrite to_of_val in H1.
- - subst. by rewrite to_of_val in H2.
- - destruct (IHvl1 vl2); auto. split; f_equal; auto. by apply (inj of_val).
-Qed.
-
-Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
- to_val e1 = None → to_val e2 = None →
- fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
-Proof.
- destruct Ki1 as [| | |v1 vl1 el1| | | | | | | | | |],
- Ki2 as [| | |v2 vl2 el2| | | | | | | | | |];
- intros He1 He2 EQ; try discriminate; simplify_eq/=;
- repeat match goal with
- | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
- end; auto.
- destruct (list_expr_val_eq_inv vl1 vl2 e1 e2 el1 el2); auto. congruence.
-Qed.
-
-Lemma shift_loc_assoc l n n' : l +ₗ n +ₗ n' = l +ₗ (n + n').
-Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0 l : l +ₗ 0 = l.
-Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
-
-Lemma shift_loc_assoc_nat l (n n' : nat) : l +ₗ n +ₗ n' = l +ₗ (n + n')%nat.
-Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
-Lemma shift_loc_0_nat l : l +ₗ 0%nat = l.
-Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
-
-Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
-Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
-
-Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
-Proof. done. Qed.
-
-Lemma lookup_init_mem σ (l l' : loc) (n : nat) :
- l.1 = l'.1 → l.2 ≤ l'.2 < l.2 + n →
- init_mem l n σ !! l' = Some (RSt 0, LitV LitPoison).
-Proof.
- intros ?. destruct l' as [? l']; simplify_eq/=.
- revert l. induction n as [|n IH]=> /= l Hl; [lia|].
- assert (l' = l.2 ∨ l.2 + 1 ≤ l') as [->|?] by lia.
- { by rewrite -surjective_pairing lookup_insert. }
- rewrite lookup_insert_ne; last by destruct l; intros ?; simplify_eq/=; lia.
- rewrite -(shift_loc_block l 1) IH /=; last lia. done.
-Qed.
-
-Lemma lookup_init_mem_ne σ (l l' : loc) (n : nat) :
- l.1 ≠ l'.1 ∨ l'.2 < l.2 ∨ l.2 + n ≤ l'.2 →
- init_mem l n σ !! l' = σ !! l'.
-Proof.
- revert l. induction n as [|n IH]=> /= l Hl; auto.
- rewrite -(IH (l +ₗ 1)); last (simpl; intuition lia).
- apply lookup_insert_ne. intros ->; intuition lia.
-Qed.
-
-Definition fresh_block (σ : state) : block :=
- let loclst : list loc := elements (dom _ σ : gset loc) in
- let blockset : gset block := foldr (λ l, ({[l.1]} ∪)) ∅ loclst in
- fresh blockset.
-
-Lemma is_fresh_block σ i : σ !! (fresh_block σ,i) = None.
-Proof.
- assert (∀ (l : loc) ls (X : gset block),
- l ∈ ls → l.1 ∈ foldr (λ l, ({[l.1]} ∪)) X ls) as help.
- { induction 1; set_solver. }
- rewrite /fresh_block /shift_loc /= -(not_elem_of_dom (D := gset loc)) -elem_of_elements.
- move=> /(help _ _ ∅) /=. apply is_fresh.
-Qed.
-
-Lemma alloc_fresh n σ :
- let l := (fresh_block σ, 0) in
- let init := repeat (LitV $ LitInt 0) (Z.to_nat n) in
- 0 < n →
- head_step (Alloc $ Lit $ LitInt n) σ [] (Lit $ LitLoc l) (init_mem l (Z.to_nat n) σ) [].
-Proof.
- intros l init Hn. apply AllocS. auto.
- - intros i. apply (is_fresh_block _ i).
-Qed.
-
-Lemma lookup_free_mem_ne σ l l' n : l.1 ≠ l'.1 → free_mem l n σ !! l' = σ !! l'.
-Proof.
- revert l. induction n as [|n IH]=> l ? //=.
- rewrite lookup_delete_ne; last congruence.
- apply IH. by rewrite shift_loc_block.
-Qed.
-
-Lemma delete_free_mem σ l l' n :
- delete l (free_mem l' n σ) = free_mem l' n (delete l σ).
-Proof.
- revert l'. induction n as [|n IH]=> l' //=. by rewrite delete_commute IH.
-Qed.
-
-(** Closed expressions *)
-Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
-Proof.
- revert e X Y. fix FIX 1; destruct e=>X Y/=; try naive_solver.
- - naive_solver set_solver.
- - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
- induction el=>/=; naive_solver.
- - rewrite !andb_True. intros [He Hel] HXY. split. by eauto.
- induction el=>/=; naive_solver.
-Qed.
-
-Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
-Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
-
-Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
-Proof.
- revert e X. fix FIX 1; destruct e=> X /=; rewrite ?bool_decide_spec ?andb_True=> He ?;
- repeat case_bool_decide; simplify_eq/=; f_equal;
- try by intuition eauto with set_solver.
- - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
- f_equal; intuition eauto with set_solver.
- - case He=> _. clear He. induction el=>//=. rewrite andb_True=>?.
- f_equal; intuition eauto with set_solver.
-Qed.
-
-Lemma is_closed_nil_subst e x es : is_closed [] e → subst x es e = e.
-Proof. intros. apply is_closed_subst with []; set_solver. Qed.
-
-Lemma is_closed_of_val X v : is_closed X (of_val v).
-Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
-
-Lemma is_closed_to_val X e v : to_val e = Some v → is_closed X e.
-Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
-
-Lemma subst_is_closed X x es e :
- is_closed X es → is_closed (x::X) e → is_closed X (subst x es e).
-Proof.
- revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
- try naive_solver; rewrite ?andb_True; intros.
- - set_solver.
- - eauto using is_closed_weaken with set_solver.
- - eapply is_closed_weaken; first done.
- destruct (decide (BNamed x = f)), (decide (BNamed x ∈ xl)); set_solver.
- - split; first naive_solver. induction el; naive_solver.
- - split; first naive_solver. induction el; naive_solver.
-Qed.
-
-Lemma subst'_is_closed X b es e :
- is_closed X es → is_closed (b:b:X) e → is_closed X (subst' b es e).
-Proof. destruct b; first done. apply subst_is_closed. Qed.
-
-(* Operations on literals *)
-Lemma lit_eq_state σ1 σ2 l1 l2 :
- (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
- lit_eq σ1 l1 l2 → lit_eq σ2 l1 l2.
-Proof. intros Heq. inversion 1; econstructor; eauto; eapply Heq; done. Qed.
-
-Lemma bin_op_eval_state σ1 σ2 op l1 l2 l' :
- (∀ l, σ1 !! l = None ↔ σ2 !! l = None) →
- bin_op_eval σ1 op l1 l2 l' → bin_op_eval σ2 op l1 l2 l'.
-Proof.
- intros Heq. inversion 1; econstructor; eauto using lit_eq_state.
-Qed.
-
-(* Misc *)
-Lemma stuck_not_head_step σ e' κ σ' ef :
- ¬head_step stuck_term σ e' κ σ' ef.
-Proof. inversion 1. Qed.
-
-(** Equality and other typeclass stuff *)
-Instance base_lit_dec_eq : EqDecision base_lit.
-Proof. solve_decision. Defined.
-Instance bin_op_dec_eq : EqDecision bin_op.
-Proof. solve_decision. Defined.
-Instance un_op_dec_eq : EqDecision order.
-Proof. solve_decision. Defined.
-
-Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
- let fix expr_list_beq el el' :=
- match el, el' with
- | [], [] => true
- | eh::eq, eh'::eq' => expr_beq eh eh' && expr_list_beq eq eq'
- | _, _ => false
- end
- in
- match e, e' with
- | Var x, Var x' => bool_decide (x = x')
- | Lit l, Lit l' => bool_decide (l = l')
- | Rec f xl e, Rec f' xl' e' =>
- bool_decide (f = f') && bool_decide (xl = xl') && expr_beq e e'
- | BinOp op e1 e2, BinOp op' e1' e2' =>
- bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
- | App e el, App e' el' | Case e el, Case e' el' =>
- expr_beq e e' && expr_list_beq el el'
- | Read o e, Read o' e' => bool_decide (o = o') && expr_beq e e'
- | Write o e1 e2, Write o' e1' e2' =>
- bool_decide (o = o') && expr_beq e1 e1' && expr_beq e2 e2'
- | CAS e0 e1 e2, CAS e0' e1' e2' =>
- expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
- | Alloc e, Alloc e' | Fork e, Fork e' => expr_beq e e'
- | Free e1 e2, Free e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
- | _, _ => false
- end.
-Lemma expr_beq_correct (e1 e2 : expr) : expr_beq e1 e2 ↔ e1 = e2.
-Proof.
- revert e1 e2; fix FIX 1.
- destruct e1 as [| | | |? el1| | | | | |? el1|],
- e2 as [| | | |? el2| | | | | |? el2|]; simpl; try done;
- rewrite ?andb_True ?bool_decide_spec ?FIX;
- try (split; intro; [destruct_and?|split_and?]; congruence).
- - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
- { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
- specialize (FIX el1h). naive_solver. }
- clear FIX. naive_solver.
- - match goal with |- context [?F el1 el2] => assert (F el1 el2 ↔ el1 = el2) end.
- { revert el2. induction el1 as [|el1h el1q]; destruct el2; try done.
- specialize (FIX el1h). naive_solver. }
- clear FIX. naive_solver.
-Qed.
-Instance expr_dec_eq : EqDecision expr.
-Proof.
- refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
-Defined.
-Instance val_dec_eq : EqDecision val.
-Proof.
- refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
-Defined.
-
-Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
-Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
-
-Canonical Structure stateC := leibnizC state.
-Canonical Structure valC := leibnizC val.
-Canonical Structure exprC := leibnizC expr.
-
-(** Language *)
-Lemma lrust_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
-Proof.
- split; apply _ || eauto using to_of_val, of_to_val,
- val_stuck, fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
-Qed.
-Canonical Structure lrust_ectxi_lang := EctxiLanguage lrust_lang_mixin.
-Canonical Structure lrust_ectx_lang := EctxLanguageOfEctxi lrust_ectxi_lang.
-Canonical Structure lrust_lang := LanguageOfEctx lrust_ectx_lang.
-
-(* Lemmas about the language. *)
-Lemma stuck_irreducible K σ : irreducible (fill K stuck_term) σ.
-Proof.
- apply: (irreducible_fill (K:=ectx_language.fill K)); first done.
- apply prim_head_irreducible; unfold stuck_term.
- - inversion 1.
- - apply ectxi_language_sub_redexes_are_values.
- intros [] ??; simplify_eq/=; eauto; discriminate_list.
-Qed.
-
-(* Define some derived forms *)
-Notation Lam xl e := (Rec BAnon xl e) (only parsing).
-Notation Let x e1 e2 := (App (Lam [x] e2) [e1]) (only parsing).
-Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing).
-Notation LamV xl e := (RecV BAnon xl e) (only parsing).
-Notation LetCtx x e2 := (AppRCtx (LamV [x] e2) [] []).
-Notation SeqCtx e2 := (LetCtx BAnon e2).
-Notation Skip := (Seq (Lit LitPoison) (Lit LitPoison)).
-Coercion lit_of_bool : bool >-> base_lit.
-Notation If e0 e1 e2 := (Case e0 (@cons expr e2 (@cons expr e1 (@nil expr)))) (only parsing).
-Notation Newlft := (Lit LitPoison) (only parsing).
-Notation Endlft := Skip (only parsing).
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
deleted file mode 100644
index 4bac7690..00000000
--- a/theories/lang/lifting.v
+++ /dev/null
@@ -1,377 +0,0 @@
-From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import ectx_lifting.
-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.
-
-Class lrustG Σ := LRustG {
- lrustG_invG : invG Σ;
- lrustG_gen_heapG :> heapG Σ
-}.
-
-Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
- iris_invG := lrustG_invG;
- state_interp σ κs _ := heap_ctx σ;
- fork_post _ := True%I;
-}.
-Global Opaque iris_invG.
-
-Ltac inv_lit :=
- repeat match goal with
- | H : lit_eq _ ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
- | H : lit_neq ?x ?y |- _ => inversion H; clear H; simplify_map_eq/=
- end.
-
-Ltac inv_bin_op_eval :=
- repeat match goal with
- | H : bin_op_eval _ ?c _ _ _ |- _ => is_constructor c; inversion H; clear H; simplify_eq/=
- end.
-
-Local Hint Extern 0 (atomic _) => solve_atomic.
-Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
-
-Local Hint Constructors head_step bin_op_eval lit_neq lit_eq.
-Local Hint Resolve alloc_fresh.
-Local Hint Resolve to_of_val.
-
-Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
- as_rec : e = Rec f xl erec.
-Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
-Instance AsRec_rec_locked_val v f xl e :
- AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
-Proof. by unlock. Qed.
-
-Class DoSubst (x : binder) (es : expr) (e er : expr) :=
- do_subst : subst' x es e = er.
-Hint Extern 0 (DoSubst _ _ _ _) =>
- rewrite /DoSubst; simpl_subst; reflexivity : typeclass_instances.
-
-Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
- do_subst_l : subst_l xl esl e = Some er.
-Instance do_subst_l_nil e : DoSubstL [] [] e e.
-Proof. done. Qed.
-Instance do_subst_l_cons x xl es esl e er er' :
- DoSubstL xl esl e er' → DoSubst x es er' er →
- DoSubstL (x :: xl) (es :: esl) e er.
-Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
-Instance do_subst_vec xl (vsl : vec val (length xl)) e :
- DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
-Proof. by rewrite /DoSubstL subst_v_eq. Qed.
-
-Section lifting.
-Context `{!lrustG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types e : expr.
-Implicit Types ef : option expr.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e :
- {{{ ▷ WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitPoison; True }}}.
-Proof.
- iIntros (?) "?HΦ". iApply wp_lift_atomic_head_step; [done|].
- iIntros (σ1 κ κs n) "Hσ !>"; iSplit; first by eauto.
- iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iFrame.
- iModIntro. by iApply "HΦ".
-Qed.
-
-(** Pure reductions *)
-Local Ltac solve_exec_safe :=
- intros; destruct_and?; subst; do 3 eexists; econstructor; simpl; eauto with lia.
-Local Ltac solve_exec_puredet :=
- simpl; intros; destruct_and?; inv_head_step; inv_bin_op_eval; inv_lit; done.
-Local Ltac solve_pure_exec :=
- intros ?; apply nsteps_once, pure_head_step_pure_step;
- constructor; [solve_exec_safe | solve_exec_puredet].
-
-Global Instance pure_rec e f xl erec erec' el :
- AsRec e f xl erec →
- TCForall AsVal el →
- Closed (f :b: xl +b+ []) erec →
- DoSubstL (f :: xl) (e :: el) erec erec' →
- PureExec True 1 (App e el) erec'.
-Proof.
- rewrite /AsRec /DoSubstL=> -> /TCForall_Forall Hel ??. solve_pure_exec.
- eapply Forall_impl; [exact Hel|]. intros e' [v <-]. rewrite to_of_val; eauto.
-Qed.
-
-Global Instance pure_le n1 n2 :
- PureExec True 1 (BinOp LeOp (Lit (LitInt n1)) (Lit (LitInt n2)))
- (Lit (bool_decide (n1 ≤ n2))).
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_eq_int n1 n2 :
- PureExec True 1 (BinOp EqOp (Lit (LitInt n1)) (Lit (LitInt n2))) (Lit (bool_decide (n1 = n2))).
-Proof. case_bool_decide; solve_pure_exec. Qed.
-
-Global Instance pure_eq_loc_0_r l :
- PureExec True 1 (BinOp EqOp (Lit (LitLoc l)) (Lit (LitInt 0))) (Lit false).
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_eq_loc_0_l l :
- PureExec True 1 (BinOp EqOp (Lit (LitInt 0)) (Lit (LitLoc l))) (Lit false).
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_plus z1 z2 :
- PureExec True 1 (BinOp PlusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 + z2).
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_minus z1 z2 :
- PureExec True 1 (BinOp MinusOp (Lit $ LitInt z1) (Lit $ LitInt z2)) (Lit $ LitInt $ z1 - z2).
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_offset l z :
- PureExec True 1 (BinOp OffsetOp (Lit $ LitLoc l) (Lit $ LitInt z)) (Lit $ LitLoc $ l +ₗ z).
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_case i e el :
- PureExec (0 ≤ i ∧ el !! (Z.to_nat i) = Some e) 1 (Case (Lit $ LitInt i) el) e | 10.
-Proof. solve_pure_exec. Qed.
-
-Global Instance pure_if b e1 e2 :
- PureExec True 1 (If (Lit (lit_of_bool b)) e1 e2) (if b then e1 else e2) | 1.
-Proof. destruct b; solve_pure_exec. Qed.
-
-(** Heap *)
-Lemma wp_alloc E (n : Z) :
- 0 < n →
- {{{ True }}} Alloc (Lit $ LitInt n) @ E
- {{{ l (sz: nat), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…sz ∗ l ↦∗ repeat (LitV LitPoison) sz }}}.
-Proof.
- 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Φ" $! _ (Z.to_nat n)). iFrame. iPureIntro. rewrite Z2Nat.id; lia.
-Qed.
-
-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 LitPoison; True }}}.
-Proof.
- 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 E l q v :
- {{{ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
- {{{ RET v; l ↦{q} v }}}.
-Proof.
- 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. by iApply "HΦ".
-Qed.
-
-Lemma wp_read_na E l q v :
- {{{ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
- {{{ RET v; l ↦{q} v }}}.
-Proof.
- 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; last done.
- 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.
- iFrame "Hσ". iSplit; [done|]. by iApply "HΦ".
-Qed.
-
-Lemma wp_write_sc E l e v v' :
- IntoVal e v →
- {{{ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
- {{{ RET LitV LitPoison; l ↦ v }}}.
-Proof.
- iIntros (<- Φ) ">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_na E l e v v' :
- IntoVal e v →
- {{{ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
- {{{ RET LitV LitPoison; l ↦ v }}}.
-Proof.
- iIntros (<- Φ) ">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; last done.
- 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_cas_int_fail E l q z1 e2 lit2 zl :
- IntoVal e2 (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 (<- ? Φ) ">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_cas_suc E l lit1 e2 lit2 :
- IntoVal e2 (LitV lit2) → lit1 ≠ LitPoison →
- {{{ ▷ l ↦ LitV lit1 }}}
- CAS (Lit $ LitLoc l) (Lit lit1) e2 @ E
- {{{ RET LitV (LitInt 1); l ↦ LitV lit2 }}}.
-Proof.
- iIntros (<- ? Φ) ">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_int_suc E l z1 e2 lit2 :
- IntoVal e2 (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 :
- IntoVal e2 (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' :
- IntoVal e2 (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 (<- ? Φ) "(>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 :
- IntoVal e2 (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 (<- Φ) ">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.
-
-Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
- (P -∗ ▷ l1 ↦{q1} v1) →
- (P -∗ ▷ l2 ↦{q2} v2) →
- (P -∗ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
- P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
-Proof.
- iIntros (Hl1 Hl2 Hpost) "HP".
- destruct (bool_decide_reflect (l1 = l2)) as [->|].
- - iApply wp_lift_pure_det_head_step_no_fork';
- [done|solve_exec_safe|solve_exec_puredet|].
- iApply wp_value. by iApply Hpost.
- - iApply wp_lift_atomic_head_step_no_fork; subst=>//.
- iIntros (σ1 ???) "Hσ1". iModIntro. inv_head_step.
- iSplitR.
- { iPureIntro. repeat eexists. econstructor. eapply BinOpEqFalse. by auto. }
- (* We need to do a little gymnastics here to apply Hne now and strip away a
- ▷ but also have the ↦s. *)
- iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
- { iSplit; last iSplit.
- + iExists _, _. by iApply Hl1.
- + iExists _, _. by iApply Hl2.
- + by iApply Hpost. }
- clear Hl1 Hl2. iNext. iIntros (e2 σ2 efs Hs) "!>".
- inv_head_step. iSplitR=>//. inv_bin_op_eval; inv_lit.
- + iExFalso. iDestruct "HP" as "[Hl1 _]".
- iDestruct "Hl1" as (??) "Hl1".
- iDestruct (heap_read σ2 with "Hσ1 Hl1") as %[??]; simplify_eq.
- + iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
- iDestruct "Hl2" as (??) "Hl2".
- iDestruct (heap_read σ2 with "Hσ1 Hl2") as %[??]; simplify_eq.
- + iDestruct "HP" as "[_ [_ $]]". done.
-Qed.
-
-(** Proof rules for working on the n-ary argument list. *)
-Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el)) vs Φ :
- AsVal f →
- ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
- (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
- WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
- WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
-Proof.
- intros [vf <-]. revert vs Ql.
- induction el as [|e el IH]=>/= vs Ql; inv_vec Ql; simpl.
- - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
- - iIntros (Q Ql) "[He Hl] HΦ".
- change (App (of_val vf) ((of_val <$> vs) ++ e :: el)) with (fill_item (AppRCtx vf vs el) e).
- iApply wp_bind. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
- rewrite cons_middle (assoc app) -(fmap_app _ _ [v]).
- iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
- iApply ("HΦ" $! (v:::vl)). iFrame.
-Qed.
-
-Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
- AsVal f →
- ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
- (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
- WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
- WP App f el @ E {{ Φ }}.
-Proof. iIntros (Hf). by iApply (wp_app_ind _ _ _ _ []). Qed.
-
-Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
- length Ql = length el → AsVal f →
- ([∗ list] eQ ∈ zip el Ql, WP eQ.1 @ E {{ eQ.2 }}) -∗
- (∀ vl : list val, ⌜length vl = length el⌝ -∗
- ([∗ list] k ↦ vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
- WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
- WP App f el @ E {{ Φ }}.
-Proof.
- iIntros (Hlen Hf) "Hel HΦ". rewrite -(vec_to_list_of_list Ql).
- generalize (list_to_vec Ql). rewrite Hlen. clear Hlen Ql=>Ql.
- iApply (wp_app_vec with "Hel"). iIntros (vl) "Hvl".
- iApply ("HΦ" with "[%] Hvl"). by rewrite vec_to_list_length.
-Qed.
-End lifting.
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
deleted file mode 100644
index a1b3db3e..00000000
--- a/theories/lang/proofmode.v
+++ /dev/null
@@ -1,259 +0,0 @@
-From iris.program_logic Require Export weakestpre.
-From iris.proofmode Require Import coq_tactics reduction.
-From iris.proofmode Require Export tactics.
-From lrust.lang Require Export tactics lifting.
-From iris.program_logic Require Import lifting.
-Set Default Proof Using "Type".
-Import uPred.
-
-Lemma tac_wp_value `{!lrustG Σ} Δ E Φ e v :
- IntoVal e v →
- envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ? ->. by apply wp_value. Qed.
-
-Ltac wp_value_head := eapply tac_wp_value; [iSolveTC|reduction.pm_prettify].
-
-Lemma tac_wp_pure `{!lrustG Σ} K Δ Δ' E e1 e2 φ n Φ :
- PureExec φ n e1 e2 →
- φ →
- MaybeIntoLaterNEnvs n Δ Δ' →
- envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
- envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
-Proof.
- rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
- rewrite -wp_bind HΔ' -wp_pure_step_later //. by rewrite -wp_bind_inv.
-Qed.
-
-Tactic Notation "wp_pure" open_constr(efoc) :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
- unify e' efoc;
- eapply (tac_wp_pure K);
- [simpl; iSolveTC (* PureExec *)
- |try done (* The pure condition for PureExec *)
- |iSolveTC (* IntoLaters *)
- |simpl_subst; try wp_value_head (* new goal *)])
- || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
- | _ => fail "wp_pure: not a 'wp'"
- end.
-
-Lemma tac_wp_eq_loc `{!lrustG Σ} K Δ Δ' E i1 i2 l1 l2 q1 q2 v1 v2 Φ :
- MaybeIntoLaterNEnvs 1 Δ Δ' →
- envs_lookup i1 Δ' = Some (false, l1 ↦{q1} v1)%I →
- envs_lookup i2 Δ' = Some (false, l2 ↦{q2} v2)%I →
- envs_entails Δ' (WP fill K (Lit (bool_decide (l1 = l2))) @ E {{ Φ }}) →
- envs_entails Δ (WP fill K (BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2))) @ E {{ Φ }}).
-Proof.
- rewrite envs_entails_eq=> ? /envs_lookup_sound /=. rewrite sep_elim_l=> ?.
- move /envs_lookup_sound; rewrite sep_elim_l=> ? HΔ. rewrite -wp_bind.
- rewrite into_laterN_env_sound /=. eapply wp_eq_loc; eauto using later_mono.
-Qed.
-
-Tactic Notation "wp_eq_loc" :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
- reshape_expr e ltac:(fun K e' => eapply (tac_wp_eq_loc K));
- [iSolveTC|iAssumptionCore|iAssumptionCore|simpl; try wp_value_head]
- | _ => fail "wp_pure: not a 'wp'"
- end.
-
-Tactic Notation "wp_rec" := wp_pure (App _ _).
-Tactic Notation "wp_lam" := wp_rec.
-Tactic Notation "wp_let" := wp_lam.
-Tactic Notation "wp_seq" := wp_let.
-Tactic Notation "wp_op" := wp_pure (BinOp _ _ _) || wp_eq_loc.
-Tactic Notation "wp_if" := wp_pure (If _ _ _).
-Tactic Notation "wp_case" := wp_pure (Case _ _); try wp_value_head.
-
-Lemma tac_wp_bind `{!lrustG Σ} K Δ E Φ e :
- envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
- envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> ->. apply: wp_bind. Qed.
-
-Ltac wp_bind_core K :=
- lazymatch eval hnf in K with
- | [] => idtac
- | _ => apply (tac_wp_bind K); simpl
- end.
-
-Tactic Notation "wp_bind" open_constr(efoc) :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
- match e' with
- | efoc => unify e' efoc; wp_bind_core K
- end) || fail "wp_bind: cannot find" efoc "in" e
- | _ => fail "wp_bind: not a 'wp'"
- end.
-
-Section heap.
-Context `{!lrustG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types Δ : envs (uPredI (iResUR Σ)).
-
-Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
- 0 < n →
- MaybeIntoLaterNEnvs 1 Δ Δ' →
- (∀ l (sz: nat), n = sz → ∃ Δ'',
- envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ repeat (LitV LitPoison) sz)) j2 (†l…sz)) Δ'
- = Some Δ'' ∧
- envs_entails Δ'' (WP fill K (Lit $ LitLoc l) @ E {{ Φ }})) →
- envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
-Proof.
- rewrite envs_entails_eq=> ?? HΔ. rewrite -wp_bind.
- eapply wand_apply; first exact:wp_alloc.
- rewrite -persistent_and_sep. apply and_intro; first by auto.
- rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
- apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
- rewrite sep_and. apply pure_elim_l=> Hn. apply wand_elim_r'.
- destruct (HΔ l sz) as (Δ''&?&HΔ'); first done.
- rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
-Qed.
-
-Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
- n = length vl →
- MaybeIntoLaterNEnvs 1 Δ Δ' →
- envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
- envs_delete false i1 false Δ' = Δ'' →
- envs_lookup i2 Δ'' = Some (false, †l…n')%I →
- envs_delete false i2 false Δ'' = Δ''' →
- n' = length vl →
- envs_entails Δ''' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
- envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
-Proof.
- rewrite envs_entails_eq; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
- 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Δ True_emp emp_wand -assoc.
-Qed.
-
-Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
- o = Na1Ord ∨ o = ScOrd →
- MaybeIntoLaterNEnvs 1 Δ Δ' →
- envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
- envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
- envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
-Proof.
- rewrite envs_entails_eq; intros [->| ->] ???.
- - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na.
- rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
- by apply later_mono, sep_mono_r, wand_mono.
- - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_sc.
- rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
- by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-
-Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
- IntoVal e v' →
- o = Na1Ord ∨ o = ScOrd →
- MaybeIntoLaterNEnvs 1 Δ Δ' →
- envs_lookup i Δ' = Some (false, l ↦ v)%I →
- envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
- envs_entails Δ'' (WP fill K (Lit LitPoison) @ E {{ Φ }}) →
- envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
-Proof.
- rewrite envs_entails_eq; intros ? [->| ->] ????.
- - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na.
- rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
- rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
- - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_sc.
- rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
- rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
-Qed.
-End heap.
-
-Tactic Notation "wp_apply" open_constr(lem) :=
- iPoseProofCore lem as false true (fun H =>
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
- reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
- lazymatch iTypeOf H with
- | Some (_,?P) => fail "wp_apply: cannot apply" P
- end
- | _ => fail "wp_apply: not a 'wp'"
- end).
-
-Tactic Notation "wp_alloc" ident(l) "as" constr(H) constr(Hf) :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
- first
- [reshape_expr e ltac:(fun K e' => eapply (tac_wp_alloc K _ _ _ H Hf))
- |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
- [try fast_done
- |iSolveTC
- |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
- first [intros l sz Hsz | fail 1 "wp_alloc:" l "not fresh"];
- (* If Hsz is "constant Z = nat", change that to an equation on nat and
- potentially substitute away the sz. *)
- try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
- apply Nat2Z.inj in Hsz;
- try (cbv [Z.to_nat Pos.to_nat] in Hsz;
- simpl in Hsz;
- (* Substitute only if we have a literal nat. *)
- match goal with Hsz : S _ = _ |- _ => subst sz end));
- eexists; split;
- [pm_reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
- |simpl; try wp_value_head]]
- | _ => fail "wp_alloc: not a 'wp'"
- end.
-
-Tactic Notation "wp_alloc" ident(l) :=
- let H := iFresh in let Hf := iFresh in wp_alloc l as H Hf.
-
-Tactic Notation "wp_free" :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
- first
- [reshape_expr e ltac:(fun K e' => eapply (tac_wp_free K))
- |fail 1 "wp_free: cannot find 'Free' in" e];
- [try fast_done
- |iSolveTC
- |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
- iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
- |pm_reflexivity
- |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
- iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
- |pm_reflexivity
- |try fast_done
- |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
- | _ => fail "wp_free: not a 'wp'"
- end.
-
-Tactic Notation "wp_read" :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
- first
- [reshape_expr e ltac:(fun K e' => eapply (tac_wp_read K))
- |fail 1 "wp_read: cannot find 'Read' in" e];
- [(right; fast_done) || (left; fast_done) ||
- fail "wp_read: order is neither Na2Ord nor ScOrd"
- |iSolveTC
- |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
- iAssumptionCore || fail "wp_read: cannot find" l "↦ ?"
- |simpl; try wp_value_head]
- | _ => fail "wp_read: not a 'wp'"
- end.
-
-Tactic Notation "wp_write" :=
- iStartProof;
- lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
- first
- [reshape_expr e ltac:(fun K e' => eapply (tac_wp_write K); [iSolveTC|..])
- |fail 1 "wp_write: cannot find 'Write' in" e];
- [(right; fast_done) || (left; fast_done) ||
- fail "wp_write: order is neither Na2Ord nor ScOrd"
- |iSolveTC
- |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
- iAssumptionCore || fail "wp_write: cannot find" l "↦ ?"
- |pm_reflexivity
- |simpl; try first [wp_pure (Seq (Lit LitPoison) _)|wp_value_head]]
- | _ => fail "wp_write: not a 'wp'"
- end.
diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v
index 360947ef..ff702ed1 100644
--- a/theories/lang/spawn.v
+++ b/theories/lang/spawn.v
@@ -95,7 +95,7 @@ Proof.
iMod (own_alloc (Excl ())) as (γe) "Hγe"; first done.
rewrite own_loc_na_vec_cons own_loc_na_vec_singleton.
iDestruct "Hl" as "[Hc Hd]". wp_write.
- iMod (GPS_vSP_Init N (λ γi, spawn_interp γe γi Ψ) IW _ () with "Hc []")
+ iMod (GPS_vSP_Init N (λ γi, spawn_interp γe γi Ψ) (λ _, IW) _ () with "Hc []")
as (γi γc t) "[[Htok1 Htok2] SW]". { iIntros (???). by iExists false. }
iDestruct (GPS_vSP_SWWriter_Reader with "SW") as "#R".
wp_apply (wp_fork with "[SW Htok1 Hf Hd]"); [done|..].
--
GitLab