diff --git a/iris b/iris
index e3cb5b14e01ac2b349516f084e7def4bf7283ab9..b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit e3cb5b14e01ac2b349516f084e7def4bf7283ab9
+Subproject commit b72a3301d7ff957cfbb06d06bba85fb4ee9a2c39
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index 0b408dad547348154d45f9f132bc2d702cc6dcb7..d3bb5777019183b5bd07568cd07c8358eae050cb 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -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.
diff --git a/theories/atomic_pcas.v b/theories/atomic_pcas.v
index 0319265b2ad213b1ef76a933086c22e51ca3917c..63358e33e6d5924c72e9cf615c70eb6241021c8f 100644
--- a/theories/atomic_pcas.v
+++ b/theories/atomic_pcas.v
@@ -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 β.
diff --git a/theories/atomic_sync.v b/theories/atomic_sync.v
index 189924157b8e06994b1fdc990c40692f750b7845..7c2906c6b86e9f13308fb5dbfb05b92ed5d1a68c 100644
--- a/theories/atomic_sync.v
+++ b/theories/atomic_sync.v
@@ -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 "!#".
diff --git a/theories/evmap.v b/theories/evmap.v
index 0a27e63ec8f101d9d242b950e0081eee503a6186..6dabdd893ef3b01cbef09a5e2fb984b7625b5032 100644
--- a/theories/evmap.v
+++ b/theories/evmap.v
@@ -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].
diff --git a/theories/flat.v b/theories/flat.v
index e9d112abae3c13d039e2ae0fa97ddec13da0475d..eeca011fe0a0f55bc661d114215efc2530d82669 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -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.
diff --git a/theories/misc.v b/theories/misc.v
index bb5703461ba386eb10e18a8d741f3dc95e43198c..deb897d64d918471233bcaa94c70ee2ed939d311 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -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.
diff --git a/theories/peritem.v b/theories/peritem.v
index c86c94fe1a69b4b28ea6b33001b5e6379fbb9a9e..a506380c8baffeeb7792e4eb8be84f2b11c8c129 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -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.
diff --git a/theories/simple_sync.v b/theories/simple_sync.v
index 0f02078edb340c0fc079d1d628b356fed578ec65..50b11a931b5b7b4e465ce5934b741b63f4fc1cca 100644
--- a/theories/simple_sync.v
+++ b/theories/simple_sync.v
@@ -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".
diff --git a/theories/sync.v b/theories/sync.v
index de42cf6c654cdf5fbd80a2609da7a72a8d500fea..a389826f4aef8e054244adf7dfaff04800237271 100644
--- a/theories/sync.v
+++ b/theories/sync.v
@@ -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.
diff --git a/theories/treiber.v b/theories/treiber.v
index bb356779cc6f24127763ceb9181af2149359d139..43b99f473d2e1aa5bd93e62e3e35fa86125bc654 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -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 /push_triple /atomic_triple.
+ iProof. rewrite /push_triple /atomic_triple.
iIntros (P Q) "#Hvs".
iLöb as "IH". iIntros "!# HP". wp_rec.
wp_let. wp_bind (! _)%E.
- iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]".
+ (* FIXME: I should not have to apply wp_atomic manually here and below. *)
+ iApply (wp_atomic _ ∅); first by eauto.
+ iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] [Hvs' _]]". iModIntro.
wp_load. iMod ("Hvs'" with "[Hs Hhd]") as "HP"; first by iFrame.
iModIntro. wp_let. wp_alloc l as "Hl". wp_let.
wp_bind (CAS _ _ _)%E.
+ iApply (wp_atomic _ ∅); first by eauto.
iMod ("Hvs" with "HP") as ([xs' hd']) "[[Hs Hhd'] Hvs']".
- destruct (decide (hd = hd')) as [->|Hneq].
+ iModIntro. destruct (decide (hd = hd')) as [->|Hneq].
* wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! #() with "[-]") as "HQ".
{ iExists l. iSplitR; first done. by iFrame. }
@@ -145,23 +140,25 @@ Section proof.
let '(xs, hd) := xs_hd in s ↦ #hd ∗ is_list hd xs)%I
(fun xs_hd ret =>
let '(xs, hd) := xs_hd in
- (ret = NONEV ∗ xs = [] ∗ s ↦ #hd ∗ is_list hd []) ∨
- (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ∗ ret = SOMEV x ∗
- xs = x :: xs' ∗ s ↦ #hd' ∗ is_list hd' xs'))%I
- (nclose heapN)
+ (⌜ret = NONEV⌠∗ ⌜xs = []⌠∗ s ↦ #hd ∗ is_list hd []) ∨
+ (∃ x q (hd': loc) xs', hd ↦{q} SOMEV (x, #hd') ∗ ⌜ret = SOMEV x⌠∗
+ ⌜xs = x :: xs'⌠∗ s ↦ #hd' ∗ is_list hd' xs'))%I
+ ∅
⊤
(pop #s).
Lemma pop_atomic_spec (s: loc):
- heapN ⊥ N → heap_ctx ⊢ pop_triple s.
+ pop_triple s.
Proof.
- iIntros (HN) "#?".
+ iProof.
rewrite /pop_triple /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. *)
+ iApply (wp_atomic _ ∅); first by eauto.
iMod ("Hvs" with "HP") as ([xs hd]) "[[Hs Hhd] Hvs']".
- destruct xs as [|y' xs'].
+ iModIntro. destruct xs as [|y' xs'].
- simpl. wp_load. iDestruct "Hvs'" as "[_ Hvs']".
iDestruct "Hhd" as (q) "[Hhd Hhd']".
iMod ("Hvs'" $! NONEV with "[-Hhd]") as "HQ".
@@ -174,20 +171,20 @@ Section proof.
iMod ("Hvs'" with "[-Hhd1 Hhd2 Hxs1]") as "HP".
{ iFrame. iExists hd', (q / 2)%Qp. by iFrame. }
iModIntro. wp_let. wp_load. wp_match. wp_proj.
- wp_bind (CAS _ _ _). iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
- destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_bind (CAS _ _ _).
+ (* FIXME: I should not have to apply wp_atomic manually here and below. *)
+ iApply (wp_atomic _ ∅); first by eauto.
+ iMod ("Hvs" with "HP") as ([xs hd'']) "[[Hs Hhd''] Hvs']".
+ iModIntro. destruct (decide (hd = hd'')) as [->|Hneq].
+ wp_cas_suc. iDestruct "Hvs'" as "[_ Hvs']".
iMod ("Hvs'" $! (SOMEV y') with "[-]") as "HQ".
{ iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
destruct xs as [|x' xs''].
- simpl. iDestruct "Hhd''" as (?) "H".
- iExFalso. iDestruct (heap_mapsto_op_1 with "[Hhd1 H]") as "[% _]".
- { iSplitL "Hhd1"; done. }
- done.
+ iExFalso. by iDestruct (@mapsto_agree loc val with "[$Hhd1 $H]") as %?.
- simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
- iDestruct (heap_mapsto_op_1 with "[Hhd1 Hhd'']") as "[% _]".
- { iSplitL "Hhd1"; done. }
- inversion H0. (* FIXME: bad naming *) subst.
+ iDestruct (@mapsto_agree loc val with "[$Hhd1 $Hhd'']") as %[=].
+ subst.
iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
repeat (iSplitR "Hxs1 Hs"; first done).
iFrame. }