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.