# Assertions

Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import Permutation.

Set Implicit Arguments.

Definition mydec (P: Prop) :=
if (excluded_middle_informative P) then true else false.

Definition val := nat.

Inductive assn :=
| Afalse
| Aemp
| Aimplies (P Q: assn)
| Aforall (PP : valassn)
| Apt (E : val)
| Aptu (E : val)
| Astar (P Q: assn)
| Arainit (E : val)
| Arel (E : val) (Q : valassn)
| Aacq (E: val) (Q : valassn)
| Armwacq (E: val) (Q : valassn)
| Atriangle (P: assn)
| Anabla (P: assn).

Definition Atrue := Aimplies Afalse Afalse.

Syntactic assertion similarity: the smallest congruence relation containing the ACI rules for Astar.

Inductive Asim : assnassnProp :=
| Asim_star_false : Asim (Astar Afalse Afalse) Afalse
| Asim_star_emp P : Asim (Astar P Aemp) P
| Asim_starC P Q : Asim (Astar P Q) (Astar Q P)
| Asim_starA P Q R : Asim (Astar (Astar P Q) R) (Astar P (Astar Q R))
| Asim_refl P : Asim P P
| Asim_sym P Q (H: Asim P Q) : Asim Q P
| Asim_trans P Q (H: Asim P Q) R (: Asim Q R) : Asim P R
| Asim_implies P1 P2 (H1: Asim P1 P2) Q1 Q2 (H2: Asim Q1 Q2) :
Asim (Aimplies P1 Q1) (Aimplies P2 Q2)
| Asim_forall Q1 Q2 (H1: v, Asim (Q1 v) (Q2 v)) :
Asim (Aforall Q1) (Aforall Q2)
| Asim_star P1 P2 (H1: Asim P1 P2) Q1 Q2 (H2: Asim Q1 Q2) :
Asim (Astar P1 Q1) (Astar P2 Q2)
| Asim_rel E P1 P2 (H1: v, Asim (P1 v) (P2 v)) :
Asim (Arel E P1) (Arel E P2)
| Asim_acq E Q1 Q2 (H1: v, Asim (Q1 v) (Q2 v)) :
Asim (Aacq E Q1) (Aacq E Q2)
| Asim_rmwacq E Q1 Q2 (H1: v, Asim (Q1 v) (Q2 v)) :
Asim (Armwacq E Q1) (Armwacq E Q2)
| Asim_triangle P Q (H: Asim P Q) : Asim (Atriangle P) (Atriangle Q)
| Asim_nabla P Q (H: Asim P Q) : Asim (Anabla P) (Anabla Q).

Lemma lenT e1 e2: (e1 e2) = falsee2 e1.

Lemma lenAS e1 e2 : e1 e2e2 e1e1 = e2.

Lemma assn_eqP : Equality.axiom (fun x y : assnmydec (x = y)).

Canonical Structure assn_eqMixin := EqMixin assn_eqP.
Canonical Structure assn_eqType := Eval hnf in EqType _ assn_eqMixin.

Definition leq_fun A (leq : AAbool) PP PP´ :=
mydec (PP = PP´ n,
leq (PP n) (PP´ n) PP n PP´ n x (LT: x < n), PP x = PP´ x).

Fixpoint assn_leq p q :=
match p, q with
| Afalse , _true
| _ , Afalsefalse
| Aemp , _true
| _ , Aempfalse
| Aimplies P Q, Aimplies if P == then assn_leq Q else assn_leq P
| Aimplies _ _, _true
| _ , Aimplies _ _false
| Aforall PP , Aforall PP´leq_fun assn_leq PP PP´
| Aforall _ , _true
| _ , Aforall _false
| Apt E1 E2 , Apt E1´ E2´if E1 == E1´ then E2 E2´ else E1 E1´
| Apt _ _ , _true
| _ , Apt _ _false
| Aptu E1 , Aptu E1´E1 E1´
| Aptu _ , _true
| _ , Aptu _false
| Astar P Q , Astar if P == then assn_leq Q else assn_leq P
| Astar _ _ , _true
| _ , Astar _ _false
| Arainit E , Arainit E
| Arainit _ , _true
| _ , Arainit _false
| Arel E PP , Arel PP´if E == then leq_fun assn_leq PP PP´ else E
| Arel _ _ , _true
| _ , Arel _ _false
| Aacq E PP , Aacq PP´if E == then leq_fun assn_leq PP PP´ else E
| Aacq _ _ , _true
| _ , Aacq _ _false
| Armwacq E PP, Armwacq PP´if E == then leq_fun assn_leq PP PP´ else E
| Armwacq _ _ , _true
| _ , Armwacq _ _false
| Atriangle P , Atriangle assn_leq P
| Atriangle _ , _true
| _ , Atriangle _false
| Anabla P , Anabla assn_leq P
end.

