https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
92c2f2a Pragmas for printing pre/post as a list of their resp. conjunctions Pragmas are: PrPo:{pr,po}:{raw,ands} 20 May 2018, 11:16:22 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
0c76343 Put configuration files under $XDG 20 March 2018, 09:11:32 UTC
9867134 Fixed bug in SMT option matching The third stage of filtering in the definition of option_matching had a bug, meaning that attempts to rely on it resulted in assertion failures. But that last stage - disambiguating from right to left - was arguably hard for users to predict, anyway. So, fixed the third stage, but left it out of algorithm. (If it's really desired, easy to put it back in, as now it'll work. But do we really think users will understand why, e.g., [prover x=1] means [prover maxlemmas=1] - because the x in maxlemmas comes earlier when working backward as opposed to the x in maxprovers?) This is how option disambiguation works: First filter-in those option names having the letters of the abbreviation abv in the correct order. Then work through the letters of abv in order, keeping only those option names in which each successive letter appears as early as possible 28 February 2018, 06:58:30 UTC
8ab4986 Fixed mistake wrt oiter. 26 February 2018, 15:04:53 UTC
9e2c45b Fixed poor spacing. 26 February 2018, 15:04:53 UTC
1ca374d Reworking specification of current provers. All use-only instructions must come first. There are two "universal" use-only instructions: "" (all known provers), and "!" (no provers). It is illegal to mix ""/"!" with prover names (no point in doing so). As before, if the use-only part is empty, it means the currently known provers. The include/exclude instructions are processed in order, acting on the result of the use-only part. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* no-op *) prover [-"Z3"]. (* removes "Z3" from current provers *) prover [+"Z3"]. (* adds "Z3" to current provers *) prover [""]. (* results in "Z3", "Alt-Ergo" *) prover ["!"]. (* results in no provers *) prover ["Z3"]. (* results in "Z3" *) prover ["Z3" "Alt-Ergo"]. (* results in "Z3", "Alt-Ergo" *) prover ["!" +"Z3"]. (* results in "Z3" *) prover ["" -"Z3"]. (* results in "Alt-Ergo" *) 26 February 2018, 15:04:53 UTC
36f7f5a Added clean way to clear the list of current provers. The elements of prover [...] have one of the following forms, where s is a string: s (add s to the use-only list) +s (add include s to the include/exclude list) -s (add exclude s to the include/exclude list) The include/exclude list is ordered, so that later instructions can supersede earlier ones. The use-only list was not ordered, but now is. The relative order of the use-only and include/exclude lists is irrelevant, so that, e.g., prover ["Z3" +"Alt-Ergo"] and prover [+"Alt-Ergo" "Z3"] are equivalent. The semantics is that the use-only list is first interpreted (if it's empty, one starts with the current provers as the base), and only then are the instructions of the include/exclude list applied to it, in order. There was already the special use-only instruction "ALL". Now, there is also the use-only instruction "CLEAR", which clears the use-only list, but may be superseded by the use-only instructions that follow. Examples (assuming "Z3" and "Alt-Ergo" are only known provers): prover []. (* a no-op *) prover [+"Z3"] (* adds just "Z3" to whatever current provers are *) prover [-"Z3"] (* removes just "Z3" from whatever current provers are *) prover ["ALL"] (* results in "Z3", "Alt-Ergo" *) prover ["CLEAR"] (* results in nothing *) prover ["CLEAR" +"Z3"] (* results in just "Z3" *) prover [+"Z3" "CLEAR"] (* results in just "Z3" *) prover ["CLEAR" "Z3"] (* result in just "Z3" *) prover ["Z3" "CLEAR"] (* results in nothing *) prover [-"Z3" "ALL"] (* results in "Alt-Ergo" *) prover [+"Z3" "ALL" -"Z3"] (* results in "Alt-Ergo" *) prover [-"Z3" "ALL" +"Z3"] (* results in "Z3", "Alt-Ergo" *) 26 February 2018, 15:04:53 UTC
5115c89 SmtMap: rng and basic results 24 February 2018, 08:13:05 UTC
9f07d02 SmtMap : fdom and related results 24 February 2018, 08:12:44 UTC
dd27d32 whitespace 22 February 2018, 10:57:52 UTC
850f427 SMT backed map/fmap 21 February 2018, 16:09:18 UTC
6c010d0 Travis/Docker : sync UID/GID + fix reports publication 21 February 2018, 15:26:26 UTC
459d1a1 focusing smt calls in hashed ElGamal 21 February 2018, 10:22:19 UTC
f033f81 FSet library: subset is an operator rather than a predicate Inclusion is now written “\subset” (instead of “<=”). Strict inclusion is now written “\proper” (instead of “<”). 21 February 2018, 08:18:07 UTC
5b2f5a7 update copyrights 12 February 2018, 17:08:40 UTC
b622d44 Docker: force OCaml version 4.03 05 February 2018, 10:30:53 UTC
2ad5a58 remove Docker file for aprhl-test-box 05 February 2018, 10:30:30 UTC
25c632b Fix bug in theory-cloning renaming Path substitution was not build using the correct old-path when a theory substitution was in place. [fix #17361] 21 January 2018, 23:57:32 UTC
7cce8c6 documenting br93 further 19 January 2018, 21:32:01 UTC
1bca807 speed PIR example up 19 January 2018, 17:51:31 UTC
26b6fd9 New tactical: try! `try!` is similar to `try`, but allows `smt` calls to fail in strict mode. This is for debugging purpose only. `try!` immediately fails on non-strict mode. 18 January 2018, 21:21:37 UTC
7bc73a4 New tactic: solve `solve` is a resolution tactics. Currently, it tries to (recursively) close goals with the lemmas in the hint databases (in the same manner as `done` with the `hint exact` database). However, `solve` can be given hint databases names with the syntax: `solve (db1, db2, ...)` The maximum depth of the resolution tree is controled by an optional argument that comes first (`solve 2` for example). By default, the depth is equal to 1. Databases can be created using the 'hint solve' command: `hint solve $priority $dbname : lemma1 lemma2'. where the priority is optional --- `solve` tries to solve goals using lemmas with a lower $priority first. `hint exact ...` is now an alias for `hint solve 0 ...` 19 December 2017, 11:21:58 UTC
19c5eed more ways to do the proof 18 December 2017, 12:13:47 UTC
34d6e51 New IP: //> & ||> The IP //> & ||> are equivalent to /> & |> but use a stronger resolution tactic. 14 December 2017, 12:26:45 UTC
ddc2701 Add alternative proof in PIR. 14 December 2017, 10:38:21 UTC
fe76f33 more lemmas on FSet.oflist 14 December 2017, 10:37:55 UTC
527d9ad add new example: Private information retrieval. 08 December 2017, 14:56:08 UTC
89618eb New tactic: wlog (without loss of generality). Syntax is: wlog: x1 ... xn / form. It transforms the goal G into: |- (forall x1 ... xn, form => G) => G |- form => G 15 November 2017, 06:54:48 UTC
1923b91 Minimal attempt at stabilising Hybrid 14 November 2017, 14:04:42 UTC
9bdd6dd More stabilising smt in ROM 14 November 2017, 13:34:09 UTC
2f6312c Stabilise smt in old ROM.ec 13 November 2017, 17:06:47 UTC
b95b795 In ROM.ec, help `smt` by using `move=> />`. 13 November 2017, 15:19:53 UTC
0c14bcb More on (zmodule) exponential & ordering. 13 November 2017, 15:19:53 UTC
d3dcd49 New syntaxe for `pose`. `pose` can now take arguments as in `pose f i j := i + k`. 09 November 2017, 23:27:41 UTC
89f2173 Strengthen reduction for le/lt (int/real) 07 November 2017, 09:14:11 UTC
7721333 Implemented (#2) rewrite Pr [...] for mu_ge0 and mu_le1, corresponding to lemma ge0_mu (d : 'a distr) p : 0%r <= mu d p. lemma le1_mu (d : 'a distr) p : mu d p <= 1%r. from Distr.ec 05 November 2017, 08:09:52 UTC
7f64de1 docker: add support for sphinx in the doc-box. 04 November 2017, 22:36:30 UTC
c7988e8 keywords script: add support for python output. 04 November 2017, 22:35:35 UTC
d492fcd Libraries: distributions: killing more admits 27 October 2017, 07:14:18 UTC
65dfe3c Libraries: refactoring + killing admits. 27 October 2017, 07:03:50 UTC
ab29b3b Libraries: distr: killing admits 26 October 2017, 21:55:18 UTC
3f125db Libraries: proof of the Cauchy-Schwarz inequality. The proof is done for any euclidean R-ev of finite dimension. The proof comes with a characterisation of zeros for 2nd degree real polynomials. 23 October 2017, 07:51:11 UTC
9c39dce Libraries: extra facts on iterated multiplication. 23 October 2017, 07:49:57 UTC
caf9b25 Libraries: solving 2nd degree real polynomials. 23 October 2017, 04:32:43 UTC
fd7a34f Libraries: link Real.(^) with generic one. 23 October 2017, 04:28:35 UTC
fb22315 Libraries: extra facts on the square root. 23 October 2017, 04:26:57 UTC
280f627 Add [field] as a rewrite tactic. 23 October 2017, 03:51:09 UTC
2d97328 build script: pass ECBRANCH to docker 23 October 2017, 02:56:49 UTC
3b4aeec New facts on lists 12 October 2017, 13:17:20 UTC
8999c70 New facts on lists 12 October 2017, 12:50:02 UTC
cfa0695 Few facts on <= and exp 12 October 2017, 11:24:33 UTC
56964f5 Update installation instructions for Windows (using opam). 10 October 2017, 07:04:02 UTC
10a2fc7 Binary packages automatisation scripts. 10 October 2017, 07:03:49 UTC
89fb774 exclude examples/incomplete recursively 28 September 2017, 11:37:51 UTC
7cee24f Support recursive exclusions in test targets 28 September 2017, 11:37:51 UTC
44ae0e6 typo in error message (ecHiGoal) 25 August 2017, 09:36:18 UTC
3e7dc31 moving ahead - some admits in FEL application 21 August 2017, 16:29:20 UTC
ac19323 oaep: experimenting with fel flexibility and style 11 August 2017, 16:15:49 UTC
2a78686 typos in Distr (comments) 11 August 2017, 16:15:05 UTC
379e448 oaep: some progress 10 August 2017, 21:33:31 UTC
9329d72 oaep: exploring useful intermediate lemmas 03 August 2017, 15:36:15 UTC
a2de959 Cleanup in examples: deleting some, porting some. 02 August 2017, 15:25:38 UTC
c589262 OAEP progress 31 July 2017, 11:27:39 UTC
68f7b62 remove garbage 28 July 2017, 10:22:23 UTC
d5c7c6e full proof of cramer shoup :-) 28 July 2017, 09:58:12 UTC
00a61be new theory allowing to switch from a sampling d to a sampling d \ X 28 July 2017, 09:58:12 UTC
cbeb6f3 more lemmas 28 July 2017, 09:58:12 UTC
55cc1ec fix bug in typing of projection on tuple. case the tuple as type "glob M" 28 July 2017, 09:58:12 UTC
back to top