7a740c5 | Benjamin Gregoire | 19 April 2021, 17:34:55 UTC | Add small range hypothesis | 22 April 2021, 06:48:35 UTC |
2d0d7cd | Manuel Barbosa | 20 April 2021, 10:34:18 UTC | merge | 20 April 2021, 10:34:18 UTC |
d9bc95e | Manuel Barbosa | 20 April 2021, 10:29:30 UTC | tqrom | 20 April 2021, 10:29:30 UTC |
f847e50 | Benjamin Gregoire | 19 April 2021, 12:18:53 UTC | fix IBE_GPV.ec | 19 April 2021, 12:18:53 UTC |
cdd755f | Benjamin Gregoire | 19 April 2021, 11:26:33 UTC | error | 19 April 2021, 11:26:33 UTC |
295c5e8 | Benjamin Gregoire | 19 April 2021, 11:21:18 UTC | fix hashed_elgamal_generic | 19 April 2021, 11:21:18 UTC |
2c9f974 | Benjamin Gregoire | 19 April 2021, 11:06:23 UTC | fix br93.ec | 19 April 2021, 11:06:23 UTC |
a4de232 | Benjamin Gregoire | 19 April 2021, 05:55:07 UTC | fix DInterval.ec | 19 April 2021, 05:55:07 UTC |
90bac37 | Benjamin Gregoire | 18 April 2021, 14:33:37 UTC | fix examples | 18 April 2021, 14:33:37 UTC |
a5d2817 | Benjamin Gregoire | 18 April 2021, 14:07:39 UTC | WIP | 18 April 2021, 14:13:12 UTC |
592bcfa | Benjamin Gregoire | 14 April 2021, 17:01:10 UTC | remove admits | 18 April 2021, 14:13:11 UTC |
3a389f8 | Benjamin Gregoire | 14 April 2021, 09:49:38 UTC | reduction of IDCPA GPV to CPA | 18 April 2021, 14:13:11 UTC |
cfc4540 | Pierre-Yves Strub | 15 April 2021, 11:42:29 UTC | fix previous merge | 15 April 2021, 11:42:29 UTC |
659231b | Manuel Barbosa | 14 April 2021, 16:52:01 UTC | lazy sampling | 14 April 2021, 16:52:01 UTC |
af21698 | Pierre-Yves Strub | 14 April 2021, 16:30:51 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-quantum | 14 April 2021, 16:30:51 UTC |
bffac06 | Pierre-Yves Strub | 14 April 2021, 16:29:23 UTC | Merge branch '1.0-preview' into deploy-cost-1.0-preview | 14 April 2021, 16:29:23 UTC |
8b8fe79 | Pierre-Yves Strub | 14 April 2021, 15:58:55 UTC | Merge branch '1.0' into 1.0-preview | 14 April 2021, 15:58:55 UTC |
2afb775 | Pierre-Yves Strub | 14 April 2021, 15:27:25 UTC | StdLib: funi + same weight => eq | 14 April 2021, 15:27:25 UTC |
0d2afd4 | Manuel Barbosa | 14 April 2021, 13:12:47 UTC | Keep only generalized version | 14 April 2021, 13:12:47 UTC |
98d3bcd | Manuel Barbosa | 14 April 2021, 00:11:01 UTC | Tweaks | 14 April 2021, 00:11:01 UTC |
35ac0b5 | Manuel Barbosa | 13 April 2021, 23:44:28 UTC | small tweaks | 13 April 2021, 23:44:28 UTC |
5df6a6f | Pierre-Yves Strub | 13 April 2021, 13:34:33 UTC | StdLib: basic facts on distributions | 13 April 2021, 13:34:33 UTC |
a9a4771 | Manuel Barbosa | 13 April 2021, 11:18:56 UTC | More lazy sampling | 13 April 2021, 11:18:56 UTC |
98e33d9 | Manuel Barbosa | 13 April 2021, 01:57:26 UTC | T_QROM | 13 April 2021, 01:57:26 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 |
ff849a2 | Manuel Barbosa | 10 April 2021, 14:20:54 UTC | Fundamental lemma | 10 April 2021, 14:20:54 UTC |
c6ad4b1 | Pierre-Yves Strub | 10 April 2021, 14:05:38 UTC | StdLib: Poly: killing last admits | 10 April 2021, 14:05:38 UTC |
7c1d65d | Manuel Barbosa | 10 April 2021, 12:08:54 UTC | efficient sampling | 10 April 2021, 12:08:54 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 |
d42fe31 | Benjamin Gregoire | 08 April 2021, 14:31:57 UTC | WIP | 08 April 2021, 14:31:57 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 |
664e736 | Benjamin Gregoire | 08 April 2021, 13:07:33 UTC | WIP | 08 April 2021, 13:07:47 UTC |
71cca8a | Benjamin Gregoire | 07 April 2021, 14:12:55 UTC | start proof of GPV | 08 April 2021, 13:07:46 UTC |
2a250ec | Benjamin Gregoire | 07 April 2021, 14:12:31 UTC | add IBE definition | 08 April 2021, 13:07:46 UTC |
18abd6d | Benjamin Gregoire | 07 April 2021, 14:11:43 UTC | add CPA definition | 08 April 2021, 13:07:46 UTC |
c98fa41 | Benjamin Gregoire | 07 April 2021, 14:11:17 UTC | add PSF hypothesis | 08 April 2021, 13:07:46 UTC |
f2ed6b7 | Manuel Barbosa | 08 April 2021, 12:02:02 UTC | semi-constant update | 08 April 2021, 12:02:02 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 |
7a4c6d1 | Pierre-Yves Strub | 05 April 2021, 09:08:22 UTC | Stdlib: ring quotients | 06 April 2021, 05:28:48 UTC |
e8e4349 | Pierre-Yves Strub | 05 April 2021, 06:43:18 UTC | Stdlib: fmin | 06 April 2021, 05:28:48 UTC |
22c656e | Pierre-Yves Strub | 05 April 2021, 06:42:55 UTC | Quotient: use std def. of eqv relation | 06 April 2021, 05:28:48 UTC |
4f4e165 | Pierre-Yves Strub | 05 April 2021, 06:37:07 UTC | Stdlib: simplify proofs in Quotient.ec | 06 April 2021, 05:28:48 UTC |
101a76d | Pierre-Yves Strub | 05 April 2021, 05:51:11 UTC | Stdlib: ideas & a bit of abstract arithmetic | 06 April 2021, 05:28:48 UTC |
94ac9ac | Pierre-Yves Strub | 05 April 2021, 05:40:35 UTC | List: fix admitted proofs | 06 April 2021, 05:28:48 UTC |
8d240f6 | Pierre-Yves Strub | 05 April 2021, 05:39:57 UTC | List: size_eq1 | 06 April 2021, 05:28:48 UTC |
6084e7e | Pierre-Yves Strub | 04 April 2021, 17:54:08 UTC | README: fix why3 config command | 06 April 2021, 05:28:48 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 |
9ff108a | Alley Stoughton | 04 April 2021, 17:44:35 UTC | Merge branch '1.0' into 1.0-preview | 04 April 2021, 17:44:35 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 |
66b5409 | Pierre-Yves Strub | 03 April 2021, 17:43:58 UTC | Merge branch '1.0' into 1.0-preview | 03 April 2021, 17:43: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 |
bab83fc | Benjamin Gregoire | 30 March 2021, 10:25:55 UTC | simplify syntaxe of call rule | 30 March 2021, 10:25:55 UTC |
7dfada7 | Benjamin Gregoire | 30 March 2021, 09:55:45 UTC | WIP | 30 March 2021, 09:55:45 UTC |
ff6c7a2 | Benjamin Gregoire | 30 March 2021, 09:23:01 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-quantum | 30 March 2021, 09:23:01 UTC |
f649eab | Benjamin Gregoire | 30 March 2021, 09:22:14 UTC | add simplification lemmas on xint | 30 March 2021, 09:22:14 UTC |
a0d3acb | Benjamin Gregoire | 30 March 2021, 09:03:44 UTC | wip | 30 March 2021, 09:04:09 UTC |
130c92d | Shih-Han Hung | 28 March 2021, 18:41:04 UTC | add definition of standard secure PRG | 28 March 2021, 18:41:04 UTC |
671c8b5 | Shih-Han Hung | 28 March 2021, 04:04:28 UTC | Merge branch 'deploy-quantum' of github.com:EasyCrypt/easycrypt into deploy-quantum | 28 March 2021, 04:04:28 UTC |
368352d | Shih-Han Hung | 28 March 2021, 04:03:40 UTC | add definition of oracle secure PRG | 28 March 2021, 04:03:40 UTC |
83108d8 | Xiong Fan | 28 March 2021, 01:26:39 UTC | T_QMAC | 28 March 2021, 01:26:39 UTC |
7f064c4 | Xiong Fan | 28 March 2021, 00:12:37 UTC | delete pk in T_QMAC | 28 March 2021, 00:12:37 UTC |
aac9ed8 | Benjamin Gregoire | 27 March 2021, 05:36:40 UTC | move prf hyp into T_QROM | 27 March 2021, 05:36:40 UTC |
431c385 | Xiong Fan | 26 March 2021, 14:04:41 UTC | QPRF | 26 March 2021, 14:04:41 UTC |
2e7cdcd | François Dupressoir | 25 March 2021, 16:47:12 UTC | Proper goal for conseq equiv hoare => hoare. | 26 March 2021, 12:57:04 UTC |
a2b6505 | Benjamin Gregoire | 26 March 2021, 12:54:52 UTC | change the way of defining quantum procedure | 26 March 2021, 12:54:52 UTC |
33273b9 | Benjamin Gregoire | 26 March 2021, 11:16:31 UTC | cleanup | 26 March 2021, 11:16:31 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 |
8356907 | Benjamin Gregoire | 24 March 2021, 10:48:22 UTC | Revert "WIP" This reverts commit 6f67a21b96334a1e1c7eac07664c7c994965d007. | 24 March 2021, 10:48:22 UTC |
c30958c | Benjamin Gregoire | 24 March 2021, 06:16:49 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-quantum | 24 March 2021, 06:16:49 UTC |