Theory DiskPaxos_Inv3

(*  Title:       Proving the Correctness of Disk Paxos

    Author:      Mauro J. Jaskelioff, Stephan Merz, 2005
    Maintainer:  Mauro J. Jaskelioff <mauro at fceia.unr.edu.ar>
*)

theory DiskPaxos_Inv3 imports DiskPaxos_Inv2  begin

subsection ‹Invariant 3›

text ‹
  This invariant says that if two processes have read each other's block 
  from disk $d$ during their current phases, then at least one of them 
  has read the other's current block.
›

definition HInv3_L :: "state ⇒ Proc ⇒ Proc ⇒ Disk ⇒ bool"
where
  "HInv3_L s p q d =  (phase s p ∈ {1,2}
                     ∧ phase s q ∈ {1,2}      
                     ∧ hasRead s p d q
                     ∧ hasRead s q d p)"

definition HInv3_R :: "state ⇒ Proc ⇒ Proc ⇒ Disk ⇒ bool"
where
  "HInv3_R s p q d =  (⦇block= dblock s q, proc= q⦈ ∈ blocksRead s p d
                     ∨ ⦇block= dblock s p, proc= p⦈ ∈ blocksRead s q d)"

definition HInv3_inner :: "state ⇒ Proc ⇒ Proc ⇒ Disk ⇒ bool"
  where "HInv3_inner s p q d = (HInv3_L s p q d ⟶ HInv3_R s p q d)"

definition HInv3 :: "state ⇒ bool"
  where "HInv3 s = (∀p q d. HInv3_inner s p q d)"

subsubsection‹Proofs of Invariant 3›

theorem HInit_HInv3: "HInit s ⟹ HInv3 s"
  by(simp add: HInit_def Init_def HInv3_def 
               HInv3_inner_def HInv3_L_def HInv3_R_def)

lemma InitPhase_HInv3_p: 
  "⟦ InitializePhase s s' p; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
  by(auto simp add: InitializePhase_def HInv3_inner_def 
                    hasRead_def HInv3_L_def HInv3_R_def)

lemma InitPhase_HInv3_q: 
  "⟦ InitializePhase s s' q ; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
  by(auto simp add: InitializePhase_def HInv3_inner_def 
                    hasRead_def HInv3_L_def HInv3_R_def)

lemma HInv3_L_sym: "HInv3_L s p q d ⟹ HInv3_L s q p d"
  by(auto simp add: HInv3_L_def)

lemma HInv3_R_sym: "HInv3_R s p q d ⟹ HInv3_R s q p d"
  by(auto simp add: HInv3_R_def)

lemma Phase1or2ReadThen_HInv3_pq: 
  assumes act:  "Phase1or2ReadThen s s' p d q"
  and  inv_L':  "HInv3_L s' p q d"
  and      pq:  "p≠q"
  and   inv2b:  "Inv2b s"
  shows   "HInv3_R s' p q d"
proof -
  from inv_L' act pq
  have "phase s q ∈ {1,2} ∧ hasRead s q d p"
    by(auto simp add: Phase1or2ReadThen_def HInv3_L_def 
            hasRead_def split: if_split_asm)
  with inv2b
  have "disk s d q = dblock s q"
    by(auto simp add: Inv2b_def Inv2b_inner_def 
             hasRead_def)
  with act
  show ?thesis
    by(auto simp add: Phase1or2ReadThen_def HInv3_def 
                       HInv3_inner_def HInv3_R_def)
qed

lemma Phase1or2ReadThen_HInv3_hasRead: 
  "⟦ ¬hasRead s pp dd qq; 
     Phase1or2ReadThen s s' p d q; 
     pp≠p ∨ qq≠q ∨ dd≠d⟧ 
  ⟹ ¬hasRead s' pp dd qq"
  by(auto simp add: hasRead_def Phase1or2ReadThen_def)

