https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
acfd4ea Definition of quotient types w.r.t. a equivalence relation 16 April 2020, 14:56:46 UTC
60a7d34 Finite groups, cyclic groups, Bezout. 16 April 2020, 13:19:53 UTC
cdb2e6f Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' 16 April 2020, 10:45:54 UTC
f44260c stdlib: distributions: dmap1E_can 16 April 2020, 09:41:06 UTC
94786bc stdlib: List: nth_default 16 April 2020, 09:40:44 UTC
136b237 lemma: fun_ext2 15 April 2020, 09:39:30 UTC
5eba66b allow writing m.[i, j] in place of m.[(i, j)] 15 April 2020, 09:31:23 UTC
4882379 views: allow application of induction principle as a view 15 April 2020, 08:28:48 UTC
64d592d elim: search quantifier modulo reduction 15 April 2020, 08:19:54 UTC
3b8b038 Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> 14 April 2020, 15:08:58 UTC
f3581d5 binomial coefficients 10 April 2020, 09:56:42 UTC
21e8fce CI: move to slack notification 09 April 2020, 16:21:20 UTC
d41a34d Matching for *hoareF & Pr 09 April 2020, 13:44:05 UTC
4062085 Merge pull request #40 from CohenCyril/nixfix default.nix: adding installFlags 09 April 2020, 13:39:11 UTC
21354f7 default.nix: adding installFlags 08 April 2020, 15:23:25 UTC
149b09f User error message for map-style lvalue on unsupported assignment [fix #17412] 28 March 2020, 08:13:21 UTC
b1b35e6 Internal: remove LvMap lvalue. 26 March 2020, 19:52:54 UTC
1a8d60a Revert "better conversion + simplify reduction algorithm." This reverts commit 11a875951d0f94381b22b362ddf8b0cc18f77886. 26 March 2020, 18:26:21 UTC
2a5b4f6 Only accepts Alt-Ergo from version 2.3.1 26 March 2020, 07:42:17 UTC
22799f1 In `rewrite`, use a keyed matching algorithm for finding occurences. 28 February 2020, 06:49:27 UTC
10b9097 drop python2 support 15 February 2020, 09:20:51 UTC
44b23b5 Allow operators of the form 'n where n is a *fixed* natural number 15 February 2020, 07:19:25 UTC
11a8759 better conversion + simplify reduction algorithm. 14 February 2020, 08:36:31 UTC
4f587f3 "hint simplify [reduce]" does one head reduction for finding the quantifers 13 February 2020, 09:06:03 UTC
2bbf3d3 Add new options to 'hint simplify': - reduce: equations are found up-to reduction - eqtrue: if no equations can be found, add a equation of the form (e = true) 13 February 2020, 08:38:38 UTC
2efb9e7 Consolidate PRP and PRF libraries Including weak PRP-PRF switching lemma, but not its strong version Squashed commit of the following: commit 005342f19a55b0ae01c88c0c729fdbad3f2519ff Merge: 5407570b 7325ae6d Author: François Dupressoir <fdupress@gmail.com> Date: Mon Feb 10 09:48:54 2020 +0000 Merge branch '1.0' into deploy-simpler-rp commit 5407570bbdeaee7b725f57fcdbbf764ff301ac9e Author: François Dupressoir <fdupress@gmail.com> Date: Fri Jan 24 12:00:21 2020 +0000 move towards merging PRF and RO also clean assignment notation commit 65e0c4eb8c702729500148e34900dc5971e583a7 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 14:14:29 2020 +0000 Integrate PRP-PRF switching lemma into PRP lib Not done for the strong version yet commit 456a7c96e40fa6827d92fbc36d8cd75fdd8abab1 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:40:25 2020 +0000 Simplifying the PRF interface No keys are needed for the ideal RP, The raw interface can be defined separately as needed. commit e7dea73e6eae21f192efc45f42e9cdc9e5ec4eb8 Author: François Dupressoir <fdupress@gmail.com> Date: Tue Jan 21 09:19:04 2020 +0000 Some nits commit 8bb90549b6084ea8189e3a4067a155f977ccd34a Author: François Dupressoir <fdupress@gmail.com> Date: Mon Jan 20 16:38:30 2020 +0000 Cleanup PRP/PRF and PRP-PRF 10 February 2020, 09:50:13 UTC
7325ae6 Refactor PlugAndPray 10 February 2020, 09:45:08 UTC
9e11412 Generalize arguments about sampling in dexcepted This pushes several complex low-level arguments related to sampling in restricted distributions into the related distribution file. This also generalizes these arguments, so that: - TwoStepSampling no longer requires a full distribution, - WhileSampling takes distributions and tests as procedure arguments rather than clone parameters. Specialized versions of theories and lemmas that reproduce the old behaviours are also included. The Dice_Sampling theory is removed, replaced with Dexcepted.WhileSamplingFixedTest (an abstract theory). Squashed commit of the following: commit e4bf1725f2a327bc58dda51d0079acb8dbb8fb1a Author: François Dupressoir <fdupress@gmail.com> Date: Thu Jan 16 20:40:23 2020 +0000 trailing white space in modified files commit 12d5ff0ae8607be10f7e925d1f0d44dd8e78dbde Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 15:49:41 2019 +0000 minor cleanup commit 7921a24e13e9f6d19ad02c0a22e8efb49bc37184 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 19 13:47:19 2019 +0000 More general ways of sampling out of a predicate TwoStep no longer requires losslessness. More sharing of proof could be obtained commit 393700f85b47b9d373be983b1451b08ae3d3be94 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:40:16 2019 +0000 PRP<->PRF uses generic resampling commit 74b9aef924cc313e358510ab9f83bc7410489db4 Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 21:27:12 2019 +0000 Slight generalization: no longer need a full distribution commit 0853fc0e313bb6adac0ad956417480ebd70f512f Author: François Dupressoir <fdupress@gmail.com> Date: Thu Dec 5 18:34:43 2019 +0000 Dexcepted: equivalence between two ways of sampling used in PRP<->PRF, but also in a current proof TODO: make PRP<->PRF use this 16 January 2020, 20:48:25 UTC
cd341ca [done] solves context of the form [false |- G] [fix 17270] 18 December 2019, 09:52:45 UTC
050cada Remove dead code in 't_solve' 18 December 2019, 09:52:45 UTC
1ec24f8 Improve />. Be sure that tactic crush (|>, />) does not transform the goal into umprovable one. 18 December 2019, 07:48:19 UTC
eb9d7e3 fix DHIES 10 December 2019, 17:19:16 UTC
7c400bd fixing examples 10 December 2019, 15:36:45 UTC
943b847 Merge remote-tracking branch 'origin/1.0' into deploy-simple-stuff 10 December 2019, 14:36:33 UTC
3acf93f fixing some examples 10 December 2019, 14:35:50 UTC
47c0851 Fix parser 10 December 2019, 14:34:52 UTC
0d33668 Printers for rewrite & solve databases 10 December 2019, 14:00:13 UTC
0b1128e add lemma in "random" database 10 December 2019, 12:38:29 UTC
babbac3 Rename internal tactic t_auto into t_solve 10 December 2019, 12:33:05 UTC
e6c9905 improve automatic simplification of rnd rule for equiv 10 December 2019, 12:29:05 UTC
5d09cc2 improve t_auto internal tactic 10 December 2019, 12:28:10 UTC
2b2b5b8 automatically remove lossless condition in rnd{i} 09 December 2019, 15:43:32 UTC
fa8b38b add simplification rule for oget_some, oget_none 07 December 2019, 09:46:33 UTC
89e35d1 Compiles with OCaml 4.07 -> 4.09 (tested) 05 December 2019, 19:54:02 UTC
132968e remove failing SMT 02 December 2019, 10:06:01 UTC
60cfeb4 More results on dlet / dprod 02 December 2019, 09:16:55 UTC
de1d4dc Fix bug in eager if 29 November 2019, 07:56:52 UTC
78e8f6e 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> 26 November 2019, 13:31:58 UTC
add72dc 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 14 November 2019, 10:15:31 UTC
e58c36a add the full PRG tutorial from FOSAD (#35) 07 November 2019, 16:19:02 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
back to top