https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
ce71c7f More reduction for le/lt (real) 07 November 2017, 08:25:14 UTC
de413c6 bug-fix 07 November 2017, 08:09:28 UTC
24a865d More reduction for le/lt (int) 07 November 2017, 07:04:50 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
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
5e3445f [list]: perm_eq_rev 19 March 2017, 10:14:37 UTC
54d6905 add lemma on big and < 19 March 2017, 10:09:31 UTC
3a7368f Makefile: fix deps-a 18 March 2017, 11:30:18 UTC
back to top