# Jacquard diagnostic codes

Every diagnostic the toolchain can emit, with an example that triggers it. Domain-qualified
identities are stable: a `(domain, code)` pair is never reused or renumbered. A test enforces that
every code emitted anywhere in `src/`, `bin/`, or the native runtime appears in this catalog.

## Diagnostic structure and rendering

A diagnostic is structured data, not a preformatted message. Every diagnostic has a domain,
severity, plain-language summary, technical cause, and exactly one primary next step. A source
span and stable code may be absent only where the historical boundary has neither; optional
contrast is reserved for one concrete, plausible confusion and records separate `mistaken` and
`intended` descriptions.

The default text renderer presents the author-facing fields in this order:

1. source span, when available, on the severity/code header;
2. plain-language summary;
3. `Cause:` with the technical reason;
4. one `Next step:`;
5. `Contrast:`, only when a specific mistaken/intended distinction applies.

Commands accept `--diagnostic-format=text|json-v1`; `text` remains the default. `json-v1` writes
one compact JSON object per diagnostic to stderr, preserving emission order and exit status. Its
schema name is `jacquard-diagnostic-v1`, with `domain`, nullable `code`, `severity`, nullable
`span`, `summary`, `cause`, and `next_step` fields. A span contains `file`, `start`, and `end`; each
position contains one-based `line` and `column` plus a zero-based byte `offset`. The `contrast`
object is omitted when it does not apply. Machine consumers should key stable identities by the
pair `(domain, code)`, not by code alone, and should tolerate `code: null` for deliberately
code-less runtime failures. Span ends are exclusive, and columns count UTF-8 bytes rather than
Unicode scalar values. Treat `cause` as opaque author-facing text: when one diagnostic explains
another, the child is projected into that text rather than exposed as a second nested JSON schema.
The JSON encoding is always valid UTF-8: well-formed input is preserved byte-for-byte, while each
malformed source, path, or host-message byte in a string field is replaced with U+FFFD.

## Process safety (E00xx)

| code | meaning | example |
|------|---------|---------|
| E0003 | last-resort host-stack guard for an unbounded internal path | input that reaches an unguarded recursive path before a structural depth diagnostic |

## Reader (E01xx)

| code | meaning | example |
|------|---------|---------|
| E0101 | unexpected character | `(lit @)` |
| E0102 | unterminated text literal | `(lit "abc` |
| E0103 | invalid escape sequence | `(lit "a\qb")` |
| E0104 | invalid hash literal | `(ref #beef term)` |
| E0105 | malformed number | `(lit 1.2.3)` |
| E0106 | unexpected end of input | `(lit 1` |
| E0107 | bad form head | `(42 x)` |
| E0108 | unexpected `)` | `)` at top level |
| E0109 | integer out of the native 63-bit range | `(lit 123456789012345678901234567890)` |
| E0110 | non-form element in a bare group | `(group 42)` |
| E0111 | invalid quoted symbol | `(var 'Foo)` |
| E0112 | invalid bare symbol | `(var a@b)` |
| E0113 | non-form at top level | `42` |
| E0114 | more than one form where one was expected | two forms passed to a one-form entry point |
| E0115 | bootstrap form nesting exceeds the structural limit | more than 10,000 nested `.jqd` forms |

## Kernel validator (E02xx)

| code | meaning | example |
|------|---------|---------|
| E0201 | not a kernel form (unknown head in this position) | `(banana 1)` |
| E0202 | wrong arity for a kernel form | `(lit)` |
| E0203 | wrong argument sort | `(lit x)` |
| E0204 | `unquote` outside `quote` | `(unquote (var f))` |
| E0205 | refutable `lam` parameter | `(lam ((plit 1)) ...)` |
| E0206 | refutable `let` binder | `(let nonrec (pcon true) ...)` |
| E0207 | `let rec` binder is not a variable | `(let rec (ptuple ...) ...)` |
| E0208 | `let rec` value is not a `lam` | `(let rec (pvar f) (lit 1) ...)` |
| E0209 | empty `match` | `(match (var x))` |
| E0210 | invalid ref kind | `(ref #... banana)` |
| E0211 | invalid rec flag | `(let sometimes ...)` |
| E0212 | `handle` without exactly one `ret` clause | two `ret` clauses |
| E0213 | invalid explicit operation mode | `(op fetch multi () (tref text))` (legacy `multi` is encoded by absence) |
| E0214 | kernel form nesting exceeds the structural limit | more than 10,000 nested expression, pattern, type, or quote-payload forms |

## Name resolution (E03xx)

| code | meaning | example |
|------|---------|---------|
| E0301 | unknown name (with near-miss suggestions) | `(var ad)` when `add` exists |
| E0302 | name kind mismatch; also a `with` field update whose callee is not a constructor | `(ann (lit 1) (tref add))` — a term used as a type; `add(s with cells: 1)` |
| E0303 | duplicate binding name in a defterm group or surface definition run | two bindings named `f` |
| E0304 | variable bound more than once in one binder group | `(lam ((pvar x) (pvar x)) ...)` |
| E0305 | labeled constructor pattern, or a `with` field update, selects an unknown field (reported at the label) | `Snapshot(missing: x)`; `Snapshot(s with missing: 1)` |
| E0306 | labeled constructor pattern, or a `with` field update, selects one field more than once (reported at the repeated label) | `Snapshot(error: x, error: y)`; `Snapshot(s with error: 1, error: 2)` |
| E0307 | constructor has no usable field-label schema for a labeled pattern or a `with` field update | `Pair(left: x)` when `Pair` has only positional fields |
| E0308 | constructor declaration has ambiguous duplicate labels at labeled-pattern use; surface declarations now refuse the duplicate itself (E1239), so this reaches only bootstrap declarations | `Pair(left: x)` when `left` is declared twice in `.jqd` |
| E0309 | callee has no usable explicit named-call ABI | `local(value: 1)` for a local function, or `plain(value: 1)` for an unlabeled top-level term |
| E0310 | named call selects an unknown label | `resize(image: img, size: 2)` when the declared label is `scale` |
| E0311 | named call repeats or overlaps one argument slot | `choose(left: 1, left: 2)`, or `choose(1, left: 2)` when `choose(left: x, right: y)` declares `left` first |
| E0312 | named call does not fill the exact arity | `choose(left: 1)` when both `left` and `right` are required |
| E0313 | declaration has an invalid explicit named-call ABI | `bad(label: (x, y)) = x` or repeated parameter labels |
| E0314 | constructor named-call schema is ambiguous or malformed | using labels on a constructor with duplicate labels or an unlabeled field after a labeled field |
| E0315 | a single source uses a constructor of an opaque type that it does not itself declare, by name or by explicit identity | `Heads` in a file run against a store where an earlier file declared `opaque type Coin = \| Heads \| Tails` |

