Commit 30664fa6 authored by Ralf Jung's avatar Ralf Jung

make thinsg work with a recent version of Iris

parent 0a54775b
Pipeline #3313 passed with stages
in 7 minutes and 17 seconds
Subproject commit e3cb5b14e01ac2b349516f084e7def4bf7283ab9
Subproject commit b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39
......@@ -15,31 +15,31 @@ Section incr.
then "oldv" (* return old value if success *)
else "incr" "l".
Global Opaque incr.
(* TODO: Can we have a more WP-style definition and avoid the equality? *)
Definition incr_triple (l: loc) :=
atomic_triple (fun (v: Z) => l #v)%I
(fun v ret => ret = #v l #(v + 1))%I
(nclose heapN)
(fun v ret => ret = #v l #(v + 1))%I
(incr #l).
Lemma incr_atomic_spec: (l: loc), heapN N heap_ctx incr_triple l.
Lemma incr_atomic_spec: (l: loc), incr_triple l.
Proof.
iIntros (l HN) "#?".
iIntros (l).
rewrite /incr_triple.
rewrite /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH".
iIntros "!# HP".
wp_rec.
wp_bind (! _)%E.
(* FIXME: I should not have to apply wp_atomic manually here and below. *)
wp_bind (! _)%E. iApply (wp_atomic _ ); first by eauto.
iMod ("Hvs" with "HP") as (x) "[Hl [Hvs' _]]".
wp_load.
iModIntro. wp_load.
iMod ("Hvs'" with "Hl") as "HP".
iModIntro. wp_let. wp_bind (CAS _ _ _). wp_op.
iMod ("Hvs" with "HP") as (x') "[Hl Hvs']".
iApply (wp_atomic _ ); first by eauto.
iMod ("Hvs" with "HP") as (x') "[Hl Hvs']". iModIntro.
destruct (decide (x = x')).
- subst.
iDestruct "Hvs'" as "[_ Hvs']".
......@@ -66,38 +66,36 @@ Section user.
(* prove that incr is safe w.r.t. data race. TODO: prove a stronger post-condition *)
Lemma incr_2_safe:
(x: Z), heapN N -> heap_ctx WP incr_2 #x {{ _, True }}.
(x: Z), (WP incr_2 #x {{ _, True }})%I.
Proof.
iIntros (x HN) "#Hh".
rewrite /incr_2.
wp_let.
iIntros (x). iProof. (* FIXME: I did iIntros, this should not be needed. *)
rewrite /incr_2 /=.
wp_lam.
wp_alloc l as "Hl".
iMod (inv_alloc N _ (x':Z, l #x')%I with "[Hl]") as "#?"; first eauto.
wp_let.
wp_bind (_ ||| _)%E.
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[]").
iFrame "Hh".
(* prove worker triple *)
iDestruct (incr_atomic_spec N l with "Hh") as "Hincr"=>//.
rewrite /incr_triple /atomic_triple.
iSpecialize ("Hincr" $! True%I (fun _ => True%I) with "[]").
- iIntros "!# _".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iMod (fupd_intro_mask' ( nclose N) heapN) as "Hvs"; first set_solver.
iModIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
- iDestruct "Hincr" as "#HIncr".
iSplitL; [|iSplitL];
try (iApply wp_wand_r; iSplitL; [by iApply "HIncr"|auto]).
iIntros (v1 v2) "_ !>".
wp_seq. iInv N as (x') ">Hl" "Hclose".
wp_load. iApply "Hclose". eauto.
iAssert ( WP incr #l {{ _, True }})%I as "#?".
{ (* prove worker triple *)
iDestruct (incr_atomic_spec l) as "Hincr"=>//.
rewrite /incr_triple /atomic_triple.
iSpecialize ("Hincr" $! True%I (fun _ => True%I) with "[]").
- iIntros "!# _".
(* open the invariant *)
iInv N as (x') ">Hl'" "Hclose".
(* mask magic *)
iMod (fupd_intro_mask' _ ) as "Hvs"; first set_solver.
iModIntro. iExists x'. iFrame "Hl'". iSplit.
+ (* provide a way to rollback *)
iIntros "Hl'".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
+ (* provide a way to commit *)
iIntros (v) "[Heq Hl']".
iMod "Hvs". iMod ("Hclose" with "[Hl']"); eauto.
- iDestruct "Hincr" as "#HIncr". iAlways. by iApply "HIncr". }
iApply (wp_par (λ _, True%I) (λ _, True%I) with "[] []"); [done..|].
iIntros (v1 v2) "_ !>".
wp_seq. iInv N as (x') ">Hl" "Hclose".
wp_load. iApply "Hclose". eauto.
Qed.
End user.
......@@ -19,17 +19,17 @@ Section atomic_pair.
Local Opaque pcas_seq.
Definition α (x: val) (_: val) : iProp Σ := ( a b: val, x = (a, b)%V)%I.
Definition α (x: val) (_: val) : iProp Σ := ( a b: val, x = (a, b)%V)%I.
Definition ϕ (ls: val) (xs: val) : iProp Σ :=
( (l1 l2: loc) (x1 x2: val),
ls = (#l1, #l2)%V xs = (x1, x2)%V l1 x1 l2 x2)%I.
ls = (#l1, #l2)%V xs = (x1, x2)%V l1 x1 l2 x2)%I.
Definition β (ab: val) (xs xs': val) (v: val) : iProp Σ :=
( a b x1 x2 x1' x2': val,
a b x1 x2 x1' x2': val,
ab = (a, b)%V xs = (x1, x2)%V xs' = (x1', x2')%V
((v = #true x1 = a x2 = a x1' = b x2' = b)
(v = #false (x1 a x2 a) xs = xs')))%I.
(v = #false (x1 a x2 a) xs = xs'))%I.
Local Opaque β.
......
......@@ -13,7 +13,7 @@ Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
Proof. by intros ?%subG_inG. Qed.
Section atomic_sync.
Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))} (N : namespace).
Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))}.
(* TODO: Rename and make opaque; the fact that this is a half should not be visible
to the user. *)
......@@ -41,16 +41,15 @@ Section atomic_sync.
Definition atomic_syncer_spec (mk_syncer: val) :=
(g0: A) (ϕ: A iProp Σ),
heapN N
{{{ heap_ctx ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 is_atomic_syncer ϕ γ s }}}.
{{{ ϕ g0 }}} mk_syncer #() {{{ γ s, RET s; gHalf γ g0 is_atomic_syncer ϕ γ s }}}.
Lemma atomic_spec (mk_syncer: val):
mk_syncer_spec N mk_syncer atomic_syncer_spec mk_syncer.
mk_syncer_spec mk_syncer atomic_syncer_spec mk_syncer.
Proof.
iIntros (Hsync g0 ϕ HN ret) "[#Hh Hϕ] Hret".
iIntros (Hsync g0 ϕ ret) "Hϕ Hret".
iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
{ by rewrite pair_op dec_agree_idemp. }
iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[$Hh Hg1 Hϕ]")=>//.
iApply (Hsync ( g: A, ϕ g gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
{ iExists g0. by iFrame. }
iNext. iIntros (s) "#Hsyncer". iApply "Hret".
iSplitL "Hg2"; first done. iIntros "!#".
......
......@@ -80,7 +80,7 @@ Section evmapR.
Lemma map_agree_eq' γm m hd x agy:
m !! hd = Some ((), agy)
ev γm hd x own γm ( m) DecAgree x = agy.
ev γm hd x own γm ( m) DecAgree x = agy.
Proof.
iIntros (?) "[#Hev Hom]".
iCombine "Hom" "Hev" as "Hauth".
......@@ -99,7 +99,7 @@ Section evmapR.
(* Evidence is the witness of membership *)
Lemma ev_map_witness γm m hd x:
ev γm hd x own γm ( m) m !! hd = Some (, DecAgree x).
ev γm hd x own γm ( m) m !! hd = Some (, DecAgree x).
Proof.
iIntros "[#Hev Hom]".
destruct (m !! hd) as [[[] agy]|] eqn:Heqn.
......@@ -109,7 +109,7 @@ Section evmapR.
(* Two evidences coincides *)
Lemma evmap_frag_agree_split γm p (a1 a2: A):
ev γm p a1 ev γm p a2 a1 = a2.
ev γm p a1 ev γm p a2 a1 = a2.
Proof.
iIntros "[Ho Ho']".
destruct (decide (a1 = a2)) as [->|Hneq].
......
......@@ -47,21 +47,19 @@ Definition mk_flat : val :=
let: "r" := loop "p" "s" "lk" in
"r".
Global Opaque doOp try_srv install loop mk_flat.
Definition reqR := prodR fracR (dec_agreeR val). (* request x should be kept same *)
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *)
Class flatG Σ := FlatG {
req_G :> inG Σ reqR;
tok_G :> inG Σ (authR tokmR);
sp_G :> savedPropG Σ (cofe_funCF val idCF)
sp_G :> savedPropG Σ (ofe_funCF val idCF)
}.
Definition flatΣ : gFunctors :=
#[ GFunctor (constRF reqR);
GFunctor (constRF (authR tokmR));
savedPropΣ (cofe_funCF val idCF)
savedPropΣ (ofe_funCF val idCF)
].
Instance subG_flatΣ {Σ} : subG flatΣ Σ flatG Σ.
......@@ -94,7 +92,7 @@ Section proof.
(* p slot invariant *)
Definition p_inv R (γm γr: gname) (v: val) :=
( (ts: toks) (p : loc),
v = #p evm γm p ts
v = #p evm γm p ts
((* INIT *)
( y: val, p {1/2} InjRV y init_s ts)
(* INSTALLED *)
......@@ -111,17 +109,16 @@ Section proof.
Lemma install_push_spec R
(p: loc) (γs γm γr: gname) (ts: toks)
(s: loc) (f x: val) (Φ: val iProp Σ) :
heapN N
heap_ctx inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
evm γm p ts installed_s R ts f x
p {1/2} InjLV (f, x) (( hd, evs γs hd #p) - Φ #())
WP push #s #p {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & #? & Hpm & Hs & Hp & HΦ)".
iIntros "(#? & Hpm & Hs & Hp & HΦ)".
rewrite /srv_stack_inv.
iDestruct (push_spec N (p_inv R γm γr) (fun v => ( hd, evs γs hd #p) v = #())%I
iDestruct (push_spec N (p_inv R γm γr) (fun v => ( hd, evs γs hd #p) v = #())%I
with "[-HΦ]") as "Hpush"=>//.
- iFrame "Hh". iSplitL "Hp Hs Hpm"; last eauto.
- iSplitL "Hp Hs Hpm"; last eauto.
iExists ts. iExists p. iSplit=>//. iFrame "Hpm".
iRight. iLeft. iExists f, x. iFrame.
- iApply wp_wand_r.
......@@ -138,26 +135,25 @@ Section proof.
R P Q
(f x: val) (γs γm γr: gname) (s: loc)
(Φ: val iProp Σ):
heapN N
heap_ctx inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
P ({{ R P }} f x {{ v, R Q v }})
( (p: loc) (ts: toks), installed_recp ts x Q - evm γm p ts -( hd, evs γs hd #p) - Φ #p)
WP install f x #s {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & #? & Hpx & Hf & HΦ)".
iIntros "(#? & Hpx & Hf & HΦ)".
wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
iApply fupd_wp.
iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
iMod (saved_prop_alloc (F:=(cofe_funCF val idCF)) Q) as (γq) "#?".
iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?".
iInv N as "[Hrs >Hm]" "Hclose".
iDestruct "Hm" as (m) "[Hm HRm]".
destruct (m !! p) eqn:Heqn.
- (* old name *)
iDestruct (big_sepM_delete (fun p _ => v : val, p {1 / 2} v)%I m with "HRm") as "[Hp HRm]"=>//.
iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hh Hl Hp". auto.
iDestruct "Hp" as (?) "Hp". iExFalso. iApply bogus_heap; last by iFrame "Hl Hp". auto.
- (* fresh name *)
iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as ">[Hm1 #Hm2]"=>//.
iDestruct "Hl" as "[Hl1 Hl2]".
......@@ -180,18 +176,17 @@ Section proof.
Qed.
Lemma loop_iter_doOp_spec R (s hd: loc) (γs γm γr: gname) xs Φ:
heapN N
heap_ctx inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm) own γr (Excl ()) R
inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm) own γr (Excl ()) R
is_list' γs hd xs (own γr (Excl ()) - R - Φ #())
WP iter #hd doOp {{ Φ }}.
Proof.
iIntros (HN) "(#Hf & #? & Ho2 & HR & Hlist' & HΦ)".
iIntros "(#? & Ho2 & HR & Hlist' & HΦ)".
iApply (iter_spec N (p_inv R γm γr) Φ
(* (fun v => v = #() own γr (Excl ()) R)%I *)
γs s (own γr (Excl ()) R)%I (srv_tokm_inv γm) xs hd doOp doOp
with "[-]")=>//.
- rewrite /f_spec.
iIntros (Φ' x _) "(#Hh & #? & Hev & [Hor HR] & HΦ')".
iIntros (Φ' x) "(#? & Hev & [Hor HR] & HΦ')".
iDestruct "Hev" as (xhd) "#Hev".
wp_rec. wp_bind (! _)%E. iInv N as "[Hs >Hm]" "Hclose".
iDestruct "Hs" as (gxs ghd) "[>Hghd [>Hgxs HRs]]". (* global xs, hd *)
......@@ -250,8 +245,9 @@ Section proof.
iDestruct (ev_map_witness _ _ _ m2 with "[Hevm Hom2]") as %?; first by iFrame.
iDestruct (big_sepM_delete _ m2 with "HRp") as "[HRk HRp]"=>//.
iDestruct "HRk" as (?) "HRk".
iDestruct (heap_mapsto_op_1 with "[HRk Hp]") as "[% Hp]"; first by iFrame.
rewrite Qp_div_2. wp_store.
(* FIXME: Giving the types here should not be necessary. *)
iDestruct (@mapsto_agree loc val with "[$HRk $Hp]") as %->.
iCombine "HRk" "Hp" as "Hp". wp_store.
(* now close the invariant *)
iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ']").
......@@ -259,6 +255,7 @@ Section proof.
iAssert (srv_tokm_inv γm) with "[Hp1 HRp Hom2]" as "HRp".
{ iExists m2. iFrame. iApply (big_sepM_delete _ m2)=>//.
iFrame. eauto. }
(* FIXME: These iFrame are really slow. *)
iFrame. iExists xs''. iFrame. iExists hd'''. iFrame.
iExists m'. iFrame.
iDestruct (big_sepM_delete _ m' with "[-]") as "?"=>//.
......@@ -299,12 +296,11 @@ Section proof.
( Q, own γx ((1 / 2)%Qp, DecAgree x) saved_prop_own γq (Q x) Q x y)%I.
Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ :
heapN N
heap_ctx inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
is_lock N γlk lk (own γr (Excl ()) R) Φ #()
WP try_srv lk #s {{ Φ }}.
Proof.
iIntros (?) "(#? & #? & #? & HΦ)".
iIntros "(#? & #? & HΦ)".
wp_seq. wp_let.
wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
iNext. iIntros ([]); last by (iIntros; wp_if).
......@@ -319,7 +315,7 @@ Section proof.
iModIntro. wp_let.
wp_bind (iter _ _).
iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
{ iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) R v = #()))%I=>//.
{ iApply (loop_iter_doOp_spec R _ _ _ _ _ _ (fun v => own γr (Excl ()) R v = #()))%I=>//.
iFrame "#". iFrame. iIntros "? ?". by iFrame. }
iIntros (f') "[Ho [HR %]]". subst.
wp_let. iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
......@@ -328,14 +324,13 @@ Section proof.
Lemma loop_spec R (p s: loc) (lk: val)
(γs γr γm γlk: gname) (ts: toks) Φ:
heapN N
heap_ctx inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
inv N (srv_stack_inv R γs γm γr s srv_tokm_inv γm)
is_lock N γlk lk (own γr (Excl ()) R)
own_γ3 ts evm γm p ts
( hd, evs γs hd #p) ( x y, finished_recp ts x y - Φ y)
WP loop #p #s lk {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & #? & #? & Ho3 & #Hev & Hhd & HΦ)".
iIntros "(#? & #? & Ho3 & #Hev & Hhd & HΦ)".
iLöb as "IH". wp_rec. repeat wp_let.
wp_bind (! _)%E. iInv N as "[Hinv >?]" "Hclose".
iDestruct "Hinv" as (xs hd) "[>Hs [>Hxs HRs]]".
......@@ -390,19 +385,19 @@ Section proof.
rewrite /ev. eauto.
Qed.
Lemma mk_flat_spec: mk_syncer_spec N mk_flat.
Lemma mk_flat_spec: mk_syncer_spec mk_flat.
Proof.
iIntros (R HN Φ) "(#Hh & HR) HΦ".
iIntros (R Φ) "HR HΦ".
iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
iMod (own_alloc ( (: tokmR) )) as (γm) "[Hm _]"; first by rewrite -auth_both_op.
iAssert (srv_tokm_inv γm) with "[Hm]" as "Hm"; first eauto.
{ iExists . iFrame. by rewrite big_sepM_empty. }
wp_seq. wp_bind (newlock _).
iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Hh $Ho2 $HR]")=>//.
iApply (newlock_spec _ (own γr (Excl ()) R)%I with "[$Ho2 $HR]")=>//.
iNext. iIntros (lk γlk) "#Hlk".
wp_let. wp_bind (new_stack _).
iApply (new_stack_spec' _ (p_inv _ γm γr))=>//.
iFrame "Hh Hm". iIntros (γ s) "#Hss".
iFrame "Hm". iIntros (γ s) "#Hss".
wp_let. iApply "HΦ". rewrite /synced.
iAlways.
iIntros (f). wp_let. iAlways.
......
......@@ -4,7 +4,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
From iris.algebra Require Import auth frac gmap dec_agree.
From iris.prelude Require Import countable.
From iris.base_logic Require Import big_op auth.
From iris.base_logic Require Import big_op auth fractional.
Import uPred.
Section lemmas.
......@@ -33,13 +33,11 @@ Section heap_extra.
Lemma bogus_heap p (q1 q2: Qp) a b:
~((q1 + q2)%Qp 1%Qp)%Qc
heap_ctx p {q1} a p {q2} b False.
p {q1} a p {q2} b False.
Proof.
iIntros (?) "(#Hh & Hp1 & Hp2)".
iCombine "Hp1" "Hp2" as "Hp".
iDestruct (heap_mapsto_op_1 with "Hp") as "[_ Hp]".
rewrite heap_mapsto_eq. iDestruct (auth_own_valid with "Hp") as %H'.
apply singleton_valid in H'. by destruct H' as [H' _].
iIntros (?) "Hp".
(* FIXME: If I dont give the types here, it loops. *)
iDestruct (@mapsto_valid_2 loc val with "Hp") as %H'. done.
Qed.
End heap_extra.
......@@ -65,7 +63,7 @@ Section pair.
Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}.
Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, DecAgree a1) own γm (q2, DecAgree a2) (a1 = a2).
own γm (q1, DecAgree a1) own γm (q2, DecAgree a2) a1 = a2.
Proof.
iIntros "[Ho Ho']".
destruct (decide (a1 = a2)) as [->|Hneq]=>//.
......@@ -77,7 +75,7 @@ Section pair.
Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
own γm (q1, DecAgree a1) own γm (q2, DecAgree a2)
own γm ((q1 + q2)%Qp, DecAgree a1) (a1 = a2).
own γm ((q1 + q2)%Qp, DecAgree a1) a1 = a2.
Proof.
iIntros "[Ho Ho']".
iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
......
......@@ -36,7 +36,7 @@ Section defs.
iApply IHxs'=>//.
Qed.
Definition perR' hd v v' := (v = ((: unitR), DecAgree v') R v' allocated hd)%I.
Definition perR' hd v v' := (v = ((: unitR), DecAgree v') R v' allocated hd)%I.
Definition perR hd v := ( v', perR' hd v v')%I.
Definition allR γ := ( m : evmapR loc val unitR, own γ ( m) [ map] hd v m, perR hd v)%I.
......@@ -51,24 +51,24 @@ Section defs.
Proof. apply _. Qed.
Lemma dup_is_list' γ : xs hd,
heap_ctx is_list' γ hd xs |==> is_list' γ hd xs is_list' γ hd xs.
is_list' γ hd xs |==> is_list' γ hd xs is_list' γ hd xs.
Proof.
induction xs as [|y xs' IHxs'].
- iIntros (hd) "(#? & Hs)".
- iIntros (hd) "Hs".
simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- iIntros (hd) "(#? & Hs)". simpl.
- iIntros (hd) "Hs". simpl.
iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hev & Hs')".
iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
Qed.
Lemma extract_is_list γ : xs hd,
heap_ctx is_list' γ hd xs |==> is_list' γ hd xs is_list hd xs.
is_list' γ hd xs |==> is_list' γ hd xs is_list hd xs.
Proof.
induction xs as [|y xs' IHxs'].
- iIntros (hd) "(#? & Hs)".
- iIntros (hd) "Hs".
simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- iIntros (hd) "(#? & Hs)". simpl.
- iIntros (hd) "Hs". simpl.
iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hev & Hs')".
iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
iModIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
......@@ -77,8 +77,7 @@ Section defs.
Definition f_spec γ (xs: list val) (s: loc) (f: val) (Rf RI: iProp Σ) :=
(* Rf, RI is some frame *)
Φ (x: val),
heapN N
heap_ctx inv N (( xs, is_stack' γ xs s) RI) ( hd, evs γ hd x)
inv N (( xs, is_stack' γ xs s) RI) ( hd, evs γ hd x)
Rf (Rf - Φ #())
WP f x {{ Φ }}.
End defs.
......@@ -88,11 +87,10 @@ Section proofs.
Context (R: val iProp Σ).
Lemma new_stack_spec' Φ RI:
heapN N
heap_ctx RI ( γ s : loc, inv N (( xs, is_stack' R γ xs s) RI) - Φ #s)
RI ( γ s : loc, inv N (( xs, is_stack' R γ xs s) RI) - Φ #s)
WP new_stack #() {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & HR & HΦ)". iApply wp_fupd.
iIntros "(HR & HΦ)". iApply wp_fupd.
iMod (own_alloc ( (: evmapR loc val unitR) )) as (γ) "[Hm Hm']".
{ apply auth_valid_discrete_2. done. }
wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
......@@ -107,16 +105,16 @@ Lemma new_stack_spec' Φ RI:
Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
xs hd (f: expr) (f': val),
heapN N f_spec N R γ xs s f' Rf RI to_val f = Some f'
heap_ctx inv N (( xs, is_stack' R γ xs s) RI)
f_spec N R γ xs s f' Rf RI to_val f = Some f'
inv N (( xs, is_stack' R γ xs s) RI)
is_list' γ hd xs Rf (Rf - Φ #())
WP (iter #hd) f {{ v, Φ v }}.
Proof.
induction xs as [|x xs' IHxs'].
- simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
- simpl. iIntros (hd f f' ? ?) "(#? & Hxs1 & HRf & HΦ)".
iDestruct "Hxs1" as (q) "Hhd".
wp_rec. wp_value. wp_let. wp_load. wp_match. by iApply "HΦ".
- simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
- simpl. iIntros (hd f f' Hf ?) "(#? & Hxs1 & HRf & HΦ)".
iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
wp_rec. wp_value. wp_let. wp_load. wp_match. wp_proj.
wp_bind (f' _). iApply Hf=>//. iFrame "#".
......@@ -127,13 +125,12 @@ Lemma new_stack_spec' Φ RI:
Qed.
Lemma push_spec Φ γ (s: loc) (x: val) RI:
heapN N
heap_ctx R x inv N (( xs, is_stack' R γ xs s) RI) (( hd, evs γ hd x) - Φ #())
R x inv N (( xs, is_stack' R γ xs s) RI) (( hd, evs γ hd x) - Φ #())
WP push #s x {{ Φ }}.
Proof.
iIntros (HN) "(#Hh & HRx & #? & HΦ)".
iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
iSpecialize ("Hpush" $! (R x) (fun ret => ( hd, evs γ hd x) ret = #())%I with "[]").
iIntros "(HRx & #? & HΦ)".
iDestruct (push_atomic_spec s x) as "Hpush"=>//.
iSpecialize ("Hpush" $! (R x) (fun ret => ( hd, evs γ hd x) ret = #())%I with "[]").
- iIntros "!# Rx".
(* open the invariant *)
iInv N as "[IH1 ?]" "Hclose".
......@@ -141,7 +138,7 @@ Lemma new_stack_spec' Φ RI:
iDestruct (extract_is_list with "[Hxs]") as ">[Hxs Hxs']"; first by iFrame.
iDestruct (dup_is_list with "[Hxs']") as "[Hxs'1 Hxs'2]"; first by iFrame.
(* mask magic *)
iMod (fupd_intro_mask' ( nclose N) heapN) as "Hvs"; first set_solver.
iMod (fupd_intro_mask' ( nclose N) ) as "Hvs"; first set_solver.
iModIntro. iExists (xs, hd).
iFrame "Hs Hxs'1". iSplit.
+ (* provide a way to rollback *)
......@@ -156,8 +153,7 @@ Lemma new_stack_spec' Φ RI:
destruct (m !! hd') eqn:Heqn.
* iDestruct (big_sepM_delete_later (perR R) m with "HRm") as "[Hx ?]"=>//.
iDestruct "Hx" as (?) "(_ & _ & >Hhd'')".
iDestruct (heap_mapsto_op_1 with "[Hhd'1 Hhd'2]") as "[_ Hhd]"; first iFrame.
rewrite Qp_div_2.
iCombine "Hhd'1" "Hhd'2" as "Hhd".
iDestruct "Hhd''" as (q v) "Hhd''". iExFalso.
iApply (bogus_heap hd' 1%Qp q); first apply Qp_not_plus_q_ge_1.
iFrame "#". iFrame.
......
......@@ -16,16 +16,14 @@ Definition mk_sync: val :=
release "l";;
"ret".
Global Opaque mk_sync.
Section syncer.
Context `{!heapG Σ, !lockG Σ} (N: namespace).
Lemma mk_sync_spec: mk_syncer_spec N mk_sync.
Lemma mk_sync_spec: mk_syncer_spec mk_sync.
Proof.
iIntros (R HN Φ) "(#Hh & HR) HΦ".
iIntros (R Φ) "HR HΦ".
wp_seq. wp_bind (newlock _).
iApply (newlock_spec _ R with "[$Hh $HR]"); first done. iNext.
iApply (newlock_spec N R with "[HR]"); first done. iNext.
iIntros (lk γ) "#Hl". wp_let. iApply "HΦ". iIntros "!#".
iIntros (f). wp_let. iAlways.
iIntros (P Q x) "#Hf !# HP".
......
......@@ -23,6 +23,6 @@ Section sync.
( (f : val), WP s f {{ f', synced R f f' }})%I.
Definition mk_syncer_spec (mk_syncer: val) :=
(R: iProp Σ), heapN N
{{{ heap_ctx R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
(R: iProp Σ),
{{{ R }}} mk_syncer #() {{{ s, RET s; is_syncer R s }}}.
End sync.
......@@ -33,8 +33,6 @@ Definition iter: val :=
| SOME "cell" => "f" (Fst "cell") ;; "iter" (Snd "cell") "f"
end.
Global Opaque new_stack push pop iter.
Section proof.
Context `{!heapG Σ} (N: namespace).
......@@ -45,43 +43,38 @@ Section proof.
end.
Lemma dup_is_list : xs hd,
heap_ctx is_list hd xs is_list hd xs is_list hd xs.
is_list hd xs is_list hd xs is_list hd xs.
Proof.
induction xs as [|y xs' IHxs'].
- iIntros (hd) "(#? & Hs)".
- iIntros (hd) "Hs".
simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
- iIntros (hd) "(#? & Hs)". simpl.
- iIntros (hd) "Hs". simpl.
iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hs')".
iDestruct (IHxs' with "[Hs']") as "[Hs1 Hs2]"; first by iFrame.
iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
Qed.
Lemma uniq_is_list:
xs ys hd, heap_ctx is_list hd xs is_list hd ys xs = ys.
xs ys hd, is_list hd xs is_list hd ys xs = ys.
Proof.
induction xs as [|x xs' IHxs'].
- induction ys as [|y ys' IHys'].
+ auto.
+ iIntros (hd) "(#? & Hxs & Hys)".
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
iExFalso. iDestruct "Hxs" as (?) "Hhd'".
iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
{ iSplitL "Hhd"; done. }
done.
(* FIXME: If I dont give the types here and below through this file, it loops. *)
by iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %?.
- induction ys as [|y ys' IHys'].
+ iIntros (hd) "(#? & Hxs & Hys)".
+ iIntros (hd) "(Hxs & Hys)".
simpl.
iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
iDestruct "Hys" as (?) "Hhd'".
iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
{ iSplitL "Hhd"; done. }
done.
+ iIntros (hd) "(#? & Hxs & Hys)".
by iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %?.
+ iIntros (hd) "(Hxs & Hys)".
simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
iDestruct (heap_mapsto_op_1 with "[Hhd Hhd']") as "[% _]".
{ iSplitL "Hhd"; done. }
inversion H3. (* FIXME: name *)
iDestruct (@mapsto_agree loc val with "[$Hhd $Hhd']") as %[= Heq].
subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
by subst.
Qed.
......@@ -96,10 +89,9 @@ Section proof.
Lemma new_stack_spec:
(Φ: val iProp Σ),
heapN N
heap_ctx ( s, is_stack s [] - Φ #s) WP new_stack #() {{ Φ }}.
( s, is_stack s [] - Φ #s) WP new_stack #() {{ Φ }}.
Proof.
iIntros (Φ HN) "[#Hh HΦ]". wp_seq.
iIntros (Φ) "HΦ". wp_seq.
wp_bind (ref NONE)%E. wp_alloc l as "Hl".
wp_alloc l' as "Hl'".
iApply "HΦ". rewrite /is_stack. iExists l.
......@@ -112,24 +104,27 @@ Section proof.
(fun xs_hd ret =>
let '(xs, hd) := xs_hd in
hd': loc,
ret = #() s #hd' hd' SOMEV (x, #hd) is_list hd xs)%I
(nclose heapN)
ret = #() s #hd' hd' SOMEV (x, #hd) is_list hd xs)%I
(push #s x).
Lemma push_atomic_spec (s: loc) (x: val) :
heapN N heap_ctx push_triple s x.
push_triple s x.
Proof.
iIntros (HN) "#?". rewrite /