The VerifiedCompiler library's root module: the trace algebra, the relation combinators built on it, and the refinement framework the passes' correctness proofs are stated in.