https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
14216cb fix default.nix 18 April 2021, 14:12:06 UTC
2afb775 StdLib: funi + same weight => eq 14 April 2021, 15:27:25 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
177f61d add trivial lemma 03 December 2020, 05:53:30 UTC
e7ca052 stack based conversion 02 December 2020, 15:08:03 UTC
93748b3 Decimal numbers are now translated to irreducible fractions 01 December 2020, 09:41:56 UTC
de9fdea In pose/trivial: use less conversion, cleanup chain of trivial calls. 01 December 2020, 08:48:33 UTC
68b3ffa make congr less costly 27 November 2020, 16:47:34 UTC
ea13c71 simplify t_split 27 November 2020, 16:46:54 UTC
2363562 fix cbv user_red 24 November 2020, 19:47:13 UTC
6857723 simplify user reduction 24 November 2020, 13:49:28 UTC
fcdfcbd Core theory for univariate polynomials 21 November 2020, 12:11:49 UTC
a08bc34 Stdlib: more results on Rn + bigops on Rn 21 November 2020, 08:29:35 UTC
7a42484 MANIFEST 21 November 2020, 00:14:50 UTC
07b937c Small addititions on distributions 20 November 2020, 22:16:40 UTC
6f68e27 More results on distributions (conditional exp, Jensen (finite)) 20 November 2020, 14:45:54 UTC
27ff637 integrating more results on distributions 18 November 2020, 06:00:50 UTC
8d01a80 fix CBC 17 November 2020, 17:48:08 UTC
ed25190 small generalization of PRP 16 November 2020, 10:58:31 UTC
8cb3e88 extend conseq rules: equivF => hoareF => hoareF and equivF => phoareF => phoareF 13 November 2020, 11:33:47 UTC
4391b04 basic results about minr 12 November 2020, 11:00:16 UTC
61de4b9 Fix "smt debug" 12 November 2020, 08:24:20 UTC
b360fa8 Fix bug in conseq 11 November 2020, 05:56:42 UTC
ffad375 New option for SMT: "debug" 03 November 2020, 09:04:00 UTC
4ef4286 Fix dfold s.t. the functor takes the index 21 October 2020, 08:49:24 UTC
19c7285 New operator: dfold 20 October 2020, 09:40:14 UTC
fa3853d README (nix) 15 October 2020, 10:30:04 UTC
bc4f6df "={_}" now supports the construction "glob M \ { p1, p2, ... }" It stands for "glob M" without "p1, p2, ..." 15 October 2020, 08:39:16 UTC
22a8b51 better printing of modules bodies w.r.t. "import var" 14 October 2020, 09:10:10 UTC
ca1f0d2 The command "import var" is now allowed at top-level 14 October 2020, 07:08:46 UTC
b34c174 add alias "include var" that stands for "include" then "import var" 14 October 2020, 06:55:56 UTC
back to top