Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import permission fslassn.
Require Import GpsSepAlg.

Set Implicit Arguments.

Model of heaps

Assertions modulo the syntactic rules

Definition assn_mod PS PSg := { P : assn PS PSg | 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
  | HLCnabladot
  | 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
    | HLCnabladot , _lbl2 = HLCnabladot 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.

The heap

Definition permissionsOK (PS : Permission) (x y z: PS) := << PSUMdef: x ## y ## z Pundef PS >>
                                                            << PSUMnonzero: x ## y ## z Pzero PS >>.
Arguments permissionsOK [PS] _ _ _.

Inductive HeapVal PS PSg :=
  | HVnone
  | HVuval (lbl: HeapLabel)
  | HVval (v: val) (Perm: Permission) (pNormal pTriangle pNabla : Perm)
                   (WFperm: permissionsOK pNormal pTriangle pNabla)
  | HVra (RR QQ: val assn_mod PS PSg) (isrmwflag: bool) (permlbl: option HeapLabelCombination)
          (init: option HeapLabelCombination).

Arguments HVnone {PS} {PSg}.

Arguments HVuval [PS] [PSg] _.

Arguments HVval [PS] [PSg] _ _ _ _ _ _.

Arguments HVra [PS] [PSg] _ _ _ _ _.

Program Definition lvalue PS PSg Perm v := @HVval PS PSg v Perm (Pfull Perm) (Pzero Perm) (Pzero Perm) _.
Next Obligation. split; pplus_zero_simpl; eauto using Pfull_is_not_Pzero, Pfull_is_not_Pundef. Qed.

Inductive heap PS PSg :=
  | Hundef
  | Hdef (hf: val HeapVal PS PSg) (g : ghost_resource).

Heap cell contains label lbl.

Definition HVlabeled PS PSg (hv : HeapVal PS PSg) (lbl : HeapLabel) :=
  match hv with
    | HVnoneTrue
    | HVuval lbl'lbl' = lbl
    | HVval _ Perm pNormal pTriangle pNabla _match lbl with
                                                   | HLnormalpNormal Pzero Perm
                                                   | HLtrianglepTriangle Pzero Perm
                                                   | HLnablapNabla Pzero Perm
                                                 end
    | 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 PS PSg (hf : val HeapVal PS PSg) lbl := (l: val) , HVlabeled (hf l) lbl.

Definition Hlabeled PS PSg (h : heap PS PSg) lbl := hf g, h = Hdef hf g HFlabeled hf lbl.

Heap cell contains olny lbl as label.

Definition HVlabeledExact PS PSg (hv: HeapVal PS PSg) (lbl: HeapLabel) :=
  match hv with
    | HVnoneTrue
    | HVuval lbl'lbl' = lbl
    | HVval _ Perm pNormal pTriangle pNabla _
              match lbl with
                | HLnormalpTriangle = Pzero Perm pNabla = Pzero Perm
                | HLtrianglepNormal = Pzero Perm pNabla = Pzero Perm
                | HLnablapNormal = Pzero Perm pTriangle = Pzero Perm
              end
    | 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 PS PSg (hf: val HeapVal PS PSg) lbl := (l: val), HVlabeledExact (hf l) lbl.

Definition HlabeledExact PS PSg (h: heap PS PSg) lbl := hf g, h = Hdef hf g HFlabeledExact hf lbl.

Read permision carries lbl as label.

Definition HVlabeledR PS PSg (hv: HeapVal PS PSg) (lbl: HeapLabel) :=
  match hv with
    | HVnoneFalse
    | HVuval _False
    | HVval _ Perm pNormal pTriangle pNabla _match lbl with
                                                   | HLnormalpNormal Pzero Perm
                                                   | HLtrianglepTriangle Pzero Perm
                                                   | HLnablapNabla Pzero Perm
                                                 end
    | HVra _ _ _ _ (Some initlbl) ⇒ HLleq lbl initlbl
    | _False
  end.

Heap similarity

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

Definition HVsim PS PSg (hv hv': HeapVal PS PSg) :=
  match hv, hv' with
    | HVnone, HVnoneTrue
    | HVuval _, HVuval _True
    | HVval v Perm pNormal pTriangle pNabla _, HVval v' Perm' pNormal' pTriangle' pNabla' _
                 ⇒ match excluded_middle_informative (Perm = Perm') return Prop with
                      | right _False
                      | left EQv = v'
                                   (eq_rect Perm (fun xx) pNormal Perm' EQ)
                                   ## (eq_rect Perm (fun xx) pTriangle Perm' EQ)
                                   ## (eq_rect Perm (fun xx) pNabla Perm' EQ)
                                   = pNormal' ## pTriangle' ## pNabla'
                    end
    | HVra RR QQ isrmwflag permlbl init, HVra RR' QQ' isrmwflag' permlbl' init'
                 ⇒ RR = RR' QQ = QQ' isrmwflag = isrmwflag' HLCsim permlbl permlbl' HLCsim init init'
    | _, _False
  end.

Definition HFsim PS PSg (hf hf': val HeapVal PS PSg) := (l: val), HVsim (hf l) (hf' l).

Definition Hsim PS PSg (h h': heap PS PSg) := hf hf' g, h = Hdef hf g h' = Hdef hf' g HFsim hf hf'.

Program Definition lupd PS PSg (h: heap PS PSg) lbl :=
  match h return heap PS PSg with
    | Hundef _ _Hundef PS PSg
    | Hdef hf gHdef (fun l
                          match hf l return HeapVal PS PSg with
                            | HVnone ⇒ @HVnone PS PSg
                            | HVuval _ ⇒ @HVuval PS PSg lbl
                            | HVval v Perm pNormal pTriangle pNabla _
                                ⇒ match lbl return HeapVal PS PSg with
                                   | HLnormal
                                       ⇒ @HVval PS PSg v
                                                 Perm (pNormal ## pTriangle ## pNabla) (Pzero Perm) (Pzero Perm) _
                                   | HLtriangle
                                       ⇒ @HVval PS PSg v
                                                 Perm (Pzero Perm) (pNormal ## pTriangle ## pNabla) (Pzero Perm) _
                                   | HLnabla
                                       ⇒ @HVval PS PSg v
                                                 Perm (Pzero Perm) (Pzero Perm) (pNormal ## pTriangle ## pNabla) _
                                   end
                            | 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) g
  end.
Next Obligation. by red; rewrite ?permission_plus_zero_r, ?permission_plus_zero_l. Qed.
Next Obligation. by red; rewrite ?permission_plus_zero_r, ?permission_plus_zero_l. Qed.
Next Obligation. by red; rewrite ?permission_plus_zero_r, ?permission_plus_zero_l. Qed.

Arguments Hundef {PS} {PSg}.

Definition is_lvalue PS PSg (v: HeapVal PS PSg) :=
  match v with
    | HVuval lbllbl = HLnormal
    | HVval _ Perm pNormal _ _ _pNormal = Pfull Perm
    | _False
  end.

Definition is_rvalue PS PSg (v: HeapVal PS PSg) :=
  match v with
    | HVval _ Perm pNormal _ _ _pNormal Pzero Perm
    | _False
  end.

Definition is_rvalueV PS PSg (hv: HeapVal PS PSg) v :=
  match hv with
    | HVval v' Perm pNormal _ _ _v = v' pNormal Pzero Perm
    | _False
  end.

Definition has_value PS PSg (hv: HeapVal PS PSg) v :=
  match hv with
    | HVval v' _ _ _ _ _v' = v
    | _False
  end.

Definition is_nonatomic PS PSg (hv: HeapVal PS PSg) :=
  match hv with
    | HVval _ _ _ _ _ _true
    | HVuval _true
    | _false
  end.

Definition is_atomic PS PSg (hv: HeapVal PS PSg) :=
  match hv with
    | HVra _ _ _ _ _true
    | _false
  end.

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

Definition hemp {PS} {PSg} := Hdef (fun v ⇒ @HVnone PS PSg) gres_emp.

Heap compatibility
Definition Acombinable PS PSg (P Q : assn PS PSg) :=
  P = Afalse Q = Afalse P = Q.

Definition hv_rval PS PSg isrmw (P: assn PS PSg) :=
  match isrmw with
    | trueP
    | falseAemp
  end.

Definition hv_acq_def PS PSg isrmw1 Q1 isrmw2 Q2 :=
  hv_rval isrmw2 Q1 = hv_rval isrmw1 Q2
   Q1 = (@Afalse PS PSg) Q2 = (@Afalse PS PSg).

Definition hvplusDEF PS PSg (hv hv' : HeapVal PS PSg) : Prop :=
  match hv, hv' return Prop with
    | HVnone, _True
    | _, HVnoneTrue
    | HVuval _, HVuval _False
    | HVval v Perm pNormal pTriangle pNabla _, HVval v' Perm' pNormal' pTriangle' pNabla' _
        match excluded_middle_informative (Perm = Perm') return Prop with
          | right _False
          | left EQv = v'
                       permissionsOK ((eq_rect Perm (fun xx) pNormal Perm' EQ) ## pNormal')
                                     ((eq_rect Perm (fun xx) pTriangle Perm' EQ) ## pTriangle')
                                     ((eq_rect Perm (fun xx) pNabla Perm' EQ) ## pNabla')
        end
    | HVra RR1 QQ1 isrmw1 permlbl1 init1, HVra RR2 QQ2 isrmw2 permlbl2 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
    | HLCnabladot , HLCtriangledotHLCdiamonddot
    | HLCnabladot , HLCdiamondHLCdiamonddot
    | HLCnabladot , HLCtriangleHLCdiamonddot
    | HLCnabladot , _HLCnabladot
    | HLCtriangledot , HLCnabladotHLCdiamonddot
    | HLCtriangledot , HLCdiamondHLCdiamonddot
    | HLCtriangledot , HLCnablaHLCdiamonddot
    | HLCtriangledot , _HLCtriangledot
    | HLCdiamond , HLCnabladotHLCdiamonddot
    | HLCdiamond , HLCtriangledotHLCdiamonddot
    | HLCdiamond , HLCnormalHLCdiamonddot
    | HLCdiamond , _HLCdiamond
    | HLCnabla , HLCnabladotHLCnabladot
    | HLCnabla , HLCtriangledotHLCdiamonddot
    | HLCnabla , HLCdiamondHLCdiamond
    | HLCnabla , HLCnablaHLCnabla
    | HLCnabla , HLCtriangleHLCdiamond
    | HLCnabla , HLCnormalHLCnabladot
    | HLCtriangle , HLCnabladotHLCdiamonddot
    | HLCtriangle , HLCtriangledotHLCtriangledot
    | HLCtriangle , HLCdiamondHLCdiamond
    | HLCtriangle , HLCnablaHLCdiamond
    | HLCtriangle , HLCtriangleHLCtriangle
    | HLCtriangle , HLCnormalHLCtriangledot
    | HLCnormal , HLCnabladotHLCnabladot
    | HLCnormal , HLCtriangledotHLCtriangledot
    | HLCnormal , HLCdiamondHLCdiamonddot
    | HLCnormal , HLCnablaHLCnabladot
    | 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.

Program Definition hvplus PS PSg (hv hv' : HeapVal PS PSg) : HeapVal PS PSg :=
  match hv, hv' return HeapVal PS PSg with
    | HVnone, _hv'
    | _, HVnonehv
    | HVval v Perm pNormal pTriangle pNabla _, HVval v' Perm' pNormal' pTriangle' pNabla' _
        match excluded_middle_informative (Perm = Perm') return HeapVal PS PSg with
          | right _ ⇒ @HVval PS PSg 0 Perm' (Pfull Perm') (Pzero Perm') (Pzero Perm') _
          | left EQif excluded_middle_informative
                            (permissionsOK ((eq_rect Perm (fun xx) pNormal Perm' EQ) ## pNormal')
                                           ((eq_rect Perm (fun xx) pTriangle Perm' EQ) ## pTriangle')
                                           ((eq_rect Perm (fun xx) pNabla Perm' EQ) ## pNabla'))
                       then @HVval PS PSg v Perm' ((eq_rect Perm (fun xx) pNormal Perm' EQ) ## pNormal')
                                                  ((eq_rect Perm (fun xx) pTriangle Perm' EQ) ## pTriangle')
                                                  ((eq_rect Perm (fun xx) pNabla Perm' EQ) ## pNabla') _
                       else @HVval PS PSg 0 Perm' (Pfull Perm') (Pzero Perm') (Pzero Perm') _
        end
    | HVra RR1 QQ1 isrmw1 permlbl1 init1, HVra RR2 QQ2 isrmw2 permlbl2 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 permlbl1 permlbl2)
              (ohlplus init1 init2)
    | _, _hv
  end.
Next Obligation.
  split; rewrite !permission_plus_zero_r; [apply Pfull_is_not_Pundef | apply Pfull_is_not_Pzero].
Qed.
Next Obligation.
  split; rewrite !permission_plus_zero_r; [apply Pfull_is_not_Pundef | apply Pfull_is_not_Pzero].
Qed.

Definition resources_compatible PS PSg (hf1 hf2: val HeapVal PS PSg) (g1 g2 : ghost_resource) :=
  excluded_middle_informative (
     << HEAPcompat: v, hvplusDEF (hf1 v) (hf2 v) >>
     << GHOSTcompat: gres_plus g1 g2 None>> ).

Definition hplus PS PSg (h1 h2: heap PS PSg) : heap PS PSg :=
  match h1, h2 with
    | Hundef, _Hundef
    | _, HundefHundef
    | Hdef hf1 g1, Hdef hf2 g2
      if resources_compatible hf1 hf2 g1 g2 then
        Hdef (fun vhvplus (hf1 v) (hf2 v)) (gres_plus_total g1 g2)
      else Hundef
  end.

hsum : iterated hplus

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

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

Singleton heap cell

Notation hsingl PS PSg l v := (Hdef (hupd (fun _ ⇒ @HVnone PS PSg) l v) gres_emp).

Notation gsingl PS PSg l g := (Hdef (fun _ : val ⇒ @HVnone PS PSg) (gres_one l g)).

Notation gheap PS PSg g := (Hdef (fun _ ⇒ @HVnone PS PSg) g).

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

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

Global Opaque hplus.

Assertion semantics


Definition Wemp {PS} {PSg} : val assn_mod PS PSg := fun _mk_assn_mod Afalse.
Definition Remp {PS} {PSg} : val assn_mod PS PSg := fun _mk_assn_mod Aemp.

Lemma equal_exist:
   (U : Type) (P : U Prop) (x y : U) (p : P x) (q : P y),
  x = y exist P x p = exist P y q.
Proof.
  ins; desf; f_equal; apply proof_irrelevance.
Qed.

Program Fixpoint assn_sem PS PSg (P : assn PS PSg) (h : heap PS PSg) :=
  match P with
    | AfalseFalse
    | Aemph = hemp
    | Aimplies P Qh Hundef (assn_sem P h assn_sem Q h)
    | Aforall PP x, assn_sem (PP x) h
    | Apt Perm _ p _ E E'h = hsingl PS PSg E (@HVval PS PSg E' Perm p (Pzero Perm) (Pzero Perm) _)
    | Aptu Eh = hsingl PS PSg E (@HVuval PS PSg HLnormal)
    | Astar P Q h1 h2, h Hundef hplus h1 h2 = h assn_sem P h1 assn_sem Q h2
    | Arainit Eh = hsingl PS PSg E (HVra Wemp Remp false None (Some HLCnormal))
    | Arel E Ph = hsingl PS PSg E (HVra (fun xmk_assn_mod (P x)) Remp false (Some HLCnormal) None)
    | Aacq E Qh = hsingl PS PSg E (HVra Wemp (fun xmk_assn_mod (Q x)) false None None)
    | Armwacq E Qh = hsingl PS PSg E (HVra Wemp (fun xmk_assn_mod (Q x)) true (Some HLCnormal) None)
    | Atriangle QHlabeledExact h HLtriangle
                        h', assn_sem Q h' Hsim h h' HlabeledExact h' HLnormal
    | Anabla QHlabeledExact h HLnabla
                        h', assn_sem Q h' Hsim h h' HlabeledExact h' HLnormal
    | Aghost PCM _ E gh = gsingl PS PSg E (Some (existT (fun m : salg_modm) PCM g))
end.
Next Obligation. by red; rewrite !permission_plus_zero_r. Qed.

Definition implies PS PSg (P Q: assn PS PSg) := h, assn_sem P h assn_sem Q h.

Definition precise PS PSg (P: assn PS PSg) :=
   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 PS PSg (P: assn PS PSg) :=
   h, assn_sem P h hN h', assn_sem P hN HlabeledExact hN HLnormal h = hplus hN h'.

Definition Anot PS PSg (P: assn PS PSg) := Aimplies P Afalse.
Definition Adisj PS PSg (P Q: assn PS PSg) := Aimplies (Anot P) Q.
Definition Aconj PS PSg (P Q: assn PS PSg) := Anot (Adisj (Anot P) (Anot Q)).
Definition Aexists PS PSg (PP: val assn PS PSg) := Anot (Aforall (fun xAnot (PP x))).


This page has been generated by coqdoc