c987761 | Pierre-Yves Strub | 11 October 2020, 07:27:44 UTC | Docker image: bump provers versions | 20 October 2020, 09:34:59 UTC |
66784bc | Vitor Pereira | 12 October 2020, 23:02:09 UTC | Merge branch '1.0-preview' of https://github.com/EasyCrypt/easycrypt into HEAD | 12 October 2020, 23:02:09 UTC |
97ebd49 | Vitor Pereira | 12 October 2020, 23:00:34 UTC | version update | 12 October 2020, 23:00:34 UTC |
f8ea221 | François Dupressoir | 10 October 2020, 12:10:17 UTC | Merge branch '1.0' into 1.0-preview | 10 October 2020, 12:10:17 UTC |
7d8a513 | François Dupressoir | 10 October 2020, 11:22:49 UTC | 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 |
221e1b2 | François Dupressoir | 10 October 2020, 10:47:31 UTC | Merge branch '1.0' into 1.0-preview | 10 October 2020, 10:47:31 UTC |
933e315 | Pierre-Yves Strub | 10 October 2020, 10:34:11 UTC | Merge branch '1.0' into 1.0-preview | 10 October 2020, 10:34:11 UTC |
469a12a | François Dupressoir | 09 October 2020, 16:20:54 UTC | easycrypt why3config uses --full-config | 09 October 2020, 16:20:54 UTC |
ef6f0ba | Pierre-Yves Strub | 09 October 2020, 15:44:59 UTC | README: add --full-config option (why3 config) | 09 October 2020, 15:44:59 UTC |
6d31cc5 | Pierre-Yves Strub | 09 October 2020, 15:44:32 UTC | Update Dockerfile w.r.t new EasyCrypt repo layout | 09 October 2020, 15:44:32 UTC |
e664da3 | Pierre-Yves Strub | 09 October 2020, 11:02:44 UTC | Docker: do not use easycrypt remote anymore | 09 October 2020, 11:02:44 UTC |
ce70fa4 | Pierre-Yves Strub | 09 October 2020, 10:23:24 UTC | opam: change post-install message | 09 October 2020, 10:23:24 UTC |
6c03840 | Pierre-Yves Strub | 09 October 2020, 10:21:16 UTC | Fix travis configuration file w.r.t recent changes | 09 October 2020, 10:21:16 UTC |
44a728a | Pierre-Yves Strub | 09 October 2020, 10:16:24 UTC | Update README (no more external opam repo) & add missing opam fields | 09 October 2020, 10:16:58 UTC |
e37a10c | Pierre-Yves Strub | 09 October 2020, 08:12:15 UTC | Import opam file s.t. travis can use it to update its dependencies | 09 October 2020, 08:41:05 UTC |
c436fd4 | Pierre-Yves Strub | 09 October 2020, 07:16:05 UTC | Travis: update EasyCrypt dependencies before running tests | 09 October 2020, 08:41:05 UTC |
730f329 | Pierre-Yves Strub | 09 October 2020, 08:02:28 UTC | default.nix: remove restriction on Why3 version | 09 October 2020, 08:41:05 UTC |
8f33b95 | Stephane Graham-Lengrand | 07 October 2020, 23:19:47 UTC | First attempt at handling Why3 1.3.X | 09 October 2020, 08:41:05 UTC |
3007982 | Benjamin Gregoire | 14 September 2020, 13:36:41 UTC | fix default.nix | 14 September 2020, 13:36:41 UTC |
d3fc323 | François Dupressoir | 15 June 2020, 15:10:39 UTC | Fix merge problem | 16 June 2020, 09:51:05 UTC |
d750dc3 | François Dupressoir | 15 June 2020, 15:10:39 UTC | Fix merge problem | 15 June 2020, 15:10:39 UTC |
66c830f | François Dupressoir | 15 June 2020, 14:55:33 UTC | 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 |
25bcf42 | Pierre-Yves Strub | 10 June 2020, 17:05:57 UTC | Merge branch '1.0' into 1.0-preview | 10 June 2020, 17:05:57 UTC |
86a9bf3 | Pierre-Yves Strub | 10 June 2020, 17:05:33 UTC | Merge branch 'deploy-rewrite' into 1.0-preview | 10 June 2020, 17:05:33 UTC |
734e5bb | Pierre-Yves Strub | 10 June 2020, 17:03:25 UTC | Do no search for rewriting patterns modulo conversion. | 10 June 2020, 17:03:25 UTC |
7c9f3ad | Pierre-Yves Strub | 10 June 2020, 16:51:38 UTC | Merge branch '1.0' into deploy-rewrite | 10 June 2020, 16:51:38 UTC |
13b70b3 | Pierre-Yves Strub | 10 June 2020, 16:28:11 UTC | | 10 June 2020, 16:28:11 UTC |
433e5ba | Pierre-Yves Strub | 10 June 2020, 15:06:40 UTC | | 10 June 2020, 15:06:40 UTC |
41d0d08 | Pierre-Yves Strub | 10 June 2020, 14:44:03 UTC | 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 |
9909f4d | Pierre-Yves Strub | 10 June 2020, 14:43:30 UTC | | 10 June 2020, 14:43:30 UTC |
e6a9d11 | Pierre-Yves Strub | 10 June 2020, 14:34:02 UTC | Merge branch 'deploy-rewrite' into 1.0-preview | 10 June 2020, 14:34:02 UTC |
502db3d | Pierre-Yves Strub | 10 June 2020, 14:33:42 UTC | change behavior of rewrite !? | 10 June 2020, 14:33:42 UTC |
2e45603 | Pierre-Yves Strub | 10 June 2020, 14:16:36 UTC | Merge branch 'deploy-rewrite' into 1.0-preview | 10 June 2020, 14:16:36 UTC |
65f0514 | Pierre-Yves Strub | 10 June 2020, 14:14:30 UTC | Merge branch 'deploy-theory-matrix-ring' into deploy-rewrite | 10 June 2020, 14:14:30 UTC |
74142f2 | Pierre-Yves Strub | 10 June 2020, 14:14:07 UTC | Merge branch '1.0' into deploy-theory-matrix-ring | 10 June 2020, 14:14:07 UTC |
4b965ee | Pierre-Yves Strub | 10 June 2020, 14:13:50 UTC | Fix compilation | 10 June 2020, 14:13:50 UTC |
8057e61 | Pierre-Yves Strub | 10 June 2020, 14:10:55 UTC | Merge branch '1.0' into deploy-theory-matrix-ring | 10 June 2020, 14:10:55 UTC |
2558d8a | Pierre-Yves Strub | 10 June 2020, 14:09:28 UTC | | 10 June 2020, 14:09:28 UTC |
21da82c | Benjamin Gregoire | 10 June 2020, 12:40:16 UTC | test | 10 June 2020, 12:40:16 UTC |
9a1afd8 | Pierre-Yves Strub | 10 June 2020, 09:53:55 UTC | Merge branch '1.0' into 1.0-preview | 10 June 2020, 09:53:55 UTC |
c9641e4 | Pierre-Yves Strub | 10 June 2020, 09:53:25 UTC | Revert "Add user reductions for iteri" This reverts commit f693233ec9a7b33ba350d7b17e1d223f33d7fb56. | 10 June 2020, 09:53:35 UTC |
bcb430c | Benjamin Gregoire | 10 June 2020, 09:44:14 UTC | Merge branch '1.0' into 1.0-preview | 10 June 2020, 09:44:14 UTC |
bacb90b | Benjamin Gregoire | 10 June 2020, 08:02:11 UTC | in rewrite find occurences using alpha conversion first. | 10 June 2020, 09:41:40 UTC |
ab61883 | Benjamin Gregoire | 10 June 2020, 07:46:56 UTC | add reduction for -i = i' | 10 June 2020, 07:47:46 UTC |
19c6c50 | Benjamin Gregoire | 10 June 2020, 07:45:48 UTC | remove duplicate declaration | 10 June 2020, 07:47:46 UTC |
c595f3c | Pierre-Yves Strub | 10 June 2020, 07:46:49 UTC | Merge branch '1.0' into 1.0-preview | 10 June 2020, 07:46:49 UTC |
6965ea6 | Pierre-Yves Strub | 10 June 2020, 07:46:26 UTC | binomial law + basic lemmas (full / support) | 10 June 2020, 07:46:26 UTC |
2064617 | Pierre-Yves Strub | 10 June 2020, 07:28:45 UTC | "search" now works with notations [fix #17317] | 10 June 2020, 07:28:49 UTC |
b915e29 | Pierre-Yves Strub | 09 June 2020, 16:09:22 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 09 June 2020, 16:09:22 UTC |
3a942c7 | Pierre-Yves Strub | 09 June 2020, 16:09:00 UTC | fix compilation | 09 June 2020, 16:09:00 UTC |
4a33a26 | Pierre-Yves Strub | 09 June 2020, 16:05:23 UTC | Merge branch '1.0' into deploy-theory-matrix-ring | 09 June 2020, 16:05:23 UTC |
3090828 | Pierre-Yves Strub | 09 June 2020, 16:05:14 UTC | Merge branch '1.0' into 1.0-preview | 09 June 2020, 16:05:14 UTC |
763732a | Benjamin Gregoire | 09 June 2020, 15:43:37 UTC | smt: do not filter wanted lemma | 09 June 2020, 15:43:43 UTC |
f693233 | Pierre-Yves Strub | 09 June 2020, 15:39:58 UTC | Add user reductions for iteri | 09 June 2020, 15:39:58 UTC |
03d203a | Pierre-Yves Strub | 09 June 2020, 11:32:57 UTC | 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:34:24 UTC |
63b4818 | Pierre-Yves Strub | 08 June 2020, 17:14:32 UTC | 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> | 09 June 2020, 11:34:24 UTC |
23b938a | Pierre-Yves Strub | 09 June 2020, 11:32:57 UTC | 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 |
6018240 | Benjamin Gregoire | 09 June 2020, 05:28:48 UTC | Merge branch '1.0' into 1.0-preview | 09 June 2020, 05:28:48 UTC |
f71bd6c | Pierre-Yves Strub | 08 June 2020, 17:14:32 UTC | 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 | Benjamin Gregoire | 27 May 2020, 13:08:56 UTC | add lemmas on bigi | 27 May 2020, 13:11:27 UTC |
d143056 | Pierre-Yves Strub | 26 May 2020, 12:22:58 UTC | Merge branch '1.0' into 1.0-preview | 26 May 2020, 12:22:58 UTC |
ad888b8 | Alley Stoughton | 26 May 2020, 12:17:04 UTC | Make nosmt operator change on get_as_ operators. | 26 May 2020, 12:18:55 UTC |
f6e775f | Alley Stoughton | 22 May 2020, 22:12:19 UTC | 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, 12:18:55 UTC |
53ed919 | Alley Stoughton | 22 May 2020, 22:12:19 UTC | 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 |
286df20 | Pierre-Yves Strub | 16 May 2020, 07:09:16 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 16 May 2020, 07:09:16 UTC |
4f38720 | Pierre-Yves Strub | 16 May 2020, 06:57:58 UTC | more results on matrices | 16 May 2020, 06:57:58 UTC |
bcc7239 | Pierre-Yves Strub | 14 May 2020, 12:45:40 UTC | Merge branch '1.0' into deploy-theory-matrix-ring | 14 May 2020, 12:45:40 UTC |
170c443 | Benjamin Gregoire | 27 April 2020, 12:23:05 UTC | fix default.nix | 27 April 2020, 12:23:05 UTC |
7fa0fc1 | François Dupressoir | 23 April 2020, 14:46:50 UTC | Merge branch 'deploy-new-rom' into 1.0-preview | 23 April 2020, 14:46:50 UTC |
27fcbdc | Antoine Séré | 21 April 2020, 14:45:19 UTC | Merge branch '1.0' into 1.0-preview | 21 April 2020, 14:45:19 UTC |
58aaed4 | AntoineSere | 20 April 2020, 17:02:04 UTC | Merge pull request #42 from AntoineSere/eqvquo Added two useful lemmas to Quotient.ec | 20 April 2020, 17:02:04 UTC |
ce4d827 | Antoine Séré | 20 April 2020, 15:04:39 UTC | Added two useful lemmas to Quotient.ec | 20 April 2020, 15:04:39 UTC |
acfd4ea | Pierre-Yves Strub | 16 April 2020, 14:56:46 UTC | Definition of quotient types w.r.t. a equivalence relation | 16 April 2020, 14:56:46 UTC |
60a7d34 | Pierre-Yves Strub | 16 April 2020, 13:19:34 UTC | Finite groups, cyclic groups, Bezout. | 16 April 2020, 13:19:53 UTC |
c620224 | François Dupressoir | 27 March 2020, 13:29:51 UTC | leverage PROM in ROM | 16 April 2020, 11:09:05 UTC |
43f5e2c | François Dupressoir | 26 March 2020, 16:23:44 UTC | New PROM to serve as foundation for all ROM proofs | 16 April 2020, 11:08:27 UTC |
cdb2e6f | François Dupressoir | 16 April 2020, 10:45:54 UTC | Use arrow-based assignments This is to align standard libraries with 1.0-preview, which forbids '=' | 16 April 2020, 10:45:54 UTC |
c2e1b8f | Pierre-Yves Strub | 16 April 2020, 09:54:20 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 16 April 2020, 09:54:20 UTC |
e05cb75 | Pierre-Yves Strub | 16 April 2020, 09:54:14 UTC | Merge branch '1.0' into 1.0-preview | 16 April 2020, 09:54:14 UTC |
43d84a5 | Pierre-Yves Strub | 16 April 2020, 09:53:57 UTC | Matrix.eca: kill admits | 16 April 2020, 09:53:57 UTC |
09eb21d | Pierre-Yves Strub | 16 April 2020, 09:52:51 UTC | Merge branch '1.0' into deploy-theory-matrix-ring | 16 April 2020, 09:52:51 UTC |
f44260c | Pierre-Yves Strub | 16 April 2020, 09:41:06 UTC | stdlib: distributions: dmap1E_can | 16 April 2020, 09:41:06 UTC |
94786bc | Pierre-Yves Strub | 16 April 2020, 09:40:44 UTC | stdlib: List: nth_default | 16 April 2020, 09:40:44 UTC |
05e3caf | Pierre-Yves Strub | 16 April 2020, 06:34:14 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 16 April 2020, 06:34:14 UTC |
f21502a | Pierre-Yves Strub | 16 April 2020, 06:33:53 UTC | vector/matrix & matrix/vector multiplication + L/R-module lemmas | 16 April 2020, 06:33:53 UTC |
e71f5fe | Pierre-Yves Strub | 15 April 2020, 19:08:08 UTC | Merge branch 'deploy-theory-matrix-ring' into 1.0-preview | 15 April 2020, 19:08:08 UTC |
40ed14d | Pierre-Yves Strub | 15 April 2020, 19:07:39 UTC | dmatrix | 15 April 2020, 19:07:39 UTC |
557fc21 | Pierre-Yves Strub | 15 April 2020, 12:39:10 UTC | square matrices from a non-commutative ring | 15 April 2020, 12:39:10 UTC |
136b237 | Pierre-Yves Strub | 15 April 2020, 09:39:30 UTC | lemma: fun_ext2 | 15 April 2020, 09:39:30 UTC |
5eba66b | Pierre-Yves Strub | 15 April 2020, 09:31:23 UTC | allow writing m.[i, j] in place of m.[(i, j)] | 15 April 2020, 09:31:23 UTC |
4882379 | Pierre-Yves Strub | 15 April 2020, 08:28:48 UTC | views: allow application of induction principle as a view | 15 April 2020, 08:28:48 UTC |
64d592d | Pierre-Yves Strub | 15 April 2020, 08:19:44 UTC | elim: search quantifier modulo reduction | 15 April 2020, 08:19:54 UTC |
3b8b038 | Adrien Koutsos | 14 April 2020, 15:08:58 UTC | Fixed unclosed box. (#41) Co-authored-by: Adrien Koutsos <akoutsos@users.noreply.github.com> | 14 April 2020, 15:08:58 UTC |
88814a4 | Pierre-Yves Strub | 10 April 2020, 09:57:07 UTC | Merge branch '1.0' into 1.0-preview | 10 April 2020, 09:57:07 UTC |
f3581d5 | Pierre-Yves Strub | 10 April 2020, 09:56:42 UTC | binomial coefficients | 10 April 2020, 09:56:42 UTC |
21e8fce | Pierre-Yves Strub | 09 April 2020, 16:21:20 UTC | CI: move to slack notification | 09 April 2020, 16:21:20 UTC |
d41a34d | Pierre-Yves Strub | 09 April 2020, 13:43:45 UTC | Matching for *hoareF & Pr | 09 April 2020, 13:44:05 UTC |
4062085 | bgregoir | 09 April 2020, 13:39:11 UTC | Merge pull request #40 from CohenCyril/nixfix default.nix: adding installFlags | 09 April 2020, 13:39:11 UTC |
21354f7 | Cyril Cohen | 08 April 2020, 15:21:04 UTC | default.nix: adding installFlags | 08 April 2020, 15:23:25 UTC |
bafcc56 | Pierre-Yves Strub | 08 April 2020, 07:28:44 UTC | Merge branch '1.0' into 1.0-preview | 08 April 2020, 07:28:44 UTC |