Require Import Vbase Varith.
Require Import Relations Wellfounded Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 rslassn rslmodel rslassnlemmas rslhmap.
Set Implicit Arguments.
Lemma hplus_eq_ra_rmwD h h1 h2 l PP QQ init :
hplus h1 h2 = Hdef h →
h l = HVra PP QQ true init →
∃ hf PP' QQ' init',
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' true init'.
Lemma hsum_eq_ra_rmwD:
∀ h' hs l PP QQ init,
hsum hs = Hdef h' →
h' l = HVra PP QQ true init →
∃ h'' PP' QQ' init', In (Hdef h'') hs ∧ h'' l = HVra PP' QQ' true init'.
Lemma hplus_eq_ra_ownD h h1 h2 l PP QQ init v :
hplus h1 h2 = Hdef h →
h l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ hf PP' QQ' init',
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' false init'
∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Lemma hsum_eq_ra_ownD:
∀ h' hs l PP QQ init v,
hsum hs = Hdef h' →
h' l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ h'' PP' QQ' init',
In (Hdef h'') hs ∧ h'' l = HVra PP' QQ' false init'
∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Lemma hplus_ra_own_l h h1 h2 l PP QQ init v :
hplus (Hdef h1) h2 = Hdef h →
h1 l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' init',
h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Lemma hplus_ra_own_r h h1 h2 l PP QQ init v :
hplus h1 (Hdef h2) = Hdef h →
h2 l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' init',
h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Lemma hsum_has_ra_own h hs hf l PP QQ init v :
hsum hs = Hdef h →
In (Hdef hf) hs →
hf l = HVra PP QQ false init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' init',
h l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Lemma go_back_one_acq :
∀ mt acts lab sb mo rf
(FIN : ExecutionFinite acts lab sb)
(CONS_A : ConsistentAlloc lab) hmap V
(HC : hist_closed mt lab sb rf mo V) e
(VALID : hmap_valid lab sb rf hmap e)
(INe : In e V) hFR l
(NALLOC : lab e ≠ Aalloc l)
(ALLOC : ∀ hf loc,
hFR = Hdef hf → hf loc ≠ HVnone →
∃ c : actid, lab c = Aalloc loc ∧ c ≠ e),
∃ pres_sb pres_sw posts_sb posts_sw,
NoDup pres_sb ∧
NoDup pres_sw ∧
NoDup posts_sb ∧
NoDup posts_sw ∧
(∀ x : actid, In x pres_sb ↔ sb x e) ∧
(∀ x : actid, In x pres_sw ↔ ann_sw lab rf x e) ∧
(∀ x : actid, In x posts_sb ↔ sb e x) ∧
(∀ x : actid, In x posts_sw ↔ ann_sw lab rf e x) ∧
(∀ h
(EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
hsum (map hmap (map (hb_sw^~ e) pres_sw)) +!+ hFR =
Hdef h),
∃ h0 : val → HeapVal,
hsum (map hmap (map (hb_sb e) posts_sb)) +!+
hsum (map hmap (map (hb_sw e) posts_sw)) +!+ hFR =
Hdef h0 ∧
∀ PP' QQ' isrmw' init' (LA: h0 l = HVra PP' QQ' isrmw' init'),
hvplus_ra2_ret (h l) QQ').
Lemma go_back_one_acq2 :
∀ acts lab sb rf
(FIN : ExecutionFinite acts lab sb)
(CONS_A : ConsistentAlloc lab) hmap a
(VALID : hmap_valid lab sb rf hmap a)
hFR typ l v pre post sws
(LL: lab a = Aload typ l v)
(Lp: unique (sb^~ a) pre)
(Lq: unique (sb a) post)
(LwND: NoDup sws)
(LwOK: ∀ x, In x sws ↔ ann_sw lab rf x a)
hp hq hw PP QQ PP' QQ'
(Ep: hmap (hb_sb pre a) = Hdef hp)
(Eq: hmap (hb_sb a post) = Hdef hq)
(Ew: hsum (map hmap (map (hb_sw^~ a) sws)) = Hdef hw)
(Gp: hp l = HVra PP QQ false true)
(Gq: hq l = HVra PP' QQ' false true) Q
(NF: ¬ Asim Q Afalse)
(L: << Gw : hw l = HVnone >> ∧
<< ASIM: Asim (sval (QQ v)) (Astar (sval (QQ' v)) Q) >>
∨ ∃ Pw' Qw' initw',
<< Gw : hw l = HVra Pw' Qw' false initw' >> ∧
<< ASIM: Asim (Astar (sval (QQ v)) (sval (Qw' v))) (Astar (sval (QQ' v)) Q) >>)
(ALLOC : ∀ hf loc,
hFR = Hdef hf →
hf loc ≠ HVnone → ∃ c : actid, lab c = Aalloc loc ∧ c ≠ a) h
(EQ: hmap (hb_sb pre a) +!+
hsum (map hmap (map (hb_sw^~ a) sws)) +!+ hFR =
Hdef h),
∃ h0 : val → HeapVal,
hmap (hb_sb a post) +!+ hFR =
Hdef h0 ∧
∀ PP' QQ' isrmw' (LA: h0 l = HVra PP' QQ' isrmw' true),
∃ PP0 QQ0, h l = HVra PP0 QQ0 isrmw' true ∧
Asim (sval (QQ0 v)) (Astar (sval (QQ' v)) Q).
Lemma go_back_one_rel :
∀ lab sb rf hmap edge
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ isrmw init v
(LA : hf l = HVra PP QQ isrmw init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' isrmw' init',
hf' l = HVra PP' QQ' isrmw' init' ∧
(∀ h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h).
Lemma heap_loc_rel_allocated :
∀ mt lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h (GET: hmap edge = Hdef h) l PP QQ isrmw init
(LA: h l = HVra PP QQ isrmw init),
∃ cpre c hf PP' QQ' isrmw' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
hf l = HVra PP' QQ' isrmw' init' ∧
(cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)) ∧
(∀ h, assn_sem (proj1_sig (PP v)) h → assn_sem (proj1_sig (PP' v)) h).
Lemma go_back_one_rmwacq :
∀ lab sb rf hmap edge
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ init
(LA : hf l = HVra PP QQ true init)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' init', hf' l = HVra PP' QQ' true init'.
Lemma heap_loc_rmwacq_allocated :
∀ mt lab sb rf mo hmap V
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h (GET: hmap edge = Hdef h) l PP QQ init
(LA: h l = HVra PP QQ true init),
∃ cpre c hf PP' QQ' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
hf l = HVra PP' QQ' true init'.
Lemma go_back_one_acq3 :
∀ lab sb rf hmap edge
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ init
(LA : hf l = HVra PP QQ false init) v
(NE : sval (QQ v) ≠ Aemp)
(NE : sval (QQ v) ≠ Afalse)
(NA : lab (hb_fst edge) ≠ Aalloc l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' init',
hf' l = HVra PP' QQ' false init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Lemma heap_loc_ra_own_allocated :
∀ mt lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h (GET: hmap edge = Hdef h) l PP QQ init
(LA: h l = HVra PP QQ false init)
(ALL: sval (QQ v) ≠ Aemp)
(NF: sval (QQ v) ≠ Afalse),
∃ cpre c hf PP' QQ' init',
sb cpre c ∧
lab cpre = Aalloc l ∧
hmap (hb_sb cpre c) = Hdef hf ∧
(cpre = hb_fst edge ∨ happens_before lab sb rf mo cpre (hb_fst edge)) ∧
hf l = HVra PP' QQ' false init'.
Lemma heap_loc_ra_no_own :
∀ mt lab sb rf mo hmap V v
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
edge' (EV: edge_valid lab sb rf edge') (IN': In (hb_fst edge') V)
h (GET: hmap edge = Hdef h) l PP QQ init (LA: h l = HVra PP QQ true init)
h' (GET: hmap edge' = Hdef h') PP' QQ' init' (LA': h' l = HVra PP' QQ' false init'),
sval (QQ' v) = Aemp ∨ sval (QQ' v) = Afalse.
Lemma hb_helper1 lab sb rf mo e e' a :
unique (sb e) e' →
(∀ x, ¬ synchronizes_with lab sb rf mo e x) →
happens_before lab sb rf mo e a →
happens_before lab sb rf mo e' a ∨ e' = a.
Lemma helper_acyclic_last :
∀ A (r: A → A → Prop)
(ACYCL: acyclic r) e i
(MHB: clos_refl_trans _ r e i) R,
∃ b,
<< PRM: In b (i :: R) >> ∧
<< BEFORE: clos_refl_trans _ r e b >> ∧
<< NAFTER: ∀ c, In c (i :: R) → ¬ clos_trans _ r b c >>.
Lemma helper_hb_last :
∀ A lab sb rf mo
(ACYCL: IrreflexiveHB lab sb rf mo) b (Q: A) R (IN: In (b, Q) R) e
(MHB: e = b ∨ happens_before lab sb rf mo e b),
∃ b Q,
<< PRM: In (b, Q) R >> ∧
<< BEFORE: e = b ∨ happens_before lab sb rf mo e b >> ∧
<< NAFTER: ∀ b' Q',
In (b', Q') R →
¬ happens_before lab sb rf mo b b' >>.
Definition RTrel A lab sb rf mo V RT RT' :=
length (A:=A) (fst RT) < length (A:=A) (fst RT') ∨
length (fst RT) = length (fst RT') ∧
depth_metric (happens_before lab sb rf mo) V (map hb_fst (snd RT)) <
depth_metric (happens_before lab sb rf mo) V (map hb_fst (snd RT')).
Definition RTrelWF A lab sb rf mo V :
well_founded (RTrel (A:=A) lab sb rf mo V).
Definition read_loses_perm hmap lab sb rf a l v (Q: assn_mod) :=
∃ typ apre apost w,
<< LL: lab a = Aload typ l v >> ∧
<< Lp: unique (sb^~ a) apre >> ∧
<< Lq: unique (sb a) apost >> ∧
<< Lw: ann_sw lab rf w a >> ∧
∃ hp hq hw PP QQ PP' QQ',
<< Ep: hmap (hb_sb apre a) = Hdef hp >> ∧
<< Eq: hmap (hb_sb a apost) = Hdef hq >> ∧
<< Ew: hmap (hb_sw w a) = Hdef hw >> ∧
<< Gp: hp l = HVra PP QQ false true >> ∧
<< Gq: hq l = HVra PP' QQ' false true >> ∧
<< PREC: precise (sval Q) >> ∧
<< LSEM: assn_sem (sval Q) (Hdef hw) >> ∧
( << Gw : hw l = HVnone >> ∧
<< ASIM: Asim (sval (QQ v)) (Astar (sval (QQ' v)) (sval Q)) >>
∨ ∃ Pw' Qw' initw',
<< Gw : hw l = HVra Pw' Qw' false initw' >> ∧
<< ASIM: Asim (Astar (sval (QQ v)) (sval (Qw' v))) (Astar (sval (QQ' v)) (sval Q)) >>).
Definition ssnd (x : actid × assn_mod) := sval (snd x).
Lemma wellformed_only_reads_helper :
∀ (goal : assn_mod → Prop) mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
T (NDt: NoDup T)
(ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
(TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V) l v
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
(NHB: ∀ a (INt: In a T) b Q (INr: In (b,Q) R),
hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b)
(INDEP: independent lab sb rf mo T)
hT (MAPt: hsum (map hmap T) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT)
(PROVE:
∀ h h' PP' QQ' isrmw' init'
(ALLOC: ∀ a apost (SB: sb a apost) (A: lab a = Aalloc l) h''
(D: hmap (hb_sb a apost) = Hdef h''), h'' l = h' l)
(VS: vshift (Hdef h) (Hdef h'))
(G : h l = HVuval ∨ ∃ isrmw QQ, h l = HVra QQ QQ isrmw false)
(G': h' l = HVra PP' QQ' isrmw' init'),
∃ FRAME, goal (mk_assn_mod (Astar (sval (QQ' v)) FRAME))),
∃ FRAME, goal (mk_assn_mod (Astar (sval (QT v)) (foldr Astar (map ssnd R) FRAME))).
Lemma wellformed :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
l v (LAB: is_writeLV (lab w) l v)
(SBw: sb wpre w) hw
sww (swwOK: ∀ x, In x sww ↔ ann_sw lab rf x w) (swwND: NoDup sww)
(MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_sw^~ w) sww)) = Hdef hw)
PW QW isrmwW initW
(HW: hw l = HVra PW QW isrmwW initW)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V)
(TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
T (NDt: NoDup T)
(ST: ∀ edge (IN: In edge T), In (hb_fst edge) V)
(TT: ∀ edge (IN: In edge T), edge_valid lab sb rf edge)
(INDEP: independent lab sb rf mo T)
(NHB: ∀ a (INt: In a T) b Q (INr: In (b,Q) R),
hb_snd a ≠ b ∧ ¬ happens_before lab sb rf mo (hb_snd a) b)
hT (MAPt: hsum (map hmap T) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
implies (proj1_sig (PW v))
(Astar (proj1_sig (QT v))
(foldr Astar (map ssnd R) Atrue)).
Lemma wellformed_one :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
l v (LAB: is_writeLV (lab w) l v)
(SBw: sb wpre w) hw
sww (swwOK: ∀ x, In x sww ↔ ann_sw lab rf x w) (swwND: NoDup sww)
(MAPw: hmap (hb_sb wpre w) +!+ hsum (map hmap (map (hb_sw^~ w) sww)) = Hdef hw)
PW QW isrmwW initW
(HW: hw l = HVra PW QW isrmwW initW)
rpre r (ST: In rpre V) (TT: sb rpre r)
(NIN: ¬ In r V)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V)
(TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
implies (proj1_sig (PW v))
(Astar (proj1_sig (QT v))
(foldr Astar (map ssnd R) Atrue)).
Lemma wellformed_one_w :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
wpre w (INw: In w V)
typ l v (LAB: lab w = Astore typ l v)
(SBw: sb wpre w) hw
(MAPw: hmap (hb_sb wpre w) = Hdef hw)
PW QW isrmwW initW
(HW: hw l = HVra PW QW isrmwW initW)
rpre r (ST: In rpre V) (TT: sb rpre r)
(NIN: ¬ In r V)
(R: list (actid × assn_mod))
(NDr: NoDup (map (@fst _ _) R))
(SR: ∀ a Q (IN: In (a, Q) R), In a V)
(TR: ∀ a Q (IN: In (a, Q) R), ann_sw lab rf w a)
(DEL: ∀ a Q (IN: In (a, Q) R), read_loses_perm hmap lab sb rf a l v Q)
hT (MAPt: hmap (hb_sb rpre r) = Hdef hT)
PT QT isrmwT initT (HT: hT l = HVra PT QT isrmwT initT),
implies (proj1_sig (PW v))
(Astar (proj1_sig (QT v))
(foldr Astar (map ssnd R) Atrue)).
Lemmas about initialization
Lemma helper_ra_init :
∀ lab sb rf hmap edge
(VAL: hmap_valid lab sb rf hmap (hb_fst edge))
(EV : edge_valid lab sb rf edge) hf
(GET: hmap edge = Hdef hf) l PP QQ isrmw
(LA : hf l = HVra PP QQ isrmw true)
(NW : ¬ is_writeL (lab (hb_fst edge)) l),
∃ edge' hf',
edge_valid lab sb rf edge' ∧
hb_snd edge' = hb_fst edge ∧
hmap edge' = Hdef hf' ∧
∃ PP' QQ' isrmw',
hf' l = HVra PP' QQ' isrmw' true.
Lemma heap_loc_ra_initialized :
∀ mt acts lab sb rf mo hmap V
(FIN: ExecutionFinite acts lab sb)
(ACYCLIC: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(HC: hist_closed mt lab sb rf mo V)
(VALID: hmap_valids lab sb rf hmap V)
edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
h (GET: hmap edge = Hdef h) l PP QQ isrmw
(LA: h l = HVra PP QQ isrmw true),
∃ cpre c,
sb cpre c ∧
is_writeL (lab c) l ∧
(c = hb_fst edge ∨ happens_before lab sb rf mo c (hb_fst edge)).
Construction of the read_loses_perm list
Fixpoint map_pairo A B (f: A → option B) l :=
match l with
| nil ⇒ nil
| x :: l' ⇒
match f x with
| Some y ⇒ (x, y) :: map_pairo f l'
| None ⇒ map_pairo f l'
end
end.
Lemma In_map_pairo A B (f : A → option B) l x :
In x (map_pairo f l) ↔ In (fst x) l ∧ f (fst x) = Some (snd x).
Lemma NoDup_map_fst_map_pairo A B (f : A → option B) l :
NoDup l → NoDup (map (@fst _ _) (map_pairo f l)).
Lemma read_loses_perm_uniq :
∀ hmap lab sb rf r E v P
(H: read_loses_perm hmap lab sb rf r E v P) P'
(H': read_loses_perm hmap lab sb rf r E v P'),
P = P'.
Lemma read_loses_perm1 hmap lab sb rf E res sws V :
NoDup sws →
∃ l,
<< NDl: NoDup (map (@fst _ _) l) >> ∧
<< EQl: ∀ r P, In (r,P) l →
In r sws ∧ In r V ∧
read_loses_perm hmap lab sb rf r E res P >> ∧
<< EQl': ∀ r P,
In r sws → In r V →
read_loses_perm hmap lab sb rf r E res P →
In (r,P) l >>.
This page has been generated by coqdoc Imprint | Data protection