We are hiring ! See our job offers.
https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
374dae6 parser: fix precedence issue 12 October 2021, 13:09:21 UTC
a39d5d1 wlog suff 12 October 2021, 12:15:35 UTC
5ec0904 gen 12 October 2021, 09:59:59 UTC
a3cd19c implement gen have 12 October 2021, 09:49:54 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
7fbcff7 StdLib: few lemmas about polynomials 08 April 2021, 16:42:07 UTC
84c2618 Fix stdlib 08 April 2021, 13:48:16 UTC
a014668 StdLib: enumerating polynomials of a given degree 08 April 2021, 13:14:10 UTC
0a6485a StdLib: Finite: explicit witnesses for finitness + related lemmas on lists 08 April 2021, 13:13:54 UTC
81cd929 Stdlib: IntDiv - add a few lemmas 08 April 2021, 13:13:27 UTC
18e7bf4 Stdlib: more results on polynomials & ring ideals 08 April 2021, 07:15:49 UTC
83e39fd Prove that polynomials form an integral domain 07 April 2021, 14:44:27 UTC
6ce66c7 Include ring quotients th. in ideals th. 07 April 2021, 14:44:12 UTC
de2158b Poly.ec -> Poly.eca 07 April 2021, 12:32:34 UTC
a62a90d Stdlib: ring quotients 05 April 2021, 09:08:22 UTC
cf1eca8 Stdlib: fmin 05 April 2021, 06:43:18 UTC
1aab7a8 Quotient: use std def. of eqv relation 05 April 2021, 06:42:55 UTC
2a8554f Stdlib: simplify proofs in Quotient.ec 05 April 2021, 06:37:07 UTC
c404a43 Stdlib: ideas & a bit of abstract arithmetic 05 April 2021, 05:51:11 UTC
940fa12 List: fix admitted proofs 05 April 2021, 05:40:35 UTC
c5d0c62 List: size_eq1 05 April 2021, 05:39:57 UTC
432c181 README: fix why3 config command 04 April 2021, 17:54:08 UTC
748c9ef remove doc-box 04 April 2021, 09:00:54 UTC
a0a0c9b Upgrade versions of supported provers 04 April 2021, 07:17:16 UTC
20a6183 Move to Why3 1.4 04 April 2021, 06:42:50 UTC
fb59000 CI: use workflow conclusion 03 April 2021, 19:32:58 UTC
7627a75 Move to GitHub Actions 03 April 2021, 17:32:12 UTC
8bcb1ae easycrypt.png 03 April 2021, 15:30:26 UTC
df9ab35 Stdlib: refactoring 02 April 2021, 20:27:10 UTC
91479fa Stdlib: integer log. 02 April 2021, 20:24:48 UTC
e8e6dc4 List: alltuples & allsubtuples 02 April 2021, 12:25:47 UTC
9c741f1 List: subseqs 02 April 2021, 11:52:49 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:20 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:52 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:44 UTC
c57f05e Proper goal for conseq equiv hoare => hoare. 25 March 2021, 17:04:40 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:53 UTC
f5ea5b3 Fix supported alt-ergo version Not that this will be valid very long... 17 March 2021, 15:55:39 UTC
4818c2e Document why3/prover version interactions 17 March 2021, 14:04:26 UTC
ddb426b Removing dead code. 16 March 2021, 16:39:12 UTC
c19a2a7 remove debugging informations 03 March 2021, 14:07:57 UTC
d6e792c tactic/if: do not eagerly simplfy the pre fix #52 02 March 2021, 19:47:13 UTC
82b7089 refactoring proofs 25 February 2021, 11:46:34 UTC
d2e0537 more lemma on dbfun 25 February 2021, 10:29:19 UTC
b2bc4e8 add lemma dfun_ll 25 February 2021, 03:37:03 UTC
e0e995f stdlib: eager biased sampling 24 February 2021, 23:34:31 UTC
f4debca stdlib: more results on dfun 24 February 2021, 21:37:09 UTC
7a60dcc stdlib: gen. def. of distr. of functions 24 February 2021, 13:00:54 UTC
a7ca8c7 Lib: uniform distributions over finite functions 02 February 2021, 14:18:43 UTC
708e88c Losslessness axioms are now added to the "rnd" database 16 January 2021, 08:38:18 UTC
9dcb1a4 Renaming: XXX_full -> XXX_fu 16 January 2021, 07:53:35 UTC
7314a12 printing added lemma by operator declaration 16 January 2021, 05:43:39 UTC
f7e2b19 Basic results on dvector/dmatrix 15 January 2021, 14:03:21 UTC
b5f65bc Basic results on dvector/dmatrix 15 January 2021, 09:29:53 UTC
844e61b More results on dlet/dmap 15 January 2021, 08:11:01 UTC
bb0a97a Axiomatized operators are now forcibly unfoldable 13 January 2021, 15:15:47 UTC
88e05a0 t_subst not in the trusted base + some improvement to />. 12 January 2021, 14:55:42 UTC
5583bca pragma -oldip become the default 12 January 2021, 14:15:46 UTC
6feb5d7 fix quadratic behavior of ecCallbyValue 05 January 2021, 11:47:23 UTC
999561c remove deprecated "cut" tactic 04 January 2021, 13:24:41 UTC
f4f3f94 implement -R flag 04 January 2021, 10:26:56 UTC
3671d46 Travis -> CircleCI 18 December 2020, 20:07:48 UTC
35e59d1 `apply` is now using product-compatible matching 04 December 2020, 14:05:15 UTC
6504b04 remove debug infos 03 December 2020, 13:55:10 UTC
3c14f4d small refactoring 03 December 2020, 07:08:30 UTC
back to top