https://github.com/EasyCrypt/easycrypt
Revision 66c830f9593684da87d07c365a68f1a17156de74 authored by François Dupressoir on 15 June 2020, 14:55:33 UTC, committed by François Dupressoir on 15 June 2020, 14:55:33 UTC
Now reduced to PROM as core, with ROM as a simpler interface.

PROM is concrete to allow reuse of its flag type.
Its internal theories, and ROM, are abstract to avoid growing forests of clones
when using eager arguments.

ROM now aligns with PROM in cloning interface: additional types `d_in_t` and `d_out_t`
specify the distinguisher's interface. (This simplifies instantiation.)

Some changes to type and oracle names to make them more explicit. Notably:
- `from` is now `in_t`,
- `to` is now `out_t`, (with associated change on name of distribution).
1 parent 734e5bb
History
Tip revision: 66c830f9593684da87d07c365a68f1a17156de74 authored by François Dupressoir on 15 June 2020, 14:55:33 UTC
Clean up the ROM libraries
Tip revision: 66c830f
File Mode Size
config
examples
lint
scripts
src
theories
.dir-locals.el -rw-r--r-- 285 bytes
.gitignore -rw-r--r-- 515 bytes
.merlin -rw-r--r-- 241 bytes
.travis.yml -rw-r--r-- 2.7 KB
COPYRIGHT -rw-r--r-- 581 bytes
COPYRIGHT.yaml -rw-r--r-- 596 bytes
MANIFEST -rw-r--r-- 596 bytes
Makefile -rw-r--r-- 4.8 KB
Makefile.system -rw-r--r-- 555 bytes
README.md -rw-r--r-- 8.3 KB
_tags -rw-r--r-- 812 bytes
default.nix -rw-r--r-- 305 bytes
myocamlbuild.ml -rw-r--r-- 2.3 KB

README.md

back to top