Yichus/Spec
Builtin package (resource spec.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/Spec
from Yichus/IO import IO
from Yichus/Service import Handler
from Yichus/Data import Db
from Yichus/Access import Principal
# Declared behavioral specifications, checked natively by `yichus spec`.
#
# A Spec models one state cell (an IOSite stateRef) as a transition system
# and declares properties that every explored interleaving must satisfy.
# Properties are ordinary pure total functions: the spec, the properties,
# and the implementation share one language and one compiler.
#
# Spec-first workflow: write the Spec (and the domain functions it uses)
# before any handler exists. Every property reports `inconclusive` with
# "no write operations" — obligations registered, nothing discharged.
# As handlers are written, verdicts flip to `holds` or `violated` with
# source-located counterexample traces.
export (
Transition(),
OpTransition,
transition,
transition2,
transition3,
StateModel(),
Property(),
StepProperty(),
Spec(),
DeltaSign(),
Delta(),
Bounds(),
KeyProperty(),
EscrowSpec(),
RowBounds(),
TableEscrowSpec(),
FlowSpec(),
FlowSpec1(),
FlowSpec2(),
FlowSpec3(),
FlowSpec4(),
FlowSpec5(),
FlowSpec6(),
FlowOp(),
Conformance(),
WorldConformance()
)
exposes (Yichus/IO, Yichus/Service, Yichus/Data, Yichus/Access)
# Binds a handler binding (by name) to its model step function. The step
# is what the checker applies to the model state each time a write from
# that binding executes in an explored interleaving.
#
# This is the input-blind string form: the step cannot see the
# operation's input, so it can only model handlers whose effect is the
# same for every request. Kept for programs already written against it;
# prefer `transition("op", op, step, show_input)` below, which references the
# handler directly and threads the operation's input into the step.
struct Transition[s](operation: String, step: s -> s)
# The input-indexed model of one operation: `step` models the
# operation's effect as a function of the model state AND that
# operation's input, and `show_input` renders a sampled input in
# counterexample traces so a failure reads in domain terms.
struct OpStep[s, i](operation: String, step: (s, i) -> s, show_input: i -> String)
# Existential wrapper so one StateModel lists operations with different
# input types. Same shape as InputEntry in Yichus/Simulation. The type is
# public but its constructor is private: a user builds it only through
# `transition(...)` / `transition2(...)` / `transition3(...)` below.
# Declare the StateModel and its op_transitions as a literal list of inline
# transition calls inside the Spec binding. The checker validates that exact
# compiled expression so a helper cannot substitute a different value.
struct OpTransition[s](model: exists i. OpStep[s, i])
# The typed, input-indexed transition declarations: `op` is a direct
# reference to the handler binding (a typo, or a step typed against a
# different input than the handler takes, is a compile error), and the
# handler's input is its LAST parameter — leading parameters are the
# world the runtime injects (a State cell, a Db, a Principal), one
# constructor per handler arity, the same shape family as FlowSpec1..6.
# The operation name must be a literal equal to the referenced handler
# binding's name. The checker validates that pair in typed IR, then resolves
# evaluated transitions by name even if their list is reordered. It samples seeded
# inputs from that input type when it walks each interleaving, so the
# verdict is bounded over interleavings x sampled inputs, never a proof.
# `op` is consumed at compile time only: it pins the types and names the
# binding in the IR; the operation name survives in the evaluated OpStep.
def transition[s, i, r](
operation: String,
op: i -> IO[r],
step: (s, i) -> s,
show_input: i -> String
) -> OpTransition[s]:
_ = op
OpTransition(OpStep(operation, step, show_input))
def transition2[s, c, i, r](
operation: String,
op: (c, i) -> IO[r],
step: (s, i) -> s,
show_input: i -> String
) -> OpTransition[s]:
_ = op
OpTransition(OpStep(operation, step, show_input))
def transition3[s, c1, c2, i, r](
operation: String,
op: (c1, c2, i) -> IO[r],
step: (s, i) -> s,
show_input: i -> String
) -> OpTransition[s]:
_ = op
OpTransition(OpStep(operation, step, show_input))
# The modeled state cell.
# state_ref: the IOSite stateRef this model binds to (the name of
# the State value in handler code, e.g.
# "submission_state")
# init: the model's initial state
# describe: human-readable rendering used in counterexample traces
# transitions: one Transition per handler binding that writes the
# cell and ignores its input (the deprecated string
# form)
# op_transitions: one `transition(...)` per handler binding whose
# effect depends on its input
struct StateModel[s](
state_ref: String,
init: s,
describe: s -> String,
transitions: List[Transition[s]],
op_transitions: List[OpTransition[s]]
)
# A state invariant, checked after every modeled step (and against init).
struct Property[s](name: String, check: s -> Bool)
# A step invariant over (pre-state, operation name, post-state), checked
# at every modeled step.
struct StepProperty[s](name: String, check: (s, String, s) -> Bool)
struct Spec[s](
model: StateModel[s],
properties: List[Property[s]],
step_properties: List[StepProperty[s]]
)
# --- Escrow / admission vocabulary (checked by `yichus admit`) ---
#
# An EscrowSpec models one state cell as a keyed family of integer values
# (O'Neil-style escrow, 1986): operations declare signed deltas against
# keys computed from their input, invariants are interval bounds per key,
# and the admission solver can then admit a batch of operations with
# interval arithmetic instead of interleaving search — for exactly the
# operations that stay inside this monotone fragment.
#
# Keys are Strings and values are Ints in this pass; generalizing values
# to arbitrary ordered commutative monoids (and keys to any ordered type)
# is noted future work, not attempted here.
# How a Delta moves the keyed value. Dec consumes headroom toward the
# lower bound, Inc toward the upper. Mixed declares that the direction is
# data-dependent: a valid declaration, but not escrow-analyzable —
# operations with a Mixed delta leave the fast path and fall back to
# bounded search.
enum DeltaSign:
Dec
Inc
Mixed
# Classifies one operation's effect on one keyed value. `operation` names
# the handler binding that performs the write (same convention as
# Transition). `key` and `amount` are ordinary pure functions of the
# operation's input, evaluated per batch operation by the compiler's own
# evaluator. An operation may declare several Deltas (a transfer is a Dec
# on the source key and an Inc on the destination key). `amount` must be
# non-negative for Dec/Inc; a negative amount is treated as Mixed.
struct Delta[i](
operation: String,
key: i -> String,
amount: i -> Int,
sign: DeltaSign
)
# Interval invariants, per key. None means unbounded on that side.
# e.g. lower = _ -> Some(0) declares "balance never goes negative";
# upper can encode per-key credit limits.
struct Bounds(
lower: String -> Option[Int],
upper: String -> Option[Int]
)
# A per-key invariant that is NOT an interval constraint (any legal total
# predicate, e.g. "the value stays even"). The affected keys must be
# declared explicitly — a small-scope finite domain, the TLC CONSTANTS
# move — because the solver cannot introspect the predicate to learn
# which keys it constrains. Operations touching these keys are not
# escrow-analyzable and fall back to bounded search.
struct KeyProperty(
name: String,
keys: List[String],
check: Int -> Bool
)
# The admission model for one keyed cell.
# state_ref: the IOSite stateRef this model binds to (the name of the
# State value in handler code, e.g. "accounts")
# init: the cell's real initial value (also used to seed the model:
# the per-key model value starts at view(init, key))
# view: projects the keyed integer out of the cell value; used to
# seed intervals and to replay-verify admission decisions
# against the actual compiled handlers
# deltas: one or more Delta rows per handler binding that writes the
# cell (an unclassified write keeps admission inconclusive)
# bounds: interval invariants per key
# properties: non-interval per-key invariants (fallback path)
struct EscrowSpec[c, i](
state_ref: String,
init: c,
view: (c, String) -> Int,
deltas: List[Delta[i]],
bounds: Bounds,
properties: List[KeyProperty]
)
# Escrow over a table (agent-era plan item 27, the forum's H9). The keyed
# family is a `Yichus/Data` table: one integer per row key, projected out
# of the row by `view`; a missing row holds `missing`. A key's bounds are
# read off the row of a second table at the same key (the forum's reply
# cap lives on the thread row), so they are functions of the key and of
# that row when it exists; a spec with no bound table names "" and the
# row is always None. The world a batch is admitted against is seeded the
# way `yichus why --rows` seeds one (`yichus admit --rows`, or the `rows`
# argument of `api_escrow_check`); an unseeded table is empty. A batch
# operation may carry a `principal` ({"user_id", "roles"}) for a handler
# that takes one; replay runs the handler on a fresh copy of the seeded
# world and reads the row back through `view`.
# table: the table whose rows hold the keyed integers
# missing: the integer a missing row holds
# view: projects the integer out of a row
# bound_table: the table whose row at the same key carries the bounds
# bounds: the interval for a key, given that row (None when absent)
# deltas: Delta rows per handler binding that writes `table`
# properties: non-interval per-key invariants (fallback path)
struct RowBounds[t](
lower: (String, Option[t]) -> Option[Int],
upper: (String, Option[t]) -> Option[Int]
)
struct TableEscrowSpec[r, t, i](
table: String,
missing: Int,
view: r -> Int,
bound_table: String,
bounds: RowBounds[t],
deltas: List[Delta[i]],
properties: List[KeyProperty]
)
# A FlowSpec declares that a family of mutation bindings all follow one
# main flow, written once as an ordinary factory function that nobody
# needs to call. The factory's function-typed parameters are the flow's
# holes; each declared mutation must be a structural instance of the
# factory body with every hole filled by a named top-level helper. The
# checker verifies conformance from the compiled IR and extracts the
# per-mutation parts; `yichus flow batch` composes those parts into an
# all-or-nothing batch whose batch-of-one behavior is replay-checked
# against the single mutation.
# name: the flow's display name
# flow: the factory binding, as "Package/Name/binding" (referenced
# by name because each flow's factory has its own arity)
# failed: result discrimination for all-or-nothing batching — a pure
# total predicate on the flow's result type (named, so the
# checker can recover its binding from the declaration)
# mutations: the bindings declared to follow the flow — a typed list,
# so the family's shared input and result types are checked
# by the compiler, not by convention
struct FlowSpec[i, r](
name: String,
flow: String,
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
# The typed flow declarations: one struct per factory arity, so the
# factory is a real typed field instead of a "Package/Name/binding"
# string. A typo'd factory, a wrong arity, or a hole-type mismatch is
# then a compile error, and the checker recovers the factory binding
# from the declaration's own IR the same way it recovers `failed` and
# the mutations. Prefer these; the string form above remains for
# programs already written against it.
# h1..hN: the hole types (each is itself a function type — the
# factory's function-typed parameters)
# factory: the flow factory itself, referenced directly
struct FlowSpec1[h1, i, r](
name: String,
factory: h1 -> i -> IO[r],
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
struct FlowSpec2[h1, h2, i, r](
name: String,
factory: (h1, h2) -> i -> IO[r],
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
struct FlowSpec3[h1, h2, h3, i, r](
name: String,
factory: (h1, h2, h3) -> i -> IO[r],
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
struct FlowSpec4[h1, h2, h3, h4, i, r](
name: String,
factory: (h1, h2, h3, h4) -> i -> IO[r],
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
struct FlowSpec5[h1, h2, h3, h4, h5, i, r](
name: String,
factory: (h1, h2, h3, h4, h5) -> i -> IO[r],
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
struct FlowSpec6[h1, h2, h3, h4, h5, h6, i, r](
name: String,
factory: (h1, h2, h3, h4, h5, h6) -> i -> IO[r],
failed: r -> Bool,
mutations: List[i -> IO[r]]
)
# One operation of a typed batch: the mutation (a direct reference to a
# binding declared in the flow's mutation list) and its input, checked
# by the compiler. A batch is then an ordinary Bosatsu binding —
# `my_batch: List[FlowOp[Order, Outcome]] = [FlowOp(restock, Order(50, 1)), ...]`
# — a program, not a JSON file: input shape errors are compile errors,
# and `yichus flow batch --ops Pkg/Name/my_batch` replays it
# all-or-nothing from the declared initial state.
struct FlowOp[i, r](
mutation: i -> IO[r],
input: i
)
# --- Conformance: the declared model checked against the compiled handler ---
#
# A Conformance binds one route handler to a declared model of its effect
# on one table, and asks the checker whether they agree. The handler is
# referenced through the same existentially-erased `Handler` vocabulary
# the routing table uses — `handler("admit", admit)` — and the checker
# recovers the typed binding from the declaration's own compiled IR, so
# the world is built from the handler's real signature: a fresh Db seeded
# from `seed`, a Principal injected, and the remaining parameter generated
# by the seeded type-driven generator.
#
# Each generated trajectory runs the compiled handler and the declared
# `step` over the same inputs and compares the table — projected through
# `project` — against the model after every operation. Agreement is
# `holds (bounded: N inputs, seed S)`, never proof; a divergence renders
# both sides through `describe` and the offending input through
# `show_input`, so the counterexample reads in domain terms. Before any
# operation runs, `project(seed)` must equal `init` — a model that starts
# somewhere the world does not is a divergence at rest, reported first.
# name: display name for the verdict
# resource: the table the model tracks (the `table(db, ...)` name)
# seed: opening rows written before any operation, in order,
# keyed as db_create would key them (ids "1".."N") so
# handlers can read, write, or delete them by id
# init: the model state matching the freshly seeded world
# describe: human rendering of a model state
# show_input: human rendering of one generated input
# project: the table's rows (in insertion order) read as model state
# same: model-state equality for the comparison
# op: the handler under conformance
# step: the declared model of one operation's effect
struct Conformance[s, row, i](
name: String,
resource: String,
seed: List[row],
init: s,
describe: s -> String,
show_input: i -> String,
project: List[row] -> s,
same: (s, s) -> Bool,
op: Handler,
step: (s, i) -> s
)
# --- WorldConformance: the model over every table, indexed by the caller ---
#
# A Conformance seeds one table and its step cannot see who calls, so a
# handler that reads other tables before it writes (a reply that reads
# the thread and the moderator roster before it writes the post) never
# reaches its write in the checker's world, and a rule that depends on
# the caller has no model form. A WorldConformance lifts both limits:
# `world` seeds every table at once, and `step` takes the Principal the
# handler ran as.
#
# The checker runs each trajectory in a fresh world built from `world`,
# picking every operation's caller from `callers` by the trajectory's
# seed (so trajectories mix callers), and compares `project(db)` —
# the model's own reads of the world, through db_read / db_query —
# against `step(model, caller, input)` after every operation. Agreement
# is `holds (bounded: N inputs, seed S)`, never proof; a divergence
# renders both sides through `describe`, the offending input through
# `show_input`, and names the caller. Before any operation, `project`
# of the freshly seeded world must equal `init`.
# name: display name for the verdict
# world: a JSON object seeding every table, exactly as
# `yichus why --rows` takes it: {table: [row, ...]}
# numbers rows "1".."n" (as db_create would);
# {table: {id: row}} sets ids; a row is the JSON
# encoding of the table's value type
# callers: user ids; each operation runs as Principal(caller, [])
# with the caller drawn from this list (never empty)
# init: the model state matching the freshly seeded world
# describe: human rendering of a model state
# show_input: human rendering of one generated input
# project: the model's view of the world, read through Yichus/Data
# in the same in-memory world the handler runs in
# same: model-state equality for the comparison
# op: the handler under conformance (`handler("name", binding)`)
# step: the declared model of one operation's effect, given the
# caller it ran as
struct WorldConformance[s, i](
name: String,
world: String,
callers: List[String],
init: s,
describe: s -> String,
show_input: i -> String,
project: Db -> IO[s],
same: (s, s) -> Bool,
op: Handler,
step: (s, Principal, i) -> s
)