theorem HPhase1or2ReadThen_HInv3:
  assumes act:  "HPhase1or2ReadThen s s' p d q"
  and     inv:  "HInv3 s"
  and      pq:  "p≠q"
  and   inv2b:  "Inv2b s"
  shows   "HInv3 s'"
proof(clarsimp simp add: HInv3_def HInv3_inner_def)
  fix pp qq dd
  assume h3l': "HInv3_L s' pp qq dd"
  show  "HInv3_R s' pp qq dd"
  proof(cases "HInv3_L s pp qq dd")
    case True
    with inv
    have "HInv3_R s pp qq dd"
      by(auto simp add: HInv3_def HInv3_inner_def)
    with act h3l'
    show ?thesis
      by(auto simp add: HInv3_R_def HInv3_L_def 
                          Phase1or2ReadThen_def)
  next
    case False
    assume nh3l: "¬ HInv3_L s pp qq dd"
    show " HInv3_R s' pp qq dd"
    proof(cases "((pp=p ∧ qq=q) ∨ (pp=q ∧ qq=p)) ∧ dd=d")
      case True
      with act pq inv2b h3l' HInv3_L_sym[OF h3l']  
      show ?thesis
        by(auto dest: Phase1or2ReadThen_HInv3_pq HInv3_R_sym)
    next
      case False
      from nh3l h3l' act
      have "(¬hasRead s pp dd qq ∨ ¬hasRead s qq dd pp) 
            ∧ hasRead s' pp dd qq ∧ hasRead s' qq dd pp"
        by(auto simp add: HInv3_L_def Phase1or2ReadThen_def)
      with act False
      show ?thesis
        by(auto dest: Phase1or2ReadThen_HInv3_hasRead)
    qed
  qed
qed

lemma StartBallot_HInv3_p:   
  "⟦ StartBallot s s' p; HInv3_L s' p q d ⟧ 
          ⟹ HInv3_R s' p q d"
by(auto simp add: StartBallot_def dest: InitPhase_HInv3_p)

lemma StartBallot_HInv3_q:   
  "⟦ StartBallot s s' q; HInv3_L s' p q d ⟧
           ⟹ HInv3_R s' p q d"
  by(auto simp add: StartBallot_def dest: InitPhase_HInv3_q)

lemma StartBallot_HInv3_nL:   
  "⟦ StartBallot s s' t; ¬HInv3_L s p q d; t≠p; t≠ q ⟧ 
           ⟹ ¬HInv3_L s' p q d"
  by(auto simp add: StartBallot_def InitializePhase_def 
                      HInv3_L_def hasRead_def)

lemma StartBallot_HInv3_R:
  "⟦ StartBallot s s' t; HInv3_R s p q d; t≠p; t≠ q ⟧
              ⟹ HInv3_R s' p q d"
  by(auto simp add: StartBallot_def InitializePhase_def 
                    HInv3_R_def hasRead_def)

lemma StartBallot_HInv3_t:
  "⟦ StartBallot s s' t; HInv3_inner s p q d; t≠p; t≠ q ⟧
                ⟹ HInv3_inner s' p q d"
  by(auto simp add: HInv3_inner_def 
        dest: StartBallot_HInv3_nL StartBallot_HInv3_R)

lemma StartBallot_HInv3:
  assumes act: "StartBallot s s' t"
  and     inv: "HInv3_inner s p q d"
  shows        "HInv3_inner s' p q d"
proof(cases "t=p ∨ t=q")
  case True
  with act inv
  show ?thesis
    by(auto simp add: HInv3_inner_def 
         dest: StartBallot_HInv3_p StartBallot_HInv3_q)
next
  case False
  with inv act
  show ?thesis
    by(auto simp add: HInv3_inner_def dest: StartBallot_HInv3_t)
qed

theorem HStartBallot_HInv3:
  "⟦ HStartBallot s s' p; HInv3 s ⟧ ⟹ HInv3 s'"
  by(auto simp add: HInv3_def dest: StartBallot_HInv3)

