| 9627258 | Jonathan Protzenko | 08 April 2020, 17:57:12 UTC | Add these hints, since the whole file is 100% replayable | 08 April 2020, 17:57:12 UTC |
| 7209f20 | Jonathan Protzenko | 08 April 2020, 17:45:24 UTC | A few backwards-compat wrappers in Hash Incremental and an rlimit bump | 08 April 2020, 17:45:24 UTC |
| d952ee5 | Jonathan Protzenko | 08 April 2020, 17:12:19 UTC | Reset dist to master to minimize diff | 08 April 2020, 17:12:19 UTC |
| f864e8e | Jonathan Protzenko | 08 April 2020, 17:11:30 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 08 April 2020, 17:11:30 UTC |
| a648e17 | Jonathan Protzenko | 08 April 2020, 17:01:00 UTC | Remove the last assume | 08 April 2020, 17:01:00 UTC |
| 4da986b | Jonathan Protzenko | 08 April 2020, 16:53:14 UTC | Kill one more assume | 08 April 2020, 16:53:14 UTC |
| 2b4a4b1 | Jonathan Protzenko | 08 April 2020, 16:34:18 UTC | Finished proof of spec equivalence for poly | 08 April 2020, 16:34:18 UTC |
| 9ae0f18 | Dzomo the everest Yak | 08 April 2020, 08:28:55 UTC | [CI] regenerate hints and dist | 08 April 2020, 08:28:55 UTC |
| e122621 | Jonathan Protzenko | 08 April 2020, 00:59:51 UTC | WIP trying to kill remaining admits in poly1305 | 08 April 2020, 00:59:51 UTC |
| 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 |
