Commit 6ec83eee authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Ofe problems.

parent 59c66c09
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9aaa3e89cd01c56798b1eb7c3cd292b83a2f582c
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9e4c13a35c6e15c44218707c6c1b77ed8bdd6e54
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 (?) "".
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.
......@@ -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. *)
......
This diff is collapsed.
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.
......@@ -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.
......
......@@ -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.
......
......@@ -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</