Skip to content
Snippets Groups Projects
Commit fc96e6a8 authored by Hai Dang's avatar Hai Dang
Browse files

Merge branch 'master' into ci/weak_mem

parents d0cb585b e9838554
No related branches found
No related tags found
No related merge requests found
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 () "Hvγ".
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. }
iMod (own_alloc ( ( : heap_freeableUR))) as () "Hfγ"; first done.
set (Hheap := HeapG _ _ _ ).
iModIntro. iExists (λ σ _, heap_ctx σ). iSplitL.
{ iExists ∅. by iFrame. }
by iApply (Hwp (LRustG _ _ Hheap)).
Qed.
This diff is collapsed.
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 omega.
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 lsz 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.
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=> ? . 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 (lsz)) Δ'
= 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=> ?? . 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 ( 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, ln')%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 -> ?? <- ? <- -> . 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 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.
From stdpp Require Import gmap.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import adequacy.
From lrust.lang Require Import tactics.
Set Default Proof Using "Type".
Inductive access_kind : Type := ReadAcc | WriteAcc | FreeAcc.
(* This is a crucial definition; if we forget to sync it with head_step,
the results proven here are worthless. *)
Inductive next_access_head : expr state access_kind * order loc Prop :=
| Access_read ord l σ :
next_access_head (Read ord (Lit $ LitLoc l)) σ (ReadAcc, ord) l
| Access_write ord l e σ :
is_Some (to_val e)
next_access_head (Write ord (Lit $ LitLoc l) e) σ (WriteAcc, ord) l
| Access_cas_fail l st e1 lit1 e2 lit2 litl σ :
to_val e1 = Some (LitV lit1) to_val e2 = Some (LitV lit2)
lit_neq lit1 litl σ !! l = Some (st, LitV litl)
next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (ReadAcc, ScOrd) l
| Access_cas_suc l st e1 lit1 e2 lit2 litl σ :
to_val e1 = Some (LitV lit1) to_val e2 = Some (LitV lit2)
lit_eq σ lit1 litl σ !! l = Some (st, LitV litl)
next_access_head (CAS (Lit $ LitLoc l) e1 e2) σ (WriteAcc, ScOrd) l
| Access_free n l σ i :
0 i < n
next_access_head (Free (Lit $ LitInt n) (Lit $ LitLoc l))
σ (FreeAcc, Na2Ord) (l + i).
(* Some sanity checks to make sure the definition above is not entirely insensible. *)
Goal e1 e2 e3 σ, head_reducible (CAS e1 e2 e3) σ
a l, next_access_head (CAS e1 e2 e3) σ a l.
Proof.
intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
(eapply Access_cas_fail; done) || eapply Access_cas_suc; done.
Qed.
Goal o e σ, head_reducible (Read o e) σ
a l, next_access_head (Read o e) σ a l.
Proof.
intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_read; done.
Qed.
Goal o e1 e2 σ, head_reducible (Write o e1 e2) σ
a l, next_access_head (Write o e1 e2) σ a l.
Proof.
intros ??? σ (?&?&?&?&?). inversion H; do 2 eexists;
eapply Access_write; try done; eexists; done.
Qed.
Goal e1 e2 σ, head_reducible (Free e1 e2) σ
a l, next_access_head (Free e1 e2) σ a l.
Proof.
intros ?? σ (?&?&?&?&?). inversion H; do 2 eexists; eapply Access_free; done.
Qed.
Definition next_access_thread (e: expr) (σ : state)
(a : access_kind * order) (l : loc) : Prop :=
K e', next_access_head e' σ a l e = fill K e'.
Definition next_accesses_threadpool (el: list expr) (σ : state)
(a1 a2 : access_kind * order) (l : loc): Prop :=
t1 e1 t2 e2 t3, el = t1 ++ e1 :: t2 ++ e2 :: t3
next_access_thread e1 σ a1 l next_access_thread e2 σ a2 l.
Definition nonracing_accesses (a1 a2 : access_kind * order) : Prop :=
match a1, a2 with
| (_, ScOrd), (_, ScOrd) => True
| (ReadAcc, _), (ReadAcc, _) => True
| _, _ => False
end.
Definition nonracing_threadpool (el : list expr) (σ : state) : Prop :=
l a1 a2, next_accesses_threadpool el σ a1 a2 l
nonracing_accesses a1 a2.
Lemma next_access_head_reductible_ctx e σ σ' a l K :
next_access_head e σ' a l reducible (fill K e) σ head_reducible e σ.
Proof.
intros Hhead Hred. apply prim_head_reducible.
- eapply (reducible_fill (K:=ectx_language.fill K)), Hred. destruct Hhead; eauto.
- apply ectxi_language_sub_redexes_are_values. intros [] ? ->; inversion Hhead; eauto.
Qed.
Definition head_reduce_not_to_stuck (e : expr) (σ : state) :=
κ e' σ' efs, ectx_language.head_step e σ κ e' σ' efs e' App (Lit $ LitInt 0) [].
Lemma next_access_head_reducible_state e σ a l :
next_access_head e σ a l head_reducible e σ
head_reduce_not_to_stuck e σ
match a with
| (ReadAcc, ScOrd | Na1Ord) => v n, σ !! l = Some (RSt n, v)
| (ReadAcc, Na2Ord) => v n, σ !! l = Some (RSt (S n), v)
| (WriteAcc, ScOrd | Na1Ord) => v, σ !! l = Some (RSt 0, v)
| (WriteAcc, Na2Ord) => v, σ !! l = Some (WSt, v)
| (FreeAcc, _) => v ls, σ !! l = Some (ls, v)
end.
Proof.
intros Ha (κ&e'&σ'&ef&Hstep) Hrednonstuck. destruct Ha; inv_head_step; eauto.
- destruct n; first by eexists. exfalso. eapply Hrednonstuck; last done.
by eapply CasStuckS.
- exfalso. eapply Hrednonstuck; last done.
eapply CasStuckS; done.
- match goal with H : m, _ |- _ => destruct (H i) as [_ [[]?]] end; eauto.
Qed.
Lemma next_access_head_Na1Ord_step e1 e2 ef σ1 σ2 κ a l :
next_access_head e1 σ1 (a, Na1Ord) l
head_step e1 σ1 κ e2 σ2 ef
next_access_head e2 σ2 (a, Na2Ord) l.
Proof.
intros Ha Hstep. inversion Ha; subst; clear Ha; inv_head_step; constructor; by rewrite to_of_val.
Qed.
Lemma next_access_head_Na1Ord_concurent_step e1 e1' e2 e'f σ σ' κ a1 a2 l :
next_access_head e1 σ (a1, Na1Ord) l
head_step e1 σ κ e1' σ' e'f
next_access_head e2 σ a2 l
next_access_head e2 σ' a2 l.
Proof.
intros Ha1 Hstep Ha2. inversion Ha1; subst; clear Ha1; inv_head_step;
destruct Ha2; simplify_eq; econstructor; eauto; try apply lookup_insert.
(* Oh my. FIXME. *)
- eapply lit_eq_state; last done.
setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
- eapply lit_eq_state; last done.
setoid_rewrite <-(not_elem_of_dom (D:=gset loc)). rewrite dom_insert_L.
cut (is_Some (σ !! l)); last by eexists. rewrite -(elem_of_dom (D:=gset loc)). set_solver+.
Qed.
Lemma next_access_head_Free_concurent_step e1 e1' e2 e'f σ σ' κ o1 a2 l :
next_access_head e1 σ (FreeAcc, o1) l head_step e1 σ κ e1' σ' e'f
next_access_head e2 σ a2 l head_reducible e2 σ'
False.
Proof.
intros Ha1 Hstep Ha2 Hred2.
assert (FREE : l n i, 0 i i < n free_mem l (Z.to_nat n) σ !! (l + i) = None).
{ clear. intros l n i Hi.
replace n with (Z.of_nat (Z.to_nat n)) in Hi by (apply Z2Nat.id; lia).
revert l i Hi. induction (Z.to_nat n) as [|? IH]=>/=l i Hi. lia.
destruct (decide (i = 0)).
- subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
- replace i with (1+(i-1)) by lia.
rewrite lookup_delete_ne -shift_loc_assoc ?IH //. lia.
destruct l; intros [=?]. lia. }
assert (FREE' : σ' !! l = None).
{ inversion Ha1; clear Ha1; inv_head_step. auto. }
destruct Hred2 as (κ'&e2'&σ''&ef&?).
inversion Ha2; clear Ha2; inv_head_step.
eapply (@is_Some_None (lock_state * val)). rewrite -FREE'. naive_solver.
Qed.
Lemma safe_step_not_reduce_to_stuck el σ K e e' σ' ef κ :
( el' σ' e', rtc erased_step (el, σ) (el', σ')
e' el' to_val e' = None reducible e' σ')
fill K e el head_step e σ κ e' σ' ef head_reduce_not_to_stuck e' σ'.
Proof.
intros Hsafe Hi Hstep κ1 e1 σ1 ? Hstep1 Hstuck.
cut (reducible (fill K e1) σ1).
{ subst. intros (?&?&?&?&?). by eapply stuck_irreducible. }
destruct (elem_of_list_split _ _ Hi) as (?&?&->).
eapply Hsafe; last by (apply: fill_not_val; subst).
- eapply rtc_l, rtc_l, rtc_refl.
+ eexists. econstructor. done. done. econstructor; done.
+ eexists. econstructor. done. done. econstructor; done.
- subst. set_solver+.
Qed.
(* TODO: Unify this and the above. *)
Lemma safe_not_reduce_to_stuck el σ K e :
( el' σ' e', rtc erased_step (el, σ) (el', σ')
e' el' to_val e' = None reducible e' σ')
fill K e el head_reduce_not_to_stuck e σ.
Proof.
intros Hsafe Hi κ e1 σ1 ? Hstep1 Hstuck.
cut (reducible (fill K e1) σ1).
{ subst. intros (?&?&?&?&?). by eapply stuck_irreducible. }
destruct (elem_of_list_split _ _ Hi) as (?&?&->).
eapply Hsafe; last by (apply: fill_not_val; subst).
- eapply rtc_l, rtc_refl.
+ eexists. econstructor. done. done. econstructor; done.
- subst. set_solver+.
Qed.
Theorem safe_nonracing el σ :
( el' σ' e', rtc erased_step (el, σ) (el', σ')
e' el' to_val e' = None reducible e' σ')
nonracing_threadpool el σ.
Proof.
intros Hsafe l a1 a2 (t1&?&t2&?&t3&->&(K1&e1&Ha1&->)&(K2&e2&Ha2&->)).
assert (to_val e1 = None). by destruct Ha1.
assert (Hrede1:head_reducible e1 σ).
{ eapply (next_access_head_reductible_ctx e1 σ σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse1:head_reduce_not_to_stuck e1 σ).
{ eapply safe_not_reduce_to_stuck with (K:=K1); first done. set_solver+. }
assert (Hσe1:=next_access_head_reducible_state _ _ _ _ Ha1 Hrede1 Hnse1).
destruct Hrede1 as (κ1'&e1'&σ1'&ef1&Hstep1). clear Hnse1.
assert (Ha1' : a1.2 = Na1Ord next_access_head e1' σ1' (a1.1, Na2Ord) l).
{ intros. eapply next_access_head_Na1Ord_step, Hstep1.
by destruct a1; simpl in *; subst. }
assert (Hrtc_step1:
rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
(t1 ++ fill K1 e1' :: t2 ++ fill K2 e2 :: t3 ++ ef1, σ1')).
{ eapply rtc_l, rtc_refl. eexists. eapply step_atomic, Ectx_step, Hstep1; try done.
by rewrite -assoc. }
assert (Hrede1: a1.2 = Na1Ord head_reducible e1' σ1').
{ destruct a1 as [a1 []]=>// _.
eapply (next_access_head_reductible_ctx e1' σ1' σ1' (a1, Na2Ord) l K1), Hsafe,
fill_not_val=>//.
by auto. abstract set_solver. by destruct Hstep1; inversion Ha1. }
assert (Hnse1: head_reduce_not_to_stuck e1' σ1').
{ eapply safe_step_not_reduce_to_stuck with (K:=K1); first done; last done. set_solver+. }
assert (to_val e2 = None). by destruct Ha2.
assert (Hrede2:head_reducible e2 σ).
{ eapply (next_access_head_reductible_ctx e2 σ σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse2:head_reduce_not_to_stuck e2 σ).
{ eapply safe_not_reduce_to_stuck with (K:=K2); first done. set_solver+. }
assert (Hσe2:=next_access_head_reducible_state _ _ _ _ Ha2 Hrede2 Hnse2).
destruct Hrede2 as (κ2'&e2'&σ2'&ef2&Hstep2).
assert (Ha2' : a2.2 = Na1Ord next_access_head e2' σ2' (a2.1, Na2Ord) l).
{ intros. eapply next_access_head_Na1Ord_step, Hstep2.
by destruct a2; simpl in *; subst. }
assert (Hrtc_step2:
rtc erased_step (t1 ++ fill K1 e1 :: t2 ++ fill K2 e2 :: t3, σ)
(t1 ++ fill K1 e1 :: t2 ++ fill K2 e2' :: t3 ++ ef2, σ2')).
{ eapply rtc_l, rtc_refl. rewrite app_comm_cons assoc. eexists.
eapply step_atomic, Ectx_step, Hstep2; try done. by rewrite -assoc. }
assert (Hrede2: a2.2 = Na1Ord head_reducible e2' σ2').
{ destruct a2 as [a2 []]=>// _.
eapply (next_access_head_reductible_ctx e2' σ2' σ2' (a2, Na2Ord) l K2), Hsafe,
fill_not_val=>//.
by auto. abstract set_solver. by destruct Hstep2; inversion Ha2. }
assert (Hnse2':head_reduce_not_to_stuck e2' σ2').
{ eapply safe_step_not_reduce_to_stuck with (K:=K2); first done; last done. set_solver+. }
assert (Ha1'2 : a1.2 = Na1Ord next_access_head e2 σ1' a2 l).
{ intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
by rewrite <-HNa, <-surjective_pairing. }
assert (Hrede1_2: head_reducible e2 σ1').
{ intros. eapply (next_access_head_reductible_ctx e2 σ1' σ a2 l K2), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse1_2:head_reduce_not_to_stuck e2 σ1').
{ eapply safe_not_reduce_to_stuck with (K:=K2).
- intros. eapply Hsafe. etrans; last done. done. done. done.
- set_solver+. }
assert (Hσe1'1:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1' Hord) (Hrede1 Hord) Hnse1).
assert (Hσe1'2:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha1'2 Hord) Hrede1_2 Hnse1_2).
assert (Ha2'1 : a2.2 = Na1Ord next_access_head e1 σ2' a1 l).
{ intros HNa. eapply next_access_head_Na1Ord_concurent_step=>//.
by rewrite <-HNa, <-surjective_pairing. }
assert (Hrede2_1: head_reducible e1 σ2').
{ intros. eapply (next_access_head_reductible_ctx e1 σ2' σ a1 l K1), Hsafe, fill_not_val=>//.
abstract set_solver. }
assert (Hnse2_1:head_reduce_not_to_stuck e1 σ2').
{ eapply safe_not_reduce_to_stuck with (K:=K1).
- intros. eapply Hsafe. etrans; last done. done. done. done.
- set_solver+. }
assert (Hσe2'1:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2'1 Hord) Hrede2_1 Hnse2_1).
assert (Hσe2'2:=
λ Hord, next_access_head_reducible_state _ _ _ _ (Ha2' Hord) (Hrede2 Hord) Hnse2').
assert (a1.1 = FreeAcc False).
{ destruct a1 as [[]?]; inversion 1.
eauto using next_access_head_Free_concurent_step. }
assert (a2.1 = FreeAcc False).
{ destruct a2 as [[]?]; inversion 1.
eauto using next_access_head_Free_concurent_step. }
destruct Ha1 as [[]|[]| | |], Ha2 as [[]|[]| | |]=>//=; simpl in *;
repeat match goal with
| H : _ = Na1Ord _ |- _ => specialize (H (eq_refl Na1Ord)) || clear H
| H : False |- _ => destruct H
| H : _, _ |- _ => destruct H
end;
try congruence.
clear κ2' e2' Hnse2' Hnse2_1 Hstep2 σ2' Hrtc_step2 Hrede2_1.
destruct Hrede1_2 as (κ2'&e2'&σ'&ef&?).
inv_head_step.
match goal with
| H : <[l:=_]> σ !! l = _ |- _ => by rewrite lookup_insert in H
end.
Qed.
Corollary adequate_nonracing e1 t2 σ1 σ2 φ :
adequate NotStuck e1 σ1 φ
rtc erased_step ([e1], σ1) (t2, σ2)
nonracing_threadpool t2 σ2.
Proof.
intros [_ Had] Hrtc. apply safe_nonracing. intros el' σ' e' ?? He'.
edestruct (Had el' σ' e') as [He''|]; try done. etrans; eassumption.
rewrite /language.to_val /= He' in He''. by edestruct @is_Some_None.
Qed.
From stdpp Require Import fin_maps.
From lrust.lang Require Export lang.
Set Default Proof Using "Type".
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
expressions into this type we can implement substitution, closedness
checking, atomic checking, and conversion into values, by computation. *)
Module W.
Inductive expr :=
| Val (v : val) (e : lang.expr) (H : to_val e = Some v)
| ClosedExpr (e : lang.expr) `{!Closed [] e}
| 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).
Fixpoint to_expr (e : expr) : lang.expr :=
match e with
| Val v e' _ => e'
| ClosedExpr e => e
| Var x => lang.Var x
| Lit l => lang.Lit l
| Rec f xl e => lang.Rec f xl (to_expr e)
| BinOp op e1 e2 => lang.BinOp op (to_expr e1) (to_expr e2)
| App e el => lang.App (to_expr e) (map to_expr el)
| Read o e => lang.Read o (to_expr e)
| Write o e1 e2 => lang.Write o (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
| Alloc e => lang.Alloc (to_expr e)
| Free e1 e2 => lang.Free (to_expr e1) (to_expr e2)
| Case e el => lang.Case (to_expr e) (map to_expr el)
| Fork e => lang.Fork (to_expr e)
end.
Ltac of_expr e :=
lazymatch e with
| lang.Var ?x => constr:(Var x)
| lang.Lit ?l => constr:(Lit l)
| lang.Rec ?f ?xl ?e => let e := of_expr e in constr:(Rec f xl e)
| lang.BinOp ?op ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
| lang.App ?e ?el =>
let e := of_expr e in let el := of_expr el in constr:(App e el)
| lang.Read ?o ?e => let e := of_expr e in constr:(Read o e)
| lang.Write ?o ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Write o e1 e2)
| lang.CAS ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
| lang.Free ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Free e1 e2)
| lang.Case ?e ?el =>
let e := of_expr e in let el := of_expr el in constr:(Case e el)
| lang.Fork ?e => let e := of_expr e in constr:(Fork e)
| @nil lang.expr => constr:(@nil expr)
| @cons lang.expr ?e ?el =>
let e := of_expr e in let el := of_expr el in constr:(e::el)
| to_expr ?e => e
| of_val ?v => constr:(Val v (of_val v) (to_of_val v))
| _ => match goal with
| H : to_val e = Some ?v |- _ => constr:(Val v e H)
| H : Closed [] e |- _ => constr:(@ClosedExpr e H)
end
end.
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Val _ _ _ | ClosedExpr _ => true
| 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.
Lemma is_closed_correct X e : is_closed X e lang.is_closed X (to_expr e).
Proof.
revert e X. fix FIX 1; destruct e=>/=;
try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
- induction el=>/=; naive_solver.
- induction el=>/=; naive_solver.
Qed.
(* We define [to_val (ClosedExpr _)] to be [None] since [ClosedExpr]
constructors are only generated for closed expressions of which we know nothing
about apart from being closed. Notice that the reverse implication of
[to_val_Some] thus does not hold. *)
Definition to_val (e : expr) : option val :=
match e with
| Val v _ _ => Some v
| Rec f xl e =>
if decide (is_closed (f :b: xl +b+ []) e) is left H
then Some (@RecV f xl (to_expr e) (is_closed_correct _ _ H)) else None
| Lit l => Some (LitV l)
| _ => None
end.
Lemma to_val_Some e v :
to_val e = Some v of_val v = W.to_expr e.
Proof.
revert v. induction e; intros; simplify_option_eq; auto using of_to_val.
Qed.
Lemma to_val_is_Some e :
is_Some (to_val e) v, of_val v = to_expr e.
Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Lemma to_val_is_Some' e :
is_Some (to_val e) is_Some (lang.to_val (to_expr e)).
Proof. intros [v ?]%to_val_is_Some. exists v. rewrite -to_of_val. by f_equal. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Val v e H => Val v e H
| ClosedExpr e => ClosedExpr e
| 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.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = lang.subst x (to_expr er) (to_expr e).
Proof.
revert e x er. fix FIX 1; destruct e=>/= ? er; repeat case_bool_decide;
f_equal; eauto using is_closed_nil_subst, is_closed_to_val, eq_sym.
- induction el=>//=. f_equal; auto.
- induction el=>//=. f_equal; auto.
Qed.
Definition is_atomic (e: expr) : bool :=
match e with
| Read (ScOrd | Na2Ord) e | Alloc e => bool_decide (is_Some (to_val e))
| Write (ScOrd | Na2Ord) e1 e2 | Free e1 e2 =>
bool_decide (is_Some (to_val e1) is_Some (to_val e2))
| CAS e0 e1 e2 =>
bool_decide (is_Some (to_val e0) is_Some (to_val e1) is_Some (to_val e2))
| _ => false
end.
Lemma is_atomic_correct e : is_atomic e Atomic WeaklyAtomic (to_expr e).
Proof.
intros He. apply ectx_language_atomic.
- intros σ e' σ' ef.
destruct e; simpl; try done; repeat (case_match; try done);
inversion 1; try (apply val_irreducible; rewrite ?language.to_of_val; naive_solver eauto); [].
rewrite -[stuck_term](fill_empty). apply stuck_irreducible.
- apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
revert He. destruct e; simpl; try done; repeat (case_match; try done);
rewrite ?bool_decide_spec;
destruct Ki; inversion Hfill; subst; clear Hfill;
try naive_solver eauto using to_val_is_Some'.
Qed.
End W.
Ltac solve_closed :=
match goal with
| |- Closed ?X ?e =>
let e' := W.of_expr e in change (Closed X (W.to_expr e'));
apply W.is_closed_correct; vm_compute; exact I
end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_into_val :=
match goal with
| |- IntoVal ?e ?v =>
let e' := W.of_expr e in change (of_val v = W.to_expr e');
apply W.to_val_Some; simpl; unfold W.to_expr;
((unlock; exact eq_refl) || (idtac; exact eq_refl))
end.
Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
Ltac solve_as_val :=
match goal with
| |- AsVal ?e =>
let e' := W.of_expr e in change ( v, of_val v = W.to_expr e');
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
Ltac solve_atomic :=
match goal with
| |- Atomic ?s ?e =>
let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
apply W.is_atomic_correct; vm_compute; exact I
end.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
(** Substitution *)
Ltac simpl_subst :=
unfold subst_v; simpl;
repeat match goal with
| |- context [subst ?x ?er ?e] =>
let er' := W.of_expr er in let e' := W.of_expr e in
change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
end;
unfold W.to_expr; simpl.
Arguments W.to_expr : simpl never.
Arguments subst : simpl never.
(** The tactic [inv_head_step] performs inversion on hypotheses of the
shape [head_step]. The tactic will discharge head-reductions starting
from values, and simplifies hypothesis related to conversions from and
to values, and finite map operations. This tactic is slightly ad-hoc
and tuned for proving our lifting lemmas. *)
Ltac inv_head_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : Lit _ = of_val ?v |- _ =>
apply (f_equal (to_val)) in H; rewrite to_of_val in H;
injection H; clear H; intro
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
| H : head_step ?e _ _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
(** The tactic [reshape_expr e tac] decomposes the expression [e] into an
evaluation context [K] and a subexpression [e']. It calls the tactic [tac K e']
for each possible decomposition until [tac] succeeds. *)
Ltac reshape_val e tac :=
let rec go e :=
match e with
| of_val ?v => v
| Lit ?l => constr:(LitV l)
| Rec ?f ?xl ?e => constr:(RecV f xl e)
end in let v := go e in tac v.
Ltac reshape_expr e tac :=
let rec go_fun K f vs es :=
match es with
| ?e :: ?es => reshape_val e ltac:(fun v => go_fun K f (v :: vs) es)
| ?e :: ?es => go (AppRCtx f (reverse vs) es :: K) e
end
with go K e :=
match e with
| _ => tac K e
| BinOp ?op ?e1 ?e2 =>
reshape_val e1 ltac:(fun v1 => go (BinOpRCtx op v1 :: K) e2)
| BinOp ?op ?e1 ?e2 => go (BinOpLCtx op e2 :: K) e1
| App ?e ?el => reshape_val e ltac:(fun f => go_fun K f (@nil val) el)
| App ?e ?el => go (AppLCtx el :: K) e
| Read ?o ?e => go (ReadCtx o :: K) e
| Write ?o ?e1 ?e2 =>
reshape_val e1 ltac:(fun v1 => go (WriteRCtx o v1 :: K) e2)
| Write ?o ?e1 ?e2 => go (WriteLCtx o e2 :: K) e1
| CAS ?e0 ?e1 ?e2 => reshape_val e0 ltac:(fun v0 => first
[ reshape_val e1 ltac:(fun v1 => go (CasRCtx v0 v1 :: K) e2)
| go (CasMCtx v0 e2 :: K) e1 ])
| CAS ?e0 ?e1 ?e2 => go (CasLCtx e1 e2 :: K) e0
| Alloc ?e => go (AllocCtx :: K) e
| Free ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (FreeRCtx v1 :: K) e2)
| Free ?e1 ?e2 => go (FreeLCtx e2 :: K) e1
| Case ?e ?el => go (CaseCtx el :: K) e
end
in go (@nil ectx_item) e.
......@@ -67,4 +67,6 @@ Theorem type_soundness_closed (main : val) σ t :
rtc erased_step ([(main [exit_cont] at init_tview)%E], mkGB ) (t, σ)
(* nonracing_threadpool t σ ∧ *) (* TODO : prove DRF theorem *)
( e 𝓥, (e at 𝓥)%E t is_Some (to_val e) reducible (e at 𝓥) σ).
Proof. intros. eapply @type_soundness; try done. apply _. Qed.
Proof.
intros. eapply @type_soundness; try done. apply _.
Qed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment