6591f41 | Jonathan Protzenko | 07 April 2020, 23:23:39 UTC | Complete functor for block-based algorithms with optional key management. | 07 April 2020, 23:23:39 UTC |
c019d75 | Jonathan Protzenko | 07 April 2020, 21:42:29 UTC | Update was easier. Don't bother with optional freeability and bolt it in | 07 April 2020, 21:42:29 UTC |
45d232f | Jonathan Protzenko | 07 April 2020, 21:03:34 UTC | Got initialization to type-check with super-index types and runtime-optional keys in the streaming functor | 07 April 2020, 21:03:37 UTC |
46b54e0 | Dzomo the everest Yak | 07 April 2020, 08:23:14 UTC | [CI] regenerate hints and dist | 07 April 2020, 08:23:14 UTC |
abc0a88 | Jonathan Protzenko | 07 April 2020, 00:45:10 UTC | Some notes on how to try to achieve things | 07 April 2020, 00:45:10 UTC |
3de8861 | Jonathan Protzenko | 07 April 2020, 00:04:46 UTC | WIP containing bug repro for Guido | 07 April 2020, 00:04:46 UTC |
2de67db | Santiago Zanella-Beguelin | 06 April 2020, 23:19:10 UTC | Merge pull request #278 from project-everest/_aseem_no_abstract Removing `abstract` keyword | 06 April 2020, 23:19:10 UTC |
278d47c | Jonathan Protzenko | 06 April 2020, 23:18:23 UTC | More general interface with two options for key management | 06 April 2020, 23:18:23 UTC |
8c1f0de | Santiago Zanella-Beguelin | 06 April 2020, 22:31:32 UTC | Merge branch 'master' into _aseem_no_abstract | 06 April 2020, 22:31:32 UTC |
05e6146 | Santiago Zanella-Beguelin | 06 April 2020, 22:31:03 UTC | Merge pull request #279 from project-everest/joonwonc_merkle_tree_fix_flush Fix the proof of `mt_flush_to_` by using `rv_flush_inplace` | 06 April 2020, 22:31:03 UTC |
29eb779 | Santiago Zanella-Beguelin | 06 April 2020, 22:28:10 UTC | Merge remote-tracking branch 'origin/joonwonc_merkle_tree_fix_flush' into _aseem_no_abstract | 06 April 2020, 22:28:10 UTC |
a77cf4b | Ann Weine | 06 April 2020, 21:37:54 UTC | lemma changed for ci | 06 April 2020, 21:37:54 UTC |
5efd148 | Jonathan Protzenko | 06 April 2020, 20:31:53 UTC | Merge branch 'master' into joonwonc_merkle_tree_fix_flush | 06 April 2020, 20:31:53 UTC |
28d2820 | Joonwon Choi | 06 April 2020, 20:07:27 UTC | Fix the proof of `mt_flush_to_` by using `rv_flush_inplace` | 06 April 2020, 20:07:27 UTC |
c510947 | Aseem Rastogi | 06 April 2020, 17:12:46 UTC | make abstract usage a fatal error | 06 April 2020, 17:12:46 UTC |
3360b87 | Aseem Rastogi | 06 April 2020, 17:12:25 UTC | removing instances of the abstract keyword | 06 April 2020, 17:12:25 UTC |
9ff42fb | Dzomo the everest Yak | 06 April 2020, 08:21:49 UTC | [CI] regenerate hints and dist | 06 April 2020, 08:21:49 UTC |
a1b56ca | Dzomo the everest Yak | 05 April 2020, 08:51:40 UTC | [CI] regenerate hints and dist | 05 April 2020, 08:51:40 UTC |
5a8163d | Jonathan Protzenko | 03 April 2020, 20:41:02 UTC | Merge pull request #276 from project-everest/protz_test Cleanup tests and makefiles | 03 April 2020, 20:41:02 UTC |
3218dfa | Jonathan Protzenko | 03 April 2020, 19:44:28 UTC | Fix tests | 03 April 2020, 19:44:28 UTC |
310fce4 | Santiago Zanella-Beguelin | 03 April 2020, 17:35:19 UTC | Merge pull request #273 from project-everest/karthik_arm_neon Compatibility with ARM Neon | 03 April 2020, 17:35:19 UTC |
64525ff | karthik.bhargavan | 03 April 2020, 16:12:43 UTC | merged | 03 April 2020, 16:12:43 UTC |
141b31b | karthik.bhargavan | 03 April 2020, 16:11:39 UTC | merged | 03 April 2020, 16:11:39 UTC |
827e156 | karthik.bhargavan | 03 April 2020, 16:11:01 UTC | merged | 03 April 2020, 16:11:01 UTC |
0c952e3 | Victor Dumitrescu | 03 April 2020, 15:22:25 UTC | OCaml API: Cleanup, remove dependency on Bigstring for now | 03 April 2020, 15:22:25 UTC |
7c4b4c8 | Aseem Rastogi | 03 April 2020, 14:52:50 UTC | Merge pull request #274 from project-everest/_aseem_abstract Interfaces in F* ulib for IntN and UIntN modules | 03 April 2020, 14:52:50 UTC |
ce5b049 | Victor Dumitrescu | 03 April 2020, 13:34:17 UTC | Reset hints and dist to be the same as master again | 03 April 2020, 13:34:17 UTC |
43ac605 | Victor Dumitrescu | 03 April 2020, 13:22:38 UTC | Update snapshot | 03 April 2020, 13:22:38 UTC |
5d5fec6 | Aseem Rastogi | 03 April 2020, 13:07:59 UTC | Revert config.json | 03 April 2020, 13:07:59 UTC |
d966a81 | Aseem Rastogi | 03 April 2020, 13:07:13 UTC | Merge branch 'master' into _aseem_abstract | 03 April 2020, 13:07:13 UTC |
6c836d2 | Victor Dumitrescu | 03 April 2020, 12:58:46 UTC | Reset hints and dist to be the same as master | 03 April 2020, 12:58:46 UTC |
c30fe0c | Aseem Rastogi | 03 April 2020, 11:54:12 UTC | merkle tree | 03 April 2020, 11:54:12 UTC |
0a6b4c4 | karthik.bhargavan | 03 April 2020, 11:40:01 UTC | trying without hints | 03 April 2020, 11:40:01 UTC |
3c42016 | Aseem Rastogi | 03 April 2020, 10:31:30 UTC | removing another admit (new hints) | 03 April 2020, 10:31:30 UTC |
3888e46 | Aseem Rastogi | 03 April 2020, 10:28:58 UTC | removing one more (new hints) | 03 April 2020, 10:28:58 UTC |
3096de7 | Aseem Rastogi | 03 April 2020, 10:25:38 UTC | removing another admit (new hints) | 03 April 2020, 10:25:38 UTC |
aed5346 | Victor Dumitrescu | 03 April 2020, 10:21:47 UTC | OCaml API: opam release process | 03 April 2020, 10:21:47 UTC |
aa85a22 | Aseem Rastogi | 03 April 2020, 10:11:44 UTC | removing an admit (new hints + removing 2 assertions that I added before) | 03 April 2020, 10:11:44 UTC |
b8e0d15 | Aseem Rastogi | 03 April 2020, 10:00:13 UTC | removing an admit (new hint) | 03 April 2020, 10:00:13 UTC |
083ed1f | Victor Dumitrescu | 03 April 2020, 09:14:23 UTC | Merge branch 'master' of github.com:project-everest/hacl-star into vdum_ctypes_evercrypt | 03 April 2020, 09:14:23 UTC |
506ecfa | Dzomo the everest Yak | 03 April 2020, 08:21:59 UTC | [CI] regenerate hints and dist | 03 April 2020, 08:21:59 UTC |
165819b | Aseem Rastogi | 03 April 2020, 08:12:20 UTC | one more | 03 April 2020, 08:12:20 UTC |
ac92990 | Aseem Rastogi | 03 April 2020, 06:10:59 UTC | some more | 03 April 2020, 06:10:59 UTC |
7a36f38 | Aseem Rastogi | 03 April 2020, 05:17:30 UTC | temp admits | 03 April 2020, 05:17:30 UTC |
4841036 | Jonathan Protzenko | 03 April 2020, 00:44:35 UTC | Merge pull request #271 from project-everest/protz_noopenssl Disable OpenSSL and BCrypt | 03 April 2020, 00:44:35 UTC |
828a1c9 | Jonathan Protzenko | 02 April 2020, 23:46:25 UTC | Fix quic_provider | 02 April 2020, 23:46:25 UTC |
52519aa | Jonathan Protzenko | 02 April 2020, 23:08:51 UTC | fix | 02 April 2020, 23:08:51 UTC |
32f9a3c | Jonathan Protzenko | 02 April 2020, 22:24:48 UTC | Disable legacy tests | 02 April 2020, 22:24:48 UTC |
c305a7f | Jonathan Protzenko | 02 April 2020, 21:46:44 UTC | Kick CI | 02 April 2020, 21:46:44 UTC |
2ac35fe | Jonathan Protzenko | 02 April 2020, 20:23:12 UTC | Fix some Makefile bugs | 02 April 2020, 20:23:12 UTC |
22f64d1 | Jonathan Protzenko | 02 April 2020, 16:48:06 UTC | WIP | 02 April 2020, 16:48:06 UTC |
9dade9e | Victor Dumitrescu | 02 April 2020, 13:24:07 UTC | OCaml API: Fix disjointess check for Bytes | 02 April 2020, 13:25:23 UTC |
86b799e | Santiago Zanella-Beguelin | 02 April 2020, 10:15:47 UTC | Cleanup PR | 02 April 2020, 10:17:50 UTC |
6cd45ad | Santiago Zanella-Beguelin | 02 April 2020, 09:47:05 UTC | Merge branch 'master' into protz_noopenssl | 02 April 2020, 09:47:05 UTC |
1df4049 | Dzomo the everest Yak | 02 April 2020, 08:22:55 UTC | [CI] regenerate hints and dist | 02 April 2020, 08:22:55 UTC |
7e2a418 | Victor Dumitrescu | 01 April 2020, 19:02:01 UTC | Merge branch 'master' of github.com:project-everest/hacl-star into vdum_ctypes_evercrypt | 01 April 2020, 19:02:01 UTC |
226a07f | Jonathan Protzenko | 01 April 2020, 17:10:34 UTC | Enough with fragile proofs. One more proof with nlarith=false | 01 April 2020, 17:10:34 UTC |
629fcb5 | karthik.bhargavan | 01 April 2020, 17:05:13 UTC | merged master | 01 April 2020, 17:05:13 UTC |
fc01b0f | Jonathan Protzenko | 01 April 2020, 16:51:21 UTC | Merge pull request #269 from project-everest/denismerigoux_wasm Follow up for JS bindings | 01 April 2020, 16:51:21 UTC |
6d5f8b6 | Jonathan Protzenko | 01 April 2020, 15:54:05 UTC | Merge branch 'master' into denismerigoux_wasm | 01 April 2020, 15:54:05 UTC |
d638355 | karthik.bhargavan | 01 April 2020, 15:31:20 UTC | fixed p256 | 01 April 2020, 15:31:20 UTC |
42e057d | Jonathan Protzenko | 01 April 2020, 15:13:54 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 01 April 2020, 15:13:54 UTC |
e545f85 | Jonathan Protzenko | 01 April 2020, 15:13:40 UTC | more rlimit | 01 April 2020, 15:13:40 UTC |
759bcb7 | karthik.bhargavan | 01 April 2020, 11:58:48 UTC | added hints | 01 April 2020, 11:58:48 UTC |
0f2ffb2 | Dzomo the everest Yak | 01 April 2020, 08:20:26 UTC | [CI] regenerate hints and dist | 01 April 2020, 08:20:26 UTC |
e70ac97 | karthik.bhargavan | 01 April 2020, 06:56:46 UTC | blake2 C test | 01 April 2020, 06:56:46 UTC |
72fc35f | karthik.bhargavan | 01 April 2020, 06:56:26 UTC | sha2 C test | 01 April 2020, 06:56:26 UTC |
200ca29 | Jonathan Protzenko | 01 April 2020, 00:17:13 UTC | Merge pull request #272 from project-everest/guido_test Bump rlimits | 01 April 2020, 00:17:13 UTC |
05cb0b3 | Jonathan Protzenko | 01 April 2020, 00:04:14 UTC | Don't need a big rlimit | 01 April 2020, 00:04:14 UTC |
8ed516e | Jonathan Protzenko | 01 April 2020, 00:01:21 UTC | A proof of spec equivalence between repeat_blocks and update_multi style specifications | 01 April 2020, 00:01:21 UTC |
a4c8941 | Jonathan Protzenko | 31 March 2020, 22:20:54 UTC | WIP | 31 March 2020, 22:20:54 UTC |
2e97fde | Jonathan Protzenko | 31 March 2020, 20:00:46 UTC | A new Spec.UpdateMulti to make reasoning generic and not just hash-specific | 31 March 2020, 20:00:46 UTC |
0303e88 | Guido Martínez | 31 March 2020, 18:27:32 UTC | rlimits | 31 March 2020, 18:27:32 UTC |
072d7d7 | Jonathan Protzenko | 31 March 2020, 17:54:00 UTC | Rewrite the associativity lemma in a form that doesn't cause as many problems | 31 March 2020, 17:54:00 UTC |
c59dd0c | Jonathan Protzenko | 31 March 2020, 17:43:02 UTC | Doc update while I'm at it | 31 March 2020, 17:43:02 UTC |
4f4b329 | Jonathan Protzenko | 31 March 2020, 17:20:59 UTC | Disable OpenSSL and BCrypt by default except for dist/mitls, now the only build with the legacy interface enabled | 31 March 2020, 17:20:59 UTC |
0ff23de | Denis Merigoux | 31 March 2020, 13:03:22 UTC | Merge branch 'master' into denismerigoux_wasm | 31 March 2020, 13:03:22 UTC |
75f6fc4 | Dzomo the everest Yak | 31 March 2020, 08:22:32 UTC | [CI] regenerate hints and dist | 31 March 2020, 08:22:32 UTC |
c17b625 | Jonathan Protzenko | 30 March 2020, 19:20:03 UTC | Remove some code now that I know that let-bindings *do* bring the SMTPat into scope | 30 March 2020, 19:20:03 UTC |
0bf649c | Jonathan Protzenko | 30 March 2020, 18:31:51 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 30 March 2020, 18:31:51 UTC |
87ef605 | Jonathan Protzenko | 30 March 2020, 18:09:33 UTC | Enforce prenex polymorphism with a superfluous index and a refinement to ensure kremlin monomorphization | 30 March 2020, 18:09:33 UTC |
5d7b3a5 | Denis Merigoux | 30 March 2020, 16:04:39 UTC | Correct folder for Javascript doc cp origin | 30 March 2020, 16:04:39 UTC |
ccff3c3 | Dzomo the everest Yak | 30 March 2020, 08:27:41 UTC | [CI] regenerate hints and dist | 30 March 2020, 08:27:41 UTC |
bf27d25 | Jonathan Protzenko | 30 March 2020, 01:58:27 UTC | Ported over EverCrypt.Hash.Incremental | 30 March 2020, 01:58:27 UTC |
bee27e1 | Jonathan Protzenko | 30 March 2020, 01:18:05 UTC | Split to an fsti | 30 March 2020, 01:18:05 UTC |
461f22d | Jonathan Protzenko | 30 March 2020, 01:05:30 UTC | Done with the finish function | 30 March 2020, 01:05:30 UTC |
b6d1fdf | Jonathan Protzenko | 30 March 2020, 00:37:02 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 30 March 2020, 00:37:02 UTC |
cbf94d2 | Jonathan Protzenko | 30 March 2020, 00:36:52 UTC | Extend the type class with the final missing bits: the incrementality lemma | 30 March 2020, 00:36:52 UTC |
a9aa154 | Jonathan Protzenko | 29 March 2020, 23:49:04 UTC | Merge pull request #262 from project-everest/denismerigoux_wasm Javascript bindings for HACL-Wasm | 29 March 2020, 23:49:04 UTC |
9d71beb | Jonathan Protzenko | 29 March 2020, 23:48:31 UTC | Done with all the update variants | 29 March 2020, 23:48:31 UTC |
63276cb | Jonathan Protzenko | 29 March 2020, 22:52:10 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 29 March 2020, 22:52:10 UTC |
f8dc6fb | Jonathan Protzenko | 29 March 2020, 22:30:29 UTC | Fix Makefile for various bits, also fixup things after HPKE landed | 29 March 2020, 22:30:29 UTC |
aa7c574 | Jonathan Protzenko | 29 March 2020, 21:46:28 UTC | Merge remote-tracking branch 'origin/master' into denismerigoux_wasm | 29 March 2020, 21:46:28 UTC |
27128e0 | Jonathan Protzenko | 29 March 2020, 21:44:52 UTC | Small fix for Makefile | 29 March 2020, 21:44:52 UTC |
422b1f8 | Jonathan Protzenko | 29 March 2020, 19:53:26 UTC | whitespace | 29 March 2020, 19:53:26 UTC |
4df94ef | karthikbhargavan | 29 March 2020, 19:26:56 UTC | make in tests | 29 March 2020, 19:26:56 UTC |
9c0a3ac | karthikbhargavan | 29 March 2020, 19:12:05 UTC | passes arm tests | 29 March 2020, 19:12:05 UTC |
967fbdb | karthikbhargavan | 29 March 2020, 19:03:24 UTC | added arm tests | 29 March 2020, 19:03:24 UTC |
daafc8f | karthikbhargavan | 29 March 2020, 17:18:50 UTC | Merge branch 'karthik_blake2' of github.com:mitls/hacl-star into karthik_blake2 | 29 March 2020, 17:18:50 UTC |
7abbbe5 | karthikbhargavan | 29 March 2020, 17:18:34 UTC | fixed arm intrinsics | 29 March 2020, 17:18:34 UTC |