ch:trusted-kernels: ch:trusted-kernels

Problem and invariant. Construct an elaborator whose result is accepted only after an independent kernel has reconstructed its type. The invariant has two parts: each core variable annotation agrees with the de Bruijn context, and each stored result type agrees with the type obtained by recursively rechecking the core.

Two representations. Use separate Raw and Core datatypes. Raw lambdas omit their domain; an enclosing ascription supplies it to checking. Core variables, lambdas, applications, and ascriptions store enough type information for a second traversal. An intrinsically typed core would prevent malformed values, but the extrinsic representation permits the decisive tampered-core test.

First complete version. Implement structural type equality and context lookup. Define infer for variables, constants, application, ascription, successor, and RNatElim; define check by a separate lambda clause followed by inference and comparison. Add RReflNat and RIdElim: reflexivity checks a natural endpoint, while identity elimination checks the equality proof and the constant-motive base before returning the motive result. The natural-eliminator clause checks a base at the motive result, a step at Nat -> result -> result, and a scrutinee at Nat.

Now define recheck without calling infer or check. Its CAnn clause first rechecks the body and then compares the result with the claimed type. Its eliminator clause independently checks all three premises. Its CReflNat and CIdElim clauses reconstruct the identity classifier and independently recheck both the base and equality proof. Finally implement shiftAbove and substitute; under a lambda, increment the wanted index and shift the replacement before recursing.

Observable result. The accepted corpus prints exactly:

identity=accept:Nat->Nat
successor=accept:Nat->Nat
application=accept:Nat
beta-substitution=accept:zero
nat-elim=accept:Nat
j-certificate=accept:Bool
wrong-step=reject:motive
wrong-ascription=reject:annotation
wrong-j-base=reject:motive
tampered-core=reject:recheck
tampered-j-proof=reject:recheck
All 11 Chapter 110 corpus cases passed.

The beta case checks the substitution implementation directly. The final five rejection cases cross distinct elaboration and rechecking boundaries.

A failing version. Replace the CAnn rechecker arm by Some claimed. The program still typechecks, but the hand-written CAnn CZero BoolTy core is accepted. The tampered-core line changes to FAIL, so the inline harness exits nonzero. Restore the body recheck and comparison. Then replace the entire CIdElim rechecker arm by a result stub. The program still checks, but the hand-written certificate whose alleged equality proof is CZero changes tampered-j-proof to FAIL. Restore the independent child checks.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact twelve-line run transcript, and an empty audit. Replay both mutations independently, require nonzero test status for each, restore the accepted source, and repeat all four commands. Appendix E owns the accepted and mutant digests and must agree with the artifact README and transcript.

Mathematical boundary. The program has structural type equality, constant motives, finite application and identity certificates, and no universes or dependent function space. It tests independence on the finite corpus; it does not prove that elaboration and rechecking agree for every term of the chapter’s kernel.