Assertions

Require Import Omega.
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 : val → assn)
  | Apt (E E' : val)
  | Aptu (E : val)
  | Astar (P Q: assn)
  | Arainit (E : val)
  | Arel (E : val) (Q : val → assn)
  | Aacq (E: val) (Q : val → assn)
  | Armwacq (E: val) (Q : val → assn).

Definition Atrue := Aimplies Afalse Afalse.

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

Inductive Asim : assn → assn → Prop :=
  | 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 (H': 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).

Lemma lenT e1 e2: (e1 ≤ e2) = false → e2 ≤ e1.

Lemma lenAS e1 e2 : e1 ≤ e2 → e2 ≤ e1 → e1 = e2.

Lemma assn_eqP : Equality.axiom (fun x y : assn ⇒ mydec (x = y)).

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

Definition leq_fun A (leq : A → A → bool) 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
    | _ , Afalse ⇒ false
    | Aemp , _ ⇒ true
    | _ , Aemp ⇒ false
    | Aimplies P Q, Aimplies P' Q' ⇒ if P == P' then assn_leq Q Q' else assn_leq P 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 P' Q' ⇒ if P == P' then assn_leq Q Q' else assn_leq P P'
    | Astar _ _ , _ ⇒ true
    | _ , Astar _ _ ⇒ false
    | Arainit E , Arainit E' ⇒ E ≤ E'
    | Arainit _ , _ ⇒ true
    | _ , Arainit _ ⇒ false
    | Arel E PP , Arel E' PP' ⇒ if E == E' then leq_fun assn_leq PP PP' else E ≤ E'
    | Arel _ _ , _ ⇒ true
    | _ , Arel _ _ ⇒ false
    | Aacq E PP , Aacq E' PP' ⇒ if E == E' then leq_fun assn_leq PP PP' else E ≤ E'
    | Aacq _ _ , _ ⇒ true
    | _ , Aacq _ _ ⇒ false
    | Armwacq E PP, Armwacq E' PP' ⇒ if E == E' then leq_fun assn_leq PP PP' else E ≤ E'
  end.

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

Lemma leq_fun_trans A (leq : A → A → bool) p q r
  (AS: ∀ p q, leq p q → leq q p → p = q)
  (T: ∀ x, leq (p x) (q x) → leq (q x) (r x) → leq (p x) (r x)) :
  leq_fun (A:=A) leq p q → leq_fun leq q r → leq_fun leq p r.

Lemma assn_leqAS :
  ∀ p q, assn_leq p q → assn_leq q p → p = q.

Lemma assn_leq_refl :
  ∀ p, assn_leq p p.

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

Lemma neq_min_neq A (f g : nat → A) (NEQ: f ≠ g) :
  ∃ m, f m ≠ g m ∧ (∀ x, x < m → f x = g x).

Lemma assn_leqT :
  ∀ p q, assn_leq p q = false → assn_leq q p.

Lemma assn_leq_false_ne :
  ∀ p q, assn_leq p q = false → p ≠ q.

Lemma assn_leqTT :
  ∀ p q, assn_leq p q = false → p ≠ q ∧ assn_leq q p = true.

Lemma assn_leq_AfalseD P : assn_leq P Afalse → P = Afalse.

Opaque assn_leq.

Normalization


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

Definition assn_merge_fst P :=
  match P with
    | Astar p q ⇒ p
    | _ ⇒ P
  end.

Definition assn_merge_snd P :=
  match P with
    | Astar p q ⇒ Some 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 q ⇒ assn_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 q ⇒ assn_wf p ∧ assn_wf q
    | Arel _ pp
    | Aacq _ pp
    | Armwacq _ pp
    | Aforall pp ⇒ ∀ x, assn_wf (pp x)
  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
                 | None ⇒ P
                 | Some Q' ⇒ @assn_merge_rec P Q' sz
               end)
        else
        Astar (assn_merge_fst P)
              (match assn_merge_snd P with
                 | None ⇒ Q
                 | Some P' ⇒ @assn_merge_rec P' Q sz
               end)
      else
        Astar (assn_merge_fst Q)
              (match assn_merge_snd Q with
                 | None ⇒ P
                 | Some Q' ⇒ @assn_merge_rec P Q' 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
  | Afalse ⇒ Afalse
  | Aemp ⇒ Aemp
  | Aimplies P Q ⇒ Aimplies (assn_norm P) (assn_norm Q)
  | Aforall PP ⇒ Aforall (fun x ⇒ assn_norm (PP x))
  | Apt E E' ⇒ Apt E E'
  | Aptu E ⇒ Aptu E
  | Astar P Q ⇒
      let P' := assn_norm P in
      let Q' := assn_norm Q in
      if P' == Aemp then Q'
      else if Q' == Aemp then P'
      else assn_merge P' Q'
  | Arainit E ⇒ Arainit E
  | Arel E QQ ⇒ Arel E (fun v ⇒ assn_norm (QQ v))
  | Aacq E QQ ⇒ Aacq E (fun v ⇒ assn_norm (QQ v))
  | Armwacq E QQ ⇒ Armwacq E (fun v ⇒ assn_norm (QQ v))
  end.

Lemmas about assn_merge

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 p → assn_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 p' q' ⇒
      if assn_leq p p' then assn_star_rdf p q
      else Astar p' (assn_insert p q')
    | _ ⇒
      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 p → assn_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 : Prop); [|by clear -H; destruct p]; clear H; intro H
    | H : assn_leq ?p ?q = true, H' : assn_leq ?q ?p = true |- _ ⇒
      eapply assn_leqAS in H; eauto; try subst p; try subst q
    | H : assn_leq ?p ?q = true, H' : 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 p → assn_not_star q → assn_insert p q = assn_insert q p.

