Consensus_Demo.thy

theory
  Consensus_Demo
imports
  Network
begin

datatype 'val msg
  = Propose 'val
  | Accept 'val

fun acceptor_step where
  ‹acceptor_step state (Receive sender (Propose val)) =
     (case state of
        None   ⇒ (Some val, {Send sender (Accept val)}) |
        Some v ⇒ (Some v,   {Send sender (Accept v)}))› |
  ‹acceptor_step state _ = (state, {})›

fun proposer_step where
  ‹proposer_step None (Request val) = (None, {Send 0 (Propose val)})› |
  ‹proposer_step None (Receive _ (Accept val)) = (Some val, {})› |
  ‹proposer_step state _ = (state, {})›

fun consensus_step where
  ‹consensus_step proc =
     (if proc = 0 then acceptor_step else proposer_step)›

(* Invariant 1: for any proposer p, if p's state is ``Some val'',
   then there exists a process that has sent a message
   ``Accept val'' to p. *)

definition inv1 where
  ‹inv1 msgs states ⟷
     (∀proc val. proc ≠ 0 ∧ states proc = Some val ⟶
                 (∃sender. (sender, Send proc (Accept val)) ∈ msgs))›

(* Invariant 2: if a message ``Accept val'' has been sent, then
   the acceptor is in the state ``Some val''. *)

definition inv2 where
  ‹inv2 msgs states ⟷
     (∀sender recpt val. (sender, Send recpt (Accept val)) ∈ msgs ⟶
                         states 0 = Some val)›

lemma invariant_propose:
  assumes ‹msgs' = msgs ∪ {(proc, Send 0 (Propose val))}›
    and ‹inv1 msgs states ∧ inv2 msgs states›
  shows ‹inv1 msgs' states ∧ inv2 msgs' states›
proof -
  have ‹∀sender proc val.
      (sender, Send proc (Accept val)) ∈ msgs' ⟷
      (sender, Send proc (Accept val)) ∈ msgs›
    using assms(1) by blast
  then show ?thesis
    by (meson assms(2) inv1_def inv2_def)
qed

lemma invariant_decide:
  assumes ‹states' = states (0 := Some val)›
    and ‹msgs' = msgs ∪ {(0, Send sender (Accept val))}›
    and ‹states 0 = None ∨ states 0 = Some val›
    and ‹inv1 msgs states ∧ inv2 msgs states›
  shows ‹inv1 msgs' states' ∧ inv2 msgs' states'›
proof -
  {
    fix p v
    assume asm: ‹p ≠ 0 ∧ states' p = Some v›
    hence ‹states p = Some v›
      by (simp add: asm assms(1))
    hence ‹∃sender. (sender, Send p (Accept v)) ∈ msgs›
      by (meson asm assms(4) inv1_def)
    hence ‹∃sender. (sender, Send p (Accept v)) ∈ msgs'›
      using assms(2) by blast
  }
  moreover {
    fix p1 p2 v
    assume asm: ‹(p1, Send p2 (Accept v)) ∈ msgs'›
    have ‹states' 0 = Some v›
    proof (cases ‹(p1, Send p2 (Accept v)) ∈ msgs›)
      case True
      then show ?thesis
        by (metis assms(1) assms(3) assms(4) fun_upd_same inv2_def option.distinct(1))
    next
      case False
      then show ?thesis
        using asm assms(1) assms(2) by auto
    qed
  }
  ultimately show ?thesis
    by (simp add: inv1_def inv2_def)
qed

lemma invariant_learn:
  assumes ‹states' = states (proc := Some val)›
    and ‹(sender, Send proc (Accept val)) ∈ msgs›
    and ‹inv1 msgs states ∧ inv2 msgs states›
  shows ‹inv1 msgs states' ∧ inv2 msgs states'›
