See the related paper (to appear in PLDI'23), the main Zar Github repository, and similar OCaml package.
See the README of the OCaml version of this package for a general introduction.
This package defines an interface to formally verified samplers constructed by Zar via the streaming abstractions provided by the pipes library.
Core.hs contains the trusted computing base of
the package including functions for converting between Z (the type of
integers used internally by Zar) and Integer (Haskell's type for
arbitrary-precision integers), and driver code for executing the
interaction tree samplers generated by Zar. The numeric conversion
functions are tested thoroughly via QuickCheck in
test/Spec.hs. To run the tests yourself just clone this repo and do stack test.
See Coin.hs.
coin_consumer num denom creates a Consumer of random bits (assumed
to be distributed uniformly) that can be composed with a Producer of
Bool to obtain an Effect that can be run to produce a single
Bool sample with Pr(True) = num / denom. Requires 0 <= num <= denom and 0 < denom.
coin num denom composes the Consumer described above with a
default bit Producer implementation based on the
mwc-random package.
coin_pipe num denom creates a Pipe that behaves similarly to
coin_consumer num denom but produces a stream of output samples. Can
be composed with a uniform bit Producer to obtain a biased bit
Producer.
coin_producer num denom composes coin_pipe num denom with the
default bit Producer.
See Die.hs and Findist.hs. Their interfaces are the same as for the biased coin.