8bceccd | Cécile BARITEL-RUET | 13 December 2017, 16:30:02 UTC | . | 13 December 2017, 16:30:02 UTC |
3a67d24 | Cécile BARITEL-RUET | 13 December 2017, 16:21:43 UTC | get stmt from env | 13 December 2017, 16:21:43 UTC |
2691c6b | Cécile BARITEL-RUET | 12 December 2017, 18:01:18 UTC | . | 12 December 2017, 18:01:18 UTC |
fa26463 | Cécile BARITEL-RUET | 12 December 2017, 14:42:13 UTC | . | 12 December 2017, 14:42:13 UTC |
aa993b1 | Cécile BARITEL-RUET | 08 December 2017, 17:01:33 UTC | . | 08 December 2017, 17:01:33 UTC |
8ee0ec4 | Cécile BARITEL-RUET | 08 December 2017, 12:56:46 UTC | instanceAdv : replace local variables do not work | 08 December 2017, 12:56:46 UTC |
ca3dd67 | Cécile BARITEL-RUET | 06 December 2017, 17:43:15 UTC | instance adversary | 06 December 2017, 17:43:15 UTC |
475f60d | Cécile BARITEL-RUET | 05 December 2017, 16:27:21 UTC | i forgot to commit & push | 05 December 2017, 16:27:21 UTC |
8853b38 | Cécile BARITEL-RUET | 13 November 2017, 10:20:34 UTC | forgot the file ecTestMatching.ml | 13 November 2017, 10:20:34 UTC |
1dc5aaf | Cécile BARITEL-RUET | 13 November 2017, 10:12:22 UTC | "rewrite<*> lemma_name" is a test command for matches works with the symbols Pr Next steps : include strategies/reductions/higher order | 13 November 2017, 10:12:22 UTC |
bc00e57 | Cécile BARITEL-RUET | 10 November 2017, 12:07:56 UTC | minor changes | 10 November 2017, 12:07:56 UTC |
a2bd95d | Cécile BARITEL-RUET | 08 November 2017, 16:29:40 UTC | quantifs & binds added to matches a named pattern cannot have the same ident as a binding | 08 November 2017, 16:29:40 UTC |
779581f | Cécile BARITEL-RUET | 03 November 2017, 14:26:55 UTC | val pattern_of_form : bindings -> form -> pattern (first shot in implementation) | 03 November 2017, 14:26:55 UTC |
7c59f91 | Cécile BARITEL-RUET | 02 November 2017, 16:46:44 UTC | Name = String => EcIdent matches = (form | memory | mpath | xpath) map.t TODO : - add xpath/mpath patterns - add hyps (and its env inside) in the engine context to replace f_equal by reduction - add bindings to t_matches | 02 November 2017, 16:46:44 UTC |
dc41379 | Cécile BARITEL-RUET | 31 October 2017, 10:12:53 UTC | comments erased | 31 October 2017, 10:12:53 UTC |
b878e37 | Cécile BARITEL-RUET | 30 October 2017, 14:35:24 UTC | second short for patterns + ecTrashTest that propose 4 tests | 30 October 2017, 14:35:24 UTC |
f662881 | Cécile BARITEL-RUET | 26 October 2017, 14:48:23 UTC | store BasicNamed construction | 26 October 2017, 14:48:23 UTC |
7dfb639 | Cécile BARITEL-RUET | 26 October 2017, 07:46:39 UTC | keyword "test" -> keyword "test_pattern" | 26 October 2017, 07:46:39 UTC |
df2c68f | Cécile BARITEL-RUET | 25 October 2017, 16:18:05 UTC | first shot on patterns + 1 test in ecTrashTest | 25 October 2017, 16:18:05 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 |
1953e05 | Pierre-Yves Strub | 02 June 2017, 08:17:00 UTC | Column/lineno pretty-printer for statements | 02 June 2017, 08:17:14 UTC |
908afa4 | Francois Dupressoir | 17 May 2017, 14:12:10 UTC | README.md: Fix opam prefix | 17 May 2017, 14:12:10 UTC |
7cb1468 | Pierre-Yves Strub | 26 April 2017, 17:17:47 UTC | README | 26 April 2017, 17:17:47 UTC |
a8c2c61 | Pierre-Yves Strub | 07 April 2017, 12:08:01 UTC | List: all_count_in | 07 April 2017, 12:08:01 UTC |
b4866ca | Pierre-Yves Strub | 27 March 2017, 12:30:31 UTC | Travis: reporting | 27 March 2017, 12:31:22 UTC |
1079832 | Benjamin Gregoire | 24 March 2017, 13:19:27 UTC | Use “is_lossless” and "predT" in rnd rules instead of their expansions | 24 March 2017, 13:19:27 UTC |
4950e67 | Benjamin Gregoire | 22 March 2017, 08:55:29 UTC | add the “selected” option to smt tactic the option prints the list of selected lemmas which are sent to smt. | 22 March 2017, 08:59:38 UTC |
4f24928 | Pierre-Yves Strub | 21 March 2017, 19:45:07 UTC | Merging NewLogic & Logic, removing old API | 21 March 2017, 19:45:23 UTC |
91d7e7d | Pierre-Yves Strub | 20 March 2017, 19:14:22 UTC | Fix all admits in Tuple | 20 March 2017, 19:14:22 UTC |
17ab666 | Benjamin Gregoire | 20 March 2017, 15:33:59 UTC | Switching EasyCrypt && stdlib to new distributions library | 20 March 2017, 15:33:59 UTC |
ebd097f | Pierre-Yves Strub | 20 March 2017, 09:19:34 UTC | Fixing all admits in List | 20 March 2017, 09:19:34 UTC |
061186a | Pierre-Yves Strub | 19 March 2017, 21:59:49 UTC | Restore PrimeField.ec | 19 March 2017, 21:59:49 UTC |
221aca5 | Pierre-Yves Strub | 19 March 2017, 21:04:37 UTC | Remove unused theories | 19 March 2017, 21:04:37 UTC |
32a4616 | Pierre-Yves Strub | 19 March 2017, 18:14:19 UTC | increase default timeout | 19 March 2017, 18:14:19 UTC |
451b29d | Pierre-Yves Strub | 19 March 2017, 18:05:54 UTC | Travis: check examples | 19 March 2017, 18:05:54 UTC |
acdc38f | Pierre-Yves Strub | 19 March 2017, 18:03:08 UTC | Move all examples in examples/old/ Have to be moved back when ported. | 19 March 2017, 18:03:08 UTC |
abd8e9a | Pierre-Yves Strub | 19 March 2017, 13:50:37 UTC | Adapt stdlib to new Int.ec | 19 March 2017, 13:50:37 UTC |
ec2fa26 | Pierre-Yves Strub | 19 March 2017, 13:37:00 UTC | Splitting and fixing Int.ec | 19 March 2017, 13:37:14 UTC |
d09c1a7 | Pierre-Yves Strub | 19 March 2017, 10:53:21 UTC | Killing admits in StdBigop. | 19 March 2017, 10:53:21 UTC |
67e0bba | Pierre-Yves Strub | 19 March 2017, 10:53:13 UTC | [bigop]: big_flatten | 19 March 2017, 10:53:13 UTC |
4b2cc9e | Pierre-Yves Strub | 19 March 2017, 10:53:01 UTC | [list]: basic facts on `count` (count_pred0_eq, count_pred_eq) | 19 March 2017, 10:53:01 UTC |
91de244 | Benjamin Gregoire | 18 March 2017, 17:14:16 UTC | add surjective predicate | 19 March 2017, 10:22:14 UTC |
aa1442d | Pierre-Yves Strub | 19 March 2017, 10:21:37 UTC | [bigop]: perm_eq_big_map | 19 March 2017, 10:21:37 UTC |