Lemma leq_funAS A leq (AS: antisymmetric leq) p q :
leq_fun (A:=A) leq p qleq_fun leq q pp = q.

Lemma leq_fun_trans A (leq : AAbool) p q r
(AS: p q, leq p qleq q pp = q)
(T: x, leq (p x) (q x) → leq (q x) (r x) → leq (p x) (r x)) :
leq_fun (A:=A) leq p qleq_fun leq q rleq_fun leq p r.

Lemma assn_leqAS :
p q, assn_leq p qassn_leq q pp = q.

Lemma assn_leq_refl :
p, assn_leq p p.

Lemma assn_leq_trans :
p q r (H: assn_leq p q) (: assn_leq q r), assn_leq p r.

Lemma neq_min_neq A (f g : natA) (NEQ: f g) :
m, f m g m ( x, x < mf x = g x).

Lemma assn_leqT :
p q, assn_leq p q = falseassn_leq q p.

Lemma assn_leq_false_ne :
p q, assn_leq p q = falsep q.

Lemma assn_leqTT :
p q, assn_leq p q = falsep q assn_leq q p = true.

Lemma assn_leq_AfalseD P : assn_leq P AfalseP = Afalse.

Opaque assn_leq.

## Normalization

Fixpoint assn_merge_size P :=
match P with
| Astar p qS (assn_merge_size q)
| _ ⇒ 0
end.

Definition assn_merge_fst P :=
match P with
| Astar p qp
| _P
end.

Definition assn_merge_snd P :=
match P with
| Astar p qSome q
| _None
end.

Definition assn_not_star P :=
match P with
| Astar _ _false
| _true
end.

Fixpoint assn_wf P :=
match P with
| Afalse | Aemp | Apt _ _ | Aptu _ | Arainit _True
| Astar p qassn_wf p assn_wf q
assn_not_star p p Aemp q Aemp
assn_leq p (assn_merge_fst q)
¬ (p = Afalse assn_merge_fst q = Afalse)
| Aimplies p qassn_wf p assn_wf q
| Arel _ pp
| Aacq _ pp
| Armwacq _ pp
| Aforall pp x, assn_wf (pp x)
| Atriangle passn_wf p
| Anabla passn_wf p
end.

Fixpoint assn_merge_rec P Q SZ :=
match SZ with
0 ⇒ Aemp
| S sz
if assn_leq (assn_merge_fst P) (assn_merge_fst Q) then
if (assn_merge_fst P == Afalse) && (assn_merge_fst Q == Afalse) then
(match assn_merge_snd Q with
| NoneP
| Some ⇒ @assn_merge_rec P sz
end)
else
Astar (assn_merge_fst P)
(match assn_merge_snd P with
| NoneQ
| Some ⇒ @assn_merge_rec Q sz
end)
else
Astar (assn_merge_fst Q)
(match assn_merge_snd Q with
| NoneP
| Some ⇒ @assn_merge_rec P sz
end)
end.

Definition assn_star_rdf P Q :=
if (P == Afalse) && (assn_merge_fst Q == Afalse) then Q
else Astar P Q.

Definition assn_merge P Q :=
assn_merge_rec P Q (S (assn_merge_size P + assn_merge_size Q)).

Fixpoint assn_norm p := match p with
| AfalseAfalse
| AempAemp
| Aimplies P QAimplies (assn_norm P) (assn_norm Q)
| Aforall PPAforall (fun xassn_norm (PP x))
| Apt E Apt E
| Aptu EAptu E
| Astar P Q
let := assn_norm P in
let := assn_norm Q in
if == Aemp then
else if == Aemp then
else assn_merge
| Arainit EArainit E
| Arel E QQArel E (fun vassn_norm (QQ v))
| Aacq E QQAacq E (fun vassn_norm (QQ v))
| Armwacq E QQArmwacq E (fun vassn_norm (QQ v))
| Atriangle PAtriangle (assn_norm P)
| Anabla PAnabla (assn_norm P)
end.

