Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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. proc0states 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:
assumesmsgs' = msgs{(proc, Send 0 (Propose val))}
andinv1 msgs statesinv2 msgs states
showsinv1 msgs' statesinv2 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:
assumesstates' = states (0 := Some val)
andmsgs' = msgs{(0, Send sender (Accept val))}
andstates 0 = Nonestates 0 = Some val
andinv1 msgs statesinv2 msgs states
showsinv1 msgs' states'inv2 msgs' states'
proof -
{
fix p v
assume asm:p0states' p = Some v
hencestates 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'
havestates' 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:
assumesstates' = states (proc := Some val)
and(sender, Send proc (Accept val))msgs
andinv1 msgs statesinv2 msgs states
showsinv1 msgs states'inv2 msgs states'
proof -
{
fix p v
assume asm:p0states' p = Some v
have ‹∃sender. (sender, Send p (Accept v))msgs
proof (casesp = 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
hencestates' 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:
assumesproposer_step (states proc) event = (new_state, sent)
andmsgs' = 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)
andstates' = states (0 := new_state)
andexecute consensus_step (λp. None) UNIV (events @ [(0, event)]) msgs' states'
andinv1 msgs statesinv2 msgs states
showsinv1 msgs' states'inv2 msgs' states'
proof (cases event)
case (Receive sender msg)
then showinv1 msgs' states'inv2 msgs' states'
proof (cases msg)
case (Propose val)
then show ?thesis
proof (casesstates 0)
case None (* not decided yet: decide now *)
hencestates' = 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 *)
hencestates' = 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 showinv1 msgs' states'inv2 msgs' states'
using assms by auto
next
case Timeout
then showinv1 msgs' states'inv2 msgs' states'
using assms by auto
qed
lemma invariants:
assumesexecute consensus_step (λx. None) UNIV events msgs' states'
showsinv1 msgs' states'inv2 msgs' states'
using assms proof(induction events arbitrary: msgs' states' rule: List.rev_induct)
case Nil
from this showinv1 msgs' states'inv2 msgs' states'
using execute_init inv1_def inv2_def by fastforce
next
case (snoc x events)
obtain proc event wherex = (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
sectionNetwork model
textWe 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
textA 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)
textAn 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
textA 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)
textA 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) setboolwhere
valid_event (Receive sender msg) proc msgs = ((sender, Send proc msg)msgs)|
valid_event (Request _) _ _ = True|
valid_event Timeout _ _ = True
textA 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)boolwhere
execute step init procs [] {} init|
‹⟦execute step init procs events msgs states;
procprocs;
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:
assumesexecute 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 listboolwhere
only_fives []|
‹⟦only_fives xs⟧ ⟹ only_fives (xs @ [5])
theorem only_fives_concat:
assumesonly_fives xsandonly_fives ys
showsonly_fives (xs @ ys)
using assms proof (induction ys rule: List.rev_induct)
case Nil
then showonly_fives (xs @ [])
by auto
next
case (snoc y ys)
henceonly_fives ys
using only_fives.simps by blast
henceonly_fives (xs @ ys)
by (simp add: snoc.IH snoc.prems(1))
moreover havey = 5
using only_fives.cases snoc.prems(2) by auto
ultimately showonly_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
You can’t perform that action at this time.