| ce26305 | Christian Doczkal | 06 July 2021, 15:27:24 UTC | nominal groups | 06 July 2021, 15:27:24 UTC |
| 902ff25 | Pierre Boutry | 06 July 2021, 05:31:34 UTC | cleanup | 06 July 2021, 05:31:34 UTC |
| 495f2a1 | Pierre Boutry | 03 July 2021, 17:01:43 UTC | version of the ideal CCA with sampling | 03 July 2021, 17:01:43 UTC |
| 0a7e540 | Pierre Boutry | 29 June 2021, 13:17:52 UTC | try to weaken ICCA assumptions | 29 June 2021, 13:17:52 UTC |
| 4d7aa10 | Pierre Boutry | 23 June 2021, 15:33:34 UTC | rename ICCA into ICCA_Oracle | 23 June 2021, 15:33:34 UTC |
| 8c2e45c | Pierre Boutry | 23 June 2021, 15:30:57 UTC | useless pk bis | 23 June 2021, 15:30:57 UTC |
| b615455 | Pierre Boutry | 23 June 2021, 15:30:04 UTC | useless pk | 23 June 2021, 15:30:04 UTC |
| d5425ab | Pierre Boutry | 23 June 2021, 14:24:54 UTC | fix clone import of CCA | 23 June 2021, 14:24:54 UTC |
| ccd9f4e | Benjamin Gregoire | 21 June 2021, 09:50:10 UTC | use local clone to remove restriction | 21 June 2021, 09:50:33 UTC |
| 2e6f1fc | Pierre Boutry | 21 June 2021, 07:01:42 UTC | close section and theory | 21 June 2021, 07:01:42 UTC |
| fd6d126 | Pierre Boutry | 17 June 2021, 19:18:35 UTC | weaken AB_bound | 17 June 2021, 19:18:35 UTC |
| 74131f2 | Pierre Boutry | 17 June 2021, 19:01:01 UTC | done? | 17 June 2021, 19:01:01 UTC |
| 6cf0d6f | Pierre Boutry | 17 June 2021, 17:11:44 UTC | only AB_bound left | 17 June 2021, 17:11:44 UTC |
| 590699c | Christian Doczkal | 17 June 2021, 16:52:47 UTC | prove Real'_CCA_L (fix B) | 17 June 2021, 16:52:47 UTC |
| 18e7eac | Christian Doczkal | 17 June 2021, 16:05:31 UTC | fix definitions, Real_Real | 17 June 2021, 16:08:47 UTC |
| c729530 | Pierre Boutry | 17 June 2021, 15:29:10 UTC | forgot to inline one equiv | 17 June 2021, 15:29:10 UTC |
| 9fe28cf | Pierre Boutry | 17 June 2021, 15:12:07 UTC | fix ICCA_CCALR statement and prove it | 17 June 2021, 15:12:07 UTC |
| ec1f1cb | Pierre Boutry | 17 June 2021, 14:47:31 UTC | finish stating lemmas | 17 June 2021, 14:47:31 UTC |
| b105c98 | Christian Doczkal | 16 June 2021, 16:47:45 UTC | first part of Real/Ideal formulation of IND-CCA2 | 16 June 2021, 16:48:13 UTC |
| 6c32d1e | Pierre Boutry | 15 June 2021, 12:20:18 UTC | inline some lemmas | 15 June 2021, 12:20:18 UTC |
| ad72aa9 | Pierre Boutry | 15 June 2021, 11:08:57 UTC | done? | 15 June 2021, 11:08:57 UTC |
| e3a5bbb | Christian Doczkal | 14 June 2021, 08:47:15 UTC | finish proof of A_bound' | 14 June 2021, 08:47:25 UTC |
| 1b09a83 | Christian Doczkal | 11 June 2021, 20:06:20 UTC | split CCA counting out of Wrap (WIP: problems with write restrictions) | 11 June 2021, 20:06:20 UTC |
| bb5d411 | Christian Doczkal | 11 June 2021, 11:54:15 UTC | stuck with A'_call (A_bound too weak?) | 11 June 2021, 11:54:15 UTC |
| ad6d972 | Pierre Boutry | 10 June 2021, 17:45:40 UTC | islossless lemmas | 10 June 2021, 17:45:40 UTC |
| 00539aa | Christian Doczkal | 10 June 2021, 15:06:24 UTC | second half of CCA_1n | 10 June 2021, 15:06:24 UTC |
| f9d36ba | Christian Doczkal | 09 June 2021, 14:44:40 UTC | first part of CCA_1n | 09 June 2021, 14:44:40 UTC |
| 3049d3f | Pierre Boutry | 09 June 2021, 11:44:57 UTC | indentation and stuff | 09 June 2021, 11:44:57 UTC |
| c61e2f9 | Christian Doczkal | 08 June 2021, 15:55:03 UTC | WIP on CCA_1n | 08 June 2021, 15:55:03 UTC |
| 6acd6c9 | Pierre Boutry | 08 June 2021, 12:44:44 UTC | reorder | 08 June 2021, 12:44:44 UTC |
| 3ccf937 | Christian Doczkal | 07 June 2021, 11:52:33 UTC | finish proof of B_bound | 07 June 2021, 11:52:33 UTC |
| 1790338 | Christian Doczkal | 04 June 2021, 11:57:19 UTC | changes from Benjamin | 04 June 2021, 11:57:19 UTC |
| 7091f1f | Christian Doczkal | 04 June 2021, 11:54:19 UTC | inital draft of oracle_PKE | 04 June 2021, 11:54:19 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 |
| 98608e4 | Benjamin Gregoire | 24 March 2021, 03:41:53 UTC | 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 | Francois Dupressoir | 17 March 2021, 15:55:39 UTC | Fix supported alt-ergo version Not that this will be valid very long... | 17 March 2021, 15:55:39 UTC |
| 4818c2e | Francois Dupressoir | 17 March 2021, 14:04:26 UTC | Document why3/prover version interactions | 17 March 2021, 14:04:26 UTC |
| ddb426b | Alley Stoughton | 16 March 2021, 16:39:12 UTC | Removing dead code. | 16 March 2021, 16:39:12 UTC |
| c19a2a7 | Pierre-Yves Strub | 03 March 2021, 14:07:57 UTC | remove debugging informations | 03 March 2021, 14:07:57 UTC |
| d6e792c | Pierre-Yves Strub | 02 March 2021, 19:46:05 UTC | tactic/if: do not eagerly simplfy the pre fix #52 | 02 March 2021, 19:47:13 UTC |
| 82b7089 | Pierre-Yves Strub | 25 February 2021, 11:46:34 UTC | refactoring proofs | 25 February 2021, 11:46:34 UTC |
| d2e0537 | Benjamin Gregoire | 25 February 2021, 10:29:19 UTC | more lemma on dbfun | 25 February 2021, 10:29:19 UTC |
| b2bc4e8 | Benjamin Gregoire | 25 February 2021, 03:37:03 UTC | add lemma dfun_ll | 25 February 2021, 03:37:03 UTC |
