Theory DiskPaxos_Model

(*  Title:       Proving the Correctness of Disk Paxos

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

section "Disk Paxos Algorithm Specification"

theory DiskPaxos_Model imports Main begin

text‹This is the specification of the Disk Synod algorithm.›

typedecl InputsOrNi
typedecl Disk
typedecl Proc

axiomatization
  Inputs :: "InputsOrNi set" and
  NotAnInput :: "InputsOrNi" and
  Ballot :: "Proc ⇒ nat set" and
  IsMajority :: "Disk set ⇒ bool"
where
  NotAnInput: "NotAnInput ∉ Inputs" and
  InputsOrNi: "(UNIV :: InputsOrNi set) = Inputs ∪ {NotAnInput}" and
  Ballot_nzero: "∀p. 0 ∉ Ballot p" and
  Ballot_disj: "∀p q. p ≠ q ⟶ (Ballot p) ∩ (Ballot q) = {}" and
  Disk_isMajority: "IsMajority(UNIV)" and
  majorities_intersect: 
    "∀S T. IsMajority(S) ∧ IsMajority(T) ⟶ S ∩ T ≠ {}"

lemma ballots_not_zero [simp]:
  "b ∈ Ballot p ⟹ 0 < b"
proof (rule ccontr)
  assume b: "b ∈ Ballot p"
  and contr: "¬ (0 < b)"
  from Ballot_nzero
  have "0 ∉ Ballot p" ..
  with b contr 
  show "False"
    by auto
qed

lemma majority_nonempty [simp]: "IsMajority(S) ⟹ S ≠ {}"
proof(auto)
  from majorities_intersect
  have "IsMajority({}) ∧ IsMajority({}) ⟶ {} ∩ {} ≠ {}"
    by auto
  thus "IsMajority {} ⟹ False"
    by auto
qed

definition AllBallots :: "nat set"
  where "AllBallots = (UN p. Ballot p)"

record
  DiskBlock = 
    mbal:: nat
    bal :: nat
    inp :: InputsOrNi

definition InitDB :: DiskBlock
  where "InitDB = ⦇ mbal = 0, bal = 0, inp = NotAnInput ⦈"

record
  BlockProc =
    block :: DiskBlock
    proc  :: Proc
 
record 
  state =
    inpt :: "Proc ⇒ InputsOrNi"
    outpt :: "Proc ⇒ InputsOrNi"
    disk :: "Disk ⇒ Proc ⇒ DiskBlock"
    dblock :: "Proc ⇒ DiskBlock"
    phase :: "Proc ⇒ nat"
    disksWritten :: "Proc ⇒ Disk set"
    blocksRead :: "Proc ⇒ Disk ⇒ BlockProc set"
  (* History Variables *) 
    allInput  :: "InputsOrNi set"
    chosen    :: "InputsOrNi"


definition hasRead :: "state ⇒ Proc ⇒ Disk ⇒ Proc ⇒ bool"
  where "hasRead s p d q = (∃ br ∈ blocksRead s p d. proc br = q)"

definition allRdBlks :: "state ⇒ Proc ⇒ BlockProc set"
  where "allRdBlks s p = (UN d. blocksRead s p d)"

definition allBlocksRead :: "state ⇒ Proc ⇒ DiskBlock set"
  where "allBlocksRead s p = block ` (allRdBlks s p)"

definition Init :: "state ⇒ bool"
  where
    "Init s =
      (range (inpt s) ⊆ Inputs
     & outpt s = (λp. NotAnInput)
     & disk s = (λd p. InitDB)
     & phase s = (λp. 0)
     & dblock s = (λp. InitDB)
     & disksWritten s = (λp. {})
     & blocksRead s = (λp d. {}))"

definition InitializePhase :: "state ⇒ state ⇒ Proc ⇒ bool"
  where
  "InitializePhase s s' p =
    (disksWritten s' = (disksWritten s)(p := {})
   & blocksRead s' = (blocksRead s)(p := (λd. {})))"

definition StartBallot :: "state ⇒ state ⇒ Proc ⇒ bool"
where
  "StartBallot s s' p =
    (phase s p ∈ {1,2}
   & phase s' = (phase s)(p := 1)
   & (∃b ∈ Ballot p. 
         mbal (dblock s p) < b
       & dblock s' = (dblock s)(p := (dblock s p)⦇ mbal := b ⦈))
   & InitializePhase s s' p
   & inpt s' = inpt s & outpt s' = outpt s & disk s' = disk s)"

definition Phase1or2Write :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ bool"
where
  "Phase1or2Write s s' p d =
    (phase s p ∈ {1, 2}
   ∧ disk s' = (disk s) (d := (disk s d) (p := dblock s p)) 
   ∧ disksWritten s' = (disksWritten s) (p:= (disksWritten s p) ∪ {d})
   ∧ inpt s' = inpt s ∧ outpt s'= outpt s
   ∧ phase s' = phase s ∧ dblock s' = dblock s
   ∧ blocksRead s'= blocksRead s)"

definition Phase1or2ReadThen :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ Proc ⇒ bool"
where
  "Phase1or2ReadThen s s' p d q =
    (d ∈ disksWritten s p
   & mbal(disk s d q) < mbal(dblock s p)
   & blocksRead s' = (blocksRead s)(p := (blocksRead s p)(d :=
                       (blocksRead s p d) ∪ {⦇ block = disk s d q,
                                               proc = q ⦈}))
   & inpt s' = inpt s & outpt s' = outpt s
   & disk s' = disk s & phase s' = phase s
   & dblock s' = dblock s & disksWritten s' = disksWritten s)"

definition Phase1or2ReadElse :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ Proc ⇒ bool"
where
  "Phase1or2ReadElse s s' p d q =
    (d ∈ disksWritten s p
   ∧ StartBallot s s' p)"

definition Phase1or2Read :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ Proc ⇒ bool"
where
  "Phase1or2Read s s' p d q =
     (Phase1or2ReadThen s s' p d q
    ∨ Phase1or2ReadElse s s' p d q)"

definition blocksSeen :: "state ⇒ Proc ⇒ DiskBlock set"
  where "blocksSeen s p = allBlocksRead s p ∪ {dblock s p}"

definition nonInitBlks :: "state ⇒ Proc ⇒ DiskBlock set"
  where"nonInitBlks s p = {bs . bs ∈ blocksSeen s p ∧ inp bs ∈ Inputs}"

definition maxBlk :: "state ⇒ Proc ⇒ DiskBlock"
where
  "maxBlk s p =
     (SOME b. b ∈ nonInitBlks s p ∧ (∀c ∈ nonInitBlks s p. bal c ≤ bal b))"

definition EndPhase1 :: "state ⇒ state ⇒ Proc ⇒ bool"
where
  "EndPhase1 s s' p =
    (IsMajority {d . d ∈ disksWritten s p
                     ∧ (∀q ∈ UNIV - {p}. hasRead s p d q)}
   ∧ phase s p = 1
   ∧ dblock s' = (dblock s) (p := dblock s p 
           ⦇ bal := mbal(dblock s p),
             inp := 
              (if nonInitBlks s p = {}
               then inpt s p
               else inp (maxBlk s p))
           ⦈ )
   ∧ outpt s' = outpt s
   ∧ phase s' = (phase s) (p := phase s p + 1)
   ∧ InitializePhase s s' p
   ∧ inpt s' = inpt s ∧ disk s' = disk s)"

definition EndPhase2 :: "state ⇒ state ⇒ Proc ⇒ bool"
where
  "EndPhase2 s s' p =
    (IsMajority {d . d ∈ disksWritten s p
                     ∧ (∀q ∈ UNIV - {p}. hasRead s p d q)}
   ∧ phase s p = 2
   ∧ outpt s' = (outpt s) (p:= inp (dblock s p))
   ∧ dblock s' = dblock s
   ∧ phase s' = (phase s) (p := phase s p + 1)
   ∧ InitializePhase s s' p
   ∧ inpt s' = inpt s ∧ disk s' = disk s)"

definition EndPhase1or2 :: "state ⇒ state ⇒ Proc ⇒ bool"
  where "EndPhase1or2 s s' p = (EndPhase1 s s' p ∨ EndPhase2 s s' p)"

definition Fail :: "state ⇒ state ⇒ Proc ⇒ bool"
where
  "Fail s s' p =
    (∃ip ∈ Inputs. inpt s' = (inpt s) (p := ip)
   ∧ phase s' = (phase s) (p := 0)
   ∧ dblock s'= (dblock s) (p := InitDB)
   ∧ outpt s' = (outpt s) (p := NotAnInput)
   ∧ InitializePhase s s' p
   ∧ disk s'= disk s)"

definition Phase0Read :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ bool"
where
  "Phase0Read s s' p d =
    (phase s p = 0
   ∧ blocksRead s' = (blocksRead s) (p := (blocksRead s p) (d := blocksRead s p d ∪ {⦇ block = disk s d p, proc = p ⦈}))
   ∧ inpt s' = inpt s & outpt s' = outpt s
   ∧ disk s' = disk s & phase s' = phase s
   ∧ dblock s' = dblock s & disksWritten s' = disksWritten s)"

definition EndPhase0 :: "state ⇒ state ⇒ Proc ⇒ bool"
where
  "EndPhase0 s s' p =
    (phase s p = 0
   ∧ IsMajority ({d. hasRead s p d p})
   ∧ (∃b ∈ Ballot p.   
       (∀r ∈ allBlocksRead s p. mbal r < b)
     ∧ dblock s' = (dblock s) ( p:= 
                    (SOME r.   r ∈ allBlocksRead s p 
                            ∧ (∀s ∈ allBlocksRead s p. bal s ≤  bal r)) ⦇ mbal := b ⦈ ))
   ∧ InitializePhase s s' p
   ∧ phase s' = (phase s) (p:= 1)
   ∧ inpt s' = inpt s ∧ outpt s' = outpt s ∧ disk s' = disk s)"

definition Next :: "state ⇒ state ⇒ bool"
where
  "Next s s' = (∃p.
                  StartBallot s s' p
                ∨ (∃d.   Phase0Read s s' p d
                       ∨ Phase1or2Write s s' p d
                       ∨ (∃q. q ≠ p ∧ Phase1or2Read s s' p d q))
                ∨ EndPhase1or2 s s' p
                ∨ Fail s s' p
                ∨ EndPhase0 s s' p)"

text ‹
  In the following, for each action or state {\em name} we name
  {\em Hname} the corresponding action that includes 
  the history part of the HNext action or state predicate that includes 
  history variables.
›

definition HInit :: "state ⇒ bool"
where
  "HInit s =
    (Init s
   & chosen s = NotAnInput
   & allInput s = range (inpt s))"

text ‹HNextPart is the part of the Next action 
        that is concerned with history variables.
›

definition HNextPart :: "state ⇒ state => bool"
where
  "HNextPart s s' =
    (chosen s' = 
       (if chosen s ≠ NotAnInput ∨ (∀p. outpt s' p = NotAnInput )
            then chosen s
            else outpt s' (SOME p. outpt s' p ≠ NotAnInput))
   ∧ allInput s' = allInput s ∪ (range (inpt s')))"

definition HNext :: "state ⇒ state ⇒ bool"
where
  "HNext s s' =
     (Next s s'
   ∧ HNextPart s s')"

text ‹
  We add HNextPart to every action (rather than proving that Next 
  maintains the HInv invariant) to make proofs easier. 
›

definition
  HPhase1or2ReadThen :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ Proc ⇒ bool" where
  "HPhase1or2ReadThen s s' p d q = (Phase1or2ReadThen s s' p d q ∧ HNextPart s s')" 

definition
  HEndPhase1 :: "state ⇒ state ⇒ Proc ⇒ bool" where
  "HEndPhase1 s s' p = (EndPhase1 s s' p ∧ HNextPart s s')" 

definition
  HStartBallot :: "state ⇒ state ⇒ Proc ⇒ bool" where
  "HStartBallot s s' p = (StartBallot s s' p ∧ HNextPart s s')"

definition
  HPhase1or2Write :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ bool" where
  "HPhase1or2Write s s' p d = (Phase1or2Write s s' p d ∧ HNextPart s s')" 

definition
  HPhase1or2ReadElse :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ Proc ⇒ bool" where
  "HPhase1or2ReadElse s s' p d q = (Phase1or2ReadElse s s' p d q ∧ HNextPart s s')" 

definition
  HEndPhase2 :: "state ⇒ state ⇒ Proc ⇒ bool" where
  "HEndPhase2 s s' p = (EndPhase2 s s' p ∧ HNextPart s s')"

definition
  HFail :: "state ⇒ state ⇒ Proc ⇒ bool" where
  "HFail s s' p = (Fail s s' p  ∧ HNextPart s s')"

definition
  HPhase0Read :: "state ⇒ state ⇒ Proc ⇒ Disk ⇒ bool" where
  "HPhase0Read s s' p d = (Phase0Read s s' p d ∧ HNextPart s s')"

definition
  HEndPhase0 :: "state ⇒ state ⇒ Proc ⇒ bool" where
  "HEndPhase0 s s' p = (EndPhase0 s s' p ∧ HNextPart s s')"  

text ‹
  Since these definitions are the conjunction of two other definitions 
  declaring them as simplification rules should be harmless.
›

declare HPhase1or2ReadThen_def [simp]
declare HPhase1or2ReadElse_def [simp]
declare HEndPhase1_def  [simp]
declare HStartBallot_def  [simp]
declare HPhase1or2Write_def [simp]
declare HEndPhase2_def [simp]
declare HFail_def [simp]
declare HPhase0Read_def [simp]
declare HEndPhase0_def [simp]

end