https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
eaa7592 Fix bug in eager if 29 November 2019, 13:20:36 UTC
6f83852 Work of Roberto Metere on Sigma Protocols: - formalisation of the discrete logarithm assumption - formalisation of generic commitment schemes - formal verification of the Pedersen commitment scheme - formalisation of generic Sigma protocols - Sigma Protocol example: the Schnorr proof of knowledge Co-authored-by: Roberto Metere <r.metere2@ncl.ac.uk> 29 November 2019, 13:20:36 UTC
3f5c47d Squashed commit of the following: [closes #17403] commit 55d4c60f675f8baf509682dd12e817377ba682e9 Author: Pierre-Yves Strub <pierre-yves@strub.nu> Date: Thu Nov 14 10:30:54 2019 +0100 Regeneralization of unspecified arguments in applicative views 29 November 2019, 13:20:36 UTC
9c8cdb0 add the full PRG tutorial from FOSAD (#35) 29 November 2019, 13:20:36 UTC
ac72951 [SmtMap] add has, find and some lemmas these are focused on a specific proof and deserve expanding, fleshing out and cleaning up 06 November 2019, 20:46:14 UTC
e53aab7 Check .eco after the loader has been configured [fix #17400] 25 October 2019, 15:59:33 UTC
6489ade Make ECO handling more robust - do not fail when an .eco file is invalid - fix the reading of the `version' flag - erase staled .eco file - do not accept to compile files not handing with .ec or .eca - API: .mli file for EcEco [fix #17398] 25 October 2019, 06:46:13 UTC
10b2ab0 Add EC hash to .eco 18 October 2019, 08:36:08 UTC
51f8ab0 .gitignore: .eco 18 October 2019, 08:11:34 UTC
f38226c Generate and use .eco files. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr> 17 October 2019, 10:08:11 UTC
1c35db0 Fix t_auto. (was pruning opened goals) 16 October 2019, 09:09:32 UTC
2139beb CI: test 1.0-preview 15 October 2019, 07:46:58 UTC
2f6587f In `case`, normalized 'glob' when searching for an inductive type. [fix #17391] 15 October 2019, 07:09:54 UTC
74207ab Remove debugging infos 14 October 2019, 15:22:16 UTC
e023995 New option from inline: [tuple]. Allows no to not use tuple assignments. 14 October 2019, 12:27:51 UTC
a38b2e9 Fix handling of abstract theories imports. 14 October 2019, 12:05:09 UTC
e12e2c2 This commit introduces two major features. - call by value reduction strategy. - user defined reduction rules. Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> Co-authored-by: Benjamin Gregoire <benjamin.gregoire@inria.fr> 14 October 2019, 08:39:46 UTC
651df3f Solve tactic: apply is now done modulo delta 14 October 2019, 08:24:30 UTC
e77d659 Misc. in SmtMap.ec 14 October 2019, 07:45:06 UTC
297f528 Add interleave tactic 14 October 2019, 07:10:05 UTC
ce9380d Add transitivity * (transivity with generation of VC) 14 October 2019, 06:42:35 UTC
3b9667b Pragmas for printing pre/post as a list of their resp. conjunctions Pragmas are: PrPo:{pr,po}:{raw,ands} (Pragma system has been revamped by this commit) 14 October 2019, 06:27:33 UTC
66e7f99 Add decimal literals 14 October 2019, 05:55:27 UTC
115229e New intro pattern: [#|]. [#|] is a multi-case i-p (like [#]) that works also on on disjunctions. 14 October 2019, 05:19:52 UTC
1f45fde refactor flagged map && PROM (#22) 10 October 2019, 11:50:05 UTC
da0b25a Some extra lemmas on nseq (#26) 10 October 2019, 07:49:06 UTC
408d1b0 Add a more general version of dmap_uni (#30, #33) 10 October 2019, 07:19:29 UTC
e9598be Add lemmas to filter noncontributing list items in bigops (#29) 10 October 2019, 06:50:06 UTC
8eb2491 Critical bugfix on dot-product (#34) * Critical bugfix on dot-product * CauchySchwarz is now an abstract theory 09 October 2019, 19:14:57 UTC
c8257d3 Namespace for libraries and th. renaming 02 October 2019, 06:23:52 UTC
f2bcd42 README: add a note about installing external deps for provers 01 October 2019, 20:12:36 UTC
b6a4d3a Docker: bump Z3 version 01 October 2019, 19:49:59 UTC
4860685 Fetch more up-to-date smt binaries & compress unnecessary layers 01 October 2019, 10:54:42 UTC
88ded1b Fix "n?" intro pattern. 17 September 2019, 11:28:41 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
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
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
27c1df3 Allow : t1 || t2 || ... || tn 28 March 2019, 05:41:39 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
4387903 Fix pretty printing of records projectors (when applied) 28 January 2019, 13:48:44 UTC
9c1fdfb Reduction fix: reduces record projections when applied. 28 January 2019, 13:40:40 UTC
a893051 add missing quantification over memory in async while 17 January 2019, 17:22:08 UTC
337a8ab fix a smt call 20 December 2018, 14:25:05 UTC
b2b7e5b fix List.ec 20 December 2018, 13:13:35 UTC
532e12b fix types of an operator when its definition is a match, where its type was only its return type inside its body. 20 December 2018, 12:28:06 UTC
192a23f fix type of pred1 from 'a -> bool to 'a -> 'a -> bool 19 December 2018, 17:24:55 UTC
0b59cac fix bug in LDecl where the type of the operator was not correct. 18 December 2018, 14:35:55 UTC
88a87da Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0 17 December 2018, 14:33:18 UTC
dfe37eb fix bug where the type of pred1 was bool instead of 'a -> bool 17 December 2018, 14:32:33 UTC
5a31709 simplify proof 12 December 2018, 17:00:34 UTC
17eced8 Simplifying async-while examples 11 December 2018, 16:29:13 UTC
2d05f8b async-while: example for nested loops 11 December 2018, 16:24:53 UTC
ed7bf6c (internal API) - typed application soft-constructor for forms 03 December 2018, 12:40:04 UTC
f120f53 fix error message 13 November 2018, 08:12:18 UTC
9959602 More results in ZModP 07 November 2018, 21:51:34 UTC
5c95527 New tactic: - exlim (shorthand for exists*; elim*) - ecall (seq + exlim + call with inference) 07 November 2018, 21:47:02 UTC
28c5228 Fix Cramer Shoup 25 October 2018, 15:21:38 UTC
672c36d weaken axiom 25 October 2018, 14:38:06 UTC
5b694ae add some lemma 25 October 2018, 07:14:05 UTC
9d34c3b README 25 September 2018, 16:48:02 UTC
6b07f83 Extend SmtMap theory with new results. Co-authored-by: Alley Stoughton <alley.stoughton@icloud.com> 20 September 2018, 09:37:23 UTC
92effbe adding joint operator (+) and its lemmas (#21) 18 September 2018, 16:03:04 UTC
5cbf6f1 better simplification of int/real addition Expressions of the form (x + c1) + c2 are now simplified to (x + [c1+c2]) (modulo commutativity of (+). 17 September 2018, 11:33:37 UTC
back to top