Lemma assn_merge_notemp:
SZ p1 p2 (PF: assn_merge_size p1 + assn_merge_size p2 < SZ),
assn_merge_rec p1 p2 SZ Aemp.

Lemma assn_merge_fst_merge_rec p1 p2 SZ :
assn_merge_size p1 + assn_merge_size p2 < SZ
assn_merge_fst (assn_merge_rec p1 p2 SZ) =
if assn_leq (assn_merge_fst p1) (assn_merge_fst p2) then
assn_merge_fst p1
else
assn_merge_fst p2.

Lemma assn_merge_leq:
r SZ p (WFp : assn_wf p) (Lp : assn_leq r (assn_merge_fst p))
q (WFq : assn_wf q) (Lq : assn_leq r (assn_merge_fst q))
(PF: assn_merge_size p + assn_merge_size q < SZ),
assn_leq r (assn_merge_fst (assn_merge_rec p q SZ)).

Lemma assn_merge_wf:
SZ p1 (WF1: assn_wf p1) (NE1: p1 Aemp)
p2 (WF2: assn_wf p2) (NE2: p2 Aemp)
(PF: assn_merge_size p1 + assn_merge_size p2 < SZ),
assn_wf (assn_merge_rec p1 p2 SZ).

Lemma assn_merge_wf2:
SZ p1 (WF1: assn_wf p1) (NE1: assn_not_star p1)
p2 (WF2: assn_wf p2) (NE2: p2 Aemp)
(LT: assn_leq p1 (assn_merge_fst p2))
(NP: ¬ (p1 = Afalse assn_merge_fst p2 = Afalse))
(PF: assn_merge_size p1 + assn_merge_size p2 < SZ),
assn_merge_rec p1 p2 SZ = Astar p1 p2.

Lemma assn_norm_wf p : assn_wf (assn_norm p).

Lemma assn_norm_wf2 p : assn_wf passn_norm p = p.

Lemma assn_merge_recC :
n p (WFp: assn_wf p) q (WF : assn_wf q)
(PF : assn_merge_size p + assn_merge_size q < n),
assn_merge_rec p q n = assn_merge_rec q p n.

Lemma assn_mergeC :
p (WFp: assn_wf p) q (WF : assn_wf q),
assn_merge p q = assn_merge q p.

Lemma assn_merge_size_merge :
n p (WFp: assn_wf p) (NEp: p Aemp)
q (WFq: assn_wf q) (NEq: q Aemp)
(LT : assn_merge_size p + assn_merge_size q < n),
assn_merge_size (assn_merge_rec p q n)
S (assn_merge_size p + assn_merge_size q).

Definition assn_rdf P Q :=
if (P == Afalse) && (Q == Afalse) then Q
else Astar P Q.

Fixpoint assn_insert p q :=
match q with
| Astar
if assn_leq p then assn_star_rdf p q
else Astar (assn_insert p )
| _
if assn_leq p q then assn_star_rdf p q
else Astar q p
end.

Lemma assn_merge_fst_not_star p : assn_not_star passn_merge_fst p = p.

Ltac assn_merge_clarify :=
repeat (clarify; match goal with
| H: assn_merge_snd ?p = Some _ |- _
destruct p; ins; inv H; clear H; try rewrite addnS in *; desf
| H: assn_merge_snd ?p = None |- _
cut (assn_not_star p); [|by clear -H; destruct p]; clear H; intro H
| H : assn_leq ?p ?q = true, : assn_leq ?q ?p = true |- _
eapply assn_leqAS in H; eauto; try subst p; try subst q
| H : assn_leq ?p ?q = true, : assn_leq ?q ?r = true, H´´: assn_leq ?r ?p = true |- _
eapply assn_leqAS in H; eauto using assn_leq_trans; try subst p; try subst q
| H : assn_leq ?p ?q = false |- _
eapply assn_leqTT in H; desc
| H : is_true (assn_not_star ?p) |- _
rewrite (@assn_merge_fst_not_star p H) in *; try done
| H : ¬ (_ _) |- _destruct H; done
end); eauto using assn_leqAS.

Lemma assn_merge_ins :
n p (WFp: assn_wf p) (NEp: assn_not_star p)
q (WFq: assn_wf q) (NEq: q Aemp)
(LTn : assn_merge_size p + assn_merge_size q < n),
assn_merge_rec p q n = assn_insert p q.

