Appendix B — Error and Trap Registry

Every code in this book’s labs, with the fixture that earned it. The checker’s error codes are falsifiable claims: each one exists because a violation exists. Bands: 10xx–70xx compiler front end, 32xx–37xx typecheck, 36xx MMIO, 50xx effects/contexts, 51xx stack bounds, | 52xx loader.

# Compile-time rejections verified in this book

# Runtime trap codes

Hosted exit status equals the trap code.

Environmental failure semantics. Traps 24/25/26 are environmental failure classes, not language-invariant violations: a program proven under the verification discipline can still die by task-queue overflow, deadlock, or region exhaustion, and the docs say so in exactly those words (Q14). The static-verification plan’s obligation schema treats them as defined runtime behavior, not proof obligations.

# Verification pipeline (chapter 14)

# Loader verdicts (chapter 13)

Suite: cargo test -p execution-tests --test dynamic_negative executes ten of these as attempted crimes (Lab 13.4).

# Verification artifact band (64xx)

Compile-time codes of the verification subsystem (devdocs/plans/static-verification.md, slices P2+; owner doc devdocs/plans/design-doc/verification-obligations.md). These are not runtime trap codes; they live in the claim table so artifacts and report tooling share one registry.

# Report-field glossary (slices P3–P8)

verify-report.json (tyu.verify-report/v2, written by tyu build beside the image; owner doc verification-obligations.md §6.5). Every field is enforced by a gate, not by convention:

• modules[] — per-module class accounting (subtype-range / contract-pre / contract-post / stack-budget / mmio-bounds: total, discharged, assumed, open).
• contexts.stack — the per-context budget verdicts: main (high, top, N_main derived from the runtime binary’s DS geometry, verdict) and isr (N_isr from the [verification] grant); guards = "retained" | "elided" (slice P7 — a truthful label of the object).
• open[] — obligations whose verdict is not closed, with the interval engine’s reason when one was recorded (drives E6410).
• provably_failing[] — interval-proven always out of range; the check is retained and the report names why (never a discharge).
• assumed[] — human decisions, recorded with their justification.
• retained[] — checks kept for a policy reason (e.g. dynamic exports under module-loading, slice P6/FR-21).
• assumptions_trusted[] — runtime facts (derived N_main) and descriptor facts (isr grant, aperture sizes) a discharge relied on — counted as trusted, never folded into “proven”.
• emitted_checks — the truth block (subtype_range, contract, mmio_bounds, data_stack_guards) MUST agree with the object code (FR-16; the corpus gate + slice tests enforce the bijection).
• stale_verdicts, verdict_sources — input verdicts that matched nothing, and the file-vs-in-tree discharge split.
• trust / methods / surfaces (per-module, PLAN-VERIFY-3 §Q6/§7.3) — the v2 trust-class split (proof / checked / assumed / open), the closed-method split, and the certificate surface split (source / ir).
• tcb[] — the shipped trust-computing-base boundary (§6.8): each trust-bearing component named with its status (assumed, reviewed+vectors, drift-locked, theorem, structural, structural+modeled, empirical).
• proof — the P6.2 section: the proof pipeline’s status (none / lean-skipped / lean), harvest (not-built / ok), gen_digest (verified / …), and the per-module statement accounting (rendered, proven, unproven).
• policy — the enforced verify policy (open-ok / no-open / no-open-no-assumptions / proven; off under --verify=off).

P6 extends the band: E6413 (stale interface / .def↔.obl hash disagreement). P7 (PLAN-VERIFY-3 P6/P7) adds: E6416 (proof-pipeline failure class), E6417 (closed-registry violation), E6418 (Gen digest), E6419 (axiom audit), E6420 (harvest missing statement), E6421 (statement-stale at consumption) — each allocated in §6.9 of the developer-proof-pipeline plan with its owning phase.

# Manifest / certification band (65xx)

The in-module verify_manifest record (P11.1/P11.2) and the certification package (P11.3). Loader codes are on-device admission (the loader never interprets proofs — it validates integrity and applies the platform policy); the deploy/package codes are host-side.