ff849a2 | Manuel Barbosa | 10 April 2021, 14:20:54 UTC | Fundamental lemma | 10 April 2021, 14:20:54 UTC |
7c1d65d | Manuel Barbosa | 10 April 2021, 12:08:54 UTC | efficient sampling | 10 April 2021, 12:08:54 UTC |
d42fe31 | Benjamin Gregoire | 08 April 2021, 14:31:57 UTC | WIP | 08 April 2021, 14:31:57 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 |
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 |
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 |
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 |
3990ed8 | Benjamin Gregoire | 24 March 2021, 06:10:58 UTC | fix previous merge | 24 March 2021, 06:10:58 UTC |
18fa1b6 | Benjamin Gregoire | 24 March 2021, 06:08:13 UTC | Merge branch '1.0-preview' into deploy-cost-1.0-preview | 24 March 2021, 06:08:13 UTC |
81b28cf | Benjamin Gregoire | 24 March 2021, 05:56:58 UTC | Merge branch '1.0' into 1.0-preview | 24 March 2021, 05:56:58 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 |
6f67a21 | Benjamin Gregoire | 23 March 2021, 16:03:28 UTC | WIP | 23 March 2021, 16:03:28 UTC |
84d8b6a | Benjamin Gregoire | 23 March 2021, 16:02:20 UTC | add is_finite predicate | 23 March 2021, 16:02:20 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 |
f672a21 | Alley Stoughton | 16 March 2021, 16:42:57 UTC | Merge branch '1.0' into 1.0-preview | 16 March 2021, 16:42:57 UTC |
ddb426b | Alley Stoughton | 16 March 2021, 16:39:12 UTC | Removing dead code. | 16 March 2021, 16:39:12 UTC |
2c76c51 | Benjamin Gregoire | 14 March 2021, 16:09:43 UTC | WIP | 14 March 2021, 16:09:43 UTC |
3046b3d | Benjamin Gregoire | 14 March 2021, 14:15:46 UTC | Add test for wf_quantum formulas and classical formulas, need to be propagate to all core equiv tactic | 14 March 2021, 14:15:46 UTC |
483c976 | Benjamin Gregoire | 14 March 2021, 06:25:47 UTC | start proof of FDH in the QROM | 14 March 2021, 06:25:47 UTC |
61e6f19 | Benjamin Gregoire | 14 March 2021, 06:24:45 UTC | check quantum info for subtyping | 14 March 2021, 06:24:45 UTC |
ff5192c | Benjamin Gregoire | 14 March 2021, 06:23:42 UTC | fix FDH example | 14 March 2021, 06:23:42 UTC |
fdc332f | Benjamin Gregoire | 12 March 2021, 17:49:00 UTC | start adding quantum stuff | 12 March 2021, 17:49:00 UTC |
e62237a | Benjamin Gregoire | 11 March 2021, 17:46:27 UTC | WIP | 11 March 2021, 17:46:27 UTC |
c59053a | Benjamin Gregoire | 11 March 2021, 17:03:22 UTC | Merge branch 'deploy-cost-1.0-preview' into deploy-quantum | 11 March 2021, 17:03:22 UTC |
7a82c65 | Benjamin Gregoire | 11 March 2021, 16:57:31 UTC | WIP | 11 March 2021, 16:57:31 UTC |
432d808 | Benjamin Gregoire | 10 March 2021, 11:00:25 UTC | fix hashed_elgamal_generic.ec | 10 March 2021, 11:00:25 UTC |
e79afc7 | Benjamin Gregoire | 10 March 2021, 10:48:11 UTC | fix br93 | 10 March 2021, 10:48:11 UTC |
1ea7f90 | Adrien Koutsos | 09 March 2021, 14:48:29 UTC | fixed proc and cramer-shoup | 09 March 2021, 14:48:29 UTC |
c30265e | Benjamin Gregoire | 09 March 2021, 08:18:31 UTC | add LHL | 09 March 2021, 08:18:31 UTC |
bf1d54e | Pierre-Yves Strub | 03 March 2021, 14:08:12 UTC | Merge branch '1.0' into 1.0-preview | 03 March 2021, 14:08:12 UTC |
c19a2a7 | Pierre-Yves Strub | 03 March 2021, 14:07:57 UTC | remove debugging informations | 03 March 2021, 14:07:57 UTC |
c4afc9a | Pierre-Yves Strub | 02 March 2021, 19:49:17 UTC | Merge branch '1.0' into 1.0-preview | 02 March 2021, 19:49:17 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 |
a4cff37 | Adrien Koutsos | 02 March 2021, 16:25:32 UTC | fixed async-while | 02 March 2021, 16:25:32 UTC |
5611cfd | Adrien Koutsos | 02 March 2021, 15:52:37 UTC | fixed small cost tutorial | 02 March 2021, 15:52:37 UTC |
151cbd7 | Pierre-Yves Strub | 02 March 2021, 14:58:00 UTC | done with stdlib | 02 March 2021, 14:58:00 UTC |
6a0033a | Adrien Koutsos | 02 March 2021, 13:08:30 UTC | fixed some syntax errors in examples | 02 March 2021, 13:08:30 UTC |
82b7089 | Pierre-Yves Strub | 25 February 2021, 11:46:34 UTC | refactoring proofs | 25 February 2021, 11:46:34 UTC |
baae291 | Benjamin Gregoire | 25 February 2021, 11:15:08 UTC | remove admits and axioms | 25 February 2021, 11:15:08 UTC |
dfde2a8 | Benjamin Gregoire | 25 February 2021, 10:29:54 UTC | Merge branch '1.0' into deploy-quantum | 25 February 2021, 10:29:54 UTC |
d2e0537 | Benjamin Gregoire | 25 February 2021, 10:29:19 UTC | more lemma on dbfun | 25 February 2021, 10:29:19 UTC |
a72e6d9 | Benjamin Gregoire | 25 February 2021, 03:38:09 UTC | Merge branch '1.0' into deploy-quantum | 25 February 2021, 03:38:09 UTC |
b2bc4e8 | Benjamin Gregoire | 25 February 2021, 03:37:03 UTC | add lemma dfun_ll | 25 February 2021, 03:37:03 UTC |
0479079 | Benjamin Gregoire | 25 February 2021, 03:09:48 UTC | Merge branch '1.0' into deploy-quantum | 25 February 2021, 03:09:48 UTC |
e0e995f | Pierre-Yves Strub | 24 February 2021, 23:34:31 UTC | stdlib: eager biased sampling | 24 February 2021, 23:34:31 UTC |
f4debca | Pierre-Yves Strub | 24 February 2021, 21:37:09 UTC | stdlib: more results on dfun | 24 February 2021, 21:37:09 UTC |
7a60dcc | Pierre-Yves Strub | 24 February 2021, 13:00:54 UTC | stdlib: gen. def. of distr. of functions | 24 February 2021, 13:00:54 UTC |
7a5e119 | Benjamin Gregoire | 23 February 2021, 04:59:03 UTC | try to clarify SC hyp | 23 February 2021, 04:59:03 UTC |
a45326f | Pierre-Yves Strub | 19 February 2021, 17:31:04 UTC | Merge branch '1.0' into 1.0-preview | 19 February 2021, 17:31:04 UTC |
50d97d4 | Benjamin Gregoire | 19 February 2021, 04:44:59 UTC | Skeleton for FDH | 19 February 2021, 04:44:59 UTC |
a7ca8c7 | Pierre-Yves Strub | 02 February 2021, 14:18:43 UTC | Lib: uniform distributions over finite functions | 02 February 2021, 14:18:43 UTC |
708e88c | Pierre-Yves Strub | 16 January 2021, 08:38:18 UTC | Losslessness axioms are now added to the "rnd" database | 16 January 2021, 08:38:18 UTC |
9dcb1a4 | Pierre-Yves Strub | 16 January 2021, 07:53:24 UTC | Renaming: XXX_full -> XXX_fu | 16 January 2021, 07:53:35 UTC |
7314a12 | Benjamin Gregoire | 16 January 2021, 05:42:38 UTC | printing added lemma by operator declaration | 16 January 2021, 05:43:39 UTC |
107ae0b | Adrien Koutsos | 15 January 2021, 17:26:40 UTC | Merge remote-tracking branch 'origin/1.0-preview' into deploy-cost-1.0-preview | 15 January 2021, 17:26:40 UTC |
f7e2b19 | Pierre-Yves Strub | 15 January 2021, 14:03:21 UTC | Basic results on dvector/dmatrix | 15 January 2021, 14:03:21 UTC |
b5f65bc | Pierre-Yves Strub | 15 January 2021, 09:29:53 UTC | Basic results on dvector/dmatrix | 15 January 2021, 09:29:53 UTC |
844e61b | Pierre-Yves Strub | 15 January 2021, 08:11:01 UTC | More results on dlet/dmap | 15 January 2021, 08:11:01 UTC |
6231501 | Pierre-Yves Strub | 15 January 2021, 07:20:27 UTC | In CBN, add a dedicated stack element for "match" [closes #49] | 15 January 2021, 07:20:29 UTC |
3a94832 | Pierre-Yves Strub | 14 January 2021, 20:24:20 UTC | Add `Fmatch` in cbn head-reduction. [fix #48] | 14 January 2021, 20:24:52 UTC |
b329d8f | Pierre-Yves Strub | 13 January 2021, 15:19:44 UTC | | 13 January 2021, 15:19:44 UTC |
b6414a4 | Pierre-Yves Strub | 13 January 2021, 15:16:02 UTC | Merge branch '1.0' into 1.0-preview | 13 January 2021, 15:16:02 UTC |
bb0a97a | Pierre-Yves Strub | 13 January 2021, 15:15:47 UTC | Axiomatized operators are now forcibly unfoldable | 13 January 2021, 15:15:47 UTC |
88e05a0 | Benjamin Gregoire | 12 January 2021, 14:55:42 UTC | t_subst not in the trusted base + some improvement to />. | 12 January 2021, 14:55:42 UTC |
5583bca | Benjamin Gregoire | 12 January 2021, 14:15:46 UTC | pragma -oldip become the default | 12 January 2021, 14:15:46 UTC |
ba4243a | Pierre-Yves Strub | 11 January 2021, 14:05:21 UTC | Merge branch 'deploy-debug-mark' into 1.0-preview | 11 January 2021, 14:05:21 UTC |
3a2ef0e | Pierre-Yves Strub | 11 January 2021, 14:04:57 UTC | Add debug mark | 11 January 2021, 14:04:57 UTC |
3b66108 | Pierre-Yves Strub | 05 January 2021, 12:53:49 UTC | Merge branch '1.0' into 1.0-preview | 05 January 2021, 12:53:49 UTC |
6feb5d7 | Benjamin Gregoire | 05 January 2021, 11:47:23 UTC | fix quadratic behavior of ecCallbyValue | 05 January 2021, 11:47:23 UTC |
92f57b4 | Pierre-Yves Strub | 04 January 2021, 13:25:09 UTC | Merge branch '1.0' into 1.0-preview | 04 January 2021, 13:25:09 UTC |
999561c | Pierre-Yves Strub | 04 January 2021, 13:24:41 UTC | remove deprecated "cut" tactic | 04 January 2021, 13:24:41 UTC |
cb4def3 | Pierre-Yves Strub | 04 January 2021, 10:39:56 UTC | Merge branch '1.0' into 1.0-preview | 04 January 2021, 10:39:56 UTC |
f4f3f94 | Pierre-Yves Strub | 04 January 2021, 10:26:56 UTC | implement -R flag | 04 January 2021, 10:26:56 UTC |
3671d46 | Pierre-Yves Strub | 18 December 2020, 20:07:48 UTC | Travis -> CircleCI | 18 December 2020, 20:07:48 UTC |
35e59d1 | Pierre-Yves Strub | 04 December 2020, 14:05:15 UTC | `apply` is now using product-compatible matching | 04 December 2020, 14:05:15 UTC |
6504b04 | Pierre-Yves Strub | 03 December 2020, 13:54:55 UTC | remove debug infos | 03 December 2020, 13:55:10 UTC |
3c14f4d | Benjamin Gregoire | 03 December 2020, 07:08:30 UTC | small refactoring | 03 December 2020, 07:08:30 UTC |
177f61d | Benjamin Gregoire | 03 December 2020, 05:53:30 UTC | add trivial lemma | 03 December 2020, 05:53:30 UTC |
e7ca052 | Benjamin Gregoire | 02 December 2020, 15:08:03 UTC | stack based conversion | 02 December 2020, 15:08:03 UTC |
93748b3 | Pierre-Yves Strub | 01 December 2020, 09:41:56 UTC | Decimal numbers are now translated to irreducible fractions | 01 December 2020, 09:41:56 UTC |
de9fdea | Pierre-Yves Strub | 01 December 2020, 08:48:33 UTC | In pose/trivial: use less conversion, cleanup chain of trivial calls. | 01 December 2020, 08:48:33 UTC |
68b3ffa | Benjamin Gregoire | 27 November 2020, 16:47:34 UTC | make congr less costly | 27 November 2020, 16:47:34 UTC |