Lemma assn_insertC_base p q :
assn_not_star passn_not_star qassn_insert p q = assn_insert q p.

Lemma assn_insertC r p q :
assn_not_star passn_not_star q
assn_insert p (assn_insert q r) =
assn_insert q (assn_insert p r).

Lemma assn_insert_before p q:
assn_leq p (assn_merge_fst q) →
assn_insert p q =
if (p == Afalse) && (assn_merge_fst q == Afalse) then q else Astar p q.

Lemma assn_insert_ff p :
assn_insert Afalse (assn_insert Afalse p) = assn_insert Afalse p.

Lemma assn_merge_fst_insert p q :
assn_not_star p
assn_merge_fst (assn_insert p q) =
if assn_leq p (assn_merge_fst q) then p
else assn_merge_fst q.

Lemma assn_merge_ins2 :
n p (WFp: assn_wf p) (NEp: p Aemp)
q (WFq: assn_wf q) (NEq: q Aemp)
(LTn : assn_merge_size p + assn_merge_size q < n),
assn_merge_rec p q n =
match assn_merge_snd p with
| Noneassn_insert p q
| Some assn_insert (assn_merge_fst p) (assn_merge_rec q (Peano.pred n))
end.

Lemma assn_merge_star :
p (WFp: assn_wf p) (NEp: p Aemp)
q (WFq: assn_wf q) (NEq: q Aemp) (NSq: assn_not_star q)
r (WFr: assn_wf r) (NEr: r Aemp) (LT: assn_leq q (assn_merge_fst r))
(NFF: ¬ (q = Afalse assn_merge_fst r = Afalse)),
assn_merge p (Astar q r) = assn_insert q (assn_merge p r).

Lemma assn_merge_not_star :
q p (WFp: assn_wf p) (NEp: p Aemp)
(WFq: assn_wf q) (NEq: q Aemp) (NSq: assn_not_star q),
assn_merge p q = assn_insert q p.

Lemma assn_merge_rdf :
p (WFp: assn_wf p) (NEp: p Aemp)
q (WFq: assn_wf q) (NEq: q Aemp) (NSq: assn_not_star q)
r (WFr: assn_wf r) (NEr: r Aemp) (LT: assn_leq q (assn_merge_fst r)),
assn_merge p (assn_star_rdf q r) = assn_insert q (assn_merge p r).

Lemma assn_merge_insert :
p (WFp: assn_wf p) (NEp: p Aemp)
q (WFq: assn_wf q) (NEq: q Aemp) (NSq: assn_not_star q)
r (WFr: assn_wf r) (NEr: r Aemp),
assn_merge p (assn_insert q r) = assn_insert q (assn_merge p r).

Lemma assn_mergeA :
p (WFp: assn_wf p) (NEp: p Aemp)
q (WFq: assn_wf q) (NEq: q Aemp)
r (WFr: assn_wf r) (NEr: r Aemp),
assn_merge p (assn_merge q r) = assn_merge (assn_merge p q) r.

Lemma Asim_assn_norm p : Asim p (assn_norm p).

Two assertions are syntactically similar iff they have the same normal form.

## Syntactic properties of assertions

Lemma Asim_star_emp_l P : Asim P (Astar Aemp P).

Lemma Asim_star_emp_r P : Asim P (Astar P Aemp).

Ltac Asim_simpl_loop :=
repeat
first [eapply Asim_trans, Asim_assn_norm|
eapply Asim_trans, Asim_star_emp_l|
eapply Asim_trans, Asim_star_emp_r|
apply Asim_star|
apply Asim_refl].

Ltac Asim_simpl :=
do 2 (eapply Asim_trans;[apply Asim_sym|Asim_simpl_loop]);
try apply Asim_refl; try done.

Ltac Asim_simpl_asm H :=
do 2 (eapply Asim_trans in H;[apply Asim_sym in H|Asim_simpl_loop]).

Lemma Asim_norm_l P Q: Asim (assn_norm P) Q Asim P Q.

Lemma Asim_norm_r P Q: Asim P (assn_norm Q) Asim P Q.

Lemma Asim_starAC P Q R :
Asim (Astar P (Astar Q R)) (Astar Q (Astar P R)).

