https://github.com/EasyCrypt/easycrypt
Revision 8f0c487e34e3ab34eeb73877aad0115c17bb7624 authored by Adrien Koutsos on 13 June 2022, 10:01:08 UTC, committed by Adrien Koutsos on 13 June 2022, 10:01:08 UTC
Second version of the cost Hoare logic. Here are the objectives of this new version (some are still [WIP]): - 1) removed the "flattened" semantics of cost vectors - 2) [WIP] less boilerplate, better user interaction - 3) [WIP] use cost information in other Hoare logics 1) No flattened semantics: - the previous semantics flattened the cost vectors, i.e. `{42, A.f: 2}` was to be understood as the integer `42 + 2 * intr_A.f` where `intr_A.f` is the intrinsic cost of `A.f`. This flattened semantics prevent from ignoring the concrete cost of a procedure (setting it to be at most +infinity), while still bounding the number of calls to some specific module parameters or abstract modules. - previous point necessary to use cost information in other Hoare logics (especially to remove counting wrappers), while ignoring the concrete cost. - in some settings (e.g. quantum, information theoretic arguments, rejection samplings), the worst-case concrete cost may be unbounded. It is therefore crucial to get rid of the flattened semantics to apply the cost logic in these settings 2) Less boilerplate (still [WIP]): - w.r.t. the old approach, which requires to write, for every pair of procedure and oracle procedure, the number of times the former can call the latter => somehow quadratic number of constants to introduce/write - no new boilerplate added even though we prove more. Indeed, if we remove the flattened semantics and kept the old style for stating lemmas, then we also need to anticipate and state that some procedure will call some abstract module (not a functor parameter) some number of times. Issues: * this is heavy; * if we use many times the lemma, in ≠ contexts with ≠ abstract modules, then we need to anticipate *each* usage in the lemma statement. 3) use cost information in Hoare logics (still [WIP]): - remove wrappers with little overhead.
1 parent cec6716
Tip revision: 8f0c487e34e3ab34eeb73877aad0115c17bb7624 authored by Adrien Koutsos on 13 June 2022, 10:01:08 UTC
Cost Hoare logic v2
Cost Hoare logic v2
Tip revision: 8f0c487
File | Mode | Size |
---|---|---|
.github | ||
config | ||
examples | ||
lint | ||
scripts | ||
src | ||
theories | ||
.dir-locals.el | -rw-r--r-- | 285 bytes |
.gitignore | -rw-r--r-- | 118 bytes |
AUTHORS | -rw-r--r-- | 543 bytes |
LICENSE | -rw-r--r-- | 1.2 KB |
Makefile | -rw-r--r-- | 1.2 KB |
README.md | -rw-r--r-- | 7.7 KB |
default.nix | -rw-r--r-- | 855 bytes |
dune | -rw-r--r-- | 116 bytes |
dune-project | -rw-r--r-- | 388 bytes |
easycrypt.opam | -rw-r--r-- | 1.2 KB |
easycrypt.opam.template | -rw-r--r-- | 915 bytes |
easycrypt.png | -rw-r--r-- | 182.6 KB |
Computing file changes ...