diff --git a/.github/workflows/README.md b/.github/workflows/README.md index bf65dc78162a..07e6d9404580 100644 --- a/.github/workflows/README.md +++ b/.github/workflows/README.md @@ -114,6 +114,10 @@ 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. +The temporary migration-evidence job builds and audits the Lean mirror of the +legacy Rust/Stateright disaster recovery model, exercises both implementations, +and exhaustively compares their complete graphs for up to three nodes. + File: `lean.yml` 3rd party dependencies: None diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml index 081a8fc0604b..cb1f134a392a 100644 --- a/.github/workflows/lean.yml +++ b/.github/workflows/lean.yml @@ -4,6 +4,7 @@ on: pull_request: paths: - "lean/**" + - "tla/disaster-recovery/**" - ".github/workflows/lean.yml" concurrency: @@ -45,3 +46,55 @@ jobs: lake build --wfail lake lint lake exe canonical-checks + + migration-evidence: + name: Temporary migration evidence + runs-on: ubuntu-latest + timeout-minutes: 90 + + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + + - name: Install Lean and Rust + shell: bash + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y elan + elan toolchain install "$(cat lean/disaster-recovery-migration/lean-toolchain)" + rustup toolchain install stable --profile minimal + rustup default stable + + - name: Build and check Rust model + working-directory: tla/disaster-recovery + shell: bash + run: | + set -euo pipefail + cargo check --locked + cargo build --locked + cargo run --quiet --locked -- --nodes 2 check + + - name: Restore Mathlib cache + working-directory: lean/disaster-recovery-migration + shell: bash + run: | + set -euo pipefail + lake exe cache get + + - name: Build and check migration model + working-directory: lean/disaster-recovery-migration + shell: bash + run: | + set -euo pipefail + lake exe mk_all --check --lib DisasterRecoveryMigration + lake build --wfail + lake lint + lake exe migration-semantic-checks + lake exe migration-model-checker --nodes 3 + + - name: Compare complete Rust and Lean graphs + working-directory: lean/disaster-recovery-migration + shell: bash + run: | + set -euo pipefail + python3 compare.py --nodes 1 2 3 diff --git a/lean/disaster-recovery-migration/DisasterRecoveryMigration.lean b/lean/disaster-recovery-migration/DisasterRecoveryMigration.lean new file mode 100644 index 000000000000..f17bd8ffc407 --- /dev/null +++ b/lean/disaster-recovery-migration/DisasterRecoveryMigration.lean @@ -0,0 +1,3 @@ +import DisasterRecoveryMigration.Legacy.Checker +import DisasterRecoveryMigration.Legacy.Model +import DisasterRecoveryMigration.Refinement diff --git a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean new file mode 100644 index 000000000000..659daef03546 --- /dev/null +++ b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean @@ -0,0 +1,152 @@ +import DisasterRecoveryMigration.Legacy.Model + +namespace DisasterRecoveryMigration.Legacy + +structure Edge where + src : Nat + action : Action + dst : Nat +deriving Repr, BEq + +structure Graph where + states : Array GlobalState + edges : Array Edge + parents : Array (Option (Prod Nat Action)) + +def enumerate (n : Nat) : IO Graph := do + let initial := initialState n + let mut states := #[initial] + let mut edges := #[] + let mut parents : Array (Option (Prod Nat Action)) := #[none] + let mut seen : Std.HashMap String Nat := {} + seen := seen.insert (stateKey initial) 0 + let mut cursor := 0 + while cursor < states.size do + let state := states[cursor]! + for action in actions state do + match nextState n state action with + | none => pure () + | some next => + let key := stateKey next + let (dst, discovered) := + match seen[key]? with + | some index => (index, false) + | none => (states.size, true) + if discovered then + seen := seen.insert key dst + states := states.push next + parents := parents.push (some (cursor, action)) + edges := edges.push { src := cursor, action, dst } + cursor := cursor + 1 + pure { states, edges, parents } + +def valuationBits (values : Array Bool) : String := + String.ofList (values.toList.map fun value => if value then '1' else '0') + +private structure ExportEdge where + src : Nat + action : String + dst : Nat + +private def exportEdgeLE (left right : ExportEdge) : Bool := + left.src < right.src || + (left.src == right.src && + (left.action < right.action || + (left.action == right.action && left.dst <= right.dst))) + +private def traceTo (graph : Graph) (target : Nat) : List Action := + let rec collect (index : Nat) (fuel : Nat) (suffix : List Action) : List Action := + match fuel with + | 0 => suffix + | fuel + 1 => + match graph.parents[index]? |>.bind id with + | none => suffix + | some (parent, action) => collect parent fuel (action :: suffix) + collect target graph.states.size [] + +private def printTrace (graph : Graph) (target : Nat) : IO Unit := do + let trace := traceTo graph target + if trace.isEmpty then + IO.eprintln " trace: " + else + for (action, step) in trace.zipIdx do + IO.eprintln s!" {step + 1}. {actionKey action}" + +private def eventuallyGood (graph : Graph) (property : Nat) : Array Bool := + Id.run do + let mut good := + graph.states.map fun state => (legacyValuations state.actors.size state)[property]! + let mut remaining := Array.replicate graph.states.size 0 + let mut predecessors : Array (List Nat) := Array.replicate graph.states.size [] + for edge in graph.edges do + remaining := remaining.modify edge.src (fun count => count + 1) + predecessors := predecessors.modify edge.dst (fun values => edge.src :: values) + let mut queue := #[] + for index in List.range good.size do + if good[index]! then queue := queue.push index + let mut cursor := 0 + while cursor < queue.size do + let resolved := queue[cursor]! + for predecessor in predecessors[resolved]! do + if !good[predecessor]! then + remaining := remaining.modify predecessor (fun count => count - 1) + if remaining[predecessor]! == 0 then + good := good.set! predecessor true + queue := queue.push predecessor + cursor := cursor + 1 + return good + +def checkGraph (n : Nat) (graph : Graph) : IO Bool := do + IO.eprintln s!"reachable states: {graph.states.size}, transitions: {graph.edges.size}" + let mut passed := true + for property in List.range legacyPropertyNames.size do + let name := legacyPropertyNames[property]! + let expectation := legacyExpectations[property]! + let values := graph.states.map fun state => (legacyValuations n state)[property]! + let eventual := if expectation == "eventually" then eventuallyGood graph property else #[] + let result := + if expectation == "always" then values.all id + else if expectation == "sometimes" then values.any id + else eventual[0]! + IO.eprintln s!"{if result then "PASS" else "FAIL"} [{expectation}] {name}" + if result && expectation == "sometimes" then + match (List.range values.size).find? (fun index => values[index]!) with + | none => pure () + | some index => + IO.eprintln " shortest example:" + printTrace graph index + else if !result then + passed := false + let witness := + if expectation == "always" then + (List.range values.size).find? fun index => !values[index]! + else if expectation == "sometimes" then + some 0 + else + (List.range values.size).find? fun index => + !eventual[index]! + match witness with + | none => IO.eprintln " no reachable example" + | some index => printTrace graph index + pure passed + +def exportGraph (n : Nat) (graph : Graph) : IO Unit := do + let canonical := (graph.states.toList.zipIdx.map fun (state, bfsId) => + (stateKey state, bfsId)).mergeSort (fun left right => left.1 <= right.1) + let mut ids := Array.replicate graph.states.size 0 + for ((_, bfsId), canonicalId) in canonical.zipIdx do + ids := ids.set! bfsId canonicalId + IO.println "format\tccf-legacy-dr-graph-v1" + IO.println s!"nodes\t{n}" + IO.println s!"init\t{ids[0]!}" + for ((key, bfsId), canonicalId) in canonical.zipIdx do + IO.println s!"state\t{canonicalId}\t{key}\t{valuationBits (legacyValuations n graph.states[bfsId]!)}" + let canonicalEdges := (graph.edges.toList.map fun edge => { + src := ids[edge.src]! + action := actionKey edge.action + dst := ids[edge.dst]! + }).mergeSort exportEdgeLE + for edge in canonicalEdges do + IO.println s!"edge\t{edge.src}\t{edge.action}\t{edge.dst}" + +end DisasterRecoveryMigration.Legacy diff --git a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Model.lean b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Model.lean new file mode 100644 index 000000000000..91000ae2f1b5 --- /dev/null +++ b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Model.lean @@ -0,0 +1,392 @@ +import Std + +namespace DisasterRecoveryMigration.Legacy + +abbrev Id := Nat +abbrev Txid := Nat + +structure Gossip where + src : Id + txid : Txid +deriving Repr, BEq, Hashable + +structure Vote where + src : Id + recv : List Gossip +deriving Repr, BEq, Hashable + +inductive Msg where + | gossip (value : Gossip) + | vote (value : Vote) + | iAmOpen (src : Id) +deriving Repr, BEq, Hashable + +inductive Phase where + | vote + | openJoin + | open (timeout : Bool) + | join +deriving Repr, BEq, Hashable, Inhabited + +structure ActorState where + nextStep : Phase + gossips : List Gossip + votes : List Vote + submittedVote : Option (Prod Id Vote) + txid : Txid +deriving Repr, BEq, Hashable, Inhabited + +structure Envelope where + src : Id + dst : Id + msg : Msg +deriving Repr, BEq, Hashable + +structure GlobalState where + actors : Array ActorState + timers : Array Bool + network : List Envelope +deriving Repr, BEq, Hashable, Inhabited + +inductive Action where + | deliver (envelope : Envelope) + | timeout (id : Id) +deriving Repr, BEq, Hashable + +structure Output where + sent : List (Prod Id Msg) := [] + setTimer : Bool := false +deriving Repr, BEq + +private def comma (values : List String) : String := + String.intercalate "," values + +def gossipKey (gossip : Gossip) : String := + s!"g({gossip.src},{gossip.txid})" + +def voteKey (vote : Vote) : String := + s!"v({vote.src},[{comma (vote.recv.map gossipKey)}])" + +def msgKey : Msg -> String + | .gossip gossip => gossipKey gossip + | .vote vote => voteKey vote + | .iAmOpen src => s!"o({src})" + +def envelopeKey (envelope : Envelope) : String := + s!"e({envelope.src},{envelope.dst},{msgKey envelope.msg})" + +def phaseKey : Phase -> String + | .vote => "vote" + | .openJoin => "openjoin" + | .open false => "open0" + | .open true => "open1" + | .join => "join" + +def submittedKey : Option (Prod Id Vote) -> String + | none => "none" + | some (dst, vote) => s!"some({dst},{voteKey vote})" + +def actorKey (actor : ActorState) : String := + s!"s({phaseKey actor.nextStep},[{comma (actor.gossips.map gossipKey)}],[{comma (actor.votes.map voteKey)}],{submittedKey actor.submittedVote},{actor.txid})" + +private def networkRunsFrom (current : Envelope) (count : Nat) : + List Envelope -> List (Prod Envelope Nat) + | [] => [(current, count)] + | head :: tail => + if head == current then + networkRunsFrom current (count + 1) tail + else + (current, count) :: networkRunsFrom head 1 tail + +private def networkRuns : List Envelope -> List (Prod Envelope Nat) + | [] => [] + | head :: tail => networkRunsFrom head 1 tail + +def stateKey (state : GlobalState) : String := + let actors := String.intercalate ";" (state.actors.toList.map actorKey) + let timers := comma (((List.range state.timers.size).filter + (fun id => state.timers[id]!)).map toString) + let network := comma ((networkRuns state.network).map fun (env, count) => + s!"{envelopeKey env}#{count}") + s!"S([{actors}],[{timers}],[{network}])" + +def actionKey : Action -> String + | .deliver env => s!"deliver({env.src},{env.dst},{msgKey env.msg})" + | .timeout id => s!"timeout({id},election)" + +private def insertSorted (before : a -> a -> Bool) (value : a) : List a -> List a + | [] => [value] + | head :: tail => + if before value head then + value :: head :: tail + else + head :: insertSorted before value tail + +private def insertUniqueSorted [BEq a] (before : a -> a -> Bool) (value : a) (values : List a) : + List a := + if values.contains value then values else insertSorted before value values + +private def removeOne [BEq a] (value : a) : List a -> List a + | [] => [] + | head :: tail => if head == value then tail else head :: removeOne value tail + +private def gossipGreater (left right : Gossip) : Bool := + right.txid < left.txid || (right.txid == left.txid && right.src < left.src) + +private def gossipBefore (left right : Gossip) : Bool := + left.src < right.src || (left.src == right.src && left.txid < right.txid) + +private def gossipListBefore : List Gossip -> List Gossip -> Bool + | [], [] => false + | [], _ :: _ => true + | _ :: _, [] => false + | left :: leftTail, right :: rightTail => + if left == right then gossipListBefore leftTail rightTail + else gossipBefore left right + +private def voteBefore (left right : Vote) : Bool := + left.src < right.src || (left.src == right.src && gossipListBefore left.recv right.recv) + +private def msgBefore : Msg -> Msg -> Bool + | .gossip left, .gossip right => gossipBefore left right + | .gossip _, _ => true + | .vote _, .gossip _ => false + | .vote left, .vote right => voteBefore left right + | .vote _, .iAmOpen _ => true + | .iAmOpen _, .gossip _ => false + | .iAmOpen _, .vote _ => false + | .iAmOpen left, .iAmOpen right => left < right + +private def envelopeBefore (left right : Envelope) : Bool := + left.src < right.src || + (left.src == right.src && + (left.dst < right.dst || (left.dst == right.dst && msgBefore left.msg right.msg))) + +private def maximumGossip : List Gossip -> Option Gossip + | [] => none + | head :: tail => + some (tail.foldl (fun current candidate => + if gossipGreater candidate current then candidate else current) head) + +private def voteForMax (gossips : List Gossip) (id : Id) : Option (Prod Id Vote) := do + let maximum <- maximumGossip gossips + pure (maximum.src, { src := id, recv := gossips }) + +private def otherPeers (n id : Nat) : List Id := + (List.range n).filter (fun peer => peer != id) + +private def advanceStep (n id : Nat) (timeout : Bool) (state : ActorState) : + Prod ActorState (Prod Output Bool) := + match state.nextStep with + | .vote => + if state.gossips.length == n || timeout then + match voteForMax state.gossips id with + | none => (state, {}, false) + | some (dst, vote) => + let next := { + state with + nextStep := .openJoin + submittedVote := some (dst, vote) + votes := if dst == id then insertUniqueSorted voteBefore vote state.votes else state.votes + } + let sent := if dst == id then [] else [(dst, Msg.vote vote)] + (next, { sent }, true) + else + (state, {}, false) + | .openJoin => + if state.votes.length >= (n + 1) / 2 || timeout then + let sent := (otherPeers n id).map (fun peer => (peer, Msg.iAmOpen id)) + ({ state with nextStep := .open timeout }, { sent }, true) + else + (state, {}, false) + | _ => (state, {}, false) + +def advanceSeveral (n id : Nat) (timeout : Bool) (state : ActorState) : + Prod ActorState Output := + let (state1, output1, advanced1) := advanceStep n id timeout state + if advanced1 then + let (state2, output2, _) := advanceStep n id timeout state1 + (state2, { sent := output1.sent ++ output2.sent }) + else + (state, {}) + +def onMessage (n id : Nat) (state : ActorState) (msg : Msg) : + Option (Prod ActorState Output) := + let received := + match msg with + | .gossip gossip => + if !state.gossips.contains gossip && state.submittedVote.isNone then + { state with gossips := insertUniqueSorted gossipBefore gossip state.gossips } + else + state + | .vote vote => + { state with votes := insertUniqueSorted voteBefore vote state.votes } + | .iAmOpen _ => + match state.nextStep with + | .open _ => state + | _ => { state with nextStep := .join } + let (next, output) := advanceSeveral n id false received + some (next, output) + +def onTimeout (n id : Nat) (state : ActorState) : Option (Prod ActorState Output) := + match state.nextStep with + | .vote => + if state.gossips.isEmpty then none + else + let (next, output) := advanceSeveral n id true state + some (next, { output with setTimer := true }) + | .openJoin => + if state.votes.isEmpty then none + else some (advanceSeveral n id true state) + | _ => none + +private def applyOutput (src : Id) (output : Output) (state : GlobalState) : GlobalState := + let network := output.sent.foldl + (fun current (dst, msg) => insertSorted envelopeBefore { src, dst, msg } current) + state.network + let timers := if output.setTimer then state.timers.set! src true else state.timers + { state with network, timers } + +private def startActor (n id : Nat) : Prod ActorState Output := + let gossip := { src := id, txid := id } + let initial : ActorState := { + nextStep := .vote + gossips := [gossip] + votes := [] + submittedVote := none + txid := id + } + let output : Output := { + sent := (otherPeers n id).map (fun peer => (peer, Msg.gossip gossip)) + setTimer := true + } + let (state, advanced) := advanceSeveral n id false initial + (state, { sent := output.sent ++ advanced.sent, setTimer := true }) + +def initialState (n : Nat) : GlobalState := + (List.range n).foldl (fun global id => + let (actor, output) := startActor n id + let withActor := { + global with + actors := global.actors.push actor + timers := global.timers.push false + } + applyOutput id output withActor) + { actors := #[], timers := #[], network := [] } + +private def distinctNetworkFrom (previous : Envelope) : List Envelope -> List Envelope + | [] => [] + | head :: tail => + if head == previous then + distinctNetworkFrom previous tail + else + head :: distinctNetworkFrom head tail + +private def distinctNetwork : List Envelope -> List Envelope + | [] => [] + | head :: tail => head :: distinctNetworkFrom head tail + +def actions (state : GlobalState) : List Action := + (distinctNetwork state.network).map Action.deliver ++ + ((List.range state.timers.size).filter + (fun id => state.timers[id]!)).map Action.timeout + +def nextState (n : Nat) (state : GlobalState) : Action -> Option GlobalState + | .deliver envelope => do + let actor <- state.actors[envelope.dst]? + let (nextActor, output) <- onMessage n envelope.dst actor envelope.msg + let delivered := { + state with + actors := state.actors.set! envelope.dst nextActor + network := removeOne envelope state.network + } + pure (applyOutput envelope.dst output delivered) + | .timeout id => do + guard (state.timers[id]?.getD false) + let actor <- state.actors[id]? + let (nextActor, output) <- onTimeout n id actor + let expired := { + state with + actors := state.actors.set! id nextActor + timers := state.timers.set! id false + } + pure (applyOutput id output expired) + +def reachedOpen (state : GlobalState) : Bool := + state.actors.any fun actor => + match actor.nextStep with + | .open _ => true + | _ => false + +def reachedOpenTimeout (state : GlobalState) (expected : Bool) : Bool := + state.actors.any fun actor => actor.nextStep == .open expected + +def unanimousVotes (n : Nat) (state : GlobalState) : Bool := + state.actors.all fun actor => + match actor.submittedVote with + | none => false + | some (_, vote) => + (List.range n).all fun peer => vote.recv.any (fun gossip => gossip.src == peer) + +def majorityHaveSameMaximum (state : GlobalState) : Bool := + let chosen := state.actors.toList.filterMap fun actor => do + let (_, vote) <- actor.submittedVote + let maximum <- maximumGossip vote.recv + pure maximum.src + let chosen := chosen.foldl (fun values id => + insertSorted (fun left right => left < right) id values) [] + let majorityIndex := state.actors.size / 2 + match chosen[majorityIndex]? with + | none => false + | some majority => (chosen.take majorityIndex).all (fun chosen => chosen == majority) + +private def implies (left right : Bool) : Bool := + !left || right + +def legacyValuations (n : Nat) (state : GlobalState) : Array Bool := + let openCount := state.actors.countP fun actor => + match actor.nextStep with + | .open _ => true + | _ => false + let allOpenJoin := state.actors.all (fun actor => actor.nextStep == .openJoin) + let allVotesDelivered := !state.network.any fun envelope => + match envelope.msg with + | .vote _ => true + | _ => false + let majorityIndex := state.actors.size / 2 + let commitTxid := (state.actors[majorityIndex]!).txid + let persisted := state.actors.all fun actor => + match actor.nextStep with + | .open _ => actor.txid >= commitTxid + | _ => true + #[ + implies (unanimousVotes n state) (reachedOpenTimeout state false), + reachedOpen state, + implies (majorityHaveSameMaximum state) (reachedOpenTimeout state false), + implies (!reachedOpenTimeout state true) (openCount <= 1), + !(allOpenJoin && allVotesDelivered), + implies (!reachedOpenTimeout state true) persisted, + implies (state.actors.size > 1) (reachedOpen state), + reachedOpenTimeout state true, + majorityHaveSameMaximum state && reachedOpenTimeout state false + ] + +def legacyPropertyNames : Array String := #[ + "Unanimous votes => no chance of a fork", + "Open", + "Majority votes => no fork", + "No open with timeout, no fork", + "Deadlock", + "Persist committed txs", + "Open is possible", + "Unsafe open with timeout", + "Majority vote still opens without timeout" +] + +def legacyExpectations : Array String := #[ + "eventually", "eventually", "eventually", + "always", "always", "always", + "sometimes", "sometimes", "sometimes" +] + +end DisasterRecoveryMigration.Legacy diff --git a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Refinement.lean b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Refinement.lean new file mode 100644 index 000000000000..722e5d2229e1 --- /dev/null +++ b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Refinement.lean @@ -0,0 +1,335 @@ +import DisasterRecoveryMigration.Legacy.Model +import DisasterRecovery.Protocol.Model +import Mathlib.Logic.Relation + +namespace DisasterRecoveryMigration.Refinement + +open DisasterRecovery.Protocol + +def projectPhase (state : NodeState) : DisasterRecoveryMigration.Legacy.Phase := + match state.phase with + | .gossiping => .vote + | .voting => .openJoin + | .opening | .open => + match state.openKind with + | some .failover => .open true + | _ => .open false + | .joining => .join + +inductive LegacyAtomic : + DisasterRecoveryMigration.Legacy.Phase -> DisasterRecoveryMigration.Legacy.Phase -> Prop where + | gossipToVoting : LegacyAtomic .vote .openJoin + | quorumOpen : LegacyAtomic .openJoin (.open false) + | failoverOpen : LegacyAtomic .openJoin (.open true) + | gossipToJoin : LegacyAtomic .vote .join + | votingToJoin : LegacyAtomic .openJoin .join + +abbrev LegacyWeakStep := + Relation.ReflTransGen LegacyAtomic + +def embeddedTxID + (config : Config) + (source : Location) + (txid : TxID) : Prop := + txid.view = 0 /\ config.expectedLocations[txid.seqno]? = some source + +structure LegacyDataAssumptions + (config : Config) + (event : Event) + (after : NodeState) : Prop where + /-- Recorded for a future data refinement; phase simulation does not assume it. -/ + oddNodeCount : + exists half, config.expectedLocations.length = 2 * half + 1 + acceptedExpectedInput : + match event with + | .receiveGossip source txid validation => + validation = .accepted /\ + expectedSource config source = true /\ + embeddedTxID config source txid + | .receiveVote source validation => + validation = .accepted /\ expectedSource config source = true + | .receiveIAmOpen source validation => + validation = .accepted /\ expectedSource config source = true + | .timeout | .retry => True + quorumOnly : + after.openKind != some .failover + +structure CompatibilityStep + (config : Config) + (before : NodeState) + (event : Event) + (after : NodeState) : Prop where + canonical : + after = (step config before event).state + +private theorem advance_simulates + (config : Config) + (state : NodeState) + (timeout : Bool) + (output : StepOutput) + (advanced : advance config state timeout = some output) : + LegacyWeakStep (projectPhase state) (projectPhase output.state) := by + cases timeout <;> cases phase : state.phase <;> + simp [advance, phase] at advanced <;> + repeat' split at advanced <;> + simp_all [projectPhase, advanceTimeoutLane, advanceTimeoutState] + all_goals subst output + all_goals simp_all [projectPhase, advanceTimeoutLane] + all_goals + first + | (split <;> simp_all) + | skip + all_goals + first + | exact .refl + | exact .single .gossipToVoting + | exact .single .quorumOpen + | exact .single .failoverOpen + +private theorem receive_gossip_simulates + (config : Config) + (before : NodeState) + (source : Location) + (txid : TxID) + (validation : Validation) : + LegacyWeakStep + (projectPhase before) + (projectPhase + (step config before (.receiveGossip source txid validation)).state) := by + cases validation with + | rejected => + simp [step, rejected] + exact .refl + | accepted => + by_cases frozen : before.chosen != none + case pos => + simp [step, frozen, rejected] + exact .refl + case neg => + let received := { + before with gossips := insertGossip source txid before.gossips } + have same : projectPhase received = projectPhase before := by + simp [received, projectPhase] + cases advanced : advance config received false with + | none => + simp [step, frozen, received, advanced, rejected] + exact .refl + | some output => + simp [step, frozen, received, advanced] + have simulation := + advance_simulates config received false output advanced + rw [same] at simulation + exact simulation + +private theorem receive_vote_simulates + (config : Config) + (before : NodeState) + (source : Location) + (validation : Validation) : + LegacyWeakStep + (projectPhase before) + (projectPhase + (step config before (.receiveVote source validation)).state) := by + cases validation with + | rejected => + simp [step, rejected] + exact .refl + | accepted => + let received := { before with votes := insertVote source before.votes } + have same : projectPhase received = projectPhase before := by + simp [received, projectPhase] + cases advanced : advance config received false with + | none => + simp [step, received, advanced, rejected] + exact .refl + | some output => + simp [step, received, advanced] + have simulation := + advance_simulates config received false output advanced + rw [same] at simulation + exact simulation + +private theorem receive_iamopen_simulates + (config : Config) + (before : NodeState) + (source : Location) + (validation : Validation) : + LegacyWeakStep + (projectPhase before) + (projectPhase + (step config before (.receiveIAmOpen source validation)).state) := by + cases validation with + | rejected => + simp [step, rejected] + exact .refl + | accepted => + cases phase : before.phase <;> + simp [step, phase, advance, rejected, projectPhase, + advanceTimeoutLane] + all_goals + first + | exact .single .gossipToJoin + | exact .single .votingToJoin + | exact .refl + +theorem canonical_step_simulates + (config : Config) + (before : NodeState) + (event : Event) : + LegacyWeakStep + (projectPhase before) + (projectPhase (step config before event).state) := by + cases event with + | receiveGossip source txid validation => + exact receive_gossip_simulates config before source txid validation + | receiveVote source validation => + exact receive_vote_simulates config before source validation + | receiveIAmOpen source validation => + exact receive_iamopen_simulates config before source validation + | timeout => + cases advanced : advance config before true with + | none => + simp [step, advanced, rejected] + exact .refl + | some output => + simp [step, advanced] + exact advance_simulates config before true output advanced + | retry => + exact .refl + +theorem compatibility_step_simulates + {config : Config} + {before after : NodeState} + {event : Event} + (compatible : CompatibilityStep config before event after) : + LegacyWeakStep (projectPhase before) (projectPhase after) := by + rw [compatible.canonical] + exact canonical_step_simulates config before event + +theorem retryCompatibility + (config : Config) + (state : NodeState) : + CompatibilityStep config state .retry state := { + canonical := rfl +} + +theorem voteQuorumCompatibility + (config : Config) + (before : NodeState) + (source : Location) : + CompatibilityStep config before + (.receiveVote source .accepted) + (step config before (.receiveVote source .accepted)).state := { + canonical := rfl +} + +theorem quorum_phase_step_is_weak + (before after : NodeState) + (beforePhase : before.phase = .voting) + (afterPhase : after.phase = .opening) + (kind : after.openKind = some .quorum) : + LegacyWeakStep (projectPhase before) (projectPhase after) := by + simp [projectPhase, beforePhase, afterPhase, kind] + exact .single .quorumOpen + +theorem opening_to_open_is_stuttering + (before after : NodeState) + (beforePhase : before.phase = .opening) + (afterPhase : after.phase = .open) + (kind : after.openKind = before.openKind) : + LegacyWeakStep (projectPhase before) (projectPhase after) := by + simp [projectPhase, beforePhase, afterPhase, kind] + exact .refl + +inductive CompatibilityTrace + (config : Config) : + NodeState -> + List Event -> + NodeState -> + Prop where + | nil (state) : CompatibilityTrace config state [] state + | cons + (first middle last event rest) + (head : CompatibilityStep config first event middle) + (tail : CompatibilityTrace config middle rest last) : + CompatibilityTrace config first (event :: rest) last + +theorem compatibility_trace_simulates + {config : Config} + {first last : NodeState} + {events : List Event} + (compatible : CompatibilityTrace config first events last) : + LegacyWeakStep (projectPhase first) (projectPhase last) := by + induction compatible with + | nil state => exact .refl + | cons first middle last event rest head tail induction => + exact Relation.ReflTransGen.trans + (compatibility_step_simulates head) induction + +theorem initial_phase_correspondence : + projectPhase (initialNode "node0") = DisasterRecoveryMigration.Legacy.Phase.vote := by + rfl + +theorem three_node_initial_correspondence : + let config : Config := { + instanceId := "compat" + expectedLocations := ["0", "1", "2"] + } + ((initialSystem config).nodes.map + (fun entry => projectPhase entry.2) == + (DisasterRecoveryMigration.Legacy.initialState 3).actors.toList.map + (fun actor => actor.nextStep)) = true := by + rfl + +theorem odd_quorum_matches_legacy + (nodes half : Nat) + (odd : nodes = 2 * half + 1) : + nodes / 2 + 1 = (nodes + 1) / 2 := by + subst nodes + simp [Nat.add_div] + +theorem even_quorum_exceeds_legacy_by_one + (nodes half : Nat) + (even : nodes = 2 * half) : + nodes / 2 + 1 = (nodes + 1) / 2 + 1 := by + subst nodes + simp [Nat.add_div] + +def canonicalReachedOpen (state : NodeState) : Prop := + state.phase = .opening \/ state.phase = .open + +def projectedReachedOpen (state : NodeState) : Prop := + match projectPhase state with + | .open _ => True + | _ => False + +theorem reached_open_is_preserved + (state : NodeState) : + canonicalReachedOpen state <-> projectedReachedOpen state := by + cases phase : state.phase <;> + cases kind : state.openKind <;> + simp [canonicalReachedOpen, projectedReachedOpen, projectPhase, phase, kind] + all_goals + rename_i value + cases value <;> + simp + +theorem quorum_kind_projects_to_non_timeout_open + (state : NodeState) + (phase : state.phase = .opening \/ state.phase = .open) + (kind : state.openKind = some .quorum) : + projectPhase state = .open false := by + cases phase with + | inl opening => + cases state + simp_all [projectPhase] + | inr opened => + cases state + simp_all [projectPhase] + +theorem single_node_full_initial_models_differ : + projectPhase (initialNode "0") != + (DisasterRecoveryMigration.Legacy.initialState 1).actors[0]!.nextStep := by + decide + +end DisasterRecoveryMigration.Refinement \ No newline at end of file diff --git a/lean/disaster-recovery-migration/ExportMain.lean b/lean/disaster-recovery-migration/ExportMain.lean new file mode 100644 index 000000000000..f7500f6a967c --- /dev/null +++ b/lean/disaster-recovery-migration/ExportMain.lean @@ -0,0 +1,24 @@ +import DisasterRecoveryMigration.Legacy.Checker + +open DisasterRecoveryMigration.Legacy + +private def usage : String := + "usage: migration-exporter [--nodes N]" + +private def parseNodes : List String -> Except String Nat + | [] => pure 3 + | ["--nodes", value] => + match value.toNat? with + | some n => if n > 0 then pure n else throw "--nodes must be positive" + | none => throw s!"invalid node count: {value}" + | _ => throw usage + +def main (args : List String) : IO UInt32 := do + match parseNodes args with + | .error message => + IO.eprintln message + pure 2 + | .ok n => + let graph <- enumerate n + exportGraph n graph + pure 0 diff --git a/lean/disaster-recovery-migration/Main.lean b/lean/disaster-recovery-migration/Main.lean new file mode 100644 index 000000000000..c943598da3bc --- /dev/null +++ b/lean/disaster-recovery-migration/Main.lean @@ -0,0 +1,23 @@ +import DisasterRecoveryMigration.Legacy.Checker + +open DisasterRecoveryMigration.Legacy + +private def usage : String := + "usage: migration-model-checker [--nodes N]" + +private def parseNodes : List String -> Except String Nat + | [] => pure 3 + | ["--nodes", value] => + match value.toNat? with + | some n => if n > 0 then pure n else throw "--nodes must be positive" + | none => throw s!"invalid node count: {value}" + | _ => throw usage + +def main (args : List String) : IO UInt32 := do + match parseNodes args with + | .error message => + IO.eprintln message + pure 2 + | .ok n => + let graph <- enumerate n + if <- checkGraph n graph then pure 0 else pure 1 diff --git a/lean/disaster-recovery-migration/README.md b/lean/disaster-recovery-migration/README.md new file mode 100644 index 000000000000..3ea813d5400b --- /dev/null +++ b/lean/disaster-recovery-migration/README.md @@ -0,0 +1,113 @@ +# Temporary disaster recovery migration evidence + +This package is the temporary PR 2 evidence layer for migrating the legacy +Rust/Stateright disaster recovery model to Lean. It depends locally on the +canonical package in `../disaster-recovery`; it does not modify or duplicate +that package. This directory and the shared Lean workflow's migration-evidence +job are intended to be deleted by PR 3 once the evidence has served its +purpose. + +## Scope + +There are two distinct and deliberately weaker claims: + +1. The executable model in `DisasterRecoveryMigration.Legacy` is an exact + Lean mirror of the Rust/Stateright model in `tla/disaster-recovery`. + `compare.py` establishes exhaustive bounded equivalence for one, two, and + three nodes. +2. `DisasterRecoveryMigration.Refinement` relates the canonical C++-aligned + Lean model to the legacy Lean mirror only at the protocol-phase level. + +The bounded comparison is not a theorem about arbitrary node counts or a +formal semantics for Rust or Stateright. The phase refinement is not a full +bisimulation, data refinement, or proof that the canonical model is identical +to the Rust model. + +## Exact bounded equivalence + +Both exporters emit the stable `ccf-legacy-dr-graph-v1` format. State IDs are +assigned after sorting normalized state keys, independently of traversal +order. For each requested node count, `compare.py` checks: + +- the normalized initial state; +- every normalized reachable state in both directions; +- every labeled edge, including source and destination, in both directions; +- all nine registered predicate valuations for every reachable state; and +- the expected complete state and edge counts below. + +| Nodes | Reachable states | Labeled edges | Predicate values per state | +| ----: | ---------------: | ------------: | -------------------------: | +| 1 | 1 | 0 | 9 | +| 2 | 54 | 95 | 9 | +| 3 | 105,558 | 552,282 | 9 | + +The comparator fails on a difference from either exporter and reports a +shortest path to a representative state or edge mismatch. + +The mirror intentionally retains the legacy semantics, including message +multiplicity, unordered delivery, timer behavior, no-op suppression, immediate +multi-phase advancement, and the existing predicate definitions and names. +Differences in the canonical model are not backported into this oracle. + +## Canonical phase refinement and limitations + +`DisasterRecoveryMigration.Refinement` imports the canonical +`DisasterRecovery.Protocol.Model` through the local Lake dependency and +projects canonical phases as follows: + +- Gossiping maps to legacy Vote. +- Voting maps to legacy OpenJoin. +- canonical Opening and Open collapse to legacy Open, retaining quorum versus + failover as the legacy timeout flag. +- Joining maps to legacy Join. + +`canonical_step_simulates` proves that each canonical local step projects to a +reflexive-transitive legacy phase step. The file also proves finite compatible +trace simulation, collapsed-Open preservation, quorum-kind projection, and +Opening-to-Open stuttering. + +This phase-only result does not relate gossip sets, votes, timeout-lane state, +network state, transaction persistence, or all nine legacy predicates. It +does not establish a global scheduler correspondence or preserve the legacy +liveness expectations. + +Two intentional model differences are explicit: + +- The canonical quorum is the strict majority `n / 2 + 1`; the legacy quorum + is `(n + 1) / 2`. They agree for odd node counts, while for even node counts + the canonical threshold is one larger. +- With one node, the legacy full initial state opens immediately without a + timeout. The canonical initial node remains in Gossiping, whose projected + phase is Vote. `single_node_full_initial_models_differ` proves this mismatch. + +## Files + +| File | Purpose | +| ----------------------------------------------- | --------------------------------------------- | +| `DisasterRecoveryMigration/Legacy/Model.lean` | Exact executable legacy semantics | +| `DisasterRecoveryMigration/Legacy/Checker.lean` | BFS model checker and canonical graph encoder | +| `Main.lean` | Legacy model-checker CLI | +| `ExportMain.lean` | Separate Lean graph-exporter CLI | +| `Tests.lean` | Focused legacy semantic checks | +| `DisasterRecoveryMigration/Refinement.lean` | Canonical-to-legacy phase refinement | +| `compare.py` | Bidirectional exhaustive Rust/Lean comparison | + +## Validation + +Run from this directory: + +```console +lake exe cache get +lake exe mk_all --check --lib DisasterRecoveryMigration +lake build --wfail +lake lint +lake exe migration-semantic-checks +lake exe migration-model-checker --nodes 3 +python3 compare.py --nodes 1 2 3 +``` + +The canonical package's own axiom-audit configuration remains authoritative +for all canonical declarations and is run by the canonical job in the shared +Lean workflow. The migration Lake package pins Lean 4.33.1, transitively +resolves Mathlib v4.33.1, treats warnings as errors, verifies complete library +coverage with `mk_all --check`, and audits transitive axioms with `lake lint`. diff --git a/lean/disaster-recovery-migration/Tests.lean b/lean/disaster-recovery-migration/Tests.lean new file mode 100644 index 000000000000..1555b42e0972 --- /dev/null +++ b/lean/disaster-recovery-migration/Tests.lean @@ -0,0 +1,72 @@ +import DisasterRecoveryMigration.Legacy.Model + +open DisasterRecoveryMigration.Legacy + +private def expect (condition : Bool) (message : String) : IO Unit := + unless condition do throw (IO.userError message) + +private def deliverByKey (n : Nat) (state : GlobalState) (key : String) : Option GlobalState := do + let action <- (actions state).find? (fun action => actionKey action == key) + nextState n state action + +def main : IO UInt32 := do + let single := initialState 1 + expect (single.actors[0]!.nextStep == .open false) + "single node did not open immediately without timeout" + + let initial3 := initialState 3 + let timed <- match nextState 3 initial3 (.timeout 0) with + | some state => pure state + | none => throw (IO.userError "node 0 timeout was suppressed") + expect (timed.actors[0]!.nextStep == .open true) + "timeout did not drive vote and open-join closure to timeout-open" + + let opened := timed.actors[0]! + let lateGossip : Gossip := { src := 2, txid := 2 } + let frozen <- match onMessage 3 0 opened (.gossip lateGossip) with + | some result => pure result + | none => throw (IO.userError "message callback was unexpectedly suppressed") + expect (frozen.1.gossips == opened.gossips) + "gossip collection changed after the vote was submitted" + + let joinActor : ActorState := { + nextStep := .openJoin + gossips := [{ src := 1, txid := 1 }] + votes := [] + submittedVote := none + txid := 1 + } + let joined <- match onMessage 3 1 joinActor (.iAmOpen 0) with + | some result => pure result + | none => throw (IO.userError "IAmOpen was suppressed") + expect (joined.1.nextStep == .join) "IAmOpen did not cause Join" + + let firstOrder <- match deliverByKey 3 initial3 "deliver(1,0,g(1,1))" with + | some state => pure state + | none => throw (IO.userError "first unordered delivery failed") + let firstOrder <- match deliverByKey 3 firstOrder "deliver(2,0,g(2,2))" with + | some state => pure state + | none => throw (IO.userError "second unordered delivery failed") + let secondOrder <- match deliverByKey 3 initial3 "deliver(2,0,g(2,2))" with + | some state => pure state + | none => throw (IO.userError "reverse first unordered delivery failed") + let secondOrder <- match deliverByKey 3 secondOrder "deliver(1,0,g(1,1))" with + | some state => pure state + | none => throw (IO.userError "reverse second unordered delivery failed") + expect (firstOrder == secondOrder) "unordered deliveries produced different states" + + let duplicate : Envelope := { src := 1, dst := 0, msg := .gossip { src := 1, txid := 1 } } + let duplicated := { initial3 with network := duplicate :: duplicate :: initial3.network } + let once <- match nextState 3 duplicated (.deliver duplicate) with + | some state => pure state + | none => throw (IO.userError "first duplicate delivery was suppressed") + expect (once.network.count duplicate + 1 == duplicated.network.count duplicate) + "delivery did not remove exactly one duplicate" + let twice <- match nextState 3 once (.deliver duplicate) with + | some state => pure state + | none => throw (IO.userError "second duplicate delivery was suppressed") + expect (twice.network.count duplicate + 1 == once.network.count duplicate) + "second delivery did not remove exactly one duplicate" + + IO.println "all Lean semantic checks passed" + pure 0 diff --git a/lean/disaster-recovery-migration/compare.py b/lean/disaster-recovery-migration/compare.py new file mode 100755 index 000000000000..005d09c1df5a --- /dev/null +++ b/lean/disaster-recovery-migration/compare.py @@ -0,0 +1,358 @@ +#!/usr/bin/env python3 +# Copyright (c) Microsoft Corporation. All rights reserved. +# Licensed under the Apache 2.0 License. + +import argparse +import filecmp +import subprocess +import sys +import tempfile +from collections import defaultdict, deque +from dataclasses import dataclass +from pathlib import Path + +FORMAT = "ccf-legacy-dr-graph-v1" +PROPERTY_NAMES = ( + "Unanimous votes => no chance of a fork", + "Open", + "Majority votes => no fork", + "No open with timeout, no fork", + "Deadlock", + "Persist committed txs", + "Open is possible", + "Unsafe open with timeout", + "Majority vote still opens without timeout", +) +EXPECTED_COUNTS = { + 1: (1, 0), + 2: (54, 95), + 3: (105558, 552282), +} + + +@dataclass(frozen=True) +class Summary: + initial_key: str + states: int + edges: int + + +@dataclass +class Graph: + initial: str + valuations: dict[str, str] + edges: set[tuple[str, str, str]] + + +def run(command: list[str], cwd: Path, output: Path | None = None) -> None: + print(f"+ (cd {cwd} && {' '.join(command)})", flush=True) + if output is None: + result = subprocess.run( + command, cwd=cwd, text=True, capture_output=True, check=False + ) + else: + with output.open("w", encoding="ascii", newline="") as stream: + result = subprocess.run( + command, + cwd=cwd, + text=True, + stdout=stream, + stderr=subprocess.PIPE, + check=False, + ) + if result.returncode != 0: + if result.stderr: + print(result.stderr, file=sys.stderr, end="") + raise RuntimeError(f"command exited with status {result.returncode}") + + +def validate(path: Path, expected_nodes: int) -> Summary: + ids_to_keys: list[str] = [] + initial_id: int | None = None + edge_count = 0 + previous_edge: tuple[int, str, int] | None = None + section = "header" + + with path.open(encoding="ascii") as stream: + for line_number, raw_line in enumerate(stream, 1): + fields = raw_line.rstrip("\n").split("\t") + if fields == ["format", FORMAT] and line_number == 1: + continue + if fields == ["nodes", str(expected_nodes)] and line_number == 2: + continue + if len(fields) == 2 and fields[0] == "init" and line_number == 3: + initial_id = int(fields[1]) + section = "states" + continue + if len(fields) == 4 and fields[0] == "state" and section == "states": + state_id = int(fields[1]) + if state_id != len(ids_to_keys): + raise ValueError( + f"{path}:{line_number}: expected dense state id " + f"{len(ids_to_keys)}, found {state_id}" + ) + if ids_to_keys and fields[2] <= ids_to_keys[-1]: + raise ValueError( + f"{path}:{line_number}: state keys are unsorted or duplicated" + ) + bits = fields[3] + if len(bits) != len(PROPERTY_NAMES) or set(bits) - {"0", "1"}: + raise ValueError( + f"{path}:{line_number}: invalid property bitstring" + ) + ids_to_keys.append(fields[2]) + continue + if len(fields) == 4 and fields[0] == "edge": + section = "edges" + edge = (int(fields[1]), fields[2], int(fields[3])) + if edge[0] >= len(ids_to_keys) or edge[2] >= len(ids_to_keys): + raise ValueError( + f"{path}:{line_number}: edge references unknown state" + ) + if previous_edge is not None and edge <= previous_edge: + raise ValueError( + f"{path}:{line_number}: edges are unsorted or duplicated" + ) + previous_edge = edge + edge_count += 1 + continue + raise ValueError( + f"{path}:{line_number}: invalid record: {raw_line.rstrip()}" + ) + + if initial_id is None or initial_id >= len(ids_to_keys): + raise ValueError(f"{path}: invalid or missing initial state") + return Summary(ids_to_keys[initial_id], len(ids_to_keys), edge_count) + + +def load(path: Path) -> Graph: + ids_to_keys: list[str] = [] + valuations: dict[str, str] = {} + raw_edges: list[tuple[int, str, int]] = [] + initial_id = -1 + with path.open(encoding="ascii") as stream: + for raw_line in stream: + fields = raw_line.rstrip("\n").split("\t") + if fields[0] == "init": + initial_id = int(fields[1]) + elif fields[0] == "state": + state_id = int(fields[1]) + key = fields[2] + if state_id != len(ids_to_keys): + raise ValueError(f"{path}: non-dense state IDs") + ids_to_keys.append(key) + valuations[key] = fields[3] + elif fields[0] == "edge": + raw_edges.append((int(fields[1]), fields[2], int(fields[3]))) + edges = { + (ids_to_keys[src], action, ids_to_keys[dst]) for src, action, dst in raw_edges + } + return Graph(ids_to_keys[initial_id], valuations, edges) + + +def shortest_paths(graph: Graph) -> tuple[dict[str, int], dict[str, tuple[str, str]]]: + adjacency: dict[str, list[tuple[str, str]]] = defaultdict(list) + for src, action, dst in graph.edges: + adjacency[src].append((action, dst)) + for outgoing in adjacency.values(): + outgoing.sort() + + distance = {graph.initial: 0} + parent: dict[str, tuple[str, str]] = {} + pending = deque([graph.initial]) + while pending: + src = pending.popleft() + for action, dst in adjacency[src]: + if dst not in distance: + distance[dst] = distance[src] + 1 + parent[dst] = (src, action) + pending.append(dst) + return distance, parent + + +def describe_path( + graph: Graph, target: str, cached: tuple[dict[str, int], dict[str, tuple[str, str]]] +) -> str: + distance, parent = cached + if target not in distance: + return f"unreachable target key {target}" + actions: list[str] = [] + cursor = target + while cursor != graph.initial: + cursor, action = parent[cursor] + actions.append(action) + actions.reverse() + rendered = "\n".join( + f" {index}. {action}" for index, action in enumerate(actions, 1) + ) + return f"target: {target}\n{rendered or ' '}" + + +def mismatch(rust: Graph, lean: Graph) -> str: + if rust.initial != lean.initial: + return f"initial state mismatch\nRust: {rust.initial}\nLean: {lean.initial}" + + rust_paths = lean_paths = None + rust_states = set(rust.valuations) + lean_states = set(lean.valuations) + if rust_states != lean_states: + rust_only = rust_states - lean_states + lean_only = lean_states - rust_states + candidates: list[tuple[int, str, str, Graph]] = [] + if rust_only: + rust_paths = shortest_paths(rust) + state = min( + rust_only, key=lambda key: (rust_paths[0].get(key, sys.maxsize), key) + ) + candidates.append( + (rust_paths[0].get(state, sys.maxsize), "Rust-only", state, rust) + ) + if lean_only: + lean_paths = shortest_paths(lean) + state = min( + lean_only, key=lambda key: (lean_paths[0].get(key, sys.maxsize), key) + ) + candidates.append( + (lean_paths[0].get(state, sys.maxsize), "Lean-only", state, lean) + ) + _, side, state, graph = min(candidates) + paths = rust_paths if graph is rust else lean_paths + return ( + f"reachable state mismatch ({len(rust_only)} Rust-only, " + f"{len(lean_only)} Lean-only); shortest is {side}\n" + f"{describe_path(graph, state, paths)}" + ) + + rust_only_edges = rust.edges - lean.edges + lean_only_edges = lean.edges - rust.edges + if rust_only_edges or lean_only_edges: + candidates = [] + if rust_only_edges: + rust_paths = shortest_paths(rust) + edge = min( + rust_only_edges, + key=lambda value: (rust_paths[0].get(value[0], sys.maxsize), value), + ) + candidates.append( + ( + rust_paths[0].get(edge[0], sys.maxsize), + "Rust-only", + edge, + rust, + ) + ) + if lean_only_edges: + lean_paths = shortest_paths(lean) + edge = min( + lean_only_edges, + key=lambda value: (lean_paths[0].get(value[0], sys.maxsize), value), + ) + candidates.append( + ( + lean_paths[0].get(edge[0], sys.maxsize), + "Lean-only", + edge, + lean, + ) + ) + _, side, (src, action, dst), graph = min(candidates) + paths = rust_paths if graph is rust else lean_paths + return ( + f"labeled edge mismatch ({len(rust_only_edges)} Rust-only, " + f"{len(lean_only_edges)} Lean-only); shortest source is {side}\n" + f"{describe_path(graph, src, paths)}\n" + f"missing edge action: {action}\ndestination: {dst}" + ) + + differing = { + key for key in rust_states if rust.valuations[key] != lean.valuations[key] + } + if differing: + rust_paths = shortest_paths(rust) + state = min( + differing, key=lambda key: (rust_paths[0].get(key, sys.maxsize), key) + ) + rust_bits = rust.valuations[state] + lean_bits = lean.valuations[state] + details = [ + f" {index + 1}. {name}: Rust={rust_bits[index]} Lean={lean_bits[index]}" + for index, name in enumerate(PROPERTY_NAMES) + if rust_bits[index] != lean_bits[index] + ] + return ( + f"property valuation mismatch in {len(differing)} states\n" + f"{describe_path(rust, state, rust_paths)}\n" + "\n".join(details) + ) + + return "canonical files differ despite identical graph content" + + +def compare(nodes: int, lean_dir: Path, rust_dir: Path, temporary: Path) -> Summary: + rust_path = temporary / f"rust-{nodes}.tsv" + lean_path = temporary / f"lean-{nodes}.tsv" + run( + [ + "cargo", + "run", + "--quiet", + "--", + "export", + "--nodes", + str(nodes), + "-o", + str(rust_path), + ], + rust_dir, + ) + run( + ["lake", "exe", "migration-exporter", "--nodes", str(nodes)], + lean_dir, + lean_path, + ) + rust_summary = validate(rust_path, nodes) + lean_summary = validate(lean_path, nodes) + if rust_summary != lean_summary or not filecmp.cmp( + rust_path, lean_path, shallow=False + ): + raise AssertionError(mismatch(load(rust_path), load(lean_path))) + expected = EXPECTED_COUNTS.get(nodes) + if expected is not None and (rust_summary.states, rust_summary.edges) != expected: + raise AssertionError( + f"n={nodes}: expected {expected[0]} states/{expected[1]} edges, " + f"found {rust_summary.states}/{rust_summary.edges}" + ) + return rust_summary + + +def main() -> int: + parser = argparse.ArgumentParser( + description="Exhaustively compare Rust/Stateright and Lean legacy DR graphs" + ) + parser.add_argument("--nodes", type=int, nargs="+", default=[1, 2, 3]) + args = parser.parse_args() + if any(nodes < 1 for nodes in args.nodes): + parser.error("node counts must be positive") + + lean_dir = Path(__file__).resolve().parent + rust_dir = lean_dir.parents[1] / "tla" / "disaster-recovery" + try: + scratch = lean_dir / ".lake" + scratch.mkdir(exist_ok=True) + with tempfile.TemporaryDirectory( + prefix="ccf-legacy-dr-", dir=scratch + ) as directory: + for nodes in args.nodes: + summary = compare(nodes, lean_dir, rust_dir, Path(directory)) + print( + f"n={nodes}: equivalent initial state, {summary.states} states, " + f"{summary.edges} labeled edges compared in both directions, " + f"{len(PROPERTY_NAMES)} valuations/state" + ) + except (AssertionError, OSError, RuntimeError, ValueError) as error: + print(f"equivalence failed: {error}", file=sys.stderr) + return 1 + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/lean/disaster-recovery-migration/lake-manifest.json b/lean/disaster-recovery-migration/lake-manifest.json new file mode 100644 index 000000000000..2fcc2ce77743 --- /dev/null +++ b/lean/disaster-recovery-migration/lake-manifest.json @@ -0,0 +1,138 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "type": "path", + "scope": "", + "name": "disaster_recovery", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../disaster-recovery", + "configFile": "lakefile.toml" + }, + { + "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": true, + "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": true, + "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_migration", + "lakeDir": ".lake", + "fixedToolchain": false +} diff --git a/lean/disaster-recovery-migration/lakefile.toml b/lean/disaster-recovery-migration/lakefile.toml new file mode 100644 index 000000000000..2096426c753f --- /dev/null +++ b/lean/disaster-recovery-migration/lakefile.toml @@ -0,0 +1,31 @@ +name = "disaster_recovery_migration" +version = "0.1.0" +moreLeanArgs = ["-DwarningAsError=true"] +# Quote the hyphenated executable name for Lean's name parser. +lintDriver = "axiomAudit/\u00abaxiom-audit\u00bb" +lintDriverArgs = ["--root", "DisasterRecoveryMigration"] +defaultTargets = [ + "DisasterRecoveryMigration", + "migration-model-checker", + "migration-semantic-checks", + "migration-exporter", +] + +[[require]] +name = "disaster_recovery" +path = "../disaster-recovery" + +[[lean_lib]] +name = "DisasterRecoveryMigration" + +[[lean_exe]] +name = "migration-model-checker" +root = "Main" + +[[lean_exe]] +name = "migration-semantic-checks" +root = "Tests" + +[[lean_exe]] +name = "migration-exporter" +root = "ExportMain" diff --git a/lean/disaster-recovery-migration/lean-toolchain b/lean/disaster-recovery-migration/lean-toolchain new file mode 100644 index 000000000000..a8afa7d1b02d --- /dev/null +++ b/lean/disaster-recovery-migration/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.33.1 diff --git a/tla/disaster-recovery/Readme.md b/tla/disaster-recovery/Readme.md index e337787e0027..d13a98b9ac84 100644 --- a/tla/disaster-recovery/Readme.md +++ b/tla/disaster-recovery/Readme.md @@ -9,3 +9,51 @@ The specification can be checked from the command line via `cargo run check`. However, a more useful UX is via the web-view which is hosted locally via `cargo run serve`. This allows you to explore the specification actions interactively, and the checker can be exhaustively run using the `Run to completion` button, which should find several useful examples of states where the network is opened, and where a deadlock is reached. + +## Exporting the state graph + +`cargo run --quiet -- export --nodes [-o ]` exhaustively enumerates the reachable +state graph (via the public `stateright::Model` interface, i.e. `init_states`/`next_steps`) +and writes it to `` (or stdout) in the shared `ccf-legacy-dr-graph-v1` TSV contract, so +it can be diffed against an independent re-implementation of the same model (e.g. in Python +or Lean). The encoder (`src/export.rs`) never uses `Debug` formatting, so output is insulated +from field order, hash-set iteration order, and library-version changes. Full grammar and +design notes are documented in the module doc comment at the top of `src/export.rs`; summary: + +```text +format ccf-legacy-dr-graph-v1 +nodes +init +state (one per reachable state, ascending ) +edge (one per reachable transition, sorted) +``` + +- `` is a dense integer (`0..N_STATES`) assigned by sorting every reachable state's + `` lexicographically -- _not_ BFS/discovery order -- so numbering is a pure + function of the reachable state set. Edges reference states only by `` (not by + repeating ``), since e.g. `n=3` already has 105,558 states / 552,282 edges and + repeating full state keys per edge does not scale. `edge` records are sorted by the tuple + `(, text, )` -- numeric on the ids, lexicographic on the action -- + and de-duplicated. +- `` is 9 chars of `1`/`0`, one per predicate registered via + `ActorModel::property` (`model.properties`), in registration order -- the exact same `fn` + pointers used by `check`/`serve`, so the export can never drift from their semantics. +- `` is `S([ACTORS],[TIMERS],[ENVELOPES])`: `ACTORS` are semicolon-separated + `s(PHASE,[GOSSIPS],[VOTES],SUBMITTED,txid)` records (`PHASE` in `vote`/`openjoin`/`open0`/ + `open1`/`join`), `TIMERS` are the ids of actors with an active election timeout, and + `ENVELOPES` are `e(src,dst,msg)#count` in flight. `history`/`random_choices`/ + `actor_storages` (always the unit value `()` for this model) and `crashed` (always all + `false`, since `max_crashes` is never set above `0`) are omitted, as they carry no + information here. +- `` is `deliver(src,dst,msg)` or `timeout(id,election)`. +- Set elements (`GOSSIPS`, `VOTES`) and `ENVELOPES` are ordered using the real Rust + `#[derive(Ord)]` implementations of `GossipStruct`/`VoteStruct`/`Envelope` (not a + string sort). +- Per `Model::next_state`'s "`None` = no-op" contract, only actions where `next_state` + returns `Some` produce an `edge` line (`Model::next_steps`'s default implementation + already filters these out). + +`--nodes` is an alias for the existing `--n-nodes`/`-n` flag, and (being a global clap +argument) is accepted either before or after the subcommand, so existing invocations +(`cargo run -- --n-nodes 3 check`, `cargo run check`, `cargo run -- --n-nodes 3 serve`) keep +working unchanged alongside `cargo run --quiet -- export --nodes `. diff --git a/tla/disaster-recovery/src/export.rs b/tla/disaster-recovery/src/export.rs new file mode 100644 index 000000000000..e62e4702c8dc --- /dev/null +++ b/tla/disaster-recovery/src/export.rs @@ -0,0 +1,377 @@ +//! Dependency-free canonical export of the reachable state graph. +//! +//! Implements the shared `ccf-legacy-dr-graph-v1` TSV contract: the model is +//! enumerated exhaustively using only the public `stateright::Model` +//! interface (`init_states`, `next_steps`, `within_boundary`), and every +//! state/action is serialized with an explicit hand-written grammar (never +//! `Debug`), so the output is stable across compiler/library versions and +//! diffable byte-for-byte against an independent re-implementation (e.g. +//! Python, Lean) of the same state machine. +//! +//! No new dependencies are introduced: only `stateright` (already a direct +//! dependency) and `std` are used. +//! +//! # Format +//! +//! ```text +//! format\tccf-legacy-dr-graph-v1 +//! nodes\t +//! init\t +//! state\t\t\t (one per reachable state) +//! edge\t\t\t (one per reachable transition) +//! ``` +//! +//! `` is a canonical, dense integer id (`0..N_STATES`) assigned by +//! sorting every reachable state's `` (see below) lexicographically +//! and numbering them in that order -- *not* BFS/discovery order -- so ids are +//! reproducible independent of traversal strategy. `state` records are +//! emitted in ascending `` order (equivalently, ascending `` +//! order). `edge` records are emitted sorted by the tuple +//! `(, text, )` (numeric on the ids, lexicographic on +//! the action text), and de-duplicated. Repeating the full `` in +//! every edge does not scale (e.g. `n=3` already has 105,558 states / 552,282 +//! edges), so edges reference states only by ``; a reader reconstructs the +//! `` for any `` via the `state` block. +//! +//! `` is exactly 9 characters of `1`/`0`, one per predicate +//! currently registered on the model via `ActorModel::property` +//! (`model.properties`), in registration order (liveness, then invariant, +//! then reachable properties -- *not* alphabetical). Each bit is the exact +//! existing `Property::condition` closure evaluated on that state, so the +//! export can never drift from `check`/`serve` behaviour, and preserves each +//! predicate's existing (sometimes misleadingly worded) name/meaning even +//! though names themselves are not repeated in the TSV output. +//! +//! Grammar for ``/`` tokens (no token contains whitespace): +//! +//! - gossip: `g(src,txid)` +//! - vote: `v(src,[GOSSIPS])` where `GOSSIPS` is a comma-separated gossip list +//! - msg: a gossip, a vote, or `o(id)` (`IAmOpen`) +//! - envelope: `e(src,dst,msg)` +//! - submitted vote: `none` or `some(dst,vote)` +//! - actor: `s(PHASE,[GOSSIPS],[VOTES],SUBMITTED,txid)` where `PHASE` is one +//! of `vote`, `openjoin`, `open0` (`Open { timeout: false }`), `open1` +//! (`Open { timeout: true }`), `join` +//! - global state: `S([ACTORS],[TIMERS],[ENVELOPES])` where `ACTORS` is +//! semicolon-separated (positional, by actor index), `TIMERS` is a +//! comma-separated list of actor ids with an active election timeout, and +//! `ENVELOPES` is a comma-separated list of `envelope#count` (count being +//! the in-flight multiplicity of that exact envelope) +//! - action: `deliver(src,dst,msg)` or `timeout(id,election)` +//! +//! `history` (`H = ()`), `random_choices` (`Node::Random = ()`), +//! `actor_storages` (`Node::Storage = ()`), and `crashed` (always all-`false`, +//! since `max_crashes` is never configured above `0`) are all omitted from +//! `S(...)`: for this model they are always constant/empty and carry no +//! information. +//! +//! Set elements (`GOSSIPS`, `VOTES`) are ordered using the actual Rust +//! `#[derive(Ord)]` implementation of `GossipStruct`/`VoteStruct` (not a +//! string sort), and `ENVELOPES` are ordered using `Envelope`'s derived +//! `Ord`. Per `Model::next_state`'s documented contract ("`None` indicates +//! the action does not change state"), only actions for which `next_state` +//! returns `Some` produce an edge; this is preserved by using +//! `Model::next_steps`, whose default implementation already filters out +//! `None` results. + +use crate::model::{GossipStruct, ModelCfg, Msg, NextStep, Node, State, Timer, VoteStruct}; +use stateright::actor::{ + ActorModel, ActorModelAction, ActorModelState, Envelope, Id, Network, Timers, +}; +use stateright::Model; +use std::collections::{HashMap, VecDeque}; +use std::io::{self, Write}; + +const PREDICATE_COUNT: usize = 9; + +fn fmt_id(id: Id) -> String { + usize::from(id).to_string() +} + +fn fmt_gossip(g: &GossipStruct) -> String { + format!("g({},{})", fmt_id(g.src), g.txid) +} + +/// Clones and sorts a gossip set using `GossipStruct`'s derived `Ord` +/// (compares `src` then `txid`), per the shared contract's "sort set +/// elements by Rust derived Ord". +fn sorted_gossips(set: &stateright::util::HashableHashSet) -> Vec { + let mut v: Vec = set.iter().cloned().collect(); + v.sort(); + v +} + +fn fmt_gossip_list(set: &stateright::util::HashableHashSet) -> String { + let items: Vec = sorted_gossips(set).iter().map(fmt_gossip).collect(); + format!("[{}]", items.join(",")) +} + +fn fmt_vote(v: &VoteStruct) -> String { + format!("v({},{})", fmt_id(v.src), fmt_gossip_list(&v.recv)) +} + +/// Clones and sorts a vote set using `VoteStruct`'s derived `Ord` (compares +/// `src` then `recv`). +fn sorted_votes(set: &stateright::util::HashableHashSet) -> Vec { + let mut v: Vec = set.iter().cloned().collect(); + v.sort(); + v +} + +fn fmt_vote_list(set: &stateright::util::HashableHashSet) -> String { + let items: Vec = sorted_votes(set).iter().map(fmt_vote).collect(); + format!("[{}]", items.join(",")) +} + +fn fmt_submitted(sv: &Option<(Id, VoteStruct)>) -> String { + match sv { + None => "none".to_string(), + Some((dst, vote)) => format!("some({},{})", fmt_id(*dst), fmt_vote(vote)), + } +} + +fn fmt_phase(n: &NextStep) -> &'static str { + match n { + NextStep::Vote => "vote", + NextStep::OpenJoin => "openjoin", + NextStep::Open { timeout: false } => "open0", + NextStep::Open { timeout: true } => "open1", + NextStep::Join => "join", + } +} + +fn fmt_actor(s: &State) -> String { + format!( + "s({},{},{},{},{})", + fmt_phase(&s.next_step), + fmt_gossip_list(&s.gossips), + fmt_vote_list(&s.votes), + fmt_submitted(&s.submitted_vote), + s.txid, + ) +} + +fn fmt_msg(m: &Msg) -> String { + match m { + Msg::Gossip(g) => fmt_gossip(g), + Msg::Vote(v) => fmt_vote(v), + Msg::IAmOpen(id) => format!("o({})", fmt_id(*id)), + } +} + +fn fmt_envelope(env: &Envelope) -> String { + format!( + "e({},{},{})", + fmt_id(env.src), + fmt_id(env.dst), + fmt_msg(&env.msg) + ) +} + +/// Tallies in-flight multiplicity per distinct envelope. `Network::iter_all` +/// yields one item per unit of multiplicity regardless of the underlying +/// `Network` variant (this model only ever uses +/// `new_unordered_nonduplicating`, whose internal representation already +/// tracks a count directly), so tallying via `iter_all` is variant-agnostic +/// and stays correct if the network configuration ever changes. +fn network_counts(network: &Network) -> Vec<(Envelope, usize)> { + let mut counts: HashMap, usize> = HashMap::new(); + for env in network.iter_all() { + *counts.entry(env.to_cloned_msg()).or_insert(0) += 1; + } + let mut v: Vec<(Envelope, usize)> = counts.into_iter().collect(); + // Envelope's derived Ord (src, dst, msg), per the shared contract. + v.sort_by(|a, b| a.0.cmp(&b.0)); + v +} + +fn fmt_network(network: &Network) -> String { + let items: Vec = network_counts(network) + .iter() + .map(|(env, count)| format!("{}#{}", fmt_envelope(env), count)) + .collect(); + format!("[{}]", items.join(",")) +} + +/// Comma-separated, ascending list of actor ids with an active election +/// timeout. `Timer` currently has a single variant, so presence alone is +/// significant (no timer-kind tag is emitted). +fn fmt_timers(timers_set: &[Timers]) -> String { + let mut ids: Vec = timers_set + .iter() + .enumerate() + .filter(|(_, t)| t.iter().next().is_some()) + .map(|(i, _)| i) + .collect(); + ids.sort_unstable(); + let items: Vec = ids.iter().map(|i| i.to_string()).collect(); + format!("[{}]", items.join(",")) +} + +/// Canonical `S(...)` encoding of a full `ActorModelState`. Used both +/// as the state field in `state` records and as the basis of the canonical +/// state id, so two independent implementations that compute the same +/// reachable state always produce the same key, regardless of traversal order. +pub fn fmt_state(state: &ActorModelState) -> String { + let actors: Vec = state.actor_states.iter().map(|s| fmt_actor(s)).collect(); + format!( + "S([{}],{},{})", + actors.join(";"), + fmt_timers(&state.timers_set), + fmt_network(&state.network), + ) +} + +/// Canonical encoding of an `ActorModelAction`. Only `Deliver` and `Timeout` +/// are part of the `ccf-legacy-dr-graph-v1` contract: this model never +/// produces `Drop` (`LossyNetwork::No`), `Crash`/`Recover` (`max_crashes == +/// 0`), or `SelectRandom` (no `Actor` ever issues a `ChooseRandom` command), +/// so encountering one is a bug (e.g. a future model config change) rather +/// than a case the contract needs to define. +pub fn fmt_action(action: &ActorModelAction) -> String { + match action { + ActorModelAction::Deliver { src, dst, msg } => { + format!( + "deliver({},{},{})", + fmt_id(*src), + fmt_id(*dst), + fmt_msg(msg) + ) + } + ActorModelAction::Timeout(id, Timer::ElectionTimeout) => { + format!("timeout({},election)", fmt_id(*id)) + } + _ => unreachable!( + "action variant is outside the ccf-legacy-dr-graph-v1 contract \ + (only Deliver/Timeout are ever produced by this model's configuration)" + ), + } +} + +/// The 9-character `1`/`0` bitstring for `state`, one bit per predicate +/// currently registered on `model` (`model.properties`) in registration +/// order -- i.e. exactly the same `fn` pointers used by `check`/`serve`, so +/// this can never drift from their semantics. +fn predicate_bitstring( + model: &ActorModel, + state: &ActorModelState, +) -> String { + model + .properties + .iter() + .map(|p| { + if (p.condition)(model, state) { + '1' + } else { + '0' + } + }) + .collect() +} + +/// Exhaustively enumerates the reachable state graph of `model` via the +/// public `stateright::Model` interface (`init_states`, `next_steps`, +/// `within_boundary`) and writes it to `out` as `ccf-legacy-dr-graph-v1`. +/// +/// States are discovered by BFS (for traversal only), but ``s are +/// assigned afterwards by sorting all discovered ``s +/// lexicographically -- so the numbering is a pure function of the reachable +/// state set, independent of traversal order. Edges reference states by +/// `` only, keeping output size linear in (states + edges) rather than +/// (edges * average state size). +pub fn export_graph( + model: &ActorModel, + out: &mut W, +) -> io::Result<()> { + assert_eq!( + model.properties.len(), + PREDICATE_COUNT, + "ccf-legacy-dr-graph-v1 requires exactly {PREDICATE_COUNT} registered model properties" + ); + + // Indexed by BFS discovery order (a "discovery id"); remapped to the + // canonical sorted-key id only once the full state set is known. + let mut visited: HashMap, usize> = HashMap::new(); + let mut keys: Vec = Vec::new(); + let mut bits: Vec = Vec::new(); + let mut frontier: VecDeque> = VecDeque::new(); + // (discovery src id, action text, discovery dst id) + let mut edges: Vec<(usize, String, usize)> = Vec::new(); + + let mut init_states = model.init_states(); + assert_eq!( + init_states.len(), + 1, + "ccf-legacy-dr-graph-v1 assumes a single deterministic init state" + ); + let init_state = init_states.remove(0); + assert!( + model.within_boundary(&init_state), + "ccf-legacy-dr-graph-v1 assumes the init state is within the model boundary" + ); + let init_discovery_id = keys.len(); + keys.push(fmt_state(&init_state)); + bits.push(predicate_bitstring(model, &init_state)); + visited.insert(init_state.clone(), init_discovery_id); + frontier.push_back(init_state); + + while let Some(s) = frontier.pop_front() { + let src_discovery_id = *visited + .get(&s) + .expect("every frontier state was inserted into `visited` before being queued"); + // `next_steps` (default `Model` trait method) already filters out + // actions for which `next_state` returns `None`, preserving the + // documented no-op-suppression contract. + for (action, ns) in model.next_steps(&s) { + if !model.within_boundary(&ns) { + continue; + } + let action_key = fmt_action(&action); + let dst_discovery_id = if let Some(&id) = visited.get(&ns) { + id + } else { + let id = keys.len(); + keys.push(fmt_state(&ns)); + bits.push(predicate_bitstring(model, &ns)); + visited.insert(ns.clone(), id); + frontier.push_back(ns); + id + }; + edges.push((src_discovery_id, action_key, dst_discovery_id)); + } + } + + // Canonical id assignment: number every discovered state by the + // lexicographic order of its ``, not by discovery order. + let mut order: Vec = (0..keys.len()).collect(); + order.sort_by(|&a, &b| keys[a].cmp(&keys[b])); + let mut canonical_id: Vec = vec![0; keys.len()]; + for (id, &discovery_id) in order.iter().enumerate() { + canonical_id[discovery_id] = id; + } + + // Remap edges to canonical ids, then sort by (SRC_ID, ACTION, DST_ID) -- + // numeric on the ids (real `usize` comparison, not string comparison), + // lexicographic on the action text -- and de-duplicate. + let mut canonical_edges: Vec<(usize, String, usize)> = edges + .into_iter() + .map(|(src, action, dst)| (canonical_id[src], action, canonical_id[dst])) + .collect(); + canonical_edges.sort(); + canonical_edges.dedup(); + + writeln!(out, "format\tccf-legacy-dr-graph-v1")?; + writeln!(out, "nodes\t{}", model.actors.len())?; + writeln!(out, "init\t{}", canonical_id[init_discovery_id])?; + for (id, &discovery_id) in order.iter().enumerate() { + writeln!( + out, + "state\t{}\t{}\t{}", + id, keys[discovery_id], bits[discovery_id] + )?; + } + for (src, action, dst) in &canonical_edges { + writeln!(out, "edge\t{src}\t{action}\t{dst}")?; + } + Ok(()) +} diff --git a/tla/disaster-recovery/src/main.rs b/tla/disaster-recovery/src/main.rs index d92767d1a0f0..15bcef28f7ad 100644 --- a/tla/disaster-recovery/src/main.rs +++ b/tla/disaster-recovery/src/main.rs @@ -1,7 +1,9 @@ extern crate clap; extern crate stateright; use clap::Parser; +mod export; mod model; +use export::export_graph; use model::{ModelCfg, Msg, NextStep, Node, State}; use stateright::{actor::*, report::WriteReporter, util::HashableHashSet, Checker, Model}; use std::sync::Arc; @@ -198,7 +200,11 @@ fn properties(model: ActorModel) -> ActorModel, + }, } fn check(model: ActorModel) { @@ -227,6 +241,21 @@ fn serve(model: ActorModel) { checker.serve("localhost:8080"); } +fn export(model: ActorModel, out: Option) { + match out { + Some(path) => { + let mut file = std::fs::File::create(&path) + .unwrap_or_else(|e| panic!("failed to create '{}': {}", path, e)); + export_graph(&model, &mut file).expect("failed to write model export"); + } + None => { + let stdout = std::io::stdout(); + let mut handle = stdout.lock(); + export_graph(&model, &mut handle).expect("failed to write model export"); + } + } +} + fn main() { let args = CliArgs::parse(); @@ -240,5 +269,6 @@ fn main() { match args.command { Commands::Check => check(model), Commands::Serve => serve(model), + Commands::Export { out } => export(model, out), } }