https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
3f7727c easycrypt.opam 23 November 2021, 09:37:12 UTC
bde5d35 [depends] yaml 22 November 2021, 17:49:47 UTC
f8514a6 remove ocamlbuild.ml 22 November 2021, 17:48:42 UTC
50dae1b [build] install runtest (as ec-runtest) 21 November 2021, 16:30:31 UTC
3476312 script for graphing a dependency graph for .eco 19 November 2021, 10:53:40 UTC
08ed0c2 New format for eco (v3) Store whether a theory has been directly required or not. 19 November 2021, 07:18:46 UTC
471ea3b foo 19 November 2021, 07:04:08 UTC
a549eb4 Add an option to define opaque operators This can be done by adding the "opaque" tag, e.g.: op [opaque] myop = ... solve #94 19 November 2021, 06:27:09 UTC
10e1563 remove \# files 19 November 2021, 06:09:01 UTC
ffe0656 New command: locate [partial-qualid] This command allows to locate and print the fullname & shortest name of an operator, a lemma or a type declaration. fix #82 18 November 2021, 14:23:49 UTC
92f23db Add the project name in dune-project This is needed by "dune subst" ref #99 18 November 2021, 12:06:45 UTC
5e3929a remove debugging code 18 November 2021, 12:06:09 UTC
17e143c 17 November 2021, 15:41:35 UTC
b38a5aa 17 November 2021, 15:39:37 UTC
dfb413d fix opam package (do not do "dune subst") 17 November 2021, 15:35:07 UTC
0a2d4ad [build] use dune to install & find resources 17 November 2021, 08:23:14 UTC
31ce231 [SmtMap] add has, find and some lemmas these are focused on a specific proof and deserve expanding, fleshing out and cleaning up 17 November 2021, 07:51:50 UTC
229ac7a Remove EcFortune 17 November 2021, 06:24:47 UTC
02082bd Update copyright 17 November 2021, 06:22:22 UTC
e7d401f remove the script for creating tarballs 17 November 2021, 06:01:10 UTC
e46ef74 disable warning as errors 17 November 2021, 05:57:03 UTC
a54cec2 remove deprecated functions and reenable warning 3 17 November 2021, 05:52:23 UTC
b7a2ee2 reenable warning 39 17 November 2021, 05:43:59 UTC
4217836 reenable warning 38 17 November 2021, 05:41:36 UTC
061e164 reenable warning 35 17 November 2021, 05:40:28 UTC
43a1b9f reenable warning 34 17 November 2021, 05:39:17 UTC
5b09921 reenable warning 6 17 November 2021, 05:34:48 UTC
003fc41 [build] only consider src/theories/examples are deps 17 November 2021, 05:34:23 UTC
df78b65 .gitignore (.eca at root) 17 November 2021, 05:34:13 UTC
f8d5b79 Merge pull request #31 from ejgallego/1.0+dune [build] Add basic dune support 16 November 2021, 18:32:37 UTC
e39463d .gitignore: cleanup 16 November 2021, 17:37:59 UTC
68bbd4b [nix] update dependencies 16 November 2021, 17:35:05 UTC
f7c671c [build] use dune in Makefile 16 November 2021, 17:35:05 UTC
5334126 [build] do not create an internal EC library we do not currently expose any stable API. 16 November 2021, 17:35:05 UTC
3f13dec Use the old build system in opam. 16 November 2021, 17:35:04 UTC
fd804d6 [build] Add basic dune support Add experimental support for buidling `ec` using dune. Use ``` dune build ``` We don't add support for building the stdlib yet. 16 November 2021, 17:35:04 UTC
743a247 [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t 16 November 2021, 17:35:04 UTC
4b604bf renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 16 November 2021, 17:35:04 UTC
ab62416 adapt to consistent use of mu1 16 November 2021, 17:35:04 UTC
15946aa use mu1 instead of mass in in Distr 16 November 2021, 17:35:04 UTC
5a0238b [ci] do not send a slack message for PR from forked repo These PR do not have access to the webhook.t 16 November 2021, 16:56:20 UTC
ec1f979 Merge pull request #88 from EasyCrypt/deploy-mu1 Consistently use `mu1` instead of `mass`. 09 November 2021, 16:32:05 UTC
e770f0f Refactor & generalize the section mechanism the section mechanism has been refactored s.t. it provides a more uniform interface where any kind of declaration can be marked as local / declared and erased / generalized when the section is closed. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> 09 November 2021, 15:36:49 UTC
b0e609d Fix the pretty printing of \ as a binop fix #93 05 November 2021, 15:08:07 UTC
b37085c renamings: dletE[_swap] -> dlet_muE[_swap] and dletE_mu -> dletE 04 November 2021, 14:56:36 UTC
d5d3d94 adapt to consistent use of mu1 04 November 2021, 12:09:30 UTC
6676710 use mu1 instead of mass in in Distr 04 November 2021, 12:06:45 UTC
b9c7685 comments, renaming, proof* 04 November 2021, 10:00:49 UTC
4da60d2 allow sdist-distinguishers for ROs to call sample and set 04 November 2021, 10:00:49 UTC
8a26fe5 some more simplifications 04 November 2021, 10:00:49 UTC
6851729 remove weight equality side conditions 04 November 2021, 10:00:49 UTC
a21c135 implement feedback from review 04 November 2021, 10:00:49 UTC
570f090 fix compilation 04 November 2021, 10:00:49 UTC
7fcfa1d move lemmas from SDist to RealSeries and Distr, rename summableM 04 November 2021, 10:00:49 UTC
f1d2f19 use PROM rather than ROM 04 November 2021, 10:00:49 UTC
051cb1d sdist for ROM distinguishers and N distinct queries 04 November 2021, 10:00:49 UTC
f5d072e reduction from N to 1 oracle call for sdist distinguisher 04 November 2021, 10:00:49 UTC
3adc9c8 sdist distinguisher for single oracle call + reduction to single sampling 04 November 2021, 10:00:49 UTC
62e1ce7 connection between sdist and distinguisher procedures 04 November 2021, 10:00:49 UTC
4529cfc statitical distance and some lemmas 04 November 2021, 10:00:49 UTC
aa6dc07 Add a simple form of pattern selection in rewrite rules Syntax is: `rewrite [pattern]rule` In this form, `pattern` is first searched against the current goal and rule LHS is then matched against the instanciated pattern. E.g. `rewrite [y+_]addrC` will instantiate `addrC` to `y` and `z` assuming that the first match of `y+_` in the current goal is `y+z`. This syntax is compatible with other variants: `rewrite -{2}[y+_]addrC` 19 October 2021, 10:19:36 UTC
4afdfe9 change "smt in rewrite" syntax New syntax is: - rewrite #smt - rewrite #smt:(db) - rewrite #smt:[options] 18 October 2021, 12:52:42 UTC
7b8aa43 Compute free program variables in *hoare statements. Fix #83 18 October 2021, 08:03:55 UTC
c854989 Implement "gen have" & "wlog suff" Fix #77 12 October 2021, 13:39:31 UTC
c132a25 StdLib: summability of partitioning 08 October 2021, 12:09:35 UTC
3ffc3be Some lemmas for floor and ceil, in particular letting one rewrite floor x and ceil x. 07 October 2021, 06:39:26 UTC
0656ac7 Added disjoint xs ys as an abbreviation for xs `&` ys = fset0. Added lemma disjointP (xs ys : 'a fset): disjoint xs ys <=> forall (x : 'a), x \in xs => ! x \in ys. 04 October 2021, 07:24:14 UTC
c07e880 Fix global positions reporting 06 September 2021, 09:47:40 UTC
512f0f2 [docker] get CVC4 from a more stable URL 30 June 2021, 14:43:36 UTC
489ff17 default.nix 30 June 2021, 10:01:04 UTC
410f882 improve default.nix 28 June 2021, 10:11:24 UTC
692a017 remove duplicate eq_in_count/eq_count_in, keep eq_in_count 09 June 2021, 06:26:37 UTC
1890ad1 Update README.md 08 June 2021, 19:43:54 UTC
73afe4f improve error msg for proc 04 June 2021, 05:35:25 UTC
aeac2d4 Fix: cleanup exact hint DB after clone 27 May 2021, 10:03:14 UTC
eb6ce7c [stdlib] Array: fix set_set_swap 26 May 2021, 15:07:59 UTC
4dbdb88 Extend cloning with - inline but keep override (<=) - override theories 26 May 2021, 07:20:22 UTC
16e5d3b remove 'search' commands 25 May 2021, 12:40:30 UTC
aae9601 Merge pull request #67 from EasyCrypt/merge-chachapoly Soft-merge chachapoly proof and its stdlib changes We'll want to consider shifting the generic arguments on SKE (EUF-CMA + IND-CPA ⇒ IND-CCA) into standard libraries. 20 May 2021, 16:48:40 UTC
f30e424 Some nits in the new SmtMap lemmas 20 May 2021, 16:31:22 UTC
c750a58 FinType.FinType → FinType 20 May 2021, 09:59:20 UTC
82fd774 Shift some results to SmtMap Shift specific map-merging strategies from SplitRO to SmtMap. The `pair` strategy now does a product (with None as zero). 20 May 2021, 09:26:40 UTC
edd02d0 ChaCha-Poly x Easter He has risen! Authored by Benjamin Grégoire and Cécile Baritel-Ruet. Co-Authored-By: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-Authored-By: Cécile Baritel-Ruet <cecile.baritel-ruet@inria.fr> 18 May 2021, 22:22:47 UTC
8774376 Library work towards soft-merge of ChaCha-Poly 18 May 2021, 22:17:02 UTC
ba45bb5 Merge pull request #63 from EasyCrypt/deploy-clean-oldmonoid StdLib: Remove old Monoid dependency, port Hybrid argument to Bigops 26 April 2021, 12:10:43 UTC
14216cb fix default.nix 18 April 2021, 14:12:06 UTC
1313a7d Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid 14 April 2021, 18:20:13 UTC
49d7ad3 'Cleanup' but it's mostly shifting things around 14 April 2021, 15:32:51 UTC
2afb775 StdLib: funi + same weight => eq 14 April 2021, 15:27:25 UTC
d809ef8 StdLib: use bigops in generic Hybrid This instantiates BigOp for Booleans (with xor, or, and and) and gets rid of the old Monoid library, which Hybrid arguments relied upon. Some proof cleaning left to do in Hybrid, Indist, and PKE_Hybrid. 13 April 2021, 15:50:46 UTC
5df6a6f StdLib: basic facts on distributions 13 April 2021, 13:34:33 UTC
1b25ed4 Fix bug in theory renamings 12 April 2021, 09:31:13 UTC
40d1950 StdLib: ZModP: finite + uniform distribution 12 April 2021, 06:10:36 UTC
7ad9727 StdLib: linking sampling in Z/pZ and Z/qZ when q|p 11 April 2021, 13:06:28 UTC
c6ad4b1 StdLib: Poly: killing last admits 10 April 2021, 14:05:38 UTC
81f358d StdLib: polynomials distributions 10 April 2021, 10:47:47 UTC
639a76e StdLib: lead coeff. and degree of X^n+1 09 April 2021, 20:10:53 UTC
8e6dd9a StdLib: ring quotient for non-integral domains 09 April 2021, 18:16:22 UTC
6a4bbab StdLib: ring regular element + poly over non integral domains 09 April 2021, 16:55:55 UTC
9e43d2c StdLib: more results on pmin 09 April 2021, 15:30:53 UTC
back to top