https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
dab7c47 Merge pull request #81 from Cameron-Low/csidh-group-action Csidh group action 11 October 2021, 09:55:19 UTC
55b0769 Dealt with admit, local Security lemma now holds. 10 September 2021, 12:58:45 UTC
0ca8da1 Fixed laziness issue with GO and LGO. Created an XY_Ideal, one admit left. 30 July 2021, 15:38:23 UTC
f16cb24 Narrow the gap at the top 30 July 2021, 13:03:11 UTC
719a12d More merge conflict resolution, PRF counting added. 30 July 2021, 11:34:54 UTC
5144b43 Fix the rest and the second step of wPRP -> sampling fresh input output pairs 30 July 2021, 09:37:23 UTC
d682778 Sneakily make q a local parameter instead of a global one. Only one of the two proofs is done. 30 July 2021, 09:32:08 UTC
75d7abb Resolving conflicts. Added full reduction, and setup security proof lemma. 29 July 2021, 15:37:12 UTC
9eb26cf Close the gaps at the foundation 29 July 2021, 15:05:58 UTC
9c8257c One step closer to final statement 28 July 2021, 16:21:42 UTC
2f06546 Reworking the WeakPseurandom EGA assumption. Layering reductions (partially admitted). To bring the foundation layer back to where it was. Removing Bounding until where it is needed. 27 July 2021, 17:20:48 UTC
70b7320 ROs from WP 26 July 2021, 12:55:19 UTC
659868a Sectionize 26 July 2021, 11:10:45 UTC
6313c6a Killed off last hybrid proof. 23 July 2021, 15:18:49 UTC
c706607 Generalised l and re-proved a bunch of the hybrid lemmas. 21 July 2021, 16:06:43 UTC
0b7a0a8 Fiddle with naming 19 July 2021, 14:27:54 UTC
ecc5df7 Reading with a pen 19 July 2021, 14:02:18 UTC
45a2b9d Finished proof of PRF side of the hybrid. 19 July 2021, 13:40:03 UTC
41971ad Splitting random maps to product types 16 July 2021, 23:22:10 UTC
cdbe2c7 Completed one half of hybrid proof. 16 July 2021, 18:25:41 UTC
fff66f4 Progress on ideal hybrid reduction. Plus some refactoring. 15 July 2021, 08:53:05 UTC
3ce8ec1 Weakening the invariant so it holds 14 July 2021, 08:49:24 UTC
93afc79 Progress on the second hybrid 13 July 2021, 15:46:50 UTC
652ccf1 Completed a few more proofs. 13 July 2021, 13:53:43 UTC
ec881d3 Progress on the hybrid 13 July 2021, 10:41:35 UTC
1b24f47 A selection of changes, some useful. 13 July 2021, 09:46:12 UTC
44bc365 Finished proof for first half of the middle reduction. 09 July 2021, 11:54:41 UTC
287f74a Another restructure heavily inspired by a certain XSalsa formalisation. Also almost finished one half of the middle proof. 08 July 2021, 15:54:20 UTC
1f83b64 Adding an explicit contract for fun 06 July 2021, 08:25:30 UTC
fd4d115 Clean up one proof 05 July 2021, 14:41:59 UTC
31e5efb Added reduction from hybrid wpr to the hardness assumption of weak pseudorandomness. 05 July 2021, 14:11:13 UTC
d3ef778 Full restructuring of the formalisation. Converted from unbounded games to bounded games and re-proved the previous lemmas. 01 July 2021, 14:47:48 UTC
099c7a7 Progress with Cameron 29 June 2021, 11:20:34 UTC
fd7cf05 Completed other Ind game proof. 29 June 2021, 09:56:57 UTC
70aa5fe Made use of the regular EGA to remove most of the admits, just one to go. Also transformed the Adversary of lemma 4.20 to coincide with the changes done previously. 25 June 2021, 15:37:17 UTC
4079f89 Added a regular EGA that is abelian with some useful lemmas on the uniqueness of extract, did slight restructuring, and made a change to 'sample' so it is now a uniform distribution. 25 June 2021, 15:35:24 UTC
3df9225 Expanded on proof of equivalence between set distribution and action distribution. Also some cosmetic changes to proof layout. 25 June 2021, 09:39:45 UTC
eb83d84 Transitivity of equivalence Much power. Such wonderful. Wow. 24 June 2021, 21:22:58 UTC
6a9caaf Added most of a proof 24 June 2021, 13:45:54 UTC
950a4ea Fixing my reduction 24 June 2021, 08:46:07 UTC
4c6ed8a Some progress with Cameron 23 June 2021, 15:49:28 UTC
985afa5 Setup basic abstractions, initial games. 23 June 2021, 12:29:45 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
back to top