Quint Lang

module MyProtocol {
  // type aliases, constants, state, actions, properties
}

import Voting.*              // all definitions
import Voting(quorum)        // specific definition
import Voting as V           // namespace alias

type NodeId = int
type Phase = Idle | Propose | Vote | Commit   // enum — prefer over string literals

// Module parameter — fixed at instantiation, not a state variable
const N: int
const Nodes: Set[str]

// Pure function — no state access, usable anywhere
pure def max(a: int, b: int): int = if (a > b) a else b

// Stateful operator — can read vars, takes arguments (unlike val)
def isActive(n: str): bool = active.contains(n)

// State-reading value — can read vars, no arguments
val quorum: bool = votes.size() * 2 > nodes.size()

// Compile-time constant
pure val N: int = 4
val threshold: int = N / 2 + 1

type LocalState = {
  leader: int,
  phase: Phase,        // enum (see Type aliases) — prefer over a bare str
  votes: Set[int],
  log: List[str],
}

var localState: LocalState  // cohesive local protocol state
var peers: int -> str       // independent concern (peer metadata)

action init: bool = all {
  leader' = 0,
  phase' = Idle,
  votes' = Set(),
  log' = List(),
  state' = Map(),
}

action propose(node: int): bool = all {
  phase == Idle,
  node > 0,
  leader' = node,
  phase' = Propose,
  votes' = votes,
  log' = log,
  state' = state,
}

action step: bool = any {
  propose(1),
  propose(2),
  vote,
  timeout,
}

// Non-deterministic choice from a set
action deliverMessage: bool = {
  nondet msg = pending.oneOf()
  all {
    pending.size() > 0,
    delivered' = delivered.union(Set(msg)),
    pending' = pending.exclude(Set(msg)),
    // ... other vars unchanged
  }
}

Set(1, 2, 3).contains(2)          // true
Set(1, 2).union(Set(2, 3))        // Set(1, 2, 3)
Set(1, 2, 3).intersect(Set(2, 3)) // Set(2, 3)
Set(1, 2, 3).exclude(Set(2))      // Set(1, 3)
Set(1, 2, 3).filter(x => x > 1)  // Set(2, 3)
Set(1, 2, 3).map(x => x * 2)     // Set(2, 4, 6)
Set(1, 2, 3).fold(0, (acc, x) => acc + x)  // 6
Set(1, 2, 3).size()               // 3
Set(1, 2, 3).forall(x => x > 0)  // true
Set(1, 2, 3).exists(x => x > 2)  // true
1.to(5)                           // Set(1, 2, 3, 4, 5)
nondet x = Set(1, 2, 3).oneOf()   // non-deterministic pick — only valid in nondet bindings

List(1, 2, 3).head()              // 1
List(1, 2, 3).tail()              // List(2, 3)
List(1, 2, 3).length()            // 3
List(1, 2, 3).nth(1)              // 2  (0-indexed)
List(1, 2, 3).append(4)           // List(1, 2, 3, 4)
List(1, 2).concat(List(3, 4))     // List(1, 2, 3, 4)
List(1, 2, 3).foldl(0, (acc, x) => acc + x)  // 6
List(1, 2, 3).select(x => x > 1) // List(2, 3)

Map("a" -> 1, "b" -> 2).get("a")        // 1
Map("a" -> 1).put("b", 2)               // Map("a" -> 1, "b" -> 2)
Map("a" -> 1, "b" -> 2).keys()          // Set("a", "b")
Set(1, 2, 3).mapBy(k => k * 2)          // Map(1 -> 2, 2 -> 4, 3 -> 6)  — set of keys → map

type NodeState = {
  phase:  Phase,   // enum: Idle | Propose | Vote | Commit
  voted:  bool,
  log:    List[int],
}

type Message = {
  from:    int,
  to:      int,
  round:   int,
  payload: str,
}

val n: NodeState = { phase: Idle, voted: false, log: List() }
n.phase                          // Idle
n.voted                          // false

{ ...n, phase: Propose }                            // ✅ preferred — idiomatic, handles multiple fields
{ ...n, voted: true, phase: Vote }                  // ✅ multiple fields at once

n.with("phase", Propose)                            // ⚠️ valid but non-idiomatic — field name is a string literal

type LocalState = {
  id: int,
  phase: Phase,
  est1: int,
  est2: Option[int],   // Option is from basicSpells, not built in — see Basic spells below
  round: int,
  crashed: bool,
  leader: int,
  received_messages: Set[Message],
}

var localState: LocalState

var id: int
var phase: Phase
var est1: int
var est2: Option[int]
var round: int
var crashed: bool
var leader: int
var received_messages: Set[Message]

type LocalState = { phase: Phase, votedFor: int, log: List[int] }

var nodes: int -> LocalState

action commit(id: int): bool = {
  val node = nodes.get(id)
  all {
    node.phase == Vote,
    nodes' = nodes.put(id, {...node, phase: Commit}),
  }
}

type ClusterState = {
  nodes:   int -> NodeState,
  leader:  int,
  epoch:   int,
}

var cluster: ClusterState

// Read nested field:
cluster.nodes.get(1).phase

// Update nested field (must rebuild from the inside out):
val updated = {...cluster.nodes.get(1), phase: Commit}
cluster' = {...cluster, nodes: cluster.nodes.put(1, updated)}

var inFlight: Set[Message]

action send(src: int, dst: int, r: int, p: str): bool = all {
  inFlight' = inFlight.union(Set({ from: src, to: dst, round: r, payload: p })),
  // ...
}

// Filter by field:
inFlight.filter(m => m.to == nodeId)
inFlight.exists(m => m.round == currentRound and m.payload == "vote")

type Action =
  | Propose({ value: int, proposer: int })
  | Vote({ value: int, voter: int })
  | Decide({ value: int })

val a: Action = Propose({ value: 1, proposer: 2 })

pure def describeAction(a: Action): str =
  match a {
    | Propose(p) => "proposal"
    | Vote(v)    => "vote"
    | Decide(d)  => "decision"
  }

match a {
  | Propose(_) => "proposal"
  | _          => "other"
}

type Phase = Idle | Propose | Vote | Commit
var phase: Phase

if (phase == Propose) { ... }

not(p)             // negation — Quint has no ! operator
p and q            // conjunction
p or q             // disjunction
p implies q        // p => q  (not(p) or q)
p iff q            // p == q for booleans

and { p1, p2, p3 } // block form — equivalent to p1 and p2 and p3
or  { p1, p2, p3 } // block form — at least one must hold

// Safety invariant — must hold in every reachable state
// @invariant
val noDuplicateLeader: bool =
  leaders.size() <= 1

// Temporal property — evaluated over traces
// @temporal
temporal eventualProgress: bool =
  eventually(committed.size() > 0)

// Temporal operators
eventually(p)      // p holds in some future state
always(p)          // p holds in all future states
p.implies(q)       // p => q

assume nodeCountPositive = N > 0
assume quorumMajority = 2 * quorum > N

run quorumAssumptionTest = all {
  2 * quorum > N,
  N > 0,
}

if (x > 0) "positive" else "non-positive"

val result = {
  val doubled = x * 2
  doubled + 1
}

>>> :type myExpression