https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
ad258e9 no need for List.sort for maps 27 March 2018, 12:38:51 UTC
250d260 27 March 2018, 11:55:31 UTC
061bb46 Merge branch '1.0' into deploy-poly-record 27 March 2018, 11:47:41 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
500436c cleaneeeer 19 March 2018, 13:53:04 UTC
de52730 cleaner 19 March 2018, 12:13:45 UTC
d4e3f5a cleaner 19 March 2018, 10:52:55 UTC
47336dd t_case ok? 19 March 2018, 10:43:14 UTC
f87b7f9 t_split looks ok 19 March 2018, 10:02:07 UTC
7f5920e - 15 March 2018, 15:22:12 UTC
b2d376e - 13 March 2018, 15:17:35 UTC
18a33a6 Better pretty printing 13 March 2018, 11:10:57 UTC
141d0f5 - 12 March 2018, 15:12:12 UTC
7647c90 adding values /lots of warning solved 08 March 2018, 15:33:20 UTC
43bdb7d better variable names 07 March 2018, 13:15:56 UTC
7518022 - 06 March 2018, 15:34:12 UTC
002c195 - 05 March 2018, 15:07:12 UTC
e76c57d - 02 March 2018, 19:44:36 UTC
e6c3564 induction scheme for drecords 02 March 2018, 19:41:28 UTC
0acd11c - 02 March 2018, 14:38:46 UTC
cba360f - 01 March 2018, 17:43:32 UTC
8c89ae8 - 28 February 2018, 13:01:43 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
e2879a1 27 February 2018, 14:45:50 UTC
96b0ca3 - 27 February 2018, 14:18:04 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
ae51632 19 February 2018, 13:32:08 UTC
5b2f5a7 update copyrights 12 February 2018, 17:08:40 UTC
e300f4f 06 February 2018, 13:54:02 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
9e231d4 Printing of a Dynamic Record 04 February 2018, 16:49:10 UTC
316fc53 -8 warnings 01 February 2018, 14:54:07 UTC
97f611c typing of polymorphic record types 01 February 2018, 11:37:48 UTC
7a7139a parsing polymorphic records 01 February 2018, 10:27:05 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
00cc7d0 intermediary stuff 28 July 2017, 09:58:12 UTC
back to top