Commit caa2e4e8 authored by Robbert Krebbers's avatar Robbert Krebbers

Use new ndisj_solver.

parent e79c3919
......@@ -15,8 +15,7 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : l : loc, N L .@ l)
(HΔ : x v, PersistentP (Δ x v)) :
(HNLdisj : N L) (HΔ : x v, PersistentP (Δ x v)) :
Γ ⊢ₜ e : τ
length Γ = length vs
heap_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
......@@ -115,8 +114,7 @@ Section typed_interp.
iApply wp_atomic; cbn; eauto using to_of_val.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
......@@ -126,8 +124,7 @@ Section typed_interp.
iPvsIntro.
iInv (L .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iApply (wp_store N); auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro.
iSplitL; eauto 10.
Qed.
......
......@@ -17,14 +17,14 @@ Section Soundness.
interp (nroot .@ "Fμ,ref" .@ 1) τ free_type_context v}}.
Proof.
iIntros {H1} "Hemp".
iPvs (heap_alloc (nroot .@ "Fμ,ref" .@ 2) _ _ _ _ with "Hemp") as {H} "[Hheap Hemp]".
iPvs (heap_alloc (nroot .@ "Fμ,ref" .@ 2) with "Hemp")
as {H} "[Hheap Hemp]"; first solve_ndisj.
iApply wp_wand_l. iSplitR.
{ iIntros {v} "HΦ". iExists H. iExact "HΦ". }
rewrite -(empty_env_subst e).
iApply (@typed_interp _ _ (nroot .@ "Fμ,ref" .@ 1)
(nroot .@ "Fμ,ref" .@ 2) _ _ []); eauto.
intros l. apply ndot_preserve_disjoint_r, ndot_ne_disjoint; auto.
Unshelve. all: trivial.
solve_ndisj.
Qed.
Local Arguments of_heap : simpl never.
......@@ -42,7 +42,7 @@ Section Soundness.
τ free_type_context v)%I)
e e' (e' :: thp) h)
as [Ha|Ha]; eauto; try tauto.
- apply ucmra_unit_valid.
- done.
- iIntros "[Hp Hg]". by iApply H1.
- by rewrite of_empty_heap in Hstp.
- constructor.
......
......@@ -251,15 +251,9 @@ Section CG_Counter.
Lemma FG_counter_closed f : FG_counter.[f] = FG_counter.
Proof. asimpl; rewrite counter_read_subst; by asimpl. Qed.
Ltac prove_disj N n n' :=
let Hneq := fresh "Hneq" in
let Hdsj := fresh "Hdsj" in
assert (Hneq : n n') by omega;
set (Hdsj := ndot_ne_disjoint N n n' Hneq); set_solver_ndisj.
Lemma FG_CG_counter_refinement N Δ {HΔ : x v, PersistentP (Δ x v)} :
(@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)) HΔ).
@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
(TProd (TArrow TUnit TUnit) (TArrow TUnit TNat)) HΔ.
Proof.
(* executing the preambles *)
intros [|v vs] Hlen; simplify_eq.
......@@ -312,8 +306,7 @@ Section CG_Counter.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iApply wp_load; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iIntros "> {$Hcnt} Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_lam; trivial. asimpl. iNext.
......@@ -332,18 +325,16 @@ Section CG_Counter.
iPvs (steps_CG_locked_increment
_ _ _ _ _ _ _ _ _ with "[Hj Hl Hcnt']") as "[Hj [Hcnt' Hl]]".
{ iFrame "Hspec Hcnt' Hl Hj"; trivial. }
iApply wp_cas_suc; simpl; trivial; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iNext; iFrame "Hcnt"; iIntros "Hcnt". iPvsIntro.
iApply wp_cas_suc; simpl; trivial; [|iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_true. iNext. iApply wp_value; trivial.
iExists UnitV; iFrame; auto.
+ (* CAS fails *)
(* In this case, we perform a recursive call *)
iApply (wp_cas_fail _ _ _ _ (v n')); simpl; trivial;
[inversion 1; subst; auto | | iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iNext; iFrame "Hcnt"; iIntros "Hcnt". iPvsIntro.
[inversion 1; subst; auto | | iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iApply wp_if_false. iNext. by iApply "Hlat".
- (* refinement of read *)
......@@ -353,18 +344,15 @@ Section CG_Counter.
Transparent counter_read.
unfold counter_read at 2.
iApply wp_lam; trivial. simpl.
iNext.
iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iNext. iInv> (N .@4) as {n} "[Hl [Hcnt Hcnt']]".
iPvs (steps_counter_read (N .@ 3) with "[Hj Hcnt']") as "[Hj Hcnt']".
{ prove_disj N 3 4. }
{ solve_ndisj. }
{ by iFrame "Hspec Hcnt' Hj". }
iApply wp_load; [|iFrame "Hheap"].
{ abstract prove_disj N 2 4. }
iFrame "Hcnt"; iIntros "> Hcnt". iPvsIntro.
iApply wp_load; [|iFrame "Hheap"]. solve_ndisj.
iIntros "{$Hcnt} > Hcnt". iPvsIntro.
iSplitL "Hl Hcnt Hcnt'"; [iExists _; iFrame "Hl Hcnt Hcnt'"; trivial|].
iExists (v _); eauto.
Unshelve.
all: abstract prove_disj N 3 4.
Unshelve. solve_ndisj.
Qed.
End CG_Counter.
......
......@@ -10,12 +10,6 @@ Section Stack_refinement.
{iSTK : authG lang Σ stackUR}.
Implicit Types Δ : varC -n> bivalC -n> iPropG lang Σ.
Ltac prove_disj N n n' :=
let Hneq := fresh "Hneq" in
let Hdsj := fresh "Hdsj" in
assert (Hneq : n n') by omega;
set (Hdsj := ndot_ne_disjoint N n n' Hneq); set_solver_ndisj.
Lemma FG_CG_counter_refinement N Δ {HΔ : x vw, PersistentP (Δ x vw)} :
@bin_log_related _ _ _ N Δ [] FG_stack CG_stack
(TForall
......@@ -101,8 +95,7 @@ Section Stack_refinement.
(* refinement of push and pop *)
- iExists (_, _), (_, _); iSplit; eauto. iSplit.
+ (* refinement of push *)
iAlways. clear j K. iIntros {j K v}. destruct v as [v1 v2].
iIntros "[#Hrel Hj]". simpl.
iAlways. clear j K. iIntros {j K [v1 v2] } "[#Hrel Hj] /=".
rewrite -(FG_push_folding (Loc stk)).
iLöb as "Hlat".
rewrite {2}(FG_push_folding (Loc stk)).
......@@ -113,8 +106,8 @@ Section Stack_refinement.
iApply (@wp_bind _ _ _ [AppRCtx (LamV _)]);
iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
iInv (N .@4) as {istk v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
iApply (wp_load _ _ _ _ _ _ _). iFrame "Hheap Hstk".
iNext. iIntros "Hstk". iPvsIntro.
iApply (wp_load _ _ _ _ _ _ _).
iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro.
iSplitL "Hoe Hstk' HLK Hl Hstk".
iNext. iExists _, _, _; by iFrame "Hoe Hstk' HLK Hl Hstk".
clear v h.
......@@ -126,7 +119,7 @@ Section Stack_refinement.
iApply wp_alloc; simpl; trivial; [by rewrite to_of_val|].
iFrame "Hheap". iNext. iIntros {ltmp} "Hltmp". iPvsIntro.
iApply (@wp_bind _ _ _ [IfCtx _ _]);
iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
iApply wp_wand_l; iSplitR; [by iIntros {w} "$"|].
iInv (N .@4) as {istk2 v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
(* deciding whether CAS will succeed or fail *)
destruct (decide (istk = istk2)) as [|Hneq]; subst.
......@@ -151,7 +144,7 @@ Section Stack_refinement.
iApply wp_if_true. iNext; iApply wp_value; trivial.
iExists UnitV; eauto.
* iApply (wp_cas_fail _ _ _ _ _ _ _ _ _ _ _ _ _ _); simpl; trivial.
iFrame "Hheap Hstk". iNext. iIntros "Hstk". iPvsIntro.
iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro.
iSplitR "Hj".
{ iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
iApply wp_if_false. iNext. by iApply "Hlat".
......@@ -374,15 +367,8 @@ Section Stack_refinement.
|- to_val _ = _ => simpl; by rewrite ?to_of_val
end.
all: trivial.
all: try match goal with
|- _ _ => let H := fresh "H" in intros H; inversion H; auto
end.
all: match goal with
|- @subseteq
_ _ (nclose (?N .@ ?A))
(@difference _ _ (nclose (?N .@ ?B))) =>
abstract (prove_disj N A B)
end.
all: try match goal with |- _ _ => congruence end.
all: solve_ndisj.
Qed.
End Stack_refinement.
......
......@@ -345,20 +345,6 @@ Section typed_interp.
Unshelve. all: eauto using to_of_val.
Qed.
Lemma Disjoint_after_dot : i (l : loc * loc), i 1 N .@ i N .@ 1 .@ l.
Proof.
intros i l h.
apply ndot_preserve_disjoint_r, ndot_ne_disjoint; auto.
Qed.
Ltac SolveDisj i l :=
let Hneq := fresh "Hneq" in
let Hdsj := fresh "Hdsj" in
assert (Hneq : i 1) by omega; set (Hdsj := Disjoint_after_dot i l Hneq);
clearbody Hdsj; clear Hneq; revert Hdsj;
generalize (N .@ 1) as S1; generalize (N .@ 2) as S2;
intros S1 S2 Hsdj; set_solver_ndisj.
Lemma typed_binary_interp_Load Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' (Tref τ)) :
Δ Γ Load e log Load e' τ.
......@@ -371,14 +357,12 @@ Section typed_interp.
iTimeless "Hw2".
iPvs (step_load _ _ _ j K (l.2) 1 (w.2) _ with "[Hv Hw2]") as "[Hv Hw2]".
iFrame "Hspec Hv"; trivial.
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
SolveDisj 2 l.
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
+ iNext; iExists w; by iFrame.
+ destruct w as [w1 w2]; iExists w2; iFrame "Hv Hw3"; trivial.
(* unshelving *)
Unshelve. all: eauto using to_of_val.
SolveDisj 3 l.
Unshelve. all: eauto using to_of_val || solve_ndisj.
Qed.
Lemma typed_binary_interp_Store Δ Γ e1 e2 e1' e2' τ {HΔ : ✓✓ Δ}
......@@ -398,14 +382,12 @@ Section typed_interp.
iPvs (step_store _ _ _ j K (l.2) (z.2) (# w') w' _ _ with "[Hw Hw2]")
as "[Hw Hw2]".
iFrame "Hspec Hw Hw2"; trivial.
iApply (wp_store (N .@ 2)); auto using to_of_val.
SolveDisj 2 l.
iApply (wp_store (N .@ 2)); auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
+ iNext; iExists (w, w'); by iFrame.
+ iExists UnitV; iFrame "Hw" ; iSplit; trivial.
(* unshelving *)
Unshelve. all: eauto using to_of_val.
SolveDisj 3 l.
Unshelve. all: eauto using to_of_val || solve_ndisj.
Qed.
Lemma typed_binary_interp_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ {HΔ : ✓✓ Δ}
......@@ -433,8 +415,7 @@ Section typed_interp.
rewrite ?EqType_related_eq; trivial.
iDestruct "Hiw" as "%". iDestruct "Hw3" as "%".
repeat subst; trivial. }
iApply (wp_cas_suc (N .@ 2)); eauto using to_of_val.
SolveDisj 2 l.
iApply (wp_cas_suc (N .@ 2)); eauto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
* iExists (v true); iFrame "Hw"; eauto.
......@@ -443,13 +424,12 @@ Section typed_interp.
{ iFrame "Hspec Hu Hw2". iNext.
rewrite ?EqType_related_eq; trivial.
iDestruct "Hiw" as "%". iDestruct "Hw3" as "%"; subst; eauto. }
iApply (wp_cas_fail (N .@ 2)); eauto using to_of_val.
SolveDisj 2 l.
iApply (wp_cas_fail (N .@ 2)); eauto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL "Hw1 Hw2".
* iNext; iExists (_, _); by iFrame "Hw1 Hw2".
* iExists (v false); eauto.
(* unshelving *)
Unshelve. all: eauto using to_of_val. all: SolveDisj 3 l.
Unshelve. all: eauto using to_of_val || solve_ndisj.
Qed.
Lemma typed_binary_interp Δ Γ e τ {HΔ : x vw, PersistentP (Δ x vw)} :
......
......@@ -15,7 +15,7 @@ Section typed_interp.
Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].
Lemma typed_interp N (Δ : varC -n> valC -n> iPropG lang Σ) Γ vs e τ
(HNLdisj : l : loc, N L .@ l) (HΔ : x v, PersistentP (Δ x v)) :
(HNLdisj : N L) (HΔ : x v, PersistentP (Δ x v)) :
Γ ⊢ₜ e : τ
length Γ = length vs
heapI_ctx N [] zip_with (λ τ, interp L τ Δ) Γ vs
......@@ -134,9 +134,8 @@ Section typed_interp.
iApply wp_atomic; cbn; eauto using to_of_val.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
iFrame "Hw1". iIntros "> Hw1". iPvsIntro; iSplitL; eauto.
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial. solve_ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro; iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
smart_wp_bind (StoreRCtx _) w "#Hw" IHHtyped2; cbn. iClear "HΓ".
......@@ -145,8 +144,7 @@ Section typed_interp.
iPvsIntro.
iInv (L .@ l) as {z} "[Hz1 #Hz2]".
eapply bool_decide_spec; eauto using to_of_val.
iApply (wp_store N); auto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
iApply (wp_store N); auto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10.
- (* CAS *)
smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn.
......@@ -157,14 +155,10 @@ Section typed_interp.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]"; [cbn; eauto 10 using to_of_val|].
destruct (val_dec_eq v2 w) as [|Hneq]; subst.
+ iApply (wp_cas_suc N); eauto using to_of_val.
specialize (HNLdisj l); set_solver_ndisj.
+ iApply (wp_cas_suc N); eauto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1"; iPvsIntro.
iSplitL; [|iPvsIntro]; eauto.
+ iApply (wp_cas_fail N); eauto using to_of_val.
clear Hneq. specialize (HNLdisj l); set_solver_ndisj.
(* Weird that Hneq above makes set_solver_ndisj diverge or
take exceptionally long!?!? *)
+ iApply (wp_cas_fail N); eauto using to_of_val. solve_ndisj.
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
Qed.
End typed_interp.
......@@ -14,20 +14,19 @@ Section Soundness.
interp (nroot .@ "Fμ,ref,par" .@ 1) τ free_type_context v }}.
Proof.
iIntros {H1} "Hemp".
iPvs (heap_alloc (nroot .@ "Fμ,ref,par" .@ 2) _ _ _ _ with "Hemp")
as {H} "[Hheap Hemp]".
iPvs (heap_alloc (nroot .@ "Fμ,ref,par" .@ 2) with "Hemp")
as {H} "[Hheap Hemp]"; first solve_ndisj.
iApply wp_wand_l. iSplitR.
{ iIntros {v} "HΦ". iExists H. iExact "HΦ". }
rewrite -(empty_env_subst e).
iApply (@typed_interp _ H (nroot .@ "Fμ,ref,par" .@ 1)
(nroot .@ "Fμ,ref,par" .@ 2) _ _ []); eauto.
intros l; apply ndot_preserve_disjoint_r, ndot_ne_disjoint; auto.
Unshelve. all: trivial.
solve_ndisj.
Qed.
Theorem Soundness e τ :
[] ⊢ₜ e : τ
e' thp h, rtc step ([e], (of_heap )) (e' :: thp, h)
e' thp h, rtc step ([e], of_heap ) (e' :: thp, h)
¬reducible e' h is_Some (to_val e').
Proof.
intros H1 e' thp h Hstp Hnr.
......@@ -35,7 +34,7 @@ Section Soundness.
edestruct (@wp_adequacy_reducible lang (globalF Σ) (λ v, H,
@interp Σ H (nroot .@ "Fμ,ref,par" .@ 1) τ free_type_context v)%I
e e' (e' :: thp) h) as [Ha|Ha]; eauto; try tauto.
- apply ucmra_unit_valid.
- done.
- iIntros "[Hp Hg]". by iApply H1.
- by rewrite of_empty_heap in Hstp.
- constructor.
......
......@@ -4,4 +4,4 @@ This version is known to compile with:
- Coq 8.5pl1
- Ssreflect 1.6
- Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/26d86662
- Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/280d91b0
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment