Reference Checker

Reference Checker (the TCB)

Verification has two permanently separated roles, and only one of them is trusted:

EncodeLive(obj) → bytes          CheckBytes(package, config) → VALID(J) | INVALID(code) | INDETERMINATE(code)
  the untrusted adapter            the NORMATIVE checker — the sole trusted function of the authority layer
  may run getters / toJSON         total, deterministic, over immutable octets; a live object never enters it
  NOT in the TCB                   IS the TCB (with the leaf crypto it imports)

checkAuthorityProofBytes takes immutable bytes in and returns a tri-state verdict out. It re-derives every authority judgment from leaf crypto over content-addressed bytes, importing only leaf primitives (canon/H/keyId/edVerifyStrict/contentHash + the pure Merkle verifiers) — never the producer stack. So it is a genuine independent second derivation, and the producer is demoted to an untrusted prover that only proposes terms. TCB = this checker + the leaf primitives.

Why it is built this way

• Total, deterministic, closed tri-state. Every input maps to VALID / INVALID / INDETERMINATE — it never throws, loops, or returns something else. INDETERMINATE (cannot decide) is never conflated with INVALID (forged).
• Soundness statement. check_C(π, W) = VALID(J) ⇒ there exists a derivation of J whose leaves are crypto verifications over W (proof: structural induction on the term). This is the L1 executable-soundness candidate; the Formal Model is the semantics it realizes, and the L2 milestone is the machine-checked (Lean) end state.

How it stays honest

• Conformance vectors + a byte corpus (vectors/) are the cross-implementation arbiter — any implementation must pass them byte-for-byte.
• Robustness fuzz asserts totality/determinism (no throws, no non-tri-state, no false-accepts) over thousands of probes.
• A recurring diverse-model adversarial audit → math-first remediation hardens it: an external model attacks the checker, every finding is independently reproduced, adjudicated against the formal model, and fixed structurally (not point-wise). The audit itself is dogfooded as a UST request↔response [[Chains and Layered Shards|chain]].

Progress is tracked in the Reference checker milestone. The value model, the vector arbiter, and the crypto boundary for a clean-room port are in PORTING.md.