Commit a412a684 authored by Amin Timany's avatar Amin Timany

Update to work with the latest iris

parent e79c3919
......@@ -116,7 +116,7 @@ Section typed_interp.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
specialize (HNLdisj l). auto with ndisj.
iIntros "{$Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
......@@ -127,7 +127,7 @@ Section typed_interp.
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.
specialize (HNLdisj l); auto with ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro.
iSplitL; eauto 10.
Qed.
......
......@@ -255,7 +255,7 @@ Section CG_Counter.
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.
set (Hdsj := ndot_ne_disjoint N n n' Hneq); auto with ndisj.
Lemma FG_CG_counter_refinement N Δ {HΔ : x v, PersistentP (Δ x v)} :
(@bin_log_related _ _ _ N Δ [] FG_counter CG_counter
......
......@@ -14,7 +14,7 @@ Section Stack_refinement.
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.
set (Hdsj := ndot_ne_disjoint N n n' Hneq); auto with ndisj.
Lemma FG_CG_counter_refinement N Δ {HΔ : x vw, PersistentP (Δ x vw)} :
@bin_log_related _ _ _ N Δ [] FG_stack CG_stack
......
......@@ -357,7 +357,7 @@ Section typed_interp.
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.
intros S1 S2 Hsdj; auto with ndisj.
Lemma typed_binary_interp_Load Δ Γ e e' τ {HΔ : ✓✓ Δ}
(IHHtyped : Δ Γ e log e' (Tref τ)) :
......
......@@ -135,7 +135,7 @@ Section typed_interp.
iPvsIntro.
iInv (L .@ l) as {w} "[Hw1 #Hw2]".
iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
specialize (HNLdisj l); set_solver_ndisj.
specialize (HNLdisj l); auto with ndisj.
iFrame "Hw1". iIntros "> Hw1". iPvsIntro; iSplitL; eauto.
- (* Store *)
smart_wp_bind (StoreLCtx _) v "#Hv" IHHtyped1; cbn.
......@@ -146,7 +146,7 @@ Section typed_interp.
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.
specialize (HNLdisj l); auto with ndisj.
iIntros "{$Hheap $Hz1} > Hz1". iPvsIntro. iSplitL; eauto 10.
- (* CAS *)
smart_wp_bind (CasLCtx _ _) v1 "#Hv1" IHHtyped1; cbn.
......@@ -158,11 +158,11 @@ Section typed_interp.
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.
specialize (HNLdisj l); auto with 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.
clear Hneq. specialize (HNLdisj l); auto with ndisj.
(* Weird that Hneq above makes set_solver_ndisj diverge or
take exceptionally long!?!? *)
iIntros "{$Hheap $Hw1} > Hw1". iPvsIntro. iSplitL; eauto.
......
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