diff --git a/.gitattributes b/.gitattributes index 05028087a749..dadda9180eae 100644 --- a/.gitattributes +++ b/.gitattributes @@ -8,4 +8,7 @@ src/crypto/test/cbor_fuzz_corpus/* binary *.h linguist-language=C++ *.cpp linguist-language=C++ -.*canary merge=keeplocal \ No newline at end of file +.*canary merge=keeplocal + +lean/disaster-recovery/DisasterRecovery/Proofs/**/*.lean linguist-generated=true +lean/disaster-recovery/DisasterRecovery.lean text eol=lf \ No newline at end of file diff --git a/.github/workflows/README.md b/.github/workflows/README.md index 4eb030772236..e648cab7db61 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -101,6 +101,22 @@ Runs on pull requests that change `tla/` or `src/consensus/aft/raft.h`. File: `tla-shallow.yml` 3rd party dependencies: None +# Lean + +Runs all Lean verification for the repository. Future Lean checks should be +added as jobs to this workflow. + +The disaster recovery job builds the canonical model with `lake build --wfail`, +audits its transitive axiom dependencies with `lake lint`, and runs its +executable canonical behavior checks on Ubuntu 26.04 on relevant pull requests. +The build and audit include both the human-reviewed model and system properties +and the proof implementation files marked as generated for review purposes. +The standard `mk_all --check` command ensures that the audit root imports every +library module, so newly added proofs cannot silently escape the checks. + +File: `lean.yml` +3rd party dependencies: None + # Vendored Dependency Verification Verifies that files under `3rdparty/` match the Git commits or release artifacts diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml new file mode 100644 index 000000000000..d34e5678487f --- /dev/null +++ b/.github/workflows/lean.yml @@ -0,0 +1,47 @@ +name: "Lean" + +on: + pull_request: + paths: + - "lean/**" + - ".github/workflows/lean.yml" + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: read-all + +jobs: + disaster-recovery: + name: Disaster recovery model and proofs + runs-on: ubuntu-26.04 + timeout-minutes: 30 + + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + + - name: Install Lean + shell: bash + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y elan + elan toolchain install "$(cat lean/disaster-recovery/lean-toolchain)" + + - name: Restore Mathlib cache + working-directory: lean/disaster-recovery + shell: bash + run: | + set -euo pipefail + lake exe cache get + + - name: Build and check canonical model + working-directory: lean/disaster-recovery + shell: bash + run: | + set -euo pipefail + lake exe mk_all --check --lib DisasterRecovery + lake build --wfail + lake lint + lake exe canonical-checks diff --git a/lean/.gitignore b/lean/.gitignore new file mode 100644 index 000000000000..01f8cdb637da --- /dev/null +++ b/lean/.gitignore @@ -0,0 +1 @@ +.lake/ diff --git a/lean/disaster-recovery/CanonicalTests.lean b/lean/disaster-recovery/CanonicalTests.lean new file mode 100644 index 000000000000..db28b2921e4d --- /dev/null +++ b/lean/disaster-recovery/CanonicalTests.lean @@ -0,0 +1,145 @@ +import DisasterRecovery.Protocol.Model + +open DisasterRecovery.Protocol.Model + +private def expect (condition : Bool) (message : String) : IO Unit := + unless condition do throw (IO.userError message) + +private def eventsFor (config : Config) : List Event := + let messages := config.expectedLocations.flatMap fun source => + [ + .receiveGossip source { view := 0, seqno := source.length } .accepted, + .receiveGossip source { view := 0, seqno := source.length } .rejected, + .receiveVote source .accepted, + .receiveVote source .rejected, + .receiveIAmOpen source .accepted, + .receiveIAmOpen source .rejected + ] + messages ++ [.timeout, .retry] + +private def invariant (state : NodeState) : Bool := + let chosenReady := + if state.phase == .voting then state.chosen.isSome else true + let openingKind := + if state.phase == .opening || state.phase == .open then + state.openKind.isSome + else + true + let restartOnlyJoining := + if state.restartRequested then state.phase == .joining else true + chosenReady && openingKind && restartOnlyJoining + +private def enumerate (config : Config) (location : Location) : IO (Prod Nat Nat) := do + let initial := initialNode location + let mut states := #[initial] + let mut seen : Std.HashMap String Nat := {} + seen := seen.insert (stateKey initial) 0 + let mut cursor := 0 + let mut edges := 0 + while cursor < states.size do + let state := states[cursor]! + expect (invariant state) s!"canonical invariant failed: {stateKey state}" + for event in eventsFor config do + let next := (step config state event).state + edges := edges + 1 + let key := stateKey next + if !seen.contains key then + seen := seen.insert key states.size + states := states.push next + cursor := cursor + 1 + pure (states.size, edges) + +def main : IO UInt32 := do + let config : Config := { + instanceId := "canonical-tests" + expectedLocations := ["A", "B"] + } + expect config.isValid "canonical test configuration is invalid" + expect + (!({ instanceId := "invalid", expectedLocations := ["A", "A"] } : + Config).isValid) + "duplicate expected locations were accepted" + expect (voteQuorum config == 2) "two-node strict majority must be two" + + let initial := initialNode "A" + expect initial.gossips.isEmpty "canonical C++ state must start without gossip" + + let first := step config initial + (.receiveGossip "A" { view := 1, seqno := 10 } .accepted) + expect (first.state.phase == .gossiping) "one of two gossips advanced early" + let duplicate := step config first.state + (.receiveGossip "A" { view := 99, seqno := 99 } .accepted) + expect (duplicate.state == first.state) + "duplicate gossip source changed its recorded TxID" + let second := step config first.state + (.receiveGossip "B" { view := 2, seqno := 1 } .accepted) + expect (second.state.phase == .voting) "all expected gossips did not advance" + expect (second.state.chosen == some "B") "full TxID maximum was not chosen" + + let tiedA := step config initial + (.receiveGossip "A" { view := 2, seqno := 1 } .accepted) + let tiedB := step config tiedA.state + (.receiveGossip "B" { view := 2, seqno := 1 } .accepted) + expect (tiedB.state.chosen == some "B") + "location name did not break an equal TxID tie lexicographically" + + let frozen := step config second.state + (.receiveGossip "C" { view := 9, seqno := 9 } .accepted) + expect (!frozen.accepted && frozen.state == second.state) + "gossip did not freeze after choosing a node" + + let oneVote := step config second.state (.receiveVote "A" .accepted) + expect (oneVote.state.phase == .voting) "even-node quorum used legacy threshold" + let twoVotes := step config oneVote.state (.receiveVote "B" .accepted) + expect (twoVotes.state.phase == .opening) "strict voting quorum did not open" + expect (twoVotes.state.openKind == some .quorum) "quorum path mislabeled" + + let emptyVoting := { + initial with + phase := .voting + timeoutState := .voting + chosen := some "A" + } + let noVotes := step config emptyVoting .timeout + expect (noVotes.state == emptyVoting) + "aligned voting timeout with zero votes advanced" + + let oneVoteWaiting := { emptyVoting with votes := ["A"] } + let failover := step config oneVoteWaiting .timeout + expect (failover.state.phase == .opening) "failover vote did not open" + expect (failover.state.openKind == some .failover) "failover path mislabeled" + + let opening := { + twoVotes.state with + timeoutState := .opening + } + let complete := step config opening .timeout + expect (complete.state.phase == .open) "Opening timeout did not reach Open" + + let joining := step config initial + (.receiveIAmOpen "B" .accepted) + expect (joining.state.phase == .joining && joining.state.restartRequested) + "IAmOpen did not request joining restart" + + let retry := step config second.state .retry + expect + (retry.effects == + [.sendVote "B", .sendGossip "A", .sendGossip "B"]) + "Voting retry did not send vote before continuing gossip" + + let unexpectedConfig : Config := { + instanceId := "unexpected" + expectedLocations := ["A"] + } + let unexpected := step unexpectedConfig (initialNode "A") + (.receiveGossip "OUTSIDE" { view := 1, seqno := 1 } .accepted) + expect (unexpected.state.phase == .voting) + "model no longer exposes C++ acceptance of unexpected validated locations" + + let (oneStates, oneEdges) <- enumerate + { instanceId := "n1", expectedLocations := ["A"] } "A" + let (twoStates, twoEdges) <- enumerate config "A" + IO.println s!"canonical n=1: {oneStates} states, {oneEdges} event edges" + IO.println s!"canonical n=2: {twoStates} states, {twoEdges} event edges" + IO.println "all canonical semantic checks passed" + pure 0 diff --git a/lean/disaster-recovery/DisasterRecovery.lean b/lean/disaster-recovery/DisasterRecovery.lean new file mode 100644 index 000000000000..e65fc0ebad9b --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery.lean @@ -0,0 +1,10 @@ +import DisasterRecovery.Proofs.Committed +import DisasterRecovery.Proofs.Invariants +import DisasterRecovery.Proofs.Model +import DisasterRecovery.Proofs.Quorum +import DisasterRecovery.Properties +import DisasterRecovery.Protocol.Committed +import DisasterRecovery.Protocol.Global +import DisasterRecovery.Protocol.Invariants +import DisasterRecovery.Protocol.Model +import DisasterRecovery.Protocol.Quorum diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Committed.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Committed.lean new file mode 100644 index 000000000000..d5a926a7a046 --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Committed.lean @@ -0,0 +1,240 @@ +import DisasterRecovery.Protocol.Committed +import DisasterRecovery.Proofs.Quorum +import Mathlib.Tactic + +/-! +Machine-checked proof implementations. Review the system-level statements in +`DisasterRecovery.Properties` and assumptions in `DisasterRecovery.Protocol.Committed`. +-/ + +namespace DisasterRecovery.Proofs.Committed + +open Protocol +open Model hiding Config +open Global Protocol.Invariants Protocol.Quorum Protocol.Committed +open DisasterRecovery.Proofs.Invariants DisasterRecovery.Proofs.Quorum + +lemma prefix_refl (txid : TxID) : TxID.EarlierThan txid txid := by + simp [TxID.EarlierThan] + +lemma prefix_trans + {first second third : TxID} + (firstSecond : TxID.EarlierThan first second) + (secondThird : TxID.EarlierThan second third) : + TxID.EarlierThan first third := by + simp [TxID.EarlierThan] at firstSecond secondThird ⊢ + omega + +lemma prefix_of_score_true + (leftName rightName : Location) + (left right : TxID) + (score : + txScoreGreater leftName left rightName right = true) : + TxID.EarlierThan right left := by + simp [txScoreGreater] at score + simp [TxID.EarlierThan] + omega + +lemma prefix_of_score_false + (leftName rightName : Location) + (left right : TxID) + (score : + txScoreGreater leftName left rightName right = false) : + TxID.EarlierThan left right := by + simp [txScoreGreater] at score + simp [TxID.EarlierThan] + omega + +lemma current_prefix_selectMaximum + (current candidate : Prod Location TxID) : + TxID.EarlierThan current.2 + (selectMaximum current candidate).2 := by + unfold selectMaximum + split + · rename_i score + exact prefix_of_score_true + candidate.1 current.1 candidate.2 current.2 score + · exact prefix_refl current.2 + +lemma candidate_prefix_selectMaximum + (current candidate : Prod Location TxID) : + TxID.EarlierThan candidate.2 + (selectMaximum current candidate).2 := by + unfold selectMaximum + split + · exact prefix_refl candidate.2 + · rename_i score + exact prefix_of_score_false + candidate.1 current.1 candidate.2 current.2 + (Bool.eq_false_iff.mpr score) + +lemma foldl_selectMaximum_upper_bound + (current member : Prod Location TxID) + (tail : List (Prod Location TxID)) + (membership : member = current \/ member ∈ tail) : + TxID.EarlierThan member.2 + (tail.foldl selectMaximum current).2 := by + induction tail generalizing current member with + | nil => + simp at membership + subst member + exact prefix_refl current.2 + | cons candidate rest ih => + simp only [List.foldl_cons] + rcases membership with currentMember | tailMember + · subst member + exact prefix_trans + (current_prefix_selectMaximum current candidate) + (ih (selectMaximum current candidate) + (selectMaximum current candidate) (Or.inl rfl)) + · rw [List.mem_cons] at tailMember + rcases tailMember with candidateMember | restMember + · subst member + exact prefix_trans + (candidate_prefix_selectMaximum current candidate) + (ih (selectMaximum current candidate) + (selectMaximum current candidate) (Or.inl rfl)) + · exact ih (selectMaximum current candidate) member + (Or.inr restMember) + +lemma maximumGossip_upper_bound + {gossips : List (Prod Location TxID)} + {selected member : Prod Location TxID} + (maximum : maximumGossip gossips = some selected) + (membership : member ∈ gossips) : + TxID.EarlierThan member.2 selected.2 := by + cases gossips with + | nil => simp at membership + | cons head tail => + simp [maximumGossip] at maximum + rw [←maximum] + apply foldl_selectMaximum_upper_bound head member tail + simpa using membership + +lemma foldl_selectMaximum_mem + (current : Prod Location TxID) + (tail : List (Prod Location TxID)) : + tail.foldl selectMaximum current ∈ current :: tail := by + induction tail generalizing current with + | nil => simp + | cons candidate rest ih => + simp only [List.foldl_cons] + have selected : + selectMaximum current candidate = current \/ + selectMaximum current candidate = candidate := by + unfold selectMaximum + split <;> simp + have member := + ih (selectMaximum current candidate) + rw [List.mem_cons] at member + rcases member with currentMember | restMember + · rw [currentMember] + rcases selected with selected | selected + · simp [selected] + · simp [selected] + · simp [restMember] + +lemma maximumGossip_mem + {gossips : List (Prod Location TxID)} + {selected : Prod Location TxID} + (maximum : maximumGossip gossips = some selected) : + selected ∈ gossips := by + cases gossips with + | nil => simp [maximumGossip] at maximum + | cons head tail => + simp [maximumGossip] at maximum + rw [←maximum] + exact foldl_selectMaximum_mem head tail + +lemma recoveredTxID_of_mem + {config : Config} + {location : Location} + {txid : TxID} + (valid : config.Valid) + (membership : (location, txid) ∈ config.recovered) : + recoveredTxID config location = some txid := by + have keysNodup : (config.recovered.map Prod.fst).Nodup := by + rw [valid.2.2] + exact valid.2.1 + unfold recoveredTxID + cases found : + config.recovered.find? fun entry => entry.1 == location with + | none => + rw [List.find?_eq_none] at found + exact False.elim + (found (location, txid) membership (by simp)) + | some entry => + have foundMember : entry ∈ config.recovered := + List.mem_of_find?_eq_some found + have foundLocation : entry.1 = location := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location TxID => + entry.1 == location) found) + have same : + entry = (location, txid) := + eq_of_key_eq keysNodup foundMember membership foundLocation + simp [same] + +lemma full_gossip_selection_preserves_commit + {config : Config} + {state : State} + {opener : Location} + {committed : TxID} + (reachable : Reachable config state) + (full : FullGossipSelection config state opener) + (durable : DurableCommit config committed) : + exists recovered, + recoveredTxID config opener = some recovered /\ + TxID.EarlierThan committed recovered := by + have configValid := reachable_config_valid reachable + have wellFormed := reachable_well_formed reachable + have invariant := reachable_quorum_invariant reachable + rcases full with + ⟨vote, sent, payload, target, complete⟩ + have voteState := + retry_vote_state (wellFormed.sentValid vote sent) payload + rcases invariant.sentVotesSelected vote sent payload with + ⟨selectedTarget, selectedTxID, choice, selected⟩ + have selectedTargetEq : selectedTarget = vote.target := + Option.some.inj (choice.symm.trans voteState.2) + rw [selectedTargetEq, target] at selected + rcases durable with + ⟨durableLocation, durableTxID, durableMember, committedDurable⟩ + have durableGossip : + (durableLocation, durableTxID) ∈ vote.sourceState.gossips := + (complete (durableLocation, durableTxID)).2 durableMember + have durableMaximum := + maximumGossip_upper_bound selected durableGossip + have selectedGossip : + (opener, selectedTxID) ∈ vote.sourceState.gossips := + maximumGossip_mem selected + have selectedRecovered : + (opener, selectedTxID) ∈ config.recovered := + (complete (opener, selectedTxID)).1 selectedGossip + exact + ⟨selectedTxID, + recoveredTxID_of_mem configValid selectedRecovered, + prefix_trans committedDurable durableMaximum⟩ + +/-- +Quorum opening scopes the result to an actual decision, while the separate +`FullGossipSelection` premise carries the completeness requirement. Quorum +opening alone does not imply complete gossip because voting may follow a +gossip timeout. +-/ +lemma quorum_open_preserves_commit + {config : Config} + {state : State} + {opener : Location} + {committed : TxID} + (reachable : Reachable config state) + (_opened : QuorumOpened state opener) + (full : FullGossipSelection config state opener) + (durable : DurableCommit config committed) : + exists recovered, + recoveredTxID config opener = some recovered /\ + TxID.EarlierThan committed recovered := + full_gossip_selection_preserves_commit reachable full durable + +end DisasterRecovery.Proofs.Committed diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean new file mode 100644 index 000000000000..935ebc646ac4 --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Invariants.lean @@ -0,0 +1,874 @@ +import DisasterRecovery.Protocol.Invariants +import Mathlib.Tactic + +/-! +Machine-checked proof implementations. Review the system-level statements in +`DisasterRecovery.Properties` and definitions in `DisasterRecovery.Protocol.Invariants`. +-/ + +namespace DisasterRecovery.Proofs.Invariants + +open Protocol +open Model hiding Config +open Global Protocol.Invariants + +lemma messageForEffect_source + {config : Config} + {source : Location} + {sourceState : NodeState} + {effect : Effect} + {envelope : Envelope} + (created : + messageForEffect config source sourceState effect = some envelope) : + envelope.source = source /\ + envelope.sourceState = sourceState := by + cases effect with + | sendGossip target => + cases found : recoveredTxID config source with + | none => + simp [messageForEffect, found] at created + | some txid => + simp [messageForEffect, found] at created + rw [←created] + exact ⟨rfl, rfl⟩ + | sendVote target => + simp [messageForEffect] at created + rw [←created] + exact ⟨rfl, rfl⟩ + | sendIAmOpen target => + simp [messageForEffect] at created + rw [←created] + exact ⟨rfl, rfl⟩ + | opening kind => + simp_all [messageForEffect] + | restart chosen => + simp_all [messageForEffect] + | completed => + simp_all [messageForEffect] + | rejected reason => + simp_all [messageForEffect] + +lemma retryMessages_source + {config : Config} + {source : Location} + {sourceState : NodeState} + {envelope : Envelope} + (created : + envelope ∈ retryMessages config source sourceState) : + envelope.source = source /\ + envelope.sourceState = sourceState := by + rw [retryMessages, List.mem_filterMap] at created + rcases created with ⟨effect, _, produced⟩ + exact messageForEffect_source produced + +lemma retryMessages_valid + (config : Config) + (source : Location) + (sourceState : NodeState) + (sourceLocation : sourceState.location = source) : + forall envelope, + envelope ∈ retryMessages config source sourceState -> + envelope.Valid config := by + intro envelope created + rcases retryMessages_source created with + ⟨sourceEq, stateEq⟩ + constructor + · rw [stateEq, sourceEq] + exact sourceLocation + · rw [sourceEq, stateEq] + exact created + +lemma valid_envelope_effect + {config : Config} + {envelope : Envelope} + (valid : envelope.Valid config) : + exists effect, + effect ∈ + (step config.protocol envelope.sourceState .retry).effects /\ + messageForEffect config envelope.source + envelope.sourceState effect = some envelope := by + rcases valid with ⟨_, created⟩ + rw [retryMessages, List.mem_filterMap] at created + exact created + +lemma valid_gossip_uses_recovered_txid + {config : Config} + {envelope : Envelope} + {txid : TxID} + (valid : envelope.Valid config) + (gossip : envelope.payload = .gossip txid) : + recoveredTxID config envelope.source = some txid := by + rcases valid_envelope_effect valid with + ⟨effect, _, created⟩ + cases effect with + | sendGossip target => + cases found : recoveredTxID config envelope.source with + | none => + simp [messageForEffect, found] at created + | some recovered => + simp [messageForEffect, found] at created + rw [←created] at gossip + injection gossip with same + subst recovered + rfl + | sendVote target => + simp [messageForEffect] at created + rw [←created] at gossip + contradiction + | sendIAmOpen target => + simp [messageForEffect] at created + rw [←created] at gossip + contradiction + | opening kind => + simp [messageForEffect] at created + | restart chosen => + simp [messageForEffect] at created + | completed => + simp [messageForEffect] at created + | rejected reason => + simp [messageForEffect] at created + +lemma step_preserves_location + (config : Model.Config) + (state : NodeState) + (event : Event) : + (step config state event).state.location = state.location := by + cases event <;> + simp [step, rejected, advance, advanceTimeoutLane] + all_goals repeat first | split | simp_all + +lemma nodeState_location + {state : State} + {node : Location} + {foundState : NodeState} + (locations : + forall entry, entry ∈ state.system.nodes -> + entry.2.location = entry.1) + (found : nodeState state node = some foundState) : + foundState.location = node := by + rw [nodeState, Option.map_eq_some_iff] at found + rcases found with ⟨entry, findEq, stateEq⟩ + have membership : entry ∈ state.system.nodes := + List.mem_of_find?_eq_some findEq + have condition : (entry.1 == node) = true := + List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == node) findEq + have keyEq : entry.1 = node := beq_iff_eq.mp condition + rw [←stateEq, locations entry membership, keyEq] + +lemma initial_well_formed + (config : Config) + (active : List Location) + (valid : config.Valid) + (activeNodup : active.Nodup) + (activeConfigured : + forall node, node ∈ active -> + node ∈ config.protocol.expectedLocations) : + WellFormed config (initial config active) := by + constructor + · simp [Global.initial, initialSystem, Function.comp_def] + · simpa [Global.initial, initialSystem, Function.comp_def] using valid.2.1 + · simp [Global.initial, initialSystem, initialNode] + · exact activeNodup + · exact activeConfigured + · simp [Global.initial] + · simp [Global.initial] + · simp [Global.initial] + · constructor <;> simp [Global.initial] + +@[simp] +lemma recordEffects_active + (node : Location) + (nodeState : NodeState) + (effects : List Effect) + (state : State) : + (recordEffects node nodeState effects state).active = state.active := by + induction effects generalizing state with + | nil => rfl + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + change + (recordEffects node nodeState tail + (recordEffect node nodeState state effect)).active = + state.active + rw [ih] + cases effect <;> rfl + +@[simp] +lemma recordEffects_system + (node : Location) + (nodeState : NodeState) + (effects : List Effect) + (state : State) : + (recordEffects node nodeState effects state).system = state.system := by + induction effects generalizing state with + | nil => rfl + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + change + (recordEffects node nodeState tail + (recordEffect node nodeState state effect)).system = + state.system + rw [ih] + cases effect <;> rfl + +@[simp] +lemma recordEffects_network + (node : Location) + (nodeState : NodeState) + (effects : List Effect) + (state : State) : + (recordEffects node nodeState effects state).network = state.network := by + induction effects generalizing state with + | nil => rfl + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + change + (recordEffects node nodeState tail + (recordEffect node nodeState state effect)).network = + state.network + rw [ih] + cases effect <;> rfl + +@[simp] +lemma recordEffects_sent + (node : Location) + (nodeState : NodeState) + (effects : List Effect) + (state : State) : + (recordEffects node nodeState effects state).sent = state.sent := by + induction effects generalizing state with + | nil => rfl + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + change + (recordEffects node nodeState tail + (recordEffect node nodeState state effect)).sent = + state.sent + rw [ih] + cases effect <;> rfl + +lemma recordEffect_preserves_histories_active + {node : Location} + {nodeState : NodeState} + {state : State} + {effect : Effect} + (wellFormed : HistoriesActive state) + (nodeActive : node ∈ state.active) : + HistoriesActive (recordEffect node nodeState state effect) := by + rcases wellFormed with ⟨openings, restarts, completed⟩ + cases effect <;> + constructor <;> + simp_all [recordEffect] + +lemma recordEffects_preserves_histories_active + {node : Location} + {nodeState : NodeState} + {effects : List Effect} + {state : State} + (wellFormed : HistoriesActive state) + (nodeActive : node ∈ state.active) : + HistoriesActive (recordEffects node nodeState effects state) := by + induction effects generalizing state with + | nil => exact wellFormed + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + apply ih + · exact recordEffect_preserves_histories_active wellFormed nodeActive + · cases effect <;> simpa [recordEffect] using nodeActive + +lemma mem_of_mem_removeOne + [BEq α] + (value member : α) + (values : List α) : + member ∈ removeOne value values -> + member ∈ values := by + induction values with + | nil => simp [removeOne] + | cons head tail ih => + simp only [removeOne] + split + · exact List.mem_cons_of_mem head + · intro membership + rw [List.mem_cons] at membership ⊢ + exact membership.imp_right ih + +lemma mem_openings_recordEffect + {node : Location} + {nodeState : NodeState} + {state : State} + {effect : Effect} + {opening : Opening} + (membership : opening ∈ state.openings) : + opening ∈ (recordEffect node nodeState state effect).openings := by + cases effect <;> simp_all [recordEffect] + +lemma mem_restarts_recordEffect + {node : Location} + {nodeState : NodeState} + {state : State} + {effect : Effect} + {restart : Location} + (membership : restart ∈ state.restarts) : + restart ∈ (recordEffect node nodeState state effect).restarts := by + cases effect <;> simp_all [recordEffect] + +lemma mem_completed_recordEffect + {node : Location} + {nodeState : NodeState} + {state : State} + {effect : Effect} + {completed : Location} + (membership : completed ∈ state.completed) : + completed ∈ (recordEffect node nodeState state effect).completed := by + cases effect <;> simp_all [recordEffect] + +lemma mem_openings_recordEffects + {node : Location} + {nodeState : NodeState} + {state : State} + {effects : List Effect} + {opening : Opening} + (membership : opening ∈ state.openings) : + opening ∈ (recordEffects node nodeState effects state).openings := by + induction effects generalizing state with + | nil => exact membership + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + exact ih (mem_openings_recordEffect membership) + +lemma mem_restarts_recordEffects + {node : Location} + {nodeState : NodeState} + {state : State} + {effects : List Effect} + {restart : Location} + (membership : restart ∈ state.restarts) : + restart ∈ (recordEffects node nodeState effects state).restarts := by + induction effects generalizing state with + | nil => exact membership + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + exact ih (mem_restarts_recordEffect membership) + +lemma mem_completed_recordEffects + {node : Location} + {nodeState : NodeState} + {state : State} + {effects : List Effect} + {completed : Location} + (membership : completed ∈ state.completed) : + completed ∈ (recordEffects node nodeState effects state).completed := by + induction effects generalizing state with + | nil => exact membership + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + exact ih (mem_completed_recordEffect membership) + +lemma replaceNode_keys + (target : Location) + (nextState : NodeState) + (nodes : List (Prod Location NodeState)) : + (replaceNode target nextState nodes).map Prod.fst = + nodes.map Prod.fst := by + induction nodes with + | nil => rfl + | cons entry tail ih => + simp only [replaceNode, List.map_cons] + split + · + rename_i condition + have same : entry.1 = target := beq_iff_eq.mp condition + simp only [List.cons.injEq] + constructor + · exact same.symm + · simpa [replaceNode] using ih + · + simp only [List.cons.injEq, true_and] + simpa [replaceNode] using ih + +lemma replaceNode_locations + (target : Location) + (nextState : NodeState) + (nodes : List (Prod Location NodeState)) + (locations : + forall entry, entry ∈ nodes -> + entry.2.location = entry.1) + (nextLocation : nextState.location = target) : + forall entry, entry ∈ replaceNode target nextState nodes -> + entry.2.location = entry.1 := by + intro entry membership + rw [replaceNode, List.mem_map] at membership + rcases membership with ⟨previous, previousMember, rfl⟩ + split + · exact nextLocation + · exact locations previous previousMember + +lemma findNode_replaceNode_ne + (target other : Location) + (nextState : NodeState) + (nodes : List (Prod Location NodeState)) + (different : other ≠ target) : + ((replaceNode target nextState nodes).find? + fun entry => entry.1 == other).map Prod.snd = + (nodes.find? fun entry => entry.1 == other).map Prod.snd := by + let replace : Prod Location NodeState -> Prod Location NodeState := + fun entry => + if entry.1 == target then (target, nextState) else entry + change + Option.map Prod.snd + (List.find? (fun entry => entry.1 == other) + (nodes.map replace)) = + Option.map Prod.snd + (List.find? (fun entry => entry.1 == other) nodes) + rw [List.find?_map] + have predicate : + ((fun entry : Prod Location NodeState => entry.1 == other) ∘ + replace) = + (fun entry => entry.1 == other) := by + funext entry + by_cases atTarget : entry.1 = target + · simp [replace, atTarget] + · simp [replace, atTarget] + rw [predicate] + cases found : + List.find? (fun entry : Prod Location NodeState => + entry.1 == other) nodes with + | none => simp + | some entry => + have condition : + (entry.1 == other) = true := + List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == other) found + have entryOther : entry.1 = other := + beq_iff_eq.mp condition + have notTarget : entry.1 ≠ target := by + simpa [entryOther] using different + simp [replace, notTarget] + +lemma systemStep_node_keys_eq + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (transition : + systemStep config before target event = some (after, output)) : + after.nodes.map Prod.fst = before.nodes.map Prod.fst := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with ⟨node, _, stateEq, _⟩ + rw [←stateEq] + exact replaceNode_keys target + (step config node event).state before.nodes + +lemma systemStep_preserves_node_locations + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (locations : + forall entry, entry ∈ before.nodes -> + entry.2.location = entry.1) + (transition : + systemStep config before target event = some (after, output)) : + forall entry, entry ∈ after.nodes -> + entry.2.location = entry.1 := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, stateEq, _⟩ + rw [←stateEq] + apply replaceNode_locations + · exact locations + · calc + (step config node event).state.location = + node.location := step_preserves_location config node event + _ = key := + locations (key, node) (List.mem_of_find?_eq_some found) + _ = target := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == target) found) + +lemma systemStep_other_node_eq + {config : Model.Config} + {before after : SystemState} + {target other : Location} + {event : Event} + {output : StepOutput} + (different : other ≠ target) + (transition : + systemStep config before target event = some (after, output)) : + (after.nodes.find? fun entry => entry.1 == other).map Prod.snd = + (before.nodes.find? fun entry => entry.1 == other).map Prod.snd := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with ⟨node, _, stateEq, _⟩ + rw [←stateEq] + exact findNode_replaceNode_ne target other + (step config node event).state before.nodes different + +lemma next_active_eq + {config : Config} + {before after : State} + {action : Action} + (transition : next config before action = some after) : + after.active = before.active := by + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + rfl + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, _, system, output, _, rfl⟩ + simp + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, system, output, _, _, rfl⟩ + simp + +lemma next_node_keys_eq + {config : Config} + {before after : State} + {action : Action} + (transition : next config before action = some after) : + after.system.nodes.map Prod.fst = + before.system.nodes.map Prod.fst := by + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + rfl + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, _, system, output, systemStep, rfl⟩ + simpa using systemStep_node_keys_eq systemStep + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, system, output, systemStep, _, rfl⟩ + simpa using systemStep_node_keys_eq systemStep + +lemma retry_system_eq + {config : Config} + {before after : State} + {source : Location} + (transition : next config before (.retry source) = some after) : + after.system = before.system := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + rfl + +lemma deliver_network_eq + {config : Config} + {before after : State} + {envelope : Envelope} + (transition : next config before (.deliver envelope) = some after) : + after.network = removeOne envelope before.network := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, rfl⟩ + simp + +lemma timeout_network_eq + {config : Config} + {before after : State} + {target : Location} + (transition : next config before (.timeout target) = some after) : + after.network = before.network := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, rfl⟩ + simp + +lemma deliver_other_node_eq + {config : Config} + {before after : State} + {envelope : Envelope} + {other : Location} + (different : other ≠ envelope.target) + (transition : next config before (.deliver envelope) = some after) : + nodeState after other = nodeState before other := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, systemStep, stateEq⟩ + rw [←stateEq] + simp only [nodeState, recordEffects_system] + exact systemStep_other_node_eq different systemStep + +lemma timeout_other_node_eq + {config : Config} + {before after : State} + {target other : Location} + (different : other ≠ target) + (transition : next config before (.timeout target) = some after) : + nodeState after other = nodeState before other := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, systemStep, _, stateEq⟩ + rw [←stateEq] + simp only [nodeState, recordEffects_system] + exact systemStep_other_node_eq different systemStep + +lemma next_sent_extends + {config : Config} + {before after : State} + {action : Action} + (transition : next config before action = some after) : + exists added, after.sent = before.sent ++ added := by + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + exact ⟨retryMessages config source sourceState, rfl⟩ + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, rfl⟩ + refine ⟨[], ?_⟩ + simp + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, rfl⟩ + refine ⟨[], ?_⟩ + simp + +lemma next_openings_monotonic + {config : Config} + {before after : State} + {action : Action} + (transition : next config before action = some after) : + forall opening, opening ∈ before.openings -> + opening ∈ after.openings := by + intro opening membership + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + exact membership + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, rfl⟩ + apply mem_openings_recordEffects + simpa using membership + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, rfl⟩ + apply mem_openings_recordEffects + simpa using membership + +lemma next_restarts_monotonic + {config : Config} + {before after : State} + {action : Action} + (transition : next config before action = some after) : + forall restart, restart ∈ before.restarts -> + restart ∈ after.restarts := by + intro restart membership + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + exact membership + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, rfl⟩ + apply mem_restarts_recordEffects + simpa using membership + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, rfl⟩ + apply mem_restarts_recordEffects + simpa using membership + +lemma next_completed_monotonic + {config : Config} + {before after : State} + {action : Action} + (transition : next config before action = some after) : + forall completed, completed ∈ before.completed -> + completed ∈ after.completed := by + intro completed membership + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + exact membership + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, rfl⟩ + apply mem_completed_recordEffects + simpa using membership + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, rfl⟩ + apply mem_completed_recordEffects + simpa using membership + +lemma retry_preserves_well_formed + {config : Config} + {before after : State} + {source : Location} + (wellFormed : WellFormed config before) + (transition : next config before (.retry source) = some after) : + WellFormed config after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨sourceActive, sourceState, found, _, stateEq⟩ + have sourceLocation : sourceState.location = source := + nodeState_location wellFormed.nodeLocations found + rw [←stateEq] + constructor + · exact wellFormed.nodeKeys + · exact wellFormed.nodeKeysNodup + · exact wellFormed.nodeLocations + · exact wellFormed.activeNodup + · exact wellFormed.activeConfigured + · intro envelope membership + rw [List.mem_append] at membership + rcases membership with membership | membership + · exact wellFormed.sentValid envelope membership + · exact retryMessages_valid config source sourceState + sourceLocation envelope membership + · intro envelope membership + rw [List.mem_append] at membership + rcases membership with membership | membership + · exact wellFormed.sentSourceActive envelope membership + · rw [(retryMessages_source membership).1] + exact sourceActive + · intro envelope membership + rw [List.mem_append] at membership ⊢ + rcases membership with membership | membership + · exact Or.inl (wellFormed.networkSent envelope membership) + · exact Or.inr membership + · constructor + · exact wellFormed.historiesActive.openings + · exact wellFormed.historiesActive.restarts + · exact wellFormed.historiesActive.completed + +lemma deliver_preserves_well_formed + {config : Config} + {before after : State} + {envelope : Envelope} + (wellFormed : WellFormed config before) + (transition : next config before (.deliver envelope) = some after) : + WellFormed config after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, targetActive, system, output, systemStep, stateEq⟩ + rw [←stateEq] + constructor + · simp only [recordEffects_system] + exact (systemStep_node_keys_eq systemStep).trans + wellFormed.nodeKeys + · rw [recordEffects_system, systemStep_node_keys_eq systemStep] + exact wellFormed.nodeKeysNodup + · simp only [recordEffects_system] + exact systemStep_preserves_node_locations + wellFormed.nodeLocations systemStep + · simpa using wellFormed.activeNodup + · simpa using wellFormed.activeConfigured + · intro sent membership + rw [recordEffects_sent] at membership + exact wellFormed.sentValid sent membership + · intro sent membership + rw [recordEffects_sent] at membership + rw [recordEffects_active] + exact wellFormed.sentSourceActive sent membership + · intro pending membership + rw [recordEffects_network] at membership + rw [recordEffects_sent] + exact wellFormed.networkSent pending + (mem_of_mem_removeOne envelope pending before.network membership) + · apply recordEffects_preserves_histories_active + · constructor + · simpa using wellFormed.historiesActive.openings + · simpa using wellFormed.historiesActive.restarts + · simpa using wellFormed.historiesActive.completed + · simpa using targetActive + +lemma timeout_preserves_well_formed + {config : Config} + {before after : State} + {target : Location} + (wellFormed : WellFormed config before) + (transition : next config before (.timeout target) = some after) : + WellFormed config after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨targetActive, system, output, systemStep, _, stateEq⟩ + rw [←stateEq] + constructor + · simp only [recordEffects_system] + exact (systemStep_node_keys_eq systemStep).trans + wellFormed.nodeKeys + · rw [recordEffects_system, systemStep_node_keys_eq systemStep] + exact wellFormed.nodeKeysNodup + · simp only [recordEffects_system] + exact systemStep_preserves_node_locations + wellFormed.nodeLocations systemStep + · simpa using wellFormed.activeNodup + · simpa using wellFormed.activeConfigured + · intro sent membership + rw [recordEffects_sent] at membership + exact wellFormed.sentValid sent membership + · intro sent membership + rw [recordEffects_sent] at membership + rw [recordEffects_active] + exact wellFormed.sentSourceActive sent membership + · intro pending membership + rw [recordEffects_network] at membership + rw [recordEffects_sent] + exact wellFormed.networkSent pending membership + · apply recordEffects_preserves_histories_active + · constructor + · simpa using wellFormed.historiesActive.openings + · simpa using wellFormed.historiesActive.restarts + · simpa using wellFormed.historiesActive.completed + · simpa using targetActive + +lemma next_preserves_well_formed + {config : Config} + {before after : State} + {action : Action} + (wellFormed : WellFormed config before) + (transition : next config before action = some after) : + WellFormed config after := by + cases action with + | retry source => + exact retry_preserves_well_formed wellFormed transition + | deliver envelope => + exact deliver_preserves_well_formed wellFormed transition + | timeout target => + exact timeout_preserves_well_formed wellFormed transition + +lemma reachable_well_formed + {config : Config} + {state : State} + (reachable : Reachable config state) : + WellFormed config state := by + induction reachable with + | initial active valid nodup configured => + exact initial_well_formed config active valid nodup configured + | step reachable transition wellFormed => + exact next_preserves_well_formed wellFormed transition + +lemma reachable_config_valid + {config : Config} + {state : State} + (reachable : Reachable config state) : + config.Valid := by + induction reachable with + | initial active valid nodup configured => exact valid + | step reachable transition valid => exact valid + +end DisasterRecovery.Proofs.Invariants diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Model.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Model.lean new file mode 100644 index 000000000000..03ddc38e6c0a --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Model.lean @@ -0,0 +1,115 @@ +import DisasterRecovery.Protocol.Model +import Mathlib.Tactic.Lemma + +/-! +Machine-checked proof implementations. Review the system-level statements in +`DisasterRecovery.Properties` and definitions in `DisasterRecovery.Protocol.Model`. +-/ + +namespace DisasterRecovery.Proofs.Model + +open Protocol.Model + +lemma valid_timeout_requires_alignment + (state : NodeState) + (h : validTimeout state true = true) : + state.phase = state.timeoutState := by + simpa [validTimeout] using h + +lemma gossip_freezes_after_choice + (config : Config) + (state : NodeState) + (source : Location) + (txid : TxID) + (h : state.chosen.isSome = true) : + let output := step config state (.receiveGossip source txid .accepted) + output.state = state /\ output.accepted = false := by + cases chosen : state.chosen <;> simp_all [step, rejected] + +lemma rejected_gossip_stutters + (config : Config) + (state : NodeState) + (source : Location) + (txid : TxID) : + let output := step config state (.receiveGossip source txid .rejected) + output.state = state /\ output.accepted = false := by + simp [step, rejected] + +lemma duplicate_vote_is_idempotent + (source : Location) + (votes : List Location) + (h : votes.contains source = true) : + insertVote source votes = votes := by + unfold insertVote + rw [h] + simp + +lemma opening_rejects_iamopen + (config : Config) + (state : NodeState) + (source : Location) : + let opening := { state with phase := .opening } + let output := step config opening (.receiveIAmOpen source .accepted) + output.state = opening /\ output.accepted = false := by + simp [step, rejected] + +lemma open_rejects_iamopen + (config : Config) + (state : NodeState) + (source : Location) : + let opened := { state with phase := .open } + let output := step config opened (.receiveIAmOpen source .accepted) + output.state = opened /\ output.accepted = false := by + simp [step, rejected] + +lemma aligned_voting_timeout_without_votes_stutters + (config : Config) + (state : NodeState) : + let waiting := { + state with + phase := .voting + timeoutState := .voting + votes := [] + } + step config waiting .timeout = { state := waiting } := by + simp [step, advance, validTimeout, voteQuorum] + +lemma aligned_opening_timeout_completes + (config : Config) + (state : NodeState) : + let opening := { + state with + phase := .opening + timeoutState := .opening + } + let output := step config opening .timeout + output.state.phase = .open /\ + output.state.timeoutState = .opening /\ + output.effects = [.completed] := by + simp [step, advance, validTimeout, advanceTimeoutLane, advanceTimeoutState] + +lemma quorum_advance_opens + (config : Config) + (state : NodeState) + (phase : state.phase = .voting) + (quorum : state.votes.length >= voteQuorum config) : + let output := (advance config state false).get! + output.state.phase = .opening /\ + output.state.openKind = some .quorum /\ + output.effects = [.opening .quorum] := by + simp [advance, phase, quorum, validTimeout, advanceTimeoutLane] + +lemma aligned_empty_gossip_timeout_aborts + (config : Config) + (state : NodeState) : + let waiting := { + state with + phase := .gossiping + timeoutState := .gossiping + gossips := [] + } + let output := step config waiting .timeout + output.state = waiting /\ output.accepted = false := by + simp [step, advance, validTimeout, rejected, maximumGossip] + +end DisasterRecovery.Proofs.Model \ No newline at end of file diff --git a/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean b/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean new file mode 100644 index 000000000000..6f39a4e87c00 --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Proofs/Quorum.lean @@ -0,0 +1,1394 @@ +import DisasterRecovery.Protocol.Quorum +import DisasterRecovery.Proofs.Invariants +import Mathlib.Tactic + +/-! +Machine-checked proof implementations. Review the system-level statements in +`DisasterRecovery.Properties` and definitions in `DisasterRecovery.Protocol.Quorum`. +-/ + +namespace DisasterRecovery.Proofs.Quorum + +open Protocol +open Model hiding Config +open Global Protocol.Invariants Protocol.Quorum +open DisasterRecovery.Proofs.Invariants + +lemma insertVote_nodup + (source : Location) + {votes : List Location} + (nodup : votes.Nodup) : + (insertVote source votes).Nodup := by + unfold insertVote + split + · exact nodup + · rename_i absent + apply (List.mergeSort_perm _ _).symm.nodup + rw [List.nodup_cons] + exact + ⟨fun member => absent (List.contains_iff_mem.mpr member), nodup⟩ + +lemma mem_insertVote + {member source : Location} + {votes : List Location} + (membership : member ∈ insertVote source votes) : + member ∈ votes \/ member = source := by + unfold insertVote at membership + split at membership + · exact Or.inl membership + · have unsorted := + (List.mergeSort_perm _ _).mem_iff.mp membership + rw [List.mem_cons] at unsorted + exact unsorted.symm + +lemma step_preserves_votes_nodup + (config : Model.Config) + (state : NodeState) + (event : Event) + (nodup : state.votes.Nodup) : + (step config state event).state.votes.Nodup := by + cases event <;> + simp [step, rejected, advance, advanceTimeoutLane] + all_goals + repeat first | split | simp_all [insertVote_nodup] + +lemma step_votes_shape + (config : Model.Config) + (state : NodeState) + (event : Event) : + (step config state event).state.votes = state.votes \/ + exists source, + acceptedVoteSource event = some source /\ + (step config state event).state.votes = + insertVote source state.votes := by + cases event + all_goals try cases_type Validation + all_goals + simp [acceptedVoteSource, step, rejected, advance, advanceTimeoutLane] + all_goals repeat first | split | simp_all + +lemma step_vote_origin + (config : Model.Config) + (state : NodeState) + (event : Event) + (voter : Location) + (membership : voter ∈ (step config state event).state.votes) : + voter ∈ state.votes \/ + acceptedVoteSource event = some voter := by + rcases step_votes_shape config state event with + unchanged | ⟨source, sourceEq, changed⟩ + · rw [unchanged] at membership + exact Or.inl membership + · rw [changed] at membership + rcases mem_insertVote membership with old | added + · exact Or.inl old + · subst source + exact Or.inr sourceEq + +lemma step_preserves_non_gossiping + (config : Model.Config) + (state : NodeState) + (event : Event) + (pastGossip : state.phase ≠ .gossiping) : + (step config state event).state.phase ≠ .gossiping := by + cases event <;> + simp [step, rejected, advance, advanceTimeoutLane] + all_goals repeat first | split | simp_all + +lemma voting_step_preserves_choice + (config : Model.Config) + (state : NodeState) + (event : Event) + (pastGossip : state.phase ≠ .gossiping) + (stillVoting : (step config state event).state.phase = .voting) : + state.phase = .voting /\ + (step config state event).state.chosen = state.chosen := by + cases event <;> + simp [step, rejected, advance, advanceTimeoutLane] at stillVoting ⊢ + all_goals repeat first | split at stillVoting | split | simp_all + +lemma step_preserves_voting_selection + (config : Model.Config) + (state : NodeState) + (event : Event) + (before : + state.phase = .voting -> + NodeVotingSelection state) + (voting : (step config state event).state.phase = .voting) : + NodeVotingSelection (step config state event).state := by + cases event + all_goals try cases_type Validation + all_goals + simp [NodeVotingSelection, step, rejected, advance, + advanceTimeoutLane, validTimeout] at before voting ⊢ + all_goals + repeat first | split at voting | split | simp_all | aesop + +lemma retry_vote_state + {config : Config} + {envelope : Envelope} + (valid : envelope.Valid config) + (vote : envelope.payload = .vote) : + envelope.sourceState.phase = .voting /\ + envelope.sourceState.chosen = some envelope.target := by + rcases valid_envelope_effect valid with + ⟨effect, member, created⟩ + cases effect with + | sendGossip target => + cases found : recoveredTxID config envelope.source with + | none => + simp [messageForEffect, found] at created + | some txid => + simp [messageForEffect, found] at created + rw [←created] at vote + contradiction + | sendVote target => + simp [messageForEffect] at created + rw [←created] at vote ⊢ + cases phase : envelope.sourceState.phase <;> + simp [step, phase] at member + next => + cases chosen : envelope.sourceState.chosen <;> + simp_all + | sendIAmOpen target => + simp [messageForEffect] at created + rw [←created] at vote + contradiction + | opening kind => + simp [messageForEffect] at created + | restart chosen => + simp [messageForEffect] at created + | completed => + simp [messageForEffect] at created + | rejected reason => + simp [messageForEffect] at created + +lemma opening_effect_state + (config : Model.Config) + (state : NodeState) + (event : Event) + (kind : OpenKind) + (opening : .opening kind ∈ (step config state event).effects) : + (step config state event).state.phase = .opening /\ + (step config state event).state.openKind = some kind := by + cases event + all_goals try cases_type Validation + all_goals + simp [step, rejected, advance, advanceTimeoutLane, validTimeout] + at opening ⊢ + all_goals + repeat first | split at opening | split | simp_all | aesop + +lemma quorum_effect_has_threshold + (config : Model.Config) + (state : NodeState) + (event : Event) + (opening : + .opening .quorum ∈ (step config state event).effects) : + voteQuorum config <= + (step config state event).state.votes.length := by + cases event + all_goals try cases_type Validation + all_goals + simp [step, rejected, advance, advanceTimeoutLane, validTimeout] + at opening ⊢ + all_goals + repeat first | split at opening | split | simp_all | aesop + +lemma sentVote_mono + {before after : State} + {voter target : Location} + (sent : forall envelope, envelope ∈ before.sent -> + envelope ∈ after.sent) + (vote : SentVote before voter target) : + SentVote after voter target := by + rcases vote with + ⟨envelope, membership, source, destination, payload⟩ + exact + ⟨envelope, sent envelope membership, source, destination, payload⟩ + +lemma opening_valid_of_sent_eq + {config : Config} + {before after : State} + {opening : Opening} + (sentEq : after.sent = before.sent) + (valid : Opening.Valid config before opening) : + Opening.Valid config after opening := by + rcases valid with + ⟨location, phase, kind, nodup, quorum, votesSent⟩ + constructor + · exact location + · exact phase + · exact kind + · exact nodup + · exact quorum + · intro voter membership + apply sentVote_mono + · intro envelope sent + rw [sentEq] + exact sent + · exact votesSent voter membership + +lemma opening_valid_mono + {config : Config} + {before after : State} + {opening : Opening} + (sent : + forall envelope, envelope ∈ before.sent -> + envelope ∈ after.sent) + (valid : Opening.Valid config before opening) : + Opening.Valid config after opening := by + rcases valid with + ⟨location, phase, kind, nodup, quorum, votesSent⟩ + constructor + · exact location + · exact phase + · exact kind + · exact nodup + · exact quorum + · intro voter membership + exact sentVote_mono sent (votesSent voter membership) + +lemma recordEffect_preserves_openings_valid + {config : Config} + {node : Location} + {nodeState : NodeState} + {state : State} + {effect : Effect} + (valid : OpeningsValid config state) + (newValid : + forall kind, + effect = .opening kind -> + Opening.Valid config state + { node, kind, state := nodeState }) : + OpeningsValid config + (recordEffect node nodeState state effect) := by + intro opening membership + cases effect with + | opening kind => + simp [recordEffect] at membership + rcases membership with rfl | old + · apply opening_valid_of_sent_eq + (before := state) + (after := recordEffect node nodeState state (.opening kind)) + rfl + exact newValid kind rfl + · apply opening_valid_of_sent_eq + (before := state) + (after := recordEffect node nodeState state (.opening kind)) + rfl + exact valid opening old + | sendGossip target => + exact valid opening membership + | sendVote target => + exact valid opening membership + | sendIAmOpen target => + exact valid opening membership + | restart target => + apply opening_valid_of_sent_eq + (before := state) + (after := recordEffect node nodeState state (.restart target)) + rfl + exact valid opening membership + | completed => + apply opening_valid_of_sent_eq + (before := state) + (after := recordEffect node nodeState state .completed) + rfl + exact valid opening membership + | rejected reason => + exact valid opening membership + +lemma recordEffects_preserves_openings_valid + {config : Config} + {node : Location} + {nodeState : NodeState} + {state : State} + {effects : List Effect} + (valid : OpeningsValid config state) + (newValid : + forall kind, + .opening kind ∈ effects -> + Opening.Valid config state + { node, kind, state := nodeState }) : + OpeningsValid config + (recordEffects node nodeState effects state) := by + induction effects generalizing state with + | nil => exact valid + | cons effect tail ih => + simp only [recordEffects, List.foldl_cons] + apply ih + · apply recordEffect_preserves_openings_valid valid + intro kind effectEq + subst effect + exact newValid kind (by simp) + · intro kind membership + apply opening_valid_of_sent_eq + (before := state) + (after := recordEffect node nodeState state effect) + (by cases effect <;> rfl) + exact newValid kind (by simp [membership]) + +lemma eventFor_vote_source + {envelope : Envelope} + {voter : Location} + (source : + acceptedVoteSource (eventFor envelope) = some voter) : + envelope.payload = .vote /\ + envelope.source = voter := by + cases payload : envelope.payload <;> + simp_all [eventFor, acceptedVoteSource] + +lemma systemStep_preserves_votes_nodup + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (nodup : + forall entry, entry ∈ before.nodes -> + entry.2.votes.Nodup) + (transition : + systemStep config before target event = some (after, output)) : + forall entry, entry ∈ after.nodes -> + entry.2.votes.Nodup := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, stateEq, _⟩ + rw [←stateEq] + intro entry membership + rw [replaceNode, List.mem_map] at membership + rcases membership with ⟨previous, previousMember, rfl⟩ + split + · apply step_preserves_votes_nodup + exact nodup (key, node) (List.mem_of_find?_eq_some found) + · exact nodup previous previousMember + +lemma systemStep_preserves_voting_selections + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (valid : + forall entry, entry ∈ before.nodes -> + entry.2.phase = .voting -> + NodeVotingSelection entry.2) + (transition : + systemStep config before target event = some (after, output)) : + forall entry, entry ∈ after.nodes -> + entry.2.phase = .voting -> + NodeVotingSelection entry.2 := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, systemEq, outputEq⟩ + rw [←systemEq] + intro entry membership voting + rw [replaceNode, List.mem_map] at membership + rcases membership with ⟨previous, previousMember, rfl⟩ + split + · rename_i atTarget + apply step_preserves_voting_selection config node event + · exact valid (key, node) + (List.mem_of_find?_eq_some found) + · simpa [atTarget, outputEq] using voting + · rename_i notTarget + exact valid previous previousMember + (by simpa [notTarget] using voting) + +lemma systemStep_output_location + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (locations : + forall entry, entry ∈ before.nodes -> + entry.2.location = entry.1) + (transition : + systemStep config before target event = some (after, output)) : + output.state.location = target := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, _, outputEq⟩ + calc + output.state.location = + node.location := by + rw [←outputEq] + exact step_preserves_location config node event + _ = key := + locations (key, node) (List.mem_of_find?_eq_some found) + _ = target := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == target) found) + +lemma systemStep_output_mem + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (transition : + systemStep config before target event = some (after, output)) : + (target, output.state) ∈ after.nodes := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, systemEq, outputEq⟩ + rw [←systemEq, replaceNode, List.mem_map] + refine ⟨(key, node), List.mem_of_find?_eq_some found, ?_⟩ + have keyEq : key = target := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == target) found) + simp [keyEq, outputEq] + +lemma systemStep_opening_effect_state + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + {kind : OpenKind} + (transition : + systemStep config before target event = some (after, output)) + (opening : .opening kind ∈ output.effects) : + output.state.phase = .opening /\ + output.state.openKind = some kind := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, _, _, outputEq⟩ + rw [←outputEq] at opening ⊢ + exact opening_effect_state config node event kind opening + +lemma systemStep_quorum_effect_has_threshold + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + (transition : + systemStep config before target event = some (after, output)) + (opening : .opening .quorum ∈ output.effects) : + voteQuorum config <= output.state.votes.length := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, _, _, outputEq⟩ + rw [←outputEq] at opening ⊢ + exact quorum_effect_has_threshold config node event opening + +lemma initial_node_votes_nodup + (config : Config) + (active : List Location) : + NodeVotesNodup (initial config active) := by + simp [NodeVotesNodup, Global.initial, initialSystem, initialNode] + +lemma initial_node_votes_sent + (config : Config) + (active : List Location) : + NodeVotesSent (initial config active) := by + simp [NodeVotesSent, Global.initial, initialSystem, initialNode] + +lemma initial_sent_votes_functional + (config : Config) + (active : List Location) : + SentVotesFunctional (initial config active) := by + simp [SentVotesFunctional, SentVote, Global.initial] + +lemma initial_sent_vote_stable + (config : Config) + (active : List Location) : + SentVoteStable (initial config active) := by + simp [SentVoteStable, Global.initial] + +lemma initial_voting_selections + (config : Config) + (active : List Location) : + VotingSelectionsValid (initial config active) := by + simp [VotingSelectionsValid, Global.initial, initialSystem, initialNode] + +lemma initial_sent_votes_selected + (config : Config) + (active : List Location) : + SentVotesSelected (initial config active) := by + simp [SentVotesSelected, Global.initial] + +lemma initial_openings_valid + (config : Config) + (active : List Location) : + OpeningsValid config (initial config active) := by + simp [OpeningsValid, Global.initial] + +lemma systemStep_preserves_node_votes_sent + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + {beforeState afterState : State} + (beforeSystem : beforeState.system = before) + (votesSent : NodeVotesSent beforeState) + (carry : + forall voter destination, + SentVote beforeState voter destination -> + SentVote afterState voter destination) + (introduced : + forall voter, + acceptedVoteSource event = some voter -> + SentVote afterState voter target) + (transition : + systemStep config before target event = some (after, output)) : + forall entry, entry ∈ after.nodes -> + forall voter, voter ∈ entry.2.votes -> + SentVote afterState voter entry.1 := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, systemEq, outputEq⟩ + rw [←systemEq] + intro entry membership voter vote + rw [replaceNode, List.mem_map] at membership + rcases membership with ⟨previous, previousMember, rfl⟩ + split + · rename_i atTarget + have targetEq : previous.1 = target := + beq_iff_eq.mp atTarget + rcases step_vote_origin config node event voter + (by simpa [outputEq, atTarget] using vote) with + old | added + · have keyEq : key = target := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == target) found) + apply carry + rw [←keyEq] + exact votesSent (key, node) + (by + rw [beforeSystem] + exact List.mem_of_find?_eq_some found) + voter old + · exact introduced voter added + · rename_i notTarget + apply carry + exact votesSent previous + (by + rw [beforeSystem] + exact previousMember) + voter (by simpa [notTarget] using vote) + +lemma eq_of_key_eq + {α : Type} + {nodes : List (Prod Location α)} + (nodup : (nodes.map Prod.fst).Nodup) + {first second : Prod Location α} + (firstMember : first ∈ nodes) + (secondMember : second ∈ nodes) + (keyEq : first.1 = second.1) : + first = second := by + induction nodes generalizing first second with + | nil => simp at firstMember + | cons head tail ih => + rw [List.map_cons, List.nodup_cons] at nodup + rcases nodup with ⟨headFresh, tailNodup⟩ + rw [List.mem_cons] at firstMember secondMember + rcases firstMember with rfl | firstTail + · rcases secondMember with rfl | secondTail + · rfl + · exfalso + apply headFresh + rw [List.mem_map] + exact ⟨second, secondTail, keyEq.symm⟩ + · rcases secondMember with rfl | secondTail + · exfalso + apply headFresh + rw [List.mem_map] + exact ⟨first, firstTail, keyEq⟩ + · exact ih tailNodup firstTail secondTail keyEq + +lemma systemStep_preserves_vote_stability + {config : Model.Config} + {before after : SystemState} + {target : Location} + {event : Event} + {output : StepOutput} + {envelope : Envelope} + (stable : + forall entry, entry ∈ before.nodes -> + entry.1 = envelope.source -> + entry.2.phase ≠ .gossiping /\ + (entry.2.phase = .voting -> + entry.2.chosen = some envelope.target)) + (transition : + systemStep config before target event = some (after, output)) : + forall entry, entry ∈ after.nodes -> + entry.1 = envelope.source -> + entry.2.phase ≠ .gossiping /\ + (entry.2.phase = .voting -> + entry.2.chosen = some envelope.target) := by + simp [systemStep, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨node, ⟨key, found⟩, systemEq, outputEq⟩ + rw [←systemEq] + intro entry membership sourceEq + rw [replaceNode, List.mem_map] at membership + rcases membership with ⟨previous, previousMember, rfl⟩ + split + · rename_i atTarget + have targetEq : previous.1 = target := + beq_iff_eq.mp atTarget + have targetSource : target = envelope.source := by + simpa [atTarget] using sourceEq + have keyEq : key = target := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == target) found) + have beforeStable := + stable (key, node) (List.mem_of_find?_eq_some found) + (keyEq.trans targetSource) + constructor + · exact step_preserves_non_gossiping config node event + beforeStable.1 + · intro voting + rcases voting_step_preserves_choice config node event + beforeStable.1 voting with ⟨beforeVoting, chosenEq⟩ + rw [chosenEq] + exact beforeStable.2 beforeVoting + · rename_i notTarget + exact stable previous previousMember + (by simpa [notTarget] using sourceEq) + +lemma next_preserves_node_votes_nodup + {config : Config} + {before after : State} + {action : Action} + (nodup : NodeVotesNodup before) + (transition : next config before action = some after) : + NodeVotesNodup after := by + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + exact nodup + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, systemStep, rfl⟩ + intro entry membership + rw [recordEffects_system] at membership + exact systemStep_preserves_votes_nodup nodup systemStep + entry membership + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, systemStep, _, rfl⟩ + intro entry membership + rw [recordEffects_system] at membership + exact systemStep_preserves_votes_nodup nodup systemStep + entry membership + +lemma next_preserves_voting_selections + {config : Config} + {before after : State} + {action : Action} + (valid : VotingSelectionsValid before) + (transition : next config before action = some after) : + VotingSelectionsValid after := by + cases action with + | retry source => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + exact valid + | deliver envelope => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, systemStep, rfl⟩ + intro entry membership voting + rw [recordEffects_system] at membership + exact systemStep_preserves_voting_selections valid systemStep + entry membership voting + | timeout target => + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, systemStep, _, rfl⟩ + intro entry membership voting + rw [recordEffects_system] at membership + exact systemStep_preserves_voting_selections valid systemStep + entry membership voting + +lemma retry_preserves_sent_votes_selected + {config : Config} + {before after : State} + {source : Location} + (wellFormed : WellFormed config before) + (votingSelections : VotingSelectionsValid before) + (selected : SentVotesSelected before) + (transition : next config before (.retry source) = some after) : + SentVotesSelected after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, sourceState, found, _, stateEq⟩ + have sourceLocation : sourceState.location = source := + nodeState_location wellFormed.nodeLocations found + rw [←stateEq] + intro envelope membership payload + rw [List.mem_append] at membership + rcases membership with old | added + · exact selected envelope old payload + · have valid : envelope.Valid config := + retryMessages_valid config source sourceState sourceLocation + envelope added + have voteState := retry_vote_state valid payload + have identity := retryMessages_source added + rw [identity.2] at voteState + rw [nodeState, Option.map_eq_some_iff] at found + rcases found with ⟨entry, findEq, stateEq⟩ + have sourceSelection := + votingSelections entry (List.mem_of_find?_eq_some findEq) + (by simpa [stateEq] using voteState.1) + simpa [identity.2, stateEq] using sourceSelection + +lemma deliver_preserves_sent_votes_selected + {config : Config} + {before after : State} + {envelope : Envelope} + (selected : SentVotesSelected before) + (transition : next config before (.deliver envelope) = some after) : + SentVotesSelected after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, stateEq⟩ + rw [←stateEq] + intro vote membership payload + rw [recordEffects_sent] at membership + exact selected vote membership payload + +lemma timeout_preserves_sent_votes_selected + {config : Config} + {before after : State} + {target : Location} + (selected : SentVotesSelected before) + (transition : next config before (.timeout target) = some after) : + SentVotesSelected after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, stateEq⟩ + rw [←stateEq] + intro vote membership payload + rw [recordEffects_sent] at membership + exact selected vote membership payload + +lemma retry_preserves_node_votes_sent + {config : Config} + {before after : State} + {source : Location} + (votesSent : NodeVotesSent before) + (transition : next config before (.retry source) = some after) : + NodeVotesSent after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, rfl⟩ + intro entry membership voter vote + apply sentVote_mono (before := before) + · intro envelope sent + exact List.mem_append_left _ sent + · exact votesSent entry membership voter vote + +lemma deliver_preserves_node_votes_sent + {config : Config} + {before after : State} + {envelope : Envelope} + (wellFormed : WellFormed config before) + (votesSent : NodeVotesSent before) + (transition : next config before (.deliver envelope) = some after) : + NodeVotesSent after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨inNetwork, _, system, output, systemStep, stateEq⟩ + rw [←stateEq] + intro entry membership voter vote + rw [recordEffects_system] at membership + let afterState := + recordEffects envelope.target output.state output.effects + { + before with + system + network := removeOne envelope before.network + } + have carry : + forall oldVoter oldTarget, + SentVote before oldVoter oldTarget -> + SentVote afterState oldVoter oldTarget := by + intro oldVoter oldTarget oldVote + apply sentVote_mono (before := before) (after := afterState) + · intro sent sentMember + simpa [afterState] using sentMember + · exact oldVote + have introducedVote : + forall newVoter, + acceptedVoteSource (eventFor envelope) = some newVoter -> + SentVote afterState newVoter envelope.target := by + intro newVoter introduced + rcases eventFor_vote_source introduced with + ⟨payload, source⟩ + subst newVoter + refine ⟨envelope, ?_, rfl, rfl, payload⟩ + simp [afterState] + exact wellFormed.networkSent envelope + inNetwork + exact systemStep_preserves_node_votes_sent + (before := before.system) + (after := system) + (beforeState := before) + (afterState := afterState) + rfl votesSent carry introducedVote systemStep + entry membership voter vote + +lemma timeout_preserves_node_votes_sent + {config : Config} + {before after : State} + {target : Location} + (votesSent : NodeVotesSent before) + (transition : next config before (.timeout target) = some after) : + NodeVotesSent after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, systemStep, _, stateEq⟩ + rw [←stateEq] + intro entry membership voter vote + rw [recordEffects_system] at membership + let afterState := + recordEffects target output.state output.effects + { before with system } + have carry : + forall oldVoter oldTarget, + SentVote before oldVoter oldTarget -> + SentVote afterState oldVoter oldTarget := by + intro oldVoter oldTarget oldVote + apply sentVote_mono (before := before) (after := afterState) + · intro sent sentMember + simpa [afterState] using sentMember + · exact oldVote + have introducedVote : + forall newVoter, + acceptedVoteSource Event.timeout = some newVoter -> + SentVote afterState newVoter target := by + intro newVoter introduced + simp [acceptedVoteSource] at introduced + exact systemStep_preserves_node_votes_sent + (before := before.system) + (after := system) + (beforeState := before) + (afterState := afterState) + rfl votesSent carry introducedVote systemStep + entry membership voter vote + +lemma retry_preserves_openings_valid + {config : Config} + {before after : State} + {source : Location} + (valid : OpeningsValid config before) + (transition : next config before (.retry source) = some after) : + OpeningsValid config after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with ⟨_, sourceState, _, _, stateEq⟩ + rw [←stateEq] + intro opening membership + apply opening_valid_mono + · intro envelope sent + exact List.mem_append_left _ sent + · exact valid opening membership + +lemma deliver_preserves_openings_valid + {config : Config} + {before after : State} + {envelope : Envelope} + (wellFormed : WellFormed config before) + (votesNodup : NodeVotesNodup before) + (votesSent : NodeVotesSent before) + (valid : OpeningsValid config before) + (transition : next config before (.deliver envelope) = some after) : + OpeningsValid config after := by + have afterNodup := + next_preserves_node_votes_nodup votesNodup transition + have afterVotesSent := + deliver_preserves_node_votes_sent wellFormed votesSent transition + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, systemStep, stateEq⟩ + rw [←stateEq] at afterNodup afterVotesSent ⊢ + let delivered : State := { + before with + system + network := removeOne envelope before.network + } + apply recordEffects_preserves_openings_valid + · intro opening membership + apply opening_valid_of_sent_eq + (before := before) (after := delivered) rfl + exact valid opening membership + · intro kind openingEffect + have effectState := + systemStep_opening_effect_state systemStep openingEffect + constructor + · exact systemStep_output_location + wellFormed.nodeLocations systemStep + · exact effectState.1 + · exact effectState.2 + · apply afterNodup (envelope.target, output.state) + rw [recordEffects_system] + exact systemStep_output_mem systemStep + · intro quorumKind + have kindEq : kind = .quorum := by simpa using quorumKind + rw [kindEq] at openingEffect + simpa using + systemStep_quorum_effect_has_threshold systemStep openingEffect + · intro voter vote + have sent := + afterVotesSent (envelope.target, output.state) + (by + rw [recordEffects_system] + exact systemStep_output_mem systemStep) + voter vote + simpa [SentVote, delivered] using sent + +lemma timeout_preserves_openings_valid + {config : Config} + {before after : State} + {target : Location} + (wellFormed : WellFormed config before) + (votesNodup : NodeVotesNodup before) + (votesSent : NodeVotesSent before) + (valid : OpeningsValid config before) + (transition : next config before (.timeout target) = some after) : + OpeningsValid config after := by + have afterNodup := + next_preserves_node_votes_nodup votesNodup transition + have afterVotesSent := + timeout_preserves_node_votes_sent votesSent transition + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, systemStep, _, stateEq⟩ + rw [←stateEq] at afterNodup afterVotesSent ⊢ + let timedOut : State := { before with system } + apply recordEffects_preserves_openings_valid + · intro opening membership + apply opening_valid_of_sent_eq + (before := before) (after := timedOut) rfl + exact valid opening membership + · intro kind openingEffect + have effectState := + systemStep_opening_effect_state systemStep openingEffect + constructor + · exact systemStep_output_location + wellFormed.nodeLocations systemStep + · exact effectState.1 + · exact effectState.2 + · apply afterNodup (target, output.state) + rw [recordEffects_system] + exact systemStep_output_mem systemStep + · intro quorumKind + have kindEq : kind = .quorum := by simpa using quorumKind + rw [kindEq] at openingEffect + simpa using + systemStep_quorum_effect_has_threshold systemStep openingEffect + · intro voter vote + have sent := + afterVotesSent (target, output.state) + (by + rw [recordEffects_system] + exact systemStep_output_mem systemStep) + voter vote + simpa [SentVote, timedOut] using sent + +lemma retry_preserves_sent_vote_stable + {config : Config} + {before after : State} + {source : Location} + (wellFormed : WellFormed config before) + (stable : SentVoteStable before) + (transition : next config before (.retry source) = some after) : + SentVoteStable after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, sourceState, found, _, stateEq⟩ + have sourceLocation : sourceState.location = source := + nodeState_location wellFormed.nodeLocations found + rw [←stateEq] + intro envelope membership payload entry entryMember keyEq + rw [List.mem_append] at membership + rcases membership with old | added + · exact stable envelope old payload entry entryMember keyEq + · have valid : envelope.Valid config := + retryMessages_valid config source sourceState sourceLocation + envelope added + have voteState := retry_vote_state valid payload + rcases retryMessages_source added with + ⟨sourceEq, stateEq⟩ + rw [nodeState, Option.map_eq_some_iff] at found + rcases found with ⟨foundEntry, findEq, foundStateEq⟩ + have foundMember : foundEntry ∈ before.system.nodes := + List.mem_of_find?_eq_some findEq + have foundKey : foundEntry.1 = source := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == source) findEq) + have sameEntry : entry = foundEntry := + eq_of_key_eq wellFormed.nodeKeysNodup entryMember foundMember + ((keyEq.trans sourceEq).trans foundKey.symm) + subst entry + rw [foundStateEq, ←stateEq] + exact ⟨by simp [voteState.1], fun _ => voteState.2⟩ + +lemma deliver_preserves_sent_vote_stable + {config : Config} + {before after : State} + {delivered : Envelope} + (stable : SentVoteStable before) + (transition : next config before (.deliver delivered) = some after) : + SentVoteStable after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, systemStep, stateEq⟩ + rw [←stateEq] + intro envelope membership payload entry entryMember keyEq + rw [recordEffects_sent] at membership + rw [recordEffects_system] at entryMember + exact systemStep_preserves_vote_stability + (fun previous previousMember source => + stable envelope membership payload previous previousMember source) + systemStep entry entryMember keyEq + +lemma timeout_preserves_sent_vote_stable + {config : Config} + {before after : State} + {target : Location} + (stable : SentVoteStable before) + (transition : next config before (.timeout target) = some after) : + SentVoteStable after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, systemStep, _, stateEq⟩ + rw [←stateEq] + intro envelope membership payload entry entryMember keyEq + rw [recordEffects_sent] at membership + rw [recordEffects_system] at entryMember + exact systemStep_preserves_vote_stability + (fun previous previousMember source => + stable envelope membership payload previous previousMember source) + systemStep entry entryMember keyEq + +lemma sentVote_stable_at_node + {state : State} + {voter target : Location} + {current : NodeState} + (stable : SentVoteStable state) + (vote : SentVote state voter target) + (found : nodeState state voter = some current) : + current.phase ≠ .gossiping /\ + (current.phase = .voting -> + current.chosen = some target) := by + rcases vote with + ⟨envelope, sent, sourceEq, targetEq, payload⟩ + rw [nodeState, Option.map_eq_some_iff] at found + rcases found with ⟨entry, findEq, stateEq⟩ + have entryMember : entry ∈ state.system.nodes := + List.mem_of_find?_eq_some findEq + have entryKey : entry.1 = voter := + beq_iff_eq.mp + (List.find?_some + (p := fun entry : Prod Location NodeState => + entry.1 == voter) findEq) + have result := + stable envelope sent payload entry entryMember + (entryKey.trans sourceEq.symm) + rw [stateEq] at result + simpa [targetEq] using result + +lemma retry_preserves_sent_votes_functional + {config : Config} + {before after : State} + {source : Location} + (wellFormed : WellFormed config before) + (functional : SentVotesFunctional before) + (stable : SentVoteStable before) + (transition : next config before (.retry source) = some after) : + SentVotesFunctional after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, sourceState, found, _, stateEq⟩ + have sourceLocation : sourceState.location = source := + nodeState_location wellFormed.nodeLocations found + rw [←stateEq] + have classify : + forall voter target, + SentVote + { + before with + network := before.network ++ + retryMessages config source sourceState + sent := before.sent ++ + retryMessages config source sourceState + } + voter target -> + SentVote before voter target \/ + (voter = source /\ + sourceState.phase = .voting /\ + sourceState.chosen = some target) := by + intro voter target vote + rcases vote with + ⟨envelope, membership, sourceEq, targetEq, payload⟩ + rw [List.mem_append] at membership + rcases membership with old | added + · exact Or.inl + ⟨envelope, old, sourceEq, targetEq, payload⟩ + · have valid : envelope.Valid config := + retryMessages_valid config source sourceState sourceLocation + envelope added + have voteState := retry_vote_state valid payload + have retryIdentity := retryMessages_source added + rw [retryIdentity.2] at voteState + exact Or.inr + ⟨sourceEq.symm.trans retryIdentity.1, + voteState.1, + by simpa [targetEq] using voteState.2⟩ + intro voter first second firstVote secondVote + rcases classify voter first firstVote with + firstOld | ⟨firstSource, firstPhase, firstChoice⟩ + · rcases classify voter second secondVote with + secondOld | ⟨secondSource, secondPhase, secondChoice⟩ + · exact functional voter first second firstOld secondOld + · have oldState := + sentVote_stable_at_node stable firstOld + (by simpa [secondSource] using found) + have oldChoice := oldState.2 secondPhase + rw [oldChoice] at secondChoice + exact Option.some.inj secondChoice + · rcases classify voter second secondVote with + secondOld | ⟨secondSource, secondPhase, secondChoice⟩ + · have oldState := + sentVote_stable_at_node stable secondOld + (by simpa [firstSource] using found) + have oldChoice := oldState.2 firstPhase + rw [oldChoice] at firstChoice + exact (Option.some.inj firstChoice).symm + · rw [firstChoice] at secondChoice + exact Option.some.inj secondChoice + +lemma deliver_preserves_sent_votes_functional + {config : Config} + {before after : State} + {envelope : Envelope} + (functional : SentVotesFunctional before) + (transition : next config before (.deliver envelope) = some after) : + SentVotesFunctional after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, _, system, output, _, stateEq⟩ + rw [←stateEq] + intro voter first second firstVote secondVote + apply functional voter first second + · simpa [SentVote] using firstVote + · simpa [SentVote] using secondVote + +lemma timeout_preserves_sent_votes_functional + {config : Config} + {before after : State} + {target : Location} + (functional : SentVotesFunctional before) + (transition : next config before (.timeout target) = some after) : + SentVotesFunctional after := by + simp [next, Option.bind_eq_some_iff] at transition + rcases transition with + ⟨_, system, output, _, _, stateEq⟩ + rw [←stateEq] + intro voter first second firstVote secondVote + apply functional voter first second + · simpa [SentVote] using firstVote + · simpa [SentVote] using secondVote + +lemma initial_quorum_invariant + (config : Config) + (active : List Location) : + QuorumInvariant config (initial config active) := { + votesNodup := initial_node_votes_nodup config active + votesSent := initial_node_votes_sent config active + sentVoteStable := initial_sent_vote_stable config active + sentVotesFunctional := initial_sent_votes_functional config active + votingSelections := initial_voting_selections config active + sentVotesSelected := initial_sent_votes_selected config active + openingsValid := initial_openings_valid config active +} + +lemma next_preserves_quorum_invariant + {config : Config} + {before after : State} + {action : Action} + (wellFormed : WellFormed config before) + (invariant : QuorumInvariant config before) + (transition : next config before action = some after) : + QuorumInvariant config after := by + cases action with + | retry source => + constructor + · exact next_preserves_node_votes_nodup + invariant.votesNodup transition + · exact retry_preserves_node_votes_sent + invariant.votesSent transition + · exact retry_preserves_sent_vote_stable + wellFormed invariant.sentVoteStable transition + · exact retry_preserves_sent_votes_functional + wellFormed invariant.sentVotesFunctional + invariant.sentVoteStable transition + · exact next_preserves_voting_selections + invariant.votingSelections transition + · exact retry_preserves_sent_votes_selected + wellFormed invariant.votingSelections + invariant.sentVotesSelected transition + · exact retry_preserves_openings_valid + invariant.openingsValid transition + | deliver envelope => + constructor + · exact next_preserves_node_votes_nodup + invariant.votesNodup transition + · exact deliver_preserves_node_votes_sent + wellFormed invariant.votesSent transition + · exact deliver_preserves_sent_vote_stable + invariant.sentVoteStable transition + · exact deliver_preserves_sent_votes_functional + invariant.sentVotesFunctional transition + · exact next_preserves_voting_selections + invariant.votingSelections transition + · exact deliver_preserves_sent_votes_selected + invariant.sentVotesSelected transition + · exact deliver_preserves_openings_valid + wellFormed invariant.votesNodup invariant.votesSent + invariant.openingsValid transition + | timeout target => + constructor + · exact next_preserves_node_votes_nodup + invariant.votesNodup transition + · exact timeout_preserves_node_votes_sent + invariant.votesSent transition + · exact timeout_preserves_sent_vote_stable + invariant.sentVoteStable transition + · exact timeout_preserves_sent_votes_functional + invariant.sentVotesFunctional transition + · exact next_preserves_voting_selections + invariant.votingSelections transition + · exact timeout_preserves_sent_votes_selected + invariant.sentVotesSelected transition + · exact timeout_preserves_openings_valid + wellFormed invariant.votesNodup invariant.votesSent + invariant.openingsValid transition + +lemma reachable_quorum_invariant + {config : Config} + {state : State} + (reachable : Reachable config state) : + QuorumInvariant config state := by + induction reachable with + | initial active valid nodup configured => + exact initial_quorum_invariant config active + | step reachable transition invariant => + exact next_preserves_quorum_invariant + (reachable_well_formed reachable) invariant transition + +lemma quorum_lists_intersect + {α : Type} + [DecidableEq α] + (expected first second : List α) + (firstNodup : first.Nodup) + (secondNodup : second.Nodup) + (firstSubset : + forall value, value ∈ first -> value ∈ expected) + (secondSubset : + forall value, value ∈ second -> value ∈ expected) + (firstQuorum : + expected.length / 2 + 1 <= first.length) + (secondQuorum : + expected.length / 2 + 1 <= second.length) : + exists value, value ∈ first /\ value ∈ second := by + by_contra noShared + push Not at noShared + have disjoint : Disjoint first.toFinset second.toFinset := + Finset.disjoint_left.mpr (by + intro value firstMember secondMember + exact noShared value + (List.mem_toFinset.mp firstMember) + (List.mem_toFinset.mp secondMember)) + have unionSubset : + first.toFinset ∪ second.toFinset ⊆ expected.toFinset := by + intro value membership + rw [Finset.mem_union] at membership + rw [List.mem_toFinset] + exact membership.elim + (fun member => + firstSubset value (List.mem_toFinset.mp member)) + (fun member => + secondSubset value (List.mem_toFinset.mp member)) + have unionCard := Finset.card_le_card unionSubset + rw [Finset.card_union_of_disjoint disjoint, + List.toFinset_card_of_nodup firstNodup, + List.toFinset_card_of_nodup secondNodup] at unionCard + have expectedCard := List.toFinset_card_le expected + omega + +lemma opening_vote_configured + {config : Config} + {state : State} + {opening : Opening} + (wellFormed : WellFormed config state) + (valid : Opening.Valid config state opening) + {voter : Location} + (vote : voter ∈ opening.state.votes) : + voter ∈ config.protocol.expectedLocations := by + rcases valid.votesSent voter vote with + ⟨envelope, sent, sourceEq, _, _⟩ + apply wellFormed.activeConfigured voter + simpa [sourceEq] using + wellFormed.sentSourceActive envelope sent + +lemma quorum_opener_unique + {config : Config} + {state : State} + {first second : Location} + (reachable : Reachable config state) + (firstOpened : QuorumOpened state first) + (secondOpened : QuorumOpened state second) : + first = second := by + have wellFormed := reachable_well_formed reachable + have invariant := reachable_quorum_invariant reachable + rcases firstOpened with + ⟨firstOpening, firstMember, firstNode, firstKind⟩ + rcases secondOpened with + ⟨secondOpening, secondMember, secondNode, secondKind⟩ + have firstValid := + invariant.openingsValid firstOpening firstMember + have secondValid := + invariant.openingsValid secondOpening secondMember + rcases quorum_lists_intersect + config.protocol.expectedLocations + firstOpening.state.votes + secondOpening.state.votes + firstValid.votesNodup + secondValid.votesNodup + (fun voter vote => + opening_vote_configured wellFormed firstValid vote) + (fun voter vote => + opening_vote_configured wellFormed secondValid vote) + (by + simpa [voteQuorum] using firstValid.quorum firstKind) + (by + simpa [voteQuorum] using secondValid.quorum secondKind) with + ⟨voter, firstVote, secondVote⟩ + have targetEq := + invariant.sentVotesFunctional voter + firstOpening.node secondOpening.node + (firstValid.votesSent voter firstVote) + (secondValid.votesSent voter secondVote) + exact firstNode.symm.trans (targetEq.trans secondNode) + +end DisasterRecovery.Proofs.Quorum diff --git a/lean/disaster-recovery/DisasterRecovery/Properties.lean b/lean/disaster-recovery/DisasterRecovery/Properties.lean new file mode 100644 index 000000000000..90fc5c171970 --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Properties.lean @@ -0,0 +1,134 @@ +import DisasterRecovery.Proofs.Committed +import DisasterRecovery.Proofs.Invariants +import DisasterRecovery.Proofs.Model +import DisasterRecovery.Proofs.Quorum + +/-! +# Human-reviewed system properties + +Review these statements together with the definitions and assumptions in +`DisasterRecovery.Protocol`. Each theorem explicitly applies a machine-checked +lemma from `DisasterRecovery.Proofs`; changing a statement must preserve that +checked connection. Intermediate facts remain lemmas in the proof modules. +-/ + +namespace DisasterRecovery.Properties + +section Local + +open Protocol.Model + +/-! ## Local safety -/ + +theorem gossip_freezes_after_choice + (config : Config) + (state : NodeState) + (source : Location) + (txid : TxID) + (chosen : state.chosen.isSome = true) : + let output := step config state (.receiveGossip source txid .accepted) + output.state = state /\ output.accepted = false := + Proofs.Model.gossip_freezes_after_choice config state source txid chosen + +theorem rejected_gossip_stutters + (config : Config) + (state : NodeState) + (source : Location) + (txid : TxID) : + let output := step config state (.receiveGossip source txid .rejected) + output.state = state /\ output.accepted = false := + Proofs.Model.rejected_gossip_stutters config state source txid + +theorem quorum_advance_opens + (config : Config) + (state : NodeState) + (phase : state.phase = .voting) + (quorum : state.votes.length >= voteQuorum config) : + let output := (advance config state false).get! + output.state.phase = .opening /\ + output.state.openKind = some .quorum /\ + output.effects = [.opening .quorum] := + Proofs.Model.quorum_advance_opens config state phase quorum + +theorem aligned_opening_timeout_completes + (config : Config) + (state : NodeState) : + let opening := { + state with + phase := .opening + timeoutState := .opening + } + let output := step config opening .timeout + output.state.phase = .open /\ + output.state.timeoutState = .opening /\ + output.effects = [.completed] := + Proofs.Model.aligned_opening_timeout_completes config state + +end Local + +section Global + +open Protocol.Model hiding Config +open Protocol.Global Protocol.Invariants Protocol.Quorum Protocol.Committed + +/-! ## Reachability and quorum safety -/ + +theorem reachable_well_formed + {config : Config} + {state : State} + (reachable : Reachable config state) : + WellFormed config state := + Proofs.Invariants.reachable_well_formed reachable + +theorem reachable_quorum_invariant + {config : Config} + {state : State} + (reachable : Reachable config state) : + QuorumInvariant config state := + Proofs.Quorum.reachable_quorum_invariant reachable + +theorem quorum_opener_unique + {config : Config} + {state : State} + {first second : Location} + (reachable : Reachable config state) + (firstOpened : QuorumOpened state first) + (secondOpened : QuorumOpened state second) : + first = second := + Proofs.Quorum.quorum_opener_unique + reachable firstOpened secondOpened + +/-! ## Committed-prefix safety -/ + +theorem full_gossip_selection_preserves_commit + {config : Config} + {state : State} + {opener : Location} + {committed : TxID} + (reachable : Reachable config state) + (full : FullGossipSelection config state opener) + (durable : DurableCommit config committed) : + exists recovered, + recoveredTxID config opener = some recovered /\ + TxID.EarlierThan committed recovered := + Proofs.Committed.full_gossip_selection_preserves_commit + reachable full durable + +theorem quorum_open_preserves_commit + {config : Config} + {state : State} + {opener : Location} + {committed : TxID} + (reachable : Reachable config state) + (opened : QuorumOpened state opener) + (full : FullGossipSelection config state opener) + (durable : DurableCommit config committed) : + exists recovered, + recoveredTxID config opener = some recovered /\ + TxID.EarlierThan committed recovered := + Proofs.Committed.quorum_open_preserves_commit + reachable opened full durable + +end Global + +end DisasterRecovery.Properties diff --git a/lean/disaster-recovery/DisasterRecovery/Protocol/Committed.lean b/lean/disaster-recovery/DisasterRecovery/Protocol/Committed.lean new file mode 100644 index 000000000000..11ce44bd732b --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Protocol/Committed.lean @@ -0,0 +1,35 @@ +import DisasterRecovery.Protocol.Quorum + +/-! Human-reviewed committed-prefix ordering and completeness assumptions. -/ + +namespace DisasterRecovery.Protocol.Committed + +open Model hiding Config +open Global + +namespace TxID + +def EarlierThan (left right : TxID) : Prop := + left.view < right.view \/ + (left.view = right.view /\ left.seqno <= right.seqno) + +end TxID + +def FullGossipSelection + (config : Config) + (state : State) + (opener : Location) : Prop := + exists vote, + vote ∈ state.sent /\ + vote.payload = .vote /\ + vote.target = opener /\ + forall gossip, + gossip ∈ vote.sourceState.gossips <-> + gossip ∈ config.recovered + +def DurableCommit (config : Config) (committed : TxID) : Prop := + exists location txid, + (location, txid) ∈ config.recovered /\ + TxID.EarlierThan committed txid + +end DisasterRecovery.Protocol.Committed diff --git a/lean/disaster-recovery/DisasterRecovery/Protocol/Global.lean b/lean/disaster-recovery/DisasterRecovery/Protocol/Global.lean new file mode 100644 index 000000000000..0dd29c4ae4f3 --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Protocol/Global.lean @@ -0,0 +1,168 @@ +import DisasterRecovery.Protocol.Model + +namespace DisasterRecovery.Protocol.Global + +open Model + +structure Config where + protocol : Model.Config + recovered : List (Prod Location TxID) +deriving Repr, BEq + +def Config.Valid (config : Config) : Prop := + config.protocol.isValid = true /\ + config.protocol.expectedLocations.Nodup /\ + config.recovered.map Prod.fst = config.protocol.expectedLocations + +def recoveredTxID (config : Config) (source : Location) : Option TxID := + (config.recovered.find? fun entry => entry.1 == source).map Prod.snd + +inductive Payload where + | gossip (txid : TxID) + | vote + | iAmOpen +deriving Repr, BEq, ReflBEq, LawfulBEq + +structure Envelope where + source : Location + target : Location + payload : Payload + sourceState : NodeState +deriving Repr, BEq, ReflBEq, LawfulBEq + +structure Opening where + node : Location + kind : OpenKind + state : NodeState +deriving Repr, BEq + +structure State where + system : SystemState + active : List Location + network : List Envelope := [] + sent : List Envelope := [] + openings : List Opening := [] + restarts : List Location := [] + completed : List Location := [] +deriving Repr, BEq + +inductive Action where + | retry (source : Location) + | deliver (envelope : Envelope) + | timeout (target : Location) +deriving Repr, BEq + +def nodeState (state : State) (node : Location) : Option NodeState := + (state.system.nodes.find? fun entry => entry.1 == node).map Prod.snd + +def messageForEffect + (config : Config) + (source : Location) + (sourceState : NodeState) : Effect -> Option Envelope + | .sendGossip target => do + let txid <- recoveredTxID config source + pure { source, target, payload := .gossip txid, sourceState } + | .sendVote target => + some { source, target, payload := .vote, sourceState } + | .sendIAmOpen target => + some { source, target, payload := .iAmOpen, sourceState } + | _ => none + +def retryMessages + (config : Config) + (source : Location) + (sourceState : NodeState) : List Envelope := + (step config.protocol sourceState .retry).effects.filterMap + (messageForEffect config source sourceState) + +def Envelope.Valid (config : Config) (envelope : Envelope) : Prop := + envelope.sourceState.location = envelope.source /\ + envelope ∈ retryMessages config envelope.source envelope.sourceState + +def eventFor (envelope : Envelope) : Event := + match envelope.payload with + | .gossip txid => .receiveGossip envelope.source txid .accepted + | .vote => .receiveVote envelope.source .accepted + | .iAmOpen => .receiveIAmOpen envelope.source .accepted + +def removeOne [BEq α] (value : α) : List α -> List α + | [] => [] + | head :: tail => + if head == value then tail else head :: removeOne value tail + +def recordEffect + (node : Location) + (nodeState : NodeState) + (state : State) : Effect -> State + | .opening kind => + { + state with + openings := { node, kind, state := nodeState } :: state.openings + } + | .restart _ => + { state with restarts := node :: state.restarts } + | .completed => + { state with completed := node :: state.completed } + | _ => state + +def recordEffects + (node : Location) + (nodeState : NodeState) + (effects : List Effect) + (state : State) : State := + effects.foldl (recordEffect node nodeState) state + +def initial (config : Config) (active : List Location) : State := { + system := initialSystem config.protocol + active +} + +def next (config : Config) (state : State) : Action -> Option State + | .retry source => do + guard (state.active.contains source) + let sourceState <- nodeState state source + let messages := retryMessages config source sourceState + guard (!messages.isEmpty) + pure { + state with + network := state.network ++ messages + sent := state.sent ++ messages + } + | .deliver envelope => do + guard (state.network.contains envelope) + guard (state.active.contains envelope.target) + let (system, output) <- + systemStep config.protocol state.system envelope.target + (eventFor envelope) + let delivered := { + state with + system + network := removeOne envelope state.network + } + pure + (recordEffects envelope.target output.state output.effects delivered) + | .timeout target => do + guard (state.active.contains target) + let (system, output) <- + systemStep config.protocol state.system target .timeout + guard output.accepted + pure + (recordEffects target output.state output.effects { state with system }) + +inductive Reachable (config : Config) : State -> Prop where + | initial + (active : List Location) + (valid : config.Valid) + (nodup : active.Nodup) + (configured : + forall node, node ∈ active -> + node ∈ config.protocol.expectedLocations) : + Reachable config (Global.initial config active) + | step + {state nextState : State} + {action : Action} + (reachable : Reachable config state) + (transition : next config state action = some nextState) : + Reachable config nextState + +end DisasterRecovery.Protocol.Global diff --git a/lean/disaster-recovery/DisasterRecovery/Protocol/Invariants.lean b/lean/disaster-recovery/DisasterRecovery/Protocol/Invariants.lean new file mode 100644 index 000000000000..977084ed4e9a --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Protocol/Invariants.lean @@ -0,0 +1,44 @@ +import DisasterRecovery.Protocol.Global + +/-! Human-reviewed reachability and message-provenance invariants. -/ + +namespace DisasterRecovery.Protocol.Invariants + +open Model hiding Config +open Global + +structure HistoriesActive (state : State) : Prop where + openings : + forall opening, opening ∈ state.openings -> + opening.node ∈ state.active + restarts : + forall node, node ∈ state.restarts -> + node ∈ state.active + completed : + forall node, node ∈ state.completed -> + node ∈ state.active + +structure WellFormed (config : Config) (state : State) : Prop where + nodeKeys : + state.system.nodes.map Prod.fst = + config.protocol.expectedLocations + nodeKeysNodup : (state.system.nodes.map Prod.fst).Nodup + nodeLocations : + forall entry, entry ∈ state.system.nodes -> + entry.2.location = entry.1 + activeNodup : state.active.Nodup + activeConfigured : + forall node, node ∈ state.active -> + node ∈ config.protocol.expectedLocations + sentValid : + forall envelope, envelope ∈ state.sent -> + envelope.Valid config + sentSourceActive : + forall envelope, envelope ∈ state.sent -> + envelope.source ∈ state.active + networkSent : + forall envelope, envelope ∈ state.network -> + envelope ∈ state.sent + historiesActive : HistoriesActive state + +end DisasterRecovery.Protocol.Invariants diff --git a/lean/disaster-recovery/DisasterRecovery/Protocol/Model.lean b/lean/disaster-recovery/DisasterRecovery/Protocol/Model.lean new file mode 100644 index 000000000000..0565be759d16 --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Protocol/Model.lean @@ -0,0 +1,290 @@ +import Std + +namespace DisasterRecovery.Protocol.Model + +abbrev Location := String + +structure TxID where + view : Nat + seqno : Nat +deriving Repr, BEq, ReflBEq, LawfulBEq, Hashable, Inhabited, DecidableEq + +inductive Phase where + | gossiping + | voting + | opening + | joining + | open +deriving Repr, BEq, ReflBEq, LawfulBEq, Hashable, Inhabited, DecidableEq + +inductive OpenKind where + | quorum + | failover +deriving Repr, BEq, ReflBEq, LawfulBEq, Hashable, Inhabited, DecidableEq + +inductive Validation where + | accepted + | rejected +deriving Repr, BEq, Hashable, Inhabited, DecidableEq + +structure Config where + instanceId : String + expectedLocations : List Location +deriving Repr, BEq, Hashable, Inhabited + +def Config.isValid (config : Config) : Bool := + !config.instanceId.isEmpty && + !config.expectedLocations.isEmpty && + !config.expectedLocations.any String.isEmpty && + config.expectedLocations.eraseDups.length = + config.expectedLocations.length + +structure NodeState where + location : Location + phase : Phase := .gossiping + timeoutState : Phase := .gossiping + gossips : List (Prod Location TxID) := [] + votes : List Location := [] + chosen : Option Location := none + openKind : Option OpenKind := none + restartRequested : Bool := false +deriving Repr, BEq, ReflBEq, LawfulBEq, Hashable, Inhabited + +inductive Event where + | receiveGossip (source : Location) (txid : TxID) (validation : Validation) + | receiveVote (source : Location) (validation : Validation) + | receiveIAmOpen (source : Location) (validation : Validation) + | timeout + | retry +deriving Repr, BEq, Hashable + +inductive Effect where + | sendGossip (destination : Location) + | sendVote (destination : Location) + | sendIAmOpen (destination : Location) + | opening (kind : OpenKind) + | restart (chosen : Location) + | completed + | rejected (reason : String) +deriving Repr, BEq, Hashable + +structure StepOutput where + state : NodeState + effects : List Effect := [] + accepted : Bool := true +deriving Repr, BEq, Inhabited + +structure SystemState where + nodes : List (Prod Location NodeState) +deriving Repr, BEq, Hashable, Inhabited + +def phaseName : Phase -> String + | .gossiping => "GOSSIPING" + | .voting => "VOTING" + | .opening => "OPENING" + | .joining => "JOINING" + | .open => "OPEN" + +def openKindName : OpenKind -> String + | .quorum => "QUORUM" + | .failover => "FAILOVER" + +def initialNode (location : Location) : NodeState := + { location } + +def initialSystem (config : Config) : SystemState := + { nodes := config.expectedLocations.map fun location => + (location, initialNode location) } + +def voteQuorum (config : Config) : Nat := + config.expectedLocations.length / 2 + 1 + +def validTimeout (state : NodeState) (timeout : Bool) : Bool := + timeout && decide (state.phase = state.timeoutState) + +def txScoreGreater + (leftName : Location) + (left : TxID) + (rightName : Location) + (right : TxID) : Bool := + right.view < left.view || + (right.view == left.view && + (right.seqno < left.seqno || + (right.seqno == left.seqno && rightName < leftName))) + +def selectMaximum + (current candidate : Prod Location TxID) : + Prod Location TxID := + if txScoreGreater candidate.1 candidate.2 current.1 current.2 then + candidate + else + current + +def maximumGossip : List (Prod Location TxID) -> Option (Prod Location TxID) + | [] => none + | head :: tail => + some (tail.foldl selectMaximum head) + +def insertGossip + (source : Location) + (txid : TxID) + (gossips : List (Prod Location TxID)) : + List (Prod Location TxID) := + if gossips.any (fun entry => entry.1 == source) then + gossips + else + ((source, txid) :: gossips).mergeSort (fun left right => left.1 <= right.1) + +def insertVote (source : Location) (votes : List Location) : List Location := + if votes.contains source then votes + else (source :: votes).mergeSort (fun left right => left <= right) + +def advanceTimeoutState : Phase -> Phase + | .gossiping => .voting + | .voting => .opening + | state => state + +def advanceTimeoutLane (state : NodeState) (timeout : Bool) : NodeState := + if timeout then + { state with timeoutState := advanceTimeoutState state.timeoutState } + else + state + +def advance (config : Config) (state : NodeState) (timeout : Bool) : + Option StepOutput := + let aligned := validTimeout state timeout + match state.phase with + | .gossiping => + if decide (state.gossips.length >= config.expectedLocations.length) || aligned then + match maximumGossip state.gossips with + | none => none + | some (chosen, _) => + let next := { state with phase := .voting, chosen := some chosen } + some { state := advanceTimeoutLane next timeout } + else + some { state := advanceTimeoutLane state timeout } + | .voting => + let sufficient := decide (state.votes.length >= voteQuorum config) + if sufficient || aligned then + if aligned && state.votes.isEmpty then + some { state } + else + let kind := if aligned && !sufficient then .failover else .quorum + let next := { + state with + phase := .opening + openKind := some kind + } + some { + state := advanceTimeoutLane next timeout + effects := [.opening kind] + } + else + some { state := advanceTimeoutLane state timeout } + | .joining => + match state.chosen with + | none => none + | some chosen => + some { + state := advanceTimeoutLane + { state with restartRequested := true } timeout + effects := [.restart chosen] + } + | .opening => + if aligned then + some { + state := advanceTimeoutLane { state with phase := .open } timeout + effects := [.completed] + } + else + some { state := advanceTimeoutLane state timeout } + | .open => + some { state := advanceTimeoutLane state timeout } + +def rejected (state : NodeState) (reason : String) : StepOutput := + { state, effects := [.rejected reason], accepted := false } + +def step (config : Config) (state : NodeState) : Event -> StepOutput + | .receiveGossip source txid validation => + match validation with + | .rejected => rejected state "quote-or-certificate" + | .accepted => + if state.chosen != none then + rejected state "gossip-frozen" + else + let received := { state with + gossips := insertGossip source txid state.gossips } + (advance config received false).getD + (rejected state "empty-gossip-advance") + | .receiveVote source validation => + match validation with + | .rejected => rejected state "quote-or-certificate" + | .accepted => + let received := { state with votes := insertVote source state.votes } + (advance config received false).getD + (rejected state "vote-advance") + | .receiveIAmOpen source validation => + match validation with + | .rejected => rejected state "quote-or-certificate" + | .accepted => + match state.phase with + | .opening | .open => + rejected state "already-opening-or-open" + | _ => + let received := { + state with + phase := .joining + chosen := some source + } + (advance config received false).getD + (rejected state "join-without-chosen") + | .timeout => + (advance config state true).getD + (rejected state "empty-gossip-timeout-aborts") + | .retry => + let effects := + match state.phase with + | .gossiping => + config.expectedLocations.map .sendGossip + | .voting => + match state.chosen with + | none => config.expectedLocations.map .sendGossip + | some chosen => + .sendVote chosen :: config.expectedLocations.map .sendGossip + | .opening => + (config.expectedLocations.filter + (fun location => location != state.location)).map .sendIAmOpen + | .joining | .open => [] + { state, effects } + +def replaceNode + (target : Location) + (next : NodeState) + (nodes : List (Prod Location NodeState)) : + List (Prod Location NodeState) := + nodes.map fun entry => if entry.1 == target then (target, next) else entry + +def systemStep + (config : Config) + (state : SystemState) + (target : Location) + (event : Event) : + Option (Prod SystemState StepOutput) := do + let node <- (state.nodes.find? fun entry => entry.1 == target).map Prod.snd + let output := step config node event + pure ({ + nodes := replaceNode target output.state state.nodes + }, output) + +def expectedSource (config : Config) (source : Location) : Bool := + config.expectedLocations.contains source + +def stateKey (state : NodeState) : String := + let gossips := String.intercalate "," (state.gossips.map fun entry => + s!"{entry.1}@{entry.2.view}.{entry.2.seqno}") + let votes := String.intercalate "," state.votes + let chosen := state.chosen.getD "-" + let kind := state.openKind.map openKindName |>.getD "-" + s!"{state.location}|{phaseName state.phase}|{phaseName state.timeoutState}|g={gossips}|v={votes}|c={chosen}|k={kind}|r={state.restartRequested}" + +end DisasterRecovery.Protocol.Model diff --git a/lean/disaster-recovery/DisasterRecovery/Protocol/Quorum.lean b/lean/disaster-recovery/DisasterRecovery/Protocol/Quorum.lean new file mode 100644 index 000000000000..80683f4e858f --- /dev/null +++ b/lean/disaster-recovery/DisasterRecovery/Protocol/Quorum.lean @@ -0,0 +1,94 @@ +import DisasterRecovery.Protocol.Invariants + +/-! Human-reviewed vote provenance, quorum and opening predicates. -/ + +namespace DisasterRecovery.Protocol.Quorum + +open Model hiding Config +open Global + +def SentVote (state : State) (voter target : Location) : Prop := + exists envelope, + envelope ∈ state.sent /\ + envelope.source = voter /\ + envelope.target = target /\ + envelope.payload = .vote + +def NodeVotesNodup (state : State) : Prop := + forall entry, entry ∈ state.system.nodes -> + entry.2.votes.Nodup + +def NodeVotesSent (state : State) : Prop := + forall entry, entry ∈ state.system.nodes -> + forall voter, voter ∈ entry.2.votes -> + SentVote state voter entry.1 + +def SentVotesFunctional (state : State) : Prop := + forall voter first second, + SentVote state voter first -> + SentVote state voter second -> + first = second + +def SentVoteStable (state : State) : Prop := + forall envelope, envelope ∈ state.sent -> + envelope.payload = .vote -> + forall entry, entry ∈ state.system.nodes -> + entry.1 = envelope.source -> + entry.2.phase ≠ .gossiping /\ + (entry.2.phase = .voting -> + entry.2.chosen = some envelope.target) + +def NodeVotingSelection (state : NodeState) : Prop := + exists target txid, + state.chosen = some target /\ + maximumGossip state.gossips = some (target, txid) + +def VotingSelectionsValid (state : State) : Prop := + forall entry, entry ∈ state.system.nodes -> + entry.2.phase = .voting -> + NodeVotingSelection entry.2 + +def SentVotesSelected (state : State) : Prop := + forall envelope, envelope ∈ state.sent -> + envelope.payload = .vote -> + NodeVotingSelection envelope.sourceState + +structure Opening.Valid + (config : Config) + (globalState : State) + (opening : Opening) : Prop where + location : opening.state.location = opening.node + phase : opening.state.phase = .opening + kind : opening.state.openKind = some opening.kind + votesNodup : opening.state.votes.Nodup + quorum : + opening.kind = .quorum -> + voteQuorum config.protocol <= opening.state.votes.length + votesSent : + forall voter, voter ∈ opening.state.votes -> + SentVote globalState voter opening.node + +def OpeningsValid (config : Config) (state : State) : Prop := + forall opening, opening ∈ state.openings -> + Opening.Valid config state opening + +structure QuorumInvariant (config : Config) (state : State) : Prop where + votesNodup : NodeVotesNodup state + votesSent : NodeVotesSent state + sentVoteStable : SentVoteStable state + sentVotesFunctional : SentVotesFunctional state + votingSelections : VotingSelectionsValid state + sentVotesSelected : SentVotesSelected state + openingsValid : OpeningsValid config state + +def acceptedVoteSource : Event -> Option Location + | .receiveVote source .accepted => some source + | _ => none + +def QuorumOpened (state : State) (node : Location) : Prop := + exists opening, + opening ∈ state.openings /\ + opening.node = node /\ + opening.kind = .quorum + +end DisasterRecovery.Protocol.Quorum diff --git a/lean/disaster-recovery/README.md b/lean/disaster-recovery/README.md new file mode 100644 index 000000000000..c6dc5b382d25 --- /dev/null +++ b/lean/disaster-recovery/README.md @@ -0,0 +1,133 @@ +# Lean disaster recovery model + +This package contains the canonical Lean model of CCF's C++ recovery decision +protocol and its permanent safety proofs. It is pinned to Lean 4.33.1 and +Mathlib `v4.33.1`. + +## Model + +`DisasterRecovery.Protocol.Model` models one protocol node. Its state machine +covers Gossiping, Voting, Opening, Joining, and Open, including the separate +timeout lane, retries, duplicate receives, strict-majority voting, failover, +restart, and completion. + +`DisasterRecovery.Protocol.Global` lifts the local transition function to a +system with active nodes, in-flight messages, immutable send history, and +terminal effects. Deliveries consume previously sent envelopes, so receives +cannot appear without a modeled send. + +The model follows the current C++ behavior in which a successfully validated +location is not rejected merely because it is absent from +`expectedLocations`. In particular, an accepted gossip from an unexpected +location can satisfy a size threshold. `CanonicalTests.lean` checks this +intentional accepted-unexpected-location behavior so that the implementation +discrepancy remains explicit. + +`Validation.accepted` and `Validation.rejected` are the boundary at which the +model receives the result of C++ quote and certificate validation. The model +does not formalize or prove the cryptography that produces that result. + +## Review guide + +Start with `DisasterRecovery/Properties.lean`: it exposes 9 system-level +`theorem` statements, each with an explicit application of its checked proof. +Review those statements and every definition or assumption they use in +`DisasterRecovery/Protocol/`. Machine checking does not establish that the +model matches the C++ implementation or that its assumptions describe a real +deployment. + +The 124 supporting declarations are `lemma`s in +`DisasterRecovery/Proofs/`. Their implementations can normally be omitted from +line-by-line human review once the build and axiom audit pass. Mathlib's +`lemma` is a synonym for `theorem`, not a weaker form of checking. The public +statements remain explicitly linked to these lemmas rather than being detached +specifications. + +Declaration namespaces follow the module paths. Model definitions live under +`DisasterRecovery.Protocol.`, supporting lemmas under +`DisasterRecovery.Proofs.`, and the 9 reviewed theorems under +`DisasterRecovery.Properties`. For example, +`DisasterRecovery.Properties.gossip_freezes_after_choice` explicitly applies +`DisasterRecovery.Proofs.Model.gossip_freezes_after_choice` from +`DisasterRecovery/Proofs/Model.lean`. Local and global properties share the +`DisasterRecovery.Properties` namespace; their `Config` types come from the +corresponding protocol modules. + +Only the Lean files under `DisasterRecovery/Proofs/` are marked +`linguist-generated` in the repository's `.gitattributes`, so GitHub can collapse +them without collapsing the review-required model and properties. Changes to imports, the review boundary, +the toolchain, dependencies, or checking machinery still require human review. +`DisasterRecovery.lean`, `CanonicalTests.lean`, the Lake configuration and lockfile, +and the CI workflow are part of that review surface. + +## Proof coverage and limits + +`DisasterRecovery.Proofs.Model` proves local transition-safety properties. + +`DisasterRecovery.Proofs.Invariants` proves global well-formedness, +message provenance, locality of transitions, append-only send history, and +monotonic terminal histories for reachable states. + +`DisasterRecovery.Proofs.Quorum` proves that votes are unique and backed by +prior sends, strict-majority quorums intersect, and any two quorum openings in +a reachable execution select the same opener. This safety result is independent +of scheduling assumptions. + +`DisasterRecovery.Proofs.Committed` proves TxID maximum properties and +committed-prefix preservation under two explicit premises: + +- `DurableCommit` requires at least one configured recovered ledger to cover + the committed TxID. +- `FullGossipSelection` requires a real sent vote whose selection snapshot + contains exactly the configured recovered TxIDs. + +A quorum opening alone does not imply `FullGossipSelection`, because voting may +begin after a gossip timeout. The committed-prefix result deliberately does not +derive or hide either durability or full-gossip evidence. + +Liveness, fairness, progress, and termination properties are out of scope at +this stage. + +## Files + +| File | Review role | Purpose | +| ------------------------------------------- | --------------- | ---------------------------------------------------- | +| `DisasterRecovery/Properties.lean` | Human | Selected system properties and checked proof links | +| `DisasterRecovery/Protocol/Model.lean` | Human | C++-aligned local transition model | +| `DisasterRecovery/Protocol/Global.lean` | Human | Distributed transitions and reachability | +| `DisasterRecovery/Protocol/Invariants.lean` | Human | Well-formedness and message-provenance predicates | +| `DisasterRecovery/Protocol/Quorum.lean` | Human | Vote and quorum-opening predicates | +| `DisasterRecovery/Protocol/Committed.lean` | Human | Prefix ordering, durability and full-gossip premises | +| `DisasterRecovery/Proofs/*.lean` | Machine-checked | Supporting lemmas and proof implementations | +| `DisasterRecovery.lean` | Human | Complete library import and audit root | +| `CanonicalTests.lean` | Human | Executable canonical behavior checks | + +## Validation + +Run from this directory: + +```console +lake exe cache get +lake exe mk_all --check --lib DisasterRecovery +lake build --wfail +lake lint +lake exe canonical-checks +``` + +`lake build --wfail` treats build warnings, including uses of `sorry` and +`admit`, as errors. `lake lint` runs +[`axiom-audit`](https://github.com/leanprover-community/axiom-audit) over the +`DisasterRecovery` library's transitive axiom dependencies. Only `propext`, +`Classical.choice`, and `Quot.sound` are allowed, so `sorryAx`, user-defined +axioms, and `native_decide` dependencies are rejected. + +The build compiles the reviewed statements and their proof implementations; +`lake exe canonical-checks` separately exercises the transition model. +`mk_all --check` verifies that `DisasterRecovery.lean` imports every library +module, preventing newly added proofs from being silently omitted from the +build and audit. Run `lake exe mk_all --lib DisasterRecovery` to refresh the +import root when adding a module. + +When refreshing the auditor dependency, use +`lake --keep-toolchain update axiomAudit` to retain the package's pinned +Lean and Mathlib versions. diff --git a/lean/disaster-recovery/lake-manifest.json b/lean/disaster-recovery/lake-manifest.json new file mode 100644 index 000000000000..6c10c12ab941 --- /dev/null +++ b/lean/disaster-recovery/lake-manifest.json @@ -0,0 +1,129 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/axiom-audit.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "46024e005996495c65ef609368e11ab39c4222e3", + "name": "axiomAudit", + "manifestFile": "lake-manifest.json", + "inputRev": "46024e005996495c65ef609368e11ab39c4222e3", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.1", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "disaster_recovery", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/lean/disaster-recovery/lakefile.toml b/lean/disaster-recovery/lakefile.toml new file mode 100644 index 000000000000..83c7c7e13827 --- /dev/null +++ b/lean/disaster-recovery/lakefile.toml @@ -0,0 +1,27 @@ +name = "disaster_recovery" +version = "0.1.0" +moreLeanArgs = ["-DwarningAsError=true"] +# Quote the hyphenated executable name for Lean's name parser. +lintDriver = "axiomAudit/\u00abaxiom-audit\u00bb" +lintDriverArgs = ["--root", "DisasterRecovery"] +defaultTargets = [ + "DisasterRecovery", + "canonical-checks", +] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "v4.33.1" + +[[require]] +name = "axiomAudit" +git = "https://github.com/leanprover-community/axiom-audit.git" +rev = "46024e005996495c65ef609368e11ab39c4222e3" # v0.1.2 + +[[lean_lib]] +name = "DisasterRecovery" + +[[lean_exe]] +name = "canonical-checks" +root = "CanonicalTests" diff --git a/lean/disaster-recovery/lean-toolchain b/lean/disaster-recovery/lean-toolchain new file mode 100644 index 000000000000..a8afa7d1b02d --- /dev/null +++ b/lean/disaster-recovery/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.1