https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
3671d46 Travis -> CircleCI 18 December 2020, 20:07:48 UTC
35e59d1 `apply` is now using product-compatible matching 04 December 2020, 14:05:15 UTC
6504b04 remove debug infos 03 December 2020, 13:55:10 UTC
3c14f4d small refactoring 03 December 2020, 07:08:30 UTC
177f61d add trivial lemma 03 December 2020, 05:53:30 UTC
e7ca052 stack based conversion 02 December 2020, 15:08:03 UTC
93748b3 Decimal numbers are now translated to irreducible fractions 01 December 2020, 09:41:56 UTC
de9fdea In pose/trivial: use less conversion, cleanup chain of trivial calls. 01 December 2020, 08:48:33 UTC
68b3ffa make congr less costly 27 November 2020, 16:47:34 UTC
ea13c71 simplify t_split 27 November 2020, 16:46:54 UTC
2363562 fix cbv user_red 24 November 2020, 19:47:13 UTC
6857723 simplify user reduction 24 November 2020, 13:49:28 UTC
fcdfcbd Core theory for univariate polynomials 21 November 2020, 12:11:49 UTC
a08bc34 Stdlib: more results on Rn + bigops on Rn 21 November 2020, 08:29:35 UTC
7a42484 MANIFEST 21 November 2020, 00:14:50 UTC
07b937c Small addititions on distributions 20 November 2020, 22:16:40 UTC
6f68e27 More results on distributions (conditional exp, Jensen (finite)) 20 November 2020, 14:45:54 UTC
27ff637 integrating more results on distributions 18 November 2020, 06:00:50 UTC
8d01a80 fix CBC 17 November 2020, 17:48:08 UTC
ed25190 small generalization of PRP 16 November 2020, 10:58:31 UTC
8cb3e88 extend conseq rules: equivF => hoareF => hoareF and equivF => phoareF => phoareF 13 November 2020, 11:33:47 UTC
4391b04 basic results about minr 12 November 2020, 11:00:16 UTC
61de4b9 Fix "smt debug" 12 November 2020, 08:24:20 UTC
b360fa8 Fix bug in conseq 11 November 2020, 05:56:42 UTC
ffad375 New option for SMT: "debug" 03 November 2020, 09:04:00 UTC
4ef4286 Fix dfold s.t. the functor takes the index 21 October 2020, 08:49:24 UTC
19c7285 New operator: dfold 20 October 2020, 09:40:14 UTC
fa3853d README (nix) 15 October 2020, 10:30:04 UTC
bc4f6df "={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..." 15 October 2020, 08:39:16 UTC
22a8b51 better printing of modules bodies w.r.t. "import var" 14 October 2020, 09:10:10 UTC
ca1f0d2 The command "import var" is now allowed at top-level 14 October 2020, 07:08:46 UTC
b34c174 add alias "include var" that stands for "include" then "import var" 14 October 2020, 06:55:56 UTC
c3114bd "import var" now takes a space-separated list of modules 14 October 2020, 06:52:22 UTC
4268b0f New command in modules: import var M This imports the variables of M in the active module scope. 14 October 2020, 06:34:14 UTC
7ba9ba4 Docker image: bump provers versions 11 October 2020, 07:27:44 UTC
7d8a513 Help smt along in brittle proofs These SMT fail when using: - Why3 1.3.1 - Z3 4.8.9 - CVC4 1.9 - Alt-Ergo 1.3.3 This appears to be bad interplay between the provers and this version of Why3: the proofs work with Why3 1.2 10 October 2020, 12:08:14 UTC
469a12a easycrypt why3config uses --full-config 09 October 2020, 16:20:54 UTC
ef6f0ba README: add --full-config option (why3 config) 09 October 2020, 15:44:59 UTC
6d31cc5 Update Dockerfile w.r.t new EasyCrypt repo layout 09 October 2020, 15:44:32 UTC
e664da3 Docker: do not use easycrypt remote anymore 09 October 2020, 11:02:44 UTC
ce70fa4 opam: change post-install message 09 October 2020, 10:23:24 UTC
6c03840 Fix travis configuration file w.r.t recent changes 09 October 2020, 10:21:16 UTC
44a728a Update README (no more external opam repo) & add missing opam fields 09 October 2020, 10:16:58 UTC
e37a10c Import opam file s.t. travis can use it to update its dependencies 09 October 2020, 08:41:05 UTC
c436fd4 Travis: update EasyCrypt dependencies before running tests 09 October 2020, 08:41:05 UTC
730f329 default.nix: remove restriction on Why3 version 09 October 2020, 08:41:05 UTC
8f33b95 First attempt at handling Why3 1.3.X 09 October 2020, 08:41:05 UTC
3007982 fix default.nix 14 September 2020, 13:36:41 UTC
d750dc3 Fix merge problem 15 June 2020, 15:10:39 UTC
66c830f Clean up the ROM libraries Now reduced to PROM as core, with ROM as a simpler interface. PROM is concrete to allow reuse of its flag type. Its internal theories, and ROM, are abstract to avoid growing forests of clones when using eager arguments. ROM now aligns with PROM in cloning interface: additional types `d_in_t` and `d_out_t` specify the distinguisher's interface. (This simplifies instantiation.) Some changes to type and oracle names to make them more explicit. Notably: - `from` is now `in_t`, - `to` is now `out_t`, (with associated change on name of distribution). 15 June 2020, 14:55:33 UTC
734e5bb Do no search for rewriting patterns modulo conversion. 10 June 2020, 17:03:25 UTC
41d0d08 Theory on square matrices (up to ring structure) `unit` predicate is still abstract. The link with the determinant has still to be done. 10 June 2020, 14:44:03 UTC
4b965ee Fix compilation 10 June 2020, 14:13:50 UTC
c9641e4 Revert "Add user reductions for iteri" This reverts commit f693233ec9a7b33ba350d7b17e1d223f33d7fb56. 10 June 2020, 09:53:35 UTC
bacb90b in rewrite find occurences using alpha conversion first. 10 June 2020, 09:41:40 UTC
ab61883 add reduction for -i = i' 10 June 2020, 07:47:46 UTC
19c6c50 remove duplicate declaration 10 June 2020, 07:47:46 UTC
6965ea6 binomial law + basic lemmas (full / support) 10 June 2020, 07:46:26 UTC
2064617 "search" now works with notations [fix #17317] 10 June 2020, 07:28:49 UTC
763732a smt: do not filter wanted lemma 09 June 2020, 15:43:43 UTC
f693233 Add user reductions for iteri 09 June 2020, 15:39:58 UTC
23b938a Refactor & merge min/max & integer/real pow. Co-Authored-By: Benjamin Gregoire <benjamin.gregoire@inria.fr> Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu> 09 June 2020, 11:33:32 UTC
f71bd6c Some extra lemmas on Ring.expr Co-Authored-By: Benjamin Gregoire <benjamin.gregoire@inria.fr> Co-Authored-By: Pierre-Yves Strub <pierre-yves@strub.nu> 08 June 2020, 17:14:32 UTC
00ffc11 add lemmas on bigi 27 May 2020, 13:11:27 UTC
53ed919 Allows nosmt with all operators other than pure, abstract ones - i.e., with plain, axiomatized (including : {t | phi} as ax) and cases operators. When cloning, [op nosmt x = ...] is allowed, but nosmt can't be used with inlining mode. 26 May 2020, 08:38:14 UTC
170c443 fix default.nix 27 April 2020, 12:23:05 UTC
58aaed4 Merge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec 20 April 2020, 17:02:04 UTC
ce4d827 Added two useful lemmas to Quotient.ec 20 April 2020, 15:04:39 UTC
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
back to top