| a208748 | Chris Hawblitzel | 04 October 2018, 18:20:48 UTC | Merge branch '_vale' into _public_proc | 04 October 2018, 18:20:48 UTC |
| 73e3470 | Bryan Parno | 04 October 2018, 16:13:39 UTC | Merge branch 'fstar-master' into _vale | 04 October 2018, 16:13:39 UTC |
| ece31d6 | Qunyan Mangus | 04 October 2018, 16:11:46 UTC | mark public procedures with {:public} attribute | 04 October 2018, 16:11:46 UTC |
| a03f119 | Jonathan Protzenko | 04 October 2018, 15:43:04 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 04 October 2018, 15:43:04 UTC |
| bbd6a1e | Jonathan Protzenko | 04 October 2018, 15:41:39 UTC | Try to regenerate hints | 04 October 2018, 15:41:39 UTC |
| 0d8cb3c | Bryan Parno | 04 October 2018, 15:05:42 UTC | Upgrade to the latest F* | 04 October 2018, 15:05:42 UTC |
| 650daab | Jonathan Protzenko | 04 October 2018, 13:57:45 UTC | hints | 04 October 2018, 13:57:45 UTC |
| 0800942 | Jonathan Protzenko | 04 October 2018, 13:02:51 UTC | Merge branch 'protz_merge' into fstar-master | 04 October 2018, 13:02:51 UTC |
| 70c0fe5 | Jonathan Protzenko | 04 October 2018, 13:01:17 UTC | Hints | 04 October 2018, 13:01:17 UTC |
| a99967f | Jonathan Protzenko | 04 October 2018, 11:33:41 UTC | Revert over-aggressive change in Vale | 04 October 2018, 11:33:41 UTC |
| 55a4e72 | Dzomo the everest Yak | 04 October 2018, 10:59:20 UTC | [CI] regenerate hints | 04 October 2018, 10:59:20 UTC |
| f1c8405 | Jonathan Protzenko | 04 October 2018, 09:57:40 UTC | Try a slightly different wording | 04 October 2018, 09:57:40 UTC |
| 462ba8c | Jonathan Protzenko | 04 October 2018, 08:07:46 UTC | A couple fresh hints... doesn't seem very different from before, though | 04 October 2018, 08:07:46 UTC |
| fca0c3d | Jonathan Protzenko | 04 October 2018, 08:04:05 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_merge | 04 October 2018, 08:04:05 UTC |
| 080f7e2 | Jonathan Protzenko | 04 October 2018, 06:24:03 UTC | Disable super fragile proof for the purposes of unblocking everest | 04 October 2018, 06:24:03 UTC |
| f92109c | Jonathan Protzenko | 03 October 2018, 15:13:42 UTC | Fresh hints, will it help? | 03 October 2018, 15:13:42 UTC |
| f481df8 | Jonathan Protzenko | 03 October 2018, 15:09:50 UTC | Hints don't see to be enough -- bump rlimit? | 03 October 2018, 15:09:50 UTC |
| dd1bf22 | Jonathan Protzenko | 03 October 2018, 15:04:48 UTC | Try increasing the rlimit | 03 October 2018, 15:04:48 UTC |
| 565e93b | Jonathan Protzenko | 03 October 2018, 14:51:51 UTC | Hints | 03 October 2018, 14:51:51 UTC |
| 8f9eb8d | Jonathan Protzenko | 03 October 2018, 14:38:12 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 03 October 2018, 14:38:12 UTC |
| fe2e97f | Jonathan Protzenko | 03 October 2018, 14:37:42 UTC | Hints | 03 October 2018, 14:37:42 UTC |
| 47cd37e | Jonathan Protzenko | 03 October 2018, 13:48:55 UTC | Fix hash-new | 03 October 2018, 13:48:55 UTC |
| 69eb9ad | Aymeric Fromherz | 03 October 2018, 13:41:26 UTC | Add interop for cpuid/sha | 03 October 2018, 13:41:26 UTC |
| c09d279 | Jonathan Protzenko | 03 October 2018, 13:28:32 UTC | Try again | 03 October 2018, 13:28:32 UTC |
| d161e2f | Aymeric Fromherz | 03 October 2018, 13:16:41 UTC | Return args in interop + Interop for cpuid/aesni | 03 October 2018, 13:16:41 UTC |
| 37470c3 | Jonathan Protzenko | 03 October 2018, 13:09:08 UTC | Try again | 03 October 2018, 13:09:08 UTC |
| c8ae271 | Jonathan Protzenko | 03 October 2018, 12:56:22 UTC | Keep compat/ on the include path | 03 October 2018, 12:56:22 UTC |
| 5c065ff | Jonathan Protzenko | 03 October 2018, 12:45:04 UTC | First step in preparation for a merge: make sure kremlib/ and kremlib/compat can co-exist on the include path | 03 October 2018, 12:45:04 UTC |
| e5530ba | Dzomo the everest Yak | 03 October 2018, 08:32:48 UTC | [CI] regenerate hints | 03 October 2018, 08:32:48 UTC |
| 595aa6e | Chris Hawblitzel | 02 October 2018, 21:14:23 UTC | Normalize "OConst?", "OReg?", "OMem?" | 02 October 2018, 21:14:23 UTC |
| 25ad7db | Aymeric Fromherz | 02 October 2018, 18:13:50 UTC | Add partial stdcalls for gctr_bytes | 02 October 2018, 18:13:50 UTC |
| 413dd9a | Aymeric Fromherz | 02 October 2018, 17:10:22 UTC | Update Interop printer and assumptions for new FunctionalExtensionality | 02 October 2018, 17:10:25 UTC |
| a661ddb | Aymeric Fromherz | 02 October 2018, 17:09:51 UTC | Update SConstruct to handle admit_smt_queries | 02 October 2018, 17:10:25 UTC |
| c0b9aac | Aymeric Fromherz | 01 October 2018, 21:12:50 UTC | Change interop main | 02 October 2018, 17:10:25 UTC |
| 7448b1b | Aymeric Fromherz | 26 September 2018, 07:05:06 UTC | Start updating taint analysis | 02 October 2018, 17:10:25 UTC |
| da7d639 | Dzomo the everest Yak | 02 October 2018, 10:53:35 UTC | [CI] regenerate hints | 02 October 2018, 10:53:35 UTC |
| bfea159 | Dzomo the everest Yak | 02 October 2018, 10:42:04 UTC | [CI] regenerate hints | 02 October 2018, 10:42:04 UTC |
| c53cae2 | Dzomo the everest Yak | 02 October 2018, 08:31:43 UTC | [CI] regenerate hints | 02 October 2018, 08:31:43 UTC |
| c46aadb | Chris Hawblitzel | 01 October 2018, 20:05:11 UTC | Increase z3rlimit | 01 October 2018, 20:05:11 UTC |
| 2763672 | Chris Hawblitzel | 01 October 2018, 17:23:20 UTC | Merge branch '_vale' into fstar-master | 01 October 2018, 17:23:20 UTC |
| c930e7c | Chris Hawblitzel | 01 October 2018, 17:20:25 UTC | Add --PROFILE option to SConstruct | 01 October 2018, 17:20:25 UTC |
| bb7cbed | Chris Hawblitzel | 01 October 2018, 17:04:27 UTC | More syntactic approach to QuickCode modifies checking for faster normalization | 01 October 2018, 17:04:27 UTC |
| 1574243 | Dzomo the everest Yak | 01 October 2018, 10:34:40 UTC | [CI] regenerate hints | 01 October 2018, 10:34:40 UTC |
| ce117b2 | Dzomo the everest Yak | 01 October 2018, 10:01:41 UTC | [CI] regenerate hints | 01 October 2018, 10:01:41 UTC |
| 010c680 | Dzomo the everest Yak | 30 September 2018, 10:36:53 UTC | [CI] regenerate hints | 30 September 2018, 10:36:53 UTC |
| f8774ad | Dzomo the everest Yak | 30 September 2018, 10:00:55 UTC | [CI] regenerate hints | 30 September 2018, 10:00:55 UTC |
| d59ff40 | Dzomo the everest Yak | 30 September 2018, 08:38:39 UTC | [CI] regenerate hints | 30 September 2018, 08:38:39 UTC |
| da8b1a2 | Dzomo the everest Yak | 29 September 2018, 10:27:23 UTC | [CI] regenerate hints | 29 September 2018, 10:27:23 UTC |
| b4ac563 | Dzomo the everest Yak | 29 September 2018, 10:02:41 UTC | [CI] regenerate hints | 29 September 2018, 10:02:41 UTC |
| d867741 | Dzomo the everest Yak | 29 September 2018, 08:38:39 UTC | [CI] regenerate hints | 29 September 2018, 08:38:39 UTC |
| 45a633a | Chris Hawblitzel | 28 September 2018, 21:58:22 UTC | Merge branch 'fstar-master' into _vale | 28 September 2018, 21:58:22 UTC |
| 6d51624 | Chris Hawblitzel | 28 September 2018, 20:44:20 UTC | Try to mitigate an unpredictable postcondition failure | 28 September 2018, 20:44:20 UTC |
| 55ff1e9 | Chris Hawblitzel | 28 September 2018, 18:52:04 UTC | Fix --RECORD-HINTS option in SConstruct so that it doesn't record hints when creating .dump files | 28 September 2018, 18:52:04 UTC |
| 50dcdde | Bryan Parno | 28 September 2018, 15:49:24 UTC | Merge branch '_vale' into _vale_cpuid | 28 September 2018, 15:49:24 UTC |
| b9b05d4 | Bryan Parno | 28 September 2018, 15:48:39 UTC | Add more time for a function that was timing out | 28 September 2018, 15:48:39 UTC |
| 64d34e4 | Bryan Parno | 28 September 2018, 15:26:39 UTC | Merge branch '_vale' into _vale_cpuid | 28 September 2018, 15:26:39 UTC |
| d83ef66 | Chris Hawblitzel | 28 September 2018, 13:57:38 UTC | Use --admit_smt_queries true when making .dump files for Vale, in case cache_checked_modules isn't working for some modules | 28 September 2018, 14:00:00 UTC |
| ad4cb71 | Dzomo the everest Yak | 28 September 2018, 09:46:25 UTC | [CI] regenerate hints | 28 September 2018, 09:46:25 UTC |
| 5eb1adf | Aseem Rastogi | 28 September 2018, 08:22:06 UTC | hints | 28 September 2018, 08:22:06 UTC |
| 801241e | Aseem Rastogi | 28 September 2018, 08:21:20 UTC | tweaking some failing vale proofs | 28 September 2018, 08:21:20 UTC |
| 0d9fceb | Chris Hawblitzel | 28 September 2018, 04:30:47 UTC | Update vale directory hints | 28 September 2018, 04:30:47 UTC |
| ef7fbf5 | Bryan Parno | 28 September 2018, 02:47:10 UTC | Merge branch '_vale' into _vale_cpuid | 28 September 2018, 02:47:10 UTC |
| 76d6eb7 | Chris Hawblitzel | 27 September 2018, 23:51:09 UTC | Work around minor F*/OCaml extraction problem | 27 September 2018, 23:51:09 UTC |
| 9707556 | Bryan Parno | 27 September 2018, 21:01:47 UTC | Merge branch '_vale' into _vale_cpuid | 27 September 2018, 21:01:47 UTC |
| d0eda3d | Chris Hawblitzel | 27 September 2018, 19:14:10 UTC | Merge branch 'fstar-master' into _vale | 27 September 2018, 19:14:10 UTC |
| 0cd3529 | Bryan Parno | 27 September 2018, 18:11:04 UTC | Add a pair of admits so BufferViewStore goes through. Given that, everything is in a verifying state | 27 September 2018, 18:11:04 UTC |
| 7b8e028 | Aseem Rastogi | 27 September 2018, 16:53:56 UTC | tested F* version for vale | 27 September 2018, 16:53:56 UTC |
| db462f4 | Aseem Rastogi | 27 September 2018, 16:10:19 UTC | merging fstar_feq branch | 27 September 2018, 16:10:19 UTC |
| 7b8ff28 | Aseem Rastogi | 27 September 2018, 16:08:56 UTC | hints | 27 September 2018, 16:08:56 UTC |
| e38cf77 | Aseem Rastogi | 27 September 2018, 16:08:46 UTC | tweaking fuel in a couple of proofs, cf. feq changes in F* master | 27 September 2018, 16:08:46 UTC |
| a32ba8b | Dzomo the everest Yak | 27 September 2018, 10:04:50 UTC | Merge commit 'a647abb827327b1c550164f7a16730c97405e587' into fstar-master | 27 September 2018, 10:04:50 UTC |
| a647abb | Dzomo the everest Yak | 27 September 2018, 10:04:45 UTC | [CI] regenerate hints | 27 September 2018, 10:04:45 UTC |
| 865bbf5 | Antoine Delignat-Lavaud | 27 September 2018, 09:41:22 UTC | Add -fparentheses for Windows path | 27 September 2018, 09:41:48 UTC |
| ca5f1b0 | Antoine Delignat-Lavaud | 27 September 2018, 09:40:03 UTC | Fix erasure of Vale calls in Hashing for Android + new static configuration without vale | 27 September 2018, 09:41:48 UTC |
| 03f9cf1 | Dzomo the everest Yak | 27 September 2018, 08:33:10 UTC | [CI] regenerate hints | 27 September 2018, 08:33:10 UTC |
| 7f1d58b | Bryan Parno | 27 September 2018, 03:00:20 UTC | Propagate CPU feature requirements | 27 September 2018, 03:00:20 UTC |
| ce48d62 | Nikhil Swamy | 26 September 2018, 22:30:28 UTC | adapt to use F.on_dom and F.restricted_t, to account for changes in FStar.FunctionalExtensionality | 26 September 2018, 22:30:28 UTC |
| 854ae35 | Nikhil Swamy | 26 September 2018, 22:29:52 UTC | bump and rlimit for an arithmetic proof | 26 September 2018, 22:29:52 UTC |
| a0d57a5 | Nikhil Swamy | 26 September 2018, 22:28:55 UTC | hint permissions | 26 September 2018, 22:28:55 UTC |
| ec8afbc | Nikhil Swamy | 26 September 2018, 22:27:53 UTC | new hints | 26 September 2018, 22:27:53 UTC |
| 1e2930c | Bryan Parno | 26 September 2018, 18:39:43 UTC | Update semantics to only allow crypto instructions when CPU supports them Still need to update the code itself | 26 September 2018, 18:39:43 UTC |
| cbcda4d | Bryan Parno | 26 September 2018, 16:22:20 UTC | Fill in proofs for admitted lemmas | 26 September 2018, 16:22:20 UTC |
| f05dc44 | Dzomo the everest Yak | 26 September 2018, 10:15:27 UTC | [CI] regenerate hints | 26 September 2018, 10:15:27 UTC |
| 627697a | Dzomo the everest Yak | 26 September 2018, 08:33:15 UTC | [CI] regenerate hints | 26 September 2018, 08:33:15 UTC |
| 2447055 | Bryan Parno | 26 September 2018, 01:43:42 UTC | Missing file! | 26 September 2018, 01:43:42 UTC |
| 4dfa3eb | Bryan Parno | 26 September 2018, 01:42:35 UTC | Add Vale procedures to check for crypto support | 26 September 2018, 01:42:35 UTC |
| c5e4cae | Chris Hawblitzel | 25 September 2018, 23:13:37 UTC | In vale/SConstruct, define ocaml_env at top level and run OCaml-generated executables in ocaml_env | 25 September 2018, 23:13:37 UTC |
| 2a15274 | Bryan Parno | 25 September 2018, 17:54:24 UTC | Add an explicit trigger to avoid Z3 explosions and prove the basic Hoare rules for CPUID | 25 September 2018, 17:54:24 UTC |
| cfaee74 | Chris Hawblitzel | 25 September 2018, 17:46:07 UTC | Fix scons --NO-VERIFY option | 25 September 2018, 17:46:47 UTC |
| 1ca9f8a | Jonathan Protzenko | 25 September 2018, 08:31:07 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 25 September 2018, 08:31:07 UTC |
| bab47d4 | Jonathan Protzenko | 25 September 2018, 08:30:58 UTC | Change path following cleanup in kremlib | 25 September 2018, 08:30:58 UTC |
| 832777b | Bryan Parno | 25 September 2018, 04:38:18 UTC | Add missing file | 25 September 2018, 04:38:18 UTC |
| 3f4886b | Bryan Parno | 25 September 2018, 04:37:13 UTC | Basic specs for crypto-relevant CPUID features | 25 September 2018, 04:37:13 UTC |
| 2862be3 | Chris Hawblitzel | 24 September 2018, 20:31:44 UTC | Fix scons --ONE option | 24 September 2018, 20:31:44 UTC |
| f3db917 | Chris Hawblitzel | 24 September 2018, 17:36:53 UTC | Upgrade vale directory to latest F* master | 24 September 2018, 17:36:53 UTC |
| a6c6d31 | Dzomo the everest Yak | 24 September 2018, 09:53:29 UTC | [CI] regenerate hints | 24 September 2018, 09:53:29 UTC |
| 195f4bb | Dzomo the everest Yak | 24 September 2018, 09:13:50 UTC | [CI] regenerate hints | 24 September 2018, 09:13:50 UTC |
| fcc852e | Dzomo the everest Yak | 24 September 2018, 08:34:58 UTC | [CI] regenerate hints | 24 September 2018, 08:34:58 UTC |
| d4ea568 | Bryan Parno | 24 September 2018, 04:24:26 UTC | Start putting together a basic SHA test harness | 24 September 2018, 04:24:58 UTC |
| 2f9cc3c | Jonathan Protzenko | 23 September 2018, 15:51:53 UTC | Try another wild guess | 23 September 2018, 15:51:53 UTC |
