https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
f47fb53 better with the files 26 November 2019, 07:51:24 UTC
dc9e664 attempt to chacha-poly 26 November 2019, 07:50:49 UTC
8134d1a fix 16 September 2019, 15:56:04 UTC
4af3bf7 Merge branch '1.0' into deploy-fmatch 16 September 2019, 15:11:06 UTC
67392e1 RndProd : random oracle of a dprod 16 September 2019, 12:56:20 UTC
a8e2f10 Fix defered start of provers 15 September 2019, 16:59:56 UTC
7641f4a merge RndO and PROM 13 September 2019, 14:21:19 UTC
2e91082 old modifications 13 September 2019, 12:56:12 UTC
3d66517 import DHIES 13 September 2019, 11:17:04 UTC
2c5203d more on lists (assoc, onth) + some facts on fmap/assoc 13 September 2019, 11:01:20 UTC
13b7bdd add PKSMK 13 September 2019, 09:49:36 UTC
3bbc09b add AEAD 13 September 2019, 09:39:56 UTC
746d64c Revert "remove duplicate lemma get_none -> domNE" This reverts commit 60d29c1f11f6c79824022608f9f83503d983ce61. 13 September 2019, 08:30:58 UTC
0344765 djoin and al 13 September 2019, 08:20:36 UTC
60d29c1 remove duplicate lemma get_none -> domNE 13 September 2019, 06:39:19 UTC
0e717db pre/post selector Syntax if #rg?name where `name` is either `pre` or `post` and `rg` is a list of filters. 12 September 2019, 21:18:52 UTC
806fa6b Fix compilation 12 September 2019, 20:57:15 UTC
2dd053c add assumption 12 September 2019, 20:35:16 UTC
7fb964c add generalized oracle Diffie-Hellman assumption 12 September 2019, 20:35:16 UTC
350728b add hash colision resistant assumption 12 September 2019, 20:35:16 UTC
0f3ebba dlet-sampling : distr are now parameters 12 September 2019, 19:10:51 UTC
65e3d88 eqv between dlet-sampling and seq-sampling 12 September 2019, 14:21:46 UTC
6ec8512 fix trivial error 12 September 2019, 12:26:49 UTC
786cb63 Add generic Lazy/Eager for random oracle 12 September 2019, 12:18:29 UTC
e5efb23 Refactor and kill all admits related to distributions and infinite sums. 06 September 2019, 13:48:52 UTC
60b76e8 Try to remove exponential behavior 05 September 2019, 09:05:32 UTC
2e3a618 use abstract theory 04 September 2019, 13:31:51 UTC
84dc271 remove unused variable 04 September 2019, 07:11:42 UTC
132aa51 Add few lemmas 03 September 2019, 14:35:01 UTC
0a6c7f8 Proving probability equal to 1/2 using prhl 03 September 2019, 08:55:55 UTC
a4fb49d fix Why3 literals comparisons [fix #17394] 04 August 2019, 19:07:17 UTC
af281fd Do eta-expansion for fix-match branches [fix #17385] 02 August 2019, 20:16:22 UTC
43ac3f3 Fix bug in subst of type definition (parameters were not substituted) 22 July 2019, 16:54:24 UTC
a9666b1 user error message for FXE_CtorInvalidArity [fix #17387] 06 July 2019, 22:07:21 UTC
af25c22 Bug fixing in phl ([closes #17380]) 19 June 2019, 13:28:03 UTC
fc8d388 Move to Why3 1.x 11 June 2019, 09:59:50 UTC
43e5a65 some cleaning 04 June 2019, 12:45:24 UTC
fbd3468 simple fix for Zand when empty 04 June 2019, 12:33:29 UTC
9dbfd56 some fix 04 June 2019, 12:29:49 UTC
0e9b41e fmatching and genregexp are mutually recursive 04 June 2019, 11:44:48 UTC
679f333 run-test: add a -timing option 17 May 2019, 05:46:17 UTC
a79235c add an option [-tstats FILE] for recording timing statistics 17 May 2019, 05:34:41 UTC
e522b67 runtest: python2 -> python3 01 May 2019, 07:37:32 UTC
f293e76 Towards fixing XDG-based config 16 April 2019, 16:18:33 UTC
bfa4f3e . 08 April 2019, 10:36:40 UTC
ce2ceb7 . 02 April 2019, 07:32:37 UTC
27c1df3 Allow : t1 || t2 || ... || tn 28 March 2019, 05:41:39 UTC
9ae843f Second try. Still does not work. 27 March 2019, 16:48:30 UTC
82c7541 First try. Does not work. 27 March 2019, 15:34:44 UTC
41219ef add reduction of Int div/mod by reduction of edivz + bind symbol to Why3 26 March 2019, 13:42:33 UTC
a041441 Add congruence rule for projections 26 March 2019, 13:32:42 UTC
5e9f955 Extend matching (projections) 26 March 2019, 10:46:03 UTC
8a0c097 Bind auto-conseq in eqobsin 26 March 2019, 09:59:05 UTC
b481f98 "call L" automatically applies "L" to "_" when needed. 25 March 2019, 12:03:45 UTC
1fb57b6 fix reduction of fixpoints with extra arguments 25 March 2019, 08:07:17 UTC
0a33156 try to convert closed pattern before failing... 24 March 2019, 09:08:50 UTC
16d3bf4 23 March 2019, 18:47:22 UTC
3515767 23 March 2019, 18:38:20 UTC
6c91e46 23 March 2019, 18:29:13 UTC
091db62 fix crypto/rom/Lazy.eca script (after fixing fun_ext) 22 March 2019, 16:44:17 UTC
19680a9 fix eta 22 March 2019, 16:34:18 UTC
972a0fa fix eta-reduction/eta-extension 22 March 2019, 16:02:09 UTC
5cb65da fix computing of free variables in patterns 22 March 2019, 15:22:15 UTC
da94e33 correct version of fun_ext to match the one in 1.0 22 March 2019, 14:13:43 UTC
8ee2bc5 . 22 March 2019, 14:01:16 UTC
70e1b67 4 bugs left 19 March 2019, 14:42:29 UTC
dd4d51a managing restrictions about mhr 19 March 2019, 14:02:52 UTC
86fce7d test 19 March 2019, 13:37:41 UTC
2babf50 fix last commit 19 March 2019, 13:27:25 UTC
5d1bb0f change reduction continuations 19 March 2019, 13:15:51 UTC
ef5eaa2 allow use of mhr 19 March 2019, 11:40:34 UTC
b80c242 fix infinite loop 19 March 2019, 10:18:17 UTC
9f349d7 fix matching same meta 19 March 2019, 09:29:59 UTC
42bee10 fix reduction 18 March 2019, 14:57:22 UTC
d5ccd83 fix reduction 18 March 2019, 12:21:32 UTC
b2b6502 fix reduction 18 March 2019, 10:14:38 UTC
530ccdd fix reduction of (=) 18 March 2019, 09:33:39 UTC
e8d6aef fix reductions 18 March 2019, 09:21:49 UTC
6019ae3 fix infinite loop 14 March 2019, 16:51:48 UTC
9031f24 no reduction in args of logical application 14 March 2019, 16:11:26 UTC
36b321b Merge branch 'deploy-fmatch' of https://github.com/EasyCrypt/easycrypt into deploy-fmatch 14 March 2019, 15:10:11 UTC
b583880 modify verbose 14 March 2019, 15:09:59 UTC
17d07ee 14 March 2019, 15:03:19 UTC
89bf6be add verbose to ecPReduction 14 March 2019, 10:35:10 UTC
c2b2381 add EcFMatching.search_eng_head_no_delta 13 March 2019, 10:01:01 UTC
67f51b9 hide ecFmatching types 11 March 2019, 16:30:29 UTC
4f92c1b fix bug 11 March 2019, 15:33:21 UTC
7821071 fix stack overflow 11 March 2019, 12:21:15 UTC
a221d83 fix order of reduce tries 07 March 2019, 16:04:49 UTC
188f91f bug fix 07 March 2019, 12:47:49 UTC
b289db5 fix bugs 07 March 2019, 12:18:57 UTC
8d9152d bug fixes 07 March 2019, 10:23:15 UTC
012a2b1 fix bug in p_subst when pat_local 07 March 2019, 10:00:37 UTC
26e0600 menv_is_full now checks if unienv is closed 07 March 2019, 09:47:39 UTC
d851a97 forgot to add ecPReduction 06 March 2019, 17:12:58 UTC
979e9bc . 06 March 2019, 17:08:33 UTC
d2845bc fix higher order 06 March 2019, 14:19:31 UTC
9e3d6df restrict higher order case when higher order unification is decidable. 06 March 2019, 13:45:15 UTC
4aaf661 fix eta-reduction 06 March 2019, 10:12:22 UTC
04e9c66 fix simplification of Int(+) and Real.(+) 05 March 2019, 17:17:26 UTC
back to top