We are hiring ! See our job offers.
https://github.com/EasyCrypt/easycrypt
14 August 2022, 19:57:04 UTC
sort by:
Revision Author Date Message Commit Date
8aa82ea Pierre-Yves Strub 29 March 2022, 10:28:41 UTC [matching]: when crossing a binder, update the env. accordingly fix #142 29 March 2022, 10:28:41 UTC
7a93224 Pierre-Yves Strub 28 March 2022, 16:59:08 UTC [build]: [dune]: auto-generation of theories/dune 28 March 2022, 17:07:06 UTC
a9748f7 Adrien Koutsos 28 March 2022, 09:19:38 UTC 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 MM 15 March 2022, 09:19:03 UTC Add lemmas divzMr and divzMl; strenghten and prove modz_pow2_div. 17 March 2022, 20:33:03 UTC
3646dd8 Oskar Goldhahn 11 March 2022, 21:20:30 UTC changed name of lemma 12 March 2022, 10:06:23 UTC
d5df8b2 Oskar Goldhahn 11 March 2022, 18:14:23 UTC added stronger version of dmap1E_can 12 March 2022, 10:06:23 UTC
c98b014 Kai-Chun Ning 03 March 2022, 15:26:36 UTC Extend standard library (IntDiv) with core results. 03 March 2022, 18:13:54 UTC
e22c918 MM 13 January 2022, 20:10:45 UTC Added definition and lemmas for 'put' operator in List.ec. 03 March 2022, 12:53:02 UTC
8cfa32b Alley Stoughton 29 March 2021, 13:09:27 UTC An axiom-free formalization of well-founded relations, induction and recursion. 03 March 2022, 09:50:40 UTC
6199997 Morten Solberg 01 March 2022, 09:53:41 UTC 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 Pierre-Yves Strub 02 March 2022, 16:27:38 UTC Stdlib: more results on integer division & exponentiation 02 March 2022, 16:28:09 UTC
c316eff Alley Stoughton 01 March 2022, 14:04:58 UTC Removed redundant "rec" in function declaration. 01 March 2022, 14:04:58 UTC
77aac4b Pierre-Yves Strub 24 February 2022, 07:02:59 UTC Revert "Unfold non-transparent operators in `case` & `elim`." This reverts commit 70662a755d2121ca1c809cf2eef68462bd720d72. 24 February 2022, 07:02:59 UTC
559910b Benjamin Gregoire 22 February 2022, 05:52:41 UTC Partially fix memory capture in substitutions closes #130 22 February 2022, 09:41:14 UTC
ce4d8ca François Dupressoir 21 February 2022, 17:58:38 UTC [dune+opam] fix git hash versioning widget 21 February 2022, 18:24:12 UTC
f278e3c François Dupressoir 14 December 2021, 12:22:51 UTC Lemma stating equality of word and list distributions 18 February 2022, 22:51:52 UTC
70662a7 Pierre-Yves Strub 18 February 2022, 22:18:29 UTC 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 Pierre-Yves Strub 18 February 2022, 22:18:29 UTC Fails gracefully when applying a tactic on a completed proof. fix #133 18 February 2022, 22:18:29 UTC
39b2562 Pierre-Yves Strub 16 February 2022, 06:38:28 UTC 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 François Dupressoir 19 January 2022, 19:29:05 UTC Add rdirs option in config file closes #127 19 January 2022, 22:45:29 UTC
46ba308 Christian Doczkal 14 December 2021, 09:43:58 UTC Apply suggestions from code review Co-authored-by: Francois Dupressoir <fdupress@gmail.com> 05 January 2022, 13:39:35 UTC
49e768e Christian Doczkal 10 November 2021, 11:05:22 UTC fix theories 05 January 2022, 13:39:35 UTC
e77248a Christian Doczkal 09 November 2021, 15:40:12 UTC allow zero queries in Hybrid and SDist 05 January 2022, 13:39:35 UTC
49aec58 Christian Doczkal 10 December 2021, 15:21:46 UTC lemmas on FSet, List, and DList 10 December 2021, 17:02:37 UTC
7df1de5 François Dupressoir 08 December 2021, 19:10:52 UTC First pass: slices are inclusive 09 December 2021, 21:39:05 UTC
32abff2 Christian Doczkal 08 December 2021, 16:05:33 UTC some lemmas on subseq, fmap, and drat 09 December 2021, 06:26:12 UTC
799d429 Christian Doczkal 08 December 2021, 12:53:47 UTC add lemma RO_LRO and generalize RO_FinRO_D 08 December 2021, 13:26:16 UTC
8e47fe3 Pierre-Yves Strub 03 December 2021, 16:11:39 UTC Fix bug that prevents `rewrite //= in h` to simplify in `h` Fix #68 03 December 2021, 16:12:21 UTC
6a6f3b8 Pierre-Yves Strub 03 December 2021, 08:56:41 UTC Merge pull request #105 from EasyCrypt/deploy-lift-lro lift LRO oracle out of FullEager 03 December 2021, 08:56:41 UTC
e77e653 Christian Doczkal 02 December 2021, 17:45:41 UTC lift LRO oracle out of FullEager 03 December 2021, 08:00:10 UTC
fe9a171 Francois Dupressoir 03 December 2021, 05:08:44 UTC Update ci.yml 03 December 2021, 05:09:09 UTC
541aa08 Benjamin Gregoire 02 December 2021, 10:41:39 UTC fix substitution of modules when cloning. fix #97 02 December 2021, 10:41:39 UTC
4a1ce0d François Dupressoir 28 November 2021, 17:26:46 UTC [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 Pierre-Yves Strub 02 December 2021, 06:15:54 UTC PROM: add a ROmap interface for RO + access to the internal map 02 December 2021, 07:48:19 UTC
dda8233 Pierre-Yves Strub 02 December 2021, 07:45:45 UTC CI / Zulip 02 December 2021, 07:46:33 UTC
f66167f François Dupressoir 26 November 2021, 11:56:31 UTC [dune] add abstract theories to install list 26 November 2021, 15:00:50 UTC
b37b762 Pierre-Yves Strub 23 November 2021, 16:58:42 UTC Prototype implementation of a match statement. 23 November 2021, 16:58:42 UTC
f8514a6 Pierre-Yves Strub 22 November 2021, 17:48:42 UTC remove ocamlbuild.ml 22 November 2021, 17:48:42 UTC
50dae1b Pierre-Yves Strub 21 November 2021, 16:30:31 UTC [build] install runtest (as ec-runtest) 21 November 2021, 16:30:31 UTC
3476312 Pierre-Yves Strub 19 November 2021, 10:53:40 UTC script for graphing a dependency graph for .eco 19 November 2021, 10:53:40 UTC
08ed0c2 Pierre-Yves Strub 19 November 2021, 07:18:43 UTC New format for eco (v3) Store whether a theory has been directly required or not. 19 November 2021, 07:18:46 UTC
471ea3b Pierre-Yves Strub 19 November 2021, 07:03:57 UTC foo 19 November 2021, 07:04:08 UTC
a549eb4 Pierre-Yves Strub 19 November 2021, 06:23:34 UTC 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 Pierre-Yves Strub 19 November 2021, 06:09:01 UTC remove \# files 19 November 2021, 06:09:01 UTC
ffe0656 Pierre-Yves Strub 18 November 2021, 14:23:49 UTC 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 Pierre-Yves Strub 18 November 2021, 12:06:18 UTC Add the project name in dune-project This is needed by "dune subst" ref #99 18 November 2021, 12:06:45 UTC
5e3929a Pierre-Yves Strub 18 November 2021, 12:06:09 UTC remove debugging code 18 November 2021, 12:06:09 UTC
17e143c Pierre-Yves Strub 17 November 2021, 15:41:35 UTC 17 November 2021, 15:41:35 UTC
b38a5aa Pierre-Yves Strub 17 November 2021, 15:39:37 UTC 17 November 2021, 15:39:37 UTC
dfb413d Pierre-Yves Strub 17 November 2021, 15:35:07 UTC fix opam package (do not do "dune subst") 17 November 2021, 15:35:07 UTC
0a2d4ad Pierre-Yves Strub 17 November 2021, 07:42:42 UTC [build] use dune to install & find resources 17 November 2021, 08:23:14 UTC
31ce231 François Dupressoir 06 November 2019, 20:46:14 UTC [SmtMap] add has, find and some lemmas these are focused on a specific proof and deserve expanding, fleshing out and cleaning up 17 November 2021, 07:51:50 UTC
229ac7a Pierre-Yves Strub 17 November 2021, 06:24:47 UTC Remove EcFortune 17 November 2021, 06:24:47 UTC
02082bd Pierre-Yves Strub 17 November 2021, 06:22:22 UTC Update copyright 17 November 2021, 06:22:22 UTC
e7d401f Pierre-Yves Strub 17 November 2021, 05:59:48 UTC remove the script for creating tarballs 17 November 2021, 06:01:10 UTC
e46ef74 Pierre-Yves Strub 17 November 2021, 05:57:03 UTC disable warning as errors 17 November 2021, 05:57:03 UTC
a54cec2 Pierre-Yves Strub 17 November 2021, 05:52:23 UTC remove deprecated functions and reenable warning 3 17 November 2021, 05:52:23 UTC
b7a2ee2 Pierre-Yves Strub 17 November 2021, 05:43:59 UTC reenable warning 39 17 November 2021, 05:43:59 UTC
4217836 Pierre-Yves Strub 17 November 2021, 05:41:36 UTC reenable warning 38 17 November 2021, 05:41:36 UTC
061e164 Pierre-Yves Strub 17 November 2021, 05:40:28 UTC reenable warning 35 17 November 2021, 05:40:28 UTC
43a1b9f Pierre-Yves Strub 17 November 2021, 05:39:00 UTC reenable warning 34 17 November 2021, 05:39:17 UTC
5b09921 Pierre-Yves Strub 17 November 2021, 05:34:48 UTC reenable warning 6 17 November 2021, 05:34:48 UTC
003fc41 Pierre-Yves Strub 17 November 2021, 05:34:23 UTC [build] only consider src/theories/examples are deps 17 November 2021, 05:34:23 UTC
df78b65 Pierre-Yves Strub 17 November 2021, 05:34:13 UTC .gitignore (.eca at root) 17 November 2021, 05:34:13 UTC
f8d5b79 Pierre-Yves Strub 16 November 2021, 18:32:37 UTC Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support 16 November 2021, 18:32:37 UTC
e39463d Pierre-Yves Strub 16 November 2021, 17:37:59 UTC .gitignore: cleanup 16 November 2021, 17:37:59 UTC
68bbd4b Pierre-Yves Strub 16 November 2021, 14:59:38 UTC [nix] update dependencies 16 November 2021, 17:35:05 UTC
f7c671c Pierre-Yves Strub 16 November 2021, 14:14:36 UTC [build] use dune in Makefile 16 November 2021, 17:35:05 UTC
5334126 Pierre-Yves Strub 16 November 2021, 13:38:29 UTC [build] do not create an internal EC library we do not currently expose any stable API. 16 November 2021, 17:35:05 UTC
3f13dec Pierre-Yves Strub 16 November 2021, 13:29:42 UTC Use the old build system in opam. 16 November 2021, 17:35:04 UTC
fd804d6 Emilio Jesus Gallego Arias 22 August 2019, 15:33:19 UTC [build] Add basic dune support Add experimental support for buidling `ec` using dune. Use ``` dune build ``` We don't add support for building the stdlib yet. 16 November 2021, 17:35:04 UTC
743a247 Pierre-Yves Strub 16 November 2021, 16:53:15 UTC [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t 16 November 2021, 17:35:04 UTC
4b604bf Christian Doczkal 04 November 2021, 14:52:23 UTC renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 16 November 2021, 17:35:04 UTC
ab62416 Christian Doczkal 24 October 2021, 10:45:16 UTC adapt to consistent use of mu1 16 November 2021, 17:35:04 UTC
15946aa Christian Doczkal 24 October 2021, 09:36:02 UTC use mu1 instead of mass in in Distr 16 November 2021, 17:35:04 UTC
5a0238b Pierre-Yves Strub 16 November 2021, 16:53:15 UTC [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t 16 November 2021, 16:56:20 UTC
ec1f979 Pierre-Yves Strub 09 November 2021, 16:32:05 UTC Merge pull request #88 from EasyCrypt/deploy-mu1 Consistently use `mu1` instead of `mass`. 09 November 2021, 16:32:05 UTC
e770f0f Pierre-Yves Strub 09 November 2021, 15:36:49 UTC Refactor & generalize the section mechanism the section mechanism has been refactored s.t. it provides a more uniform interface where any kind of declaration can be marked as local / declared and erased / generalized when the section is closed. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> 09 November 2021, 15:36:49 UTC
b0e609d Pierre-Yves Strub 05 November 2021, 15:07:43 UTC Fix the pretty printing of \ as a binop fix #93 05 November 2021, 15:08:07 UTC
b37085c Christian Doczkal 04 November 2021, 14:52:23 UTC renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 04 November 2021, 14:56:36 UTC
d5d3d94 Christian Doczkal 24 October 2021, 10:45:16 UTC adapt to consistent use of mu1 04 November 2021, 12:09:30 UTC
6676710 Christian Doczkal 24 October 2021, 09:36:02 UTC use mu1 instead of mass in in Distr 04 November 2021, 12:06:45 UTC
b9c7685 Christian Doczkal 03 November 2021, 15:28:23 UTC comments, renaming, proof* 04 November 2021, 10:00:49 UTC
4da60d2 Christian Doczkal 03 November 2021, 15:06:57 UTC allow sdist-distinguishers for ROs to call sample and set 04 November 2021, 10:00:49 UTC
8a26fe5 Christian Doczkal 03 November 2021, 12:25:10 UTC some more simplifications 04 November 2021, 10:00:49 UTC
6851729 Christian Doczkal 01 November 2021, 10:09:10 UTC remove weight equality side conditions 04 November 2021, 10:00:49 UTC
a21c135 Christian Doczkal 22 October 2021, 14:33:38 UTC implement feedback from review 04 November 2021, 10:00:49 UTC
570f090 Christian Doczkal 21 October 2021, 15:48:19 UTC fix compilation 04 November 2021, 10:00:49 UTC
7fcfa1d Christian Doczkal 21 October 2021, 14:21:07 UTC move lemmas from SDist to RealSeries and Distr, rename summableM 04 November 2021, 10:00:49 UTC
f1d2f19 Christian Doczkal 21 October 2021, 09:05:24 UTC use PROM rather than ROM 04 November 2021, 10:00:49 UTC
051cb1d Christian Doczkal 20 October 2021, 15:24:05 UTC sdist for ROM distinguishers and N distinct queries 04 November 2021, 10:00:49 UTC
f5d072e Christian Doczkal 19 October 2021, 17:49:56 UTC reduction from N to 1 oracle call for sdist distinguisher 04 November 2021, 10:00:49 UTC
3adc9c8 Christian Doczkal 18 October 2021, 16:11:21 UTC sdist distinguisher for single oracle call + reduction to single sampling 04 November 2021, 10:00:49 UTC
62e1ce7 Christian Doczkal 14 October 2021, 12:55:45 UTC connection between sdist and distinguisher procedures 04 November 2021, 10:00:49 UTC
4529cfc Christian Doczkal 12 October 2021, 12:10:25 UTC statitical distance and some lemmas 04 November 2021, 10:00:49 UTC
aa6dc07 Pierre-Yves Strub 19 October 2021, 10:19:36 UTC Add a simple form of pattern selection in rewrite rules Syntax is: `rewrite [pattern]rule` In this form, `pattern` is first searched against the current goal and rule LHS is then matched against the instanciated pattern. E.g. `rewrite [y+_]addrC` will instantiate `addrC` to `y` and `z` assuming that the first match of `y+_` in the current goal is `y+z`. This syntax is compatible with other variants: `rewrite -{2}[y+_]addrC` 19 October 2021, 10:19:36 UTC
4afdfe9 Pierre-Yves Strub 18 October 2021, 12:51:49 UTC change "smt in rewrite" syntax New syntax is: - rewrite #smt - rewrite #smt:(db) - rewrite #smt:[options] 18 October 2021, 12:52:42 UTC
7b8aa43 Pierre-Yves Strub 18 October 2021, 08:03:55 UTC Compute free program variables in *hoare statements. Fix #83 18 October 2021, 08:03:55 UTC
c854989 Pierre-Yves Strub 12 October 2021, 13:39:31 UTC Implement "gen have" & "wlog suff" Fix #77 12 October 2021, 13:39:31 UTC
c132a25 Pierre-Yves Strub 08 October 2021, 12:09:27 UTC StdLib: summability of partitioning 08 October 2021, 12:09:35 UTC
back to top