e4af4fa | Bryan Parno | 13 August 2018, 17:46:57 UTC | Fix up decrypt as well. It's not yet optimized. | 13 August 2018, 20:13:22 UTC |
2e0c25a | Bryan Parno | 13 August 2018, 16:45:39 UTC | GCMencrypt goes all the way through! | 13 August 2018, 20:13:22 UTC |
cbecf5d | Bryan Parno | 13 August 2018, 02:47:51 UTC | Update the modifies clauses of everyone higher in the call chain | 13 August 2018, 20:13:22 UTC |
2266f06 | Bryan Parno | 13 August 2018, 01:29:57 UTC | Optimized procedure passes. | 13 August 2018, 20:13:22 UTC |
3e88567 | Bryan Parno | 13 August 2018, 00:35:39 UTC | Revamped the original gcm_one_pass_blocks to better fit its new role | 13 August 2018, 20:13:22 UTC |
572b63f | Bryan Parno | 12 August 2018, 02:23:47 UTC | Loop provides ghash_incremental now too | 13 August 2018, 20:13:21 UTC |
5dd0f51 | Bryan Parno | 12 August 2018, 00:34:22 UTC | With enough time and a targeted assertion, ghash_incremental goes through | 13 August 2018, 20:13:21 UTC |
045c9e3 | Bryan Parno | 10 August 2018, 19:55:12 UTC | Part way through adding GHash to the CTR loop | 13 August 2018, 20:13:21 UTC |
8554101 | Dzomo the everest Yak | 13 August 2018, 08:51:21 UTC | [CI] regenerate hints | 13 August 2018, 08:51:21 UTC |
f4081f2 | Chris Hawblitzel | 11 August 2018, 15:31:49 UTC | Merge branch 'fstar-master' into _vale | 11 August 2018, 15:31:49 UTC |
a6d44ba | Chris Hawblitzel | 11 August 2018, 14:19:44 UTC | Merge branch 'fstar-master' into _vale | 11 August 2018, 14:19:44 UTC |
93f28da | Chris Hawblitzel | 11 August 2018, 14:17:24 UTC | Upgrade vale directory to latest F* master | 11 August 2018, 14:17:24 UTC |
4459d64 | Jonathan Protzenko | 10 August 2018, 22:53:32 UTC | Add KOPTS | 10 August 2018, 22:53:32 UTC |
872884a | Jonathan Protzenko | 10 August 2018, 22:07:28 UTC | Remove some ahcks | 10 August 2018, 22:07:28 UTC |
323651b | Jonathan Protzenko | 10 August 2018, 21:07:52 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 10 August 2018, 21:07:52 UTC |
53b00c9 | Jonathan Protzenko | 10 August 2018, 21:07:48 UTC | Fresh hints | 10 August 2018, 21:07:48 UTC |
332f944 | Gustavo Varo | 10 August 2018, 20:59:52 UTC | Fixing build script names on the docker file | 10 August 2018, 20:59:52 UTC |
c92b6e4 | Bryan Parno | 10 August 2018, 17:33:36 UTC | Reallocate registers to align with the choices already made in GHash and GCMencrypt. For some reason, this tipped Z3 off the deep end, so I made AES rounds (locally) opaque. | 10 August 2018, 17:33:36 UTC |
70aaffa | Dzomo the everest Yak | 10 August 2018, 08:20:32 UTC | [CI] regenerate hints | 10 August 2018, 08:20:32 UTC |
642858d | Bryan Parno | 09 August 2018, 20:39:08 UTC | Use lets to make the rest of the procedures more generic | 09 August 2018, 20:39:08 UTC |
93c77c0 | Bryan Parno | 09 August 2018, 20:28:52 UTC | Add more detailed provenance info | 09 August 2018, 20:28:52 UTC |
80da895 | Bryan Parno | 09 August 2018, 20:24:58 UTC | Shuffle IV around so that our signature better matches that of the existing code (at the cost of two extra Pshufb calls) | 09 August 2018, 20:25:43 UTC |
e39e2a0 | Bryan Parno | 09 August 2018, 19:49:57 UTC | Make iv emphemeral, but restore it when we're done | 09 August 2018, 19:49:57 UTC |
00ac343 | Bryan Parno | 09 August 2018, 18:47:40 UTC | Optimize ghash a bit so that we only reverse the bytes of h once, rather than doing it for every GFmul operation | 09 August 2018, 18:47:40 UTC |
4f4fcf5 | Benjamin Beurdouche | 09 August 2018, 16:39:23 UTC | Merge branch 'master' into fstar-master | 09 August 2018, 16:39:23 UTC |
2e29da9 | Bryan Parno | 09 August 2018, 14:50:27 UTC | AESCTR loop goes through | 09 August 2018, 14:50:27 UTC |
671e257 | Bryan Parno | 09 August 2018, 14:39:58 UTC | Loop invariants verify | 09 August 2018, 14:39:58 UTC |
4e93692 | Dzomo the everest Yak | 09 August 2018, 08:20:16 UTC | [CI] regenerate hints | 09 August 2018, 08:20:16 UTC |
23e7c2f | Bryan Parno | 09 August 2018, 03:27:58 UTC | Call the loop body once! | 09 August 2018, 03:28:39 UTC |
30a832d | Bryan Parno | 08 August 2018, 20:32:53 UTC | Start prepping for the loop itself | 08 August 2018, 20:33:12 UTC |
5627750 | Bryan Parno | 08 August 2018, 20:24:52 UTC | Get the loop body into a more loop-friendly form | 08 August 2018, 20:33:12 UTC |
d9638e6 | Chris Hawblitzel | 08 August 2018, 18:19:14 UTC | In vale, remove fstar_test_suite | 08 August 2018, 18:19:49 UTC |
435ecde | Bryan Parno | 08 August 2018, 16:14:56 UTC | Make reverse_bytes_nat32 and quad32_xor opaque to improve performance of X64.AESCTR | 08 August 2018, 16:15:23 UTC |
f3ece5f | Bryan Parno | 08 August 2018, 16:14:36 UTC | Fix a small bug with --ONE mode | 08 August 2018, 16:15:23 UTC |
80aa78b | Christoph M. Wintersteiger | 08 August 2018, 15:33:26 UTC | Added missing $(KREMLIN_ARGS) | 08 August 2018, 15:33:37 UTC |
8907e8c | Santiago Zanella-Beguelin | 08 August 2018, 14:05:52 UTC | Verify as much of Test as possible | 08 August 2018, 14:05:52 UTC |
cb95906 | Dzomo the everest Yak | 08 August 2018, 08:21:05 UTC | [CI] regenerate hints | 08 August 2018, 08:21:05 UTC |
6c6f448 | Jonathan Protzenko | 08 August 2018, 01:04:51 UTC | A note and a Makefile fix | 08 August 2018, 01:04:51 UTC |
0c872ad | Chris Hawblitzel | 08 August 2018, 00:04:09 UTC | Upgrade vale directory to latest F* master | 08 August 2018, 00:05:56 UTC |
a7f7299 | Jonathan Protzenko | 07 August 2018, 23:21:43 UTC | Auto-generate the public header EverCrypt.h as part of the build | 07 August 2018, 23:21:43 UTC |
1b142e1 | Bryan Parno | 07 August 2018, 19:43:41 UTC | Restore AESCTR to the scons verification | 07 August 2018, 19:44:04 UTC |
5eecf30 | Bryan Parno | 07 August 2018, 19:43:24 UTC | Add a missing ignore file | 07 August 2018, 19:44:04 UTC |
7ad834a | Chris Hawblitzel | 07 August 2018, 16:52:32 UTC | Update min_test_suite_blacklist | 07 August 2018, 16:52:58 UTC |
aee48c7 | Santiago Zanella-Beguelin | 07 August 2018, 16:17:10 UTC | Cleanup Makefiles for test | 07 August 2018, 16:17:42 UTC |
6437e7b | Santiago Zanella-Beguelin | 07 August 2018, 15:05:55 UTC | Avoid extracting equality function twice | 07 August 2018, 15:05:55 UTC |
06eb5a8 | Antoine Delignat-Lavaud | 06 August 2018, 17:50:00 UTC | Self-contained .h for EverCrypt DLL | 07 August 2018, 13:31:27 UTC |
a0396cd | Chris Hawblitzel | 07 August 2018, 13:00:39 UTC | In vale, add note about running under Cygwin | 07 August 2018, 13:00:39 UTC |
c56c2b5 | Chris Hawblitzel | 07 August 2018, 12:38:24 UTC | When -h flag is passed to scons, print help without running any build steps | 07 August 2018, 12:40:01 UTC |
57f18db | Santiago Zanella-Beguelin | 07 August 2018, 12:19:20 UTC | Use DYLD_LIBRARY_PATH on Mac OS X | 07 August 2018, 12:20:59 UTC |
91452f3 | Santiago Zanella-Beguelin | 07 August 2018, 12:04:42 UTC | Remove EverCrypt.Hash.Test from ROOTS; couldn't find any other use outside Test | 07 August 2018, 12:20:59 UTC |
bdce9ce | Chris Hawblitzel | 07 August 2018, 12:15:11 UTC | Add more details to Vale INSTALL.md and README.md | 07 August 2018, 12:16:45 UTC |
17550fa | Santiago Zanella-Beguelin | 07 August 2018, 11:29:10 UTC | Moved code in EverCrypt.Hash.Test into Test; let's refactor individual tests later inisde files in the test folder | 07 August 2018, 11:29:10 UTC |
237cc6f | Santiago Zanella-Beguelin | 07 August 2018, 11:25:43 UTC | Correct lengths in EverCrypt.Bytes.fsti | 07 August 2018, 11:25:49 UTC |
b009cf8 | Santiago Zanella-Beguelin | 07 August 2018, 11:24:35 UTC | Specify length of generated Low* test vectors and make them recallable; verify Test.Bytes; use null instead of alloca 0uy and partially verify Test | 07 August 2018, 11:25:49 UTC |
90e1243 | Dzomo the everest Yak | 07 August 2018, 08:21:03 UTC | [CI] regenerate hints | 07 August 2018, 08:21:03 UTC |
43786ee | Gustavo Varo | 06 August 2018, 22:15:00 UTC | Fix fstar path | 06 August 2018, 22:15:00 UTC |
5708711 | Gustavo Varo | 06 August 2018, 21:07:00 UTC | removing unnecessary files from docker image | 06 August 2018, 21:07:00 UTC |
1c56b57 | Bryan Parno | 06 August 2018, 21:03:20 UTC | Initial migration of Vale's verified assembly code and supporting libraries | 06 August 2018, 21:03:20 UTC |
a449b3e | Jonathan Protzenko | 06 August 2018, 17:49:47 UTC | Fix provider build on Linux: use : to separate paths in LD_LIBRARY_PATH; include <alloca.h> or <malloc.h>, depending on the OS; define the right macros from features.h to expose the endian-ness conversion functions up to Ubuntu 14.04 | 06 August 2018, 17:49:47 UTC |
ac1f864 | Antoine Delignat-Lavaud | 06 August 2018, 14:14:34 UTC | Use abspath for Windows EverCrypt DLL | 06 August 2018, 14:14:34 UTC |
206b3fe | Antoine Delignat-Lavaud | 06 August 2018, 14:09:39 UTC | Extra LD_LIBRARY_PATH for libevercrypt.so | 06 August 2018, 14:09:39 UTC |
0a5f4cf | Antoine Delignat-Lavaud | 06 August 2018, 13:03:44 UTC | Suppress warnings with casts | 06 August 2018, 13:03:44 UTC |
252e0fe | Antoine Delignat-Lavaud | 06 August 2018, 12:11:05 UTC | Refresh hints | 06 August 2018, 12:11:05 UTC |
b0340d1 | Antoine Delignat-Lavaud | 06 August 2018, 12:10:57 UTC | Remove hard-coded kremlib include | 06 August 2018, 12:10:57 UTC |
d0990ec | Antoine Delignat-Lavaud | 06 August 2018, 12:01:48 UTC | Merge branch 'fstar-master' of github.com:mitls/hacl-star into fstar-master | 06 August 2018, 12:01:48 UTC |
9d63656 | Antoine Delignat-Lavaud | 06 August 2018, 12:01:45 UTC | Revert quic_provider build | 06 August 2018, 12:01:45 UTC |
350b049 | Santiago Zanella-Beguelin | 06 August 2018, 11:27:18 UTC | Verify Test.Vectors | 06 August 2018, 11:27:18 UTC |
04d3d3d | Santiago Zanella-Beguelin | 06 August 2018, 11:20:14 UTC | Revert "Verify Test.Vectors" This reverts commit 67e0bb0292644b8fe5e66e6909b4709d13843efa. | 06 August 2018, 11:20:14 UTC |
33878c3 | Santiago Zanella-Beguelin | 06 August 2018, 11:19:46 UTC | Generate LowStar.Buffer.null instead of allocating a non-standard empty array | 06 August 2018, 11:19:46 UTC |
421b8af | Santiago Zanella-Beguelin | 06 August 2018, 11:18:02 UTC | Don't pass NULL args to OpenSSL | 06 August 2018, 11:18:02 UTC |
33736eb | Santiago Zanella-Beguelin | 06 August 2018, 10:24:39 UTC | Allow static configurations that disable both BCrypt and OpenSSL | 06 August 2018, 10:24:39 UTC |
6bbe52d | Santiago Zanella-Beguelin | 06 August 2018, 10:05:15 UTC | Don't delete temp.h | 06 August 2018, 10:05:32 UTC |
e8bc4ad | Santiago Zanella-Beguelin | 06 August 2018, 09:48:45 UTC | Fix flags for LLVM | 06 August 2018, 10:05:32 UTC |
67e0bb0 | Santiago Zanella-Beguelin | 06 August 2018, 09:36:53 UTC | Verify Test.Vectors | 06 August 2018, 10:05:32 UTC |
64727b5 | Dzomo the everest Yak | 06 August 2018, 08:20:29 UTC | [CI] regenerate hints | 06 August 2018, 08:20:29 UTC |
4c465e0 | Dzomo the everest Yak | 05 August 2018, 08:20:30 UTC | [CI] regenerate hints | 05 August 2018, 08:20:30 UTC |
56b8c39 | Gustavo Varo | 04 August 2018, 20:15:51 UTC | stamping the fstar container image version used on the log to help during debug. | 04 August 2018, 20:15:51 UTC |
de13e82 | Gustavo Varo | 04 August 2018, 19:39:10 UTC | stamping the fstar container image version used on the log to help during debug. | 04 August 2018, 19:39:10 UTC |
b360bff | Dzomo the everest Yak | 04 August 2018, 18:50:43 UTC | [CI] regenerate hints | 04 August 2018, 18:50:43 UTC |
6c20841 | Gustavo Varo | 04 August 2018, 18:26:04 UTC | Fix the branch name on the refresh hints function. | 04 August 2018, 18:26:04 UTC |
3ebcfee | Gustavo Varo | 04 August 2018, 17:26:30 UTC | Add branch name as a container argument | 04 August 2018, 17:26:30 UTC |
c02d8db | Gustavo Varo | 04 August 2018, 16:30:54 UTC | Fix refresh hints function by adding the branchname | 04 August 2018, 16:30:54 UTC |
f94ca6e | Gustavo Varo | 04 August 2018, 16:22:26 UTC | Fix refresh hints function by adding the branchname | 04 August 2018, 16:22:26 UTC |
43eaad3 | Gustavo Varo | 04 August 2018, 14:53:16 UTC | fixing build script | 04 August 2018, 14:53:16 UTC |
c7d1afb | Gustavo Varo | 04 August 2018, 14:48:07 UTC | apply changes from ci script | 04 August 2018, 14:48:07 UTC |
dfb54ff | Jonathan Protzenko | 03 August 2018, 21:54:04 UTC | Le Sigh | 03 August 2018, 21:54:04 UTC |
1c507b2 | Jonathan Protzenko | 03 August 2018, 21:44:56 UTC | Revert hkdf/ directory to pre-Fournet state | 03 August 2018, 21:44:56 UTC |
eef0531 | Tahina Ramananandro | 03 August 2018, 21:40:13 UTC | Disable `make -C quic_provider` relying on a deprecated Makefile (with @msprotz) | 03 August 2018, 21:40:13 UTC |
376ab88 | Tahina Ramananandro | 03 August 2018, 21:39:48 UTC | Solve the last 2 `assume`s based on `loc_not_unused_in` | 03 August 2018, 21:39:48 UTC |
8cabc35 | Jonathan Protzenko | 03 August 2018, 20:28:51 UTC | Missing file | 03 August 2018, 20:28:51 UTC |
0a3c3f5 | Jonathan Protzenko | 03 August 2018, 19:02:22 UTC | Merge branch 'fournet_hkdf_again' into fstar-master | 03 August 2018, 19:02:22 UTC |
2f35644 | Jonathan Protzenko | 03 August 2018, 19:00:49 UTC | Success | 03 August 2018, 19:00:49 UTC |
3feb977 | fournet | 03 August 2018, 18:38:28 UTC | sdfsdfds | 03 August 2018, 18:38:28 UTC |
ad0838a | fournet | 03 August 2018, 18:37:32 UTC | Merge branch 'fournet_hkdf_again' of github.com:mitls/hacl-star into fournet_hkdf_again | 03 August 2018, 18:37:32 UTC |
55dfef2 | fournet | 03 August 2018, 18:33:35 UTC | added test vectors for HKDF | 03 August 2018, 18:33:35 UTC |
6d35aef | Jonathan Protzenko | 03 August 2018, 16:59:51 UTC | Remove trailing whitespace; merge fstar-master | 03 August 2018, 16:59:51 UTC |
5ce2781 | Jonathan Protzenko | 03 August 2018, 16:53:27 UTC | Merge remote-tracking branch 'origin/fstar-master' into fournet_hkdf_again | 03 August 2018, 16:53:27 UTC |
7f313ae | Antoine Delignat-Lavaud | 03 August 2018, 16:32:00 UTC | Use -windows friendly static HKDF until fournet_hkdf is finally merged | 03 August 2018, 16:32:00 UTC |
b2968c4 | fournet | 03 August 2018, 15:30:49 UTC | adding tests for Hash and HMAC | 03 August 2018, 15:30:49 UTC |
1f265d9 | Antoine Delignat-Lavaud | 03 August 2018, 13:25:04 UTC | Update for QUIC draft 13 | 03 August 2018, 13:25:04 UTC |