Trusting the trust

1. TCB: Pokemon, big hack, compiler
2. Inductive definition
   1. Encoding: simplify the problem
   2. Invariants: solve the infiniteness
   3. Abstraction -> prove by refinement
   4. Modularity -> prove by composition