### Resolution warnings (W03xx)

| code | meaning | example |
|------|---------|---------|
| W0301 | a bare variable is bound across several value kinds; precedence picked one | `(var abort)` when `abort` is both a term and an op — term > con > op |

## Canonicalization and hashing (E05xx)

| code | meaning | example |
|------|---------|---------|
| E0501 | unresolved name reached hashing | hashing skipped resolution |
| E0502 | unbound variable reached hashing | free `(var x)` hashed |
| E0503 | `groupref` outside its group or out of range | `(groupref 0)` at top level |
| E0504 | malformed unquote reached hashing | internal guard |
| E0505 | defterm group too symmetric to order canonically | 8+ identical members |

## Store (E06xx)

| code | meaning | example |
|------|---------|---------|
| E0601 | unknown hash | `jacquard store name s x 000...0` |
| E0602 | unknown name | renaming a name that is not bound |
| E0603 | corrupt store file | hand-edited `names.jqd` or object file |
| E0604 | unnameable target | naming a defterm group's whole hash |
| E0605 | invalid name | `jacquard store rename s x "Bad Name"` |
| E0606 | diff source or store does not exist | `jacquard diff a /nowhere` |
| E0607 | name bound to several kinds; needs --kind | renaming `abort` when it is both an effect and an op |
| E0608 | unknown --kind value | `jacquard store rename --kind bogus` |
| E0609 | invalid, mismatched, or unreadable diff operands | diffing a file against a store |
| E0610 | diff source contains a top-level expression | diffing a runnable script instead of declarations |
| E0611 | relational constituent store cannot be created or initialized | running `jacquard relate` with an unusable temporary directory |
| E0612 | a callable hash is already bound to a different `call-abi-v1` companion | publishing new external labels for an unchanged term or operation identity |
| E0613 | interface manifest is malformed, unreadable, or not `interface-v1`/`HASH_V0` | `jacquard interface diff notes.txt lib.jqi` |
| E0614 | a store does not provide the interface a manifest describes (unbound or rebound export, missing or different `call-abi-v1` companion, a declaration whose owner, mode, arity, or field labels differ from the recorded ones, exposed hidden member) | `jacquard interface verify lib.jqi store` after relabeling `resize` |

## Prelude and grants (E07xx)

| code | meaning | example |
|------|---------|---------|
| E0701 | prelude directory missing | `--prelude /nowhere` |
| E0702 | prelude name missing or wrong kind | truncated prelude |
| E0703 | effect not grantable | `--allow filesystem` |
| E0704 | store add expects declarations only | an expression in `jacquard store add` |
| E0705 | prelude differs from the store's recorded prelude | reopening a store with an edited prelude directory |

## Type and effect checker (E08xx, W08xx)

| code | meaning | example |
|------|---------|---------|
| E0801 | type mismatch (expected vs actual, elaborated) | `(app (var add) (lit 1) (lit "x"))` |
| E0802 | application of a non-function | `(app (lit 3) (lit 1))` |
| E0803 | arity mismatch (call, op clause, resumption) | one-parameter lambda applied to two |
| E0804 | annotation mismatch | `(ann (lit 1) (tref text))` |
| E0805 | reference kind mismatch or unknown hash | `(groupref 5)` outside a group |
| E0806 | constructor pattern arity | `(pcon some)` with no argument |
| E0807 | bare surface term reference where a compatible thunk is expected | `condition = True; bool.and-then(True, condition)` instead of wrapping `condition` in `fn () -> condition` |
| E0810 | type constructor arity (kind) error | `(tapp (tref option) a b)` |
| E0811 | unbound type or row variable | `(tvar zz)` in a declaration |
| E0812 | unbound variable in an effect op signature | `(op o () (tvar zz))` |
| E0813 | non-exhaustive match (with witness); for a `with` field update of one constructor of a sum type, the message names the total setter (`use <type>.with-<label> for a total update`) | bool match missing `false`; `Circle(s with name: "c")` when `Shape` also has `Square` |
| E0814 | ungranted effect in the program manifest | running a printing program without `--allow console` |
| E0815 | effectful top-level definition body | `(defterm ((binding x () (app (var print) ...))))` |
| E0816 | a once resumption may be consumed twice on one possible path | two sequential calls to the same once-clause `resume` binder |
| E0817 | a once resumption escapes its handler clause | returning, storing, capturing, or passing `resume` to a non-`Resume` parameter |
| E0818 | polymorphic reuse of a non-value local binding (value restriction) | bind an application result, then call it at two unrelated types |
| E0819 | opaque Secret used by generic inspection or serialization | passing a `Secret` to `debug.inspect` or a Text encoder instead of explicitly calling `secret.expose` |
| E0830 | an annotation or published scheme names an instance effect whose label no capability determines, or a top-level expression leaves an instance entry | a thunk-only function over an instance |
| E0831 | a scoped instance combinator outside its checker form | a wrapper, alias, non-literal callback, wrong arity or annotated head |
| E0832 | an instance escapes its scope | returning, storing or sending a capability or a thunk over it |
| E0833 | an instance entry reaches the row of a fresh-continuation callback | spawning a thunk that uses a capability |
| E0834 | a user handler clause for an instance operation | `handle ... with get-at(...)` |
| E0835 | constructing, destructuring or pattern-matching a capability | forging a capability value |
| E0836 | a capability type in a nominal declaration or user operation signature | `type Box = Box(StateRef Int)` |
| W0801 | redundant match clause | a clause after `(pwild)` |

E0817 has one bounded transformer exception: a direct clause lambda may capture
`resume` when its `handle` expression is immediately applied once to syntactic
value arguments. Inside that lambda, a call of `resume` must be the direct
function child of one nested application with syntactic-value arguments so its
answer is immediately eliminated; binding or duplicating an answer that could carry a later Once token
emits E0817. Binding, returning, storing, passing, or aliasing the handler result
also emits E0817; consuming the captured resumption twice emits E0816.

