https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
d6f54af WIP 16 September 2021, 15:44 UTC
56a6902 experiments with log 16 September 2021, 08:52 UTC
0d926ff cleanup and DMapSampling 14 September 2021, 12:14 UTC
8ee9d8f foo_monotone no longer an axiom 13 September 2021, 09:26 UTC
7fb11dc equivalence of sdist expressed using max and sum 10 September 2021, 18:19 UTC
18af1e1 some ideas on statistical distance 09 September 2021, 16:53 UTC
59f4175 prove statistical distance bound 08 September 2021, 14:35 UTC
486afcc first part of SDist 06 September 2021, 16:06 UTC
0974fd6 comments and minor cleanup 06 September 2021, 14:56 UTC
31197a3 simplify guess_bound 02 September 2021, 13:24 UTC
371f02b inline badG'_cdh 01 September 2021, 12:27 UTC
f2a1c73 smt call simplified enough? 01 September 2021, 10:22 UTC
0aead1c more optimal G1G2_NCDH 01 September 2021, 07:15 UTC
d5e9198 reordering + final statement 31 August 2021, 15:49 UTC
2374063 replace clamp with bounds 31 August 2021, 13:53 UTC
f53b2d8 slight cleanup of guess_bound 31 August 2021, 13:02 UTC
3d0d1c8 move generic lemmas 30 August 2021, 15:52 UTC
adfd419 proof of guess_bound 30 August 2021, 13:59 UTC
ca33e5b fist cleanup pass 30 August 2021, 13:48 UTC
459831d dlist_djoin and more general mapiK 30 August 2021, 11:36 UTC
007d6c6 fix proof of S_guess 30 August 2021, 07:54 UTC
33a7c3f A_bound 27 August 2021, 15:49 UTC
41d4148 check ddh indices 27 August 2021, 15:41 UTC
927b168 i_k and j_k do not have to be within range 27 August 2021, 14:02 UTC
96cd633 some work on guess_bound 27 August 2021, 11:59 UTC
765557d dlist lemmas 25 August 2021, 12:33 UTC
1fb3dec dlist_set2E statement 24 August 2021, 12:58 UTC
ffe94d0 fix G1G2_Gbad 24 August 2021, 11:24 UTC
b39d50c stop logging after bad, fix simulation lemma 24 August 2021, 09:40 UTC
b16e9cc reduction to NCDH 23 August 2021, 09:44 UTC
150a0d0 simplify statement of guess_S 20 August 2021, 16:54 UTC
759cdcf prove first part of new proof outline 20 August 2021, 11:02 UTC
b9a1fe3 cleanup/comments 16 August 2021, 14:03 UTC
c597097 reduction from "bad /\ !stop" to existence of good triple 21 July 2021, 15:11 UTC
3a954f3 foo :) 21 July 2021, 13:16 UTC
de71993 cleanup / new lemma statements 20 July 2021, 16:46 UTC
521b70c proof of S_ia and S_ib 19 July 2021, 16:29 UTC
f32e8a9 finish prood of G'_S_stop 19 July 2021, 10:26 UTC
f0d351b G'_S_stop (up to some commits) and required fixes 15 July 2021, 17:02 UTC
25b34eb WIP 15 July 2021, 11:57 UTC
ece42a4 some more lemma statements 13 July 2021, 16:48 UTC
9c16515 tentative def of simulator and adversary 13 July 2021, 09:33 UTC
b36fcb9 nominal groups and first part of CDH_RSR proof 12 July 2021, 17:37 UTC
512f0f2 [docker] get CVC4 from a more stable URL 30 June 2021, 14:43 UTC
489ff17 default.nix 30 June 2021, 10:01 UTC
410f882 improve default.nix 28 June 2021, 10:11 UTC
692a017 remove duplicate eq_in_count/eq_count_in, keep eq_in_count 09 June 2021, 06:26 UTC
1890ad1 Update README.md 08 June 2021, 19:43 UTC
73afe4f improve error msg for proc 04 June 2021, 05: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
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
back to top