| Name | zarpy JSON |
| Version |
1.0.1
JSON |
| download |
| home_page | |
| Summary | Formally verified biased coin and n-sided die |
| upload_time | 2023-03-10 05:41:42 |
| maintainer | |
| docs_url | None |
| author | Alexander Bagnall |
| requires_python | >=3.6.3 |
| license | MIT License Copyright (c) [2022] [Alexander A. Bagnall] Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
| keywords |
zar
zarpy
random
sampler
biased
coin
bernoulli
uniform
die
verified
coq
|
| VCS |
|
| bugtrack_url |
|
| requirements |
No requirements were recorded.
|
| Travis-CI |
No Travis.
|
| coveralls test coverage |
No coveralls.
|
# Zarpy: formally verified biased coin and n-sided die.
See the [paper](https://arxiv.org/abs/2211.06747) (to appear in
PLDI'23) and [Github repository](https://github.com/bagnalla/zar).
## Why use Zarpy?
### Probabilistic choice
A basic operation in randomized algorithms is *probabilistic choice*:
for some `p ∈ [0,1]`, execute action `a1` with probability `p` or
action `a2` with probability `1-p` (i.e., flip a biased coin to
determine the path of execution). A common method for performing
probabilistic choice is as follows:
```python
if random() < p:
execute a1
else:
execute a2
```
where `p` is a float in the range `[0,1]` and `random()` produces a
random float in the range `[0,1)`. While good enough for many
applications, this approach is not always correct due to float
roundoff error. We can only expect `a1` to be executed with
probability `p + ϵ` for some small error term `ϵ`, which technically
invalidates any correctness guarantees of our overall system that
depend on the correctness of its probabilistic choices.
Zarpy provides an alternative that is guaranteed (by formal proof in
Coq) to execute `a1` with probability `p` (where `n` and `d` are
integers such that `p = n/d`):
```python
from zarpy import build_coin, flip
build_coin((n, d)) # Build and cache coin with bias p = n/d
if flip(): # Generate a Boolean value with Pr(True) = p
execute a1
else:
execute a2
```
### Uniform sampling
Another common operation is to randomly draw from a finite collection
of values with equal (uniform) probability of each. An old trick for
drawing an integer uniformly from the range `[0, n)` is to generate a
random integer from `[0, RAND_MAX]` and take the modulus wrt. `n`:
```python
x = rand() % n # Assign x random value from [0,n)
```
but this method suffers from modulo bias when `n` is not a power of 2,
causing some values to occur with higher probability than others (see,
e.g., [this
article](https://research.kudelskisecurity.com/2020/07/28/the-definitive-guide-to-modulo-bias-and-how-to-avoid-it/)
for more information on modulo bias). Zarpy provides a uniform sampler
that is guaranteed for any integer `0 < n` to generate samples from
`[0,n)` with probability `1/n` each:
```python
from zarpy import build_die, roll
build_die(n)
x = roll()
```
Although the Python function `random.randint` is ostensibly free from
modulo bias, our implementation guarantees so by a *formal proof of
correctness* in Coq.
## Trusted Computing Base
The samplers provided by Zarpy have been implemented and verified in
Coq and extracted to OCaml and bundled into Python package via
[pythonlib](https://github.com/janestreet/pythonlib). Validity of the
correctness proofs is thus dependent on the correctness of Coq's
extraction mechanism, the OCaml compiler and runtime, a small amount
of OCaml shim code (viewable
[here](https://github.com/bagnalla/zar/blob/main/python/zar/ocaml/zarpy.ml)),
and the pythonlib library.
## Proofs of correctness
The coin and die samplers are implemented as probabilistic programs in
the [Zar](https://github.com/bagnalla/zar) system and compiled to
[interaction trees](https://github.com/DeepSpec/InteractionTrees)
implementing them via reduction to sequences of fair coin flips. See
Section 3 of the [paper](https://arxiv.org/abs/2211.06747) for details
and the file
[zarpy.v](https://github.com/bagnalla/zar/blob/main/zarpy.v) for their
implementations and proofs of correctness.
Correctness is two-fold. For biased coin with bias `p`, we prove:
*
[coin_itree_correct](https://github.com/bagnalla/zar/blob/main/zarpy.v#L57):
the probability of producing `true` according to the formal probabilistic
semantics of the constructed interaction tree is equal to `p`, and
*
[coin_samples_equidistributed](https://github.com/bagnalla/zar/blob/main/zarpy.v#L75):
when the source of random bits is uniformly distributed, for any
sequence of coin flips the proportion of `true` samples converges to
`p` as the number of samples goes to +∞.
The equidistribution result is dependent on uniform distribution of
the Boolean values generated by OCaml's
[`Random.bool`](https://v2.ocaml.org/api/Random.html) function. See
[the paper](https://arxiv.org/abs/2211.06747) for a more detailed
explanation.
Similarly, the theorem
[die_itree_correct](https://github.com/bagnalla/zar/blob/main/zarpy.v#L136)
proves semantic correctness of the n-sided die, and
[die_samples_equidistributed](https://github.com/bagnalla/zar/blob/main/zarpy.v#L161)
equidistribution of its samples.
## Usage
`seed()` initializes the PRNG via
[Random.self_init](https://v2.ocaml.org/api/Random.html).
### Biased coin
`build_coin((num, denom))` builds and caches a coin with `Pr(True) =
num/denom` for nonnegative integer `num` and positive integer `denom`.
`flip()` produces a single Boolean sample by flipping the cached coin.
`flip_n(n)` produces `n` Boolean samples by flipping the cached coin.
### N-sided die
`build_die(n)` builds and caches an n-sided die with `Pr(m) = 1/n` for
integer `m` where `0 <= m < n`.
`roll()` produces a single sample by rolling the cached die.
`roll_n(n)` produces `n` integer samples by rolling the cached die.
Raw data
{
"_id": null,
"home_page": "",
"name": "zarpy",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.6.3",
"maintainer_email": "",
"keywords": "zar,zarpy,random,sampler,biased,coin,bernoulli,uniform,die,verified,coq",
"author": "Alexander Bagnall",
"author_email": "Alexander Bagnall <abagnalla@gmail.com>",
"download_url": "https://files.pythonhosted.org/packages/4c/56/0a7fc15f4a73008ee19e47a9bec2e9425776132dc131a9d35ae3e957d9fd/zarpy-1.0.1.tar.gz",
"platform": null,
"description": "# Zarpy: formally verified biased coin and n-sided die.\n\nSee the [paper](https://arxiv.org/abs/2211.06747) (to appear in\nPLDI'23) and [Github repository](https://github.com/bagnalla/zar).\n\n## Why use Zarpy?\n\n### Probabilistic choice\n\nA basic operation in randomized algorithms is *probabilistic choice*:\nfor some `p \u2208 [0,1]`, execute action `a1` with probability `p` or\naction `a2` with probability `1-p` (i.e., flip a biased coin to\ndetermine the path of execution). A common method for performing\nprobabilistic choice is as follows:\n```python\nif random() < p:\n execute a1\nelse:\n execute a2\n```\n\nwhere `p` is a float in the range `[0,1]` and `random()` produces a\nrandom float in the range `[0,1)`. While good enough for many\napplications, this approach is not always correct due to float\nroundoff error. We can only expect `a1` to be executed with\nprobability `p + \u03f5` for some small error term `\u03f5`, which technically\ninvalidates any correctness guarantees of our overall system that\ndepend on the correctness of its probabilistic choices.\n\nZarpy provides an alternative that is guaranteed (by formal proof in\nCoq) to execute `a1` with probability `p` (where `n` and `d` are\nintegers such that `p = n/d`):\n```python\nfrom zarpy import build_coin, flip\nbuild_coin((n, d)) # Build and cache coin with bias p = n/d\nif flip(): # Generate a Boolean value with Pr(True) = p \n execute a1\nelse:\n execute a2\n```\n\n### Uniform sampling\n\nAnother common operation is to randomly draw from a finite collection\nof values with equal (uniform) probability of each. An old trick for\ndrawing an integer uniformly from the range `[0, n)` is to generate a\nrandom integer from `[0, RAND_MAX]` and take the modulus wrt. `n`:\n```python\nx = rand() % n # Assign x random value from [0,n)\n```\nbut this method suffers from modulo bias when `n` is not a power of 2,\ncausing some values to occur with higher probability than others (see,\ne.g., [this\narticle](https://research.kudelskisecurity.com/2020/07/28/the-definitive-guide-to-modulo-bias-and-how-to-avoid-it/)\nfor more information on modulo bias). Zarpy provides a uniform sampler\nthat is guaranteed for any integer `0 < n` to generate samples from\n`[0,n)` with probability `1/n` each:\n```python\nfrom zarpy import build_die, roll\nbuild_die(n)\nx = roll()\n```\n\nAlthough the Python function `random.randint` is ostensibly free from\nmodulo bias, our implementation guarantees so by a *formal proof of\ncorrectness* in Coq.\n\n## Trusted Computing Base\n\nThe samplers provided by Zarpy have been implemented and verified in\nCoq and extracted to OCaml and bundled into Python package via\n[pythonlib](https://github.com/janestreet/pythonlib). Validity of the\ncorrectness proofs is thus dependent on the correctness of Coq's\nextraction mechanism, the OCaml compiler and runtime, a small amount\nof OCaml shim code (viewable\n[here](https://github.com/bagnalla/zar/blob/main/python/zar/ocaml/zarpy.ml)),\nand the pythonlib library.\n\n## Proofs of correctness\n\nThe coin and die samplers are implemented as probabilistic programs in\nthe [Zar](https://github.com/bagnalla/zar) system and compiled to\n[interaction trees](https://github.com/DeepSpec/InteractionTrees)\nimplementing them via reduction to sequences of fair coin flips. See\nSection 3 of the [paper](https://arxiv.org/abs/2211.06747) for details\nand the file\n[zarpy.v](https://github.com/bagnalla/zar/blob/main/zarpy.v) for their\nimplementations and proofs of correctness.\n\nCorrectness is two-fold. For biased coin with bias `p`, we prove:\n\n*\n [coin_itree_correct](https://github.com/bagnalla/zar/blob/main/zarpy.v#L57):\n the probability of producing `true` according to the formal probabilistic\n semantics of the constructed interaction tree is equal to `p`, and\n\n*\n [coin_samples_equidistributed](https://github.com/bagnalla/zar/blob/main/zarpy.v#L75):\n when the source of random bits is uniformly distributed, for any\n sequence of coin flips the proportion of `true` samples converges to\n `p` as the number of samples goes to +\u221e.\n\nThe equidistribution result is dependent on uniform distribution of\nthe Boolean values generated by OCaml's\n[`Random.bool`](https://v2.ocaml.org/api/Random.html) function. See\n[the paper](https://arxiv.org/abs/2211.06747) for a more detailed\nexplanation.\n\nSimilarly, the theorem\n[die_itree_correct](https://github.com/bagnalla/zar/blob/main/zarpy.v#L136)\nproves semantic correctness of the n-sided die, and\n[die_samples_equidistributed](https://github.com/bagnalla/zar/blob/main/zarpy.v#L161)\nequidistribution of its samples.\n\n## Usage\n\n`seed()` initializes the PRNG via\n[Random.self_init](https://v2.ocaml.org/api/Random.html).\n\n### Biased coin\n\n`build_coin((num, denom))` builds and caches a coin with `Pr(True) =\nnum/denom` for nonnegative integer `num` and positive integer `denom`.\n\n`flip()` produces a single Boolean sample by flipping the cached coin.\n\n`flip_n(n)` produces `n` Boolean samples by flipping the cached coin.\n\n### N-sided die\n\n`build_die(n)` builds and caches an n-sided die with `Pr(m) = 1/n` for\ninteger `m` where `0 <= m < n`.\n\n`roll()` produces a single sample by rolling the cached die.\n\n`roll_n(n)` produces `n` integer samples by rolling the cached die.\n",
"bugtrack_url": null,
"license": "MIT License Copyright (c) [2022] [Alexander A. Bagnall] Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the \"Software\"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.",
"summary": "Formally verified biased coin and n-sided die",
"version": "1.0.1",
"split_keywords": [
"zar",
"zarpy",
"random",
"sampler",
"biased",
"coin",
"bernoulli",
"uniform",
"die",
"verified",
"coq"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "6d8bc0aadb8a10c90c71e504c38e0bd36de0a34b279f0f40660f0abefdf440c0",
"md5": "8cb54012c7418996532e07d688b09a0a",
"sha256": "741d1b23f50622103a40404a40a9bfdc25f18f8138354a0ce70954f20531b047"
},
"downloads": -1,
"filename": "zarpy-1.0.1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "8cb54012c7418996532e07d688b09a0a",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.6.3",
"size": 6057384,
"upload_time": "2023-03-10T05:41:35",
"upload_time_iso_8601": "2023-03-10T05:41:35.991121Z",
"url": "https://files.pythonhosted.org/packages/6d/8b/c0aadb8a10c90c71e504c38e0bd36de0a34b279f0f40660f0abefdf440c0/zarpy-1.0.1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "4c560a7fc15f4a73008ee19e47a9bec2e9425776132dc131a9d35ae3e957d9fd",
"md5": "7c672b2c45d7ce42a6c81111b0190ad9",
"sha256": "102b4a3f591eb034cae1847a74928953dcf5843146758fa363d75ec7d29567c6"
},
"downloads": -1,
"filename": "zarpy-1.0.1.tar.gz",
"has_sig": false,
"md5_digest": "7c672b2c45d7ce42a6c81111b0190ad9",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.6.3",
"size": 6001785,
"upload_time": "2023-03-10T05:41:42",
"upload_time_iso_8601": "2023-03-10T05:41:42.185167Z",
"url": "https://files.pythonhosted.org/packages/4c/56/0a7fc15f4a73008ee19e47a9bec2e9425776132dc131a9d35ae3e957d9fd/zarpy-1.0.1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-03-10 05:41:42",
"github": false,
"gitlab": false,
"bitbucket": false,
"lcname": "zarpy"
}
