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