Extracting and compiling certified programs may introduce bugs in
otherwise proven-correct code, reducing the extent of the guarantees
that proof assistants and correct-by-construction program-derivation
frameworks provide. We present a novel approach to the extraction
and compilation of embedded domain-specific languages developed in a
proof assistant (Coq), showing how it allows us to extend
correctness guarantees all the way to a verification-aware assembly
language. Our core idea is to phrase compilation of shallowly
embedded programs to a lower-level deeply embedded language as a
synthesis problem, solved using simple proof-search techniques. This
technique is extensible (support for individual language constructs
is provided by a user-extensible database of compilation tactics and
lemmas) and allows the source programs to depend on axiomatically
specified methods on externally implemented data structures,
delaying linking to the assembly stage. We do proof-generating
static analysis of object lifetimes to avoid the need for a garbage
collector, so that our output code is suitable for embedded systems
or system infrastructure. We have composed our new transformation
with others in Coq to provide the first fully proof-generating
automatic translation from SQL-style relational programs into
executable assembly code.