theorem HPhase1or2ReadElse_HInv3:
  "⟦ HPhase1or2ReadElse s s' p d q; HInv3 s ⟧ ⟹ HInv3 s'"
  by(auto simp add: Phase1or2ReadElse_def HInv3_def 
              dest: StartBallot_HInv3)

theorem HPhase1or2Write_HInv3:
  assumes act: "HPhase1or2Write s s' p d"
  and inv: "HInv3 s"
  shows "HInv3 s'"
proof(auto simp add: HInv3_def)
  fix pp qq dd
  show " HInv3_inner s' pp qq dd"
  proof(cases "HInv3_L s pp qq dd")
    case True
    with inv
    have "HInv3_R s pp qq dd"
      by(simp add: HInv3_def HInv3_inner_def)
    with act
    show ?thesis
      by(auto simp add: HInv3_inner_def HInv3_R_def 
                      Phase1or2Write_def)
  next
    case False
    with act
    have "¬HInv3_L s' pp qq dd"
      by(auto simp add: HInv3_L_def hasRead_def Phase1or2Write_def)
    thus ?thesis
      by(simp add: HInv3_inner_def)
  qed
qed

lemma EndPhase1_HInv3_p:   
  "⟦ EndPhase1 s s' p; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
by(auto simp add: EndPhase1_def dest: InitPhase_HInv3_p)

lemma EndPhase1_HInv3_q:   
  "⟦ EndPhase1 s s' q; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
  by(auto simp add: EndPhase1_def dest: InitPhase_HInv3_q)

lemma EndPhase1_HInv3_nL:   
  "⟦ EndPhase1 s s' t; ¬HInv3_L s p q d; t≠p; t≠ q ⟧
                    ⟹ ¬HInv3_L s' p q d"
  by(auto simp add: EndPhase1_def InitializePhase_def 
                    HInv3_L_def hasRead_def)

lemma EndPhase1_HInv3_R:
  "⟦ EndPhase1 s s' t; HInv3_R s p q d; t≠p; t≠ q ⟧
                      ⟹ HInv3_R s' p q d"
  by(auto simp add: EndPhase1_def InitializePhase_def
                    HInv3_R_def hasRead_def)

lemma EndPhase1_HInv3_t:
  "⟦ EndPhase1 s s' t; HInv3_inner s p q d; t≠p; t≠ q ⟧
                ⟹ HInv3_inner s' p q d"
  by(auto simp add: HInv3_inner_def dest: EndPhase1_HInv3_nL 
                   EndPhase1_HInv3_R)

lemma EndPhase1_HInv3:
  assumes act: "EndPhase1 s s' t"
  and     inv: "HInv3_inner s p q d"
  shows        "HInv3_inner s' p q d"
proof(cases "t=p ∨ t=q")
  case True
  with act inv
  show ?thesis
    by(auto simp add: HInv3_inner_def 
                dest: EndPhase1_HInv3_p EndPhase1_HInv3_q)
next
  case False
  with inv act
  show ?thesis
    by(auto simp add: HInv3_inner_def dest: EndPhase1_HInv3_t)
qed

theorem HEndPhase1_HInv3:
  "⟦ HEndPhase1 s s' p; HInv3 s ⟧ ⟹ HInv3 s'"
  by(auto simp add: HInv3_def dest: EndPhase1_HInv3)

lemma EndPhase2_HInv3_p:   
  "⟦ EndPhase2 s s' p; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
by(auto simp add: EndPhase2_def dest: InitPhase_HInv3_p)

lemma EndPhase2_HInv3_q:   
  "⟦ EndPhase2 s s' q; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
  by(auto simp add: EndPhase2_def dest: InitPhase_HInv3_q)

