Yichus/Dist
Builtin package (resource dist.bosatsu).
This is the complete package source used by this build. The export
list names its public API; definitions below give the types and behavior.
New to the API? Start with Make a calculator or Build an API, then use this page to look up a definition.
package Yichus/Dist
# Distributed-system specifications, checked by `yichus dist`.
#
# A DistSpec declares a small closed world of named nodes exchanging
# typed messages. Node handlers are ordinary pure total functions:
# `(state, from, msg) -> Step(next_state, sends)`. Because handlers are
# pure and total, ALL nondeterminism belongs to the engine — which
# message is delivered next, which messages are dropped or duplicated,
# which nodes crash. The engine (DistEngine, on the JVM) explores
# delivery schedules exhaustively within a bound and by seeded random
# walks beyond it, evaluating the declared invariants with the
# compiler's own evaluator after every event.
#
# This is deterministic simulation testing with a model: the spec, the
# invariants, and the implementation share one language and one
# compiler, and every counterexample is a replayable schedule.
#
# Spec-first workflow: write the message enum, the state struct, the
# world wiring, and the invariants before the handlers exist (handlers
# can start as `(s, _, _) -> Step(s, [])` stubs). Every invariant then
# reports `holds` vacuously or `violated` immediately — obligations
# registered. As handlers are written, verdicts move.
export (
Send(),
Step(),
Node(),
World(),
NodeView(),
Invariant(),
FinalInvariant(),
FaultBudget(),
DistSpec(),
ExtraInvariants(),
Sometimes(),
CoverageSpec(),
AdversaryNode(),
AdvWorld(),
AdvDistSpec(),
Supervision(),
SupervisionSpec(),
)
# One message in flight: the destination node's name and the payload.
# Delivery order between distinct sends is never guaranteed; the engine
# explores reorderings freely.
struct Send[m](to: String, msg: m)
# The result of one handler activation: the node's next state and the
# messages it emits (in submission order; the network may still reorder).
struct Step[s, m](state: s, sends: List[Send[m]])
# One node in the world.
# name: unique node name (message routing key)
# init: the node's initial state
# on_start: activation run once at world start, before any delivery
# (emit initial messages here; identity for passive nodes)
# on_message: the handler: (current state, sender name, message)
struct Node[s, m](
name: String,
init: s,
on_start: s -> Step[s, m],
on_message: (s, String, m) -> Step[s, m]
)
# The closed world: every node that exists. A Send whose `to` names no
# node is a spec error (loud, not silently dropped).
struct World[s, m](nodes: List[Node[s, m]])
# One node's state as seen by an invariant check.
struct NodeView[s](name: String, state: s)
# A global safety invariant, checked after every engine event (delivery,
# drop, duplicate, crash) against the states of all nodes.
struct Invariant[s](name: String, check: List[NodeView[s]] -> Bool)
# An invariant checked only in quiescent states: no messages left in
# flight on this schedule. Use for convergence claims ("all replicas
# agree once traffic settles") that transient states legitimately break.
struct FinalInvariant[s](name: String, check: List[NodeView[s]] -> Bool)
# The fault model, as budgets the adversarial scheduler may spend.
# drops: how many in-flight messages may vanish
# duplicates: how many deliveries may be replayed a second time
# crashes: how many nodes may halt (a crashed node's state is
# frozen; messages to it are consumed without effect;
# it stays down unless a Supervision names it)
# All zero = reliable network, reorder-only.
struct FaultBudget(drops: Int, duplicates: Int, crashes: Int)
# The complete declaration `yichus dist` discovers (by checked type, not
# by filename) and checks.
struct DistSpec[s, m](
world: World[s, m],
faults: FaultBudget,
invariants: List[Invariant[s]],
final_invariants: List[FinalInvariant[s]],
describe_state: s -> String,
describe_msg: m -> String
)
# Solver-authored auxiliary invariants: scaffolding lemmas checked
# ALONGSIDE a task's given DistSpec, never replacing it. Declare these
# in your own file (importing the world's state type), pass that file
# to `yichus dist` with the given files, and every discovered
# ExtraInvariants binding is merged into the run — a sanctioned home
# for debugging lemmas when the given checker file must not be edited.
# Names must not collide with the spec's own invariants.
struct ExtraInvariants[s](
invariants: List[Invariant[s]],
final_invariants: List[FinalInvariant[s]]
)
# A reachability ("sometimes") assertion: at least one explored state
# must satisfy the predicate. This is the structural defense against
# vacuously-passing property sets — a spec whose invariants all hold
# while nothing ever HAPPENS (no job dispensed, no write committed)
# fails its coverage instead of certifying. Verdicts: `covered` (a
# witness state was reached — conclusive even under truncation),
# `violated` (complete exploration, never reached), `inconclusive`
# (truncated, never reached).
struct Sometimes[s](name: String, check: List[NodeView[s]] -> Bool)
# Discovered by checked type, like ExtraInvariants; merged into the run.
struct CoverageSpec[s](sometimes: List[Sometimes[s]])
# A node whose behavior is chosen by the ADVERSARY, not fixed. Its
# `on_message` returns a FINITE, NON-EMPTY list of alternative Steps, and
# the engine branches over that list exactly as it branches over which
# in-flight message to deliver next. So `holds` under exhaustive
# exploration means "no attacker strategy violates the property" — the
# Dolev-Yao "for all messages the attacker can derive" claim, not "for the
# one strategy we hand-coded".
#
# SOUNDNESS DISCIPLINE. The returned list is the attacker's move menu at
# this activation: forward the message (`[Step(s, [Send(next, m)])]`), drop
# it by not forwarding (`[Step(s2, [])]`, still updating knowledge), replay
# a term it has already observed, or inject a term RECOMBINED from its
# knowledge. It may never fabricate an opaque term (e.g. a signature) it has
# not seen — model such terms as constructors the attacker can carry but not
# mint. The list is finite by construction (a Bosatsu List over the finite
# knowledge state), which keeps exhaustive exploration finite and `holds`
# meaningful. It must be NON-EMPTY: an empty list is a loud spec error, not
# "do nothing" — write "do nothing" explicitly as `[Step(s, [])]`, so a
# delivery is never silently pruned.
#
# `on_start` returns a single Step (not a list): at world start the attacker
# has observed nothing, so its opening move is deterministic (usually
# passive `Step(s, [])`, or a single self-initiated message).
struct AdversaryNode[s, m](
name: String,
init: s,
on_start: s -> Step[s, m],
on_message: (s, String, m) -> List[Step[s, m]]
)
# A world with honest nodes AND adversary nodes. Unlike `World` (one field,
# so newtype-unwrapped), this is a genuine two-field product the checker
# reads directly. Honest and adversary names share one routing namespace and
# must all be distinct.
struct AdvWorld[s, m](
nodes: List[Node[s, m]],
adversaries: List[AdversaryNode[s, m]]
)
# The adversarial analogue of `DistSpec`: identical shape, but field 0 is an
# `AdvWorld`. Discovered by checked type exactly like `DistSpec`; existing
# `DistSpec` tasks are untouched.
struct AdvDistSpec[s, m](
world: AdvWorld[s, m],
faults: FaultBudget,
invariants: List[Invariant[s]],
final_invariants: List[FinalInvariant[s]],
describe_state: s -> String,
describe_msg: m -> String
)
# Recovery (register DD2; the forum's H8): a supervisor NODE restarts a
# crashed node by a message. `Supervision(supervisor, node, restart)`
# lets the engine deliver `restart` from `supervisor` to `node` while
# `node` is crashed — a `restart` event. The node is alive again and its
# own `on_message` runs on the state it crashed with: what survives is
# that handler's decision (a durable field kept, a volatile one reset or
# recomputed, an interrupted operation redone), the durable/volatile
# distinction made explicit in the model rather than assumed by the
# engine. The scheduler may restart the node at any point while it is
# down, and always does before the schedule is quiescent, so final
# invariants read a world whose supervised nodes are back. Messages from
# any other node to a crashed node are still consumed without effect,
# and a world with no Supervision keeps a crashed node down. Both names
# must be nodes of the world; an adversary node cannot be supervised.
struct Supervision[m](supervisor: String, node: String, restart: m)
# Discovered by checked type, like CoverageSpec, and merged into the
# run: a link applies to every spec whose world has its supervisor node
# (the supervisor's presence opts a world in; a world without it is
# untouched, so one file can hold the world with recovery and the world
# without). A world with the supervisor but not the supervised node is
# a loud spec error, never a silent skip.
struct SupervisionSpec[m](links: List[Supervision[m]])