Lemma Asim_rem2 Q P R :
Asim (Astar P R) (Astar ) →
Asim (Astar (Astar P Q) R)
(Astar (Astar Q) ).

Lemma Asim_foldr_simpl l Q :
Asim (foldr Astar l Q) (Astar (foldr Astar l Aemp) Q).

Lemma Asim_foldr_pull l P Q :
Asim (foldr Astar l (Astar P Q))
(Astar P (foldr Astar l Q)).

Lemma Asim_falseD P :
Asim Afalse P
P = Afalse , P = Astar
(Asim Afalse Asim Aemp
Asim Aemp Asim Afalse
Asim Afalse Asim Afalse).

Lemma assn_merge_not_false2 P Q n :
assn_merge_rec P Q n Afalse
assn_merge_size P + assn_merge_size Q < n
assn_wf Q
P AempQ Aemp
, assn_merge_rec P Q n = Astar .

Lemma Asim_starD P Q R :
Asim (Astar P Q) R
( , R = Astar )
Asim P Aemp Asim Q R
Asim Q Aemp Asim P R
Asim P Afalse Asim Q Afalse R = Afalse.

Lemma Asim_star_empD P Q :
Asim (Astar P Q) Aemp Asim P Aemp Asim Q Aemp.

Lemma Asim_emp_starD P Q :
Asim Aemp (Astar P Q) Asim Aemp P Asim Aemp Q.

Lemma assn_rdf_size p q :
¬ (p = Afalse assn_merge_fst q = Afalse)
assn_merge_size (assn_star_rdf p q) = S (assn_merge_size q).

Lemma assn_insert_size p q :
¬ (p = Afalse assn_merge_fst (assn_norm q) = Afalse)
assn_not_star p
assn_merge_size (assn_insert p q) =
S (assn_merge_size q).

Lemma assn_insert_neq p q :
¬ (p = Afalse assn_merge_fst (assn_norm q) = Afalse)
assn_not_star p
p = assn_insert p q
False.

Lemma assn_insert_not_star_eq :
p q, assn_not_star q
assn_insert p q = if assn_leq p q then assn_star_rdf p q else Astar q p.

Lemma assn_insert_cancel1 :
p (NS: assn_not_star p) (NE: p Aemp) q
(NS´: assn_not_star q)
(NF: ¬ (p = Afalse assn_merge_fst (assn_norm q) = Afalse))
(NF´: ¬ (p = Afalse assn_merge_fst (assn_norm ) = Afalse))
(EQ: assn_insert p q = assn_insert p ),
assn_wf qassn_wf q = .

Lemma assn_insert_cancel :
p (NS: assn_not_star p) (NE: p Aemp) q
(NF: ¬ (p = Afalse assn_merge_fst (assn_norm q) = Afalse))
(NF´: ¬ (p = Afalse assn_merge_fst (assn_norm ) = Afalse))
(EQ: assn_insert p q = assn_insert p )
(WF: assn_wf q) (WF´: assn_wf ),
q = .

Lemma assn_merge_cancel :
n m q p
(LT: assn_merge_size p + assn_merge_size q < n)
(LT´: assn_merge_size p + assn_merge_size < m)
(NF: ¬ (assn_merge_fst (assn_norm p) = Afalse
assn_merge_fst (assn_norm q) = Afalse))
(NF´: ¬ (assn_merge_fst (assn_norm p) = Afalse
assn_merge_fst (assn_norm ) = Afalse))
(EQ: assn_merge_rec p q n = assn_merge_rec p m),
p Aempq Aemp Aemp
assn_wf passn_wf qassn_wf q = .

Lemma assn_merge_size_merge2 :
n p (WFp: assn_wf p) (NEp: p Aemp) (NFp: assn_merge_fst p Afalse)
q (WFq: assn_wf q) (NEq: q Aemp)
(LT : assn_merge_size p + assn_merge_size q < n),
assn_merge_size (assn_merge_rec p q n) =
S (assn_merge_size p + assn_merge_size q).

Lemma Asim1 P Q :
Asim P (Astar P Q) →
Asim Q Aemp Asim Q Afalse , Asim P (Astar Afalse ).

Lemma Asim_star_cancel P Q :
Asim (Astar P Q) (Astar P ) →
Asim Q
( , Asim Q (Astar Afalse ))
( , Asim (Astar Afalse )).

Lemma assn_norm_star_false :
assn_norm (Astar Afalse Afalse) = Afalse.