proof -
  {
    fix p v
    assume asm: ‹p ≠ 0 ∧ states' p = Some v›
    have ‹∃sender. (sender, Send p (Accept v)) ∈ msgs›
    proof (cases ‹p = proc›)
      case True
      then show ?thesis
        using asm assms(1) assms(2) by auto
    next
      case False
      then show ?thesis
        by (metis asm assms(1) assms(3) fun_upd_apply inv1_def)
    qed
  }
  moreover {
    fix p1 p2 v
    assume ‹(p1, Send p2 (Accept v)) ∈ msgs›
    hence ‹states' 0 = Some v›
      by (metis assms fun_upd_apply inv2_def)
  }
  ultimately show ?thesis
    by (simp add: inv1_def inv2_def)
qed

lemma invariant_proposer:
  assumes ‹proposer_step (states proc) event = (new_state, sent)›
    and ‹msgs' = msgs ∪ ((λmsg. (proc, msg)) ` sent)›
    and ‹states' = states (proc := new_state)›
    and ‹execute consensus_step (λp. None) UNIV (events @ [(proc, event)]) msgs' states'›
    and ‹inv1 msgs states ∧ inv2 msgs states›
  shows ‹inv1 msgs' states' ∧ inv2 msgs' states'›
proof (cases event)
  case (Receive sender msg)
  then show ?thesis
  proof (cases msg)
    case (Propose val)
    then show ?thesis
      using Receive assms by auto
  next
    case (Accept val) (* proposer receives Accept message: learn the decided value *)
    then show ?thesis
    proof (cases ‹states proc›)
      case None
      hence ‹states' = states (proc := Some val) ∧ msgs' = msgs›
        using Accept Receive assms(1) assms(2) assms(3) by auto
      then show ?thesis
        by (metis Accept Receive assms(4) assms(5) execute_receive invariant_learn)
    next
      case (Some v)
      then show ?thesis
        using assms by auto
    qed
  qed
next
  (* on a Request event, proposer sends a Propose message if its state
     is None, or ignores the event if already learnt a decision *)
  case (Request val)
  then show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
  proof (cases ‹states proc›)
    case None
    hence ‹states' = states ∧ msgs' = msgs ∪ {(proc, Send 0 (Propose val))}›
      using Request assms(1) assms(2) assms(3) by auto
    then show ?thesis
      by (simp add: assms(5) invariant_propose)
  next
    case (Some v)
    then show ?thesis using assms by auto
  qed
next
  case Timeout
  then show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
    using assms by auto
qed

lemma invariant_acceptor:
  assumes ‹acceptor_step (states 0) event = (new_state, sent)›
    and ‹msgs' = msgs ∪ ((λmsg. (0, msg)) ` sent)›
    and ‹states' = states (0 := new_state)›
    and ‹execute consensus_step (λp. None) UNIV (events @ [(0, event)]) msgs' states'›
    and ‹inv1 msgs states ∧ inv2 msgs states›
  shows ‹inv1 msgs' states' ∧ inv2 msgs' states'›