Lemma assn_insertC r p q :
  assn_not_star p → assn_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
    | None ⇒ assn_insert p q
    | Some p' ⇒ assn_insert (assn_merge_fst p) (assn_merge_rec p' 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.

Lemma assn_norm_ok : ∀ P Q, Asim P Q ↔ assn_norm P = assn_norm Q.

Lemma assn_norm_idemp P : assn_norm (assn_norm P) = assn_norm P.

Lemma assn_norm_emp : assn_norm Aemp = Aemp.

Lemma assn_norm_star_emp P : assn_norm (Astar Aemp P) = assn_norm P.

Lemma assn_norm_star_emp_r P : assn_norm (Astar P Aemp) = assn_norm P.

Lemma assn_norm_star_eq_emp P Q :
  assn_norm (Astar P Q) = Aemp →
  assn_norm P = Aemp ∧ assn_norm Q = Aemp.

Lemma assn_merge_rec_not_false P Q n :
  assn_wf Q →
  assn_merge_rec P Q n = Afalse → P = Afalse ∧ Q = Afalse.

Lemma assn_norm_star_eq_false P Q :
  assn_norm (Astar P Q) = Afalse →
  assn_norm P = Aemp ∧ assn_norm Q = Afalse
  ∨ assn_norm P = Afalse ∧ assn_norm Q = Aemp
  ∨ assn_norm P = Afalse ∧ assn_norm Q = Afalse.

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 P' R R':
  Asim (Astar P R) (Astar P' R') →
  Asim (Astar (Astar P Q) R)
       (Astar (Astar P' Q) R').

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' Q', P = Astar P' Q' ∧
   (Asim P' Afalse ∧ Asim Q' Aemp ∨
    Asim P' Aemp ∧ Asim Q' Afalse ∨
    Asim P' Afalse ∧ Asim Q' 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 ≠ Aemp → Q ≠ Aemp →
  ∃ P' Q', assn_merge_rec P Q n = Astar P' Q'.

Lemma Asim_starD P Q R :
  Asim (Astar P Q) R →
  (∃ P' Q', R = Astar P' Q') ∨
  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)) q'
    (NF': ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q') = Afalse))
    (EQ: assn_insert p q = assn_insert p q'),
   assn_wf q → assn_wf q' → q = 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)) q'
    (NF': ¬ (p = Afalse ∧ assn_merge_fst (assn_norm q') = Afalse))
    (EQ: assn_insert p q = assn_insert p q')
    (WF: assn_wf q) (WF': assn_wf q'),
  q = q'.

Lemma assn_merge_cancel :
  ∀ n m q' q p
    (LT: assn_merge_size p + assn_merge_size q < n)
    (LT': assn_merge_size p + assn_merge_size q' < 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 q') = Afalse))
    (EQ: assn_merge_rec p q n = assn_merge_rec p q' m),
    p ≠ Aemp → q ≠ Aemp → q' ≠ Aemp →
    assn_wf p → assn_wf q → assn_wf q' → q = 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 ∧ ∃ P', Asim P (Astar Afalse P').

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

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 }.

Inductive HeapVal :=
  | HVnone
  | HVuval
  | HVval (v: val)
  | HVra (RR QQ: val → assn_mod) (isrmwflag: bool) (init: bool).

Inductive heap :=
  | Hundef
  | Hdef (hf: val → HeapVal).

Definition is_val v :=
  match v with
      HVval _ | HVuval ⇒ true
    | HVnone | HVra _ _ _ _ ⇒ false
  end.

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

Definition hemp : heap := Hdef (fun v ⇒ HVnone).

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

Definition hv_rval isrmw P :=
  match isrmw with
    | true ⇒ P
    | false ⇒ Aemp
  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
    | _, HVnone ⇒ True
    | HVra RR1 QQ1 isrmw1 init1, HVra RR2 QQ2 isrmw2 init2 ⇒
        (∀ v, hv_acq_def isrmw1 (sval (QQ1 v)) isrmw2 (sval (QQ2 v))) ∧
        (∀ v, Acombinable (sval (RR1 v)) (sval (RR2 v)))
    | _, _ ⇒ False
  end.

Definition hvplus (hv hv' : HeapVal) : HeapVal :=
  match hv, hv' with
    | HVnone, _ ⇒ hv'
    | _, HVnone ⇒ hv
    | HVra RR1 QQ1 isrmw1 init1, HVra RR2 QQ2 isrmw2 init2 ⇒
        HVra (fun v ⇒ if excluded_middle_informative (sval (RR1 v) = Afalse) then RR2 v else RR1 v)
              (if isrmw1 then QQ1
                else if isrmw2 then QQ2
                else fun v ⇒ mk_assn_mod (Astar (sval (QQ1 v)) (sval (QQ2 v))))
              (isrmw1 || isrmw2)
              (init1 || init2)
    | _, _ ⇒ hv
  end.

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

hsum : iterated hplus

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

Definition hupd B (h : nat → B) y z := fun x ⇒ if x == y then z else h x.

Singleton heap cell

Notation hsingl l v := (Hdef (hupd (fun _ ⇒ HVnone) l v)).

initialize : set the initialization bit of a Rel-Acq location

Definition initialize h l :=
  hupd h l (match h l with
              | HVra PP QQ isrmw _ ⇒ HVra PP QQ isrmw true
              | _ ⇒ h l end).

Global Opaque hplus.

Assertion semantics


Definition Wemp : val → assn_mod := fun _ ⇒ mk_assn_mod Afalse.
Definition Remp : val → assn_mod := fun _ ⇒ mk_assn_mod Aemp.

Fixpoint assn_sem (P : assn) (h : heap) :=
  match P with
    | Afalse ⇒ False
    | Aemp ⇒ h = hemp
    | Aimplies P Q ⇒ h ≠ Hundef ∧ (assn_sem P h → assn_sem Q h)
    | Aforall PP ⇒ ∀ x, assn_sem (PP x) h
    | Apt E E' ⇒ h = hsingl E (HVval E')
    | Aptu E ⇒ h = hsingl E HVuval
    | Astar P Q ⇒
        ∃ h1 h2, h ≠ Hundef ∧ hplus h1 h2 = h ∧ assn_sem P h1 ∧ assn_sem Q h2
    | Arainit E ⇒ h = Hdef (hupd (fun _ ⇒ HVnone) E (HVra Wemp Remp false true))
    | Arel E P ⇒ h = hsingl E (HVra (fun x ⇒ mk_assn_mod (P x)) Remp false false)
    | Aacq E Q ⇒ h = hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (Q x)) false false)
    | Armwacq E Q ⇒ h = hsingl E (HVra Wemp (fun x ⇒ mk_assn_mod (Q x)) true false)
  end.

Definition implies P Q := ∀ h, assn_sem P h → assn_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 Anot P := Aimplies P Afalse.
Definition Adisj P Q := Aimplies (Anot P) Q.
Definition Aexists PP := Anot (Aforall (fun x ⇒ Anot (PP x))).
This page has been generated by coqdoc Imprint | Data protection