Commit 2f245f20 authored by Robbert Krebbers's avatar Robbert Krebbers

Port to latest Iris and make use of the `PureExec` infrastructure.

parent d5f74898
Pipeline #5113 failed with stage
in 2 minutes and 40 seconds
......@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-iris" { (= "dev.2017-10-29.1") | (= "dev") }
"coq-iris" { (= "dev.2017-11-02.0") | (= "dev") }
]
......@@ -512,6 +512,9 @@ 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.
......
This diff is collapsed.
......@@ -27,10 +27,10 @@ Lemma wp_memcpy `{lrustG Σ} E l1 l2 vl1 vl2 q (n : Z):
{{{ RET #; l1 ↦∗ vl2 l2 ↦∗{q} vl2 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op; case_bool_decide; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try discriminate.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || omega).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
......
......@@ -22,10 +22,10 @@ Section specs.
{{{ l, RET LitV $ LitLoc l;
(l(Z.to_nat n) n = 0) l ↦∗ repeat (LitV LitPoison) (Z.to_nat n) }}}.
Proof.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; intros ?.
iIntros (? Φ) "_ HΦ". wp_lam. wp_op; case_bool_decide.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†". iApply "HΦ". subst sz.
- wp_if. wp_alloc l as "H↦" "H†". omega. iApply "HΦ". subst sz.
iFrame. auto.
Qed.
......@@ -36,7 +36,7 @@ Section specs.
{{{ RET #; True }}}.
Proof.
iIntros (? Φ) "(H↦ & [H†|%]) HΦ";
wp_lam; wp_op; intros ?; try lia; wp_if; try wp_free; by iApply "HΦ".
wp_lam; wp_op; case_bool_decide; try lia; wp_if; try wp_free; by iApply "HΦ".
Qed.
End specs.
......
......@@ -105,12 +105,11 @@ Proof.
iDestruct "Hinv" as (b) "[>Hc Ho]". wp_read. destruct b; last first.
{ iMod ("Hclose" with "[Hc]").
- iNext. iRight. iExists _. iFrame.
- iModIntro. iApply wp_if. iNext. iApply ("IH" with "Hj H†").
auto. }
- iModIntro. wp_if. iApply ("IH" with "Hj H†"). auto. }
iDestruct "Ho" as (v) "(Hd & HΨ & Hf)".
iMod ("Hclose" with "[Hj Hf]") as "_".
{ iNext. iLeft. iFrame. }
iModIntro. iApply wp_if. iNext. wp_op. wp_read. wp_let.
iModIntro. wp_if. wp_op. wp_read. wp_let.
iAssert (c ↦∗ [ #true; v])%I with "[Hc Hd]" as "Hc".
{ rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton. iFrame. }
wp_free; first done. iApply "HΦ". iApply "HΨ'". done.
......
......@@ -18,10 +18,11 @@ Lemma wp_swap `{lrustG Σ} E l1 l2 vl1 vl2 (n : Z):
{{{ RET #; l1 ↦∗ vl2 l2 ↦∗ vl1 }}}.
Proof.
iIntros (Hvl1 Hvl2 Φ) "(Hl1 & Hl2) HΦ".
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec.
wp_op; case_bool_decide; wp_if.
- iApply "HΦ". assert (n = O) by lia; subst.
destruct vl1, vl2; try discriminate. by iFrame.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try discriminate.
- destruct vl1 as [|v1 vl1], vl2 as [|v2 vl2], n as [|n|]; try (discriminate || omega).
revert Hvl1 Hvl2. intros [= Hvl1] [= Hvl2]; rewrite !heap_mapsto_vec_cons. subst n.
iDestruct "Hl1" as "[Hv1 Hl1]". iDestruct "Hl2" as "[Hv2 Hl2]".
Local Opaque Zminus.
......
......@@ -12,7 +12,7 @@ Section tests.
{{{ (b: bool), RET LitV (lit_of_bool b); (if b then l1 = l2 else l1 l2)
l1 {q1} v1 l2 {q2} v2 }}}.
Proof.
iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op; try (by eauto); [|];
intros ?; iApply "HΦ"; by iFrame.
iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op.
case_bool_decide; iApply "HΦ"; by iFrame.
Qed.
End tests.
This diff is collapsed.
This diff is collapsed.
......@@ -8,7 +8,7 @@ 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)
| 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)
......@@ -25,7 +25,7 @@ Inductive expr :=
Fixpoint to_expr (e : expr) : lang.expr :=
match e with
| Val v => of_val v
| Val v e' _ => e'
| ClosedExpr e _ => e
| Var x => lang.Var x
| Lit l => lang.Lit l
......@@ -66,13 +66,16 @@ Ltac of_expr e :=
| @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)
| _ => match goal with H : Closed [] e |- _ => constr:(@ClosedExpr e H) end
| 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
| Val _ _ _ | ClosedExpr _ _ => true
| Var x => bool_decide (x X)
| Lit _ => true
| Rec f xl e => is_closed (f :b: xl +b+ X) e
......@@ -85,7 +88,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
Lemma is_closed_correct X e : is_closed X e lang.is_closed X (to_expr e).
Proof.
revert e X. fix 1; destruct e=>/=;
try naive_solver eauto using is_closed_of_val, is_closed_weaken_nil.
try naive_solver eauto using is_closed_to_val, is_closed_weaken_nil.
- induction el=>/=; naive_solver.
- induction el=>/=; naive_solver.
Qed.
......@@ -96,7 +99,7 @@ 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
| 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
......@@ -116,7 +119,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Val v => Val v
| Val v e H => Val v e H
| ClosedExpr e H => @ClosedExpr e H
| Var y => if bool_decide (y = x) then es else Var y
| Lit l => Lit l
......@@ -136,7 +139,7 @@ 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 1; destruct e=>/= ? er; repeat case_bool_decide;
f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
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.
......@@ -174,7 +177,7 @@ Ltac solve_closed :=
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_to_val :=
rewrite /IntoVal;
rewrite /IntoVal /AsVal;
try match goal with
| |- context E [language.to_val ?e] =>
let X := context E [to_val e] in change X
......@@ -188,6 +191,7 @@ Ltac solve_to_val :=
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end.
Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
Ltac solve_atomic :=
match goal with
......@@ -270,16 +274,3 @@ Ltac reshape_expr e tac :=
| Case ?e ?el => go (CaseCtx el :: K) e
end
in go (@nil ectx_item) e.
(** The tactic [do_head_step tac] solves goals of the shape [head_reducible] and
[head_step] by performing a reduction step and uses [tac] to solve any
side-conditions generated by individual steps. *)
Tactic Notation "do_head_step" tactic3(tac) :=
try match goal with |- head_reducible _ _ => eexists _, _, _ end;
simpl;
match goal with
| |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
first [apply alloc_fresh|econstructor];
(* solve [to_val] side-conditions *)
first [rewrite ?to_of_val; reflexivity|simpl_subst; tac; fast_done]
end.
......@@ -14,6 +14,9 @@ Ltac solve_typing :=
(typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
(typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
Lemma of_val_unlock v e : of_val v = e of_val (locked v) = e.
Proof. by unlock. Qed.
  • This looks like it should go somewhere into the lang/ folder?

Please register or sign in to reply
Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
Hint Resolve
of_val_unlock
......
......@@ -27,7 +27,7 @@ Section typing.
Lemma type_bool_instr (b : Datatypes.bool) : typed_val #b bool.
Proof.
iIntros (E L tid) "_ _ $ $ _". wp_value.
iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
rewrite tctx_interp_singleton tctx_hasty_val' //. by destruct b.
Qed.
......@@ -45,7 +45,7 @@ Section typing.
iIntros (Hp) "He1 He2". iIntros (tid) "#LFT #HE Htl HL HC HT".
iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "#Hp".
wp_bind p. iApply (wp_hasty with "Hp").
iIntros ([[| |[|[]|]]|]) "_ H1"; try done; (iApply wp_case; [done..|iNext]).
iIntros ([[| |[|[]|]]|]) "_ H1"; try done; wp_case.
- iApply ("He2" with "LFT HE Htl HL HC HT").
- iApply ("He1" with "LFT HE Htl HL HC HT").
Qed.
......
......@@ -34,14 +34,12 @@ Section typing.
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2) "He2 #Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
iApply wp_let'; first by rewrite /= decide_left.
iModIntro. iApply ("He2" with "LFT HE Htl HL [HC] HT").
rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
wp_let. iApply ("He2" with "LFT HE Htl HL [HC] HT").
iLöb as "IH". iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
iNext. iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
iIntros (args) "Htl HL HT". wp_rec.
iApply ("Hecont" with "LFT HE Htl HL [HC] HT"). by iApply "IH".
Qed.
Lemma type_cont_norec argsb L1 (T' : vec val (length argsb) _) E L2 C T econt e2 kb :
......@@ -52,13 +50,11 @@ Section typing.
typed_body E L2 C T (letcont: kb argsb := econt in e2).
Proof.
iIntros (Hc1 Hc2) "He2 Hecont". iIntros (tid) "#LFT #HE Htl HL HC HT".
iApply wp_let'; first by rewrite /= decide_left.
iModIntro. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
rewrite (_ : (rec: kb argsb := econt)%E = of_val (rec: kb argsb := econt)%V); last by unlock.
wp_let. iApply ("He2" with "LFT HE Htl HL [HC Hecont] HT").
iIntros (x) "H".
iDestruct "H" as %[->|?]%elem_of_cons; last by iApply "HC".
iIntros (args) "Htl HL HT". iApply wp_rec; try done.
{ rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
iNext. iApply ("Hecont" with "LFT HE Htl HL HC HT").
iIntros (args) "Htl HL HT". wp_rec.
iApply ("Hecont" with "LFT HE Htl HL HC HT").
Qed.
End typing.
......@@ -260,7 +260,7 @@ Section typing.
clear dependent k. wp_apply (wp_hasty with "Hf"). iIntros (v) "% Hf".
iApply (wp_app_vec _ _ (_::_) ((λ v, v = (λ: ["_r"], (# ;; #) ;; k' ["_r"])%V):::
vmap (λ ty (v : val), tctx_elt_interp tid (v box ty)) (fp x).(fp_tys))%I
with "[Hargs]"); first wp_done.
with "[Hargs]").
- rewrite /=. iSplitR "Hargs".
{ simpl. iApply wp_value. by unlock. }
remember (fp_tys (fp x)) as tys. clear dependent k' p HE fp x.
......@@ -270,13 +270,11 @@ Section typing.
+ iApply (wp_hasty with "HT"). iIntros (?). rewrite tctx_hasty_val. iIntros "? $".
+ iApply "IH". done.
- simpl. change (@length expr ps) with (length ps).
iIntros (vl'). inv_vec vl'=>kv vl.
iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
iIntros (vl'). inv_vec vl'=>kv vl; csimpl.
iIntros "[-> Hvl]". iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl.
revert vl fp HE. rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
{ rewrite -fmap_cons Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
{ rewrite -fmap_cons -(subst_v_eq (fb::kb::xb) (_:::_:::vl)) //. }
iNext. iMod (lft_create with "LFT") as (ϝ) "[Htk #Hinh]"; first done.
revert vl fp HE. rewrite /= -EQl=>vl fp HE. wp_rec.
iMod (lft_create with "LFT") as (ϝ) "[Htk #Hinh]"; first done.
iSpecialize ("Hf" $! x ϝ _ vl). iDestruct (HE ϝ with "HL") as "#HE'".
iMod (bor_create _ ϝ with "LFT Hκs") as "[Hκs HκsI]"; first done.
iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
......
......@@ -26,7 +26,7 @@ Section typing.
Lemma type_int_instr (z : Z) : typed_val #z int.
Proof.
iIntros (E L tid) "_ _ $ $ _". wp_value.
iIntros (E L tid) "_ _ $ $ _". iApply wp_value.
by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
......@@ -74,7 +74,7 @@ Section typing.
iIntros (tid) "_ _ $ $ [Hp1 [Hp2 _]]".
wp_apply (wp_hasty with "Hp1"). iIntros ([[]|]) "_ H1"; try done.
wp_apply (wp_hasty with "Hp2"). iIntros ([[]|]) "_ H2"; try done.
wp_op; intros _; by rewrite tctx_interp_singleton tctx_hasty_val' //.
wp_op; case_bool_decide; by rewrite tctx_interp_singleton tctx_hasty_val' //.
Qed.
Lemma type_le E L C T T' p1 p2 x e :
......
......@@ -771,8 +771,8 @@ Section arc.
iDestruct "Hown" as (???) "(_ & Hlen & _)". wp_write. iIntros "(#Hν & Hown & H†)!>".
wp_seq. wp_op. wp_op. iDestruct "Hown" as (?) "[H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as %?. rewrite Max.max_0_r.
iDestruct "Hlen" as %[= ?]. iApply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
iNext. iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
iDestruct "Hlen" as %[= ?]. wp_apply (wp_memcpy with "[$H↦1 $H↦]"); [congruence..|].
iIntros "[? Hrc']". wp_seq. iMod ("Hdrop" with "[Hrc' H†]") as "Htok".
{ unfold P2. auto with iFrame. }
wp_apply (drop_weak_spec with "[//] Htok"). unlock. iIntros ([]); last first.
{ iIntros "_". wp_if. unlock. iFrame. iExists (_::_). rewrite heap_mapsto_vec_cons.
......@@ -780,7 +780,8 @@ Section arc.
auto 10 with iFrame. }
iIntros "([H† H1] & H2 & H3)". iDestruct "H1" as (vl') "[H1 Heq]".
iDestruct "Heq" as %<-. wp_if.
wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]"). lia.
wp_apply (wp_delete _ _ _ (_::_::vl') with "[H1 H2 H3 H†]").
{ simpl. lia. }
{ rewrite 2!heap_mapsto_vec_cons shift_loc_assoc. auto with iFrame. }
iFrame. iIntros "_". iExists (_::_). rewrite heap_mapsto_vec_cons. iFrame.
iExists 1%nat, _, []. rewrite right_id_L. iFrame. iSplit; [by auto|simpl].
......@@ -818,7 +819,7 @@ Section arc.
iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [lia| |done].
wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [simpl;lia| |done].
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
iIntros (?) "_". wp_seq.
(* Finish up the proof. *)
......@@ -874,15 +875,15 @@ Section arc.
rewrite -(firstn_skipn ty.(ty_size) vl0) heap_mapsto_vec_app.
iDestruct "Hr1" as "[Hr1 Hr2]". iDestruct "Hown" as (vl) "[Hrc' Hown]".
iDestruct (ty_size_eq with "Hown") as %Hlen.
iApply (wp_memcpy with "[$Hr1 $Hrc']"); rewrite ?firstn_length_le; try lia.
iIntros "!> [Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
wp_apply (wp_memcpy with "[$Hr1 $Hrc']"); rewrite /= ?firstn_length_le; try lia.
iIntros "[Hr1 Hrc']". wp_seq. wp_bind (drop_weak _).
iMod ("Hend" with "[$H† Hrc']") as "Htok"; first by eauto.
iApply (drop_weak_spec with "Ha Htok").
iIntros "!> * Hdrop". wp_bind (if: _ then _ else _)%E.
iApply (wp_wand _ _ (λ _, True)%I with "[Hdrop]").
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [lia| |done].
wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [simpl; lia| |done].
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
iIntros (?) "_". wp_seq.
iApply (type_type _ _ _ [ rcx box (uninit 1); #r box (Σ[ ty; arc ty ]) ]
......
......@@ -27,7 +27,7 @@ Section fake_shared_box.
rewrite heap_mapsto_vec_singleton. iSplit; auto. }
iDestruct "H" as "#H". iIntros "!# * % $". iApply step_fupd_intro. set_solver.
by iApply ty_shr_mono. }
wp_seq.
do 2 wp_seq.
iApply (type_type [] _ _ [ x box (&shr{α}(box ty)) ]
with "[] LFT [] Hna HL Hk [HT]"); last first.
{ by rewrite tctx_interp_singleton tctx_hasty_val. }
......
......@@ -20,6 +20,6 @@ Section panic.
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "!# *".
inv_vec args. iIntros (tid) "LFT HE Hna HL Hk HT /=". simpl_subst.
wp_value. done.
by iApply wp_value.
Qed.
End panic.
......@@ -692,7 +692,7 @@ Section code.
wp_apply (rc_check_unique with "[$Hna $Hrc']"); first solve_ndisj.
iIntros (strong) "[Hrc Hc]". wp_let.
iDestruct "Hc" as "[[% [_ Hproto]]|[% [Hproto _]]]".
- subst strong. wp_op=>[_|?]; last done. wp_if. wp_op.
- subst strong. wp_op. wp_if. wp_op.
rewrite shift_loc_0. wp_write. wp_bind (#;;#)%E.
iApply (wp_step_fupd with "[Hproto Hrc]");
[| |by iApply ("Hproto" with "Hrc")|];
......@@ -707,7 +707,7 @@ Section code.
iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
iDestruct "Hproto" as "[(% & H↦strong & Hna)|[% Hproto]]".
+ subst. wp_op=>[_|[]//]. wp_if.
+ subst. wp_op. wp_if.
iApply (type_type _ _ _
[ r own_ptr (ty_size Σ[ ty; rc ty ]) (Σ[ ty; rc ty]);
rcx box (uninit 1);
......@@ -722,7 +722,7 @@ Section code.
iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
iApply type_jump; solve_typing.
+ rewrite (tctx_hasty_val' _ (#rc' + #2)); last done.
iDestruct "Hrc" as "[Hrc H†2]". wp_op=>[?|_]. lia. wp_if. wp_op. wp_op. wp_write.
iDestruct "Hrc" as "[Hrc H†2]". wp_op; case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
{ rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
iApply (type_type _ _ _
......@@ -731,7 +731,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
iApply type_jump; solve_typing.
- wp_op; intros Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "[Hna Hrc]".
- wp_op; case_bool_decide as Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "[Hna Hrc]".
iApply (type_type _ _ _ [ r own_ptr (ty_size Σ[ ty; rc ty ]) (uninit _);
rcx box (uninit 1); #rc' rc ty ]
with "[] LFT HE Hna HL Hk [-]"); last first.
......@@ -791,7 +791,7 @@ Section code.
- subst strong. wp_bind (#1 = #1)%E.
iApply (wp_step_fupd with "[Hproto Hrc]");
[| |by iApply ("Hproto" with "Hrc")|];
[done..|wp_op=>[_|//]; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
[done..|wp_op; iIntros "(Hty&H†&Hna&Hproto) !>"; wp_if].
rewrite <-freeable_sz_full_S, <-(freeable_sz_split _ 2 ty.(ty_size)).
iDestruct "H†" as "[H†1 H†2]". wp_bind (_<-_;;_)%E.
iApply (wp_wand with "[Hna HL Hty Hr H†2]").
......@@ -802,7 +802,7 @@ Section code.
iIntros (?) "(Hna & HL & [Hr [Hrc _]])". wp_seq.
iMod ("Hproto" with "Hna") as (weak) "[H↦weak Hproto]". wp_op. wp_read. wp_let.
iDestruct "Hproto" as "[(% & H↦strong & Hna)|[% Hproto]]".
+ subst. wp_op=>[_|[]//]. wp_if.
+ subst. wp_op. wp_if.
iApply (type_type _ _ _
[ r own_ptr (ty_size (option ty)) (option ty);
rcx box (uninit 1);
......@@ -817,7 +817,7 @@ Section code.
iApply (type_delete (Π[uninit 2;uninit ty.(ty_size)])); [solve_typing..|].
iApply type_jump; solve_typing.
+ rewrite (tctx_hasty_val' _ (#rc' + #2)); last done.
iDestruct "Hrc" as "[Hrc H†2]". wp_op=>[?|_]. lia. wp_if. wp_op. wp_op. wp_write.
iDestruct "Hrc" as "[Hrc H†2]". wp_op. case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
iMod ("Hproto" with "[H†1 H†2] H↦weak Hrc") as "Hna".
{ rewrite -freeable_sz_full_S -(freeable_sz_split _ 2 ty.(ty_size)). iFrame. }
iApply (type_type _ _ _
......@@ -825,7 +825,7 @@ Section code.
with "[] LFT HE Hna HL Hk [-]"); last first.
{ unlock. rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val. iFrame. }
iApply type_jump; solve_typing.
- wp_op; intros Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "Hna".
- wp_op; case_bool_decide as Hc; first lia. wp_if. iMod ("Hproto" with "Hrc") as "Hna".
iApply (type_type _ _ _ [ r own_ptr (ty_size (option ty)) (uninit _);
rcx box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
......@@ -882,12 +882,12 @@ Section code.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
{ (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
iLeft. by iFrame. }
iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; intros Hc.
iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; case_bool_decide as Hc.
- wp_if. iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
iDestruct "Hweak" as "[[% Hrc]|[% [Hrc _]]]".
+ subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
wp_op=>[_|//]. iIntros "(Hl† & Hty & Hna)!>". wp_if.
wp_op. iIntros "(Hl† & Hty & Hna)!>". wp_if.
iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα]"; [|iNext; iExact "Hty"|].
{ iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
......@@ -899,7 +899,7 @@ Section code.
unlock. iFrame. }
iApply (type_sum_assign (option (&uniq{_}_))); [solve_typing..|].
iApply type_jump; solve_typing.
+ wp_op=>[?|_]; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
+ wp_op; case_bool_decide; first lia. wp_if. iMod ("Hrc" with "Hl1 Hl2") as "[Hna Hrc]".
iMod ("Hclose2" with "[] [Hrc' Hrc]") as "[Hrc' Hα]".
{ iIntros "!> HX". iModIntro. iExact "HX". }
{ iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame. auto. }
......@@ -1014,12 +1014,12 @@ Section code.
wp_apply (rc_check_unique with "[$Hna Hrcown]"); first done.
{ (* Boy this is silly... *) iDestruct "Hrcown" as "[(?&?&?&?)|?]"; last by iRight.
iLeft. by iFrame. }
iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; intros Hc; wp_if.
iIntros (c) "(Hl1 & Hc)". wp_let. wp_op; case_bool_decide as Hc; wp_if.
- iDestruct "Hc" as "[[% [Hc _]]|[% _]]"; last lia. subst.
iDestruct "Hc" as (weak) "[Hl2 Hweak]". wp_op. wp_read. wp_let.
iDestruct "Hweak" as "[[% Hrc]|[% [_ Hrc]]]".
+ subst. wp_bind (#1 = #1)%E. iApply (wp_step_fupd with "Hrc"); [done..|].
wp_op=>[_|//]. iIntros "(Hl† & Hty & Hna)!>". wp_if.
wp_op. iIntros "(Hl† & Hty & Hna)!>". wp_if.
iMod ("Hclose2" with "[Hrc' Hl1 Hl2 Hl†] [Hty]") as "[Hty Hα1]"; [|iNext; iExact "Hty"|].
{ iIntros "!> Hty". iExists [_]. rewrite heap_mapsto_vec_singleton. iFrame "Hrc'".
iLeft. by iFrame. }
......@@ -1031,7 +1031,7 @@ Section code.
tctx_hasty_val' //. unlock. iFrame. }
iApply type_assign; [solve_typing..|].
iApply type_jump; solve_typing.
+ wp_op; [lia|move=>_]. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
+ wp_op; case_bool_decide; first lia. wp_if. wp_op. rewrite shift_loc_0. wp_write. wp_op.
wp_op. wp_write. wp_bind (new _). iSpecialize ("Hrc" with "Hl1 Hl2").
iApply (wp_step_fupd with "Hrc"); [done..|]. iApply wp_new; first lia. done.
rewrite -!lock Nat2Z.id.
......
......@@ -164,7 +164,7 @@ Section code.
- (* Success case. *)
iDestruct "Hrcst" as (qb) "(Hl'1 & Hl'2 & Hl'† & >Hq''q0 & [Hν1 Hν2] & Hν†)".
iDestruct "Hq''q0" as %Hq''q0.
wp_read. wp_let. wp_op=>[//|_]. wp_if. wp_op. rewrite shift_loc_0. wp_op. wp_write.
wp_read. wp_let. wp_op. wp_if. wp_op. rewrite shift_loc_0. wp_op. wp_write.
(* Closing the invariant. *)
iMod (own_update with "Hrc●") as "[Hrc● Hrctok2]".
{ apply auth_update_alloc, prod_local_update_1,
......@@ -192,7 +192,7 @@ Section code.
iApply type_jump; solve_typing.
- (* Failure : dropping *)
(* TODO : The two failure cases are almost identical. *)
iDestruct "Hrcst" as "[Hl'1 Hl'2]". wp_read. wp_let. wp_op=>[_|//]. wp_if.
iDestruct "Hrcst" as "[Hl'1 Hl'2]". wp_read. wp_let. wp_op. wp_if.
(* Closing the invariant. *)
iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc● Hl'1 Hl'2 $Hna]") as "Hna".
......@@ -208,7 +208,7 @@ Section code.
iApply type_jump; solve_typing.
- (* Failure : general case *)
destruct weakc as [|weakc]; first by simpl in *; lia.
iDestruct "Hrcst" as "[Hl'1 Hrcst]". wp_read. wp_let. wp_op=>[_|//]. wp_if.
iDestruct "Hrcst" as "[Hl'1 Hrcst]". wp_read. wp_let. wp_op. wp_if.
(* Closing the invariant. *)
iMod ("Hclose3" with "[$Hwtok] Hna") as "[Hα1 Hna]".
iMod ("Hclose2" with "[Hrc● Hl'1 Hrcst $Hna]") as "Hna".
......@@ -421,7 +421,7 @@ Section code.
+ iRight. iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose".
iFrame. iExists _. iFrame. simpl. destruct Pos.of_succ_nat; try done.
by rewrite /= Pos.pred_double_succ. }
- subst. wp_read. wp_let. wp_op=>[_|//]. wp_if.
- subst. wp_read. wp_let. wp_op. wp_if.
iApply (type_type _ _ _ [ w box (uninit 1); #lw box (uninit (2 + ty.(ty_size))) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
......@@ -431,7 +431,7 @@ Section code.
iIntros "!> !%". simpl. congruence. }
iApply type_delete; [try solve_typing..|].
iApply type_jump; solve_typing.
- wp_read. wp_let. wp_op=>[|_]; first lia. wp_if. wp_op. wp_op. wp_write.
- wp_read. wp_let. wp_op; case_bool_decide; first lia. wp_if. wp_op. wp_op. wp_write.
iMod ("Hclose" with "Hlw") as "Hna".
iApply (type_type _ _ _ [ w box (uninit 1) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
......
......@@ -157,7 +157,7 @@ Section refcell_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[[Hβtok1 Hβtok2] Hclose']". done.
iMod (na_bor_acc with "LFT Hinv Hβtok1 Hna") as "(INV & Hna & Hclose'')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op=>?; wp_if.
iDestruct "INV" as (st) "(Hlx & Hownst & Hst)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- iMod ("Hclose''" with "[Hlx Hownst Hst] Hna") as "[Hβtok1 Hna]";
first by iExists st; iFrame.
iMod ("Hclose'" with "[$Hβtok1 $Hβtok2]") as "Hα".
......@@ -264,7 +264,7 @@ Section refcell_functions.
iMod (lctx_lft_alive_tok α with "HE HL") as (qα) "(Hα & HL & Hclose)"; [solve_typing..|].
iMod (lft_incl_acc with "Hαβ Hα") as (qβ) "[Hβtok Hclose']". done.
iMod (na_bor_acc with "LFT Hinv Hβtok Hna") as "(INV & Hna & Hclose'')"; try done.
iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op=>?; wp_if.
iDestruct "INV" as (st) "(Hlx & Hownst & Hb)". wp_read. wp_let. wp_op; case_bool_decide; wp_if.
- wp_write. wp_apply wp_new; [done..|].
iIntros (lref) "(H† & Hlref)". wp_let.
rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
......
......@@ -166,7 +166,7 @@ Section rwlock_functions.
iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & INV)". wp_read.
iMod ("Hclose''" with "[Hlx INV]") as "Hβtok1"; first by iExists _; iFrame.
iModIntro. wp_let. wp_op=>Hm1; wp_if.
iModIntro. wp_let. wp_op; case_bool_decide as Hm1; wp_if.
- iMod ("Hclose'" with "[$]") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _
[ x box (&shr{α}(rwlock ty)); r box (uninit 2) ]
......@@ -179,7 +179,7 @@ Section rwlock_functions.
iMod (at_bor_acc_tok with "LFT Hinv Hβtok1") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st') "(Hlx & Hownst & Hst)". revert Hm1.
destruct (decide (Z_of_rwlock_st st = Z_of_rwlock_st st')) as [->|?]=>?.
+ iApply (wp_cas_int_suc with "Hlx"); first done. iNext. iIntros "Hlx".
+ iApply (wp_cas_int_suc with "Hlx"). iNext. iIntros "Hlx".
iAssert ( qν ν, (qβ / 2).[β] (qν).[ν]
ty_shr ty (β ν) tid (lx + 1)
own γ ( reading_st qν ν) rwlock_inv tid lx γ β ty
......@@ -273,7 +273,7 @@ Section rwlock_functions.
wp_bind (CAS _ _ _).
iMod (at_bor_acc_tok with "LFT Hinv Hβtok") as "[INV Hclose'']"; try done.
iDestruct "INV" as (st) "(Hlx & >Hownst & Hst)". destruct st.
- iApply (wp_cas_int_fail with "Hlx"). done. by destruct c as [|[[]]|].
- iApply (wp_cas_int_fail with "Hlx"). by destruct c as [|[[]]|].
iNext. iIntros "Hlx".
iMod ("Hclose''" with "[Hlx Hownst Hst]") as "Hβtok"; first by iExists _; iFrame.
iMod ("Hclose'" with "Hβtok") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
......@@ -285,7 +285,7 @@ Section rwlock_functions.
iApply (type_sum_unit (option $ rwlockwriteguard α ty));
[solve_typing..|]; first last.
rewrite /option /=. iApply type_jump; solve_typing.
- iApply (wp_cas_int_suc with "Hlx"). done. iIntros "!> Hlx".
- iApply (wp_cas_int_suc with "Hlx"). iIntros "!> Hlx".
iMod (own_update with "Hownst") as "[Hownst ?]".
{ by eapply auth_update_alloc, (op_local_update_discrete _ _ writing_st). }
iMod ("Hclose''" with "[Hlx Hownst]") as "Hβtok". { iExists _. iFrame. }
......
......@@ -123,7 +123,7 @@ Section rwlockreadguard_functions.
iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (wp_if _ true). iIntros "!>!>".
iModIntro. wp_if.
iApply (type_type _ _ _ [ x box (uninit 1)]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_singleton tctx_hasty_val //. }
......@@ -133,7 +133,7 @@ Section rwlockreadguard_functions.
+ iApply (wp_cas_int_fail with "Hlx"); try done. iNext. iIntros "Hlx".
iMod ("Hcloseβ" with "[Hlx H● Hst]") as "Hβ". by iExists _; iFrame.
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL".
iApply (wp_if _ false). iIntros "!> !>".
iModIntro. wp_if.
iApply (type_type _ _ _ [ x box (uninit 1); #lx' rwlockreadguard α ty]
with "[] LFT HE Hna HL Hk"); first last.
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
......
......@@ -49,8 +49,7 @@ Section code.
(* Prove the continuation of the function call. *)
iIntros (r) "Hna Hϝ Hr". simpl.
iDestruct (ownptr_own with "Hr") as (lr rvl) "(% & Hlr & Hrvl & Hlr†)". subst r.
iApply wp_rec; try (done || apply _).
{ repeat econstructor. } simpl_subst. iNext.
wp_rec.
rewrite (right_id static).
wp_apply (wp_memcpy with "[$Hx'↦ $Hlr]"); [by auto using vec_to_list_length..|].
iIntros "[Hlx' Hlr]". wp_seq.
......
......@@ -117,8 +117,8 @@ Section typing_rules.
iIntros (Hc) "He He'". iIntros (tid) "#LFT #HE Htl HL HC HT". rewrite tctx_interp_app.
iDestruct "HT" as "[HT1 HT]". wp_bind e. iApply (wp_wand with "[He HL HT1 Htl]").
{ iApply ("He" with "LFT HE Htl HL HT1"). }
iIntros (v) "/= (Htl & HL & HT2)". iApply wp_let; first wp_done.
iModIntro. iApply ("He'" with "LFT HE Htl HL HC [HT2 HT]").
iIntros (v) "/= (Htl & HL & HT2)". wp_let.
iApply ("He'" with "LFT HE Htl HL HC [HT2 HT]").
rewrite tctx_interp_app. by iFrame.
Qed.
......
......@@ -47,10 +47,8 @@ Section type_soundness.
iDestruct "Hmain" as (?) "[EQ Hmain]".
rewrite eval_path_of_val. iDestruct "EQ" as %[= <-].
iDestruct "Hmain" as (f k x e ?) "(EQ & % & Hmain)". iDestruct "EQ" as %[= ->].