Spock v0 — language specification

Status: normative for the v0 toolchain. Scope: the implemented declarations — table/auth table, record, fn/mut fn, and seed — one embedded-SQLite runtime, and a minimal HTTP protocol. Future declarations such as view, role, and policy remain deliberately absent and reserved (§2.3) so v0 programs stay forward-compatible.

A conforming implementation accepts exactly the language defined here, reports the diagnostics of §4 against non-conforming programs, materializes the storage model of §7, and serves the protocol of §8. The compiled contract (§6) is the interchange artifact; the toolchain in crates/ is one conformance of this document, not its definition (RFD 0006).

1. Source files

A Spock source file is UTF-8 text, conventionally *.spock. A file contains zero or more table, record, or function declarations and zero or more seed blocks, in any order. auth modifies a table and mut modifies a function. Multiple seed blocks concatenate in file order.

Comments run from // to end of line. A comment opening with exactly three slashes (///, an outer doc comment) or with //! (an inner doc comment) is documentation, carried into the contract (§2.4, §6, RFD 0016); four or more slashes is an ordinary comment. Whitespace (spaces, tabs, newlines) separates tokens and is otherwise insignificant; there are no statement terminators.

2. Lexical structure

2.1 Identifiers

ident := [a-z_][a-z0-9_]*

Identifiers are lowercase snake_case only. An identifier containing an uppercase letter is a lexical error (L002). Keywords (§2.3) may not be used as identifiers.

2.2 Literals

string — "..." with escapes \", \\, \n, \t. Unterminated strings are a lexical error (L003).
raw string — """...""": multi-line, no escape processing (a \n is two characters), terminates at the first """ — content needing a literal """ must use the single-line form. Unterminated raw strings are a lexical error (L006). Both forms produce the same string token; the grammar does not distinguish them.
integer — optional - followed by decimal digits; must fit in a signed 64-bit integer (L004).
float — optional -, decimal digits, ., decimal digits: plain decimal notation only, both digit runs required (0.5, not .5 or 1.), no exponents. Literals fit their own type: 0 is not a float literal and 0.0 is not an integer literal.
boolean — the keywords true, false.

2.3 Keywords

Active in v0:

table  auth  record  fn  mut  key  unique  check  seed  on  delete  restrict
cascade  set  null  text  int  float  bool  timestamp  uuid
auto  now  me  true  false

sql and unchecked are contextual keywords: they form a fn body (§3) but remain legal identifiers everywhere else.

(set, null, and float became keywords in July 2026, mut followed with fn v2 (RFD 0012), check with the value tier (RFD 0013), and auth and me with the actor seam (RFD 0014) — source-level breaks for programs that used them as identifiers. The §6 freeze governs the contract artifact, not source compatibility; v0.x source may still move.)

Reserved for future versions (using one as an identifier is an error, L005):

view  role  policy  error  state  extern  unsafe  derived
protected  module  enum  expect  transition  upsert  match  with

unsafe is reserved for the runtime-integrity tier and is deliberately not the escape-body marker: the escape is unchecked — the checker does not verify it, but the runtime stays sound (RFD 0011 §3).

2.4 Doc comments

Two comment forms are doc comments (RFD 0016) — carried into the compiled contract (§6) rather than discarded:

/// — an outer doc comment: documents the entity that follows it (a table, record, field, fn, or fn parameter).
//! — an inner doc comment: documents the enclosing file, i.e. the contract. Legal only in the preamble, before the first declaration — spock has no modules, so the file is the only scope a //! can document.

Exactly three slashes is an outer doc; //! is an inner doc; // and four or more slashes (////, /////, …) are ordinary comments and are discarded. A doc comment’s text is its content after the sigil, with at most one leading space stripped and trailing whitespace trimmed; consecutive doc lines of the same kind — separated only by whitespace or ordinary comments — join with a newline into one doc string. A run whose joined text is empty documents nothing (a lone /// is a no-op).

An outer doc that precedes no documentable entity — before }, the end of the file, a key/unique/check row item, or a seed block — is a dangling doc comment (L011). An inner doc after the first declaration is misplaced (L012); document that item with /// instead. Doc comments are lexical trivia that carry attachment semantics: like ordinary comments they do not appear in the grammar of §3.

3. Grammar

file        = { table_decl | record_decl | fn_decl | seed_block } ;

table_decl  = [ "auth" ] "table" ident "{" { table_item } "}" ;
              (* `auth table` marks the identity anchor (RFD 0014); at most
                 one, with a single scalar key — E045/E046 *)
table_item  = key_decl | unique_decl | check_decl | field_decl ;

record_decl = "record" ident "{" { table_item } "}" ;
              (* items share the table grammar; table-only constructs are
                 rejected by the checker, E033 *)

fn_decl     = [ "mut" ] "fn" ident "(" [ param { "," param } [ "," ] ] ")"
              "->" ret [ "!" ident { "|" ident } ]
              "{" escape { escape } "}" ;
              (* unmarked = read, engine-enforced; `mut` may write —
                 §7.4, RFD 0012 *)
escape      = "unchecked" "sql" "(" string ")" ;
              (* statements run in order, one transaction; the last one
                 produces the return value — §7.4, RFD 0012 *)
