https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
5f1ed5a README 21 April 2021, 08:28:34 UTC
bffac06 Merge branch '1.0-preview' into deploy-cost-1.0-preview 14 April 2021, 16:29:23 UTC
8b8fe79 Merge branch '1.0' into 1.0-preview 14 April 2021, 15:58:55 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
7a4c6d1 Stdlib: ring quotients 06 April 2021, 05:28:48 UTC
e8e4349 Stdlib: fmin 06 April 2021, 05:28:48 UTC
22c656e Quotient: use std def. of eqv relation 06 April 2021, 05:28:48 UTC
4f4e165 Stdlib: simplify proofs in Quotient.ec 06 April 2021, 05:28:48 UTC
101a76d Stdlib: ideas & a bit of abstract arithmetic 06 April 2021, 05:28:48 UTC
94ac9ac List: fix admitted proofs 06 April 2021, 05:28:48 UTC
8d240f6 List: size_eq1 06 April 2021, 05:28:48 UTC
6084e7e README: fix why3 config command 06 April 2021, 05:28:48 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
9ff108a Merge branch '1.0' into 1.0-preview 04 April 2021, 17:44:35 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
66b5409 Merge branch '1.0' into 1.0-preview 03 April 2021, 17:43: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
bab83fc simplify syntaxe of call rule 30 March 2021, 10:25:55 UTC
f649eab add simplification lemmas on xint 30 March 2021, 09:22:14 UTC
2e7cdcd Proper goal for conseq equiv hoare => hoare. 26 March 2021, 12:57:04 UTC
c57f05e Proper goal for conseq equiv hoare => hoare. 25 March 2021, 17:04:40 UTC
3990ed8 fix previous merge 24 March 2021, 06:10:58 UTC
18fa1b6 Merge branch '1.0-preview' into deploy-cost-1.0-preview 24 March 2021, 06:08:13 UTC
81b28cf Merge branch '1.0' into 1.0-preview 24 March 2021, 05:56:58 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
f672a21 Merge branch '1.0' into 1.0-preview 16 March 2021, 16:42:57 UTC
ddb426b Removing dead code. 16 March 2021, 16:39:12 UTC
432d808 fix hashed_elgamal_generic.ec 10 March 2021, 11:00:25 UTC
e79afc7 fix br93 10 March 2021, 10:48:11 UTC
1ea7f90 fixed proc and cramer-shoup 09 March 2021, 14:48:29 UTC
bf1d54e Merge branch '1.0' into 1.0-preview 03 March 2021, 14:08:12 UTC
c19a2a7 remove debugging informations 03 March 2021, 14:07:57 UTC
c4afc9a Merge branch '1.0' into 1.0-preview 02 March 2021, 19:49:17 UTC
d6e792c tactic/if: do not eagerly simplfy the pre fix #52 02 March 2021, 19:47:13 UTC
a4cff37 fixed async-while 02 March 2021, 16:25:32 UTC
5611cfd fixed small cost tutorial 02 March 2021, 15:52:37 UTC
151cbd7 done with stdlib 02 March 2021, 14:58:00 UTC
6a0033a fixed some syntax errors in examples 02 March 2021, 13:08:30 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
a45326f Merge branch '1.0' into 1.0-preview 19 February 2021, 17:31:04 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
107ae0b Merge remote-tracking branch 'origin/1.0-preview' into deploy-cost-1.0-preview 15 January 2021, 17:26:40 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
6231501 In CBN, add a dedicated stack element for "match" [closes #49] 15 January 2021, 07:20:29 UTC
3a94832 Add `Fmatch` in cbn head-reduction. [fix #48] 14 January 2021, 20:24:52 UTC
b329d8f 13 January 2021, 15:19:44 UTC
b6414a4 Merge branch '1.0' into 1.0-preview 13 January 2021, 15:16:02 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
ba4243a Merge branch 'deploy-debug-mark' into 1.0-preview 11 January 2021, 14:05:21 UTC
back to top