whitepaper v2: Section 2 - SpeckDL language specification

Full technical writeup covering: - Design philosophy (spec as source of truth, state machines, type-safe, emit) - Structure of a speck (types, state, init, invariant, action, next) - Type system (Bool, Nat, Int, String, Set, Map, List, Records, Optional) - Actions (require, assignments, let bindings, if, emit, return, forall) - Invariants (documentation + runtime verification, quantified, logical ops) - Action composition (next: non-deterministic interleaving) - Complete Two-Phase Commit example (48-line spec) - What SpeckDL deliberately omits (no functions, no loops, no concurrency, no I/O, no error handling) - ~2,000 words
2026-05-06 18:07:53 -07:00 · 2026-05-06 18:07:53 -07:00 · 66ecdd69b9
commit 66ecdd69b9
parent 2ed6c13026
1 changed files with 351 additions and 1 deletions
--- a/docs/whitepaper-v2.md
+++ b/docs/whitepaper-v2.md
@ -73,7 +73,357 @@ The specification is 14 lines. The generated artifacts are hundreds of lines of

 ## 2. The SpeckDL Language

-*[Section 2: Full language specification — types, state machines, actions, invariants, compilation targets]*
+SpeckDL is a domain-specific language for defining state machines with types, invariants, and actions. It sits between formal specification languages (TLA+) and general-purpose programming languages — more structured than prose, more constrained than code, and designed from the ground up to be compilable.
+
+### 2.1 Design Philosophy
+
+SpeckDL follows four principles:
+
+1. **Spec as source of truth.** The `.speck` file is the authoritative description of system behavior. Generated code is derived, not co-equal. If the spec and the code disagree, the spec wins — and the compiler tells you they disagree.
+
+2. **State machines, not procedures.** Every SpeckDL specification models a state machine: typed state variables, guarded transitions (actions), and invariants that must hold across every transition. This is the same mental model as TLA+, but with a concrete compilation target.
+
+3. **Type-safe by construction.** SpeckDL has a static type system with primitive types (Bool, Nat, Int, String), compound types (Set, Map, List, Records), and user-defined type aliases. Every expression is type-checked before code generation.
+
+4. **Emit for observability.** Actions can emit typed events that become part of the provenance graph and generated event logs. Events make state machine execution observable without requiring external instrumentation.
+
+### 2.2 Structure of a Speck
+
+A SpeckDL file contains one or more `speck` blocks. A speck defines a named state machine:
+
+```
+speck Name {
+    type ...          // optional type aliases
+    state { ... }     // state variables
+    init { ... }      // initial state
+    invariant ...     // safety properties
+    action ...        // state transitions
+    next: ...         // action composition
+}
+```
+
+#### Types
+
+Type aliases are declared at the top of a speck using the `type` keyword. They name compound types for reuse across state declarations and action signatures:
+
+```
+type AccountId = Nat
+type Transfer = {
+    from: AccountId,
+    to: AccountId,
+    amount: Nat
+}
+```
+
+Type aliases are inlined during compilation — they exist for readability, not runtime overhead.
+
+#### State
+
+The `state` block declares the typed variables that comprise the machine's state. Every state variable must have an explicit type:
+
+```
+state {
+    counter: Nat
+    users: Set(String)
+    balances: Map(Nat, Int)
+    history: List(Event)
+    leader: { id: String, term: Nat }
+}
+```
+
+State variables are the only mutable storage in SpeckDL. There are no global variables, no hidden state, no ambient context. Everything a speck can observe or modify is declared in its `state` block.
+
+#### Init
+
+The `init` block sets the initial values of all state variables. Init expressions use equality (`==`) rather than assignment (`:=`) — they describe what must be true at startup, not a sequence of operations:
+
+```
+init {
+    counter == 0
+    users == emptySet
+    balances == emptyMap
+    history == List.empty
+    leader == { id: "", term: 0 }
+}
+```
+
+If any state variable is missing from `init`, the compiler reports an error. Every variable must have an initial value.
+
+### 2.3 Type System
+
+SpeckDL supports the following types:
+
+| Type | Syntax | Description |
+|------|--------|-------------|
+| Boolean | `Bool` | True or false |
+| Natural number | `Nat` | Non-negative integer (≥ 0) |
+| Integer | `Int` | Signed integer |
+| String | `String` | UTF-8 text |
+| Set | `Set(T)` | Unordered collection of distinct elements of type T |
+| Map | `Map(K, V)` | Key-value mapping from type K to type V |
+| List | `List(T)` | Ordered sequence of elements of type T |
+| Record | `{ field: T, ... }` | Named fields with typed values |
+| Optional | `T \| null` | A value of type T, or null |
+
+**Sets** support `union`, `intersection`, `\` (difference), `subsetOf`, `in`, `notIn`, and `size()`. The literal `emptySet` represents the empty set. Set literals use curly braces: `{"a", "b", "c"}`.
+
+**Maps** support key access (`m[k]`), key assignment (`m[k] := v`), `.keys`, `.values`, and `in` for key membership. The literal `emptyMap` represents the empty map. Maps have no literal constructor — they are built incrementally through assignments.
+
+**Lists** support indexed access (`list[i]`, 1-based), `length()`, `take()`, `concat()`, and `List.empty` for the empty list.
+
+**Records** are anonymous structural types. Two records are the same type if they have the same field names and types, regardless of declaration order:
+
+```
+type Point = { x: Nat, y: Nat }
+// Equivalent to { y: Nat, x: Nat }
+```
+
+Record values are constructed with braces: `{ x: 3, y: 5 }`. Field access uses dot notation: `point.x`.
+
+**Optional types** use the `| null` syntax. A field typed `String | null` can hold either a string or the null value. Null checks use `== null` and `!= null` in expressions.
+
+### 2.4 Actions
+
+Actions are the transitions of the state machine. Each action has a name, optional parameters, preconditions (`require`), a body of state mutations, and optional return/emit statements:
+
+```
+action Transfer(from: Nat, to: Nat, amount: Nat) {
+    require from in accounts
+    require to in accounts
+    require balances[from] >= amount
+
+    balances[from] := balances[from] - amount
+    balances[to] := balances[to] + amount
+    emit TransferCompleted { from: from, to: to, amount: amount }
+    return balances[from]
+}
+```
+
+#### Preconditions (require)
+
+`require` statements are boolean expressions that must be true for the action to execute. If any require fails, the action aborts and no state is modified. Requires are the runtime enforcement of invariants — they're compiled to guard clauses in generated code.
+
+In the generated TypeScript, a failed `require` throws a `PreconditionError`. In the generated WASM, it traps.
+
+#### State Mutation (assignment)
+
+State variables are modified with the `:=` operator. Assignments can target:
+- Simple variables: `counter := counter + 1`
+- Map entries: `balances[id] := 100`
+- Set membership: `users := users union {newUser}`
+- Record fields (in expressions, not directly assigned): `balances[pt.to] := balances[pt.to] + pt.amount`
+
+All assignments within an action are atomic — either all succeed (the action completes) or none apply (a require failed).
+
+#### Let Bindings
+
+`let` binds an expression result to a local name for use later in the action body. Let bindings are immutable:
+
+```
+action CommitTransfer(tid: Nat) {
+    require tid in pendingTransfers.keys
+
+    let pt := pendingTransfers[tid]
+    balances[pt.to] := balances[pt.to] + pt.amount
+    pendingTransfers := pendingTransfers \ {tid}
+}
+```
+
+Let bindings reduce repetition and make action bodies more readable. They are scoped to the enclosing action.
+
+#### If Statements
+
+SpeckDL supports conditional logic within actions:
+
+```
+action GrantVote(voter: String, req: RequestVoteReq) {
+    require req.term >= serverState[voter].currentTerm
+
+    if req.term > serverState[voter].currentTerm {
+        serverState[voter].currentTerm := req.term
+        serverState[voter].role := "follower"
+    }
+
+    serverState[voter].votedFor := req.candidateId
+}
+```
+
+If conditions must be boolean expressions. There are no else-if chains (nest if statements for multi-branch logic).
+
+#### Emit
+
+`emit` produces a typed event that becomes part of the provenance graph. Events are structured records:
+
+```
+emit TransferCreated { id: tid, from: from, to: to, amount: amount }
+```
+
+Emitted events serve three purposes:
+1. They make state machine execution traceable.
+2. They appear in generated PROV-O graphs as activities.
+3. In generated TypeScript, they're emitted via an `EventEmitter` interface for integration with logging, metrics, and audit systems.
+
+#### Return
+
+`return` produces an optional output value from the action. Actions that don't call `return` implicitly return void. Return values are typed according to the action's signature or inferred from the return expression.
+
+#### Forall Loops
+
+Actions can iterate over sets with `forall` loops:
+
+```
+action TMCommit {
+    require tmPrepared == rms
+
+    tmState := "committed"
+    forall rm in rms:
+        rmState[rm] := "committed"
+}
+```
+
+The loop variable (`rm`) is read-only. Forall loops iterate over the entire collection; there is no `break` or early termination.
+
+### 2.5 Invariants
+
+Invariants are properties that must hold in every reachable state of the machine. They are declared with the `invariant` keyword:
+
+```
+invariant NoNegativeBalances {
+    forall id in accounts:
+        balances[id] >= 0
+}
+```
+
+Invariants serve two roles:
+
+1. **Documentation.** They state the safety properties the system guarantees, in unambiguous, executable form.
+2. **Runtime verification.** In generated TypeScript and WASM, invariants are checked after every action execution. A violated invariant throws a `InvariantViolationError` (TypeScript) or traps (WASM).
+
+#### Quantified Invariants
+
+SpeckDL supports universal quantification (`forall`) in invariants:
+
+```
+invariant SingleLeaderPerTerm {
+    forall s1 in servers:
+        forall s2 in servers:
+            s1 != s2 and
+            serverState[s1].role == "leader" and
+            serverState[s2].role == "leader" implies
+                serverState[s1].currentTerm != serverState[s2].currentTerm
+}
+```
+
+Quantified invariants are compiled to nested loops in generated code. For finite state spaces (the common case), this provides tractable runtime verification. For large or infinite state spaces, invariants can be selectively disabled at compile time (`--skip-invariants`) and verified through external model checking.
+
+#### Logical Operators
+
+Invariants and require expressions use C-like logical operators:
+
+| Operator | Meaning |
+|----------|---------|
+| `==`, `!=` | Equality, inequality |
+| `<`, `<=`, `>`, `>=` | Comparison |
+| `+`, `-`, `*`, `/` | Arithmetic |
+| `and`, `or`, `not` | Logical conjunction, disjunction, negation |
+| `implies` | Logical implication (A implies B) |
+| `in`, `notIn` | Set/map membership |
+| `subsetOf` | Set subset relation |
+| `union`, `\` | Set union, set difference |
+| `size()` | Set cardinality |
+| `length()` | List length |
+
+### 2.6 Next — Action Composition
+
+The `next` declaration defines which actions can follow which states. It's the state machine's transition relation:
+
+```
+next: OpenAccount | CreateTransfer | CommitTransfer | VoidTransfer
+```
+
+This declares that at any point, any of these four actions may be invoked. SpeckDL does not currently support sequential action composition (`action1 then action2`) — the `next` operator `|` means "any of these, chosen non-deterministically." This matches the TLA+ model where the environment (user, scheduler, network) chooses the next action.
+
+### 2.7 Complete Example: Two-Phase Commit
+
+Here is a complete SpeckDL specification for the Two-Phase Commit protocol, demonstrating types, state, init, invariants, actions with require/emit/forall, and action composition:
+
+```
+speck TwoPhaseCommit {
+    state {
+        rmState: Map(String, String)
+        tmState: String
+        tmPrepared: Set(String)
+        msgs: Set(Message)
+        rms: Set(String)
+    }
+
+    init {
+        let allRms := {"rm1", "rm2", "rm3"}
+
+        rms == allRms
+        rmState == mapKeys(allRms, "working")
+        tmState == "init"
+        tmPrepared == emptySet
+        msgs == emptySet
+    }
+
+    invariant TPConsistency {
+        tmState == "committed" implies
+            forall rm in rms: rmState[rm] == "committed"
+        tmState == "aborted" implies
+            forall rm in rms: rmState[rm] == "aborted"
+    }
+
+    action RMPrepare(rm: String) {
+        require rm in rms
+        require rmState[rm] == "working"
+
+        rmState[rm] := "prepared"
+        msgs := msgs union {{ type: "Prepared", rm: rm }}
+        emit Prepared { rm: rm }
+    }
+
+    action TMCommit {
+        require tmState == "init"
+        require tmPrepared == rms
+
+        tmState := "committed"
+        forall rm in rms:
+            rmState[rm] := "committed"
+        emit AllCommitted {}
+    }
+
+    action TMAbort {
+        require tmState == "init"
+
+        tmState := "aborted"
+        forall rm in rms:
+            if rmState[rm] != "committed":
+                rmState[rm] := "aborted"
+        emit Aborted {}
+    }
+
+    next: RMPrepare | TMCommit | TMAbort
+}
+```
+
+This specification is 48 lines. The compiled output spans ~300 lines of TypeScript, ~200 lines of WAT (WebAssembly Text), and three machine-readable provenance documents. Every generated line traces back to these 48 lines of intent.
+
+### 2.8 What SpeckDL Doesn't Have
+
+It's instructive to note what SpeckDL deliberately omits:
+
+**No functions.** There are no user-defined functions, no recursion, no higher-order abstractions. This is intentional — specifications should be flat and auditable. Complex logic belongs in the implementation, not the spec.
+
+**No loops (except forall).** There are no while loops, no for loops with mutable state, no iterators with side effects. The only iteration construct is `forall`, which is side-effect-free in invariants and bounded in actions.
+
+**No concurrency primitives.** SpeckDL models state machines sequentially. Concurrency is expressed through non-deterministic interleaving of actions (`next: A | B | C`), not through threads, locks, or channels. This is the same approach as TLA+.
+
+**No I/O.** Actions can `emit` events and `return` values, but there is no file system access, no network calls, no database queries. The spec is pure computation over typed state.
+
+**No error handling.** There are no try/catch blocks, no error values, no exception types. If a `require` fails, the action aborts. That's the only error path.
+
+These omissions are the point. SpeckDL constrains the spec author to describe what the system does and what must be true — not how it does it, not how it handles failure, not how it optimizes. The implementation fills in those details.

 ## 3. Compiler Architecture