Skip to content

Instantly share code, notes, and snippets.

@ret
Forked from ept/Consensus_Demo.thy
Created September 15, 2019 01:49
Show Gist options
  • Save ret/d9d508e04d99b3f670a5b5c02802e576 to your computer and use it in GitHub Desktop.
Save ret/d9d508e04d99b3f670a5b5c02802e576 to your computer and use it in GitHub Desktop.
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
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
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment