https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
8bceccd . 13 December 2017, 16:30:02 UTC
3a67d24 get stmt from env 13 December 2017, 16:21:43 UTC
2691c6b . 12 December 2017, 18:01:18 UTC
fa26463 . 12 December 2017, 14:42:13 UTC
aa993b1 . 08 December 2017, 17:01:33 UTC
8ee0ec4 instanceAdv : replace local variables do not work 08 December 2017, 12:56:46 UTC
ca3dd67 instance adversary 06 December 2017, 17:43:15 UTC
475f60d i forgot to commit & push 05 December 2017, 16:27:21 UTC
8853b38 forgot the file ecTestMatching.ml 13 November 2017, 10:20:34 UTC
1dc5aaf "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 minor changes 10 November 2017, 12:07:56 UTC
a2bd95d quantifs & binds added to matches a named pattern cannot have the same ident as a binding 08 November 2017, 16:29:40 UTC
779581f val pattern_of_form : bindings -> form -> pattern (first shot in implementation) 03 November 2017, 14:26:55 UTC
7c59f91 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 comments erased 31 October 2017, 10:12:53 UTC
b878e37 second short for patterns + ecTrashTest that propose 4 tests 30 October 2017, 14:35:24 UTC
f662881 store BasicNamed construction 26 October 2017, 14:48:23 UTC
7dfb639 keyword "test" -> keyword "test_pattern" 26 October 2017, 07:46:39 UTC
df2c68f first shot on patterns + 1 test in ecTrashTest 25 October 2017, 16:18:05 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
13e9173 Check validity of obtained named from a theory cloning renaming. [fix #17354] 27 July 2017, 06:23:37 UTC
058bd27 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 Lining definitions up for OAEP. 25 July 2017, 17:16:19 UTC
b4c2a37 bound the probability that an adversary distinguish between the oracle x <@ d \ X and x <@ d 24 July 2017, 17:18:23 UTC
e401883 more info when local lemma fail. 24 July 2017, 17:18:23 UTC
ddf604b Fixing vonNeumann 24 July 2017, 17:17:56 UTC
f173dc4 "Fixing" PRP<->PRF lemmas 24 July 2017, 17:15:18 UTC
e456402 fix some theories 21 July 2017, 13:32:33 UTC
3e10ebb restart the proof of cramershoup 21 July 2017, 13:32:33 UTC
d831de8 more lemma on distribution 21 July 2017, 13:32:33 UTC
7dccbf0 Fix error in the definition of PKE (cstar was not initialised) 21 July 2017, 13:32:33 UTC
78c7d52 add the ceil and floor functions 21 July 2017, 13:32:33 UTC
ebadb1b fix bug in bypr and put some condition in the good order. 21 July 2017, 13:32:33 UTC
e425db8 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 Hash ElGamal (Generic): ported. 11 July 2017, 14:55:24 UTC
0fb20bc VonNeumann: ported. 11 July 2017, 12:49:01 UTC
e4cdb04 BR93: use \in for sets. 11 July 2017, 12:38:21 UTC
183c9a5 FSet: add \in notation 11 July 2017, 12:26:05 UTC
b2071e1 PRG: more nits 11 July 2017, 12:16:41 UTC
1558277 (Hashed) ElGamal: ported 11 July 2017, 12:16:17 UTC
204eb6f PRG: pWhile assignment notation 11 July 2017, 07:03:26 UTC
d8d89a3 BR93: removing progress. 10 July 2017, 09:26:20 UTC
765d68c PRG: ported. 10 July 2017, 09:26:11 UTC
ce8d888 BR93: cleanup, limiting smt, clarity. 10 July 2017, 08:01:07 UTC
a73ed57 BR93: further cleanup and lib extensions 07 July 2017, 21:33:02 UTC
6390747 MEE-CBC: Ported? 04 July 2017, 22:46:09 UTC
5068ae6 BR93: Fixed after stdlib changes. 04 July 2017, 21:55:50 UTC
7af9061 Theory Word: clone MFinite rather than ad hoc redef 04 July 2017, 20:46:26 UTC
e6cd83e BR93: use BitWord, some renaming AWord is deprecated and should not be used. 04 July 2017, 19:22:11 UTC
a2ad181 BR93: ported 04 July 2017, 09:34:05 UTC
dea2238 Docker doc box 28 June 2017, 08:15:23 UTC
0f658e6 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 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 API: generic tree regexp matcher. 15 June 2017, 08:19:25 UTC
8c21183 Misc: add explicit entry point for EC 15 June 2017, 08:05:54 UTC
449d0f2 Internals: remove unimplemented `ByPattern case for [inline] 15 June 2017, 08:05:25 UTC
d49a3f6 Travis 13 June 2017, 20:31:03 UTC
1953e05 Column/lineno pretty-printer for statements 02 June 2017, 08:17:14 UTC
908afa4 README.md: Fix opam prefix 17 May 2017, 14:12:10 UTC
7cb1468 README 26 April 2017, 17:17:47 UTC
a8c2c61 List: all_count_in 07 April 2017, 12:08:01 UTC
b4866ca Travis: reporting 27 March 2017, 12:31:22 UTC
1079832 Use “is_lossless” and "predT" in rnd rules instead of their expansions 24 March 2017, 13:19:27 UTC
4950e67 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 Merging NewLogic & Logic, removing old API 21 March 2017, 19:45:23 UTC
91d7e7d Fix all admits in Tuple 20 March 2017, 19:14:22 UTC
17ab666 Switching EasyCrypt && stdlib to new distributions library 20 March 2017, 15:33:59 UTC
ebd097f Fixing all admits in List 20 March 2017, 09:19:34 UTC
061186a Restore PrimeField.ec 19 March 2017, 21:59:49 UTC
221aca5 Remove unused theories 19 March 2017, 21:04:37 UTC
32a4616 increase default timeout 19 March 2017, 18:14:19 UTC
451b29d Travis: check examples 19 March 2017, 18:05:54 UTC
acdc38f Move all examples in examples/old/ Have to be moved back when ported. 19 March 2017, 18:03:08 UTC
abd8e9a Adapt stdlib to new Int.ec 19 March 2017, 13:50:37 UTC
ec2fa26 Splitting and fixing Int.ec 19 March 2017, 13:37:14 UTC
d09c1a7 Killing admits in StdBigop. 19 March 2017, 10:53:21 UTC
67e0bba [bigop]: big_flatten 19 March 2017, 10:53:13 UTC
4b2cc9e [list]: basic facts on `count` (count_pred0_eq, count_pred_eq) 19 March 2017, 10:53:01 UTC
91de244 add surjective predicate 19 March 2017, 10:22:14 UTC
aa1442d [bigop]: perm_eq_big_map 19 March 2017, 10:21:37 UTC
back to top