Global Opaque assn_norm.

## Model of heaps

Assertions modulo the syntactic rules

Definition assn_mod := { P : assn | assn_norm P = P }.

Labels for non-atomic locations

Inductive HeapLabel :=
| HLnormal
| HLtriangle
| HLnabla.

Labels for atomic locations

Inductive HeapLabelCombination :=
| HLCnormal
| HLCtriangle
| HLCnabla
| HLCdiamond
| HLCtriangledot
| HLCdiamonddot.

Coercion label_to_combination (lbl: HeapLabel) :=
match lbl with
| HLnormalHLCnormal
| HLtriangleHLCtriangle
| HLnablaHLCnabla
end.

Coercion label_to_combination_option (lbl: HeapLabel) := Some (label_to_combination lbl).

Definition is_basic lbl := lbl = HLCnormal lbl = HLCtriangle lbl = HLCnabla.

Definition is_normal lbl := lbl = HLCnormal lbl = HLCtriangledot lbl = HLCnabladot lbl = HLCdiamonddot.

Definition is_triangle lbl := lbl = HLCtriangle lbl = HLCtriangledot lbl = HLCdiamond lbl = HLCdiamonddot.

Definition is_nabla lbl := lbl = HLCnabla lbl = HLCnabladot lbl = HLCdiamond lbl = HLCdiamonddot.

Definition is_normalO olbl :=
match olbl with
| Some lblis_normal lbl
| NoneFalse
end.

Definition HLleq lbl1 lbl2 :=
match lbl1, lbl2 with
| HLCnormal , _is_normal lbl2
| HLCtriangle , _is_triangle lbl2
| HLCnabla , _is_nabla lbl2
| HLCdiamond , _lbl2 = HLCdiamond lbl2 = HLCdiamonddot
| HLCtriangledot, _lbl2 = HLCtriangledot lbl2 = HLCdiamonddot
| HLCdiamonddot , _lbl2 = HLCdiamonddot
end.

Definition oHLleq (olbl1 olbl2: option HeapLabelCombination) :=
match olbl1, olbl2 with
| None, _True
| Some lbl1, Some lbl2HLleq lbl1 lbl2
| _, _False
end.

Inductive HeapVal :=
| HVnone
| HVuval (lbl: HeapLabel)
| HVval (v: val) (lbl: HeapLabel)
| HVra (RR QQ: valassn_mod) (isrmwflag: bool) (perm: option HeapLabelCombination)
(init: option HeapLabelCombination).

Inductive heap :=
| Hundef
| Hdef (hf: valHeapVal).

Definition HVlabeled hv (lbl: HeapLabel) :=
match hv with
| HVnoneTrue
| HVuval lbl´lbl = lbl´
| HVval _ lbl´lbl = lbl´
| HVra _ _ _ None NoneFalse
| HVra _ _ _ (Some permlbl) NoneHLleq lbl permlbl
| HVra _ _ _ None (Some initlbl) ⇒ HLleq lbl initlbl
| HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ HLleq lbl permlbl HLleq lbl initlbl
end.

Definition HFlabeled hf lbl := (l: val) , HVlabeled (hf l) lbl.

Definition Hlabeled h lbl := hf, h = Hdef hf HFlabeled hf lbl.

Definition HVlabeledExact hv (lbl: HeapLabel) :=
match hv with
| HVnoneTrue
| HVuval lbl´lbl´ = lbl
| HVval _ lbl´lbl´ = lbl
| HVra _ _ _ None NoneTrue
| HVra _ _ _ (Some permlbl) Nonepermlbl = lbl
| HVra _ _ _ None (Some initlbl) ⇒ initlbl = lbl
| HVra _ _ _ (Some permlbl) (Some initlbl) ⇒ permlbl = lbl initlbl = lbl
end.

Definition HFlabeledExact hf lbl := (l: val), HVlabeledExact (hf l) lbl.

Definition HlabeledExact h lbl := hf, h = Hdef hf HFlabeledExact hf lbl.

Definition HVlabeledW hv (lbl: HeapLabel) :=
match hv with
| HVnoneFalse
| HVuval lbl´lbl = lbl´
| HVval _ lbl´lbl = lbl´
| HVra _ _ _ (Some permlbl) _HLleq lbl permlbl
| _False
end.

