https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
4bcb388 20 December 2017, 13:51:13 UTC
ee3d6a1 Merge branch '1.0' into deploy-theory-matrix 20 December 2017, 13:45:34 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
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
6652128 Merge branch '1.0' into deploy-theory-matrix 20 March 2017, 19:18:27 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
back to top