Instantly share code, notes, and snippets.

# ept/Consensus_Demo.thy

Last active May 20, 2024 03:03
Show Gist options
• Save ept/b6872fc541a68a321a26198b53b3896b to your computer and use it in GitHub Desktop.

# Correctness proofs of distributed systems with Isabelle

This Gist accompanies a Talk by Martin Kleppmann:

## Abstract

Testing systems is great, but tests can only explore a finite set of inputs and behaviors. Many real systems, especially distributed systems, have a potentially infinite state space. If you want to be sure that a program does the right thing in all possible situations, testing is not sufficient: you need proof. Only mathematical proof, e.g. by induction, can cover an infinite state space.

Pen-and-paper proofs are well established in mathematics, but they need to be laboriously checked by hand, and humans sometimes make mistakes. Automated theorem provers and computerized proof assistants can help here. This talk introduces Isabelle/HOL, an interactive proof assistant that can be used to formally prove the correctness of algorithms. It is somewhat like a programming language and REPL for proofs.

In this talk we will explore how Isabelle can be used to analyze algorithms for distributed systems, and prove them correct. We will work through some example problems in live demos, and prove real theorems about some simple algorithms. Proof assistants still have a pretty steep learning curve, and this talk won’t be able to teach you everything, but you will get a sense of the style of reasoning, and maybe you will be tempted to try it for yourself.

This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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 simp next case (snoc y ys) hence \only_fives ys\ using only_fives.cases by auto 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 blast ultimately show \only_fives (xs @ ys @ [y])\ using only_fives.intros(2) by fastforce qed end