Definition HVlabeledR hv (lbl: HeapLabel) :=
match hv with
| HVnoneFalse
| HVuval lbl´False
| HVval _ lbl´lbl = lbl´
| HVra _ _ _ _ (Some initlbl) ⇒ HLleq lbl initlbl
| _False
end.

Definition HLCsim (lbl1 lbl2: option HeapLabelCombination) :=
match lbl1, lbl2 with
| None, NoneTrue
| (Some _), (Some _) ⇒ True
| _, _False
end.

Definition HVsim hv hv´ :=
match hv, hv´ with
| HVnone, HVnoneTrue
| HVuval _, HVuval _True
| HVval v _, HVval _v =
| HVra RR QQ isrmwflag perm init, HVra RR´ QQ´ isrmwflag´ perm´ init´
⇒ RR = RR´ QQ = QQ´ isrmwflag = isrmwflag´ HLCsim perm perm´ HLCsim init init´
| _, _False
end.

Definition HFsim hf hf´ := (l: nat), HVsim (hf l) (hf´ l).

Definition Hsim h := hf hf´, h = Hdef hf = Hdef hf´ HFsim hf hf´.

Definition lupd h lbl :=
match h with
| HundefHundef
| Hdef hfHdef (fun lmatch hf l with
| HVnoneHVnone
| HVuval _HVuval lbl
| HVval v _HVval v lbl
| HVra PP QQ isrmw None NoneHVra PP QQ isrmw None None
| HVra PP QQ isrmw (Some _) NoneHVra PP QQ isrmw lbl None
| HVra PP QQ isrmw None (Some _) ⇒ HVra PP QQ isrmw None lbl
| HVra PP QQ isrmw (Some _) (Some _) ⇒ HVra PP QQ isrmw lbl lbl
end)
end.

Definition is_val v :=
match v with
HVval _ HLnormal | HVuval HLnormaltrue
| HVnone | HVra _ _ _ _ _ | _false
end.

Definition has_value hv v :=
match hv with
| HVval _ = v
| _False
end.

Definition is_nonatomic hv :=
match hv with
| HVval _ _true
| HVuval _true
| _false
end.

Definition is_atomic hv :=
match hv with
| HVra _ _ _ _ _true
| _false
end.

Definition mk_assn_mod (P: assn) : assn_mod := exist _ _ (assn_norm_idemp P).

Definition hemp : heap := Hdef (fun vHVnone).

Definition Acombinable (P Q : assn) :=
P = Afalse Q = Afalse P = Q.

Definition hv_rval isrmw P :=
match isrmw with
| trueP
| falseAemp
end.

Definition hv_acq_def isrmw1 Q1 isrmw2 Q2 :=
hv_rval isrmw2 Q1 = hv_rval isrmw1 Q2
Q1 = Afalse Q2 = Afalse.

Definition hvplusDEF (hv hv´ : HeapVal) : Prop :=
match hv, hv´ with
| HVnone, _True
| _, HVnoneTrue
| HVra RR1 QQ1 isrmw1 perm1 init1, HVra RR2 QQ2 isrmw2 perm2 init2
( v, hv_acq_def isrmw1 (sval (QQ1 v)) isrmw2 (sval (QQ2 v)))
( v, Acombinable (sval (RR1 v)) (sval (RR2 v)))
| _, _False
end.

Definition hlplus lbl1 lbl2 :=
match lbl1, lbl2 with
| HLCdiamonddot , _HLCdiamonddot
| _ , HLCdiamonddotHLCdiamonddot
| HLCtriangledot , HLCdiamondHLCdiamonddot
| HLCtriangledot , HLCnablaHLCdiamonddot
| HLCtriangledot , _HLCtriangledot
| HLCdiamond , HLCtriangledotHLCdiamonddot
| HLCdiamond , HLCnormalHLCdiamonddot
| HLCdiamond , _HLCdiamond
| HLCnabla , HLCtriangledotHLCdiamonddot
| HLCnabla , HLCdiamondHLCdiamond
| HLCnabla , HLCnablaHLCnabla
| HLCnabla , HLCtriangleHLCdiamond
| HLCtriangle , HLCtriangledotHLCtriangledot
| HLCtriangle , HLCdiamondHLCdiamond
| HLCtriangle , HLCnablaHLCdiamond
| HLCtriangle , HLCtriangleHLCtriangle
| HLCtriangle , HLCnormalHLCtriangledot
| HLCnormal , HLCtriangledotHLCtriangledot
| HLCnormal , HLCdiamondHLCdiamonddot
| HLCnormal , HLCtriangleHLCtriangledot
| HLCnormal , HLCnormalHLCnormal
end.

