https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
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
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
back to top