| eff9650 | Chris Hawblitzel | 05 December 2019, 00:03:10 UTC | Better Vale quickcode support for global invariants | 05 December 2019, 00:03:10 UTC |
| a6499ff | Chris Hawblitzel | 27 November 2019, 15:50:24 UTC | Merge branch 'fstar-master' of https://github.com/project-everest/hacl-star into fstar-master | 27 November 2019, 15:50:24 UTC |
| b947b15 | Chris Hawblitzel | 27 November 2019, 13:31:29 UTC | Fix some more quantifier patterns | 27 November 2019, 13:31:29 UTC |
| 401b9ba | Jonathan Protzenko | 27 November 2019, 13:05:21 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_static | 27 November 2019, 13:05:21 UTC |
| a49bebc | Aseem Rastogi | 27 November 2019, 05:47:27 UTC | hints | 27 November 2019, 05:47:27 UTC |
| 086b36a | Aseem Rastogi | 27 November 2019, 05:47:19 UTC | tweak to incremental hash proof | 27 November 2019, 05:47:19 UTC |
| b8bf24b | Jonathan Protzenko | 27 November 2019, 02:33:02 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_static | 27 November 2019, 02:33:02 UTC |
| 28fee40 | Jonathan Protzenko | 26 November 2019, 22:20:38 UTC | hints | 26 November 2019, 22:20:38 UTC |
| cbc4577 | Jonathan Protzenko | 26 November 2019, 22:13:59 UTC | double up rilimit because of flaky proof | 26 November 2019, 22:13:59 UTC |
| ba51f45 | Jonathan Protzenko | 26 November 2019, 20:15:09 UTC | Try to fix tests and benchmark | 26 November 2019, 20:15:09 UTC |
| c1acdbe | Tahina Ramananandro | 26 November 2019, 19:30:05 UTC | try to address instable proof on Windows | 26 November 2019, 19:30:05 UTC |
| 3c44008 | Jonathan Protzenko | 26 November 2019, 17:58:23 UTC | More aggressive bundling | 26 November 2019, 17:58:23 UTC |
| 96789a2 | Jonathan Protzenko | 26 November 2019, 16:21:02 UTC | Forgot an include path | 26 November 2019, 16:21:02 UTC |
| 6c29297 | Jonathan Protzenko | 26 November 2019, 16:03:45 UTC | linking without libkremlib.a | 26 November 2019, 16:03:45 UTC |
| 5cb6e79 | Tahina Ramananandro | 26 November 2019, 15:53:31 UTC | disable the infamous unused_in_not_unused_in_disjoint2 pattern | 26 November 2019, 15:53:31 UTC |
| c8c1bb0 | Jonathan Protzenko | 26 November 2019, 15:24:43 UTC | forgot quic provider | 26 November 2019, 15:24:43 UTC |
| f6672a2 | Dzomo the everest Yak | 26 November 2019, 08:37:37 UTC | [CI] regenerate hints | 26 November 2019, 08:37:37 UTC |
| 3d3a8bc | Dzomo the everest Yak | 25 November 2019, 08:32:57 UTC | [CI] regenerate hints | 25 November 2019, 08:32:57 UTC |
| d9b8f8c | Aseem Rastogi | 24 November 2019, 17:04:17 UTC | Merge branch 'fstar-master' into aseem_buffer_functoriality | 24 November 2019, 17:04:17 UTC |
| bb29b9b | Dzomo the everest Yak | 24 November 2019, 08:29:26 UTC | [CI] regenerate hints | 24 November 2019, 08:29:26 UTC |
| 074cf01 | Aseem Rastogi | 23 November 2019, 16:08:32 UTC | Merge branch 'fstar-master' into aseem_buffer_functoriality | 23 November 2019, 16:08:32 UTC |
| c9d970b | Aseem Rastogi | 23 November 2019, 16:07:55 UTC | some proof tweaks in incremental hash | 23 November 2019, 16:07:55 UTC |
| 58251ca | Dzomo the everest Yak | 23 November 2019, 08:29:38 UTC | [CI] regenerate hints | 23 November 2019, 08:29:38 UTC |
| 00b1b40 | Jonathan Protzenko | 22 November 2019, 19:59:31 UTC | fixup following changes in the syntax of -static-header | 22 November 2019, 19:59:31 UTC |
| 72453a8 | Aseem Rastogi | 22 November 2019, 14:03:43 UTC | adding a pattern after all | 22 November 2019, 14:03:43 UTC |
| 07b61b5 | Aseem Rastogi | 22 November 2019, 13:54:36 UTC | removing a problematic pattern | 22 November 2019, 13:54:36 UTC |
| 4930dc0 | Dzomo the everest Yak | 22 November 2019, 08:29:29 UTC | [CI] regenerate hints | 22 November 2019, 08:29:29 UTC |
| 45888a0 | Guido Martínez | 21 November 2019, 21:57:01 UTC | Merge branch 'fstar-master' of github.com:mitls/hacl-star into fstar-master | 21 November 2019, 21:57:01 UTC |
| 8f1d47e | Guido Martínez | 21 November 2019, 20:20:14 UTC | commenting out some CAbstractStruct attributes These were previously ignored, and now cause issues cc @msprotz | 21 November 2019, 20:20:14 UTC |
| 94889fc | Dzomo the everest Yak | 21 November 2019, 08:28:48 UTC | [CI] regenerate hints | 21 November 2019, 08:28:48 UTC |
| 54cb7b5 | Jonathan Protzenko | 20 November 2019, 20:08:03 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 20 November 2019, 20:08:03 UTC |
| 7d95993 | Guido Martínez | 20 November 2019, 18:58:41 UTC | fix | 20 November 2019, 18:58:41 UTC |
| 52e9162 | Guido Martínez | 20 November 2019, 16:35:53 UTC | fix norm calls (zeta and iota now off by default) | 20 November 2019, 16:35:53 UTC |
| 436e4bd | Dzomo the everest Yak | 20 November 2019, 08:26:35 UTC | [CI] regenerate hints | 20 November 2019, 08:26:35 UTC |
| 717de90 | Chris Hawblitzel | 20 November 2019, 04:25:06 UTC | Change some Vale procedures to be {:quick} | 20 November 2019, 04:25:06 UTC |
| 9478979 | Jonathan Protzenko | 19 November 2019, 16:20:03 UTC | Hints should not be executable | 19 November 2019, 16:20:03 UTC |
| 7466775 | Santiago Zanella-Beguelin | 19 November 2019, 15:26:37 UTC | Make hint replay | 19 November 2019, 15:26:37 UTC |
| c7f6fde | Aymeric Fromherz | 14 November 2019, 20:05:21 UTC | rlimits | 14 November 2019, 20:05:21 UTC |
| 69c7386 | Aymeric Fromherz | 14 November 2019, 19:50:01 UTC | Stabilize EverCrypt.Autoconfig2 | 14 November 2019, 19:50:01 UTC |
| 042dfca | Aymeric Fromherz | 14 November 2019, 19:24:02 UTC | Add CPU detection for RDRAND | 14 November 2019, 19:24:02 UTC |
| 541de72 | Chris Hawblitzel | 14 November 2019, 02:52:23 UTC | Update Vale version | 14 November 2019, 02:52:23 UTC |
| 4973362 | Dzomo the everest Yak | 13 November 2019, 08:29:54 UTC | [CI] regenerate hints | 13 November 2019, 08:29:54 UTC |
| 0cade51 | Chris Hawblitzel | 12 November 2019, 19:26:35 UTC | For better proof stability in Vale/Low* interop code, avoid forall_intro because forall_intro doesn't establish a useful SMT pattern. Instead, call lemmas that use {:pattern ...} to establish a useful SMT pattern. | 12 November 2019, 19:26:35 UTC |
| 738b566 | Aymeric Fromherz | 12 November 2019, 16:07:15 UTC | Merge pull request #205 from project-everest/afromher_cpuid CPU preconditions on SSE and MOVBE | 12 November 2019, 16:07:15 UTC |
| 7f9fba6 | Aymeric Fromherz | 12 November 2019, 14:57:02 UTC | Merge branch 'fstar-master' into afromher_cpuid | 12 November 2019, 14:57:02 UTC |
| cd5fbc5 | Santiago Zanella-Beguelin | 12 November 2019, 12:18:09 UTC | Remove test | 12 November 2019, 12:18:09 UTC |
| 37232f0 | Santiago Zanella-Beguelin | 11 November 2019, 17:00:03 UTC | Remove equal_domains in Lib.Buffer.fst | 12 November 2019, 10:22:38 UTC |
| 2ea0bb8 | Dzomo the everest Yak | 12 November 2019, 08:42:53 UTC | [CI] regenerate hints | 12 November 2019, 08:42:53 UTC |
| d40b393 | Aymeric Fromherz | 11 November 2019, 19:06:26 UTC | Avoid code duplication for Vale semantics: Factorize sems for P/VP instructions | 11 November 2019, 19:06:26 UTC |
| 3bfd282 | Aymeric Fromherz | 11 November 2019, 16:16:00 UTC | Merge branch 'fstar-master' into afromher_cpuid | 11 November 2019, 16:16:00 UTC |
| 88e56bc | Aymeric Fromherz | 11 November 2019, 16:15:20 UTC | Tweak options to get hints for interop wrappers | 11 November 2019, 16:15:20 UTC |
| 7dd68bb | Dzomo the everest Yak | 11 November 2019, 08:25:59 UTC | [CI] regenerate hints | 11 November 2019, 08:25:59 UTC |
| eb49073 | Dzomo the everest Yak | 10 November 2019, 08:25:39 UTC | [CI] regenerate hints | 10 November 2019, 08:25:39 UTC |
| 4c67468 | Dzomo the everest Yak | 09 November 2019, 08:25:18 UTC | [CI] regenerate hints | 09 November 2019, 08:25:18 UTC |
| cbccb7f | Dzomo the everest Yak | 08 November 2019, 08:25:52 UTC | [CI] regenerate hints | 08 November 2019, 08:25:52 UTC |
| 5c7b290 | Aymeric Fromherz | 07 November 2019, 21:15:10 UTC | Merge branch 'fstar-master' into afromher_cpuid | 07 November 2019, 21:15:10 UTC |
| cd1d5bf | Aymeric Fromherz | 07 November 2019, 21:11:12 UTC | Propagate more CPUID preconditions through call graph | 07 November 2019, 21:11:12 UTC |
| 8efd1ca | Jonathan Protzenko | 07 November 2019, 18:00:40 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 07 November 2019, 18:00:40 UTC |
| 0c023fe | Jonathan Protzenko | 07 November 2019, 16:32:22 UTC | Fix local Makefiles for Marina | 07 November 2019, 16:32:22 UTC |
| 0948e6e | Santiago Zanella-Beguelin | 07 November 2019, 10:34:41 UTC | Merge branch 'fstar-master' into santiago_hmac_drbg | 07 November 2019, 10:34:41 UTC |
| c829362 | Santiago Zanella-Beguelin | 07 November 2019, 10:34:29 UTC | Merge remote-tracking branch 'origin/fstar-master' into santiago_hmac_drbg | 07 November 2019, 10:34:29 UTC |
| 546f65c | Santiago Zanella-Beguelin | 07 November 2019, 10:33:39 UTC | Avoid including Hacl_HMAC.c | 07 November 2019, 10:33:57 UTC |
| a13fd0f | Santiago Zanella-Beguelin | 07 November 2019, 09:49:17 UTC | Streamline test | 07 November 2019, 10:33:57 UTC |
| de5219f | Santiago Zanella-Beguelin | 07 November 2019, 09:49:17 UTC | Streamline test | 07 November 2019, 09:49:17 UTC |
| 6e8379a | Dzomo the everest Yak | 07 November 2019, 08:26:06 UTC | [CI] regenerate hints | 07 November 2019, 08:26:06 UTC |
| 4846e0e | Aymeric Fromherz | 07 November 2019, 07:24:13 UTC | Start propagating sse_enabled and movbe_enabled throughout Vale | 07 November 2019, 07:24:13 UTC |
| eb31441 | Aymeric Fromherz | 07 November 2019, 04:35:45 UTC | Update trusted Vale semantics with cpuid preconditions for sse2, ssse3, sse4.1 and movbe | 07 November 2019, 04:35:45 UTC |
| 1fc9e29 | Santiago Zanella-Beguelin | 06 November 2019, 22:52:03 UTC | Merge pull request #202 from project-everest/santiago_hmac_drbg HMAC_DRBG | 06 November 2019, 22:52:03 UTC |
| 5e9ac4c | Santiago Zanella-Beguelin | 06 November 2019, 18:30:09 UTC | Forgot an inline | 06 November 2019, 21:42:57 UTC |
| b4469bc | Santiago Zanella-Beguelin | 06 November 2019, 21:38:10 UTC | Merge branch 'fstar-master' into santiago_hmac_drbg | 06 November 2019, 21:38:10 UTC |
| 2064283 | Jonathan Protzenko | 06 November 2019, 21:16:00 UTC | Fixup Makefile for WASM | 06 November 2019, 21:16:00 UTC |
| 7220996 | Santiago Zanella-Beguelin | 06 November 2019, 11:36:15 UTC | HMAC_DRBG: add create_in function in Hacl code; check bounds in EverCrypt API rather than requiring them to hold | 06 November 2019, 17:34:59 UTC |
| 9619309 | Santiago Zanella-Beguelin | 06 November 2019, 11:44:44 UTC | Merge pull request #192 from franziskuskiefer/fstar-master-local Docker image for local builds | 06 November 2019, 11:44:44 UTC |
| 29f0495 | Santiago Zanella-Beguelin | 06 November 2019, 10:44:07 UTC | Merge branch 'fstar-master' into fstar-master-local | 06 November 2019, 10:44:07 UTC |
| 2b1f4bf | Santiago Zanella-Beguelin | 06 November 2019, 01:01:52 UTC | Factor helpers in new Lib.Meta module | 06 November 2019, 10:43:09 UTC |
| 0512089 | Dzomo the everest Yak | 06 November 2019, 08:26:48 UTC | [CI] regenerate hints | 06 November 2019, 08:26:48 UTC |
| a673f5d | Santiago Zanella-Beguelin | 06 November 2019, 00:53:01 UTC | HMAC_DRBG: Allow requesting 0 bits | 06 November 2019, 00:53:01 UTC |
| 6475ee0 | Santiago Zanella-Beguelin | 06 November 2019, 00:10:10 UTC | HMAC_DRBG: Use memset instead of fillT | 06 November 2019, 00:10:10 UTC |
| 2850f1d | Santiago Zanella-Beguelin | 05 November 2019, 18:02:20 UTC | Use output in test rather than returned_bits from test vector | 06 November 2019, 00:07:51 UTC |
| 1067610 | Santiago Zanella-Beguelin | 06 November 2019, 00:04:02 UTC | Merge branch 'fstar-master' into fstar-master-local | 06 November 2019, 00:04:02 UTC |
| fa6af3e | Santiago Zanella-Beguelin | 05 November 2019, 23:58:09 UTC | Merge branch 'fstar-master' into santiago_hmac_drbg | 05 November 2019, 23:58:09 UTC |
| c310ec7 | Santiago Zanella-Beguelin | 05 November 2019, 15:17:45 UTC | Remove hints to clean up for PR | 05 November 2019, 15:17:45 UTC |
| 0d1bf7b | Santiago Zanella-Beguelin | 05 November 2019, 14:39:38 UTC | Nits | 05 November 2019, 14:45:39 UTC |
| 8faa9e9 | Dzomo the everest Yak | 01 November 2019, 08:27:02 UTC | [CI] regenerate hints | 05 November 2019, 14:45:39 UTC |
| 080ab32 | Santiago Zanella-Beguelin | 05 November 2019, 13:33:19 UTC | Hints | 05 November 2019, 14:45:38 UTC |
| 3504349 | Santiago Zanella-Beguelin | 05 November 2019, 13:24:58 UTC | HMAC_DRBG: EverCrypt-level tests. Disable CMacro extraction; it break F* clients, which still refer to the non-extracted definition | 05 November 2019, 14:45:38 UTC |
| 6807cc0 | Santiago Zanella-Beguelin | 05 November 2019, 13:23:49 UTC | HMAC_DRBG: define disjointness predicate and remove admit | 05 November 2019, 14:45:37 UTC |
| 28f131a | Santiago Zanella-Beguelin | 04 November 2019, 17:46:03 UTC | HMAC_DRBG: Integrate into EverCrypt | 05 November 2019, 14:45:36 UTC |
| c940bb9 | Santiago Zanella-Beguelin | 04 November 2019, 10:42:39 UTC | Move DRBG spec modules to specs/drbg; add interfaces, script and Makefile to generate test vectors | 05 November 2019, 14:45:36 UTC |
| ecfeb70 | Santiago Zanella-Beguelin | 03 November 2019, 00:02:13 UTC | Hints | 05 November 2019, 14:45:35 UTC |
| 7326523 | Santiago Zanella-Beguelin | 03 November 2019, 00:01:50 UTC | HMAC-DRBG: add support for optional additional_input | 05 November 2019, 14:45:35 UTC |
| 7d7d19d | Santiago Zanella-Beguelin | 02 November 2019, 14:47:54 UTC | HMAC-DRBG: add support for optional personalization_string | 05 November 2019, 14:45:34 UTC |
| 8d6f82d | Santiago Zanella-Beguelin | 02 November 2019, 14:47:13 UTC | Hints | 05 November 2019, 14:45:34 UTC |
| 9d9f134 | Santiago Zanella-Beguelin | 02 November 2019, 13:41:33 UTC | Document what is implemented from SP 800-90 and how to use the algorithms with an entropy source | 05 November 2019, 14:45:33 UTC |
| 5b8ab84 | Santiago Zanella-Beguelin | 02 November 2019, 12:49:29 UTC | Hints | 05 November 2019, 14:45:33 UTC |
| fbd3dfd | Santiago Zanella-Beguelin | 02 November 2019, 12:14:44 UTC | Verified Hacl.HMAC_DRBG.generate | 05 November 2019, 14:45:32 UTC |
| 9a692bd | Santiago Zanella-Beguelin | 01 November 2019, 19:39:51 UTC | Add monomorphic HMAC variants | 05 November 2019, 14:45:32 UTC |
| 9fe08db | Santiago Zanella-Beguelin | 31 October 2019, 14:27:47 UTC | HMAC-DBRG | 05 November 2019, 14:45:31 UTC |
| ca14b22 | Guido Martínez | 05 November 2019, 14:24:35 UTC | fix | 05 November 2019, 14:24:35 UTC |
| a552ce0 | Guido Martínez | 05 November 2019, 13:20:11 UTC | fix splice tactic for new convention | 05 November 2019, 13:20:11 UTC |
