diff --git a/.github/workflows/ci-verification.yml b/.github/workflows/ci-verification.yml index 1a72ca4feb9..71bf6fa49b8 100644 --- a/.github/workflows/ci-verification.yml +++ b/.github/workflows/ci-verification.yml @@ -243,24 +243,34 @@ jobs: path: | tla/traces/* - model-checking-self-healing-open: - name: Model Checking - Self-Healing Open - runs-on: [self-hosted, 1ES.Pool=gha-vmss-d16av6-ci] - container: - image: mcr.microsoft.com/azurelinux/base/core:3.0 - options: --user root --publish-all --cap-add NET_ADMIN --cap-add NET_RAW --cap-add SYS_PTRACE + lean-disaster-recovery: + name: Lean Disaster Recovery - Canonical Model + runs-on: ubuntu-latest + timeout-minutes: 30 steps: - - name: "Checkout dependencies" + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + + - name: Install Lean shell: bash run: | - gpg --import /etc/pki/rpm-gpg/MICROSOFT-RPM-GPG-KEY - tdnf -y update - tdnf -y install ca-certificates git + set -euo pipefail + sudo apt-get update + sudo apt-get install -y elan + elan toolchain install "$(cat lean/disaster-recovery/lean-toolchain)" - - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - - name: Install Stateright dependencies + - name: Restore Mathlib cache + working-directory: lean/disaster-recovery + shell: bash run: | - tdnf install -y cargo + set -euo pipefail + lake exe cache get - - run: cd tla/disaster-recovery && cargo run check + - name: Build and check canonical model + working-directory: lean/disaster-recovery + shell: bash + run: | + set -euo pipefail + lake build + lake env lean -DwarningAsError=true AxiomChecks.lean + lake exe canonical-checks diff --git a/.github/workflows/lean-disaster-recovery-migration.yml b/.github/workflows/lean-disaster-recovery-migration.yml deleted file mode 100644 index f559e52bb22..00000000000 --- a/.github/workflows/lean-disaster-recovery-migration.yml +++ /dev/null @@ -1,71 +0,0 @@ -name: "Lean Disaster Recovery Migration Evidence" - -on: - pull_request: - paths: - - "lean/disaster-recovery/**" - - "lean/disaster-recovery-migration/**" - - "tla/disaster-recovery/**" - - ".github/workflows/lean-disaster-recovery-migration.yml" - -concurrency: - group: ${{ github.workflow }}-${{ github.ref }} - cancel-in-progress: true - -permissions: read-all - -jobs: - 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: Check canonical Lean package - working-directory: lean/disaster-recovery - shell: bash - run: | - set -euo pipefail - lake exe cache get - lake build - lake env lean -DwarningAsError=true AxiomChecks.lean - lake exe canonical-checks - - - name: Build and check migration Lean package - working-directory: lean/disaster-recovery-migration - shell: bash - run: | - set -euo pipefail - lake exe cache get - lake build - lake env lean -DwarningAsError=true AxiomChecks.lean - 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/.gitignore b/lean/disaster-recovery-migration/.gitignore deleted file mode 100644 index 4080d07dfc3..00000000000 --- a/lean/disaster-recovery-migration/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/.lake/ diff --git a/lean/disaster-recovery-migration/AxiomChecks.lean b/lean/disaster-recovery-migration/AxiomChecks.lean deleted file mode 100644 index 689bd7be343..00000000000 --- a/lean/disaster-recovery-migration/AxiomChecks.lean +++ /dev/null @@ -1,27 +0,0 @@ -import DisasterRecovery -import DisasterRecoveryMigration -import Lean.Elab.Command -import Lean.Util.CollectAxioms - -open Lean Elab Command - -elab "#assert_no_migration_sorries" : command => do - let env <- getEnv - let mut offenders : Array Name := #[] - for (name, _) in env.constants.toList do - let projectDeclaration := - match env.getModuleIdxFor? name with - | none => false - | some index => - env.header.moduleNames[index.toNat]!.toString.startsWith "DisasterRecovery" - if projectDeclaration then - let axioms <- liftCoreM <| Lean.collectAxioms name - if axioms.contains (Name.mkSimple "sorryAx") then - offenders := offenders.push name - unless offenders.isEmpty do - throwError "declarations contain sorryAx: {offenders}" - -#assert_no_migration_sorries - -def main : IO Unit := - pure () diff --git a/lean/disaster-recovery-migration/DisasterRecoveryMigration.lean b/lean/disaster-recovery-migration/DisasterRecoveryMigration.lean deleted file mode 100644 index c1479820c03..00000000000 --- a/lean/disaster-recovery-migration/DisasterRecoveryMigration.lean +++ /dev/null @@ -1,3 +0,0 @@ -import DisasterRecoveryMigration.Legacy.Model -import DisasterRecoveryMigration.Legacy.Checker -import DisasterRecoveryMigration.Refinement diff --git a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean b/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean deleted file mode 100644 index 659daef0354..00000000000 --- a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Checker.lean +++ /dev/null @@ -1,152 +0,0 @@ -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 deleted file mode 100644 index 91000ae2f1b..00000000000 --- a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Legacy/Model.lean +++ /dev/null @@ -1,392 +0,0 @@ -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 deleted file mode 100644 index b339e8d17aa..00000000000 --- a/lean/disaster-recovery-migration/DisasterRecoveryMigration/Refinement.lean +++ /dev/null @@ -1,335 +0,0 @@ -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 - -def retryCompatibility - (config : Config) - (state : NodeState) : - CompatibilityStep config state .retry state := { - canonical := rfl -} - -def 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 deleted file mode 100644 index f7500f6a967..00000000000 --- a/lean/disaster-recovery-migration/ExportMain.lean +++ /dev/null @@ -1,24 +0,0 @@ -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 deleted file mode 100644 index c943598da3b..00000000000 --- a/lean/disaster-recovery-migration/Main.lean +++ /dev/null @@ -1,23 +0,0 @@ -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 deleted file mode 100644 index 25976e5a701..00000000000 --- a/lean/disaster-recovery-migration/README.md +++ /dev/null @@ -1,111 +0,0 @@ -# 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 its dedicated workflow are intended to be -deleted wholesale by PR 3 once the migration 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 | -| `AxiomChecks.lean` | `sorryAx` rejection for loaded migration and canonical declarations | -| `compare.py` | Bidirectional exhaustive Rust/Lean comparison | - -## Validation - -Run from this directory: - -```console -lake exe cache get -lake build -lake exe migration-semantic-checks -lake exe migration-model-checker --nodes 3 -lake env lean -DwarningAsError=true AxiomChecks.lean -python3 compare.py --nodes 1 2 3 -``` - -The canonical package's own `AxiomChecks.lean` remains authoritative for all -canonical declarations and is also run by the dedicated migration workflow. -The migration Lake package pins the same Lean toolchain, transitively resolves -the same Mathlib revision, and treats warnings as errors. diff --git a/lean/disaster-recovery-migration/Tests.lean b/lean/disaster-recovery-migration/Tests.lean deleted file mode 100644 index 1555b42e097..00000000000 --- a/lean/disaster-recovery-migration/Tests.lean +++ /dev/null @@ -1,72 +0,0 @@ -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 deleted file mode 100755 index 005d09c1df5..00000000000 --- a/lean/disaster-recovery-migration/compare.py +++ /dev/null @@ -1,358 +0,0 @@ -#!/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 deleted file mode 100644 index b3664513dd6..00000000000 --- a/lean/disaster-recovery-migration/lake-manifest.json +++ /dev/null @@ -1,125 +0,0 @@ -{ - "version": "1.1.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/mathlib4.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", - "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": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", - "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": "85b59af46828c029a9168f2f9c35119bd0721e6e", - "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": "be3b2e63b1bbf496c478cef98b86972a37c1417d", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.87", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", - "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": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", - "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": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", - "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": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0", - "inherited": true, - "configFile": "lakefile.toml" - } - ], - "name": "disaster_recovery_migration", - "lakeDir": ".lake" -} diff --git a/lean/disaster-recovery-migration/lakefile.toml b/lean/disaster-recovery-migration/lakefile.toml deleted file mode 100644 index d9c53898bb4..00000000000 --- a/lean/disaster-recovery-migration/lakefile.toml +++ /dev/null @@ -1,28 +0,0 @@ -name = "disaster_recovery_migration" -version = "0.1.0" -moreLeanArgs = ["-DwarningAsError=true"] -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 deleted file mode 100644 index 4c685fa085f..00000000000 --- a/lean/disaster-recovery-migration/lean-toolchain +++ /dev/null @@ -1 +0,0 @@ -leanprover/lean4:v4.28.0 diff --git a/tla/disaster-recovery/.gitignore b/tla/disaster-recovery/.gitignore deleted file mode 100644 index eb5a316cbd1..00000000000 --- a/tla/disaster-recovery/.gitignore +++ /dev/null @@ -1 +0,0 @@ -target diff --git a/tla/disaster-recovery/Cargo.lock b/tla/disaster-recovery/Cargo.lock deleted file mode 100644 index 9666614b5e3..00000000000 --- a/tla/disaster-recovery/Cargo.lock +++ /dev/null @@ -1,592 +0,0 @@ -# This file is automatically @generated by Cargo. -# It is not intended for manual editing. -version = 4 - -[[package]] -name = "ahash" -version = "0.8.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a15f179cd60c4584b8a8c596927aadc462e27f2ca70c04e0071964a73ba7a75" -dependencies = [ - "cfg-if", - "getrandom", - "once_cell", - "version_check", - "zerocopy", -] - -[[package]] -name = "anstream" -version = "0.6.19" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "301af1932e46185686725e0fad2f8f2aa7da69dd70bf6ecc44d6b703844a3933" -dependencies = [ - "anstyle", - "anstyle-parse", - "anstyle-query", - "anstyle-wincon", - "colorchoice", - "is_terminal_polyfill", - "utf8parse", -] - -[[package]] -name = "anstyle" -version = "1.0.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "862ed96ca487e809f1c8e5a8447f6ee2cf102f846893800b20cebdf541fc6bbd" - -[[package]] -name = "anstyle-parse" -version = "0.2.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e7644824f0aa2c7b9384579234ef10eb7efb6a0deb83f9630a49594dd9c15c2" -dependencies = [ - "utf8parse", -] - -[[package]] -name = "anstyle-query" -version = "1.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c8bdeb6047d8983be085bab0ba1472e6dc604e7041dbf6fcd5e71523014fae9" -dependencies = [ - "windows-sys", -] - -[[package]] -name = "anstyle-wincon" -version = "3.0.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "403f75924867bb1033c59fbf0797484329750cfbe3c4325cd33127941fabc882" -dependencies = [ - "anstyle", - "once_cell_polyfill", - "windows-sys", -] - -[[package]] -name = "ascii" -version = "1.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d92bec98840b8f03a5ff5413de5293bfcd8bf96467cf5452609f939ec6f5de16" - -[[package]] -name = "autocfg" -version = "1.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" - -[[package]] -name = "bitflags" -version = "2.9.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b8e56985ec62d17e9c1001dc89c88ecd7dc08e47eba5ec7c29c7b5eeecde967" - -[[package]] -name = "ccf-selfhealingopen" -version = "0.0.0" -dependencies = [ - "clap", - "stateright", -] - -[[package]] -name = "cfg-if" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" - -[[package]] -name = "choice" -version = "0.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a3b71fc821deaf602a933ada5c845d088156d0cdf2ebf43ede390afe93466553" - -[[package]] -name = "chunked_transfer" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6e4de3bc4ea267985becf712dc6d9eed8b04c953b3fcfb339ebc87acd9804901" - -[[package]] -name = "clap" -version = "4.5.40" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "40b6887a1d8685cebccf115538db5c0efe625ccac9696ad45c409d96566e910f" -dependencies = [ - "clap_builder", - "clap_derive", -] - -[[package]] -name = "clap_builder" -version = "4.5.40" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e0c66c08ce9f0c698cbce5c0279d0bb6ac936d8674174fe48f736533b964f59e" -dependencies = [ - "anstream", - "anstyle", - "clap_lex", - "strsim", -] - -[[package]] -name = "clap_derive" -version = "4.5.40" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2c7947ae4cc3d851207c1adb5b5e260ff0cca11446b1d6d1423788e442257ce" -dependencies = [ - "heck", - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "clap_lex" -version = "0.7.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b94f61472cee1439c0b966b47e3aca9ae07e45d070759512cd390ea2bebc6675" - -[[package]] -name = "colorchoice" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75" - -[[package]] -name = "crossbeam-utils" -version = "0.8.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" - -[[package]] -name = "dashmap" -version = "6.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5041cc499144891f3790297212f32a74fb938e5136a14943f338ef9e0ae276cf" -dependencies = [ - "cfg-if", - "crossbeam-utils", - "hashbrown", - "lock_api", - "once_cell", - "parking_lot_core", -] - -[[package]] -name = "getrandom" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26145e563e54f2cadc477553f1ec5ee650b00862f0a58bcd12cbdc5f0ea2d2f4" -dependencies = [ - "cfg-if", - "libc", - "r-efi", - "wasi", -] - -[[package]] -name = "hashbrown" -version = "0.14.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" - -[[package]] -name = "heck" -version = "0.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" - -[[package]] -name = "httpdate" -version = "1.0.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "df3b46402a9d5adb4c86a0cf463f42e19994e3ee891101b1841f30a545cb49a9" - -[[package]] -name = "id-set" -version = "0.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9633fadf6346456cf8531119ba4838bc6d82ac4ce84d9852126dd2aa34d49264" - -[[package]] -name = "is_terminal_polyfill" -version = "1.70.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" - -[[package]] -name = "itoa" -version = "1.0.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4a5f13b858c8d314ee3e8f639011f7ccefe71f97f96e50151fb991f267928e2c" - -[[package]] -name = "libc" -version = "0.2.173" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d8cfeafaffdbc32176b64fb251369d52ea9f0a8fbc6f8759edffef7b525d64bb" - -[[package]] -name = "lock_api" -version = "0.4.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "96936507f153605bddfcda068dd804796c84324ed2510809e5b2a624c81da765" -dependencies = [ - "autocfg", - "scopeguard", -] - -[[package]] -name = "log" -version = "0.4.27" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "13dc2df351e3202783a1fe0d44375f7295ffb4049267b0f3018346dc122a1d94" - -[[package]] -name = "memchr" -version = "2.7.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a282da65faaf38286cf3be983213fcf1d2e2a58700e808f83f4ea9a4804bc0" - -[[package]] -name = "nohash-hasher" -version = "0.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2bf50223579dc7cdcfb3bfcacf7069ff68243f8c363f62ffa99cf000a6b9c451" - -[[package]] -name = "once_cell" -version = "1.21.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "42f5e15c9953c5e4ccceeb2e7382a716482c34515315f7b03532b8b4e8393d2d" - -[[package]] -name = "once_cell_polyfill" -version = "1.70.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a4895175b425cb1f87721b59f0f286c2092bd4af812243672510e1ac53e2e0ad" - -[[package]] -name = "parking_lot" -version = "0.12.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70d58bf43669b5795d1576d0641cfb6fbb2057bf629506267a92807158584a13" -dependencies = [ - "lock_api", - "parking_lot_core", -] - -[[package]] -name = "parking_lot_core" -version = "0.9.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bc838d2a56b5b1a6c25f55575dfc605fabb63bb2365f6c2353ef9159aa69e4a5" -dependencies = [ - "cfg-if", - "libc", - "redox_syscall", - "smallvec", - "windows-targets", -] - -[[package]] -name = "ppv-lite86" -version = "0.2.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" -dependencies = [ - "zerocopy", -] - -[[package]] -name = "proc-macro2" -version = "1.0.95" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "02b3e5e68a3a1a02aad3ec490a98007cbc13c37cbe84a3cd7b8e406d76e7f778" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "quote" -version = "1.0.40" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1885c039570dc00dcb4ff087a89e185fd56bae234ddc7f056a945bf36467248d" -dependencies = [ - "proc-macro2", -] - -[[package]] -name = "r-efi" -version = "5.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74765f6d916ee2faa39bc8e68e4f3ed8949b48cccdac59983d287a7cb71ce9c5" - -[[package]] -name = "rand" -version = "0.9.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" -dependencies = [ - "rand_chacha", - "rand_core", -] - -[[package]] -name = "rand_chacha" -version = "0.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" -dependencies = [ - "ppv-lite86", - "rand_core", -] - -[[package]] -name = "rand_core" -version = "0.9.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "99d9a13982dcf210057a8a78572b2217b667c3beacbf3a0d8b454f6f82837d38" -dependencies = [ - "getrandom", -] - -[[package]] -name = "redox_syscall" -version = "0.5.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d04b7d0ee6b4a0207a0a7adb104d23ecb0b47d6beae7152d0fa34b692b29fd6" -dependencies = [ - "bitflags", -] - -[[package]] -name = "ryu" -version = "1.0.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28d3b2b1366ec20994f1fd18c3c594f05c5dd4bc44d8bb0c1c632c8d6829481f" - -[[package]] -name = "scopeguard" -version = "1.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" - -[[package]] -name = "serde" -version = "1.0.219" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f0e2c6ed6606019b4e29e69dbaba95b11854410e5347d525002456dbbb786b6" -dependencies = [ - "serde_derive", -] - -[[package]] -name = "serde_derive" -version = "1.0.219" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b0276cf7f2c73365f7157c8123c21cd9a50fbbd844757af28ca1f5925fc2a00" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] - -[[package]] -name = "serde_json" -version = "1.0.140" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "20068b6e96dc6c9bd23e01df8827e6c7e1f2fddd43c21810382803c136b99373" -dependencies = [ - "itoa", - "memchr", - "ryu", - "serde", -] - -[[package]] -name = "smallvec" -version = "1.15.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" - -[[package]] -name = "stateright" -version = "0.31.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fd1157f21b11916f90fe1f2ac9a8d0e09a8813b28701584141060f414eedf6ba" -dependencies = [ - "ahash", - "choice", - "crossbeam-utils", - "dashmap", - "id-set", - "log", - "nohash-hasher", - "parking_lot", - "rand", - "serde", - "serde_json", - "tiny_http", -] - -[[package]] -name = "strsim" -version = "0.11.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" - -[[package]] -name = "syn" -version = "2.0.103" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e4307e30089d6fd6aff212f2da3a1f9e32f3223b1f010fb09b7c95f90f3ca1e8" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "tiny_http" -version = "0.12.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "389915df6413a2e74fb181895f933386023c71110878cd0825588928e64cdc82" -dependencies = [ - "ascii", - "chunked_transfer", - "httpdate", - "log", -] - -[[package]] -name = "unicode-ident" -version = "1.0.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a5f39404a5da50712a4c1eecf25e90dd62b613502b7e925fd4e4d19b5c96512" - -[[package]] -name = "utf8parse" -version = "0.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" - -[[package]] -name = "version_check" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - -[[package]] -name = "wasi" -version = "0.14.2+wasi-0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9683f9a5a998d873c0d21fcbe3c083009670149a8fab228644b8bd36b2c48cb3" -dependencies = [ - "wit-bindgen-rt", -] - -[[package]] -name = "windows-sys" -version = "0.59.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets", -] - -[[package]] -name = "windows-targets" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" -dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", -] - -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" - -[[package]] -name = "windows_aarch64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" - -[[package]] -name = "windows_i686_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" - -[[package]] -name = "windows_i686_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" - -[[package]] -name = "windows_i686_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" - -[[package]] -name = "windows_x86_64_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" - -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" - -[[package]] -name = "windows_x86_64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" - -[[package]] -name = "wit-bindgen-rt" -version = "0.39.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f42320e61fe2cfd34354ecb597f86f413484a798ba44a8ca1165c58d42da6c1" -dependencies = [ - "bitflags", -] - -[[package]] -name = "zerocopy" -version = "0.8.25" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1702d9583232ddb9174e01bb7c15a2ab8fb1bc6f227aa1233858c351a3ba0cb" -dependencies = [ - "zerocopy-derive", -] - -[[package]] -name = "zerocopy-derive" -version = "0.8.25" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28a6e20d751156648aa063f3800b706ee209a32c0b4d9f24be3d980b01be55ef" -dependencies = [ - "proc-macro2", - "quote", - "syn", -] diff --git a/tla/disaster-recovery/Cargo.toml b/tla/disaster-recovery/Cargo.toml deleted file mode 100644 index 92950edbfb1..00000000000 --- a/tla/disaster-recovery/Cargo.toml +++ /dev/null @@ -1,7 +0,0 @@ -[package] -name = "ccf-selfhealingopen" -version = "0.0.0" - -[dependencies] -clap = { version = "4.5.38", features = ["derive"] } -stateright = "0.31.0" diff --git a/tla/disaster-recovery/Readme.md b/tla/disaster-recovery/Readme.md deleted file mode 100644 index d13a98b9ac8..00000000000 --- a/tla/disaster-recovery/Readme.md +++ /dev/null @@ -1,59 +0,0 @@ -# Self-healing-open specification in [stateright](https://github.com/stateright/stateright) - -The properties are specified in [main.rs](./src/main.rs), while the model is specified in [model.rs](./src/model.rs). - -Due to stateright being executable, there is little syntactic sugar, and so there is quite a bit of boilerplate. -The functional parts of the specification are in `advance_step`, `on_start`, `on_timeout` and `on_msg`. - -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 deleted file mode 100644 index e62e4702c8d..00000000000 --- a/tla/disaster-recovery/src/export.rs +++ /dev/null @@ -1,377 +0,0 @@ -//! 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 deleted file mode 100644 index 15bcef28f7a..00000000000 --- a/tla/disaster-recovery/src/main.rs +++ /dev/null @@ -1,274 +0,0 @@ -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; - -fn implies(a: bool, b: bool) -> bool { - !a || b -} - -fn reached_open(state: &ActorModelState) -> bool { - state - .actor_states - .iter() - .any(|actor_state: &Arc| matches!(actor_state.next_step, NextStep::Open { .. })) -} - -fn reached_open_timeout(state: &ActorModelState, expected_to_timeout: bool) -> bool { - state.actor_states.iter().any(|actor_state: &Arc| { - matches! ( - actor_state.next_step, - NextStep::Open {timeout} if timeout == expected_to_timeout - ) - }) -} - -fn unanimous_votes(model: &ActorModel, state: &ActorModelState) -> bool { - let peers: HashableHashSet = (0..model.cfg.n_nodes) - .map(|i| Id::from(i as usize)) - .collect(); - state.actor_states.iter().all(|actor_state: &Arc| { - actor_state.submitted_vote.is_some() - && peers.iter().all(|peer| { - actor_state - .submitted_vote - .clone() - .unwrap() - .1 - .recv - .iter() - .any(|g| g.src == *peer) - }) - }) -} - -fn majority_have_same_maximum(state: &ActorModelState) -> bool { - // get the chosen replica of each replica into a vector and sort that vector - // that there is only one value up to the n/2th index - let mut chosen_replicas: Vec = state - .actor_states - .iter() - .filter(|actor_state: &&Arc| actor_state.submitted_vote.is_some()) - .map(|actor_state| { - actor_state - .submitted_vote - .clone() - .unwrap() - .1 - .recv - .iter() - .max_by_key(|g| (g.txid, g.src)) - .unwrap() - .src - }) - .collect(); - chosen_replicas.sort(); - let majority_idx = state.actor_states.len() / 2; - let majority_chosen_replica = chosen_replicas.get(majority_idx); - majority_chosen_replica.is_some() - && chosen_replicas[0..majority_idx] - .iter() - .all(|&r| r == *majority_chosen_replica.unwrap()) -} - -fn liveness_properties(model: ActorModel) -> ActorModel { - let model = model - .property( - stateright::Expectation::Eventually, - "Unanimous votes => no chance of a fork", - |model: &ActorModel, state: &ActorModelState| { - // Define deadlock as a path which does not reach open without - // Hence unanimous votes => reach open - // Hence on every path unanimous votes => <> reached open - // Since votes are not forgotten on a node, we check for a state where unanimous votes => reached open - return implies( - unanimous_votes(model, state), - reached_open_timeout(state, false), - ); - }, - ) - .property( - stateright::Expectation::Eventually, - "Open", - |_, state: &ActorModelState| { - // all runs should eventually open, either via the reliable method, or via the failover timeout - reached_open(state) - }, - ) - .property( - stateright::Expectation::Eventually, - "Majority votes => no fork", - |_, state: &ActorModelState| { - return implies( - majority_have_same_maximum(state), - reached_open_timeout(state, false), - ); - }, - ); - return model; -} - -fn invariant_properties(model: ActorModel) -> ActorModel { - let model = model - .property( - stateright::Expectation::Always, - "No open with timeout, no fork", - |_model: &ActorModel, state: &ActorModelState| { - // Check if there is no fork in the state - let open_node_count = state - .actor_states - .iter() - .filter(|actor_state: &&Arc| { - matches!(actor_state.next_step, NextStep::Open { .. }) - }) - .count(); - implies(!reached_open_timeout(state, true), open_node_count <= 1) - }, - ) - .property( - stateright::Expectation::Always, - "Deadlock", - |_model, state| { - let all_open_join = state - .actor_states - .iter() - .all(|actor_state: &Arc| actor_state.next_step == NextStep::OpenJoin); - let all_votes_delivered = state - .network - .iter_all() - .filter(|msg| matches!(msg.msg, Msg::Vote(_))) - .count() - == 0; - !(all_open_join && all_votes_delivered) - }, - ) - .property( - stateright::Expectation::Always, - "Persist committed txs", - |_model: &ActorModel, state: &ActorModelState| { - let majority_idx = state.actor_states.len() / 2; - let commit_txid = state - .actor_states - .iter() - .map(|actor_state| actor_state.txid) - .collect::>()[majority_idx]; - let cond = state - .actor_states - .iter() - .filter(|actor_state: &&Arc| { - matches!(actor_state.next_step, NextStep::Open { .. }) - }) - .all(|actor_state: &Arc| actor_state.txid >= commit_txid); - implies(!reached_open_timeout(state, true), cond) - }, - ); - return model; -} - -fn reachable_properties(model: ActorModel) -> ActorModel { - let model = model - .property( - stateright::Expectation::Sometimes, - "Open is possible", - |_, state| implies(state.actor_states.len() > 1, reached_open(state)), - ) - .property( - stateright::Expectation::Sometimes, - "Unsafe open with timeout", - |_, state| reached_open_timeout(state, true), - ) - .property( - stateright::Expectation::Sometimes, - "Majority vote still opens without timeout", - |_model, state| majority_have_same_maximum(state) && reached_open_timeout(state, false), - ); - return model; -} - -fn properties(model: ActorModel) -> ActorModel { - let model = liveness_properties(model); - let model = invariant_properties(model); - let model = reachable_properties(model); - return model; -} - -#[derive(Parser, Debug)] -#[command(version, about = "Model for CCF's self-healing-open", long_about = None)] -struct CliArgs { - /// `global = true` lets this be given either before or after the - /// subcommand (e.g. `--n-nodes 3 check` or `export --nodes 3`); the - /// `nodes` alias matches the shared exporter invocation - /// `export --nodes N`. - #[clap(short, long, alias = "nodes", default_value = "3", global = true)] - n_nodes: usize, - - #[command(subcommand)] - command: Commands, -} - -#[derive(Parser, Debug)] -enum Commands { - /// Check the model - Check, - /// Serve the model on localhost:8080 - Serve, - /// Export the exhaustive reachable state graph in a stable, canonical, - /// line-oriented text format (see Readme.md), suitable for byte-for-byte - /// comparison against an independent re-implementation of the model. - Export { - /// Output file path; defaults to stdout - #[clap(short, long)] - out: Option, - }, -} - -fn check(model: ActorModel) { - let checker = model - .checker() - .spawn_bfs() - .join_and_report(&mut WriteReporter::new(&mut std::io::stderr())); - checker.assert_properties(); -} - -fn serve(model: ActorModel) { - let checker = model.checker(); - println!("Serving model on http://localhost:8080"); - 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(); - - let model = ModelCfg { - n_nodes: args.n_nodes, - } - .into_model(); - - let model = properties(model); - - match args.command { - Commands::Check => check(model), - Commands::Serve => serve(model), - Commands::Export { out } => export(model, out), - } -} diff --git a/tla/disaster-recovery/src/model.rs b/tla/disaster-recovery/src/model.rs deleted file mode 100644 index 735db319318..00000000000 --- a/tla/disaster-recovery/src/model.rs +++ /dev/null @@ -1,193 +0,0 @@ -extern crate stateright; -use stateright::{actor::*, util::HashableHashSet}; -use std::borrow::Cow; - -type Txid = u64; - -#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub struct GossipStruct { - pub src: Id, - pub txid: Txid, -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub struct VoteStruct { - pub src: Id, - pub recv: HashableHashSet, -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub enum Msg { - Gossip(GossipStruct), - Vote(VoteStruct), - IAmOpen(Id), -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub enum Timer { - ElectionTimeout, -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub enum NextStep { - Vote, - OpenJoin, - Open { timeout: bool }, - Join, -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub struct State { - pub next_step: NextStep, - pub gossips: HashableHashSet, - pub votes: HashableHashSet, - pub submitted_vote: Option<(Id, VoteStruct)>, - pub txid: Txid, -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq)] -pub struct Node { - pub peers: HashableHashSet, -} - -impl Node { - fn vote_for_max<'a>(gossips: &HashableHashSet, id: Id) -> (Id, VoteStruct) { - let dst = gossips - .iter() - .max_by_key(|g| (g.txid, g.src)) - .unwrap() - .src; - let vote = VoteStruct { - src: id, - recv: gossips.clone(), - }; - return (dst, vote); - } - - fn other_peers(&self, id: Id) -> Vec { - self.peers.iter().filter(|&&p| p != id).cloned().collect() - } - - fn advance_step(&self, state: &mut State, o: &mut Out, id: Id, timeout: bool) -> bool { - match state.next_step { - NextStep::Vote if state.gossips.len() == self.peers.len() || timeout => { - let (dst, vote) = Node::vote_for_max(&state.gossips, id); - state.submitted_vote = Some((dst, vote.clone())); - if dst == id { - state.votes.insert(vote); - } else { - o.send(dst, Msg::Vote(vote)); - } - state.next_step = NextStep::OpenJoin; - return true; - } - NextStep::OpenJoin if state.votes.len() >= (self.peers.len() + 1) / 2 || timeout => { - state.next_step = NextStep::Open { timeout }; - o.broadcast(&self.other_peers(id), &Msg::IAmOpen(id)); - return true; - } - _ => false, - } - } - - fn advance_several(&self, state: &mut State, o: &mut Out, id: Id, timeout: bool) { - while self.advance_step(state, o, id, timeout) {} - } -} - -impl Actor for Node { - type Msg = Msg; - type State = State; - type Timer = Timer; - type Storage = (); - type Random = (); - - fn on_start(&self, id: Id, _storage: &Option, o: &mut Out) -> Self::State { - let txid = usize::from(id) as Txid; // Use id as txid for simplicity - let gossip = GossipStruct { src: id, txid }; - let mut gossips = HashableHashSet::new(); - gossips.insert(gossip.clone()); - let mut state = State { - next_step: NextStep::Vote, - gossips, - votes: HashableHashSet::new(), - submitted_vote: None, - txid: usize::from(id) as Txid, - }; - o.broadcast(&self.other_peers(id), &Msg::Gossip(gossip)); - o.set_timer(Timer::ElectionTimeout, model_timeout()); - self.advance_several(&mut state, o, id, false); - return state; - } - - fn on_timeout(&self, id: Id, state: &mut Cow, timer: &Timer, o: &mut Out) { - match timer { - Timer::ElectionTimeout => match state.next_step { - NextStep::Vote if !state.gossips.is_empty() => { - let state = state.to_mut(); - self.advance_several(state, o, id, true); - o.set_timer(Timer::ElectionTimeout, model_timeout()); - } - NextStep::OpenJoin if !state.votes.is_empty() => { - let state = state.to_mut(); - self.advance_several(state, o, id, true); - } - _ => { - o.set_timer(Timer::ElectionTimeout, model_timeout()); - } - }, - } - } - - fn on_msg( - &self, - id: Id, - state: &mut Cow, - _src: Id, - msg: Self::Msg, - o: &mut Out, - ) { - let state = state.to_mut(); - match msg { - Msg::Gossip(gossip) => { - // Freeze gossip collection after voting is submitted - if !state.gossips.contains(&gossip) && state.submitted_vote.is_none() { - state.gossips.insert(gossip.clone()); - } - } - Msg::Vote(vote) => { - if !state.votes.contains(&vote) { - state.votes.insert(vote); - } - } - Msg::IAmOpen(_) => { - if !matches!(state.next_step, NextStep::Open { .. }) { - state.next_step = NextStep::Join; - } - } - }; - self.advance_several(state, o, id, false); - } -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq)] -pub struct ModelCfg { - pub n_nodes: usize, -} - -impl ModelCfg { - pub fn into_model(self) -> ActorModel { - let peers: HashableHashSet = (0..self.n_nodes).map(|i| Id::from(i as usize)).collect(); - ActorModel::new(self.clone(), ()) - .actors( - (0..self.n_nodes) - .map(|_| Node { - peers: peers.clone(), - }) - .collect::>(), - ) - //.init_network(Network::new_ordered([])) - .init_network(Network::new_unordered_nonduplicating([])) - .lossy_network(LossyNetwork::No) - } -}