We present Zar: a formally verified compiler pipeline from discrete probabilistic programs with unbounded loops in the conditional probabilistic guarded command language (cpGCL) to proved-correct executable samplers in the random bit model. We exploit the key idea that all discrete probability distributions can be reduced to unbiased coin-flipping schemes. The compiler pipeline first translates a cpGCL program into choice-fix trees, an intermediate representation suitable for reduction of biased probabilistic choices. Choice-fix trees are then translated to coinductive interaction trees for execution within the random bit model. The correctness of the composed translations establishes the sampling equidistribution theorem: compiled samplers are correct wrt. the conditional weakest pre-expectation semantics of cpGCL source programs. Zar is implemented and fully verified in the Coq proof assistant. We extract verified samplers to OCaml and Python and empirically validate them on a number of illustrative examples.

翻译：我们提出Zar：一个从带无界循环的条件概率守卫命令语言(cpGCL)离散概率程序到随机比特模型中经正确性证明的可执行采样器的形式化验证编译器流水线。我们利用所有离散概率分布均可归约为无偏抛硬币方案这一关键思想。该编译器流水线首先将cpGCL程序转化为选择修复树——一种适用于减少有偏概率选择的中间表示。随后将选择修复树转化为适用于随机比特模型执行的余归纳交互树。复合翻译的正确性确立了采样等分布定理：经编译的采样器相对于cpGCL源程序的条件最弱前期望语义是正确的。Zar在Coq证明助手中实现并经过完全验证。我们提取经验证的采样器至OCaml和Python，并在多个示例上进行了实证验证。