Non-Interactive Zero-Knowledge (NIZK) Proofs enable a prover to cryptographically prove that any polynomial-time program will produce a certain output on a provided set of inputs, while hiding any combination of inputs and outputs. However, current tools for specifying NIZKs operate at a very low level of abstraction. They fail to leverage an inherent duality between how proofs are constructed and verified, preventing significant code reuse and complicating maintenance. Towards this end, we present a new language feature that addresses this shortcoming by combining these two operations as a single piece of code that represents both. We define a translation that compiles the combined code into two separate components, matching the low-level structure expected by existing cryptographic libraries. Our ongoing work aims to prove critical metatheory about our language, including powerful notions of compiler correctness.