065ca5f | Marina Polubelova | 29 November 2019, 15:42:58 UTC | Merge remote-tracking branch 'origin/dev' into _dev | 29 November 2019, 15:42:58 UTC |
182b605 | Dzomo the everest Yak | 29 November 2019, 09:44:57 UTC | [CI] regenerate hints | 29 November 2019, 09:44:57 UTC |
e23ae60 | Aseem Rastogi | 29 November 2019, 02:59:46 UTC | Merge branch 'fstar-master' into aseem_dev | 29 November 2019, 02:59:46 UTC |
4a0181f | Aseem Rastogi | 28 November 2019, 15:19:34 UTC | Merge branch 'aseem_dynamic_regions_cleanup' into fstar-master | 28 November 2019, 15:19:34 UTC |
1316c7f | Dzomo the everest Yak | 28 November 2019, 13:05:32 UTC | [CI] regenerate hints | 28 November 2019, 13:05:32 UTC |
eecbb2c | Santiago Zanella-Beguelin | 28 November 2019, 11:16:26 UTC | Merge remote-tracking branch 'origin/fstar-master' into dev | 28 November 2019, 11:16:26 UTC |
9cea348 | Dzomo the everest Yak | 28 November 2019, 08:49:58 UTC | [CI] regenerate hints | 28 November 2019, 08:49:58 UTC |
a403d75 | Aseem Rastogi | 28 November 2019, 08:31:34 UTC | some proof tweak to separate out relation between total_len and max_input_len | 28 November 2019, 08:31:34 UTC |
0d9565a | Benjamin Beurdouche | 27 November 2019, 17:41:00 UTC | Refresh hints | 27 November 2019, 17:41:00 UTC |
fb529e0 | Benjamin Beurdouche | 27 November 2019, 17:40:41 UTC | Fix Chacha20 Makefile for local builds | 27 November 2019, 17:40:41 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 |
53785c8 | Aseem Rastogi | 27 November 2019, 05:47:19 UTC | tweak to incremental hash proof | 27 November 2019, 10:10:00 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 |
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 |