Theory OG_Hoare

(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)
section ‹ Owicki-Gries for Partial Correctness ›
theory OG_Hoare
imports OG_Annotations 
begin

subsection ‹Validity of Hoare Tuples: ‹Γ⊨⇘/F⇙ P c Q,A››

definition
  valid :: "[('s,'p,'f) body,'f set,'s assn,('s,'p,'f) com,'s assn,'s assn] => bool"
                (‹_ ⊨⇘'/_⇙/ _ _ _, _›  [61,60,1000, 20, 1000,1000] 60)
where
  "Γ ⊨⇘/F⇙ P c Q,A ≡ ∀s t c'. Γ⊢(c,s) →⇧* (c', t) ⟶ final (c', t ) ⟶ s ∈ Normal ` P ⟶ t ∉ Fault ` F  
                      ⟶  c' = Skip ∧ t ∈ Normal ` Q ∨ c' = Throw ∧ t ∈ Normal ` A"

subsection ‹Interference Freedom›

inductive
 atomicsR :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ ('s, 'p, 'f) ann ⇒ ('s,'p,'f) com ⇒ ('s assn × ('s, 'p, 'f) com) ⇒ bool"
  for Γ::"('s,'p,'f) body"
  and Θ :: " ('s,'p,'f) proc_assns"
where
  AtBasic: "atomicsR Γ Θ (AnnExpr p) (Basic f) (p, Basic f)"
| AtSpec: "atomicsR Γ Θ (AnnExpr p) (Spec r) (p, Spec r)"
| AtAwait: "atomicsR Γ Θ (AnnRec r ae) (Await b e) (r ∩ b, Await b e)"
| AtWhileExpr: "atomicsR Γ Θ p e a ⟹ atomicsR Γ Θ (AnnWhile r i p) (While b e) a"
| AtGuardExpr: "atomicsR Γ Θ p e a ⟹ atomicsR Γ Θ (AnnRec r p) (Guard f b e) a" 
| AtDynCom: "x ∈ r ⟹ atomicsR Γ Θ ad (f x) a ⟹ atomicsR Γ Θ (AnnRec r ad) (DynCom f) a" 
| AtCallExpr: "Γ f = Some b ⟹ Θ f = Some as ⟹
                n < length as ⟹
                atomicsR Γ Θ  (as!n) b a ⟹
               atomicsR Γ Θ (AnnCall r n) (Call f) a"
| AtSeqExpr1: "atomicsR Γ Θ  a1 c1 a ⟹
               atomicsR Γ Θ (AnnComp a1 a2) (Seq c1 c2) a" 
| AtSeqExpr2: "atomicsR Γ Θ  a2 c2 a ⟹
               atomicsR Γ Θ (AnnComp a1 a2) (Seq c1 c2) a" 
| AtCondExpr1: "atomicsR Γ Θ  a1 c1 a ⟹
               atomicsR Γ Θ (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AtCondExpr2: "atomicsR Γ Θ  a2 c2 a ⟹
               atomicsR Γ Θ (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AtCatchExpr1: "atomicsR Γ Θ  a1 c1 a ⟹
               atomicsR Γ Θ (AnnComp a1 a2) (Catch c1 c2) a" 
| AtCatchExpr2: "atomicsR Γ Θ  a2 c2 a ⟹
               atomicsR Γ Θ (AnnComp a1 a2) (Catch c1 c2) a" 
| AtParallelExprs: "i < length cs ⟹ atomicsR Γ Θ (fst (as!i)) (cs!i) a ⟹
    atomicsR Γ Θ (AnnPar as) (Parallel cs) a"

lemma atomicsR_Skip[simp]:
  "atomicsR Γ Θ a Skip r = False"
 by (auto elim: atomicsR.cases)

lemma atomicsR_Throw[simp]:
  "atomicsR Γ Θ a Throw r = False"
 by (auto elim: atomicsR.cases)

inductive
 assertionsR :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 's assn ⇒ 's assn ⇒ ('s, 'p, 'f) ann ⇒ ('s,'p,'f) com ⇒ 's assn ⇒ bool"
  for Γ::"('s,'p,'f) body"
  and Θ :: " ('s,'p,'f) proc_assns"
where
  AsSkip: "assertionsR Γ Θ Q A (AnnExpr p) Skip p"
| AsThrow: "assertionsR Γ Θ Q A (AnnExpr p) Throw p"
| AsBasic: "assertionsR Γ Θ Q A (AnnExpr p) (Basic f) p"
| AsBasicSkip: "assertionsR Γ Θ Q A (AnnExpr p) (Basic f) Q"
| AsSpec: "assertionsR Γ Θ Q A (AnnExpr p) (Spec r) p"
| AsSpecSkip: "assertionsR Γ Θ Q A (AnnExpr p) (Spec r) Q"
| AsAwaitSkip: "assertionsR Γ Θ Q A (AnnRec r ae) (Await b e) Q"
| AsAwaitThrow: "assertionsR Γ Θ Q A (AnnRec r ae) (Await b e) A"
| AsAwait: "assertionsR Γ Θ Q A (AnnRec r ae) (Await b e) r"
| AsWhileExpr: "assertionsR Γ Θ i A p e a ⟹ assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) a" 
| AsWhileAs: "assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) r"
| AsWhileInv: "assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) i"
| AsWhileSkip: "assertionsR Γ Θ Q A (AnnWhile r i p) (While b e) Q"
| AsGuardExpr: "assertionsR Γ Θ Q A p e a ⟹ assertionsR Γ Θ Q A (AnnRec r p) (Guard f b e) a" 
| AsGuardAs: "assertionsR Γ Θ Q A (AnnRec r p) (Guard f b e) r" 
| AsDynComExpr: "x ∈ r ⟹ assertionsR Γ Θ Q A ad (f x) a ⟹ assertionsR Γ Θ Q A (AnnRec r ad) (DynCom f) a" 
| AsDynComAs: "assertionsR Γ Θ Q A (AnnRec r p) (DynCom f) r" 
| AsCallAs: "assertionsR Γ Θ Q A (AnnCall r n) (Call f) r" 
| AsCallExpr: "Γ f = Some b ⟹ Θ f = Some as ⟹
                n < length as ⟹
                assertionsR Γ Θ Q A (as!n) b a ⟹
               assertionsR Γ Θ Q A (AnnCall r n) (Call f) a" 
| AsSeqExpr1: "assertionsR Γ Θ (pre a2) A a1 c1 a ⟹
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Seq c1 c2) a" 
| AsSeqExpr2: "assertionsR Γ Θ Q A a2 c2 a ⟹
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Seq c1 c2) a" 
| AsCondExpr1: "assertionsR Γ Θ Q A a1 c1 a ⟹
               assertionsR Γ Θ Q A (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AsCondExpr2: "assertionsR Γ Θ Q A a2 c2 a ⟹
               assertionsR Γ Θ Q A (AnnBin r a1 a2) (Cond b c1 c2) a" 
| AsCondAs: "assertionsR Γ Θ Q A (AnnBin r a1 a2) (Cond b c1 c2) r" 
| AsCatchExpr1: "assertionsR Γ Θ Q (pre a2) a1 c1 a ⟹
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Catch c1 c2) a" 
| AsCatchExpr2: "assertionsR Γ Θ Q A a2 c2 a ⟹
               assertionsR Γ Θ Q A (AnnComp a1 a2) (Catch c1 c2) a" 

| AsParallelExprs: "i < length cs ⟹ assertionsR Γ Θ (postcond (as!i)) (abrcond (as!i)) (pres (as!i)) (cs!i) a ⟹
    assertionsR Γ Θ Q A (AnnPar as) (Parallel cs) a" 
| AsParallelSkips: "Qs = ⋂ (set (map postcond as)) ⟹
  assertionsR Γ Θ Q A (AnnPar as) (Parallel cs) (Qs)" 

definition
  interfree_aux :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set ⇒ (('s,'p,'f) com × ('s, 'p, 'f) ann_triple × ('s,'p,'f) com × ('s, 'p, 'f) ann) ⇒ bool"
where
  "interfree_aux Γ Θ F ≡ λ(c⇩1, (P⇩1, Q⇩1, A⇩1), c⇩2, P⇩2).
                              (∀p c .atomicsR Γ Θ P⇩2 c⇩2 (p,c) ⟶ 
                               Γ⊨⇘/F⇙ (Q⇩1 ∩ p) c Q⇩1,Q⇩1  ∧ Γ⊨⇘/F⇙ (A⇩1 ∩ p) c A⇩1,A⇩1  ∧
                                (∀a. assertionsR Γ Θ Q⇩1 A⇩1 P⇩1 c⇩1 a ⟶ Γ⊨⇘/F⇙ (a ∩ p) c a,a))"

definition
  interfree :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set ⇒ (('s, 'p, 'f) ann_triple) list ⇒ ('s,'p,'f) com list  ⇒ bool"
where 
  "interfree Γ Θ F Ps Ts ≡ ∀i j. i < length Ts ∧ j < length Ts ∧ i ≠ j ⟶ 
                         interfree_aux Γ Θ F (Ts!i, Ps!i, Ts!j, fst (Ps!j))"

subsection ‹The Owicki-Gries Logic for COMPLX›

inductive
  oghoare :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set
              ⇒ ('s, 'p, 'f) ann ⇒ ('s,'p,'f) com ⇒ 's assn ⇒ 's assn ⇒ bool"
    (‹(4_, _/ ⊢⇘'/_⇙ (_/ (_)/ _, _))› [60,60,60,1000,1000,1000,1000]60)
and
  oghoare_seq :: "('s,'p,'f) body ⇒ ('s,'p,'f) proc_assns ⇒ 'f set
              ⇒ 's assn ⇒ ('s, 'p, 'f) ann ⇒ ('s,'p,'f) com ⇒ 's assn ⇒ 's assn ⇒ bool"
    (‹(4_, _/ ⊩⇘'/_⇙ (_/ _/ (_)/ _, _))› [60,60,60,1000,1000,1000,1000]60)

where
 Skip: " Γ, Θ ⊢⇘/F⇙ (AnnExpr Q) Skip Q,A"

| Throw: "Γ, Θ ⊢⇘/F⇙ (AnnExpr A) Throw Q,A"

| Basic: "Γ, Θ ⊢⇘/F⇙ (AnnExpr {s. f s ∈ Q}) (Basic f) Q,A"

| Spec: "Γ, Θ ⊢⇘/F⇙ (AnnExpr {s. (∀t. (s,t) ∈ rel ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ rel)}) (Spec rel) Q,A"

| Seq: "⟦Γ, Θ ⊢⇘/F⇙ P⇩1 c⇩1 (pre P⇩2),A;
         Γ, Θ ⊢⇘/F⇙ P⇩2 c⇩2 Q,A ⟧
         ⟹ Γ, Θ ⊢⇘/F⇙ (AnnComp P⇩1 P⇩2) (Seq c⇩1 c⇩2) Q,A"

| Catch: "⟦Γ, Θ ⊢⇘/F⇙ P⇩1 c⇩1 Q,(pre P⇩2);
           Γ, Θ ⊢⇘/F⇙ P⇩2 c⇩2 Q,A ⟧ 
      ⟹  Γ, Θ ⊢⇘/F⇙ (AnnComp P⇩1 P⇩2) (Catch c⇩1 c⇩2) Q,A"
  
| Cond: "⟦ Γ, Θ ⊢⇘/F⇙ P⇩1 c⇩1 Q,A;
           Γ, Θ ⊢⇘/F⇙ P⇩2 c⇩2 Q,A;
          r ∩ b ⊆ pre P⇩1;
          r ∩ -b ⊆ pre P⇩2 ⟧
         ⟹ 
         Γ, Θ ⊢⇘/F⇙ (AnnBin r P⇩1 P⇩2) (Cond b c⇩1 c⇩2) Q,A"

| While: "⟦ Γ, Θ ⊢⇘/F⇙ P c i,A;
            i ∩ b ⊆ pre P;
            i ∩ -b ⊆ Q;
            r ⊆ i  ⟧
          ⟹
          Γ, Θ ⊢⇘/F⇙ (AnnWhile r i P) (While b c) Q,A"

| Guard: "⟦ Γ, Θ ⊢⇘/F⇙ P c Q,A;
            r ∩ g ⊆ pre P;
            r ∩ -g ≠ {} ⟶ f ∈ F⟧ ⟹
          Γ, Θ ⊢⇘/F⇙ (AnnRec r P) (Guard f g c) Q,A"

| Call: "⟦  Θ p = Some as;
          (as ! n) = P;
          r ⊆ pre P;
          Γ p = Some b;
          n < length as;
          Γ,Θ ⊢⇘/F⇙ P b Q,A
          ⟧ 
         ⟹ 
         Γ, Θ ⊢⇘/F⇙ (AnnCall r n) (Call p) Q,A"

| DynCom:
      "r ⊆ pre a ⟹ ∀s∈r. Γ, Θ ⊢⇘/F⇙ a (c s) Q,A 
      ⟹ 
      Γ, Θ ⊢⇘/F⇙ (AnnRec r a) (DynCom c) Q,A"

| Await: "⟦Γ, Θ ⊩⇘/F⇙(r ∩ b) P c Q,A; atom_com c ⟧ ⟹
  Γ, Θ ⊢⇘/F⇙ (AnnRec r P) (Await b c) Q,A"

| Parallel: "⟦ length as = length cs;
               ∀i < length cs. Γ,Θ⊢⇘/F⇙(pres (as!i)) (cs!i) (postcond (as!i)),(abrcond (as!i));
               interfree Γ Θ F as cs;
               ⋂ (set (map postcond as)) ⊆ Q;
               ⋃ (set (map abrcond as)) ⊆ A
              ⟧
        ⟹ Γ,Θ⊢⇘/F⇙ (AnnPar as) (Parallel cs) Q,A"

| Conseq: "∃P' Q' A'. Γ,Θ⊢⇘/F⇙ (weaken_pre P P') c Q',A' ∧ Q' ⊆ Q ∧ A' ⊆ A 
           ⟹ Γ,Θ⊢⇘/F⇙ P c Q,A"

| SeqSkip:   "Γ, Θ ⊩⇘/F⇙ Q (AnnExpr x) Skip Q,A"

| SeqThrow:   "Γ, Θ ⊩⇘/F⇙ A (AnnExpr x) Throw Q,A"

| SeqBasic:   "Γ, Θ ⊩⇘/F⇙ {s. f s ∈ Q} (AnnExpr x) (Basic f) Q,A"

| SeqSpec:   "Γ, Θ ⊩⇘/F⇙ {s. (∀t. (s,t) ∈ r ⟶ t ∈ Q) ∧ (∃t. (s,t) ∈ r)} (AnnExpr x) (Spec r) Q,A"

| SeqSeq:    "⟦ Γ, Θ ⊩⇘/F⇙ R P⇩2 c⇩2 Q,A ; Γ, Θ ⊩⇘/F⇙ P P⇩1 c⇩1 R,A⟧
         ⟹ Γ, Θ ⊩⇘/F⇙ P (AnnComp P⇩1 P⇩2) (Seq c⇩1 c⇩2) Q,A"

| SeqCatch:  "⟦Γ, Θ ⊩⇘/F⇙ R P⇩2 c2 Q,A ; Γ, Θ ⊩⇘/F⇙ P P⇩1 c1 Q,R ⟧ ⟹
    Γ, Θ ⊩⇘/F⇙ P (AnnComp P⇩1 P⇩2) (Catch c1 c2) Q,A"

| SeqCond: "⟦ Γ, Θ ⊩⇘/F⇙ (P ∩ b) P⇩1 c⇩1 Q,A;
           Γ, Θ ⊩⇘/F⇙ (P ∩ -b) P⇩2 c⇩2 Q,A ⟧
         ⟹ 
         Γ, Θ ⊩⇘/F⇙ P (AnnBin r P⇩1 P⇩2) (Cond b c⇩1 c⇩2) Q,A"

| SeqWhile: "⟦ Γ, Θ ⊩⇘/F⇙ (P∩b) a c P,A ⟧
          ⟹
          Γ, Θ ⊩⇘/F⇙ P (AnnWhile r i a) (While b c) (P ∩ -b),A"

| SeqGuard: "⟦ Γ, Θ ⊩⇘/F⇙ (P∩g) a c Q,A;
            P ∩ -g ≠ {} ⟹ f ∈ F⟧ ⟹
          Γ, Θ ⊩⇘/F⇙ P (AnnRec r a) (Guard f g c) Q,A"

| SeqCall: "⟦  Θ p = Some as;
          (as ! n) = P'';
          Γ p = Some b;
          n < length as;
          Γ,Θ ⊩⇘/F⇙ P P'' b Q,A
          ⟧ 
         ⟹ 
         Γ, Θ ⊩⇘/F⇙ P (AnnCall r n) (Call p) Q,A"

| SeqDynCom:
      "r ⊆ pre a ⟹
      ∀s∈r. Γ, Θ ⊩⇘/F⇙P a (c s) Q,A ⟹
      P⊆r
      ⟹ 
      Γ, Θ ⊩⇘/F⇙ P (AnnRec r a) (DynCom c) Q,A"

| SeqConseq: "⟦ P ⊆ P'; Γ,Θ⊩⇘/F⇙ P' a c Q',A'; Q' ⊆ Q; A' ⊆ A ⟧
           ⟹ Γ,Θ⊩⇘/F⇙ P a c Q,A"

| SeqParallel: "P ⊆ pre (AnnPar as) ⟹ Γ,Θ⊢⇘/F⇙ (AnnPar as) (Parallel cs) Q,A
  ⟹ Γ,Θ⊩⇘/F⇙ P (AnnPar as) (Parallel cs) Q,A"

lemmas oghoare_intros = "oghoare_oghoare_seq.intros"

lemmas oghoare_inducts = oghoare_oghoare_seq.inducts

lemmas oghoare_induct = oghoare_oghoare_seq.inducts(1)

lemmas oghoare_seq_induct = oghoare_oghoare_seq.inducts(2)

end