proof (cases event)
  case (Receive sender msg)
  then show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
  proof (cases msg)
    case (Propose val)
    then show ?thesis
    proof (cases ‹states 0›)
      case None (* not decided yet: decide now *)
      hence ‹states' = states (0 := Some val) ∧
             msgs' = msgs ∪ {(0, Send sender (Accept val))}›
        using Receive Propose assms(1) assms(2) assms(3) by auto
        (* for some reason sledgehammer couldn't find the line above *)
      then show ?thesis
        by (simp add: None assms(5) invariant_decide)
    next
      case (Some val') (* already decided previously *)
      hence ‹states' = states ∧
             msgs' = msgs ∪ {(0, Send sender (Accept val'))}›
        using Receive Propose assms(1) assms(2) assms(3) by auto
        (* for some reason sledgehammer couldn't find the line above *)
      then show ?thesis
        by (metis Some assms(3) assms(5) fun_upd_same invariant_decide)
    qed
  next
    case (Accept val)
    then show ?thesis
      using Receive assms by auto
  qed
next
  case (Request val)
  then show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
    using assms by auto
next
  case Timeout
  then show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
    using assms by auto
qed

lemma invariants:
  assumes ‹execute consensus_step (λx. None) UNIV events msgs' states'›
  shows ‹inv1 msgs' states' ∧ inv2 msgs' states'›
using assms proof(induction events arbitrary: msgs' states' rule: List.rev_induct)
  case Nil
  from this show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
    using execute_init inv1_def inv2_def by fastforce
next
  case (snoc x events)
  obtain proc event where ‹x = (proc, event)›
    by fastforce
  hence exec: ‹execute consensus_step (λp. None) UNIV
               (events @ [(proc, event)]) msgs' states'›
    using snoc.prems by blast
  from this obtain msgs states sent new_state
    where step_rel1: ‹execute consensus_step (λx. None) UNIV events msgs states›
      and step_rel2: ‹consensus_step proc (states proc) event = (new_state, sent)›
      and step_rel3: ‹msgs' = msgs ∪ ((λmsg. (proc, msg)) ` sent)›
      and step_rel4: ‹states' = states (proc := new_state)›
    by auto
  have inv_before: ‹inv1 msgs states ∧ inv2 msgs states›
    using snoc.IH step_rel1 by fastforce
  then show ‹inv1 msgs' states' ∧ inv2 msgs' states'›
  proof (cases ‹proc = 0›)
    case True
    then show ?thesis
      by (metis consensus_step.simps exec inv_before invariant_acceptor
          step_rel2 step_rel3 step_rel4)
  next
    case False
    then show ?thesis
      by (metis consensus_step.simps exec inv_before invariant_proposer
          step_rel2 step_rel3 step_rel4)
  qed
qed

theorem agreement:
  assumes ‹execute consensus_step (λx. None) UNIV events msgs states›
    and ‹states proc1 = Some val1› and ‹states proc2 = Some val2›
  shows ‹val1 = val2›
proof -
  have ‹states 0 = Some val1›
    by (metis assms(1) assms(2) inv1_def inv2_def invariants)
  moreover have ‹states 0 = Some val2›
    by (metis assms(1) assms(3) inv1_def inv2_def invariants)
  ultimately show ‹val1 = val2›
    by simp
qed

end

Network.thy

section ‹Network model›

text ‹We define a simple model of a distributed system. The system consists of
a set of processes, each of which has a unique identifier and local state that
it can update. There is no shared state between processes; processes can
communicate only by sending messages to each other. The communication is
\emph{asynchronous} -- that is, messages may be delayed arbitrarily,
reordered, duplicated, or dropped entirely.

In reality, processes execute concurrently, possibly at different speeds (in
particular, a process may fail by stopping execution entirely). To model this,
we say that the system as a whole makes progress by one of the processes
performing an execution step, and processes may perform steps in any order.

An execution step involves a process handling an \emph{event}. An event could
be one of several things: a request from a user, receiving a message from
another process, or the elapsing of a timeout. In response to such an event,
a process can update its local state, and/or send messages to other processes.›

theory
  Network
imports
  Main
begin


text ‹A message is always sent to a particular recipient. This datatype
encapsulates the name of the recipient process and the message being sent.›

datatype ('proc, 'msg) send
  = Send (msg_recipient: 'proc) (send_msg: 'msg)


text ‹An event that a process may handle: receiving a message from another
process, or a request from a user, or an elapsed timeout.›

datatype ('proc, 'msg, 'val) event
  = Receive (msg_sender: 'proc) (recv_msg: 'msg)
  | Request 'val
  | Timeout


text ‹A step function takes three arguments: the name of the process that is
executing, its current local state, and the event being handled. It returns two
things: the new local state, and a set of messages to send to other processes.›

type_synonym ('proc, 'state, 'msg, 'val) step_func =
  ‹'proc ⇒ 'state ⇒ ('proc, 'msg, 'val) event ⇒ ('state × ('proc, 'msg) send set)›


text ‹A process may only receive a message from a given sender if that sender
process did previously send that message. Request and Timeout events can occur
at any time.›

fun valid_event :: ‹('proc, 'msg, 'val) event ⇒ 'proc ⇒
                    ('proc × ('proc, 'msg) send) set ⇒ bool› where
  ‹valid_event (Receive sender msg) proc msgs = ((sender, Send proc msg) ∈ msgs)› |
  ‹valid_event (Request _) _ _ = True› |
  ‹valid_event Timeout _ _ = True›


text ‹A valid execution of a distributed algorithm is a sequence of execution
steps. At each step, any of the processes handles any valid event. We call the
step function to compute the next state for that process, and any messages it
sends are added to a global set of all messages ever sent.›

inductive execute ::
    ‹('proc, 'state, 'msg, 'val) step_func ⇒ ('proc ⇒ 'state) ⇒ 'proc set ⇒
     ('proc × ('proc, 'msg, 'val) event) list ⇒
     ('proc × ('proc, 'msg) send) set ⇒ ('proc ⇒ 'state) ⇒ bool› where
  ‹execute step init procs [] {} init› |
  ‹⟦execute step init procs events msgs states;
    proc ∈ procs;
    valid_event event proc msgs;
    step proc (states proc) event = (new_state, sent);
    events' = events @ [(proc, event)];
    msgs' = msgs ∪ ((λmsg. (proc, msg)) ` sent);
    states' = states (proc := new_state)
   ⟧ ⟹ execute step init procs events' msgs' states'›


subsection ‹Lemmas for the network model›

text ‹We prove a few lemmas that are useful when working with the above network model.›

inductive_cases execute_indcases: ‹execute step init procs events msg states›

lemma execute_init:
  assumes ‹execute step init procs [] msgs states›
  shows ‹msgs = {} ∧ states = init›
  using assms by(auto elim: execute.cases)

inductive_cases execute_snocE [elim!]:
  ‹execute step init procs (events @ [(proc, event)]) msgs' states'›

lemma execute_step:
  assumes ‹execute step init procs (events @ [(proc, event)]) msgs' states'›
  shows ‹∃msgs states sent new_state.
          execute step init procs events msgs states ∧
          proc ∈ procs ∧
          valid_event event proc msgs ∧
          step proc (states proc) event = (new_state, sent) ∧
          msgs' = msgs ∪ ((λmsg. (proc, msg)) ` sent) ∧
          states' = states (proc := new_state)›
  using assms by auto

lemma execute_receive:
  assumes ‹execute step init procs (events @ [(recpt, Receive sender msg)]) msgs' states'›
  shows ‹(sender, Send recpt msg) ∈ msgs'›
  using assms execute_step by fastforce

end

Only_Fives.thy

theory
  Only_Fives
imports
  Main
begin

inductive only_fives :: ‹nat list ⇒ bool› where
  ‹only_fives []› |
  ‹⟦only_fives xs⟧ ⟹ only_fives (xs @ [5])›

theorem only_fives_concat:
  assumes ‹only_fives xs› and ‹only_fives ys›
  shows ‹only_fives (xs @ ys)›
using assms proof (induction ys rule: List.rev_induct)
  case Nil
  then show ‹only_fives (xs @ [])›
    by auto
next
  case (snoc y ys)
  hence ‹only_fives ys›
    using only_fives.simps by blast
  hence ‹only_fives (xs @ ys)›
    by (simp add: snoc.IH snoc.prems(1))
  moreover have ‹y = 5›
    using only_fives.cases snoc.prems(2) by auto
  ultimately show ‹only_fives (xs @ ys @ [y])›
    using only_fives.intros(2) by force
qed

end