36f7f5a | Alley Stoughton | 21 February 2018, 22:32:02 UTC | 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 | François Dupressoir | 23 February 2018, 12:20:12 UTC | SmtMap: rng and basic results | 24 February 2018, 08:13:05 UTC |
9f07d02 | Pierre-Yves Strub | 23 February 2018, 08:37:48 UTC | SmtMap : fdom and related results | 24 February 2018, 08:12:44 UTC |
dd27d32 | François Dupressoir | 22 February 2018, 10:57:52 UTC | whitespace | 22 February 2018, 10:57:52 UTC |
850f427 | Pierre-Yves Strub | 21 February 2018, 16:09:18 UTC | SMT backed map/fmap | 21 February 2018, 16:09:18 UTC |
6c010d0 | Pierre-Yves Strub | 21 February 2018, 15:25:06 UTC | Travis/Docker : sync UID/GID + fix reports publication | 21 February 2018, 15:26:26 UTC |
459d1a1 | François Dupressoir | 21 February 2018, 10:22:19 UTC | focusing smt calls in hashed ElGamal | 21 February 2018, 10:22:19 UTC |
f033f81 | Vincent Laporte | 21 February 2018, 07:28:00 UTC | 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 | Pierre-Yves Strub | 12 February 2018, 17:08:40 UTC | update copyrights | 12 February 2018, 17:08:40 UTC |
b622d44 | Pierre-Yves Strub | 05 February 2018, 10:30:53 UTC | Docker: force OCaml version 4.03 | 05 February 2018, 10:30:53 UTC |
2ad5a58 | Pierre-Yves Strub | 04 February 2018, 17:12:04 UTC | remove Docker file for aprhl-test-box | 05 February 2018, 10:30:30 UTC |
25c632b | Pierre-Yves Strub | 21 January 2018, 23:32:19 UTC | 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 | François Dupressoir | 19 January 2018, 21:32:01 UTC | documenting br93 further | 19 January 2018, 21:32:01 UTC |
1bca807 | François Dupressoir | 19 January 2018, 17:51:31 UTC | speed PIR example up | 19 January 2018, 17:51:31 UTC |
26b6fd9 | Pierre-Yves Strub | 18 January 2018, 21:21:37 UTC | 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 | Pierre-Yves Strub | 19 December 2017, 11:17:37 UTC | 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 | Benjamin Gregoire | 18 December 2017, 12:13:27 UTC | more ways to do the proof | 18 December 2017, 12:13:47 UTC |
34d6e51 | Pierre-Yves Strub | 14 December 2017, 12:26:29 UTC | New IP: //> & ||> The IP //> & ||> are equivalent to /> & |> but use a stronger resolution tactic. | 14 December 2017, 12:26:45 UTC |
ddc2701 | Benjamin Gregoire | 14 December 2017, 10:38:21 UTC | Add alternative proof in PIR. | 14 December 2017, 10:38:21 UTC |
fe76f33 | Benjamin Gregoire | 14 December 2017, 10:37:55 UTC | more lemmas on FSet.oflist | 14 December 2017, 10:37:55 UTC |
527d9ad | Benjamin Gregoire | 08 December 2017, 14:56:08 UTC | add new example: Private information retrieval. | 08 December 2017, 14:56:08 UTC |
89618eb | Pierre-Yves Strub | 15 November 2017, 06:54:48 UTC | 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 | François Dupressoir | 14 November 2017, 14:04:42 UTC | Minimal attempt at stabilising Hybrid | 14 November 2017, 14:04:42 UTC |
9bdd6dd | François Dupressoir | 14 November 2017, 13:34:09 UTC | More stabilising smt in ROM | 14 November 2017, 13:34:09 UTC |
2f6312c | François Dupressoir | 13 November 2017, 17:02:56 UTC | Stabilise smt in old ROM.ec | 13 November 2017, 17:06:47 UTC |
b95b795 | Pierre-Yves Strub | 13 November 2017, 15:06:41 UTC | In ROM.ec, help `smt` by using `move=> />`. | 13 November 2017, 15:19:53 UTC |
0c14bcb | Pierre-Yves Strub | 13 November 2017, 14:46:37 UTC | More on (zmodule) exponential & ordering. | 13 November 2017, 15:19:53 UTC |
d3dcd49 | Pierre-Yves Strub | 09 November 2017, 23:27:41 UTC | 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 | Pierre-Yves Strub | 07 November 2017, 09:14:11 UTC | Strengthen reduction for le/lt (int/real) | 07 November 2017, 09:14:11 UTC |
7721333 | Alley Stoughton | 05 November 2017, 08:09:52 UTC | 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 | Pierre-Yves Strub | 04 November 2017, 22:36:30 UTC | docker: add support for sphinx in the doc-box. | 04 November 2017, 22:36:30 UTC |
c7988e8 | Pierre-Yves Strub | 04 November 2017, 22:35:35 UTC | keywords script: add support for python output. | 04 November 2017, 22:35:35 UTC |
d492fcd | Pierre-Yves Strub | 27 October 2017, 07:14:18 UTC | Libraries: distributions: killing more admits | 27 October 2017, 07:14:18 UTC |
65dfe3c | Pierre-Yves Strub | 27 October 2017, 07:03:50 UTC | Libraries: refactoring + killing admits. | 27 October 2017, 07:03:50 UTC |
ab29b3b | Pierre-Yves Strub | 26 October 2017, 21:55:18 UTC | Libraries: distr: killing admits | 26 October 2017, 21:55:18 UTC |
3f125db | Pierre-Yves Strub | 23 October 2017, 07:51:11 UTC | 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 | Pierre-Yves Strub | 23 October 2017, 07:49:57 UTC | Libraries: extra facts on iterated multiplication. | 23 October 2017, 07:49:57 UTC |
caf9b25 | Pierre-Yves Strub | 23 October 2017, 04:32:43 UTC | Libraries: solving 2nd degree real polynomials. | 23 October 2017, 04:32:43 UTC |
fd7a34f | Pierre-Yves Strub | 23 October 2017, 04:28:35 UTC | Libraries: link Real.(^) with generic one. | 23 October 2017, 04:28:35 UTC |
fb22315 | Pierre-Yves Strub | 23 October 2017, 04:26:57 UTC | Libraries: extra facts on the square root. | 23 October 2017, 04:26:57 UTC |
280f627 | Pierre-Yves Strub | 23 October 2017, 03:51:09 UTC | Add [field] as a rewrite tactic. | 23 October 2017, 03:51:09 UTC |
2d97328 | Pierre-Yves Strub | 23 October 2017, 02:56:49 UTC | build script: pass ECBRANCH to docker | 23 October 2017, 02:56:49 UTC |
3b4aeec | Pierre-Yves Strub | 12 October 2017, 13:17:20 UTC | New facts on lists | 12 October 2017, 13:17:20 UTC |
8999c70 | Pierre-Yves Strub | 12 October 2017, 12:50:02 UTC | New facts on lists | 12 October 2017, 12:50:02 UTC |
cfa0695 | Pierre-Yves Strub | 12 October 2017, 11:24:33 UTC | Few facts on <= and exp | 12 October 2017, 11:24:33 UTC |
56964f5 | Pierre-Yves Strub | 10 October 2017, 07:04:02 UTC | Update installation instructions for Windows (using opam). | 10 October 2017, 07:04:02 UTC |
10a2fc7 | Pierre-Yves Strub | 10 October 2017, 07:03:49 UTC | Binary packages automatisation scripts. | 10 October 2017, 07:03:49 UTC |
89fb774 | François Dupressoir | 02 August 2017, 16:25:38 UTC | exclude examples/incomplete recursively | 28 September 2017, 11:37:51 UTC |
7cee24f | François Dupressoir | 02 August 2017, 16:25:11 UTC | Support recursive exclusions in test targets | 28 September 2017, 11:37:51 UTC |
44ae0e6 | François Dupressoir | 25 August 2017, 09:35:52 UTC | typo in error message (ecHiGoal) | 25 August 2017, 09:36:18 UTC |
3e7dc31 | François Dupressoir | 21 August 2017, 16:29:20 UTC | moving ahead - some admits in FEL application | 21 August 2017, 16:29:20 UTC |
ac19323 | François Dupressoir | 11 August 2017, 16:15:49 UTC | oaep: experimenting with fel flexibility and style | 11 August 2017, 16:15:49 UTC |
2a78686 | François Dupressoir | 11 August 2017, 16:15:05 UTC | typos in Distr (comments) | 11 August 2017, 16:15:05 UTC |
379e448 | François Dupressoir | 10 August 2017, 21:33:27 UTC | oaep: some progress | 10 August 2017, 21:33:31 UTC |
9329d72 | François Dupressoir | 03 August 2017, 15:36:15 UTC | oaep: exploring useful intermediate lemmas | 03 August 2017, 15:36:15 UTC |
a2de959 | François Dupressoir | 02 August 2017, 15:25:38 UTC | Cleanup in examples: deleting some, porting some. | 02 August 2017, 15:25:38 UTC |
c589262 | François Dupressoir | 31 July 2017, 11:27:25 UTC | OAEP progress | 31 July 2017, 11:27:39 UTC |
68f7b62 | Benjamin Gregoire | 28 July 2017, 10:22:23 UTC | remove garbage | 28 July 2017, 10:22:23 UTC |
d5c7c6e | Benjamin Gregoire | 28 July 2017, 09:57:53 UTC | full proof of cramer shoup :-) | 28 July 2017, 09:58:12 UTC |
00a61be | Benjamin Gregoire | 28 July 2017, 06:05:18 UTC | new theory allowing to switch from a sampling d to a sampling d \ X | 28 July 2017, 09:58:12 UTC |
cbeb6f3 | Benjamin Gregoire | 28 July 2017, 06:04:26 UTC | more lemmas | 28 July 2017, 09:58:12 UTC |
55cc1ec | Benjamin Gregoire | 28 July 2017, 06:03:58 UTC | fix bug in typing of projection on tuple. case the tuple as type "glob M" | 28 July 2017, 09:58:12 UTC |
00cc7d0 | Benjamin Gregoire | 28 July 2017, 04:19:44 UTC | intermediary stuff | 28 July 2017, 09:58:12 UTC |
13e9173 | Pierre-Yves Strub | 27 July 2017, 06:23:30 UTC | Check validity of obtained named from a theory cloning renaming. [fix #17354] | 27 July 2017, 06:23:37 UTC |
058bd27 | Pierre-Yves Strub | 27 July 2017, 06:05:52 UTC | Fix bug in pretty printer. Fix printing of higher-order notation (not in eta-normal form). [fix #17355] | 27 July 2017, 06:05:52 UTC |
0c50716 | François Dupressoir | 25 July 2017, 17:12:23 UTC | Lining definitions up for OAEP. | 25 July 2017, 17:16:19 UTC |
b4c2a37 | Benjamin Gregoire | 24 July 2017, 17:18:07 UTC | bound the probability that an adversary distinguish between the oracle x <@ d \ X and x <@ d | 24 July 2017, 17:18:23 UTC |
e401883 | Benjamin Gregoire | 24 July 2017, 17:16:15 UTC | more info when local lemma fail. | 24 July 2017, 17:18:23 UTC |
ddf604b | François Dupressoir | 24 July 2017, 17:17:56 UTC | Fixing vonNeumann | 24 July 2017, 17:17:56 UTC |
f173dc4 | François Dupressoir | 24 July 2017, 17:15:18 UTC | "Fixing" PRP<->PRF lemmas | 24 July 2017, 17:15:18 UTC |
e456402 | Benjamin Gregoire | 21 July 2017, 13:32:24 UTC | fix some theories | 21 July 2017, 13:32:33 UTC |
3e10ebb | Benjamin Gregoire | 21 July 2017, 13:25:02 UTC | restart the proof of cramershoup | 21 July 2017, 13:32:33 UTC |
d831de8 | Benjamin Gregoire | 21 July 2017, 13:24:11 UTC | more lemma on distribution | 21 July 2017, 13:32:33 UTC |
7dccbf0 | Benjamin Gregoire | 21 July 2017, 13:23:51 UTC | Fix error in the definition of PKE (cstar was not initialised) | 21 July 2017, 13:32:33 UTC |
78c7d52 | Benjamin Gregoire | 21 July 2017, 13:21:38 UTC | add the ceil and floor functions | 21 July 2017, 13:32:33 UTC |
ebadb1b | Benjamin Gregoire | 21 July 2017, 13:21:02 UTC | fix bug in bypr and put some condition in the good order. | 21 July 2017, 13:32:33 UTC |
e425db8 | François Dupressoir | 19 July 2017, 21:52:54 UTC | BR93 example: refactor to illustrate instantiation More work is needed to clean definitions and final statement up. | 19 July 2017, 21:52:54 UTC |
c552f14 | François Dupressoir | 11 July 2017, 14:55:24 UTC | Hash ElGamal (Generic): ported. | 11 July 2017, 14:55:24 UTC |
0fb20bc | François Dupressoir | 11 July 2017, 12:49:01 UTC | VonNeumann: ported. | 11 July 2017, 12:49:01 UTC |
e4cdb04 | François Dupressoir | 11 July 2017, 12:38:21 UTC | BR93: use \in for sets. | 11 July 2017, 12:38:21 UTC |
183c9a5 | François Dupressoir | 11 July 2017, 12:26:05 UTC | FSet: add \in notation | 11 July 2017, 12:26:05 UTC |
b2071e1 | François Dupressoir | 11 July 2017, 12:16:41 UTC | PRG: more nits | 11 July 2017, 12:16:41 UTC |
1558277 | François Dupressoir | 11 July 2017, 12:16:17 UTC | (Hashed) ElGamal: ported | 11 July 2017, 12:16:17 UTC |
204eb6f | François Dupressoir | 11 July 2017, 07:03:26 UTC | PRG: pWhile assignment notation | 11 July 2017, 07:03:26 UTC |
d8d89a3 | François Dupressoir | 10 July 2017, 09:26:20 UTC | BR93: removing progress. | 10 July 2017, 09:26:20 UTC |
765d68c | François Dupressoir | 10 July 2017, 09:26:11 UTC | PRG: ported. | 10 July 2017, 09:26:11 UTC |
ce8d888 | François Dupressoir | 10 July 2017, 08:01:07 UTC | BR93: cleanup, limiting smt, clarity. | 10 July 2017, 08:01:07 UTC |
a73ed57 | François Dupressoir | 07 July 2017, 21:33:02 UTC | BR93: further cleanup and lib extensions | 07 July 2017, 21:33:02 UTC |
6390747 | François Dupressoir | 04 July 2017, 22:46:09 UTC | MEE-CBC: Ported? | 04 July 2017, 22:46:09 UTC |
5068ae6 | François Dupressoir | 04 July 2017, 21:55:50 UTC | BR93: Fixed after stdlib changes. | 04 July 2017, 21:55:50 UTC |
7af9061 | François Dupressoir | 04 July 2017, 20:46:22 UTC | Theory Word: clone MFinite rather than ad hoc redef | 04 July 2017, 20:46:26 UTC |
e6cd83e | François Dupressoir | 04 July 2017, 19:22:03 UTC | BR93: use BitWord, some renaming AWord is deprecated and should not be used. | 04 July 2017, 19:22:11 UTC |
a2ad181 | François Dupressoir | 04 July 2017, 09:33:49 UTC | BR93: ported | 04 July 2017, 09:34:05 UTC |
dea2238 | Pierre-Yves Strub | 28 June 2017, 08:15:23 UTC | Docker doc box | 28 June 2017, 08:15:23 UTC |
0f658e6 | Pierre-Yves Strub | 15 June 2017, 11:18:48 UTC | Bug fix in cloning. When aliasing a theory, do alias the constructors path of the enclosed datatypes. | 15 June 2017, 11:18:48 UTC |
d6e9a3c | Cécile BARITEL-RUET | 15 June 2017, 08:21:56 UTC | New tactic: `replace`. Extension to `transitivity` that allows to construct the intermediate program via pattern matching and back-references. | 15 June 2017, 08:21:56 UTC |
b1b1a1e | Pierre-Yves Strub | 15 June 2017, 08:19:25 UTC | API: generic tree regexp matcher. | 15 June 2017, 08:19:25 UTC |
8c21183 | Pierre-Yves Strub | 15 June 2017, 08:05:54 UTC | Misc: add explicit entry point for EC | 15 June 2017, 08:05:54 UTC |
449d0f2 | Pierre-Yves Strub | 15 June 2017, 08:05:25 UTC | Internals: remove unimplemented `ByPattern case for [inline] | 15 June 2017, 08:05:25 UTC |
d49a3f6 | Pierre-Yves Strub | 13 June 2017, 20:31:03 UTC | Travis | 13 June 2017, 20:31:03 UTC |