param       = ident ":" type [ "?" ] ;
ret         = "[" ret_target "]" | ret_target [ "?" ] ;
ret_target  = "text" | "int" | "float" | "bool" | "timestamp" | "uuid"
            | ident ;
              (* the ident names a table or record; a type keyword is a
                 scalar return — one column, bare values on the wire *)

key_decl    = "key" "(" ident "," ident { "," ident } ")" ;
unique_decl = "unique" "(" ident "," ident { "," ident } ")" ;
check_decl  = "check" "(" ident "," ident { "," ident } ")" ident ;
              (* a cross-column row check (RFD 0013): the trailing ident
                 names a validator fn; mirrors unique_decl *)

field_decl  = [ "key" ] ident ":" type [ "?" ] [ "check" ident ] [ "unique" ]
              [ "=" default ]
              [ "on" "delete" ( "restrict" | "cascade" | "set" "null" ) ] ;
type        = "text" | "int" | "float" | "bool" | "timestamp" | "uuid"
            | ident | set_type ;
set_type    = string { "|" string } ;
              (* a closed-set type (RFD 0013): the value is one of these
                 strings. The singleton/duplicate/empty-value laws are the
                 checker's, E043 *)
default     = "auto" | "now" | "me" | literal ;
              (* `me` is the current actor (RFD 0014); legal only on a
                 reference to the `auth` table — E016 carve-out / E047 *)
literal     = string | integer | float | "true" | "false" ;

seed_block  = "seed" "{" { seed_stmt } "}" ;
seed_stmt   = [ ident "=" ] ident "{" [ seed_field { "," seed_field } [ "," ] ] "}" ;
seed_field  = ident ":" seed_value ;
seed_value  = literal | ident | file_value ;    (* ident = seed binding *)
file_value  = "file" "(" string ")" ;           (* a seed asset, RFD 0018 *)

Disambiguation: inside a table body, key followed by ( is a composite key_decl; otherwise it is the inline-key modifier of a field_decl. unique followed by ( at item position is a unique_decl; after a field’s type it is the field modifier. Field modifiers appear in exactly the order shown. A key_decl/unique_decl names two or more fields; a single-field key or unique is written as the field modifier.

A type that is a set of string literals joined by | is a closed-set type (RFD 0013): the field’s value is one of the listed strings, storage is TEXT, and a <table>_<field>_invalid CHECK enforces membership. A closed set may not be a key field, a record field, or a fn parameter (E043/E034/E036) — the enum case is a stored table-field type in v0. A set field’s default and any seed literal must be one of its values (E009/E023).

A check names a validator fn (RFD 0013): a field check (name: type check fn) or a cross-column row check (check (a, b) fn). The referenced fn must be an unmarked (read) fn returning bool from a single SELECT whose body is one boolean expression over its parameters — no FROM/WHERE/other clause and no subquery (E042), so it inline-expands into a CHECK (§7.1); it may not use a non-deterministic function (E042). Its parameters match the checked fields’ value types positionally. A check may not attach to a closed-set field (which self-validates) or an auto/now-defaulted field (E042); an unknown fn is E041. The validator is an ordinary read fn too — callable on the Query root and via GET /rest/v1/rpc — so a client can pre-validate against the same rule. Every value constraint derives a <table>_<fields>_invalid code, and these — like all derived codes — must be unique across the program (E044): the constraint name is the sole runtime routing channel (§7.2), and the underscore-join is not injective.

A type that is an ident is a reference: the field holds the key of a row of the named table. on delete is only meaningful on references; the default is restrict. set null requires an optional reference (E040) — deleting the target nulls the field instead of blocking or cascading, so it derives no restricted error for the target table.

In a fn body, unchecked and sql are contextual keywords (§2.3): the body is a sequence of one or more unchecked sql("...") calls (RFD 0012) — each the escape hatch and its forced acknowledgment, each carrying exactly one SQL statement, verbatim; the triple-quoted form (§2.2) is the ergonomic carrier. The escape may replace the body, never the contract: name, parameters, return shape, and declared errors stay in the language. The unchecked marker states the true thing (RFD 0011): the checker does not verify this body — the engine validates it at load (§7.4) and the runtime stays sound, but the SQL’s logic is the author’s word. An unmarked sql(...) is a parse error whose message says exactly that.

4. Static semantics

The checker resolves names and validates the program. All diagnostics carry a source span and a stable code. E-codes are program errors (compilation fails); L-codes are lexical/parse errors.

Code	Condition
E001	duplicate table name
E002	duplicate field name within a table
E003	unknown type (not builtin, not a declared table)
E005	table declares no key
E006	table declares more than one key (two inline, two composite, or both)
E007	composite key names an unknown field
E008	key field (inline or composite member) is optional
E009	default incompatible with the field type (§5.2)
E010	reference target table has a composite key (v0 restriction)
E011	unique group names an unknown field
E012	table has no fields
E014	duplicate field within a composite key or unique group
E015	`on delete` on a non-reference field
E016	default on a reference field
E017	a table’s key type resolves through a reference cycle (`a.key: b`, `b.key: a`)
E020	seed row names an unknown table
E021	seed row names an unknown field
E022	seed row omits a required field that has no default
E023	seed value incompatible with the field type (literal type, uuid or timestamp format, checked at compile time)
E024	seed value references an unknown or not-yet-defined binding
E025	seed binding’s table does not match the reference target
E026	seed binding used as the value of a non-reference field
E027	duplicate seed binding name
E028	seed row sets the same field twice
E030	duplicate record name
E031	record name collides with a table (one type namespace)
E032	record has no fields
E033	table-only syntax in a record (`key`, `unique`, default, `on delete`)
E034	record field is not a builtin scalar
E035	duplicate fn name (fns are their own namespace — a fn may share a table’s name)
E036	fn parameter type unknown, a record, or a composite-key table
E037	fn return shape is not a declared table or record
E038	duplicate fn parameter name
E039	duplicate error code in the `!` clause. (An unknown code no longer errors — RFD 0012: a code that is neither derived nor reserved is a refusal minted by this fn, §7.4. The cost is honest: a misspelled derived code mints dead metadata instead of failing — never wrong behavior, since the real constraint still routes to the true code at runtime)
E040	`on delete set null` on a required reference (only an optional field can be nulled)
E041	`check` names a fn that does not exist (RFD 0013)
E042	`check` validator law violated: not a read fn, not `bool`, not a single clauseless `SELECT`, non-deterministic, wrong arity/param types, or attached to a closed-set/`auto`/`now` field (RFD 0013)
E043	closed-set type is degenerate: fewer than two values, a duplicated value, an empty value, or used as a key field (RFD 0013)
E044	two derived error codes collide (the constraint name is the routing channel; the underscore-join is not injective, RFD 0013)
E045	more than one `auth table` — the actor space has one identity table (RFD 0014)
E046	the `auth table`’s key is not a single scalar column (`spock_actor()` returns one value, RFD 0014)
E047	`= me` is not on a reference to the `auth` table, or no anchor is declared (RFD 0014). `= me` on a reference is the one carve-out to E016
E048	a user table is named `storage_object` — the name is reserved for the storage builtin (RFD 0018)
E049	`file("...")` on a field that does not reference `storage_object` (RFD 0018)
E050	a `file("...")` seed asset path is absolute or escapes the source directory (RFD 0018)

Notes.

Doc-comment placement is checked by the parser (RFD 0016, §2.4): L011 — a /// that documents nothing (dangling); L012 — a //! after the first declaration (misplaced inner doc).
E034/E036 also reject a closed-set type in a record field / fn parameter; E009/E023 also reject a set field’s default / seed literal that is not one of its values (RFD 0013).
A reference field may be a key member (join tables: key (follower, target) over two references is valid).
unique on an optional field is permitted; rows with the field absent do not conflict (§7.1).
Self-references (reply_to: comment?) are permitted.
Seed statements execute in file order; a binding must be defined before use (E024). Bindings live in one file-wide namespace (E027). A binding on a composite-key row is legal but unusable, since references target single-key tables only (E010).

5. Types and values

5.1 Builtin types

Spock	JSON (wire)	SQLite (storage)	Notes
`text`	string	`TEXT`
`int`	number (integer)	`INTEGER`	signed 64-bit
`float`	number	`REAL`	IEEE 754 double; a whole JSON number is accepted on the wire; NaN/infinity have no JSON spelling and render as `null`
`bool`	boolean	`INTEGER` (0/1)	converted at the edge
`timestamp`	string, RFC 3339 UTC	`TEXT`	instants only (RFD 0005 stance); stored canonically — UTC, fixed six-digit fractional seconds — so text order is chronological order; inputs in any RFC 3339 offset are canonicalized on write
`uuid`	string, canonical hyphenated	`TEXT`	stored lowercase-canonical
reference	value of the target’s key	target key’s storage type

Optionality is ? on the type. An absent optional value is JSON null and SQL NULL. Optionals are absence, not a value (RFD 0005 stance): providing null for a required field is a validation error, identical to omitting it.

One deliberate carve-out — update inputs (§7.2 “Updates”): there, an absent field means keep the stored value and an explicit null means clear it (only legal on optional fields; null on a required field is the derived required error). Updates are the one place absence and null mean different things, because an update must be able to say both “don’t touch this” and “unset this”.

Files — a field typed storage_object is a reference to the builtin storage_object table (RFD 0018), which the checker injects into the contract whenever a field or fn parameter references it (and reserves the name, E048). Its value is the target key (a uuid) and it expands like any reference (a nested object under GraphQL); the bytes move over the storage protocol (§8.3), never inline. The table is read-only on the open floor — no insert/update/delete mutations are derived for it, so metadata cannot desync from bytes; its only write path is the storage protocol.

5.2 Defaults

Default	Valid on	Meaning
`auto`	`uuid`	runtime generates a UUIDv7 at insert
`now`	`timestamp`	runtime captures UTC now at insert
`me`	reference to the `auth` table	runtime stamps the current actor at insert (RFD 0014)
string literal	`text`
integer literal	`int`
float literal	`float`
boolean literal	`bool`

Anything else is E009. On the floor’s write path, defaults are applied by the runtime at insert time (§7.2); auto/now are also installed as engine DEFAULT clauses so escape bodies receive identical values (§7.1) — both paths mint from one clock and one id format, so every conforming runtime behaves identically and the paths cannot drift. Defaults apply at insert only; updates never apply them.

me (RFD 0014) is the exception, a strong preset. It is materialized by the runtime on the write path like auto/now, but (a) it is not installed as a DDL DEFAULT — spock_actor() is DIRECTONLY (§7.1), so an escape that stores the actor names spock_actor() itself (the same value, one source, no drift); and (b) it is removed from the client insert and update surface (the derived GraphQL <t>_insert_input/<t>_set_input and the generated TS types omit it), so a client cannot forge the identity column. An anonymous insert of a required = me field is the derived required error (§7.2), not a null — the floor never stores an unauthenticated identity. Seed runs before any actor exists, so a seed row must name every required = me column (E022).

6. The compiled contract

Compilation produces one JSON document — the contract — which is the artifact runtimes load and tools consume. Shape (informative example):

{
  "spock": "v0",
  "tables": [
    {
      "name": "user",
      "key": ["id"],
      "fields": [
        { "name": "id", "type": { "kind": "uuid" }, "optional": false,
          "unique": false, "default": { "kind": "auto" } },
        { "name": "username", "type": { "kind": "text" }, "optional": false,
          "unique": true, "default": null },
        { "name": "invited_by",
          "type": { "kind": "ref", "table": "user", "on_delete": "restrict" },
          "optional": true, "unique": false, "default": null }
      ],
      "uniques": [],
      "errors": [
        { "code": "user_already_exists", "kind": "key",
          "fields": ["id"], "status": 409 },
        { "code": "user_username_taken", "kind": "unique",
          "fields": ["username"], "status": 409 },
        { "code": "user_username_required", "kind": "required",
          "fields": ["username"], "status": 422 },
        { "code": "user_invited_by_not_found", "kind": "ref_not_found",
          "fields": ["invited_by"], "status": 422 },
        { "code": "user_restricted", "kind": "restricted",
          "fields": [], "status": 409 }
      ]
    }
  ],
  "seed": [ { "table": "user", "binding": "maya",
              "fields": { "username": "maya" } } ]
}

Stability. The contract shape is frozen for v0.x under the spock version field: changes are additive only (new optional fields on existing objects); renaming or removing anything shown above is a breaking change that bumps spock. Clients, generators, and agents may bind to this shape — that is what it is for. Additions so far: records (named wire shapes) and fns (declared functions, §7.4) — both default to [] when absent, so pre-fn contract JSON still loads — and returns.scalar on a fn (boolean, defaults to false; when set, returns.of names a builtin scalar type instead of a shape). The vocabulary has also grown: type kind float, default kind float, float seed values, and on_delete: "set_null", (RFD 0013) the field type kind set ({ "kind": "set", "values": [...] }) with the error kind invalid, and (RFD 0014) the table flag anchor (true on the one auth table) plus the default kind actor ({ "kind": "actor" }, the = me stamp), and (RFD 0016) an optional doc string on the contract and on each table, field, record, record field, fn, and fn parameter — the //////! doc comments, absent when undocumented. Additive means old JSON keeps loading in new consumers — it does not mean old consumers can read a contract that uses new vocabulary (a pre-float reader rejects "kind": "float"), and a consumer that ignores returns.scalar will misread a scalar of as a shape name. Consumers should reject vocabulary they do not know rather than guess. A fn’s sql body travels in the contract verbatim: the contract is the executable artifact, and v0 is the open tier by decision (§8) — GET /~contract exposes it. Since RFD 0012 the sql field is a statement array (execution order, last statement answers); readers must also accept the pre-v2 bare-string form as a one-statement body, which is how old contract JSON keeps loading. New contracts always write the array. Fns also carry readonly (boolean, defaults to false): polarity (§7.4). The default is false because every pre-v2 fn lived on the Mutation root — absent means “the mutation it always was”. And fns carry refusals (string array, defaults to []): the subset of errors this fn mints (§7.4) — errors remains the full declared failure surface, so consumers that only read errors keep seeing everything.

6.1 Derived errors

No error in v0 is hand-written; every error is derived from the schema. Per table:

Kind	Derived from	Code	Status
`key`	the key	`<table>_already_exists`	409
`unique`	each unique field/group	`<table>_<fields joined by _>_taken`	409
`required`	each required field that can be absent on insert (no default) or cleared on update (non-key)	`<table>_<field>_required`	422
`ref_not_found`	each reference field	`<table>_<field>_not_found`	422
`restricted`	any inbound `restrict` reference	`<table>_restricted`	409
`invalid`	each closed-set field (RFD 0013)	`<table>_<field>_invalid`	422

These are part of the contract (§6) — visible to clients before any request is made — and the vocabulary is frozen for v0.x with the same rule: new kinds may be added; the five above, their code-derivation templates, and the reserved non-derived codes (not_found, type_mismatch, unknown_field, bad_request, internal) do not change meaning or spelling. Error codes are API: clients are expected to match on them.

Since RFD 0012 there is one added kind: refused — a code a fn mints in its ! clause and raises from its body (§7.4). Refusals are declared, not derived, but never hand-written at the call site either: the signature names the rule, the body raises it, the envelope carries it (status 409, table: null, fields: []). Refusal codes share the one code namespace with derived codes; their shape is free-form, and nothing prevents a future table from deriving a colliding code — rename the refusal if that ever bites.

RFD 0013 adds the kind invalid — a value-constraint violation: a closed-set membership miss (§7.1) or a validator-check failure. Its status is 422, not 409: a 409 (key/unique/restricted) is a conflict with existing state — the same payload could succeed against a different database — while a value-constraint violation is intrinsic to the payload, next to required and type_mismatch. The code is <table>_<field>_invalid, derived from the declaration site, never hand-written.

7. Dynamic semantics

7.1 Storage materialization

Each table compiles to one SQLite table, declaration order preserved, all identifiers double-quoted:

types per §5.1; required fields NOT NULL;
the key → PRIMARY KEY (...);
each unique field/group → a table-level UNIQUE (...);
each closed-set field → a CONSTRAINT "<table>_<field>_invalid" CHECK ("<field>" IN (...)) (RFD 0013), the members quoted with ' doubled, emitted after the UNIQUE block and before the foreign keys. The constraint name is the derived error code, verbatim — a named CHECK fails with CHECK constraint failed: <name> and nothing else, so the name is the whole runtime routing channel (§7.2);
each check (field or row, RFD 0013) → a CONSTRAINT "<table>_<fields>_invalid" CHECK (<expr>) where <expr> is the validator fn’s body inline-expanded: its leading SELECT stripped, each :param textually replaced by its positionally-bound "column" (never inside a quoted string). Inline expansion — not a registered function — keeps the .db pure SQL, so third-party readers still open it; and the DDL prepare validates the expanded expression (an unresolved column or prohibited construct fails at load). Field checks in field order, then row checks; the first violated constraint reports (SQLite);
each reference → REFERENCES "<target>" ("<target key>") ON DELETE RESTRICT|CASCADE|SET NULL; the runtime sets PRAGMA foreign_keys = ON;
each declared default → a DEFAULT clause: literals verbatim (strings quoted, ' doubled), auto → (spock_uuid()), now → (spock_now()). A = me field emits no DEFAULT clause (RFD 0014): spock_actor() is DIRECTONLY, so the actor is materialized on the write path instead (§7.2), and an escape names spock_actor() itself.

Engine builtins. The runtime registers SQL functions on the connection before DDL: spock_uuid() (UUIDv7) and spock_now() (RFC 3339 UTC) — the same generators the write path uses for auto and now — and spock_refuse(code), the refusal raise channel (§7.4; direct-only: nothing indirect may raise). When a table is auth-marked (RFD 0014) a fourth is registered: spock_actor() — the current actor’s key (§8), NULL when anonymous — registered only with an anchor present (a body that calls it without one fails at prepare, the identity-needs-a-consumer rule) and DIRECTONLY like spock_refuse, not like spock_now: the actor is request-scoped state, correct only inside a fn call, never in a DEFAULT/CHECK the actor-blind floor evaluates. func::call re-binds it to the request’s actor before each fn transaction. Consequences: an escape body (§7.4) may omit defaulted columns from an INSERT and receive the engine’s own values via the DEFAULT clauses, or call the builtins directly; a value minted inside the escape is indistinguishable in format and id-version from one the engine minted. Hand-rolling ids or timestamps in escape SQL is never necessary.

The floor’s write path (§7.2) still materializes defaults itself — the DEFAULT clauses exist for the escape, and both mint from the same functions, so the paths cannot drift.

SQL NULLs do not conflict under UNIQUE, which implements §4’s rule for optional uniques.

7.2 Writes

The v0 runtime validates every write against the contract before the engine sees it, inside one transaction per write.

Inserts, in this order:

body must be a JSON object; unknown fields are rejected;
type-check each provided value (§5.1; uuid/timestamp format enforced); a closed-set value that is not a member → the derived invalid error (RFD 0013);
apply defaults; a required field still absent → required error. A = me field (RFD 0014) is stamped with the request actor here; an anonymous insert of a required = me field routes to that same derived required error (not a NULL — the floor never stores an unauthenticated identity);
each provided reference is checked for existence → ref_not_found;
the engine insert runs; unique/key violations map to the derived codes.

Closed-set membership is thus checked twice — once on this floor path (so the floor error carries the values) and once by the engine CHECK (the sole enforcer for escape-body writes, which never touch this path); both produce the same derived invalid code, so the layers cannot drift.

Updates address one row by its full (possibly composite) key and carry a change set with §5.1’s update semantics (absent = keep, null = clear):

unknown fields are rejected; key fields cannot appear in the change set (keys are immutable — the key is the row’s identity);
per-field: explicit null clears an optional field or is the derived required error; non-null values type-check as on insert;
the row must exist — a write that did not happen is an error (not_found), unlike a read miss;
an empty change set is a validated no-op returning the row;
changed references are checked for existence → ref_not_found;
the engine update runs; unique violations map to the derived codes exactly as on insert; defaults are never applied (§5.2);
the stored row is returned.

Deletes address one row by its full key, check inbound restrict references first (→ restricted), then delete; cascade and set null references delegate to the engine (children are deleted or their reference field nulled, respectively). A delete returns the row as it read before deletion; deleting a missing row is not_found.

The v0 runtime serializes database access (single connection); this is a documented prototype property, not a contract guarantee.

7.3 Seed

Seed rows execute at startup, in order, through the same write path as §7.2. A seed that violates the contract aborts startup with the derived error and the row’s source location. There are no migrations in v0: on every load the database is materialized fresh and the seed replayed (RFD 0008 §3 — disposable state is doctrine). Seed may not call fns.

Seed assets (RFD 0018). A field that references storage_object may take file("./path") — a seed-time asset load. At load the runtime reads the file relative to the source file’s directory, materializes a committed storage_object (name = basename, content_type = mime-guessed, size, checksum = sha256, owner = NULL), stores its bytes, and the field takes the new object’s id. file is a soft keyword (special only as file( in seed-value position). The path must be relative and stay within the source directory (E050) and may only feed a storage_object reference (E049), both checked at compile time; the bytes are read at load, so a missing asset fails this seed replay. The seed is therefore a bundle: the .spock plus its assets.

7.4 Functions

A fn (§3) is a declared operation whose contract half — name, typed parameters, return shape, declared error codes — belongs to the language, and whose body is a sequence of SQL escapes, carried verbatim in the contract and each marked unchecked at the declaration site (§3, RFD 0011). The escape may replace the body, never the contract. spock check reports the count of unchecked escapes — the ledger of what the language did not verify. Since RFD 0013 spock check is also the full load proof: it materializes the schema in an in-memory engine — the same open path spock run uses (DDL prepare, fn-body validation, the default-vs-check proof of §7.1, seed replay) — so everything the engine would reject at load surfaces at check time, without starting a server.

The body is a statement sequence (RFD 0012). Statements execute in declaration order inside one transaction. The last statement produces the return value; earlier statements are guards and effects — they are executed to completion and their result rows are discarded. A body that wants to answer with a row an earlier statement touched re-reads it (same transaction; one cheap SELECT is the price of a flat grammar).

Polarity (RFD 0012). An unmarked fn is a read; mut fn may write. The unmarked form is the read because the forgotten-mut failure is the visible one (RFD 0004): the engine checks every statement of an unmarked fn with sqlite3_stmt_readonly at load, and a statement that may write aborts startup naming the fn and the statement. mut grants write permission without requiring writes. Polarity decides the surface: read fns are GraphQL Query root fields and answer GET /rest/v1/rpc/<fn>; mut fns are Mutation root fields and are POST-only (§8). The contract carries it as readonly on the fn (§6).

Load-time validation. The engine validates every body at load, after DDL and before seed replay — a broken fn aborts startup, never a request. prepare compiles without executing, so all of this is checked with no data moved:

each escape is exactly one statement (trailing ; and comments are tolerated); an empty or comment-only escape is an error; multi-escape failures name their statement (statement 2: …);
every statement is a row statement: SELECT, INSERT, UPDATE, DELETE, REPLACE, WITH, or VALUES (allow-list, checked on the raw text before anything is prepared). A fn body reads and writes rows; engine state is the engine’s. This is load-bearing, not stylistic: SQLite reports PRAGMA and ATTACH as “read-only” and applies PRAGMAs at prepare time — without this gate an uncalled read fn could mutate the shared connection during validation itself — and BEGIN/COMMIT would break the one-transaction envelope below;
syntax and table/column resolution — the engine’s own message surfaces verbatim;
placeholders are :param only (?, ?N, @x, $x rejected), and they match the signature in both directions across the body: a placeholder that is not a declared parameter is an error, and so is a parameter used in no statement at all. Each statement binds only the parameters it names;
the last statement’s result columns equal the declared return shape’s fields, by name (duplicates rejected — row mapping is by name). A last statement returning no columns is an error: every fn answers with rows, so answering DML must use RETURNING (earlier statements need not). A scalar return (-> int and friends) requires exactly one result column instead; its name is irrelevant — there is no shape to match.

Execution. One call = one transaction spanning every statement: IMMEDIATE for mut fns (the serializable-by-default stance, RFD 0005), DEFERRED for reads — a read fn never takes the write lock. The request actor is bound to spock_actor() (§7.1) before the transaction opens, so any statement — read or write — may reference it (RFD 0014); a read fn calls it just as it may call spock_refuse. Arguments validate against the parameter types before the transaction opens; for fn arguments null means absent (there is no §5.1 update carve-out here): an absent or null optional parameter binds SQL NULL, an absent required parameter is bad_request. Rows map back by column name. Arity is enforced on the last statement’s rows before commit — a violated arity rolls the whole transaction back, earlier effects included:

Declared	Rows	Result
`-> t`	1	the row
`-> t`	0	error `not_found` — a write that did not happen must shout
`-> t`	≥2	error `internal` (truthful: the body broke its contract)
`-> t?`	0 / 1	`null` / the row
`-> t?`	≥2	error `internal`
`-> [t]`	any	the rows — uncapped; the author owns `LIMIT` (§8’s page discipline governs derived lists, not authored SQL)

Scalar returns follow the same arity table with bare values in place of rows (-> int → a number, -> [text] → an array of strings). SQL NULL values: for -> t? a missing row and a NULL value are both null, indistinguishable by design. For an un-suffixed scalar (and for every element of -> [t]) a NULL is the body breaking its declared contract, and surfaces as error internal before commit — never as a null smuggled under a non-nullable type (the GraphQL binding would otherwise violate its own SDL). Declare -> t? when null is possible. The same law covers shape fields: a NULL in a column the returned table or record declares non-optional (a LEFT JOIN miss, an aggregate over nothing) is internal before commit, for the same reason — column-name validation happens at load, but nullability is only known per row. Declare the record field optional when null is possible.

Errors. A constraint the SQL trips routes to the owning table’s derived error — cross-table, with no write-set declaration: the engine’s constraint message names table.column, which is enough to find the code. UNIQUE and PRIMARY KEY map to the table’s unique/key codes; NOT NULL maps to the derived required code; FOREIGN KEY maps to the reserved bad_request (the engine reports no table detail for FK failures — truth over guessing); anything else is internal. The declared ! code | code clause is metadata — introspection and clients see it — and codes the body can produce but the signature does not declare still surface truthfully.

Refusals (RFD 0012). A code in the ! clause that is neither a derived code nor a reserved code is a refusal minted by this fn — a product rule with a name. The body raises it through the engine builtin spock_refuse('<code>'), which always errors when evaluated — so the guard shape is a conditional selection:

SELECT spock_refuse('account_private')
WHERE EXISTS (SELECT 1 FROM user WHERE id = :target AND private)

Zero rows selected, nothing raised. The runtime routes a raised code only if this fn minted it: the envelope is the code itself, kind refused, status 409 (§6.1). Raising anything else is internal, before commit — an unminted code is the body breaking its signature, and a derived or reserved code can only be produced by its own mechanism: if bodies could raise user_username_taken by hand, derived errors would stop being evidence. A refusal raised mid-body rolls the whole transaction back like any other failure. spock_refuse is declaration-checked, not reachability-checked: a minted code the body never raises is dead metadata, visible in introspection, harmless at runtime. Read fns refuse too — SELECT spock_refuse(...) is a read-only statement.

8. HTTP protocol

The runtime serves plain HTTP + JSON on one port. The root namespace is protocol-owned: the ~ prefix is the meta surface, /rest/v1 carries the open reads, /graphql/v1 the GraphQL reads and writes (§8.2). Table names can therefore never collide with a protocol mount, and future surfaces (e.g. /auth/v1) claim mounts the same way.

The actor (RFD 0014). When a table is auth-marked, requests may carry X-Spock-Actor: <key> — the actor’s key value, verbatim and unverified in v0 (the ungoverned prototype tier; the seam a verified JWT later fills). It is canonicalized by the anchor’s key type (an uppercased/braced uuid still matches) and populates spock_actor() (§7.1) and = me (§7.2) for that request; an absent or unparseable header is anonymous (NULL), never an error. Impersonation is this header against a known identity — in v0, a seed persona row. The header is read on /graphql/v1 and /rest/v1/rpc/{fn}; the GraphQL actor is injected per request (never a process-global, which would bleed across callers). It is deliberately forgeable — v0 secures nothing.

Method & path	Meaning	Success
`GET /~contract`	the compiled contract (§6), verbatim	200
`GET /~health`	liveness	200 `{"ok":true}`
`GET /rest/v1/{table}`	list rows, ordered by key ascending	200 `{"rows":[...]}`
`GET /rest/v1/{table}/{id}`	one row by key (single-key tables only)	200 row
`POST /rest/v1/rpc/{fn}`	call a declared fn (§7.4) — REST’s deliberate surface, any polarity	200 row, `null`, or `{"rows":[...]}` per arity
`GET /rest/v1/rpc/{fn}`	call a read fn (§7.4), args in the query string	200 as above; 405 for a `mut` fn
`GET \| POST /graphql/v1`	GraphQL reads and writes (§8.2)	200

GET /rest/v1/{table} accepts ?limit=N; the default is 50 and the ceiling is 200 — a protocol default, not per-table syntax (v1-FEEDBACK L6). Row order is key ascending; with auto UUIDv7 keys this approximates insertion order.

POST /rest/v1/rpc/{fn} takes the arguments as a JSON object (an absent or empty body is {} — zero-parameter fns are curl-friendly); a non-object body is bad_request, an unknown fn is 404. The rpc segment is protocol-owned: a table named rpc fails startup.

GET /rest/v1/rpc/{fn} is the safe-method form for read fns (the PostgREST stable-function symmetry, RFD 0012): arguments arrive in the query string and parse by the declared parameter type; a value that does not parse passes through as text so the call names the canonical type_mismatch; unknown keys are the canonical unknown_field. A mut fn refuses GET with 405 (code bad_request) — a safe method must not write.

Reads are the open surface in its v0 degenerate form: every table auto-derives its identity view, all public. Writes are open too — v0 is the ungoverned prototype tier by decision: policy/RLS arrives in a later version and flips the default (RFD 0008; exposure model in RFD 0004). REST tables are read-only in v0 — table writes are GraphQL-first (§8.2); POST /rest/v1/rpc/{fn} is REST’s one deliberate write path (§7.4).

8.1 Errors on the wire

{ "error": { "code": "user_username_taken", "kind": "unique",
             "table": "user", "fields": ["username"],
             "message": "user.username is already taken" } }

Status	Used for
400	malformed JSON body; by-key GET on a composite-key table
404	unknown table, unknown path, row not found
405	GET rpc on a `mut` fn (code `bad_request`, §8)
409	`key`, `unique`, `restricted`, `refused` (fn refusals, §7.4)
422	`required`, `ref_not_found`, `invalid` (value constraints, RFD 0013), unknown field, type mismatch

Validation errors that are not schema-derived (unknown field, type mismatch, malformed body) use the reserved codes unknown_field, type_mismatch, bad_request, not_found with the same envelope.

8.2 GraphQL

The GraphQL surface has its own specification — docs/spec/graphql.md: the Hasura-mirrored dialect, its naming laws, read and write shapes, error mechanics, conformance tiers, and deviation register. The v0 runtime implements Tier 1 (the single-row core) exactly as specified there. This section records only the v0 protocol binding:

mounted at /graphql/v1 (the mount carries its own version axis, independent of the language version); POST executes a standard request body ({"query", "variables", "operationName"}, content type application/json required); GET serves GraphiQL; introspection is enabled — the schema is the contract’s metadata, and each mutation’s description lists the derived-error codes it can produce;
list fields share §8’s page discipline: default 50, ceiling 200, negative rejected (graphql.md deviation D2);
write semantics are §7.2’s, verbatim — the mutations run through the same single write path as the seed; update’s _set carries the §5.1 carve-out (absent = keep, explicit null = clear);
every contract-derived error carries the §8.1 payload in errors[].extensions: {code, kind, table, fields} (status is dropped — GraphQL is HTTP 200).

8.3 Storage

When a contract uses the builtin storage_object table (RFD 0018), the runtime mounts a Supabase-shaped byte plane at /storage/v1, beside /rest and /graphql. Files are stored out of band: the metadata is a storage_object row; the bytes live in the runtime’s blob store (v0: a SQLite BLOB, behind a swappable backend). An object is pending at mint and committed once its bytes land.

Method + path	Behavior
`POST /storage/v1/object/upload/sign`	mint a `pending` object (`owner` = `X-Spock-Actor`, else null) and return `{ id, url }` — a signed `PUT` URL
`PUT /storage/v1/object/{id}?exp&sig`	store the request body as the object’s bytes and flip `pending → committed`, recording `size`, `checksum` (sha256), and `content_type` (from the request header); the byte write and the flip are one transaction
`POST /storage/v1/object/sign/{id}`	return `{ url }` — a signed `GET` URL for a committed object
`GET /storage/v1/object/{id}?exp&sig`	serve the bytes with their recorded content type

A signed URL is a native HMAC-SHA256 bearer token binding the method, the object id, and an expiry (exp, unix seconds) into sig; the signing secret is minted per run (a URL does not survive a restart, and neither does the object). The verify is constant-time and fail-safe: a missing, malformed, or expired signature is 401; a PUT to an object that is not pending is 409; a GET of a non-committed or absent object is 404; a body past the size cap is 413.

Attach is an ordinary write — set a storage_object reference field to the object id (§7.2 / §8.2). Abandoned objects (pending never uploaded, or committed never referenced) are reclaimed by an in-process sweep.

9. v0 restrictions (explicit)

Recorded so they read as decisions, not omissions: no view, role, policy, auth, or state machines (RFD 0008); fn bodies are the SQL escape only — the native statement grammar (v1.spock’s require/let/verbs) is future; fns return rows or scalars (t, t?, [t] — no void) and land on the root their polarity names (§7.4 — reads on Query, mut on Mutation); records are fn return shapes only (not parameters, not storage); fn parameters may not reference composite-key tables (E036); seed may not call fns; the actor seam (RFD 0014) is the read/write half of identity — spock_actor() in fn bodies and = me on the floor — but it does not govern the floor: reads and non-me writes stay open, and per-row read governance, roles, and JWT claims arrive with policy/auth; references may not target composite-key tables (E010); writes are ungoverned — v0 is the open prototype tier; policy/RLS lands in a later version and flips the default; REST tables are read-only — table writes are deferred pending the filter-language question (writes are GraphQL-first, §8.2), while POST /rest/v1/rpc/{fn} is the deliberate REST write surface (§7.4); the former /~dev surface is retired, superseded by mutations; no partial/conditional uniqueness (v1-FEEDBACK L1 — undecided, so unshipped); value constraints are per-column and cross-column via validator fns (RFD 0013), but curated named formats (email) and nominal reusable domain types are deferred (a validator fn is already the reusable unit; curated formats wait for a vocabulary-versioning story); no cross-file programs; no null distinct from absence (except the §5.1 update carve-out; fn arguments treat null as absence).