https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
f7b8664 Added Above Threshold and Report Noisy Max examples, which check with current version of branch. 30 June 2021, 15:32 UTC
9a5c2d6 Merge branch '1.0' into aprhl 30 June 2021, 09:35 UTC
aeac2d4 Fix: cleanup exact hint DB after clone 27 May 2021, 10:03 UTC
eb6ce7c [stdlib] Array: fix set_set_swap 26 May 2021, 15:07 UTC
4dbdb88 Extend cloning with - inline but keep override (<=) - override theories 26 May 2021, 07:20 UTC
16e5d3b remove 'search' commands 25 May 2021, 12:40 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 UTC
f30e424 Some nits in the new SmtMap lemmas 20 May 2021, 16:31 UTC
c750a58 FinType.FinType → FinType 20 May 2021, 09:59 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 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 UTC
8774376 Library work towards soft-merge of ChaCha-Poly 18 May 2021, 22:17 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 UTC
14216cb fix default.nix 18 April 2021, 14:12 UTC
1313a7d Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid 14 April 2021, 18:20 UTC
49d7ad3 'Cleanup' but it's mostly shifting things around 14 April 2021, 15:32 UTC
2afb775 StdLib: funi + same weight => eq 14 April 2021, 15:27 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 UTC
5df6a6f StdLib: basic facts on distributions 13 April 2021, 13:34 UTC
1b25ed4 Fix bug in theory renamings 12 April 2021, 09:31 UTC
40d1950 StdLib: ZModP: finite + uniform distribution 12 April 2021, 06:10 UTC
7ad9727 StdLib: linking sampling in Z/pZ and Z/qZ when q|p 11 April 2021, 13:06 UTC
c6ad4b1 StdLib: Poly: killing last admits 10 April 2021, 14:05 UTC
81f358d StdLib: polynomials distributions 10 April 2021, 10:47 UTC
639a76e StdLib: lead coeff. and degree of X^n+1 09 April 2021, 20:10 UTC
8e6dd9a StdLib: ring quotient for non-integral domains 09 April 2021, 18:16 UTC
6a4bbab StdLib: ring regular element + poly over non integral domains 09 April 2021, 16:55 UTC
9e43d2c StdLib: more results on pmin 09 April 2021, 15:30 UTC
7fbcff7 StdLib: few lemmas about polynomials 08 April 2021, 16:42 UTC
84c2618 Fix stdlib 08 April 2021, 13:48 UTC
a014668 StdLib: enumerating polynomials of a given degree 08 April 2021, 13:14 UTC
0a6485a StdLib: Finite: explicit witnesses for finitness + related lemmas on lists 08 April 2021, 13:13 UTC
81cd929 Stdlib: IntDiv - add a few lemmas 08 April 2021, 13:13 UTC
18e7bf4 Stdlib: more results on polynomials & ring ideals 08 April 2021, 07:15 UTC
83e39fd Prove that polynomials form an integral domain 07 April 2021, 14:44 UTC
6ce66c7 Include ring quotients th. in ideals th. 07 April 2021, 14:44 UTC
de2158b Poly.ec -> Poly.eca 07 April 2021, 12:32 UTC
a62a90d Stdlib: ring quotients 05 April 2021, 09:08 UTC
cf1eca8 Stdlib: fmin 05 April 2021, 06:43 UTC
1aab7a8 Quotient: use std def. of eqv relation 05 April 2021, 06:42 UTC
2a8554f Stdlib: simplify proofs in Quotient.ec 05 April 2021, 06:37 UTC
c404a43 Stdlib: ideas & a bit of abstract arithmetic 05 April 2021, 05:51 UTC
940fa12 List: fix admitted proofs 05 April 2021, 05:40 UTC
c5d0c62 List: size_eq1 05 April 2021, 05:39 UTC
432c181 README: fix why3 config command 04 April 2021, 17:54 UTC
0d55fac Merge branch '1.0' into aprhl 04 April 2021, 17:25 UTC
748c9ef remove doc-box 04 April 2021, 09:00 UTC
a0a0c9b Upgrade versions of supported provers 04 April 2021, 07:17 UTC
20a6183 Move to Why3 1.4 04 April 2021, 06:42 UTC
fb59000 CI: use workflow conclusion 03 April 2021, 19:32 UTC
7627a75 Move to GitHub Actions 03 April 2021, 17:32 UTC
8bcb1ae easycrypt.png 03 April 2021, 15:30 UTC
df9ab35 Stdlib: refactoring 02 April 2021, 20:27 UTC
91479fa Stdlib: integer log. 02 April 2021, 20:24 UTC
e8e6dc4 List: alltuples & allsubtuples 02 April 2021, 12:25 UTC
9c741f1 List: subseqs 02 April 2021, 11:52 UTC
30b7cae Finite types pred + finfun. Co-authored-by: Benjamin Grégoire <benjamin.gregoire@inria.fr> Co-authored-by: Pierre-Yves Strub <pierre-yves@strub.nu> 02 April 2021, 07:28 UTC
f2abfb4 Merge pull request #60 from EasyCrypt/deploy-no-eco Add a -no-eco option to disable .eco generation 30 March 2021, 14:59 UTC
3a626d5 Add a -no-eco option to disable .eco generation Existing .eco cached results are used, but new ones are not generated 30 March 2021, 13:09 UTC
bb6d218 Removing debugging output inserted by P-Y. 29 March 2021, 17:45 UTC
07519e7 fix CI_Int 29 March 2021, 15:44 UTC
c57f05e Proper goal for conseq equiv hoare => hoare. 25 March 2021, 17:04 UTC
98608e4 fix translation to why3 for operator, where some of its type parameters do not appear in the its type. 24 March 2021, 03:41 UTC
f5ea5b3 Fix supported alt-ergo version Not that this will be valid very long... 17 March 2021, 15:55 UTC
4818c2e Document why3/prover version interactions 17 March 2021, 14:04 UTC
d5bad15 Merge branch '1.0' into aprhl 16 March 2021, 16:39 UTC
ddb426b Removing dead code. 16 March 2021, 16:39 UTC
b3506e2 Merge branch '1.0' into aprhl 16 March 2021, 15:34 UTC
c19a2a7 remove debugging informations 03 March 2021, 14:07 UTC
d6e792c tactic/if: do not eagerly simplfy the pre fix #52 02 March 2021, 19:47 UTC
82b7089 refactoring proofs 25 February 2021, 11:46 UTC
d2e0537 more lemma on dbfun 25 February 2021, 10:29 UTC
b2bc4e8 add lemma dfun_ll 25 February 2021, 03:37 UTC
e0e995f stdlib: eager biased sampling 24 February 2021, 23:34 UTC
f4debca stdlib: more results on dfun 24 February 2021, 21:37 UTC
7a60dcc stdlib: gen. def. of distr. of functions 24 February 2021, 13:00 UTC
a7ca8c7 Lib: uniform distributions over finite functions 02 February 2021, 14:18 UTC
708e88c Losslessness axioms are now added to the "rnd" database 16 January 2021, 08:38 UTC
9dcb1a4 Renaming: XXX_full -> XXX_fu 16 January 2021, 07:53 UTC
7314a12 printing added lemma by operator declaration 16 January 2021, 05:43 UTC
f7e2b19 Basic results on dvector/dmatrix 15 January 2021, 14:03 UTC
b5f65bc Basic results on dvector/dmatrix 15 January 2021, 09:29 UTC
844e61b More results on dlet/dmap 15 January 2021, 08:11 UTC
bb0a97a Axiomatized operators are now forcibly unfoldable 13 January 2021, 15:15 UTC
88e05a0 t_subst not in the trusted base + some improvement to />. 12 January 2021, 14:55 UTC
5583bca pragma -oldip become the default 12 January 2021, 14:15 UTC
6feb5d7 fix quadratic behavior of ecCallbyValue 05 January 2021, 11:47 UTC
999561c remove deprecated "cut" tactic 04 January 2021, 13:24 UTC
f4f3f94 implement -R flag 04 January 2021, 10:26 UTC
3671d46 Travis -> CircleCI 18 December 2020, 20:07 UTC
35e59d1 `apply` is now using product-compatible matching 04 December 2020, 14:05 UTC
6504b04 remove debug infos 03 December 2020, 13:55 UTC
3c14f4d small refactoring 03 December 2020, 07:08 UTC
177f61d add trivial lemma 03 December 2020, 05:53 UTC
e7ca052 stack based conversion 02 December 2020, 15:08 UTC
93748b3 Decimal numbers are now translated to irreducible fractions 01 December 2020, 09:41 UTC
de9fdea In pose/trivial: use less conversion, cleanup chain of trivial calls. 01 December 2020, 08:48 UTC
68b3ffa make congr less costly 27 November 2020, 16:47 UTC
ea13c71 simplify t_split 27 November 2020, 16:46 UTC
2363562 fix cbv user_red 24 November 2020, 19:47 UTC
back to top