| aa211c2 | Jonathan Protzenko | 24 April 2020, 21:11:09 UTC | More renamings, more test cleanups | 24 April 2020, 21:11:09 UTC |
| 6f91754 | Jonathan Protzenko | 24 April 2020, 20:28:39 UTC | More cleanup, sadly | 24 April 2020, 20:28:39 UTC |
| 540fe46 | Jonathan Protzenko | 24 April 2020, 19:45:32 UTC | Add proper early failures to the build script rather than get unscrutable vale errors later | 24 April 2020, 19:45:32 UTC |
| 832a7e8 | Jonathan Protzenko | 24 April 2020, 19:43:45 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 24 April 2020, 19:43:45 UTC |
| e86ba28 | Jonathan Protzenko | 24 April 2020, 19:36:21 UTC | typo | 24 April 2020, 19:36:21 UTC |
| f86de8c | Jonathan Protzenko | 24 April 2020, 19:34:27 UTC | An exemplary test, and some hints | 24 April 2020, 19:34:27 UTC |
| 8bd6ba2 | Jonathan Protzenko | 24 April 2020, 18:52:26 UTC | Move the logical reasoning to a separate spec file, one more lemma without nl arithmetic | 24 April 2020, 18:52:26 UTC |
| 70ec4c7 | Jonathan Protzenko | 24 April 2020, 18:09:29 UTC | Refresh selected bits of the snapshot | 24 April 2020, 18:09:29 UTC |
| 1e08089 | Jonathan Protzenko | 24 April 2020, 18:04:14 UTC | Merge branch 'protz_streaming' of pro.github.com:project-everest/hacl-star into protz_streaming | 24 April 2020, 18:04:14 UTC |
| d6b7e91 | Jonathan Protzenko | 24 April 2020, 18:01:54 UTC | Refresh selected bits of the snapshot | 24 April 2020, 18:02:35 UTC |
| 5c9ec83 | Jonathan Protzenko | 24 April 2020, 17:55:18 UTC | More sharing of definition | 24 April 2020, 17:55:18 UTC |
| a85cd04 | Jonathan Protzenko | 24 April 2020, 17:39:38 UTC | Renaming, comments | 24 April 2020, 17:39:38 UTC |
| 3444b4b | Dzomo the everest Yak | 24 April 2020, 08:21:13 UTC | [CI] regenerate hints and dist | 24 April 2020, 08:21:13 UTC |
| ab3fdfd | Marina Polubelova | 23 April 2020, 22:30:30 UTC | add precomp_inv_zeros lemma | 23 April 2020, 22:30:30 UTC |
| da9453e | Jonathan Protzenko | 23 April 2020, 19:57:35 UTC | Fix inefficiency thanks to Marina's new lemma | 23 April 2020, 19:57:35 UTC |
| 8b6588a | Jonathan Protzenko | 23 April 2020, 19:47:31 UTC | Merge remote-tracking branch 'origin/poly_ctx_zeros' into protz_streaming | 23 April 2020, 19:47:31 UTC |
| f3e83c2 | Marina Polubelova | 23 April 2020, 18:36:44 UTC | add ctx_inv_zeros lemma | 23 April 2020, 18:36:44 UTC |
| d1d43c7 | Jonathan Protzenko | 23 April 2020, 15:57:16 UTC | Also fixup OCaml bindings | 23 April 2020, 15:57:16 UTC |
| e3bc2bc | Dzomo the everest Yak | 23 April 2020, 08:22:47 UTC | [CI] regenerate hints and dist | 23 April 2020, 08:22:47 UTC |
| 59583fe | Jonathan Protzenko | 23 April 2020, 00:03:22 UTC | Selective refresh of dist | 23 April 2020, 00:03:22 UTC |
| 861fb42 | Jonathan Protzenko | 22 April 2020, 23:09:14 UTC | Dump more facts to strengthen this proof | 22 April 2020, 23:09:14 UTC |
| da3f8ad | Jonathan Protzenko | 22 April 2020, 21:53:20 UTC | Try larger rlimit | 22 April 2020, 21:53:20 UTC |
| 69423d9 | Jonathan Protzenko | 22 April 2020, 20:56:18 UTC | Address review comments | 22 April 2020, 20:58:56 UTC |
| 4e89581 | Jonathan Protzenko | 22 April 2020, 20:43:07 UTC | Kill the last flaky proof in this module | 22 April 2020, 20:43:07 UTC |
| df1e80b | Jonathan Protzenko | 22 April 2020, 20:32:01 UTC | Bump rlimit | 22 April 2020, 20:32:01 UTC |
| 5b32488 | Jonathan Protzenko | 22 April 2020, 20:29:17 UTC | Merge remote-tracking branch 'origin/master' into protz_streaming | 22 April 2020, 20:29:17 UTC |
| 40fcbb8 | Aseem Rastogi | 22 April 2020, 15:10:56 UTC | Merge pull request #286 from project-everest/_aseem_fstar_no_return Fixes for changes in F* VC generation | 22 April 2020, 15:10:56 UTC |
| fc79758 | Aseem Rastogi | 22 April 2020, 12:26:24 UTC | hints | 22 April 2020, 12:26:24 UTC |
| 67bd506 | Aseem Rastogi | 22 April 2020, 12:25:17 UTC | some tweaks for F* VC changes | 22 April 2020, 12:25:17 UTC |
| 0f7967b | Dzomo the everest Yak | 22 April 2020, 08:20:07 UTC | [CI] regenerate hints and dist | 22 April 2020, 08:20:07 UTC |
| 0bcd4ea | Dzomo the everest Yak | 21 April 2020, 08:24:45 UTC | [CI] regenerate hints and dist | 21 April 2020, 08:24:45 UTC |
| 7420b7b | Jonathan Protzenko | 21 April 2020, 04:39:19 UTC | Merge pull request #284 from project-everest/guido_bump_vale Bump Vale version to 0.3.13 | 21 April 2020, 04:39:19 UTC |
| 4e1c6c8 | Guido Martínez | 21 April 2020, 01:20:41 UTC | bump vale version | 21 April 2020, 01:20:41 UTC |
| 059787e | Dzomo the everest Yak | 20 April 2020, 08:21:22 UTC | [CI] regenerate hints and dist | 20 April 2020, 08:21:22 UTC |
| 03f1e46 | Dzomo the everest Yak | 19 April 2020, 08:20:19 UTC | [CI] regenerate hints and dist | 19 April 2020, 08:20:19 UTC |
| cc10765 | Dzomo the everest Yak | 18 April 2020, 08:20:23 UTC | [CI] regenerate hints and dist | 18 April 2020, 08:20:23 UTC |
| 5ea63a9 | Guido Martínez | 17 April 2020, 18:55:23 UTC | Merge pull request #282 from project-everest/guido_nit Remove custom lemma, use FStar.Math.Lemmas instead | 17 April 2020, 18:55:23 UTC |
| a46784e | Jonathan Protzenko | 17 April 2020, 18:13:13 UTC | Merge branch 'master' into guido_nit | 17 April 2020, 18:13:13 UTC |
| 4edacd6 | Victor Dumitrescu | 17 April 2020, 18:12:09 UTC | Merge pull request #275 from project-everest/vdum_ctypes_evercrypt OCaml API | 17 April 2020, 18:12:09 UTC |
| 69ff7c4 | Victor Dumitrescu | 17 April 2020, 15:36:44 UTC | Merge branch 'vdum_ctypes_evercrypt' of github.com:project-everest/hacl-star into vdum_ctypes_evercrypt | 17 April 2020, 15:36:44 UTC |
| 9af01f1 | Victor Dumitrescu | 17 April 2020, 15:35:21 UTC | A few more nits + update opam archive | 17 April 2020, 15:35:21 UTC |
| 333af8a | Jonathan Protzenko | 17 April 2020, 15:32:50 UTC | Merge branch 'master' into vdum_ctypes_evercrypt | 17 April 2020, 15:32:50 UTC |
| 3a84f46 | Victor Dumitrescu | 17 April 2020, 15:12:30 UTC | Merge branch 'master' of github.com:project-everest/hacl-star into vdum_ctypes_evercrypt | 17 April 2020, 15:12:30 UTC |
| b34c480 | Guido Martínez | 17 April 2020, 14:44:00 UTC | Remove custom lemma, use FStar.Math.Lemmas instead | 17 April 2020, 14:44:00 UTC |
| b96d052 | Dzomo the everest Yak | 17 April 2020, 08:20:36 UTC | [CI] regenerate hints and dist | 17 April 2020, 08:20:36 UTC |
| 4cc0657 | Jonathan Protzenko | 16 April 2020, 16:48:58 UTC | Merge remote-tracking branch 'origin/master' into vdum_ctypes_evercrypt | 16 April 2020, 16:48:58 UTC |
| 96bd4b7 | Jonathan Protzenko | 16 April 2020, 16:46:33 UTC | Merge pull request #281 from project-everest/protz_ci A configure script for ARM | 16 April 2020, 16:46:33 UTC |
| 3a0ba5b | Jonathan Protzenko | 16 April 2020, 15:03:51 UTC | Merge branch 'master' into protz_ci | 16 April 2020, 15:03:51 UTC |
| dd4761e | Victor Dumitrescu | 16 April 2020, 14:37:45 UTC | Nit | 16 April 2020, 14:37:45 UTC |
| 724d104 | Victor Dumitrescu | 16 April 2020, 09:31:08 UTC | Attempt to set environment correctly for Windows Co-authored-by: @protz | 16 April 2020, 09:31:08 UTC |
| 1674197 | Dzomo the everest Yak | 16 April 2020, 08:20:03 UTC | [CI] regenerate hints and dist | 16 April 2020, 08:20:03 UTC |
| ca37fbf | Jonathan Protzenko | 15 April 2020, 23:12:23 UTC | Revert to dynamic linking | 15 April 2020, 23:12:23 UTC |
| b9f6cf8 | Jonathan Protzenko | 15 April 2020, 22:32:53 UTC | And now try to other way with a static library, see which works on which platform | 15 April 2020, 22:32:53 UTC |
| 33b99c7 | Jonathan Protzenko | 15 April 2020, 22:21:06 UTC | Don't link the cmxa against both static and dynamic libraries | 15 April 2020, 22:21:06 UTC |
| ebb69c2 | Jonathan Protzenko | 15 April 2020, 22:04:37 UTC | Forgot dll files for windows | 15 April 2020, 22:04:37 UTC |
| 53f0308 | Victor Dumitrescu | 15 April 2020, 20:52:22 UTC | Some more build fixes | 15 April 2020, 20:52:22 UTC |
| b9e7d26 | Jonathan Protzenko | 15 April 2020, 20:40:12 UTC | Make sure configure is properly copied via nightly | 15 April 2020, 20:40:12 UTC |
| 3986157 | Jonathan Protzenko | 15 April 2020, 18:46:45 UTC | Merge branch 'master' into protz_streaming | 15 April 2020, 18:46:45 UTC |
| 354c09c | Jonathan Protzenko | 15 April 2020, 18:29:16 UTC | Off by two, try Travis again | 15 April 2020, 18:29:16 UTC |
| 9328136 | Jonathan Protzenko | 15 April 2020, 18:25:02 UTC | Tweak configure script | 15 April 2020, 18:25:02 UTC |
| 321f8c4 | Jonathan Protzenko | 15 April 2020, 18:21:31 UTC | Merge remote-tracking branch 'origin/master' into protz_ci | 15 April 2020, 18:21:31 UTC |
| 0887472 | Jonathan Protzenko | 15 April 2020, 18:20:12 UTC | Try to enable Travis for ARM | 15 April 2020, 18:20:12 UTC |
| ba5ddc6 | Jonathan Protzenko | 15 April 2020, 18:10:39 UTC | Run tests against gcc-compatible (should be the same) | 15 April 2020, 18:10:39 UTC |
| ed70189 | Jonathan Protzenko | 15 April 2020, 18:02:03 UTC | One more tweak | 15 April 2020, 18:02:03 UTC |
| d67c453 | Jonathan Protzenko | 15 April 2020, 18:01:20 UTC | One last issue | 15 April 2020, 18:01:20 UTC |
| adf0331 | Victor Dumitrescu | 15 April 2020, 17:50:31 UTC | Attempt to fix Windows build 2 | 15 April 2020, 17:50:31 UTC |
| 25d668c | Jonathan Protzenko | 15 April 2020, 17:46:36 UTC | Add proper platform guards to avoid undefined linker references on ARM | 15 April 2020, 17:46:36 UTC |
| f7de6c9 | Victor Dumitrescu | 15 April 2020, 16:15:39 UTC | Attempt to fix Windows build | 15 April 2020, 16:15:39 UTC |
| 0df449a | Victor Dumitrescu | 15 April 2020, 09:56:18 UTC | Merge branch 'master' of github.com:project-everest/hacl-star into vdum_ctypes_evercrypt | 15 April 2020, 09:56:18 UTC |
| 223b91a | Victor Dumitrescu | 15 April 2020, 09:52:35 UTC | OCaml API: Various fixes | 15 April 2020, 09:52:35 UTC |
| 94a40cb | Dzomo the everest Yak | 15 April 2020, 08:21:45 UTC | [CI] regenerate hints and dist | 15 April 2020, 08:21:45 UTC |
| 7348189 | Jonathan Protzenko | 14 April 2020, 19:15:33 UTC | A configure script for ARM | 14 April 2020, 19:15:33 UTC |
| 45a0360 | Jonathan Protzenko | 14 April 2020, 01:50:58 UTC | Merge branch 'master' into vdum_ctypes_evercrypt | 14 April 2020, 01:50:58 UTC |
| aa27ec3 | Jonathan Protzenko | 13 April 2020, 15:33:05 UTC | Merge branch 'master' into protz_streaming | 13 April 2020, 15:33:05 UTC |
| fe27d23 | Dzomo the everest Yak | 13 April 2020, 08:22:03 UTC | [CI] regenerate hints and dist | 13 April 2020, 08:22:03 UTC |
| 922bace | Dzomo the everest Yak | 12 April 2020, 08:19:27 UTC | [CI] regenerate hints and dist | 12 April 2020, 08:19:27 UTC |
| ede0f8c | Dzomo the everest Yak | 11 April 2020, 08:36:01 UTC | [CI] regenerate hints and dist | 11 April 2020, 08:36:01 UTC |
| 5fcfae2 | Dzomo the everest Yak | 10 April 2020, 08:21:43 UTC | [CI] regenerate hints and dist | 10 April 2020, 08:21:43 UTC |
| e2f1edf | Jonathan Protzenko | 09 April 2020, 22:18:24 UTC | Merge branch 'master' into protz_streaming | 09 April 2020, 22:18:24 UTC |
| 64122b3 | Jonathan Protzenko | 09 April 2020, 16:14:34 UTC | my bad | 09 April 2020, 16:14:34 UTC |
| 1cf2055 | Victor Dumitrescu | 09 April 2020, 16:10:53 UTC | Add OCaml API test to CI | 09 April 2020, 16:10:53 UTC |
| f3b5190 | Dzomo the everest Yak | 09 April 2020, 08:19:47 UTC | [CI] regenerate hints and dist | 09 April 2020, 08:19:47 UTC |
| 6f7aab3 | Jonathan Protzenko | 09 April 2020, 03:59:27 UTC | Remove superfluous lemma | 09 April 2020, 03:59:27 UTC |
| 109ef73 | Jonathan Protzenko | 09 April 2020, 00:50:08 UTC | More tweaks | 09 April 2020, 00:50:08 UTC |
| dbcfe75 | Jonathan Protzenko | 09 April 2020, 00:49:19 UTC | More tweaks | 09 April 2020, 00:49:19 UTC |
| 7a76af3 | Jonathan Protzenko | 09 April 2020, 00:29:19 UTC | Cleaner code | 09 April 2020, 00:29:19 UTC |
| 0084580 | Jonathan Protzenko | 08 April 2020, 20:04:54 UTC | Missing bits | 08 April 2020, 20:04:54 UTC |
| d5b8a9e | Jonathan Protzenko | 08 April 2020, 19:00:42 UTC | Add two new files in dist/ to show up in the diff | 08 April 2020, 19:00:42 UTC |
| 5b2fbf3 | Jonathan Protzenko | 08 April 2020, 18:59:46 UTC | Makefile tweaks | 08 April 2020, 18:59:46 UTC |
| d4ca892 | Jonathan Protzenko | 08 April 2020, 18:53:41 UTC | Apply the same prenex polymorphism trick to get monomorphization on the key type | 08 April 2020, 18:53:41 UTC |
| 8a2eebd | Jonathan Protzenko | 08 April 2020, 18:32:01 UTC | Down to some kremlin extraction errors | 08 April 2020, 18:32:01 UTC |
| 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 |
