https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
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
2e3a618 use abstract theory 04 September 2019, 13:31:51 UTC
84dc271 remove unused variable 04 September 2019, 07:11:42 UTC
132aa51 Add few lemmas 03 September 2019, 14:35:01 UTC
0a6c7f8 Proving probability equal to 1/2 using prhl 03 September 2019, 08:55:55 UTC
a4fb49d fix Why3 literals comparisons [fix #17394] 04 August 2019, 19:07:17 UTC
af281fd Do eta-expansion for fix-match branches [fix #17385] 02 August 2019, 20:16:22 UTC
43ac3f3 Fix bug in subst of type definition (parameters were not substituted) 22 July 2019, 16:54:24 UTC
a9666b1 user error message for FXE_CtorInvalidArity [fix #17387] 06 July 2019, 22:07:21 UTC
af25c22 Bug fixing in phl ([closes #17380]) 19 June 2019, 13:28:03 UTC
fc8d388 Move to Why3 1.x 11 June 2019, 09:59:50 UTC
679f333 run-test: add a -timing option 17 May 2019, 05:46:17 UTC
a79235c add an option [-tstats FILE] for recording timing statistics 17 May 2019, 05:34:41 UTC
e522b67 runtest: python2 -> python3 01 May 2019, 07:37:32 UTC
f293e76 Towards fixing XDG-based config 16 April 2019, 16:18:33 UTC
27c1df3 Allow : t1 || t2 || ... || tn 28 March 2019, 05:41:39 UTC
41219ef add reduction of Int div/mod by reduction of edivz + bind symbol to Why3 26 March 2019, 13:42:33 UTC
a041441 Add congruence rule for projections 26 March 2019, 13:32:42 UTC
5e9f955 Extend matching (projections) 26 March 2019, 10:46:03 UTC
8a0c097 Bind auto-conseq in eqobsin 26 March 2019, 09:59:05 UTC
b481f98 "call L" automatically applies "L" to "_" when needed. 25 March 2019, 12:03:45 UTC
1fb57b6 fix reduction of fixpoints with extra arguments 25 March 2019, 08:07:17 UTC
4387903 Fix pretty printing of records projectors (when applied) 28 January 2019, 13:48:44 UTC
9c1fdfb Reduction fix: reduces record projections when applied. 28 January 2019, 13:40:40 UTC
a893051 add missing quantification over memory in async while 17 January 2019, 17:22:08 UTC
337a8ab fix a smt call 20 December 2018, 14:25:05 UTC
b2b7e5b fix List.ec 20 December 2018, 13:13:35 UTC
532e12b 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 fix type of pred1 from 'a -> bool to 'a -> 'a -> bool 19 December 2018, 17:24:55 UTC
0b59cac fix bug in LDecl where the type of the operator was not correct. 18 December 2018, 14:35:55 UTC
88a87da Merge branch '1.0' of https://github.com/EasyCrypt/easycrypt into 1.0 17 December 2018, 14:33:18 UTC
dfe37eb fix bug where the type of pred1 was bool instead of 'a -> bool 17 December 2018, 14:32:33 UTC
5a31709 simplify proof 12 December 2018, 17:00:34 UTC
17eced8 Simplifying async-while examples 11 December 2018, 16:29:13 UTC
2d05f8b async-while: example for nested loops 11 December 2018, 16:24:53 UTC
ed7bf6c (internal API) - typed application soft-constructor for forms 03 December 2018, 12:40:04 UTC
f120f53 fix error message 13 November 2018, 08:12:18 UTC
9959602 More results in ZModP 07 November 2018, 21:51:34 UTC
5c95527 New tactic: - exlim (shorthand for exists*; elim*) - ecall (seq + exlim + call with inference) 07 November 2018, 21:47:02 UTC
28c5228 Fix Cramer Shoup 25 October 2018, 15:21:38 UTC
672c36d weaken axiom 25 October 2018, 14:38:06 UTC
5b694ae add some lemma 25 October 2018, 07:14:05 UTC
9d34c3b README 25 September 2018, 16:48:02 UTC
6b07f83 Extend SmtMap theory with new results. Co-authored-by: Alley Stoughton <alley.stoughton@icloud.com> 20 September 2018, 09:37:23 UTC
92effbe adding joint operator (+) and its lemmas (#21) 18 September 2018, 16:03:04 UTC
5cbf6f1 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 refining bound on Strong_RP_RF (#20) 17 September 2018, 10:58:49 UTC
c997f51 fix parsing of codeposition Syntax for offset is now: &+n and &-n. 12 September 2018, 11:42:33 UTC
978d985 fix handling of negative code positions 12 September 2018, 11:42:02 UTC
d3a650a fix condition in the rule for asynchrone while 24 July 2018, 05:53:40 UTC
7a4cb50 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 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 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 fix the checking of generated name in TheoryReplay 12 July 2018, 23:57:01 UTC
97e5b1d fix error in"unroll for" tactic in case of hoare and phoare 10 July 2018, 22:33:36 UTC
fecd089 apply: tactic now takes a clear/revert list as parameter 09 July 2018, 06:47:56 UTC
b75dc92 Add syntax for cast in expr/form: (e :~ ty) 07 July 2018, 21:11:06 UTC
85eabe3 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 add nix 21 June 2018, 13:51:13 UTC
fb7a987 More lemmas on List.take 19 June 2018, 13:25:10 UTC
ba545a9 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 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 Docker image: bump OCaml version to 4.04.0 31 May 2018, 13:00:17 UTC
6da5cf4 Docker: install Z3 & CVC4 via apt-get 25 May 2018, 20:12:54 UTC
1b9269a 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 `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 characterization lemmas for <=> and \proper [closes #17377] 29 April 2018, 09:34:36 UTC
aa75b1d 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 Docker : allow the use of any branch for building a Docker image 27 April 2018, 11:38:53 UTC
64c24ed 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 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 including mee-cbc in examples target 25 April 2018, 16:27:44 UTC
d30050d Induction principle for fmap 25 April 2018, 09:05:52 UTC
1845635 eta-conversion should only be triggered on terms with compatible types [fix #17306] 24 April 2018, 13:13:19 UTC
728c306 prove the equivalence between two versions of CPA LR and b. 24 April 2018, 09:11:41 UTC
a27bd48 Extending SmtMap with new facts (eq_except, map) + adapting lib/examples 24 April 2018, 06:25:41 UTC
9ae0786 New revert pattern: `@x` This revert pattern revert a local-binding as a let-in construct. [closes #17291] 23 April 2018, 14:06:48 UTC
a18abdf Deploy multi args eta ticket 17278 (#12) * Reduction for multi-arg eta rule. [fix #17278] 23 April 2018, 13:37:01 UTC
d7510b9 is_finite : provide a weaker characterization 23 April 2018, 12:16:30 UTC
de0e240 New smt option: quorum This option expects an integer argument. It indicates the number of smt provers that must solve a goal before being accepted. A value of 0 set the quorum to its default value (1). Note that if provers do not agree while waiting to reach a quorum, the goal is rejected. [closes #17371] 21 April 2018, 20:20:39 UTC
6ffe960 Swap the semantic of `` and `!` for smt provers option. [closes #17372] 21 April 2018, 20:06:23 UTC
e8b4835 moving OldDistr to oldlibs to mark deprecation 21 April 2018, 20:05:37 UTC
dcbc9de forgotten example (not included in CI) 21 April 2018, 20:05:37 UTC
6124ea4 pruning some deprecated theories 21 April 2018, 20:05:37 UTC
cefe872 porting example Upto 20 April 2018, 16:27:35 UTC
61fef31 porting example Fundamental Lemma 20 April 2018, 16:27:35 UTC
f027390 removing old WhileSampling 20 April 2018, 16:27:35 UTC
55d12be porting example WhileSampling 20 April 2018, 16:27:35 UTC
a7ed76c porting example Dice4_6 20 April 2018, 16:27:35 UTC
526d0c0 fix [#17369] : bug in printing of module application 20 April 2018, 14:36:26 UTC
1a54e95 Squashed commit of the following: commit 8a24a7237a36b7dda929a03eeaf70be1058d1e10 Author: Benjamin Gregoire <Benjamin.Gregoire@inria.fr> Date: Mon Apr 16 13:37:55 2018 +0200 fix glob bug by normalising glob in axioms/lemmas fix #17132 16 April 2018, 22:52:00 UTC
e5969ba 05 April 2018, 13:22:23 UTC
81d62ac pretty printer with {| ... with ... |} 03 April 2018, 16:48:08 UTC
79c3916 Add new construction for records: { x with f1 = v1; ...; fn = vn; } 03 April 2018, 08:09:24 UTC
dd158c9 Why3config: only try user configuration file 21 March 2018, 09:30:54 UTC
6453d5f Do not load Why3 config files when executing why3config cmd 21 March 2018, 09:29:50 UTC
bd4c706 New command: why3config 21 March 2018, 09:06:16 UTC
back to top