Zar

Paper: https://arxiv.org/abs/2211.06747

Setup

• Coq development:

opam pin add coq 8.16.0
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-itree
make -j4

• zarpy pip package (see python/zar/test/test.py for an example of using it after installation):

opam install pythonlib ppx_import ppx_deriving
cd python/zar/ocaml
dune build zar.so
cd ..
make install

Or:

pip install zarpy

• Extracted sampler analysis scripts (e.g., analyze.py):

pip install numpy matplotlib scipy

Foundational

• Axioms: axioms.v
• Extended reals: eR.v
• Tactics: tactics.v

cpGCL and cwp

• cpGCL syntax: cpGCL.v
• cwp semantics: cwp.v

CF Trees

• CF trees: tree.v, tcwp.v, tcwp_facts.v
• Compiler from cpGCL to CF trees: compile.v, cwp_tcwp.v
• De-biasing: uniform.v, debias.v

Generating Interaction Trees

• Generating itrees: itree.v

Order/Domain Theory and Algebraic Coinductives

• Basic order theory: order.v
• CPOs: cpo.v
• Algebraic CPOs and comorphisms: aCPO.v
• Cotrees: cotree.v, cocwp.v, cocwp_facts.v

Sampling Equidistribution Theorems

• Equidistribution theorems for itrees, cotrees, CF trees, and cpGCL: equidistribution.v

Empirical Validation

extract/ contains driver code and scripts for evaluating extracted samplers (e.g., dueling coins, n-sided die, geometric distribution, discrete gaussian, hare and tortoise).

fast-loaded-dice-roller/ contains a clone of https://github.com/probcomp/fast-loaded-dice-roller modified to track entropy usage.

optimal-approximate-sampling/ contains a clone of https://github.com/probcomp/optimal-approximate-sampling modified to track entropy usage.

python/zar/ contains the zarpy pip package source.

python/tf/ contains the TensorFlow 2 project, with batch_gen.py implementing a sampling-without-replacement generator on top of the zarpy sampler package.