| f9f81a5 | Kevin Kane | 23 October 2019, 23:55:59 UTC | Merge branch 'fstar-master' into qtesla | 23 October 2019, 23:55:59 UTC |
| 48ad88c | Kevin Kane | 23 October 2019, 22:30:39 UTC | Remove admits; assume a couple disjointness facts that should be obvious | 23 October 2019, 22:38:43 UTC |
| f5542c5 | Jonathan Protzenko | 23 October 2019, 22:10:02 UTC | Generalize proofs a little bit for and_inplace as well | 23 October 2019, 22:10:02 UTC |
| 3106bff | Jonathan Protzenko | 23 October 2019, 21:42:19 UTC | Connecting C.Loops and xor_inplace... | 23 October 2019, 21:42:19 UTC |
| 464ac22 | Kevin Kane | 23 October 2019, 16:47:47 UTC | Sync non-qTESLA hints with fstar-master to avoid conflicts | 23 October 2019, 16:47:47 UTC |
| 5ac158e | Kevin Kane | 23 October 2019, 16:47:18 UTC | Merge remote-tracking branch 'origin/fstar-master' into qtesla | 23 October 2019, 16:47:18 UTC |
| be73a2c | Dzomo the everest Yak | 23 October 2019, 08:25:21 UTC | [CI] regenerate hints | 23 October 2019, 08:25:21 UTC |
| 602c625 | Kevin Kane | 22 October 2019, 23:23:54 UTC | Delete hints from old build directory | 22 October 2019, 23:23:54 UTC |
| b64afe9 | Kevin Kane | 22 October 2019, 22:45:51 UTC | Hints | 22 October 2019, 22:45:51 UTC |
| 0af1106 | Kevin Kane | 22 October 2019, 21:52:11 UTC | Merge remote-tracking branch 'origin/fstar-master' into qtesla | 22 October 2019, 21:52:11 UTC |
| c34530c | Jonathan Protzenko | 22 October 2019, 20:37:15 UTC | Missing inline_for_extraction | 22 October 2019, 20:37:15 UTC |
| adb75e4 | Jonathan Protzenko | 22 October 2019, 20:19:04 UTC | Rely on a new pattern | 22 October 2019, 20:19:04 UTC |
| f5d466e | Jonathan Protzenko | 22 October 2019, 20:14:52 UTC | fix extract argument | 22 October 2019, 20:14:52 UTC |
| d3a624a | Jonathan Protzenko | 22 October 2019, 19:57:18 UTC | Merge remote-tracking branch 'origin/fstar-master' into quic_transport | 22 October 2019, 19:57:18 UTC |
| 21186a4 | Jonathan Protzenko | 22 October 2019, 19:56:32 UTC | hints | 22 October 2019, 19:56:32 UTC |
| dab2762 | Jonathan Protzenko | 22 October 2019, 19:41:11 UTC | Debugging proof robustness... removed one reason for non-replayable hints | 22 October 2019, 19:41:11 UTC |
| 19eb38c | Jonathan Protzenko | 22 October 2019, 19:29:36 UTC | Tweak options all over the place in the hope that the file verifies in batch mode | 22 October 2019, 19:29:36 UTC |
| 18f2300 | Jonathan Protzenko | 22 October 2019, 19:10:42 UTC | Fix up a few things following renamings, bounds changes, new preconditions... | 22 October 2019, 19:10:42 UTC |
| 295f725 | Jonathan Protzenko | 22 October 2019, 18:50:35 UTC | Merge remote-tracking branch 'other2/quic_transport' into quic_transport | 22 October 2019, 18:50:35 UTC |
| a8ff537 | Jonathan Protzenko | 22 October 2019, 18:50:31 UTC | Catch up on naming changes | 22 October 2019, 18:50:31 UTC |
| f69afd4 | Jonathan Protzenko | 22 October 2019, 18:47:33 UTC | It works... | 22 October 2019, 18:47:33 UTC |
| ebd48c4 | Jonathan Protzenko | 22 October 2019, 18:34:21 UTC | Merge remote-tracking branch 'origin/fstar-master' into quic_transport | 22 October 2019, 18:34:21 UTC |
| 983ea28 | Jonathan Protzenko | 22 October 2019, 18:29:13 UTC | WIP | 22 October 2019, 18:29:13 UTC |
| a15a2b6 | Kevin Kane | 22 October 2019, 18:24:31 UTC | Post-merge fixes | 22 October 2019, 18:24:31 UTC |
| 4dbafa8 | Jonathan Protzenko | 22 October 2019, 17:01:41 UTC | WIP | 22 October 2019, 17:01:41 UTC |
| 2ea7d03 | Santiago Zanella-Beguelin | 22 October 2019, 15:20:35 UTC | Merge pull request #197 from franziskuskiefer/patch-3 drop unused variable in update | 22 October 2019, 15:20:35 UTC |
| a62bbd9 | Franziskus Kiefer | 22 October 2019, 10:55:31 UTC | drop unused variable in update `k` is unused here. | 22 October 2019, 10:55:31 UTC |
| e0d9505 | Jonathan Protzenko | 22 October 2019, 09:20:18 UTC | Signature of create_in | 22 October 2019, 09:20:18 UTC |
| 8156a1d | Dzomo the everest Yak | 22 October 2019, 08:30:07 UTC | [CI] regenerate hints | 22 October 2019, 08:30:07 UTC |
| 3622524 | Kevin Kane | 21 October 2019, 17:35:52 UTC | Merge remote-tracking branch 'origin/fstar-master' into qtesla | 21 October 2019, 17:35:52 UTC |
| e7a753b | Santiago Zanella-Beguelin | 21 October 2019, 14:05:08 UTC | Merge remote-tracking branch 'origin/santiago_cipher' into fstar-master | 21 October 2019, 14:05:08 UTC |
| 5031109 | Santiago Zanella-Beguelin | 21 October 2019, 13:21:13 UTC | Don't inline | 21 October 2019, 13:21:13 UTC |
| 72ed93d | Santiago Zanella-Beguelin | 21 October 2019, 09:44:24 UTC | Add EverCrypt.Cipher interface | 21 October 2019, 09:44:24 UTC |
| e313a7f | Dzomo the everest Yak | 21 October 2019, 08:26:12 UTC | [CI] regenerate hints | 21 October 2019, 08:26:12 UTC |
| 2b49377 | Dzomo the everest Yak | 20 October 2019, 08:25:52 UTC | [CI] regenerate hints | 20 October 2019, 08:25:52 UTC |
| b8007d2 | Dzomo the everest Yak | 19 October 2019, 08:25:53 UTC | [CI] regenerate hints | 19 October 2019, 08:25:53 UTC |
| eb6977c | Jonathan Protzenko | 18 October 2019, 08:09:52 UTC | With Aymeric and Karthik, look at the bundling mechanism and tweak the distribution for Mozilla | 18 October 2019, 08:09:52 UTC |
| 2981493 | Jonathan Protzenko | 18 October 2019, 07:30:21 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 18 October 2019, 07:30:21 UTC |
| 80b7bad | Jonathan Protzenko | 18 October 2019, 07:30:16 UTC | Disable benchmarking on windows | 18 October 2019, 07:30:16 UTC |
| fa96731 | Santiago Zanella-Beguelin | 17 October 2019, 15:51:13 UTC | eta-expand definitions so that they get extracted to functions and defined in the text section of the library | 17 October 2019, 16:33:35 UTC |
| efe6761 | Jonathan Protzenko | 17 October 2019, 13:30:27 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 17 October 2019, 13:30:27 UTC |
| 32e4c51 | Jonathan Protzenko | 17 October 2019, 12:45:59 UTC | Enable more stuff for Mozilla | 17 October 2019, 12:45:59 UTC |
| 0c28bb7 | Aymeric Fromherz | 17 October 2019, 12:37:53 UTC | Temporary aliases in hashes specs | 17 October 2019, 12:37:53 UTC |
| d45ce8f | Jonathan Protzenko | 17 October 2019, 12:12:41 UTC | Cleaner: only include curve25519-inline for the right file | 17 October 2019, 12:12:41 UTC |
| c9b9c4a | Aymeric Fromherz | 17 October 2019, 12:11:30 UTC | Merge branch 'fstar-master' into afromher_merge | 17 October 2019, 12:11:30 UTC |
| 6127c28 | Aymeric Fromherz | 17 October 2019, 12:10:48 UTC | Fix randombuffer C implementation | 17 October 2019, 12:10:48 UTC |
| f0bc5aa | Santiago Zanella-Beguelin | 17 October 2019, 09:44:59 UTC | Document HKDF changes | 17 October 2019, 10:17:04 UTC |
| d242c99 | Aymeric Fromherz | 17 October 2019, 09:29:17 UTC | Rename randombuffer into randombuffer.System | 17 October 2019, 09:29:17 UTC |
| 5ac8e43 | Santiago Zanella-Beguelin | 17 October 2019, 09:09:44 UTC | Restore hkdf_expand, hkdf_extract as deprecated synonyms of expand, extract | 17 October 2019, 09:09:44 UTC |
| 7eeecc9 | Aymeric Fromherz | 17 October 2019, 08:56:19 UTC | Fix bundling for Salsa | 17 October 2019, 08:56:19 UTC |
| 929ab61 | Dzomo the everest Yak | 17 October 2019, 08:24:32 UTC | [CI] regenerate hints | 17 October 2019, 08:24:32 UTC |
| 2c5e0e4 | Aymeric Fromherz | 16 October 2019, 21:57:40 UTC | Port nacl and salsa from _dev | 16 October 2019, 21:57:40 UTC |
| 78612b4 | Kevin Kane | 16 October 2019, 18:22:30 UTC | Use Lib.RandomBuffer as randomness source in QTesla product code Fix bug in Lib_RandomBuffer.c so function definition matches declaration | 16 October 2019, 18:22:30 UTC |
| f1dfab5 | Santiago Zanella-Beguelin | 16 October 2019, 16:45:01 UTC | Merge pull request #195 from project-everest/santiago_hkdf HKDF | 16 October 2019, 16:45:01 UTC |
| a61fe0d | Santiago Zanella-Beguelin | 16 October 2019, 15:17:33 UTC | Merge remote-tracking branch 'origin/fstar-master' into santiago_hkdf | 16 October 2019, 15:17:33 UTC |
| af64034 | Santiago Zanella-Beguelin | 16 October 2019, 15:00:13 UTC | Simplified and assume-free non-recursive HKDF | 16 October 2019, 15:14:34 UTC |
| 8d56885 | Santiago Zanella-Beguelin | 16 October 2019, 00:14:14 UTC | WIP. Verified modulo an assume; needs simplifying | 16 October 2019, 15:03:45 UTC |
| 4291bc0 | Santiago Zanella-Beguelin | 15 October 2019, 17:40:04 UTC | WIP | 16 October 2019, 15:03:45 UTC |
| f06d8a0 | Jonathan Protzenko | 15 October 2019, 14:18:11 UTC | Don't juggle with include paths -- this prevents sharing obj dirs | 16 October 2019, 15:02:02 UTC |
| 05e3798 | Jonathan Protzenko | 15 October 2019, 13:24:51 UTC | more hints & tweaks | 16 October 2019, 15:02:01 UTC |
| 847648b | Jonathan Protzenko | 15 October 2019, 13:02:45 UTC | more sharing of local makefiles | 16 October 2019, 15:02:01 UTC |
| 1149123 | Jonathan Protzenko | 15 October 2019, 13:02:45 UTC | hints | 16 October 2019, 15:02:00 UTC |
| ab13a85 | Aymeric Fromherz | 15 October 2019, 12:01:13 UTC | Change order of arguments in cswap | 16 October 2019, 15:01:59 UTC |
| 31c425c | Jonathan Protzenko | 15 October 2019, 12:33:09 UTC | More comments and tweaking for local Makefile | 16 October 2019, 15:01:58 UTC |
| b0cd6c6 | Jonathan Protzenko | 15 October 2019, 09:38:56 UTC | And some more code to compile a test locally | 16 October 2019, 15:01:57 UTC |
| 9ab20d5 | Jonathan Protzenko | 15 October 2019, 09:31:09 UTC | Local Makefile example: curve (58 lines) | 16 October 2019, 15:01:57 UTC |
| af13804 | Jonathan Protzenko | 15 October 2019, 09:30:47 UTC | hints | 16 October 2019, 15:01:08 UTC |
| 20e2d9e | Jonathan Protzenko | 14 October 2019, 21:27:10 UTC | Get rid of all KRML_CHECK_SIZE macros for Mozilla. This is enforced at compile-time since we no longer include kremlin/internal/target.h Note that Lib.IntTypes operations are *not* reduced by the normalizer, meaning that I had to cast some buffer size multiplications into FStar.UInt32.t to make sure that at extraction-time, the size argument to the buffer allocation was a constant (for which kremlin can eliminate the size check) instead of a multiplication (for which kremlin bails and inserts a KRML_CHECK_SIZE). | 16 October 2019, 15:01:07 UTC |
| 99c3b65 | Franziskus Kiefer | 14 October 2019, 10:42:00 UTC | Unused variable in Hacl.Impl.Chacha20.fst Drop unused variable `k`. | 16 October 2019, 15:01:07 UTC |
| 8eef79b | Jonathan Protzenko | 14 October 2019, 13:20:44 UTC | Fix for Mozilla for less files in the distribution | 16 October 2019, 15:01:06 UTC |
| 3e6f8df | Aymeric Fromherz | 14 October 2019, 15:41:03 UTC | Stabilize poly proof + hints | 16 October 2019, 15:01:06 UTC |
| 625bb5a | Aymeric Fromherz | 14 October 2019, 14:41:08 UTC | Fix benchmark | 16 October 2019, 15:01:05 UTC |
| 3cdefe7 | Aymeric Fromherz | 14 October 2019, 14:40:53 UTC | Unify lib/ with _dev | 16 October 2019, 15:01:05 UTC |
| dc4babe | Aymeric Fromherz | 14 October 2019, 14:01:28 UTC | Add legacy_ prefix for SHA1 and MD5 functions | 16 October 2019, 15:01:04 UTC |
| a31f4be | Aymeric Fromherz | 14 October 2019, 13:45:33 UTC | Add Authors files | 16 October 2019, 15:01:03 UTC |
| 0957d4f | Aymeric Fromherz | 14 October 2019, 12:44:46 UTC | Minor syntactic modifications in hash specs | 16 October 2019, 15:01:03 UTC |
| 93370c9 | Aymeric Fromherz | 16 October 2019, 12:16:05 UTC | Relax length conditions on Spec.Chacha | 16 October 2019, 12:16:05 UTC |
| 886c960 | Aymeric Fromherz | 16 October 2019, 11:59:28 UTC | Minor proof stabilizations | 16 October 2019, 11:59:28 UTC |
| b69d740 | Aymeric Fromherz | 16 October 2019, 09:26:34 UTC | Include Hash.Definitions in Spec.Agile | 16 October 2019, 09:26:34 UTC |
| a7d2b85 | Aymeric Fromherz | 16 October 2019, 09:14:15 UTC | Merge branch 'fstar-master' into afromher_merge | 16 October 2019, 09:14:15 UTC |
| 7469f58 | Dzomo the everest Yak | 16 October 2019, 08:26:53 UTC | [CI] regenerate hints | 16 October 2019, 08:26:53 UTC |
| 8d0b053 | Aymeric Fromherz | 15 October 2019, 21:49:25 UTC | Merge branch 'fstar-master' into afromher_merge | 15 October 2019, 21:49:25 UTC |
| 62df1a1 | Jonathan Protzenko | 15 October 2019, 21:09:57 UTC | Minor fix | 15 October 2019, 21:09:57 UTC |
| a845337 | Jonathan Protzenko | 15 October 2019, 20:55:35 UTC | A better exemplary style | 15 October 2019, 20:55:35 UTC |
| 9294356 | Jonathan Protzenko | 15 October 2019, 20:50:10 UTC | An exemplary local Makefile for chacha20, with a local C test | 15 October 2019, 20:50:10 UTC |
| ef9081e | Aymeric Fromherz | 15 October 2019, 14:52:45 UTC | Add an interface for Spec.Agile.Hash | 15 October 2019, 14:52:45 UTC |
| 7dc0715 | Jonathan Protzenko | 15 October 2019, 14:18:42 UTC | fix | 15 October 2019, 14:18:42 UTC |
| df31663 | Jonathan Protzenko | 15 October 2019, 14:18:11 UTC | Don't juggle with include paths -- this prevents sharing obj dirs | 15 October 2019, 14:18:11 UTC |
| b5b17f3 | Jonathan Protzenko | 15 October 2019, 13:24:51 UTC | more hints & tweaks | 15 October 2019, 13:24:51 UTC |
| 3f30c12 | Jonathan Protzenko | 15 October 2019, 13:02:45 UTC | more sharing of local makefiles | 15 October 2019, 13:02:45 UTC |
| 8cbe2d0 | Jonathan Protzenko | 15 October 2019, 13:02:45 UTC | hints | 15 October 2019, 13:02:45 UTC |
| 4173f61 | Jonathan Protzenko | 15 October 2019, 12:34:53 UTC | Merge remote-tracking branch 'origin/afromher_merge' into fstar-master | 15 October 2019, 12:34:53 UTC |
| 6223aa4 | Jonathan Protzenko | 15 October 2019, 12:33:09 UTC | More comments and tweaking for local Makefile | 15 October 2019, 12:34:43 UTC |
| dbb4189 | Aymeric Fromherz | 15 October 2019, 12:01:13 UTC | Change order of arguments in cswap | 15 October 2019, 12:01:13 UTC |
| 3017925 | Jonathan Protzenko | 15 October 2019, 09:38:56 UTC | And some more code to compile a test locally | 15 October 2019, 09:38:56 UTC |
| c3d11c1 | Jonathan Protzenko | 15 October 2019, 09:31:09 UTC | Local Makefile example: curve (58 lines) | 15 October 2019, 09:31:09 UTC |
| f0f3204 | Jonathan Protzenko | 15 October 2019, 09:30:47 UTC | hints | 15 October 2019, 09:30:47 UTC |
| 6c51e27 | Jonathan Protzenko | 14 October 2019, 21:27:10 UTC | Get rid of all KRML_CHECK_SIZE macros for Mozilla. This is enforced at compile-time since we no longer include kremlin/internal/target.h Note that Lib.IntTypes operations are *not* reduced by the normalizer, meaning that I had to cast some buffer size multiplications into FStar.UInt32.t to make sure that at extraction-time, the size argument to the buffer allocation was a constant (for which kremlin can eliminate the size check) instead of a multiplication (for which kremlin bails and inserts a KRML_CHECK_SIZE). | 14 October 2019, 21:27:10 UTC |
| 08b7eed | Santiago Zanella-Beguelin | 14 October 2019, 18:18:55 UTC | Add code/hkdf | 14 October 2019, 18:18:55 UTC |
| 436f25b | Santiago Zanella-Beguelin | 14 October 2019, 17:47:36 UTC | Higher-order agile HKDF implementation | 14 October 2019, 17:48:11 UTC |