Definition ohlplus lbl1 lbl2 :=
match lbl1, lbl2 with
| None, lbllbl
| lbl, Nonelbl
| (Some lbl1´), (Some lbl2´) ⇒ Some (hlplus lbl1´ lbl2´)
end.

Definition hvplus (hv hv´ : HeapVal) : HeapVal :=
match hv, hv´ with
| HVnone, _hv´
| _, HVnonehv
| HVra RR1 QQ1 isrmw1 perm1 init1, HVra RR2 QQ2 isrmw2 perm2 init2
HVra (fun vif excluded_middle_informative (sval (RR1 v) = Afalse) then RR2 v else RR1 v)
(if isrmw1 then QQ1
else if isrmw2 then QQ2
else fun vmk_assn_mod (Astar (sval (QQ1 v)) (sval (QQ2 v))))
(isrmw1 || isrmw2)
(ohlplus perm1 perm2)
(ohlplus init1 init2)
| _, _hv
end.

Definition hplus (h1 h2: heap) : heap :=
match h1, h2 with
| Hundef, _Hundef
| _, HundefHundef
| Hdef hf1, Hdef hf2
if excluded_middle_informative ( v, hvplusDEF (hf1 v) (hf2 v)) then
Hdef (fun vhvplus (hf1 v) (hf2 v))
else Hundef
end.

hsum : iterated hplus

Definition hsum (l: list heap) := foldr hplus l hemp.

Definition hupd B (h : natB) y z := fun xif x == y then z else h x.

Singleton heap cell

Notation hsingl l v := (Hdef (hupd (fun _HVnone) l v)).

initialize : add HLnormal to the set of initialization labels of an atomic location

Definition initialize h l :=
hupd h l (match h l with
| HVra PP QQ perm isrmw initHVra PP QQ perm isrmw (ohlplus init (Some HLCnormal))
| _h l end).

Global Opaque hplus.

## Assertion semantics

Definition Wemp : valassn_mod := fun _mk_assn_mod Afalse.
Definition Remp : valassn_mod := fun _mk_assn_mod Aemp.

Fixpoint assn_sem (P : assn) (h : heap) :=
match P with
| AfalseFalse
| Aemph = hemp
| Aimplies P Qh Hundef (assn_sem P hassn_sem Q h)
| Aforall PP x, assn_sem (PP x) h
| Apt E h = hsingl E (HVval HLnormal)
| Aptu Eh = hsingl E (HVuval HLnormal)
| Astar P Q
h1 h2, h Hundef hplus h1 h2 = h assn_sem P h1 assn_sem Q h2
| Arainit Eh = Hdef (hupd (fun _HVnone) E (HVra Wemp Remp false None (Some HLCnormal)))
| Arel E Ph = hsingl E (HVra (fun xmk_assn_mod (P x)) Remp false (Some HLCnormal) None)
| Aacq E Qh = hsingl E (HVra Wemp (fun xmk_assn_mod (Q x)) false None None)
| Armwacq E Qh = hsingl E (HVra Wemp (fun xmk_assn_mod (Q x)) true (Some HLCnormal) None)
| Atriangle QHlabeledExact h HLtriangle
, assn_sem Q Hsim h HlabeledExact HLnormal
| Anabla QHlabeledExact h HLnabla
, assn_sem Q Hsim h HlabeledExact HLnormal
end.

Definition assn_sem_sim P h := , assn_sem P Hsim h .

Definition implies P Q := h, assn_sem P hassn_sem Q h.

Definition precise P :=
hP (SEM: assn_sem P hP) hP´ (SEM´: assn_sem P hP´)
hF (DEF: hplus hP hF Hundef) hF´ (EQ: hplus hP hF = hplus hP´ hF´),
hP = hP´ hF = hF´.

Definition normalizable P :=
h, assn_sem P h hN , assn_sem P hN HlabeledExact hN HLnormal h = hplus hN .

Definition Anot P := Aimplies P Afalse.
Definition Adisj P Q := Aimplies (Anot P) Q.
Definition Aexists PP := Anot (Aforall (fun xAnot (PP x))).