\newcommand{\Oeuf}{\OE uf\xspace} \newcommand{\eg}{\emph{e.g.}\xspace}

Verifying systems by implementing them in the programming language of a proof assistant (\eg, Gallina for Coq) lets us directly leverage the full power of the proof assistant for verifying the system. But, to execute such an implementation requires \emph{extraction}, a large complicated process that is in the trusted computing base (TCB).

This paper presents \Oeuf, a verified compiler from a subset of Gallina to assembly. \Oeuf's correctness theorem ensures that compilation preserves the semantics of the source Gallina program. We describe how \Oeuf's specification can be used as a foreign function interface to reason about the interaction between compiled Gallina programs and surrounding shim code. Additionally, \Oeuf maintains a small TCB for its front-end by reflecting Gallina programs to \Oeuf
source and automatically ensuring equivalence using computational denotation. This design enabled us to implement some early compiler passes (\eg, lambda lifting) in the untrusted reflection and ensure their correctness via translation validation. To evaluate \Oeuf, we compile Appel's SHA256 specification from Gallina to x86 and write a shim for the generated code, yielding a verified \texttt{sha256sum} implementation with a small TCB.