Revision 9e114126d5961fa73a21372b8a44f64723d79242 authored by François Dupressoir on 16 January 2020, 20:48:25 UTC, committed by François Dupressoir on 16 January 2020, 20:48:25 UTC
This pushes several complex low-level arguments related to sampling
in restricted distributions into the related distribution file.
This also generalizes these arguments, so that:
- TwoStepSampling no longer requires a full distribution,
- WhileSampling takes distributions and tests as procedure arguments
rather than clone parameters.
Specialized versions of theories and lemmas that reproduce the old
behaviours are also included.
The Dice_Sampling theory is removed, replaced with
Dexcepted.WhileSamplingFixedTest (an abstract theory).
Squashed commit of the following:
commit e4bf1725f2a327bc58dda51d0079acb8dbb8fb1a
Author: François Dupressoir <fdupress@gmail.com>
Date: Thu Jan 16 20:40:23 2020 +0000
trailing white space in modified files
commit 12d5ff0ae8607be10f7e925d1f0d44dd8e78dbde
Author: François Dupressoir <fdupress@gmail.com>
Date: Thu Dec 19 15:49:41 2019 +0000
minor cleanup
commit 7921a24e13e9f6d19ad02c0a22e8efb49bc37184
Author: François Dupressoir <fdupress@gmail.com>
Date: Thu Dec 19 13:47:19 2019 +0000
More general ways of sampling out of a predicate
TwoStep no longer requires losslessness. More sharing of proof could be
obtained
commit 393700f85b47b9d373be983b1451b08ae3d3be94
Author: François Dupressoir <fdupress@gmail.com>
Date: Thu Dec 5 21:40:16 2019 +0000
PRP<->PRF uses generic resampling
commit 74b9aef924cc313e358510ab9f83bc7410489db4
Author: François Dupressoir <fdupress@gmail.com>
Date: Thu Dec 5 21:27:12 2019 +0000
Slight generalization: no longer need a full distribution
commit 0853fc0e313bb6adac0ad956417480ebd70f512f
Author: François Dupressoir <fdupress@gmail.com>
Date: Thu Dec 5 18:34:43 2019 +0000
Dexcepted: equivalence between two ways of sampling
used in PRP<->PRF, but also in a current proof
TODO: make PRP<->PRF use this
1 parent cd341ca
.travis.yml
sudo: required
dist: trusty
language: ocaml
branches:
only:
- 1.0
- 1.0-preview
- /^deploy-.*$/
services:
- docker
env:
global:
- secure: "eRyc2bjGlUEZ9CUuu7B6cEzV1kneAUflxaFSMNRvtAAaIjubRsoeC7XxaS5cziHLyOZeQF1KibNR/PHWkXk9R2TxxaqLhlh4FAUpGkmzF7fNCsAhnImx19yAO7p1BAkMAizbmAZK9YuNrBatBz4YC0tW7w0qhgx2BwnuYropLWiX2rAkhmrA7HxhF+FTJM84AHEFRgch4V6xrnwGmhf9FsIVsXGdJBpdBcz9s3OAmXeA5eo45x4UFmWLKejjLfnYlAeAKvSjknZbBiQwv+RtUbMBwoiPHhP7hWSVBecyMe8UWlydjUilmvw36yx4Dm/t3vj2acwqb+4EPvcpCWeYbZyug8aR+W84grDZNBI7OZVgmaacj70hrfZ35k38n5CM9mXWtWHWRW8x2nMIEapT+pGhyW09YdKtcdty+cQpwwK3yLbtZulhJ+zAdskrBzst/bOgv6+dYCd/lOiQAh3U7dFPW3h7P/uCehUZbk9ofq6iFTQsl2a0lrDBLhGBp2iZZTRz6S/7AOspK0upp988xkqsw+pE/tRndSF/b2tU0wfOARuqpuzcMl/RIhuFLmlopKC40RR3/c3Jr6RWMwia0FWheVng923SQzyxKoyTcRnJJxg5HYrg8X50b0kDzTt2cnkPbBbETtO7Ilppg7QQq9ELeuFMNyDuto9t+K2WD7M="
- secure: "shtTydyWLlFJnIu9yiRYOrpCxiJP1VaNw+6ByNBQdMb3rGJ4PHCRVmuWMN0RKy3ebFbZ1/+FNH3zd2qZn/5RKw2/X02AgqWSCR1HyO3GPOwzg6OUzIFxNHXBCBa1Zeq/kA2xlbSjuxGWWX6/SF5TS6/jeYA7jibrAf5GbjUGD3gVlOjaIgOS3R0Jw3ReA8uPE2aQhcaW36jUXKckxLbgArueubt18TzTqWRH7TysgrtgIw+YYNUP0BAeYZdlI5bFtmNmDNXOWS2UKAlLutGXgjM515Twq1plCBDZlncMTbgfFsNTNd56/T33W/GiNFNAh8sEu2AAqryu/c+SxYAgdr4eyDM1zUI+NWmKu7OEUsXHGrb0hlWYoln0lwSUyr0VoIJ0rBvTGFyi+xvkxZAGYtc/3gN86qjZ3MctoX/mckY0b7n7P6vY1FSdwNYqjP5VA9XjVXXex3gWEyhqUjWK+M2gPREVnS2mxMx8fcv9D5TJ3aoetrclro1nTrSHfPveidkGRjqTgJ01tL0U7yQePGGOhvWQhQM1E0LSGZKx/uwAKkPkOC+MiHipM8I2dQ/I2nAeJPNFqT7R66YAQi2nhjIpLTC1O1/K0YiIT92GJ39UH4+s/6tau0DvGPMX3xJNeKqaECK7cXp6Xj3I51xPgSk15BpIcOjSMieIGXpkEkE="
- TIMESTAMP=$(date -Ins)
matrix:
- TARGETS=build
- TARGETS=check
- TARGETS=examples
notifications:
email:
- tracker@easycrypt.info
before_install:
- docker pull easycryptpa/ec-build-box
after_failure:
- >-
[ -f report.log ] && curl --digest -u ${DAV_USER}:${DAV_PASSWORD} -sT report.log
https://www.easycrypt.info/reports/report-${TARGETS}-${TIMESTAMP}.log
script:
- >-
docker run -v $PWD:/home/ci/easycrypt:rw easycryptpa/ec-build-box
sh -c "cd easycrypt && opam config exec -- make ${TARGETS}"
Computing file changes ...