## Runtime and probabilistic inference (E09xx)

| domain | code | meaning | example |
|--------|------|---------|---------|
| inference | E0901 | empty posterior (impossible observations) | `observe (bernoulli 0.0) true` |
| inference | E0902 | runtime failure inside inference | a model dividing by zero |
| warp | E0902 | runtime failure during exhaustive property execution | an exhaustive property body dividing by zero |
| inference | E0903 | model file has no expression | a decls-only file passed to `jacquard infer` |
| runtime | E0904 | observe at the sampling root | `observe` under `jacquard run --allow dist` (D7 default: defect) |
| warp | E0905 | exhaustive verification budget exceeded | a property over `uniform-int(1, 1000000)` under `jacquard test --exhaustive` |
| runtime | E0906 | a once continuation was resumed more than once | applying the same once resumption twice |
| concurrency | E0907 | a Task or ChannelHandle carrier is private, malformed, foreign to the run, escaped, stale, or outside its exact structured scope | returning/storing a Task or ChannelHandle beyond `async.scope`, constructing its private carrier by hash, reusing it after its creating scope closes or in another run, or using a parent/descendant/foreign handle |
| concurrency | E0908 | a deterministic scheduler, schedule trace, trace I/O, or same-scope policy operation is illegal for its lifecycle, decision order, registration, continuation ownership, configured positive/transport bound, or strict-replay contract | checking out a suspended task, exceeding a task/decision/input bound, observing or scheduling a terminal child twice, reading/writing an unavailable trace path, parsing an unversioned/malformed trace, or replaying a missing, extra, reordered, impossible, queue-drifted, or operation-drifted event |
| inference | E0910 | exact risk enumeration has no positive terminal-branch budget | calling the trusted exact runner with `max-branches = 0` |
| inference | E0911 | an exact risk model supplied an invalid finite distribution or non-comparable observation value | a categorical support with a negative, NaN, or infinite weight, or an `observe` over closures or opaque values |
| inference | E0912 | exact risk enumeration exhausted its terminal-branch budget | a four-leaf model under `max-branches = 3` |
| inference | E0913 | an exact risk model returned something other than a released `Risk` | returning `Option Risk` or a forged constructor identity |
| inference | E0914 | an exact risk model performed an effect other than released `Dist.sample` or `Dist.observe` | throwing from a model declared for the exact boundary |
| inference | E0915 | exact risk enumeration could not initialize or the model failed at runtime | division by zero in a reached model branch |
| inference | E0916 | exact risk path or accumulation arithmetic became non-finite | multiplying finite path factors into an overflowing weight |
| inference | E0917 | inference failed numerically: every possible path or run underflowed to zero weight, or a weight or the total is non-finite or negative | two `observe` factors of `1e-200` under `jacquard infer enumerate` |
| inference | E0918 | exact enumeration exceeded its `--max-branches` terminal-path budget | a two-branch coin model under `jacquard infer enumerate --max-branches 1` |
| runtime | E0919 | the invocation's computation fuel ran out; the run is incomplete, neither a pass nor a failure (docs/computation-fuel.md) | `spin(n) = spin(add(n, 1))` under `jacquard run --fuel 2000` |
| runtime | E0920 | a scoped instance operation found no frame of its scope on the current continuation (a stale capability, reachable only through unchecked `eval`) | a capability smuggled out of `state.scoped` through `eval-code` and used later |

## Warp (E10xx)

| code | meaning | example |
|------|---------|---------|
| E1001 | expression at top level of a test file | `jacquard test file.jqd` where the file ends with `(app (var main))` |
| E1002 | eval under --dry-run | a program whose row includes `eval` run with `--dry-run` |
| E1003 | completed relational runs differ under their selected observation projection | schedule variation finds a race, Secret variation finds redacted payload-dependent Console output, or grant variation finds different live/dry result values |
| E1004 | malformed, unsupported, or noncanonical run-transcript-v1 bytes | a transcript with a noncontiguous observation index or truncated payload |
| E1005 | an observation policy is malformed, noncanonical, or refused for the observed program | unsorted operations, an operation identity the program does not have, or a pinned interface-v1 identity that differs |
| E1006 | observation-transcript-v1 bytes are malformed, or were recorded under a different observation policy | decoding a transcript under another policy, or comparing transcripts of two policies |
| E1007 | relational runs cannot be called equal under the selected observation policy | `relate --policy` where runs agree only on truncated prefixes, opaque kinds, uncoded failures, unfinished projections, or both stop incomplete |

## Native compilation (E11xx)

| code | meaning | example |
|------|---------|---------|
| E1101 | program construct is outside the native v1 compilation subset | compiling a call with more than eight arguments |
| E1102 | program requires the interpreter tier | compiling a program that uses `eval` |
| E1103 | native toolchain, grant, or build configuration cannot produce the executable | building with an unsupported `net` grant or unavailable compiler |

## Surface syntax (E12xx)

