b698ae3 | Pierre-Yves Strub | 10 February 2020, 11:25:04 UTC | Revert "ElGamal examples" This reverts commit 18fe2643e237c7a9e69745253342debfe22ff017. | 10 February 2020, 11:25:04 UTC |
515ea8d | Pierre-Yves Strub | 10 February 2020, 11:24:44 UTC | Partial revert | 10 February 2020, 11:24:44 UTC |
443a0bf | Pierre-Yves Strub | 10 February 2020, 11:20:16 UTC | Revert "progress on cramer shoup" This reverts commit 67e28210597785f42e1d0881689b9d7b128ef3b3. | 10 February 2020, 11:20:16 UTC |
5e8eafd | Pierre-Yves Strub | 10 February 2020, 11:18:44 UTC | Revert "DiffieHellman with abstract exponents" This reverts commit c752d6a29342f156a844b63dbe85990441738e1b. | 10 February 2020, 11:18:44 UTC |
4592bc2 | Pierre-Yves Strub | 10 February 2020, 11:17:27 UTC | Revert "'fix' all examples" This reverts commit c6d5455a3ffba8caf03c926a463ca969d9c93fc6. | 10 February 2020, 11:17:27 UTC |
0460309 | Pierre-Yves Strub | 10 February 2020, 11:17:17 UTC | Revert "simplify without loss (or gain) in performance" This reverts commit 2c1bea48a3bb52b6ba2f28dd3e7f8018c6ff98f3. | 10 February 2020, 11:17:17 UTC |
f4bc837 | Pierre-Yves Strub | 10 February 2020, 11:12:55 UTC | exp over a prime order | 10 February 2020, 11:12:55 UTC |
8c765a7 | Pierre-Yves Strub | 10 February 2020, 10:56:17 UTC | zmodp is a field when p is prime | 10 February 2020, 10:56:17 UTC |
2c1bea4 | François Dupressoir | 25 November 2019, 15:17:14 UTC | simplify without loss (or gain) in performance The issue seems to be with: - matching in ZModP and clones; (rewrites of exp expressions are slow, rewrites of group expressions are fast) - `congr` on g ^ x = g ^ y; On those algebra and congr calls that take a long time, in proofgeneral, interrupting using `C-c C-c` twice interrupts but progresses the proof quickly. | 25 November 2019, 15:17:14 UTC |
c6d5455 | François Dupressoir | 25 November 2019, 11:19:40 UTC | 'fix' all examples | 25 November 2019, 11:19:40 UTC |
886a29f | François Dupressoir | 22 November 2019, 13:54:33 UTC | fiddling | 25 November 2019, 10:43:34 UTC |
fc4989a | François Dupressoir | 22 November 2019, 12:53:46 UTC | try to avoid perf issues | 22 November 2019, 12:53:46 UTC |
2510842 | François Dupressoir | 22 November 2019, 12:27:38 UTC | injectivity lemmas | 22 November 2019, 12:27:38 UTC |
c752d6a | François Dupressoir | 22 November 2019, 12:04:44 UTC | DiffieHellman with abstract exponents | 22 November 2019, 12:04:44 UTC |
654f104 | François Dupressoir | 22 November 2019, 10:58:33 UTC | extend cyclic abstraction | 22 November 2019, 10:58:33 UTC |
a5bee17 | Pierre-Yves Strub | 22 November 2019, 07:01:17 UTC | pow-zmod | 22 November 2019, 07:01:17 UTC |
e9780dc | Pierre-Yves Strub | 22 November 2019, 06:46:21 UTC | zmod-cyclic | 22 November 2019, 06:46:21 UTC |
67e2821 | François Dupressoir | 21 November 2019, 14:03:17 UTC | progress on cramer shoup | 21 November 2019, 14:03:17 UTC |
6ca04dd | François Dupressoir | 21 November 2019, 12:25:52 UTC | Adding a skeletal modular inverse operator | 21 November 2019, 12:25:52 UTC |
716d29d | Pierre-Yves Strub | 21 November 2019, 07:48:54 UTC | nits | 21 November 2019, 07:48:54 UTC |
8176537 | Pierre-Yves Strub | 21 November 2019, 07:00:54 UTC | empty -> sempty | 21 November 2019, 07:00:54 UTC |
e16ffa9 | Pierre-Yves Strub | 21 November 2019, 06:54:27 UTC | redispatching | 21 November 2019, 06:54:27 UTC |
55eb853 | Pierre-Yves Strub | 21 November 2019, 06:45:57 UTC | proving existence of gcd | 21 November 2019, 06:45:57 UTC |
383efbf | Pierre-Yves Strub | 21 November 2019, 05:19:53 UTC | add missing files | 21 November 2019, 05:19:53 UTC |
c4c167a | Pierre-Yves Strub | 20 November 2019, 20:25:34 UTC | modular inverse | 20 November 2019, 20:25:34 UTC |
b71c8dd | Pierre-Yves Strub | 20 November 2019, 07:00:42 UTC | gcd props from its specs | 20 November 2019, 07:00:42 UTC |
ae00166 | Pierre-Yves Strub | 19 November 2019, 21:19:08 UTC | Bachet Bezout on top of an axiomatized gcd | 19 November 2019, 21:19:17 UTC |
3e6906c | François Dupressoir | 18 November 2019, 21:06:13 UTC | Diffie-Hellman: add some facts about dp | 18 November 2019, 21:19:33 UTC |
18fe264 | François Dupressoir | 18 November 2019, 16:48:11 UTC | ElGamal examples | 18 November 2019, 16:48:11 UTC |
d886e04 | François Dupressoir | 18 November 2019, 15:19:41 UTC | Update Diffie-Hellman | 18 November 2019, 16:19:20 UTC |
ca7332a | Pierre-Yves Strub | 18 November 2019, 14:05:41 UTC | refactoring | 18 November 2019, 14:05:41 UTC |
ed876c5 | Pierre-Yves Strub | 18 November 2019, 13:33:40 UTC | Finite & cyclic groups def + core results | 18 November 2019, 13:33:42 UTC |
add72dc | Pierre-Yves Strub | 14 November 2019, 10:15:31 UTC | 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 | Francois Dupressoir | 07 November 2019, 16:19:02 UTC | add the full PRG tutorial from FOSAD (#35) | 07 November 2019, 16:19:02 UTC |
e53aab7 | Pierre-Yves Strub | 25 October 2019, 15:59:30 UTC | Check .eco after the loader has been configured [fix #17400] | 25 October 2019, 15:59:33 UTC |
6489ade | Pierre-Yves Strub | 25 October 2019, 06:45:59 UTC | 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 | Pierre-Yves Strub | 18 October 2019, 08:36:08 UTC | Add EC hash to .eco | 18 October 2019, 08:36:08 UTC |
51f8ab0 | Pierre-Yves Strub | 18 October 2019, 08:11:34 UTC | .gitignore: .eco | 18 October 2019, 08:11:34 UTC |
f38226c | Pierre-Yves Strub | 17 October 2019, 10:08:11 UTC | 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 | Pierre-Yves Strub | 16 October 2019, 09:09:32 UTC | Fix t_auto. (was pruning opened goals) | 16 October 2019, 09:09:32 UTC |
2139beb | Pierre-Yves Strub | 15 October 2019, 07:46:58 UTC | CI: test 1.0-preview | 15 October 2019, 07:46:58 UTC |
2f6587f | Pierre-Yves Strub | 15 October 2019, 07:09:54 UTC | In `case`, normalized 'glob' when searching for an inductive type. [fix #17391] | 15 October 2019, 07:09:54 UTC |
74207ab | Pierre-Yves Strub | 14 October 2019, 15:22:16 UTC | Remove debugging infos | 14 October 2019, 15:22:16 UTC |
e023995 | Benjamin Gregoire | 14 October 2019, 12:09:21 UTC | New option from inline: [tuple]. Allows no to not use tuple assignments. | 14 October 2019, 12:27:51 UTC |
a38b2e9 | Pierre-Yves Strub | 14 October 2019, 12:05:09 UTC | Fix handling of abstract theories imports. | 14 October 2019, 12:05:09 UTC |
e12e2c2 | Pierre-Yves Strub | 14 October 2019, 08:38:48 UTC | 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 | Pierre-Yves Strub | 14 October 2019, 08:24:30 UTC | Solve tactic: apply is now done modulo delta | 14 October 2019, 08:24:30 UTC |
e77d659 | Pierre-Yves Strub | 14 October 2019, 07:45:06 UTC | Misc. in SmtMap.ec | 14 October 2019, 07:45:06 UTC |
297f528 | Benjamin Gregoire | 14 October 2019, 07:09:06 UTC | Add interleave tactic | 14 October 2019, 07:10:05 UTC |
ce9380d | Benjamin Gregoire | 14 October 2019, 06:41:25 UTC | Add transitivity * (transivity with generation of VC) | 14 October 2019, 06:42:35 UTC |
3b9667b | Pierre-Yves Strub | 14 October 2019, 06:27:33 UTC | 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 | Pierre-Yves Strub | 14 October 2019, 05:55:05 UTC | Add decimal literals | 14 October 2019, 05:55:27 UTC |
115229e | Pierre-Yves Strub | 14 October 2019, 05:19:52 UTC | New intro pattern: [#|]. [#|] is a multi-case i-p (like [#]) that works also on on disjunctions. | 14 October 2019, 05:19:52 UTC |
1f45fde | Alley Stoughton | 10 October 2019, 11:50:05 UTC | refactor flagged map && PROM (#22) | 10 October 2019, 11:50:05 UTC |
da0b25a | Francois Dupressoir | 10 October 2019, 07:49:06 UTC | Some extra lemmas on nseq (#26) | 10 October 2019, 07:49:06 UTC |
408d1b0 | Asif Mallik | 10 October 2019, 07:19:29 UTC | Add a more general version of dmap_uni (#30, #33) | 10 October 2019, 07:19:29 UTC |
e9598be | Asif Mallik | 10 October 2019, 06:50:06 UTC | Add lemmas to filter noncontributing list items in bigops (#29) | 10 October 2019, 06:50:06 UTC |
8eb2491 | nitrogl | 09 October 2019, 19:14:57 UTC | 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 | Pierre-Yves Strub | 02 October 2019, 06:23:52 UTC | Namespace for libraries and th. renaming | 02 October 2019, 06:23:52 UTC |
f2bcd42 | Pierre-Yves Strub | 01 October 2019, 20:12:36 UTC | README: add a note about installing external deps for provers | 01 October 2019, 20:12:36 UTC |
b6a4d3a | Pierre-Yves Strub | 01 October 2019, 14:26:02 UTC | Docker: bump Z3 version | 01 October 2019, 19:49:59 UTC |
4860685 | Pierre-Yves Strub | 01 October 2019, 10:54:42 UTC | Fetch more up-to-date smt binaries & compress unnecessary layers | 01 October 2019, 10:54:42 UTC |
88ded1b | Pierre-Yves Strub | 17 September 2019, 11:28:41 UTC | Fix "n?" intro pattern. | 17 September 2019, 11:28:41 UTC |
67392e1 | Cécile BARITEL-RUET | 16 September 2019, 12:54:52 UTC | RndProd : random oracle of a dprod | 16 September 2019, 12:56:20 UTC |
a8e2f10 | Pierre-Yves Strub | 15 September 2019, 12:05:31 UTC | Fix defered start of provers | 15 September 2019, 16:59:56 UTC |
7641f4a | Benjamin Gregoire | 13 September 2019, 14:21:19 UTC | merge RndO and PROM | 13 September 2019, 14:21:19 UTC |
3d66517 | Benjamin Gregoire | 13 September 2019, 11:17:04 UTC | import DHIES | 13 September 2019, 11:17:04 UTC |
2c5203d | Pierre-Yves Strub | 13 September 2019, 11:01:05 UTC | more on lists (assoc, onth) + some facts on fmap/assoc | 13 September 2019, 11:01:20 UTC |
13b7bdd | Benjamin Gregoire | 13 September 2019, 09:49:36 UTC | add PKSMK | 13 September 2019, 09:49:36 UTC |
3bbc09b | Benjamin Gregoire | 13 September 2019, 09:39:56 UTC | add AEAD | 13 September 2019, 09:39:56 UTC |
746d64c | Pierre-Yves Strub | 13 September 2019, 08:30:58 UTC | Revert "remove duplicate lemma get_none -> domNE" This reverts commit 60d29c1f11f6c79824022608f9f83503d983ce61. | 13 September 2019, 08:30:58 UTC |
0344765 | Pierre-Yves Strub | 13 September 2019, 08:20:36 UTC | djoin and al | 13 September 2019, 08:20:36 UTC |
60d29c1 | Benjamin Gregoire | 13 September 2019, 06:39:19 UTC | remove duplicate lemma get_none -> domNE | 13 September 2019, 06:39:19 UTC |
0e717db | Pierre-Yves Strub | 12 September 2019, 21:17:28 UTC | 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 | Pierre-Yves Strub | 12 September 2019, 20:57:15 UTC | Fix compilation | 12 September 2019, 20:57:15 UTC |
2dd053c | Benjamin Gregoire | 12 September 2019, 19:05:48 UTC | add assumption | 12 September 2019, 20:35:16 UTC |
7fb964c | Benjamin Gregoire | 12 September 2019, 19:01:35 UTC | add generalized oracle Diffie-Hellman assumption | 12 September 2019, 20:35:16 UTC |
350728b | Benjamin Gregoire | 12 September 2019, 18:05:03 UTC | add hash colision resistant assumption | 12 September 2019, 20:35:16 UTC |
0f3ebba | Pierre-Yves Strub | 12 September 2019, 19:10:51 UTC | dlet-sampling : distr are now parameters | 12 September 2019, 19:10:51 UTC |
65e3d88 | Pierre-Yves Strub | 12 September 2019, 14:21:46 UTC | eqv between dlet-sampling and seq-sampling | 12 September 2019, 14:21:46 UTC |
6ec8512 | Benjamin Gregoire | 12 September 2019, 12:26:49 UTC | fix trivial error | 12 September 2019, 12:26:49 UTC |
786cb63 | Benjamin Gregoire | 12 September 2019, 12:18:07 UTC | Add generic Lazy/Eager for random oracle | 12 September 2019, 12:18:29 UTC |
e5efb23 | Pierre-Yves Strub | 06 September 2019, 13:48:52 UTC | Refactor and kill all admits related to distributions and infinite sums. | 06 September 2019, 13:48:52 UTC |
60b76e8 | Benjamin Gregoire | 05 September 2019, 09:05:32 UTC | Try to remove exponential behavior | 05 September 2019, 09:05:32 UTC |
2e3a618 | Benjamin Gregoire | 04 September 2019, 13:31:51 UTC | use abstract theory | 04 September 2019, 13:31:51 UTC |
84dc271 | Benjamin Gregoire | 04 September 2019, 07:11:42 UTC | remove unused variable | 04 September 2019, 07:11:42 UTC |
132aa51 | Benjamin Gregoire | 03 September 2019, 14:35:01 UTC | Add few lemmas | 03 September 2019, 14:35:01 UTC |
0a6c7f8 | Benjamin Gregoire | 03 September 2019, 08:54:33 UTC | Proving probability equal to 1/2 using prhl | 03 September 2019, 08:55:55 UTC |
a4fb49d | Pierre-Yves Strub | 04 August 2019, 19:07:17 UTC | fix Why3 literals comparisons [fix #17394] | 04 August 2019, 19:07:17 UTC |
af281fd | Pierre-Yves Strub | 02 August 2019, 20:16:22 UTC | Do eta-expansion for fix-match branches [fix #17385] | 02 August 2019, 20:16:22 UTC |
43ac3f3 | Benjamin Gregoire | 22 July 2019, 16:54:24 UTC | Fix bug in subst of type definition (parameters were not substituted) | 22 July 2019, 16:54:24 UTC |
a9666b1 | Pierre-Yves Strub | 06 July 2019, 22:07:08 UTC | user error message for FXE_CtorInvalidArity [fix #17387] | 06 July 2019, 22:07:21 UTC |
af25c22 | Benjamin Gregoire | 19 June 2019, 13:28:03 UTC | Bug fixing in phl ([closes #17380]) | 19 June 2019, 13:28:03 UTC |
fc8d388 | Pierre-Yves Strub | 11 June 2019, 09:59:50 UTC | Move to Why3 1.x | 11 June 2019, 09:59:50 UTC |
679f333 | Pierre-Yves Strub | 17 May 2019, 05:46:17 UTC | run-test: add a -timing option | 17 May 2019, 05:46:17 UTC |
a79235c | Pierre-Yves Strub | 17 May 2019, 05:34:41 UTC | add an option [-tstats FILE] for recording timing statistics | 17 May 2019, 05:34:41 UTC |
e522b67 | Pierre-Yves Strub | 01 May 2019, 07:37:32 UTC | runtest: python2 -> python3 | 01 May 2019, 07:37:32 UTC |
f293e76 | François Dupressoir | 16 April 2019, 15:21:17 UTC | Towards fixing XDG-based config | 16 April 2019, 16:18:33 UTC |
27c1df3 | Pierre-Yves Strub | 28 March 2019, 05:41:39 UTC | Allow : t1 || t2 || ... || tn | 28 March 2019, 05:41:39 UTC |
41219ef | Pierre-Yves Strub | 26 March 2019, 13:42:33 UTC | add reduction of Int div/mod by reduction of edivz + bind symbol to Why3 | 26 March 2019, 13:42:33 UTC |