bft_locking.qnt

// BFT with Locking specification in Quint
//
// Extends BFT with multiple rounds and locking.
// Demonstrates why locking is needed to maintain safety across rounds.
//
// To run:
//   quint run bft_locking.qnt
//   quint test bft_locking.qnt

module bft_locking {
  // ==========================================================================
  // TYPES
  // ==========================================================================

  type Node = str
  type Value = str
  type Round = int

  type Status =
    | Correct
    | Faulty

  // A lock records what value a node is locked on and since which round
  type Lock = { value: Value, round: Round }

  // ==========================================================================
  // CONSTANTS
  // ==========================================================================

  pure val N1: Node = "n1"
  pure val N2: Node = "n2"
  pure val N3: Node = "n3"
  pure val N4: Node = "n4"

  pure val ALL_NODES: Set[Node] = Set(N1, N2, N3, N4)
  pure val N: int = 4
  pure val F: int = 1
  pure val QUORUM: int = 2 * F + 1  // = 3

  pure val A: Value = "A"
  pure val B: Value = "B"
  pure val NO_VALUE: Value = ""
  pure val ALL_VALUES: Set[Value] = Set(A, B)

  pure val NO_LOCK: Lock = { value: NO_VALUE, round: -1 }

  // ==========================================================================
  // STATE
  // ==========================================================================

  // Which nodes are faulty (fixed for a run)
  var status: Node -> Status

  // Current round
  var round: Round

  // Leader for each round (deterministic rotation for simplicity)
  // In practice this would be round % n or similar
  var leader: Round -> Node

  // What each node is locked on (NO_LOCK if not locked)
  var locked: Node -> Lock

  // Votes cast this round: node -> value voted for (NO_VALUE if not voted)
  var votes: Node -> Value

  // Values that have been committed (across all rounds)
  var committed: Set[Value]

  // ==========================================================================
  // HELPERS
  // ==========================================================================

  pure def voteCount(allVotes: Node -> Value, value: Value): int =
    ALL_NODES.filter(n => allVotes.get(n) == value).size()

  pure def hasQuorum(allVotes: Node -> Value, value: Value): bool =
    voteCount(allVotes, value) >= QUORUM

  pure def currentLeader(r: Round, leaders: Round -> Node): Node =
    if (leaders.keys().contains(r)) leaders.get(r) else N1

  pure def isLocked(node: Node, locks: Node -> Lock): bool =
    locks.get(node) != NO_LOCK

  pure def hasVoted(node: Node, allVotes: Node -> Value): bool =
    allVotes.get(node) != NO_VALUE

  // ==========================================================================
  // INITIALIZATION
  // ==========================================================================