lemma EndPhase2_HInv3_nL:   
  "⟦ EndPhase2 s s' t; ¬HInv3_L s p q d; t≠p; t≠ q ⟧
                     ⟹ ¬HInv3_L s' p q d"
  by(auto simp add: EndPhase2_def InitializePhase_def
                    HInv3_L_def hasRead_def)

lemma EndPhase2_HInv3_R:
  "⟦ EndPhase2 s s' t; HInv3_R s p q d; t≠p; t≠ q ⟧
                     ⟹ HInv3_R s' p q d"
  by(auto simp add: EndPhase2_def InitializePhase_def
                    HInv3_R_def hasRead_def)

lemma EndPhase2_HInv3_t:
  "⟦ EndPhase2 s s' t; HInv3_inner s p q d; t≠p; t≠ q ⟧
                    ⟹ HInv3_inner s' p q d"
  by(auto simp add: HInv3_inner_def 
              dest: EndPhase2_HInv3_nL EndPhase2_HInv3_R)

lemma EndPhase2_HInv3:
  assumes act: "EndPhase2 s s' t"
  and     inv: "HInv3_inner s p q d"
  shows        "HInv3_inner s' p q d"
proof(cases "t=p ∨ t=q")
  case True
  with act inv
  show ?thesis
    by(auto simp add: HInv3_inner_def 
                dest: EndPhase2_HInv3_p EndPhase2_HInv3_q)
next
  case False
  with inv act
  show ?thesis
    by(auto simp add: HInv3_inner_def dest: EndPhase2_HInv3_t)
qed

theorem HEndPhase2_HInv3:
  "⟦ HEndPhase2 s s' p; HInv3 s ⟧ ⟹ HInv3 s'"
  by(auto simp add: HInv3_def dest: EndPhase2_HInv3)

lemma Fail_HInv3_p:   
  "⟦ Fail s s' p; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
by(auto simp add: Fail_def dest: InitPhase_HInv3_p)

lemma Fail_HInv3_q:   
  "⟦ Fail s s' q; HInv3_L s' p q d ⟧ ⟹ HInv3_R s' p q d"
  by(auto simp add: Fail_def dest: InitPhase_HInv3_q)

lemma Fail_HInv3_nL:   
  "⟦ Fail s s' t; ¬HInv3_L s p q d; t≠p; t≠ q ⟧ 
             ⟹ ¬HInv3_L s' p q d"
  by(auto simp add: Fail_def InitializePhase_def
                    HInv3_L_def hasRead_def)

lemma Fail_HInv3_R:
  "⟦ Fail s s' t; HInv3_R s p q d; t≠p; t≠ q ⟧
             ⟹ HInv3_R s' p q d"
  by(auto simp add: Fail_def InitializePhase_def
                    HInv3_R_def hasRead_def)

lemma Fail_HInv3_t:
  "⟦ Fail s s' t; HInv3_inner s p q d; t≠p; t≠ q ⟧
              ⟹ HInv3_inner s' p q d"
  by(auto simp add: HInv3_inner_def 
              dest: Fail_HInv3_nL Fail_HInv3_R)

lemma Fail_HInv3:
  assumes act: "Fail s s' t"
  and     inv: "HInv3_inner s p q d"
  shows        "HInv3_inner s' p q d"
proof(cases "t=p ∨ t=q")
  case True
  with act inv
  show ?thesis
    by(auto simp add: HInv3_inner_def 
                dest: Fail_HInv3_p Fail_HInv3_q)
next
  case False
  with inv act
  show ?thesis
    by(auto simp add: HInv3_inner_def dest: Fail_HInv3_t)
qed

theorem HFail_HInv3:
  "⟦ HFail s s' p; HInv3 s ⟧ ⟹ HInv3 s'"
  by(auto simp add: HInv3_def dest: Fail_HInv3)

theorem HPhase0Read_HInv3:
  assumes act: "HPhase0Read s s' p d"
  and inv: "HInv3 s"
  shows "HInv3 s'"
