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 |
a041441 | Pierre-Yves Strub | 26 March 2019, 13:32:42 UTC | Add congruence rule for projections | 26 March 2019, 13:32:42 UTC |
5e9f955 | Pierre-Yves Strub | 26 March 2019, 10:46:03 UTC | Extend matching (projections) | 26 March 2019, 10:46:03 UTC |
8a0c097 | Pierre-Yves Strub | 26 March 2019, 09:59:05 UTC | Bind auto-conseq in eqobsin | 26 March 2019, 09:59:05 UTC |
b481f98 | Pierre-Yves Strub | 25 March 2019, 12:03:45 UTC | "call L" automatically applies "L" to "_" when needed. | 25 March 2019, 12:03:45 UTC |
1fb57b6 | Pierre-Yves Strub | 25 March 2019, 08:07:17 UTC | fix reduction of fixpoints with extra arguments | 25 March 2019, 08:07:17 UTC |
4387903 | Pierre-Yves Strub | 28 January 2019, 13:48:44 UTC | Fix pretty printing of records projectors (when applied) | 28 January 2019, 13:48:44 UTC |
9c1fdfb | Pierre-Yves Strub | 28 January 2019, 13:40:40 UTC | Reduction fix: reduces record projections when applied. | 28 January 2019, 13:40:40 UTC |
a893051 | Benjamin Gregoire | 17 January 2019, 17:22:08 UTC | add missing quantification over memory in async while | 17 January 2019, 17:22:08 UTC |
337a8ab | Cécile BARITEL-RUET | 20 December 2018, 14:25:05 UTC | fix a smt call | 20 December 2018, 14:25:05 UTC |
b2b7e5b | Cécile BARITEL-RUET | 20 December 2018, 13:13:35 UTC | fix List.ec | 20 December 2018, 13:13:35 UTC |
532e12b | Cécile BARITEL-RUET | 20 December 2018, 12:28:06 UTC | 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 | Cécile BARITEL-RUET | 19 December 2018, 17:24:55 UTC | fix type of pred1 from 'a -> bool to 'a -> 'a -> bool | 19 December 2018, 17:24:55 UTC |
0b59cac | Pierre-Yves Strub | 18 December 2018, 14:34:23 UTC | fix bug in LDecl where the type of the operator was not correct. | 18 December 2018, 14:35:55 UTC |
88a87da | Cécile BARITEL-RUET | 17 December 2018, 14:33:18 UTC | Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0 | 17 December 2018, 14:33:18 UTC |
dfe37eb | Cécile BARITEL-RUET | 17 December 2018, 14:32:33 UTC | fix bug where the type of pred1 was bool instead of 'a -> bool | 17 December 2018, 14:32:33 UTC |
5a31709 | Benjamin Gregoire | 12 December 2018, 17:00:34 UTC | simplify proof | 12 December 2018, 17:00:34 UTC |
17eced8 | Pierre-Yves Strub | 11 December 2018, 16:29:13 UTC | Simplifying async-while examples | 11 December 2018, 16:29:13 UTC |
2d05f8b | Pierre-Yves Strub | 11 December 2018, 16:24:53 UTC | async-while: example for nested loops | 11 December 2018, 16:24:53 UTC |
ed7bf6c | Pierre-Yves Strub | 03 December 2018, 12:40:04 UTC | (internal API) - typed application soft-constructor for forms | 03 December 2018, 12:40:04 UTC |
f120f53 | Benjamin Gregoire | 13 November 2018, 08:12:18 UTC | fix error message | 13 November 2018, 08:12:18 UTC |
9959602 | Pierre-Yves Strub | 07 November 2018, 21:51:34 UTC | More results in ZModP | 07 November 2018, 21:51:34 UTC |
5c95527 | Pierre-Yves Strub | 07 November 2018, 21:45:42 UTC | New tactic: - exlim (shorthand for exists*; elim*) - ecall (seq + exlim + call with inference) | 07 November 2018, 21:47:02 UTC |
28c5228 | Pierre-Yves Strub | 25 October 2018, 15:21:38 UTC | Fix Cramer Shoup | 25 October 2018, 15:21:38 UTC |
672c36d | Benjamin Gregoire | 25 October 2018, 14:38:06 UTC | weaken axiom | 25 October 2018, 14:38:06 UTC |
5b694ae | Benjamin Gregoire | 25 October 2018, 07:14:05 UTC | add some lemma | 25 October 2018, 07:14:05 UTC |
9d34c3b | Jorden Whitefield | 25 September 2018, 16:48:02 UTC | README | 25 September 2018, 16:48:02 UTC |
6b07f83 | Pierre-Yves Strub | 20 September 2018, 09:37:23 UTC | Extend SmtMap theory with new results. Co-authored-by: Alley Stoughton <alley.stoughton@icloud.com> | 20 September 2018, 09:37:23 UTC |
92effbe | Ruette | 18 September 2018, 16:03:04 UTC | adding joint operator (+) and its lemmas (#21) | 18 September 2018, 16:03:04 UTC |
5cbf6f1 | Pierre-Yves Strub | 17 September 2018, 11:33:37 UTC | 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 |
1b7e5bb | Ruette | 17 September 2018, 10:58:49 UTC | refining bound on Strong_RP_RF (#20) | 17 September 2018, 10:58:49 UTC |
c997f51 | Pierre-Yves Strub | 12 September 2018, 11:42:14 UTC | fix parsing of codeposition Syntax for offset is now: &+n and &-n. | 12 September 2018, 11:42:33 UTC |
978d985 | Pierre-Yves Strub | 12 September 2018, 11:42:02 UTC | fix handling of negative code positions | 12 September 2018, 11:42:02 UTC |
d3a650a | Benjamin Gregoire | 24 July 2018, 05:53:40 UTC | fix condition in the rule for asynchrone while | 24 July 2018, 05:53:40 UTC |
7a4cb50 | Pierre-Yves Strub | 14 July 2018, 05:48:00 UTC | Add an option for setting the printing width. Option can be given using: - a command line option (-pp-width) - an easycrypt.conf entry (general/pp-width) - a pervasive option (pragma PP:width = ...) | 14 July 2018, 05:58:10 UTC |
a52f327 | Pierre-Yves Strub | 13 July 2018, 18:34:30 UTC | New tactic: lossless. This tactic tries to prove goal of the form "islossless M.f". It uses random/lossless solve DB for pruning goals related to the losslessness of samplings or call to abstract procs. | 13 July 2018, 18:35:17 UTC |
de5cd4a | Pierre-Yves Strub | 13 July 2018, 10:56:47 UTC | Extend syntax for code position. Syntax is : codepos1 [.?] codepos1 [.?] ... [.?] codepos1 where codepos1 is of the form basepos [+-] offset and basepos is either an absolute position or of the form ^kw{n} where kw is amon if, while, <-, <@, <$ and {n} (which is optional) is a signed integer. | 13 July 2018, 10:57:06 UTC |
71f975a | Benjamin Gregoire | 12 July 2018, 23:57:01 UTC | fix the checking of generated name in TheoryReplay | 12 July 2018, 23:57:01 UTC |
97e5b1d | Benjamin Gregoire | 10 July 2018, 22:33:36 UTC | fix error in"unroll for" tactic in case of hoare and phoare | 10 July 2018, 22:33:36 UTC |
fecd089 | Pierre-Yves Strub | 09 July 2018, 06:47:56 UTC | apply: tactic now takes a clear/revert list as parameter | 09 July 2018, 06:47:56 UTC |
b75dc92 | Pierre-Yves Strub | 07 July 2018, 21:11:06 UTC | Add syntax for cast in expr/form: (e :~ ty) | 07 July 2018, 21:11:06 UTC |
85eabe3 | Pierre-Yves Strub | 27 June 2018, 03:27:30 UTC | Add [lossless / uniform / full] tags for operators These tags can be apply to operators whose co-domain is a distribution. It adds the relevant lossless / uniform / full axiom (named w.r.t the convention in Distr.ec) and add these axioms to the relevant lossless/random database. | 27 June 2018, 03:27:30 UTC |
e50b7a7 | Benjamin Gregoire | 21 June 2018, 13:50:55 UTC | add nix | 21 June 2018, 13:51:13 UTC |
fb7a987 | Pierre-Yves Strub | 19 June 2018, 13:25:10 UTC | More lemmas on List.take | 19 June 2018, 13:25:10 UTC |
ba545a9 | Benjamin Grégoire | 12 June 2018, 05:31:11 UTC | New tactic for static unrolling of "for-loops" The tactic statically unroll while loops of the form x <- int-constant while (guard) { body (does not write x); x <- f(x); } where "guard" and "f" can be statically evaluated at each iteration. The code is then replaced by the while loop fully unrolled. The tactic does not terminate if the unrolling leads to a infinite process. | 12 June 2018, 05:34:41 UTC |
43fd7aa | Francois Dupressoir | 03 June 2018, 23:18:05 UTC | Deploy smt blacklist (#19) Black-list all versions of Alt-Ergo < 2.2.0 + change default provers to : CVC4, Z3 & Alt-Ergo + fix relevant theories | 03 June 2018, 23:18:05 UTC |
4cf3582 | Pierre-Yves Strub | 31 May 2018, 13:00:17 UTC | Docker image: bump OCaml version to 4.04.0 | 31 May 2018, 13:00:17 UTC |
6da5cf4 | Pierre-Yves Strub | 25 May 2018, 20:12:54 UTC | Docker: install Z3 & CVC4 via apt-get | 25 May 2018, 20:12:54 UTC |
1b9269a | Pierre-Yves Strub | 21 May 2018, 20:36:27 UTC | New tactic: 'conseq ?>' where '?>' is a crush mode. Simplifies *HL post-condition from the pre using a crush-like simplication. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> | 21 May 2018, 20:36:27 UTC |
165ee99 | Pierre-Yves Strub | 20 May 2018, 06:18:32 UTC | `rnd` (in equiv mode) now tries to simplify the post. For instance, it removes all losslessness requirements when the distribution is known to be lossless. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> | 20 May 2018, 06:31:40 UTC |
7c6d40e | Pierre-Yves Strub | 28 April 2018, 15:09:18 UTC | characterization lemmas for <=> and \proper [closes #17377] | 29 April 2018, 09:34:36 UTC |
aa75b1d | Pierre-Yves Strub | 27 April 2018, 12:06:12 UTC | Move the contents of process_trivial down in the API. This makes 'seq' rules independent of hi-level tactics. | 27 April 2018, 12:06:12 UTC |
dcb1f2f | Pierre-Yves Strub | 27 April 2018, 11:38:08 UTC | Docker : allow the use of any branch for building a Docker image | 27 April 2018, 11:38:53 UTC |
64c24ed | Benjamin Gregoire | 26 April 2018, 18:31:53 UTC | improve "include" in module type and module. The following is now possible: type t, t', u, u', v, v'. module type OT = { proc f(_: t): t' proc g1(_: t): t' }. module type MT (O : OT) = { include OT proc g(_: u): u' }. module type MT1 (O : OT) = { include OT [f] proc g(_: u): u' }. module type MT2 (O : OT) = { include OT [f] {O.f} proc g(_: u): u' }. module type MT3 (O : OT) = { include OT [f] {O.g1} proc g(_: u): u' }. module ((M : MT1):MT2) (O : OT) = { proc f = O.f proc g(x: u): u' = { return witness; } }. module M1 = { proc f () : unit = { } proc g () : unit = { } }. module M2 = { include M1 }. module M3 = { include M1 [f] }. module M4 = { include M1 [+f] }. module M5 = { include M1 [-f] }. module F (O:OT) = { proc f1 () = {} }. module G (O:OT) = { include O include F(O) }. module G1 (O:OT) = { include O [-f] include F(O) }. | 26 April 2018, 18:31:53 UTC |
7f33e2a | Benjamin Grégoire | 26 April 2018, 06:13:35 UTC | Module type include & bulk proc aliasing - 'include I' in module type allows the include of the contents of I - proc f1, f2, f3, ... = M imports f1, f2, f3 from M into the current module definition. [closes #17375] | 26 April 2018, 06:18:29 UTC |
4395a7e | François Dupressoir | 25 April 2018, 15:40:02 UTC | including mee-cbc in examples target | 25 April 2018, 16:27:44 UTC |
d30050d | Pierre-Yves Strub | 25 April 2018, 09:05:52 UTC | Induction principle for fmap | 25 April 2018, 09:05:52 UTC |
1845635 | Pierre-Yves Strub | 24 April 2018, 12:47:18 UTC | eta-conversion should only be triggered on terms with compatible types [fix #17306] | 24 April 2018, 13:13:19 UTC |