  action init = all {
    nondet faultyNodes = ALL_NODES.powerset().filter(s => s.size() == F).oneOf()
    status' = ALL_NODES.mapBy(n =>
      if (faultyNodes.contains(n)) Faulty else Correct
    ),
    round' = 0,
    // Simple leader rotation: round 0 -> N1, round 1 -> N2, etc.
    leader' = Map(0 -> N1, 1 -> N2, 2 -> N3, 3 -> N4),
    locked' = ALL_NODES.mapBy(_ => NO_LOCK),
    votes' = ALL_NODES.mapBy(_ => NO_VALUE),
    committed' = Set(),
  }

  // ==========================================================================
  // ACTIONS
  // ==========================================================================

  /// Correct node votes for a value
  /// - If locked, must vote for locked value
  /// - If not locked, can vote for leader's proposal
  /// - When a quorum forms, ALL correct nodes who voted for that value lock on it
  action correctVote(node: Node, value: Value): bool = all {
    status.get(node) == Correct,
    not(hasVoted(node, votes)),
    // If locked, must vote for locked value
    if (isLocked(node, locked))
      locked.get(node).value == value
    else
      true,
    votes' = votes.set(node, value),
    // Check if this vote causes a commit
    val newVotes = votes.set(node, value)
    if (hasQuorum(newVotes, value)) all {
      committed' = committed.union(Set(value)),
      // All correct nodes who voted for this value lock on it
      locked' = ALL_NODES.mapBy(n =>
        val currentLock = locked.get(n)
        if (status.get(n) == Correct and newVotes.get(n) == value and currentLock.round < round)
          { value: value, round: round }
        else
          currentLock
      ),
    } else all {
      committed' = committed,
      locked' = locked,
    },
    status' = status,
    round' = round,
    leader' = leader,
  }

  /// Faulty node votes for any value (ignores locks)
  /// When quorum forms, correct nodes who voted for that value still lock
  action faultyVote(node: Node, value: Value): bool = all {
    status.get(node) == Faulty,
    votes' = votes.set(node, value),
    val newVotes = votes.set(node, value)
    if (hasQuorum(newVotes, value)) all {
      committed' = committed.union(Set(value)),
      // All correct nodes who voted for this value lock on it
      locked' = ALL_NODES.mapBy(n =>
        val currentLock = locked.get(n)
        if (status.get(n) == Correct and newVotes.get(n) == value and currentLock.round < round)
          { value: value, round: round }
        else
          currentLock
      ),
    } else all {
      committed' = committed,
      locked' = locked,
    },
    status' = status,
    round' = round,
    leader' = leader,
  }

  /// Node observes quorum for a value and locks on it
  action observeQuorum(node: Node, value: Value): bool = all {
    status.get(node) == Correct,
    hasQuorum(votes, value),
    // Lock on this value at current round (or keep higher lock)
    val currentLock = locked.get(node)
    if (currentLock.round < round)
      locked' = locked.set(node, { value: value, round: round })
    else
      locked' = locked,
    status' = status,
    round' = round,
    leader' = leader,
    votes' = votes,
    committed' = committed,
  }

  /// Advance to next round (e.g., leader timeout)
  /// Resets votes but preserves locks
  action nextRound: bool = all {
    round' = round + 1,
    votes' = ALL_NODES.mapBy(_ => NO_VALUE),  // clear votes for new round
    status' = status,
    leader' = leader,
    locked' = locked,  // locks persist!
    committed' = committed,
  }

  // ==========================================================================
  // STATE MACHINE
  // ==========================================================================

  action step = any {
    nondet node = ALL_NODES.oneOf()
    nondet value = ALL_VALUES.oneOf()
    correctVote(node, value),

    nondet node = ALL_NODES.oneOf()
    nondet value = ALL_VALUES.oneOf()
    faultyVote(node, value),

    nondet node = ALL_NODES.oneOf()
    nondet value = ALL_VALUES.oneOf()
    observeQuorum(node, value),

    nextRound,
  }

  // ==========================================================================
  // SAFETY PROPERTIES
  // ==========================================================================

  /// Agreement: at most one value commits (across all rounds)
  val agreement: bool =
    committed.size() <= 1

  /// Combined safety
  val safety: bool = agreement

  // ==========================================================================
  // TESTS
  // ==========================================================================

  /// Test: value commits in round 0, lock prevents conflicting commit in round 1
  run lockPreventsConflictTest = {
    all {
      status' = Map(N1 -> Faulty, N2 -> Correct, N3 -> Correct, N4 -> Correct),
      round' = 0,
      leader' = Map(0 -> N1, 1 -> N2, 2 -> N3, 3 -> N4),
      locked' = ALL_NODES.mapBy(_ => NO_LOCK),
      votes' = ALL_NODES.mapBy(_ => NO_VALUE),
      committed' = Set(),
    }
    // Round 0: A gets quorum, nodes automatically lock
    .then(correctVote(N2, A))
    .then(correctVote(N3, A))
    .then(correctVote(N4, A))
    .then(all {
      assert(committed.contains(A)),
      // Nodes who voted for A are now locked
      assert(locked.get(N2).value == A),
      assert(locked.get(N3).value == A),
      assert(locked.get(N4).value == A),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
    // Move to round 1
    .then(nextRound)
    .then(all {
      assert(round == 1),
      // Locks persist across rounds
      assert(locked.get(N2).value == A),
      assert(locked.get(N3).value == A),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
    // Round 1: faulty node tries to get B committed
    // But locked nodes can only vote A
    .then(faultyVote(N1, B))
    .then(correctVote(N2, A))  // locked, must vote A
    .then(correctVote(N3, A))  // locked, must vote A
    .then(all {
      // B has only 1 vote (N1)
      // A has 2 votes (N2, N3) - not quorum yet but B can't reach quorum
      assert(not(committed.contains(B))),
      assert(agreement),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
  }

  /// Test: locking prevents agreement violation
  /// Even with faulty node and unlocked node voting B, locked nodes prevent quorum
  run whyLockingMattersTest = {
    all {
      status' = Map(N1 -> Faulty, N2 -> Correct, N3 -> Correct, N4 -> Correct),
      round' = 0,
      leader' = Map(0 -> N1, 1 -> N2, 2 -> N3, 3 -> N4),
      locked' = ALL_NODES.mapBy(_ => NO_LOCK),
      votes' = ALL_NODES.mapBy(_ => NO_VALUE),
      committed' = Set(),
    }
    // Round 0: A gets quorum and commits, N2/N3 automatically lock
    .then(correctVote(N2, A))
    .then(correctVote(N3, A))
    .then(faultyVote(N1, A))
    .then(all {
      assert(committed.contains(A)),
      // N2, N3 are now locked on A
      assert(locked.get(N2).value == A),
      assert(locked.get(N3).value == A),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
    .then(nextRound)
    // Round 1: Even if faulty node votes B and N4 votes B,
    // locked nodes N2, N3 vote A, so B can't reach quorum
    .then(faultyVote(N1, B))
    .then(correctVote(N4, B))  // N4 wasn't locked
    .then(correctVote(N2, A))  // locked on A
    .then(all {
      // B has: N1, N4 (2 votes)
      // Can't reach quorum because N2, N3 are locked on A
      assert(not(committed.contains(B))),
      assert(agreement),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
  }

  /// Test: node that missed round 0 can still vote in round 1
  run latecomerTest = {
    all {
      status' = Map(N1 -> Faulty, N2 -> Correct, N3 -> Correct, N4 -> Correct),
      round' = 0,
      leader' = Map(0 -> N1, 1 -> N2, 2 -> N3, 3 -> N4),
      locked' = ALL_NODES.mapBy(_ => NO_LOCK),
      votes' = ALL_NODES.mapBy(_ => NO_VALUE),
      committed' = Set(),
    }
    // Round 0: only N2, N3 vote A (N4 is slow/offline)
    // N1 (faulty) completes the quorum
    .then(correctVote(N2, A))
    .then(correctVote(N3, A))
    .then(faultyVote(N1, A))
    .then(all {
      assert(committed.contains(A)),  // A commits with N1, N2, N3
      // N2, N3 automatically locked when quorum formed
      assert(locked.get(N2).value == A),
      assert(locked.get(N3).value == A),
      // N4 didn't vote, so not locked
      assert(locked.get(N4) == NO_LOCK),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
    .then(nextRound)
    // Round 1: N4 joins, but since it's not locked it could vote B
    // However, with N2, N3 locked on A, B can't get quorum
    .then(correctVote(N4, B))  // N4 not locked, votes B
    .then(faultyVote(N1, B))   // faulty helps B
    .then(correctVote(N2, A))  // locked
    .then(all {
      // B has: N1, N4 (2 votes) - not quorum
      assert(not(committed.contains(B))),
      assert(agreement),
      status' = status, round' = round, leader' = leader,
      locked' = locked, votes' = votes, committed' = committed,
    })
  }
}