proof(auto simp add: HInv3_def)
  fix pp qq dd
  show " HInv3_inner s' pp qq dd"
  proof(cases "HInv3_L s pp qq dd")
    case True
    with inv
    have "HInv3_R s pp qq dd"
      by(simp add: HInv3_def HInv3_inner_def)
    with act
    show ?thesis
      by(auto simp add: HInv3_inner_def HInv3_R_def Phase0Read_def)
  next
    case False
    with act
    have "¬HInv3_L s' pp qq dd"
      by(auto simp add: HInv3_L_def hasRead_def Phase0Read_def)
    thus ?thesis
      by(simp add: HInv3_inner_def)
  qed
qed

lemma EndPhase0_HInv3_p:   
  "⟦ EndPhase0 s s' p; HInv3_L s' p q d ⟧ 
              ⟹ HInv3_R s' p q d"
by(auto simp add: EndPhase0_def dest: InitPhase_HInv3_p)

lemma EndPhase0_HInv3_q:   
  "⟦ EndPhase0 s s' q; HInv3_L s' p q d ⟧
              ⟹ HInv3_R s' p q d"
  by(auto simp add: EndPhase0_def dest: InitPhase_HInv3_q)

lemma EndPhase0_HInv3_nL:   
  "⟦ EndPhase0 s s' t; ¬HInv3_L s p q d; t≠p; t≠ q ⟧
               ⟹ ¬HInv3_L s' p q d"
  by(auto simp add: EndPhase0_def InitializePhase_def 
                    HInv3_L_def hasRead_def)

lemma EndPhase0_HInv3_R:
  "⟦ EndPhase0 s s' t; HInv3_R s p q d; t≠p; t≠ q ⟧
                ⟹ HInv3_R s' p q d"
  by(auto simp add: EndPhase0_def InitializePhase_def 
                    HInv3_R_def hasRead_def)

lemma EndPhase0_HInv3_t:
  "⟦ EndPhase0 s s' t; HInv3_inner s p q d; t≠p; t≠ q ⟧
                 ⟹ HInv3_inner s' p q d"
  by(auto simp add: HInv3_inner_def 
              dest: EndPhase0_HInv3_nL EndPhase0_HInv3_R)

lemma EndPhase0_HInv3:
  assumes act: "EndPhase0 s s' t"
  and     inv: "HInv3_inner s p q d"
  shows        "HInv3_inner s' p q d"
proof(cases "t=p ∨ t=q")
  case True
  with act inv
  show ?thesis
    by(auto simp add: HInv3_inner_def 
                dest: EndPhase0_HInv3_p EndPhase0_HInv3_q)
next
  case False
  with inv act
  show ?thesis
    by(auto simp add: HInv3_inner_def dest: EndPhase0_HInv3_t)
qed

theorem HEndPhase0_HInv3:
  "⟦ HEndPhase0 s s' p; HInv3 s ⟧ ⟹ HInv3 s'"
  by(auto simp add: HInv3_def dest: EndPhase0_HInv3)

text‹$HInv1 \wedge HInv2 \wedge HInv3$ is an invariant of $HNext$.›

lemma I2c:
  assumes nxt: "HNext s s'"
  and inv: "HInv1 s ∧ HInv2 s ∧ HInv3 s"
  shows "HInv3 s'" using assms
  by(auto simp add: HNext_def Next_def,
     auto intro: HStartBallot_HInv3,
     auto intro: HPhase0Read_HInv3,
     auto intro: HPhase1or2Write_HInv3,
     auto simp add: Phase1or2Read_def HInv2_def
          intro: HPhase1or2ReadThen_HInv3
                 HPhase1or2ReadElse_HInv3,
     auto simp add: EndPhase1or2_def
          intro: HEndPhase1_HInv3
                 HEndPhase2_HInv3,
     auto intro: HFail_HInv3,
     auto intro: HEndPhase0_HInv3)

end