Implementing a Quorum
The broadcast had no state and made no choices of its own. The quorum has both. A coordinator sends every request to a cluster of participants. Each participant votes yes or no and sends its vote back. The coordinator collects the votes tick by tick, and decides a request once minYes yes votes for it have arrived, deciding each request only once. In Rust this is a broadcast, a map, a second broadcast back, and a sliced! block with two use::state_null streams and a use::batch. The Lean program has the same lines.
On this page, you will write only the program. Proving the Quorum states its contract and proves it.
You will learn
- How to write a
tickblock with persisted state, the Lean form ofsliced! - Why
use::batchtakes a decision argument and the commutative count does not - How the census checks a program's nondeterminism
The program as written here is hydro_lean/Examples/TutorialSteps/QuorumProgram.lean. That directory holds every stage of the tutorial, each a file that compiles, so you can open one and see the goals and warnings the tutorial shows. The finished program, with its proofs, is hydro_lean/Examples/Tutorials/Quorum.lean.
Records
The program has three runtime choices, which become arguments collected in two records:
/-- The program's one `nondet!`: where the coordinator's batches of votes end. -/
structure QuorumDec (H : HydroSem L mem) (nCoord : Nat) where
votes : H.BatchDec nCoord (Nat × Bool) .noOrder .exactlyOnce
/-- The program's two network edges: `Unit` at `Values`, delivery cursors on the machine. -/
structure QuorumSched (H : HydroSem L mem) (nCoord nPart : Nat) where
toParticipants : H.TransportDec nPart nCoord
toCoordinator : H.TransportDec nCoord nPart
QuorumDec holds the program's decisions, one per nondet! site. Here there is one: where the coordinator's batches of votes end. The contract holds for every value of this record, so it holds however the votes are batched. QuorumSched holds the delivery timing of the two network edges, like HelloSched in Hello World. It is Unit at Values.
The Signature
Besides the two locations, the program takes the quorum size, each participant's voting rule, the request stream and the two records:
hydro def vote_quorum (H : HydroSem L mem) (coord part : L) (minYes : Nat)
(vote : Fin (mem part) → Nat → Bool)
(requests : H.Stream coord Nat .noOrder .exactlyOnce)
(dec : QuorumDec H (mem coord)) (sched : QuorumSched H (mem coord) (mem part)) :
H.Stream coord Nat .noOrder .exactlyOnce :=
vote j p is participant j's vote on request p. A participant's local logic is an ordinary Lean function passed in as an argument, so every theorem about the program holds for every voting rule. The output is the stream of decided requests at the coordinator.
The Network
The body begins with the two network hops:
-- the coordinator broadcasts every request to every participant
let p_requests := H.values (H.broadcast_closed sched.toParticipants requests)
-- each participant votes on each request it receives
let p_votes := H.map p_requests (fun j p => (p, vote j p))
-- the votes travel back to the coordinator
let c_votes := H.values (H.broadcast_closed sched.toCoordinator p_votes)
In Rust these are requests.broadcast(&participants, …).values(), a map, and the same back to the coordinator. The closure that H.map takes also receives the member index j, so each participant can tag a request with its own vote.
The Tick Block
The coordinator's sliced! block becomes a tick block. Its header declares the state and the batched input, as the Rust use:: lines do:
tick (state seen : H.BoundedStream (Nat × Bool) .noOrder .exactlyOnce)
(state decided : H.BoundedStream Nat .noOrder .exactlyOnce)
(input incoming := H.batch c_votes dec.votes) :=
(state seen : H.BoundedStream …)is a persisted stream, Rust'suse::state_null::<Stream<…>>(). It starts empty and holds every vote consumed so far.decidedholds every request already decided.(input incoming := H.batch c_votes dec.votes)isuse::batch(&c_votes, nondet!(…)). Where a batch ends depends on arrival timing, soH.batchtakes the decisiondec.votesas an argument. AtValuesa batch decision is a list of cuts, one per tick, and any list is allowed: a cut that asks for a vote that has not arrived ends the run at that tick (Total Decision Spaces).
The body runs once per tick:
let all := H.bchain seen incoming
let yes := H.bkfold yesStep 0 (fun _ _ => True) (fun s x y _ => yesStep_comm s x y)
(H.binto_keyed all)
let reached := H.bksKeys (H.bksFilter yes (fun n => decide (minYes ≤ n)))
let fresh := H.bfilterNotIn reached decided
rebind (seen := all, decided := H.bchain decided fresh)
yield (decisions := fresh);
allis the votes seen so far with this tick's batch appended (chain).yescounts the yes votes per request:binto_keyedgroups the votes by request, andbkfoldfolds each group withyesStep.reachedis the requests whose count is at leastminYes, andfreshis those not already indecided.rebindgives the next tick's state, andyieldemitsfreshas this tick's decisions. The;ends the block.
The count runs over an unordered batch, so, as in Rust, it needs no nondet! as long as the fold is commutative. Rust states the claim as commutative = manual_proof!(…); bkfold takes the proof itself as an argument:
/-- The coordinator's per-key counter: one more for each yes vote. -/
def yesStep (n : Nat) (v : Bool) : Nat := if v then n + 1 else n
theorem yesStep_comm (s : Nat) (x y : Bool) :
yesStep (yesStep s x) y = yesStep (yesStep s y) x := by
cases x <;> cases y <;> rfl
After the block, decisions is in scope as a stream of per-tick batches at the coordinator. The program's result flattens it into an unbounded stream, Rust's .all_ticks():
H.allTicks decisions
The Census
The census checks that the records hold exactly the nondeterminism the program is meant to have:
#nondet_census vote_quorum (nondets := 1) (scheds := 2) (fuels := 0)
The program has one content decision (the batch), two network edges and no cycle. If a count disagrees, the build fails, so a nondet! you forgot to turn into a decision, or one you added by accident, is caught here (The Census).
What the Build Generates
When the file elaborates, hydro def reports what it generated:
info: Examples/TutorialSteps/QuorumProgram.lean:24:0: hydro def Hydro.TutorialSteps.QuorumProgram.vote_quorum: callees [], inlines [], fix := false
info: Examples/TutorialSteps/QuorumProgram.lean:24:0: hydro_couple Hydro.TutorialSteps.QuorumProgram.vote_quorum: 1 sr, 1 rr, 1 lag (+ex/vdec)
…
info: Examples/TutorialSteps/QuorumProgram.lean:24:0: hydro_project Hydro.TutorialSteps.QuorumProgram.vote_quorum: Hydro.TutorialSteps.QuorumProgram.vote_quorum.dag, Hydro.TutorialSteps.QuorumProgram.vote_quorum.dag_denote (kernel rfl)
info: Examples/TutorialSteps/QuorumProgram.lean:24:0: hydro_project Hydro.TutorialSteps.QuorumProgram.vote_quorum: Hydro.TutorialSteps.QuorumProgram.vote_quorum.dag_valid (per node), Hydro.TutorialSteps.QuorumProgram.vote_quorum.dag_agreeL
info: Examples/TutorialSteps/QuorumProgram.lean:57:0: #nondet_census Hydro.TutorialSteps.QuorumProgram.vote_quorum: nondets 1, scheds 2, fuels 0
None of this needs a contract. fix := false says the program has no cycle. The hydro_couple line generates the coupling lemmas, and +ex/vdec says the generator also built the function that reads a Values batch decision off a machine run. vote_quorum.dag is the dataflow graph the processes run, and dag_denote says that running the graph gives the same result as running the program at SchedSem. A proof carries the contract to production by citing these lemmas by name.
Next Steps
The program is written, it compiles, and its nondeterminism matches the census, but it guarantees nothing yet. In Proving the Quorum, you will write its contract, start with every proof a sorry, and work backwards until none is left.