| c8c1bb0 | Jonathan Protzenko | 26 November 2019, 15:24:43 UTC | forgot quic provider | 26 November 2019, 15:24:43 UTC |
| 473621f | Marina Polubelova | 26 November 2019, 14:10:29 UTC | compare chacha20 with jasmin | 26 November 2019, 14:10:29 UTC |
| 2caea5b | Dzomo the everest Yak | 26 November 2019, 09:31:03 UTC | [CI] regenerate hints | 26 November 2019, 09:31:03 UTC |
| f6672a2 | Dzomo the everest Yak | 26 November 2019, 08:37:37 UTC | [CI] regenerate hints | 26 November 2019, 08:37:37 UTC |
| 309af17 | Santiago Zanella-Beguelin | 25 November 2019, 15:43:47 UTC | Re-enable long logs for accurate stats | 25 November 2019, 15:43:47 UTC |
| 7caa70d | Benjamin Beurdouche | 25 November 2019, 12:17:32 UTC | Merge branch 'fstar-master' into _dev | 25 November 2019, 12:17:32 UTC |
| 9fc7d53 | Aseem Rastogi | 25 November 2019, 10:14:36 UTC | merging fstar-master in | 25 November 2019, 10:14:36 UTC |
| a8e5cdc | Benjamin Beurdouche | 25 November 2019, 08:51:22 UTC | Fix conflicts between dev and _dev, will restore Spec.HPKE.fst after the fact | 25 November 2019, 08:51:22 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 |
| 04f15bb | Santiago Zanella-Beguelin | 21 November 2019, 10:12:04 UTC | Merge remote-tracking branch 'origin/fstar-master' into santiago_dev | 21 November 2019, 10:12:04 UTC |
| eb93a44 | Benjamin Beurdouche | 21 November 2019, 08:39:21 UTC | Merge fstar-master in _dev | 21 November 2019, 08:39:21 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 |
| 9b370ff | Santiago Zanella-Beguelin | 20 November 2019, 15:37:14 UTC | Remove extra arguments of synthetized functions | 20 November 2019, 15:37:14 UTC |
| abbfb84 | Santiago Zanella-Beguelin | 20 November 2019, 15:36:37 UTC | Merge remote-tracking branch 'origin/fstar-master' into santiago_dev | 20 November 2019, 15:36:37 UTC |
| 5d0f44d | Santiago Zanella-Beguelin | 20 November 2019, 14:35:33 UTC | Propagate changes to implementation | 20 November 2019, 15:35:06 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 |
| 3978e71 | Santiago Zanella-Beguelin | 19 November 2019, 18:19:32 UTC | Merge remote-tracking branch 'origin/_dev' into dev | 19 November 2019, 18:19:32 UTC |
| 52c3b49 | Santiago Zanella-Beguelin | 19 November 2019, 17:28:01 UTC | Disable GF128 tests until the code is promoted from experimental | 19 November 2019, 17:28:01 UTC |
| 9478979 | Jonathan Protzenko | 19 November 2019, 16:20:03 UTC | Hints should not be executable | 19 November 2019, 16:20:03 UTC |
| 6fdcfa8 | Santiago Zanella-Beguelin | 19 November 2019, 15:26:37 UTC | Make hint replay | 19 November 2019, 16:05:27 UTC |
| 7466775 | Santiago Zanella-Beguelin | 19 November 2019, 15:26:37 UTC | Make hint replay | 19 November 2019, 15:26:37 UTC |
| 67bac14 | Benjamin Beurdouche | 15 November 2019, 20:31:44 UTC | Initial Lib.StringSequence module | 15 November 2019, 20:31:44 UTC |
| 146eac2 | Benjamin Beurdouche | 15 November 2019, 18:04:03 UTC | Implement failure printing function | 15 November 2019, 18:04:03 UTC |
| 757b11f | Benjamin Beurdouche | 15 November 2019, 17:58:36 UTC | Merge branch '_dev' of github.com:project-everest/hacl-star into _dev | 15 November 2019, 17:58:36 UTC |
| d234a0b | Benjamin Beurdouche | 15 November 2019, 17:58:22 UTC | Fix incorrect open/seal in Spec.HPKE | 15 November 2019, 17:58:22 UTC |
| a9ed4d5 | Aymeric Fromherz | 15 November 2019, 03:01:06 UTC | Merge pull request #204 from project-everest/afromher_hpke Implementation of HPKE | 15 November 2019, 03:01:06 UTC |
| ee7f9f5 | Aymeric Fromherz | 15 November 2019, 01:44:51 UTC | Merge branch 'dev' into afromher_hpke | 15 November 2019, 01:44:51 UTC |
| 5fdca44 | Aymeric Fromherz | 15 November 2019, 01:44:22 UTC | Add interface for Spec.agile.HPKE | 15 November 2019, 01:44:22 UTC |
| a307c72 | Aymeric Fromherz | 15 November 2019, 01:25:29 UTC | Address Santiago's comments | 15 November 2019, 01:25:29 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 |
| e7f8ffa | Marina Polubelova | 14 November 2019, 19:37:30 UTC | fix Makefile for poly and chacha | 14 November 2019, 19:37:30 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 |
| ac2c680 | Marina Polubelova | 13 November 2019, 18:48:59 UTC | set counter to 1 in chacha20-test | 13 November 2019, 18:48:59 UTC |
| 16ce192 | Marina Polubelova | 13 November 2019, 17:04:28 UTC | compare poly with jasmin | 13 November 2019, 17:04:28 UTC |
| 1958c77 | Marina Polubelova | 13 November 2019, 15:33:36 UTC | compare poly and chacha with openssl | 13 November 2019, 15:33:36 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 |
| d11c719 | Marina Polubelova | 12 November 2019, 12:48:45 UTC | add local Makefile for rsapss | 12 November 2019, 12:48:45 UTC |
| d2e92b4 | Santiago Zanella-Beguelin | 12 November 2019, 12:19:12 UTC | Remove test | 12 November 2019, 12:19:12 UTC |
| cd5fbc5 | Santiago Zanella-Beguelin | 12 November 2019, 12:18:09 UTC | Remove test | 12 November 2019, 12:18:09 UTC |
| 30b1e48 | Santiago Zanella-Beguelin | 12 November 2019, 10:16:16 UTC | Merge remote-tracking branch 'origin/fstar-master' into santiago_dev_ci | 12 November 2019, 11:13:08 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 |
| 67f872c | Santiago Zanella-Beguelin | 12 November 2019, 10:14:53 UTC | Ignore result of Argon2i spec test on Cygwin | 12 November 2019, 10:14:53 UTC |
| 2ea0bb8 | Dzomo the everest Yak | 12 November 2019, 08:42:53 UTC | [CI] regenerate hints | 12 November 2019, 08:42:53 UTC |
| d2790b8 | Santiago Zanella-Beguelin | 11 November 2019, 22:15:39 UTC | Patch QTesla proof | 11 November 2019, 22:41:37 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 |
| 7427a76 | Santiago Zanella-Beguelin | 11 November 2019, 18:37:27 UTC | Record new hints and use old hints for Vale.X64.Memory.fst, Hacl.Spec.BignumQ.Lemmas.fst, and MerkleTree.New.High.Correct.Rhs | 11 November 2019, 18:37:27 UTC |
| d096c90 | Santiago Zanella-Beguelin | 11 November 2019, 17:00:03 UTC | Remove equal_domains in Lib.Buffer.fst | 11 November 2019, 17:08:53 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 |
| c577df4 | Dzomo the everest Yak | 11 November 2019, 09:34:14 UTC | [CI] regenerate hints | 11 November 2019, 09:34:14 UTC |
| 7dd68bb | Dzomo the everest Yak | 11 November 2019, 08:25:59 UTC | [CI] regenerate hints | 11 November 2019, 08:25:59 UTC |
| 1a11bfe | Benjamin Beurdouche | 10 November 2019, 22:54:26 UTC | Create both libhacl and hacl .cmxa and .a files | 10 November 2019, 22:54:26 UTC |
| 10f7eb8 | Benjamin Beurdouche | 10 November 2019, 19:27:53 UTC | Merge branch '_dev' of github.com:project-everest/hacl-star into _dev | 10 November 2019, 19:27:53 UTC |
| bf89175 | Benjamin Beurdouche | 10 November 2019, 19:27:45 UTC | Attempt to include Lib.RandomSequence in libhacl.cmxa | 10 November 2019, 19:27:45 UTC |
| 901646d | Dzomo the everest Yak | 10 November 2019, 09:29:57 UTC | [CI] regenerate hints | 10 November 2019, 09:29:57 UTC |
| eb49073 | Dzomo the everest Yak | 10 November 2019, 08:25:39 UTC | [CI] regenerate hints | 10 November 2019, 08:25:39 UTC |
| f37e3f9 | Santiago Zanella-Beguelin | 09 November 2019, 11:00:13 UTC | Merge branch 'dev' into afromher_hpke | 09 November 2019, 11:00:13 UTC |
| 5670ce7 | Dzomo the everest Yak | 09 November 2019, 09:30:26 UTC | [CI] regenerate hints | 09 November 2019, 09:30:26 UTC |
| 4c67468 | Dzomo the everest Yak | 09 November 2019, 08:25:18 UTC | [CI] regenerate hints | 09 November 2019, 08:25:18 UTC |
| 01c9092 | Aymeric Fromherz | 08 November 2019, 23:55:07 UTC | HPKE: Use all_disjoint predicate for readibility | 08 November 2019, 23:55:07 UTC |
| b3a9efa | Aymeric Fromherz | 08 November 2019, 21:26:08 UTC | Remove unneeded inline_for_extraction annotations | 08 November 2019, 21:26:08 UTC |
| 14c9b36 | Marina Polubelova | 08 November 2019, 17:30:22 UTC | add local Makefile for gf128 | 08 November 2019, 17:30:22 UTC |
| 9ff791d | Marina Polubelova | 08 November 2019, 15:25:59 UTC | Merge remote-tracking branch 'origin/dev' into _dev | 08 November 2019, 15:25:59 UTC |
| d421822 | Marina Polubelova | 08 November 2019, 14:27:50 UTC | restore CInline in chacha20 and chacha20poly1305 | 08 November 2019, 14:27:50 UTC |
| 377dd72 | Marina Polubelova | 08 November 2019, 14:25:46 UTC | clean up chacha20 tests | 08 November 2019, 14:25:46 UTC |
| 3161ea1 | Marina Polubelova | 08 November 2019, 14:25:19 UTC | remove duplicate local tests | 08 November 2019, 14:25:19 UTC |
| 53b1a6e | Dzomo the everest Yak | 08 November 2019, 09:29:40 UTC | [CI] regenerate hints | 08 November 2019, 09:29:40 UTC |
| cbccb7f | Dzomo the everest Yak | 08 November 2019, 08:25:52 UTC | [CI] regenerate hints | 08 November 2019, 08:25:52 UTC |
| 3531390 | Aymeric Fromherz | 08 November 2019, 05:14:18 UTC | Merge branch 'dev' into afromher_hpke | 08 November 2019, 05:14:18 UTC |
| 980b529 | Aymeric Fromherz | 07 November 2019, 21:44:48 UTC | HPKE: Fix names of hashes in instantiations | 07 November 2019, 21:44:48 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 |
| 9201306 | Aymeric Fromherz | 07 November 2019, 21:12:03 UTC | Update HPKE to fit new spec | 07 November 2019, 21:12:03 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 |
| f4e31b7 | Marina Polubelova | 07 November 2019, 19:13:49 UTC | Merge remote-tracking branch 'origin/fstar-master' into _dev | 07 November 2019, 19:13:49 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 |