| code | meaning | example |
|------|---------|---------|
| E1200 | retired surface-parser scaffold diagnostic; reserved and no longer emitted | an older build rejecting every nonempty `.jac` file |
| E1201 | retired surface-printer scaffold diagnostic; reserved and no longer emitted | an older scaffold calling the pre-SS.1 printer placeholder |
| E1202 | recovered surface tree still contains holes | checking malformed `.jac` after parser recovery |
| E1203 | kernel subtree has no self-contained surface fragment | rendering an ambiguous raw `group` in a semantic diff |
| E1204 | `jac fmt` produced text that its own surface parser rejects, that drops or alters a comment, or that would format differently again; the output is discarded and the file is not changed | a formatter bug, reported instead of printing unparseable, comment-losing or unstable code |
| E1210 | unexpected surface character | `@` outside a string |
| E1211 | malformed surface identifier | `bad--name` without a kind escape |
| E1212 | malformed or overflowing numeric literal | `1..2` |
| E1213 | unterminated surface string | `"missing close` |
| E1214 | invalid surface string escape | `"\\q"` |
| E1215 | malformed kind-tagged escaped name | `` `wat:name` `` |
| E1216 | malformed kind-tagged hash reference | `#abc:term` |
| E1217 | malformed internal group reference | `#group[x]` |
| E1218 | invalid raw UTF-8 scalar in a surface string | a raw `0xff` byte between quotes |
| E1219 | malformed marked text interpolation | an unclosed `{expr}` or nested `$"..."` |
| E1220 | unexpected token in the recovering surface parser, including a malformed `with` field update | stray `|` at top level; `Snapshot(s, t with cells: 1)` |
| E1221 | unclosed braced construct during surface recovery, with opening and failure spans | a `quote`, `match`, `handle`, or block truncated before `}` or closed with `]`/`)` |
| E1222 | reserved pre-SS.9 binding-pattern parser gate; refutable binders now use E0205/E0206 during lowering | `fn (Some) -> 1` |
| E1223 | missing block-item separator | `{ 1 2 }` instead of `{ 1; 2 }` |
| E1224 | a term signature is not followed by the same definition | `x : T; x = value` |
| E1225 | malformed type/effect declaration structure; the positional-parentheses case shows both accepted spellings, and the declarations around it keep their names (see the check command's recovery report) | `type Option a = Some(a)` |
| E1226 | malformed handler boundary, clause, or raw inversion escape | `handle match x { ... } { ... }` without the D35 body wrapper |
| E1227 | surface syntax nesting exceeds the structural limit | more than 10,000 nested calls, pipes, parentheses, patterns, or types |
| E1230 | surface node is outside the SS.7 local-lowering slice | lowering a list before SS.12 |
| E1231 | empty expression block | `{}` |
| E1232 | local `let` is the final block item | `{ let x = 1 }` |
| E1233 | malformed local recursive/function binding | `let rec (f, g)(x) = x` |
| E1234 | generated lowering node lacks a real source span | lowering a hand-built spanless block AST |
| E1235 | a signature or definition was lowered without its required file context | calling `lower_top` on a signature |
| E1236 | missing, duplicated, or conflicting surface operation mode; an omitted mode includes migration guidance | `effect E where { op : () -> T }` |
| E1237 | labeled constructor pattern appears inside quoted surface syntax | `quote { match packet { \| Packet(right: value) -> value } }` |
| E1238 | named call or `with` field update appears anywhere inside quoted surface syntax, including a live unquote | `quote { unquote(choose(left: 1)) }` |
| E1239 | a constructor declares the same field label twice | `type Pair = \| Pair(left: Int, left: Text)` |
| E1240 | a field label has different types in different constructors of one type | `type Key = \| Numbered(id: Int) \| Named(id: Text)` |
| E1241 | a generated field accessor `<type>.<label>` or setter `<type>.with-<label>` collides with a term or effect operation the same file declares, or a setter with one of the type's own accessors | `type Pair = \| Pair(left: Int)` beside `pair.left(p) = 0` |
| E1242 | `try` is used inside an expression instead of as a block item | `f(try x)` |
| E1243 | a block ends in `try` | `{ try parse(x) }` |
| E1244 | `try` is used on a `let rec` local function binding | `let rec h(y) = try f(y)` |

### Surface warnings (W12xx)

| code | meaning | example |
|------|---------|---------|
| W1201 | lowercase binding pattern binds a new name instead of matching an in-scope constructor differing only in case; the warning names the constructor and both remedies | `match Up { | up -> ... }` |
| W1202 | positional constructor pattern has more than four fields | `Snapshot(_, _, _, _, _)` |
| W1203 | match scrutinee contains a nested control construct or more than twelve calls and constructions (layout is not counted) | manually bind the expression with `let`, then match on its name |
| W1204 | shortest legal type/effect declaration header exceeds the canonical formatter width | shorten the declaration name or type-variable list |
| W1205 | shortest legal `forall` prefix exceeds the canonical formatter width | split the declaration or reduce its quantified variables |
| W1206 | positional term/operation call passes a direct `Bool` constructor literal in a slot with an explicit companion label | use that label, or a purpose-specific sum such as `Mode = \| Live \| DryRun` |
| W1207 | positional term/operation call fills a definite adjacent run of same-typed parameters with an applicable companion label | call the ambiguous suffix by label so swaps remain visible in review |

## Explicit bootstrap export (E13xx)

| code | meaning | example |
|------|---------|---------|
| E1301 | export destination collision | `jac export a.jac -o existing.jqd` |
| E1302 | export input is missing, unreadable, stdin, or non-regular/non-seekable | `printf '1' \| jac export - -o out.jqd` |
| E1303 | same-directory atomic publication failed | exporting into a missing or unwritable directory |

The recovering `.jac` lexer emits an in-order invalid-token marker and continues;
the strict lexer remains fail-fast. Malformed strings resynchronize at a closing
quote or newline, so an unterminated line does not discard valid later items. The
parser synchronizes at construct boundaries including `}`, wrong `]`/`)` closers, `|`, `;`, and
newline so a malformed expression does
not hide later syntax errors. Unclosed `quote`, `match`, `if`, `handle`, and block
diagnostics use the failure token as the primary span and name the opening span in
the hint. Each damage site leaves an explicit surface hole or synthetic delimiter
marker with a stable `surface-hole` ID and `surface-form = recovery-hole` or
`recovery-delimiter` provenance. `Surface_parse.strict` rejects both error diagnostics
and any remaining hole before lowering. Semantic boundaries also recursively reject
marked trees before strict checking, execution, storage, or canonical hashing,
including markers nested in patterns, types, handlers, and quote payloads.
`Surface_check.analyze` is the separate editor/recovery API: it checks marked hole
sentinels as fresh types with no effects in a fresh isolated checker context and
returns only diagnostics and inferred signatures. Successfully checked term islands
are available to later islands through analysis-local names and schemes without
installing declarations in the store. Type and effect declarations are checked in
isolation; references to them from later islands require strict installation first.

## Audit chain (E13xx)

| code | meaning | example |
|------|---------|---------|
| E1301 | malformed or noncanonical Audit chain carrier | a blank line, alternate whitespace, or missing final LF |
| E1302 | unsupported chain version or malformed released AuditEntry | `audit-chain-v3` or a non-v2 entry shape |
| E1303 | broken predecessor linkage | reordered, removed, or duplicated records |
| E1304 | stored digest does not match the predecessor and entry bytes | altering one entry byte without recomputing the record digest |
| E1305 | reconstructed chain head differs from the independently published head | removing the final record or appending from a stale head |
| E1306 | Audit chain I/O failure, size refusal, or concurrent file change | an unreadable/over-limit entry, a log truncated while being read, or its pathname replaced during append |
| E1307 | malformed CLI Audit head | `--head beef` instead of 64 lowercase hexadecimal digits |
| E1308 | noncontiguous AuditEntry sequence | a duplicate, skipped, decreasing, or negative sequence position |

`jacquard governance verify-log LOG --head HASH` verifies offline and fails
closed. It accepts only LF-terminated canonical `audit-chain-v2` records, checks
every predecessor, digest, and exact sequence `0, 1, 2, ...` in order, then compares the reconstruction with the
separately supplied published head. Malformed input returns diagnostics; it does
not raise an exception.

## Governance verifier (E14xx)

| code | meaning | example |
|------|---------|---------|
| E1400 | verifier environment or analysis version is unsupported | rebinding `eval` to a different effect or supplying `governance-verifier-v1` input |
| E1401 | facade effect or operation mode is invalid | a non-`once` facade operation |
| E1402 | facade operation coverage is incomplete or duplicated | a frozen operation with no dry clause |
| E1403 | gate identity, branch coverage, or post-gate ordering is invalid | consuming `Resume` before recording live completion |
| E1404 | audit sequence ownership or token provenance is invalid | two `with-sequence` owners around one published stream |
| E1405 | a normalizer or summarizer is not a closed pure arrow with its exact result shape | an effectful callback hidden inside a normalizer parameter |
| E1406 | a carried identity does not match its canonical subject | a `Call.call-id` copied from different arguments |
| E1407 | action expansion disagrees with the frozen authority envelope | a forwarded operation that introduces undeclared `Net` authority |
| E1408 | gate-owned control authority appears inside the action projection | listing `State` or `Audit` as raw action authority |
| E1409 | governance review data contains a `Secret` or uses generic inspection | embedding a secret in a BoundPolicy subject instead of a `SecretRef` |
| E1410 | an `Ask` proposal does not bind every exact review hash | omitting the assessment identity |
| E1411 | forwarded-call lineage is inconsistent or not anchored to the carried Call | unrelated previous/current IDs that agree only with each other |
| E1412 | governed code can reach `Eval` | handling `Eval` locally and then claiming it is absent |
| E1413 | canonical Workspace source contract is missing, ambiguous, open, carries unreported residual authority, or is structurally unsupported | an inert `workspace.live` reference or a live root whose closed outward row also contains `Console` |

`Governance_verify.verify` consumes a versioned analysis IR produced by trusted
tooling from resolved, typechecked artifacts. That IR is verifier evidence, not
a user-authored proof or an authority grant. The verifier resolves the real
stored terms, recomputes HASH_V0 identities, expands forwarded action envelopes,
and returns all detected violations with source spans. Resource scopes remain
configured evidence rather than row-type proofs. `Eval` is an absolute
prohibition for governed code, including code that attempts to handle it
locally.

GM.8 provides the library analysis boundary. GM.16 additionally exposes
`jac governance check FILE` for the exact `workspace-v0` source contract.
E1400--E1412 retain their existing meanings; E1413 is the command's additive
fail-closed source-shape diagnostic. A successful source report does not replace
`jac governance verify-run BUNDLE` for dynamic artifact identities.

## Governance run bundle (E15xx)

| code | meaning | example |
|------|---------|---------|
| E1500 | malformed, unsupported, noncanonical, unreadable, or concurrently changed run bundle | a bundle without its final LF or fixed artifact sections |
| E1501 | an artifact is malformed or its carried identity disagrees with its unchanged canonical v0 subject | a Call wrapper carrying the hash of different arguments |
| E1502 | one artifact identity occurs more than once | two Call wrappers carrying the same Call ID |
| E1503 | an Audit entry references an artifact absent from the bundle | `Consented` names a Proposal that was not supplied |
| E1504 | Audit ordering or entry-to-artifact linkage is missing, inconsistent, or ambiguous | consent has no unique earlier matching `Ask` evaluation |
| E1505 | a Proposal's Call, policy, assessment, or authority disagrees with its linked artifacts | a Proposal repeats a different authority envelope |
| E1506 | transformed Call lineage is missing, self-referential, or cyclic | `parent-call-id` names an absent Call |
| E1507 | a bundled artifact is not used by the Audit chain | an unrelated valid Proposal is appended to the bundle |

`jacquard governance verify-run BUNDLE` is additive to `verify-log`. The bundle
contains unchanged `audit-chain-v2` record forms plus full versioned artifacts.
The verifier resolves qualified operation names and hashes through the selected
prelude/store, reconstructs the published head, recomputes the existing v0
Call, BoundPolicy, Assessment, and Proposal identities, checks proposal and
decision links, and verifies explicit parent-Call lineage. It does not infer
that an external action ran, succeeded, or rolled back from an absent
`Completed` entry. Receipt and idempotency reconciliation require a later typed
action journal and are intentionally outside this command.

## Governance action reconciliation (E151x)

| code | meaning | example |
|------|---------|---------|
| E1510 | malformed, unsupported, noncanonical, unreadable, or concurrently changed reconciliation bundle | a nonregular input or missing final LF |
| E1511 | action-journal predecessor, digest, sequence, or published head mismatch | reordering a valid journal record |
| E1512 | Attempted or Receipt semantic identity mismatch | changing the carried attempt ID without changing its subject |
| E1513 | duplicate Attempted identity or second Receipt for one attempt | copying an existing journal entry |
| E1514 | Receipt does not follow an existing Attempted entry | placing a receipt first |
| E1515 | policy/verdict, attempt authorization, Call occurrence, completion, branch, or outcome linkage contradicts the verified run | a Dry Allow, live completion after Block, repeated Call evaluation, or changed receipt outcome |
| E1516 | evidence is structurally valid but operator reconciliation remains | a durable receipt has no matching `Completed` record |

`jacquard governance reconcile BUNDLE` verifies a separate HASH_V0-chained
action journal around one unchanged run bundle. An attempt names the exact
allowing or approving Audit-record digest. A receipt names that attempt, the
exact outcome summary, and an external-receipt digest. Only exact
Call/branch/outcome agreement counts as reconciled. Every live completion is
checked, including when no action-journal entry names it. Unknown attempts,
missing receipts, and missing completions are nonzero reports, never rollback
or safe-retry claims.

## Governance approval queue (E152x)

| code | meaning | example |
|------|---------|---------|
| E1520 | malformed, noncanonical, or unrecognized physical journal framing | an arbitrary non-LF suffix rather than the exact record-envelope prefix |
| E1521 | unsupported queue record, commit, or event version | replacing a v1 record envelope with a different carrier head |
| E1522 | record predecessor, carried identity, or commit identity mismatch | editing a committed Decision without updating its record identity |
| E1523 | malformed GovernanceProposal or noncanonical allowed-approver metadata | submitting duplicate or unsorted principals |
| E1524 | malformed or stale Decision, or invalid authenticated actor binding | an Approved Decision whose approver differs from the host actor |
| E1525 | requested transition conflicts with durable queue state | deciding one proposal differently after a Decision is committed |
| E1526 | unsafe path, bounded-read, lock-adjacent, write, sync, or visibility failure | replacing the locked pathname while a transaction is appended |
| E1527 | queue-backed bridge schema or single-rendezvous workflow mismatch | rebinding a frozen approval identity or performing a second sequential approval Ask |

`Governance_approval_queue` is an explicit OCaml host adapter, not a new
Jacquard effect or ambient file API. It verifies canonical two-line
record/commit transactions under a process-local guard and one nonblocking
whole-file lock. A recognized uncommitted suffix may be reported or durably
truncated to the last commit boundary; committed corruption always fails
closed. The module consumes a proposal ID atomically: under the lock it resolves
the immutable Decision, commits the exact Decision ID, and only then returns
the exact Decision and ID.

## Governance explanation (E153x)

| code | meaning | example |
|------|---------|---------|
| E1530 | the requested Proposal ID is not exact canonical HASH_V0 text | uppercase hex or fewer than 64 digits |
| E1531 | one linked Proposal and its exact explanation records cannot be selected | the requested ID is absent or its matching Evaluated record is ambiguous |
| E1532 | the recorded verdict disagrees with the recomputed stable live-policy rule | an `ask` record is paired with `live.at-or-below-auto` |
| E1533 | Workspace action evidence cannot support the explanation | an attempt commits a noncanonical leaf driver, or a completion has no unique attempt |
| E1534 | the requested why-effect authority is unsupported | `fs` rather than exact `Fs`, or a user effect hash |
| E1535 | a reachable callable cannot be attributed without guessing | a variable, returned function, open external callable, or callable transport |
| E1536 | a reachable local handler invalidates the claimed membrane path | handling Workspace before its verified live boundary |
| E1537 | a reachable source group reference or live splice is malformed | an out-of-range `GroupRef` or invalid live unquote expression |
| E1538 | the bounded source-attribution traversal is exhausted | a reachable graph larger than the fixed analysis budget |
| E1539 | governance review fact families, profiles, queries, or exact cross-family links are incompatible | comparing `Fs` static facts with `Net` facts, or pairing an attempted driver with another operation's static driver |
| E1540 | two governance review facts conflict for one exact identity | duplicate operation facts carry different driver identities or labels |
| E1541 | typed governance review facts violate an internal comparison invariant | a reached operation is absent from the complete facade operation set |
| E1542 | a governance decision-chain presentation cannot be derived safely from the typed explanation | completion evidence disagrees with the verified action state, or a non-Ask verdict carries consent evidence |
| E1543 | a posterior-risk model cannot be resolved by exact hash or does not have the closed `(GovernanceCall) ->{Dist} Risk` signature | selecting a pure function or a model with an additional effect |
| E1544 | exact posterior configuration is invalid or bounded exhaustive inference fails | exhausting `max-branches` before the next terminal path |
| E1545 | exact posterior evidence, weights, normalization, support, or branch accounting is invalid | four zero weights or underflow that erases theoretically positive support |
| E1546 | exact projection cannot validate its Call, baseline, carried identities, rule, or conservative result | substituting a different Call, handler descriptor, source evidence, or nested posterior wrapper |
| E1547 | non-authorizing approximate evidence cannot be constructed safely | a nonpositive sample count, model failure, or non-`Risk` sampled result |
| E1548 | posterior-aware offline verification cannot select one supported committed decision | no matching `Evaluated` entry, ambiguous linkage, malformed replay artifacts, or a dry policy whose simulator availability is not bound by the bundle |
| E1549 | exact posterior replay disagrees with the committed assessment or unchanged live-policy verdict | changing the model evidence or exact budget, substituting the effective assessment, or committing a different verdict |

`jac governance explain PROPOSAL_ID --bundle RECONCILIATION_BUNDLE` accepts
exactly 64 lowercase hexadecimal digits and fully applies reconciliation-bundle
verification before selecting or writing a success report. It recognizes only
the frozen Workspace v0 operations and binds an attempted action to the exact
canonical leaf driver for that operation. Denied, escalated, and unattempted
approved decisions render `not-attempted`; they never acquire a driver by
guessing. Structurally valid reconciliation gaps remain distinct from evidence
that contradicts the selected explanation.

`jac why-effect EFFECT --source FILE` accepts only the exact GM.16
`workspace-v0` source profile. `EFFECT` is exactly `Fs`, `Net`, `Secret`, or
the released hash of one of those effects; mutable effect-name lookup is never
used. After full source verification, the analysis follows exact source-owned
term identities, valid source-group references, direct lambdas, and live
unquote splices. It evaluates application arguments before attributing the
callee and refuses the entire report when higher-order flow, a relevant local
handler, malformed staging data, or the traversal bound prevents a sound
answer. Empty chains mean only that no matching attributable Workspace
application was found; they are not proof of runtime absence.
Every reported chain includes an application site: the exact source-member
identity plus a zero-based preorder ordinal over reachable resolved-kernel
applications in that member. Direct invocations and live splices count; inert
quotes and lambda values do not. E1537 is a defensive fallback for malformed
retained data after verification, not a claim that normal public verified input
can construct such data.

`Governance_review_diff` is a pure OCaml handoff for later package tooling; it
adds no command and accepts no untrusted JSON. It compares typed GM.17A and
GM.17B projections without treating their shared schema label as family
equivalence. Static projection preserves the GM.17B source root and attribution
chains; exact hashes and the application ordinal establish chain identity, not
display names or collection order. Dynamic Decision comparison ignores only
the endpoint proposal hash in the first exact released proposal carrier and
never rewrites Approved evidence or denial/escalation reasons. E1539 rejects
incompatible endpoints or exact operation/driver linkage, E1540 rejects
conflicting facts for one identity across all retained chain fields, and E1541
guards producer invariants. A missing query-scoped operation detail is instead the
stable `operation-not-reached` availability fact and makes the report partial.
The report grants no authority, proves no execution or runtime absence, and
assigns no safety verdict.

`posterior.run-exact-v1` and `judge.posterior-exact-v1` are the only
decision-bearing GM.21 inference path. They resolve the model by exact stored
term hash, require its closed `Dist`-only signature, enforce a positive
terminal-branch budget, preserve theoretically positive support, and return no
partial posterior on failure. `posterior.project-exact-v1` revalidates the
carried identities and can only join the selected risk upward with an
independently validated baseline assessment. The distinct
`non-authorizing-approximate-risk-evidence-v1` carrier produced by seeded
likelihood weighting has no assessment projector or Judge adapter.

`Posterior_risk_verify.verify_form` is a separate offline verifier layered on
the unchanged Governance v0 run-bundle verifier. It first requires the whole
v0 bundle to verify, reruns exact posterior inference from typed artifacts,
requires exactly one matching `Evaluated` entry, compares the replayed
effective assessment byte for byte, and recomputes its unchanged live-policy
verdict. It rejects dry policies because a run bundle does not bind their
simulator-availability input. The existing v0 verifier does not make these
posterior-replay claims.

`Governance_decision_chain` is an additive, presentation-only OCaml adapter for
the local Workspace v0 playground. It accepts only an existing typed
`Governance_explain.report`, rechecks its cross-artifact relationships, and
emits six ordered stages without evaluating policy, deriving authority, or
accepting client JSON. E1542 fails closed when the typed report cannot support
that exact presentation. The browser receives no report on this failure and
cannot replace or reinterpret the diagnostic.

## Host protocol v0 (E16xx)

HB.1 freezes these `process` diagnostics for the experimental
`jacquard-host-v0` contract. No executable carrier ships yet. Before invocation
a trustworthy carrier may return them in `fatal`; after invocation they appear
in the single error `outcome`. Carrier loss can prevent Core from emitting a
diagnostic, in which case E1611 belongs to host/operator evidence rather than a
fabricated Core result.

| Code | Meaning | Example |
|---|---|---|
| E1600 | unsupported host protocol version or carrier | selecting `jacquard-host-v1` from a v0-only hello |
| E1601 | malformed frame or envelope | duplicate JSON keys, invalid UTF-8, or an unknown field |
| E1602 | host protocol limit exceeded | a 1,048,577-byte frame or a nonpositive selected limit |
| E1603 | target or pinned interface is invalid | an unresolved callable hash or mismatched parameter type |
| E1604 | type or value is unsupported at the v0 boundary, including an opaque type, a type whose fields reach one, or a value built from an opaque type's constructor | trying to transport a Secret, Task, closure, open type, or opaque type |
| E1605 | capability envelope is invalid | an extra effect, duplicate operation, or `multi` registry entry |
| E1606 | root operation is not configured | evaluation reaches an operation absent from the closed host registry |
| E1607 | host refused authority before action | the adapter rejects a requested resource without starting I/O |
| E1608 | response/order/finish-once invariant is invalid | the wrong request ID or a message after outcome |
| E1609 | host reported a non-ambiguous timeout | a deadline expires before an outside action starts |
| E1610 | host reported non-ambiguous shutdown | shutdown cancels the current response slot before action |
| E1611 | carrier was lost | EOF inside a frame or process death without a terminal message |
| E1612 | outside completion is unknown | a timed-out write may have committed and must not be retried |
| E1613 | outside action definitely failed | the adapter reports a completed failure with no successful value |
| E1614 | host cancelled non-ambiguously | explicit cancellation before an outside action starts |

See `spec/host-protocol-v0.md` and its checked vector corpus for exact schemas,
ordering, limits, terminal mapping, and non-retry behavior.

## Local projects (E17xx)

Diagnostics of the local project format (`project.jqd`,
`docs/designs/project-structure.md`). The manifest codes below ship with the
manifest reader and `jacquard project check|fmt`; the composition codes ship
with `jacquard project check|run|test`, and the dependency, visibility and pin
codes with `jacquard project pin|interface`, and the bundle codes with
`jacquard project bundle` and `--bundle`.

| code | meaning | example |
|---|---|---|
| E1700 | the manifest is malformed: not one form, wrong head, wrong field shape, or an invalid value | `(project-v2 ...)`, `(units "notes.txt")` |
| E1701 | an unknown field or sub-field (v1 fails closed) | `(license "MIT")` outside `(metadata ...)` |
| E1702 | a field, unit, export selector, dependency alias, entry key, grant, or metadata key repeats | `(units "a.jac" "a.jac")` |
| E1703 | a manifest budget (64 KiB of bytes, 1 KiB per text, or a collection limit) or the 4 MiB unit budget is exceeded | a 300-unit `(units ...)` |
| E1704 | the running Core does not satisfy `(requires (core "MAJOR.MINOR"))` | `(requires (core "9.0"))` |
| E1705 | a name another project keeps private: not exported by a direct dependency, or bound by a project that is not a direct dependency (also inside `eval-code` payloads) | `liba.helper` when `liba` exports only `liba.shout` |
| E1706 | a library name does not carry the namespace: `NS.` for terms and operations, `NS-` for types and effects; constructors are exempt and generated accessors and setters follow their type | `helper` in a `(namespace shop)` library |
| E1707 | two projects in one graph, counting the namespaces bundles record for the contexts they carry, or two contexts in one bundle, have namespaces where one is a boundary-prefix of the other | namespaces `x` and `x-y` |
| E1708 | a project that others depend on declares no namespace | `(deps (dep (as y) (path "../y") ...))` where `y` has no `(namespace ...)` |
| E1709 | an explicit identity (`#hash:term`, a `.jqd` `ref`, or one inside an `eval-code` payload) that another project keeps private; or, in a project or bundle run, a posterior model reference to a term that neither the prelude nor any context in the run exports | the hash of a dependency's private helper |
| E1710 | a direct dependency's pin differs from its context identity; the report names the changed components (interface, companions, prelude, core, deps) and the interface diff when the previous interface was recorded | a private body edit reachable from an export |
| E1711 | a dependency is unpinned (only `project pin` accepts the root's unpinned edges), or `--dep` names no dependency | `(dep (as a) (path "../liba"))` |
| E1712 | a transitive pin, declared in a dependency's own manifest, does not match; reported with its alias chain | `app -> c -> a` after `liba` changes |
| E1713 | the dependency graph has a cycle | `x -> y -> x` |
| E1714 | one namespace appears at two context identities in one graph (bundle-carried contexts included) or in one bundle | two copies of `liba` with different bodies |
| E1715 | a library unit, or a test entry's unit, contains a top-level expression | `shop.total([])` in a library unit |
| E1716 | a name is defined in two different units (generated accessors count), including an entry unit redefining a library name | `shop.even` defined in two library units |
| E1717 | an export selector names nothing the project's own units define | `(exports (term libb.nothing))` |
| E1718 | the manifest declares no entry of that name, or it is the other kind | `jacquard project run suite` for a test entry |
| E1719 | a call-ABI companion conflicts with one already composed into the graph | two projects labelling one identical callable differently |
| E1720 | a bundle's prelude or Core differs from the running tool | a bundle built by another Core release |
| E1721 | `eval-code` or the `Eval` effect is reachable from a bundle root: a run step, a test root, or an exported callable of any context in the graph (a dependency's export the root never calls included), including through a returned closure (quoted data is not code; live splices are) | exporting `app.make() = fn () -> eval-code(...)` |
| E1722 | a unit resolves, after symlinks, outside the project directory | `(units "../outside/far.jac")` |
| E1723 | a unit is missing or not a regular file | a directory named `missing.jac` |
| E1724 | two units in one composition differ only by letter case | `"src/types.jac"` and `"src/Types.jac"` |
| E1725 | an output (a bundle, a native `project build -o`, or a `project test --cache-dir`) overlaps an input unit, the manifest, or a dependency directory; a bundle output that already exists | `project build demo -o lib.jac` |
| E1726 | a bundle object does not hash to its file name | an edited `objects/*.jqd` |
| E1727 | a recorded interface export is not owned by its recorded declaration | an edited `(owner #...)` |
| E1728 | an object or root refers to an identity that is neither in the bundle nor in the prelude | a deleted object |
| E1729 | an interface does not re-derive from the checked objects, a context record does not recompute, a carried context is not a dependency of the bundle's own context, or the manifest does not match the record's digest | an edited `interfaces/` or `contexts/` file |
| E1730 | declared grants differ from checked authority, under `--strict-grants` | `(grants fs)` on an entry that never uses `fs` |
| E1731 | a library or entry constructor has the name of a visible constructor of another type | `type ShopMaybe = \| Some(value: Int)` beside the prelude's `Option` |
| E1732 | the library refers to a name only an entry defines; the library is checked before, and without, any entry | a library term calling a helper defined in `demo.jac` |
| E1733 | a manifest or unit read while pinning changed before the pin was written; nothing is written | editing a dependency during `project pin` |
| E1734 | two unit entries in one composition resolve to the same file | `"src/types.jac"` and `"./src/types.jac"` |
| E1735 | no `project.jqd` was found, or it cannot be read; or a bundle cannot be read, including a `bundle-v1` bundle that carries dependency contexts or an opaque declaration | `jacquard project check` outside any project |
| E1736 | a manifest exports a constructor of an opaque type with `(con C)`, or a bundle records such an export; opaque constructors stay sealed to their project | `(exports (type prob-value) (con prob-value))` |
| E1737 | a root without a namespace, or an entry unit, declares a type or effect inside another graph project's namespace, including one a bundle records for a context it carries | `type LibaBox = ...` in an application that depends on `liba` |
| E1738 | a bundled term that constructs or matches a sealed constructor lies in the region of a context that does not own the opaque type, or in no region at all | a consumer context re-exporting its dependency's private constructing helper |
| E1739 | a bundle's recorded namespaces do not match what it carries: a carried dependency context records none, a namespace is recorded for a context it does not carry, a recorded namespace does not prefix its context's exports, what a context's exports reach (other than through types alone) lies outside its namespace, any part of a region (entries included) reaches a type or effect in another context's namespace through a live reference, the root's differs from `project.jqd`, or one context identity appears under two namespaces: recorded so by a bundle, or two source projects sharing one identity when they are bundled | a `bundle-v2.jqd` whose `(namespace #… liba)` was relabelled `libz` |
| W1700 | declared grants differ from checked authority (a warning unless `--strict-grants`) | a run entry printing without `(grants console)` |
| W1701 | a file under the project's `.jacquard/` (caches, builds, pin records) is tracked by git | `git add -f .jacquard` |
| W1702 | beside a checker error, the definition's signature is in another unit, so the report names both files | a signature in `sig.jac`, its definition in `def.jac` |
| W1703 | the root exports a transparent type without its constructors, or that type's generated setter; the constructors are hidden by name only | `(exports (type liba-box))` for `type LibaBox = LibaBox(n: Int)` |

## Appendix: the W5.3 audit (ten message rewrites)

Before/after wording improvements applied during the audit:

1. E0802 before: "not applicable" → after: "`int` is not a function" with the hint naming
   what can be applied.
2. E0801 before: bare "type mismatch" → after: expected/actual fully elaborated plus a hint
   that the expected side comes from context.
3. E0813 before: "match not exhaustive" → after: names the exact missing witness
   (`some(some(false))`) and hints the fix.
4. Unhandled-effect runtime error before: "unhandled op" → after: names both the effect and
   the operation, and the CLI exit code is distinct (3).
5. E0814 before: nothing (new) → names the effect, the call-chain endpoint, and the exact
   `--allow` flag to add.
6. E0605 before: crash (`Bug_unprintable` escaping, truncating names.jqd) → after: a clean
   diagnostic stating the name grammar.
7. E0109 before: "invalid int" → after: names the 63-bit native range and decision D2 in
   the hint.
8. E0304 before: silent acceptance across sibling binders → after: a dedicated diagnostic
   naming the variable.
9. div-by-zero before: "type error: division by zero" (miscategorized) → after: a dedicated
   `Arithmetic` runtime error category.
10. E0901 before: NaN posterior from 0/0 → after: "the posterior is empty: every branch is
    impossible under the observations".