kernel the trusted type checker for eidos. a nox program of 9 CIC typing rules (one per term constructor) encoded as Layer 1 patterns. this is the TCB — the only component whose correctness must be assumed. everything outside the kernel is untrusted shell. interface the kernel exposes two…