dab7c47 | Cameron Low | 11 October 2021, 09:55:19 UTC | Merge pull request #81 from Cameron-Low/csidh-group-action Csidh group action | 11 October 2021, 09:55:19 UTC |
55b0769 | Cameron Low | 10 September 2021, 12:58:45 UTC | Dealt with admit, local Security lemma now holds. | 10 September 2021, 12:58:45 UTC |
0ca8da1 | Cameron Low | 30 July 2021, 15:38:23 UTC | Fixed laziness issue with GO and LGO. Created an XY_Ideal, one admit left. | 30 July 2021, 15:38:23 UTC |
f16cb24 | François Dupressoir | 30 July 2021, 13:03:11 UTC | Narrow the gap at the top | 30 July 2021, 13:03:11 UTC |
719a12d | Cameron Low | 30 July 2021, 11:34:54 UTC | More merge conflict resolution, PRF counting added. | 30 July 2021, 11:34:54 UTC |
5144b43 | François Dupressoir | 30 July 2021, 09:37:23 UTC | Fix the rest and the second step of wPRP -> sampling fresh input output pairs | 30 July 2021, 09:37:23 UTC |
d682778 | François Dupressoir | 30 July 2021, 09:32:08 UTC | 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 | Cameron Low | 29 July 2021, 15:37:12 UTC | Resolving conflicts. Added full reduction, and setup security proof lemma. | 29 July 2021, 15:37:12 UTC |
9eb26cf | François Dupressoir | 29 July 2021, 15:05:58 UTC | Close the gaps at the foundation | 29 July 2021, 15:05:58 UTC |
9c8257c | François Dupressoir | 28 July 2021, 16:21:42 UTC | One step closer to final statement | 28 July 2021, 16:21:42 UTC |
2f06546 | François Dupressoir | 27 July 2021, 17:20:48 UTC | 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 | François Dupressoir | 26 July 2021, 12:55:19 UTC | ROs from WP | 26 July 2021, 12:55:19 UTC |
659868a | François Dupressoir | 26 July 2021, 11:10:45 UTC | Sectionize | 26 July 2021, 11:10:45 UTC |
6313c6a | Cameron Low | 23 July 2021, 15:18:49 UTC | Killed off last hybrid proof. | 23 July 2021, 15:18:49 UTC |
c706607 | Cameron Low | 21 July 2021, 16:06:43 UTC | Generalised l and re-proved a bunch of the hybrid lemmas. | 21 July 2021, 16:06:43 UTC |
0b7a0a8 | François Dupressoir | 19 July 2021, 14:27:54 UTC | Fiddle with naming | 19 July 2021, 14:27:54 UTC |
ecc5df7 | François Dupressoir | 19 July 2021, 14:02:18 UTC | Reading with a pen | 19 July 2021, 14:02:18 UTC |
45a2b9d | Cameron Low | 19 July 2021, 13:40:03 UTC | Finished proof of PRF side of the hybrid. | 19 July 2021, 13:40:03 UTC |
41971ad | François Dupressoir | 16 July 2021, 23:22:10 UTC | Splitting random maps to product types | 16 July 2021, 23:22:10 UTC |
cdbe2c7 | Cameron Low | 16 July 2021, 18:25:41 UTC | Completed one half of hybrid proof. | 16 July 2021, 18:25:41 UTC |
fff66f4 | Cameron Low | 15 July 2021, 08:53:05 UTC | Progress on ideal hybrid reduction. Plus some refactoring. | 15 July 2021, 08:53:05 UTC |
3ce8ec1 | François Dupressoir | 14 July 2021, 08:49:24 UTC | Weakening the invariant so it holds | 14 July 2021, 08:49:24 UTC |
93afc79 | François Dupressoir | 13 July 2021, 15:46:50 UTC | Progress on the second hybrid | 13 July 2021, 15:46:50 UTC |
652ccf1 | Cameron Low | 13 July 2021, 13:53:43 UTC | Completed a few more proofs. | 13 July 2021, 13:53:43 UTC |
ec881d3 | François Dupressoir | 13 July 2021, 10:41:35 UTC | Progress on the hybrid | 13 July 2021, 10:41:35 UTC |
1b24f47 | Cameron Low | 13 July 2021, 09:46:12 UTC | A selection of changes, some useful. | 13 July 2021, 09:46:12 UTC |
44bc365 | Cameron Low | 09 July 2021, 11:54:41 UTC | Finished proof for first half of the middle reduction. | 09 July 2021, 11:54:41 UTC |
287f74a | Cameron Low | 08 July 2021, 15:54:20 UTC | 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 | François Dupressoir | 06 July 2021, 08:25:30 UTC | Adding an explicit contract for fun | 06 July 2021, 08:25:30 UTC |
fd4d115 | François Dupressoir | 05 July 2021, 14:41:59 UTC | Clean up one proof | 05 July 2021, 14:41:59 UTC |
31e5efb | Cameron Low | 05 July 2021, 14:11:13 UTC | Added reduction from hybrid wpr to the hardness assumption of weak pseudorandomness. | 05 July 2021, 14:11:13 UTC |
d3ef778 | Cameron Low | 01 July 2021, 14:47:48 UTC | 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 | François Dupressoir | 29 June 2021, 11:20:34 UTC | Progress with Cameron | 29 June 2021, 11:20:34 UTC |
fd7cf05 | Cameron Low | 29 June 2021, 09:56:57 UTC | Completed other Ind game proof. | 29 June 2021, 09:56:57 UTC |
70aa5fe | Cameron Low | 25 June 2021, 15:37:17 UTC | 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 | Cameron Low | 25 June 2021, 15:35:24 UTC | 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 | Cameron Low | 25 June 2021, 09:39:45 UTC | 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 | François Dupressoir | 24 June 2021, 21:22:58 UTC | Transitivity of equivalence Much power. Such wonderful. Wow. | 24 June 2021, 21:22:58 UTC |
6a9caaf | Cameron Low | 24 June 2021, 13:45:54 UTC | Added most of a proof | 24 June 2021, 13:45:54 UTC |
950a4ea | François Dupressoir | 24 June 2021, 08:46:07 UTC | Fixing my reduction | 24 June 2021, 08:46:07 UTC |
4c6ed8a | François Dupressoir | 23 June 2021, 15:49:28 UTC | Some progress with Cameron | 23 June 2021, 15:49:28 UTC |
985afa5 | Cameron Low | 23 June 2021, 12:29:45 UTC | Setup basic abstractions, initial games. | 23 June 2021, 12:29:45 UTC |
73afe4f | Benjamin Gregoire | 04 June 2021, 05:35:25 UTC | improve error msg for proc | 04 June 2021, 05:35:25 UTC |
aeac2d4 | Pierre-Yves Strub | 27 May 2021, 10:03:02 UTC | Fix: cleanup exact hint DB after clone | 27 May 2021, 10:03:14 UTC |
eb6ce7c | François Dupressoir | 26 May 2021, 15:07:59 UTC | [stdlib] Array: fix set_set_swap | 26 May 2021, 15:07:59 UTC |
4dbdb88 | Pierre-Yves Strub | 26 May 2021, 07:20:22 UTC | Extend cloning with - inline but keep override (<=) - override theories | 26 May 2021, 07:20:22 UTC |
16e5d3b | Pierre-Yves Strub | 25 May 2021, 12:40:30 UTC | remove 'search' commands | 25 May 2021, 12:40:30 UTC |
aae9601 | Francois Dupressoir | 20 May 2021, 16:48:40 UTC | 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 | François Dupressoir | 20 May 2021, 14:32:30 UTC | Some nits in the new SmtMap lemmas | 20 May 2021, 16:31:22 UTC |
c750a58 | François Dupressoir | 20 May 2021, 09:59:20 UTC | FinType.FinType → FinType | 20 May 2021, 09:59:20 UTC |
82fd774 | François Dupressoir | 20 May 2021, 09:26:40 UTC | 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 | François Dupressoir | 18 May 2021, 22:22:35 UTC | 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 | François Dupressoir | 18 May 2021, 13:15:43 UTC | Library work towards soft-merge of ChaCha-Poly | 18 May 2021, 22:17:02 UTC |
ba45bb5 | Francois Dupressoir | 26 April 2021, 12:10:43 UTC | 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 | Benjamin Gregoire | 18 April 2021, 14:12:06 UTC | fix default.nix | 18 April 2021, 14:12:06 UTC |
1313a7d | François Dupressoir | 14 April 2021, 18:20:13 UTC | Merge remote-tracking branch 'origin/1.0' into deploy-clean-oldmonoid | 14 April 2021, 18:20:13 UTC |
49d7ad3 | François Dupressoir | 14 April 2021, 15:32:51 UTC | 'Cleanup' but it's mostly shifting things around | 14 April 2021, 15:32:51 UTC |
2afb775 | Pierre-Yves Strub | 14 April 2021, 15:27:25 UTC | StdLib: funi + same weight => eq | 14 April 2021, 15:27:25 UTC |
d809ef8 | François Dupressoir | 13 April 2021, 15:50:46 UTC | 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 | Pierre-Yves Strub | 13 April 2021, 13:34:33 UTC | StdLib: basic facts on distributions | 13 April 2021, 13:34:33 UTC |
1b25ed4 | Pierre-Yves Strub | 12 April 2021, 09:31:13 UTC | Fix bug in theory renamings | 12 April 2021, 09:31:13 UTC |
40d1950 | Pierre-Yves Strub | 12 April 2021, 06:10:36 UTC | StdLib: ZModP: finite + uniform distribution | 12 April 2021, 06:10:36 UTC |
7ad9727 | Pierre-Yves Strub | 11 April 2021, 13:06:28 UTC | StdLib: linking sampling in Z/pZ and Z/qZ when q|p | 11 April 2021, 13:06:28 UTC |
c6ad4b1 | Pierre-Yves Strub | 10 April 2021, 14:05:38 UTC | StdLib: Poly: killing last admits | 10 April 2021, 14:05:38 UTC |
81f358d | Pierre-Yves Strub | 10 April 2021, 10:47:47 UTC | StdLib: polynomials distributions | 10 April 2021, 10:47:47 UTC |
639a76e | Pierre-Yves Strub | 09 April 2021, 20:10:53 UTC | StdLib: lead coeff. and degree of X^n+1 | 09 April 2021, 20:10:53 UTC |
8e6dd9a | Pierre-Yves Strub | 09 April 2021, 18:16:22 UTC | StdLib: ring quotient for non-integral domains | 09 April 2021, 18:16:22 UTC |
6a4bbab | Pierre-Yves Strub | 09 April 2021, 16:55:55 UTC | StdLib: ring regular element + poly over non integral domains | 09 April 2021, 16:55:55 UTC |
9e43d2c | Pierre-Yves Strub | 09 April 2021, 15:30:53 UTC | StdLib: more results on pmin | 09 April 2021, 15:30:53 UTC |
7fbcff7 | Pierre-Yves Strub | 08 April 2021, 16:42:07 UTC | StdLib: few lemmas about polynomials | 08 April 2021, 16:42:07 UTC |
84c2618 | Pierre-Yves Strub | 08 April 2021, 13:48:16 UTC | Fix stdlib | 08 April 2021, 13:48:16 UTC |
a014668 | Pierre-Yves Strub | 08 April 2021, 13:14:10 UTC | StdLib: enumerating polynomials of a given degree | 08 April 2021, 13:14:10 UTC |
0a6485a | Pierre-Yves Strub | 08 April 2021, 13:13:54 UTC | StdLib: Finite: explicit witnesses for finitness + related lemmas on lists | 08 April 2021, 13:13:54 UTC |
81cd929 | Pierre-Yves Strub | 08 April 2021, 13:13:27 UTC | Stdlib: IntDiv - add a few lemmas | 08 April 2021, 13:13:27 UTC |
18e7bf4 | Pierre-Yves Strub | 08 April 2021, 07:15:49 UTC | Stdlib: more results on polynomials & ring ideals | 08 April 2021, 07:15:49 UTC |
83e39fd | Pierre-Yves Strub | 07 April 2021, 14:44:27 UTC | Prove that polynomials form an integral domain | 07 April 2021, 14:44:27 UTC |
6ce66c7 | Pierre-Yves Strub | 07 April 2021, 14:44:12 UTC | Include ring quotients th. in ideals th. | 07 April 2021, 14:44:12 UTC |
de2158b | Pierre-Yves Strub | 07 April 2021, 12:32:34 UTC | Poly.ec -> Poly.eca | 07 April 2021, 12:32:34 UTC |
a62a90d | Pierre-Yves Strub | 05 April 2021, 09:08:22 UTC | Stdlib: ring quotients | 05 April 2021, 09:08:22 UTC |
cf1eca8 | Pierre-Yves Strub | 05 April 2021, 06:43:18 UTC | Stdlib: fmin | 05 April 2021, 06:43:18 UTC |
1aab7a8 | Pierre-Yves Strub | 05 April 2021, 06:42:55 UTC | Quotient: use std def. of eqv relation | 05 April 2021, 06:42:55 UTC |
2a8554f | Pierre-Yves Strub | 05 April 2021, 06:37:07 UTC | Stdlib: simplify proofs in Quotient.ec | 05 April 2021, 06:37:07 UTC |
c404a43 | Pierre-Yves Strub | 05 April 2021, 05:51:11 UTC | Stdlib: ideas & a bit of abstract arithmetic | 05 April 2021, 05:51:11 UTC |
940fa12 | Pierre-Yves Strub | 05 April 2021, 05:40:35 UTC | List: fix admitted proofs | 05 April 2021, 05:40:35 UTC |
c5d0c62 | Pierre-Yves Strub | 05 April 2021, 05:39:57 UTC | List: size_eq1 | 05 April 2021, 05:39:57 UTC |
432c181 | Pierre-Yves Strub | 04 April 2021, 17:54:08 UTC | README: fix why3 config command | 04 April 2021, 17:54:08 UTC |
748c9ef | Pierre-Yves Strub | 04 April 2021, 09:00:54 UTC | remove doc-box | 04 April 2021, 09:00:54 UTC |
a0a0c9b | Pierre-Yves Strub | 04 April 2021, 07:17:16 UTC | Upgrade versions of supported provers | 04 April 2021, 07:17:16 UTC |
20a6183 | Pierre-Yves Strub | 04 April 2021, 06:42:50 UTC | Move to Why3 1.4 | 04 April 2021, 06:42:50 UTC |
fb59000 | Pierre-Yves Strub | 03 April 2021, 19:32:58 UTC | CI: use workflow conclusion | 03 April 2021, 19:32:58 UTC |
7627a75 | Pierre-Yves Strub | 03 April 2021, 17:32:12 UTC | Move to GitHub Actions | 03 April 2021, 17:32:12 UTC |
8bcb1ae | Pierre-Yves Strub | 03 April 2021, 15:30:26 UTC | easycrypt.png | 03 April 2021, 15:30:26 UTC |
df9ab35 | Pierre-Yves Strub | 02 April 2021, 20:27:10 UTC | Stdlib: refactoring | 02 April 2021, 20:27:10 UTC |
91479fa | Pierre-Yves Strub | 02 April 2021, 20:24:48 UTC | Stdlib: integer log. | 02 April 2021, 20:24:48 UTC |
e8e6dc4 | Pierre-Yves Strub | 02 April 2021, 12:25:47 UTC | List: alltuples & allsubtuples | 02 April 2021, 12:25:47 UTC |
9c741f1 | Pierre-Yves Strub | 02 April 2021, 11:52:49 UTC | List: subseqs | 02 April 2021, 11:52:49 UTC |
30b7cae | Pierre-Yves Strub | 02 April 2021, 07:28:20 UTC | 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 | Francois Dupressoir | 30 March 2021, 14:59:52 UTC | 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 | François Dupressoir | 30 March 2021, 13:09:44 UTC | 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 | François Dupressoir | 25 March 2021, 16:47:12 UTC | Proper goal for conseq equiv hoare => hoare. | 25 March 2021, 17:04:40 UTC |