https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
e26e48e Adding missing `mli` and theory files 16 August 2022, 08:33:12 UTC
8f0c487 Cost Hoare logic v2 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. 13 June 2022, 10:01:08 UTC
cec6716 In loop fusion/fission, add more constraints on the epilog Loops' epilogs must now be deterministic and loop/calls-free. This forbids the following unsoundness: ``` require import AllCore DBool. module E = { var i,j : int proc foo () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; j <- j + 1; c <$ {0,1}; } return i = j; } proc bar () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; c <$ {0,1}; } c <- false; while (!c) { j <- j + 1; c <$ {0,1}; } return i = j; } }. equiv bad : E.foo ~ E.bar : true ==> ={res}. proof. proc. fission{1} 4!1 @1,2. by sim. qed. ``` Fix #210 11 June 2022, 06:10:21 UTC
1f8da33 Add an option that allows EasyCrypt to connect to an external Why3 server The option is -why3server and takes the unix domain socket path as argument. 11 June 2022, 06:02:38 UTC
38c4947 Clear the blocked signals mask on startup. In some circumstances, the inherited mask disturbs Why3 server. 10 June 2022, 09:40:59 UTC
7fed186 new command: exit (stops EasyCrypt) 04 June 2022, 11:20:29 UTC
4e97480 [runtest]: use all cores by default 03 June 2022, 12:06:38 UTC
0ea3d99 rename depext to opam-depext The `depext` package fails to install with recent versions of opam. The fix suggested in the package information is to use the renamed package `opam-depext` instead. 02 June 2022, 11:26:56 UTC
d083fc5 [dune]: (re)-codesign promoted binaries Dune substitution breaks the initial code-signing. The problem has been acknowledge by the dune team and should be fixed on their side at some point. 01 June 2022, 06:32:41 UTC
e45a54c smt option to dump a smt query to a file 20 May 2022, 14:00:39 UTC
90826b1 default.nix: use why3 1.5.0 19 May 2022, 08:16:49 UTC
b44893a [runtest]: exit with a non-zero exit status in case of failure. 18 May 2022, 05:22:28 UTC
168c6d7 [runtest]: do not display warnings/infos as errors Fix #198 18 May 2022, 05:22:28 UTC
3c1476b Fix pretty-printing of projections. Former printer was using an invalid priority for projections. Fixes #200 17 May 2022, 14:43:37 UTC
24b0ce7 Updating README for current why3 requirements. 17 May 2022, 08:36:55 UTC
762988d mark `transpose` as parse-only We have suffered long enough 16 May 2022, 09:27:43 UTC
b44bcba [stdlib]: more lemmas around dfun. Main result is the equivalence between sampling a function and sampling a function in the same function space, but for one point that is sample a posteriori. 14 May 2022, 21:58:53 UTC
2e5cc0e [stdlib] new lemmas around dscalar & dlet. 14 May 2022, 21:58:53 UTC
b66eb5c [stdlib]: new operator for updating a function at one point. Notation is "f.[x <- v]" for the function that is equal to "f" but at value "x" where it returns "v". 14 May 2022, 21:58:45 UTC
b6f7335 New `runtest` script - more readable output (for tty / no-tty) - more readable report 14 May 2022, 21:49:14 UTC
c629679 Fix pretty-printing of mixfix notations. The notation was not printed when the operators was over-applied. E.g., f.[x <- v] y was printed "_.[_<-_]" f x v y. 14 May 2022, 21:32:09 UTC
164a167 README: remove "make PREFIX=" 13 May 2022, 07:23:39 UTC
a76ddc7 README: configuration Why3 using EasyCrypt 13 May 2022, 07:23:18 UTC
5ff9d70 When configuring Why3, create the configuration file destination directory first 13 May 2022, 07:18:32 UTC
92941b1 [stdlib]: link Finite & FinType. 12 May 2022, 07:12:12 UTC
1e12363 error on potential procedure call in RHS of <- If the RHS of a <- fails to typecheck as an expression but could be a procedure call, mention <@ as an alternative 12 May 2022, 06:49:18 UTC
5d030a1 Enforce separation between <- and <@ more strictly This removes the error message when the RHS is a procedure call. This allows us to accept things that were rejected before, when a procedure and operator share their name. A follow-up may re-enable it. Fix #189 12 May 2022, 06:49:18 UTC
cdc065e [stdlib]: add various small lemmas (Logic, FSet, Distr, DInterval, Bigop) - #non-backward-compatible: this commits generalizes `Bigop.reindex` to restrict the cancellation property to the index list. 12 May 2022, 06:43:29 UTC
de42d06 Change configuration file resolution Do not consider locations that point to non-existing files. The configuration file location is now printing by the `config` command. 10 May 2022, 12:14:09 UTC
f1ce5ae Finite.to_seq: now have a body based on choiceb Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> 09 May 2022, 11:54:13 UTC
a49a0ac Bump Why3 version from 1.4.x to 1.5.0 fix #184 05 May 2022, 13:58:12 UTC
a1eeaf0 [github-action]: do not start as root This requires a modification of the docker image s.t. the user UID is compatible with the one used by Github Action 05 May 2022, 13:14:49 UTC
aab2ca4 Use local configuration file in priority 27 April 2022, 12:46:45 UTC
dbdca26 Fic computation of source root for local builds 27 April 2022, 12:46:13 UTC
577c882 Fix the license announced in the banner 27 April 2022, 09:48:51 UTC
8f314e4 Makefile 26 April 2022, 08:49:07 UTC
89df8ee move cost axioms in abstract theories (fix #175) 26 April 2022, 08:43:31 UTC
9c03562 Reject `x <- RHS` when `RHS` is a procedure call 22 April 2022, 11:13:38 UTC
7b70089 Improve parser for anonymous proc parameters Anonymous and named parameters can be mixed for abstract procedures. Corner cases are not exercised by test suites and may crop up. Resolves #108. 22 April 2022, 10:53:46 UTC
74a4d02 Fixing list of authors 22 April 2022, 06:59:36 UTC
2c53183 [env]: fully head-norm the type before fetching its top-level decl. This commit involves a lot of code motion. partially address #121 22 April 2022, 06:59:22 UTC
bfd4f84 [reduction]: in cbv, fix handling of stack arguments The API was s.t. it was possibly to detect a non-empty stack as an empty one. Partially address #121 22 April 2022, 06:59:22 UTC
ecb156d error message if cost information are missing in the call tactic 08 April 2022, 19:27:18 UTC
4dec70e Fix typing of modules expressions fix #171 07 April 2022, 09:47:53 UTC
ae4fe92 [reduction]: use symmetric "and" when reducing tuples equality fix #171 05 April 2022, 10:59:53 UTC
d5941d0 pretty printer improvements for module restrs + local memtypes 31 March 2022, 15:38:14 UTC
3491166 Remove superflous renamings fixes #146 31 March 2022, 13:49:22 UTC
98fbc44 [tactic]: [proc*]: fix procedure's arguments substitution Instead of introduce a single variable for the arguments tuple, introduce all the procedure's arguments as single program variables. Fix #166 31 March 2022, 07:49:56 UTC
29061b7 [chore] update theories/dune 30 March 2022, 12:32:24 UTC
0b0aa5d [tactic]: [rewrite]: support for multi-rules `rewrite h` with `h : eq1 /\ eq2 /\ ... /\ eqn` is equivalent to `rewrite ?(h1, h2, ..., hn)` with `hi : eqi` address #155 30 March 2022, 08:50:08 UTC
f876954 License change: CeCILL B/C -> MIT 29 March 2022, 19:39:31 UTC
b229a87 dopt: extend subdistribution to lossless distributions on options 29 March 2022, 14:19:04 UTC
1a754ad [tactic]: in `apply... in...`, check that all variables are instantiated fix #149 29 March 2022, 09:05:09 UTC
7a93224 [build]: [dune]: auto-generation of theories/dune 28 March 2022, 17:07:06 UTC
a9748f7 New logic to upper-bound the worst-case complexity of programs ** Breaking change: - to be consistent with oracle calls restrictions, negative memory restrictions are now set using a minus symbol (e.g. `(M <: T {-H})` instead of `(M <: T {H})`). - use `pragma +old_mem_restr` to retrieve old behaviour on memory restrictions ** Additions: - added a new hoare logic for cost, using predicates of the form `choare [H.f: pre ==> post] time [c]`, meaning: from any initial memory satisfying `pre`, the final memory obtained after the execution of `H.f` satisfies `post`, in time at most `c` - in choare predicates, the cost `c` is a cost-vector, comprising: + a concrete cost of type `xint`, where `xint` is a algebraic data-type with two constructors, `N of int` (for bounded running times) and `Inf` (for potentially unbounded running times). + a list of abstract procedures together with an integer indicated the number of times they can be called (e.g. `ROM.o : 42`). - complexity restrictions can be attached to module types procedures, restricting their instantiations. - added a new predicate, `cost`, to establish the cost of evaluating an expression (while `choare` upper-bound the cost of a statement). - (small) examples showing how to use the cost hoare logic can be found in the sub-directory `examples/cost/` - more advanced examples, using a new UC framework in EasyCrypt, can be found in `examples/UC/composition_cost.ec` `examples/UC/dh_enc_cost.ec` 28 March 2022, 10:45:44 UTC
b13fb54 Add lemmas divzMr and divzMl; strenghten and prove modz_pow2_div. 17 March 2022, 20:33:03 UTC
3646dd8 changed name of lemma 12 March 2022, 10:06:23 UTC
d5df8b2 added stronger version of dmap1E_can 12 March 2022, 10:06:23 UTC
c98b014 Extend standard library (IntDiv) with core results. 03 March 2022, 18:13:54 UTC
e22c918 Added definition and lemmas for 'put' operator in List.ec. 03 March 2022, 12:53:02 UTC
8cfa32b An axiom-free formalization of well-founded relations, induction and recursion. 03 March 2022, 09:50:40 UTC
6199997 Generalize `LorR` theory Generalize the `LorR` theory to make it possible to give some input to `L.main` and `R.main`. Using the theory for procedures without input is still possible by cloning the theory with type `input <- unit`. 03 March 2022, 09:50:19 UTC
b06e700 Stdlib: more results on integer division & exponentiation 02 March 2022, 16:28:09 UTC
c316eff Removed redundant "rec" in function declaration. 01 March 2022, 14:04:58 UTC
77aac4b Revert "Unfold non-transparent operators in `case` & `elim`." This reverts commit 70662a755d2121ca1c809cf2eef68462bd720d72. 24 February 2022, 07:02:59 UTC
559910b Partially fix memory capture in substitutions closes #130 22 February 2022, 09:41:14 UTC
ce4d8ca [dune+opam] fix git hash versioning widget 21 February 2022, 18:24:12 UTC
f278e3c Lemma stating equality of word and list distributions 18 February 2022, 22:51:52 UTC
70662a7 Unfold non-transparent operators in `case` & `elim`. When `case` or `elim` search for a redex, allows the reduction to unfold non-transparent operators. This does not affect tactics that does case/elim internally (e.g., />). fix #132 18 February 2022, 22:18:29 UTC
03a3fe8 Fails gracefully when applying a tactic on a completed proof. fix #133 18 February 2022, 22:18:29 UTC
39b2562 Get rid of dune-site dune-site is currently in a very alpha-state and not stable enough. fix #99 fix #115 16 February 2022, 06:38:37 UTC
ce56b10 Add rdirs option in config file closes #127 19 January 2022, 22:45:29 UTC
46ba308 Apply suggestions from code review Co-authored-by: Francois Dupressoir <fdupress@gmail.com> 05 January 2022, 13:39:35 UTC
49e768e fix theories 05 January 2022, 13:39:35 UTC
e77248a allow zero queries in Hybrid and SDist 05 January 2022, 13:39:35 UTC
49aec58 lemmas on FSet, List, and DList 10 December 2021, 17:02:37 UTC
7df1de5 First pass: slices are inclusive 09 December 2021, 21:39:05 UTC
32abff2 some lemmas on subseq, fmap, and drat 09 December 2021, 06:26:12 UTC
799d429 add lemma RO_LRO and generalize RO_FinRO_D 08 December 2021, 13:26:16 UTC
8e47fe3 Fix bug that prevents `rewrite //= in h` to simplify in `h` Fix #68 03 December 2021, 16:12:21 UTC
6a6f3b8 Merge pull request #105 from EasyCrypt/deploy-lift-lro lift LRO oracle out of FullEager 03 December 2021, 08:56:41 UTC
e77e653 lift LRO oracle out of FullEager 03 December 2021, 08:00:10 UTC
fe9a171 Update ci.yml 03 December 2021, 05:09:09 UTC
541aa08 fix substitution of modules when cloning. fix #97 02 December 2021, 10:41:39 UTC
4a1ce0d [docker] Build box base is now an opam image The original base was 5 months out of date. An issue in the build was due to opam running as root. The replacement base image is setup for opam to not run as root while allowing passwordless sudo. 02 December 2021, 08:09:28 UTC
2e815c5 PROM: add a ROmap interface for RO + access to the internal map 02 December 2021, 07:48:19 UTC
dda8233 CI / Zulip 02 December 2021, 07:46:33 UTC
f66167f [dune] add abstract theories to install list 26 November 2021, 15:00:50 UTC
b37b762 Prototype implementation of a match statement. 23 November 2021, 16:58:42 UTC
f8514a6 remove ocamlbuild.ml 22 November 2021, 17:48:42 UTC
50dae1b [build] install runtest (as ec-runtest) 21 November 2021, 16:30:31 UTC
3476312 script for graphing a dependency graph for .eco 19 November 2021, 10:53:40 UTC
08ed0c2 New format for eco (v3) Store whether a theory has been directly required or not. 19 November 2021, 07:18:46 UTC
471ea3b foo 19 November 2021, 07:04:08 UTC
a549eb4 Add an option to define opaque operators This can be done by adding the "opaque" tag, e.g.: op [opaque] myop = ... solve #94 19 November 2021, 06:27:09 UTC
10e1563 remove \# files 19 November 2021, 06:09:01 UTC
ffe0656 New command: locate [partial-qualid] This command allows to locate and print the fullname & shortest name of an operator, a lemma or a type declaration. fix #82 18 November 2021, 14:23:49 UTC
92f23db Add the project name in dune-project This is needed by "dune subst" ref #99 18 November 2021, 12:06:45 UTC
5e3929a remove debugging code 18 November 2021, 12:06:09 UTC
17e143c 17 November 2021, 15:41:35 UTC
back to top