| 1a7d0aa | Aymeric Fromherz | 09 October 2019, 08:11:52 UTC | Propagate metapoly to chachapoly + rlimit | 09 October 2019, 08:11:52 UTC |
| 35db01d | Aymeric Fromherz | 09 October 2019, 07:13:06 UTC | Use tactic for poly1305 | 09 October 2019, 07:13:06 UTC |
| f3652b6 | Jonathan Protzenko | 08 October 2019, 12:52:26 UTC | Instantiate some things, but still need to restructure | 08 October 2019, 12:52:26 UTC |
| 6bc8151 | Jonathan Protzenko | 08 October 2019, 08:15:41 UTC | Write down some debug info | 08 October 2019, 08:15:41 UTC |
| e268263 | Jonathan Protzenko | 08 October 2019, 07:38:56 UTC | Better debug info | 08 October 2019, 07:38:56 UTC |
| 945b3f0 | Jonathan Protzenko | 08 October 2019, 07:14:18 UTC | Try with_opts | 08 October 2019, 07:14:18 UTC |
| 48ffaf9 | Jonathan Protzenko | 08 October 2019, 06:55:51 UTC | fix name collision within the tactic | 08 October 2019, 06:55:51 UTC |
| 030f7a1 | Jonathan Protzenko | 07 October 2019, 17:08:12 UTC | Try to debug a little more | 07 October 2019, 17:08:12 UTC |
| 99a502b | Jonathan Protzenko | 07 October 2019, 17:07:34 UTC | Merge branch 'protz_meta_interfaces' of pro.github.com:mitls/hacl-star into protz_meta_interfaces | 07 October 2019, 17:07:34 UTC |
| 582160e | Jonathan Protzenko | 07 October 2019, 16:48:42 UTC | Merge branch 'fstar-master' into protz_meta_interfaces | 07 October 2019, 16:48:42 UTC |
| 68c6955 | Guido Martínez | 07 October 2019, 15:17:00 UTC | Meta.Interface: fixes with @msprotz | 07 October 2019, 15:17:00 UTC |
| defd606 | Dzomo the everest Yak | 07 October 2019, 08:29:33 UTC | [CI] regenerate hints | 07 October 2019, 08:29:33 UTC |
| b89f213 | Jonathan Protzenko | 06 October 2019, 16:22:38 UTC | state of the bug | 06 October 2019, 16:22:38 UTC |
| 90088ba | Jonathan Protzenko | 06 October 2019, 16:07:17 UTC | fix a bug in the tactic; try to debug the rest | 06 October 2019, 16:07:17 UTC |
| 454f6d9 | Dzomo the everest Yak | 05 October 2019, 08:26:41 UTC | [CI] regenerate hints | 05 October 2019, 08:26:41 UTC |
| f5a6894 | Jonathan Protzenko | 04 October 2019, 17:27:17 UTC | Names are wrong | 04 October 2019, 17:27:17 UTC |
| 2d1bfb6 | Jonathan Protzenko | 04 October 2019, 16:03:12 UTC | Fix a few bugs. Don't run this yet -- uses up to 25GB | 04 October 2019, 16:03:12 UTC |
| d89f09d | Jonathan Protzenko | 04 October 2019, 14:55:51 UTC | Snapshot | 04 October 2019, 14:55:51 UTC |
| eb9adc1 | Jonathan Protzenko | 04 October 2019, 12:54:11 UTC | Take the index as an extra parameter | 04 October 2019, 12:54:11 UTC |
| 9c7fd25 | Jonathan Protzenko | 04 October 2019, 12:46:30 UTC | missing file | 04 October 2019, 12:46:30 UTC |
| 76f6fd9 | Jonathan Protzenko | 04 October 2019, 12:37:17 UTC | Annotations should be roughly ok | 04 October 2019, 12:37:17 UTC |
| b8cb23c | Jonathan Protzenko | 04 October 2019, 10:28:32 UTC | Sanity check | 04 October 2019, 10:28:32 UTC |
| 5e380d2 | Jonathan Protzenko | 04 October 2019, 10:16:14 UTC | WIP | 04 October 2019, 10:16:14 UTC |
| 14db060 | Jonathan Protzenko | 04 October 2019, 10:09:31 UTC | Broken state exhibiting the error for Guido | 04 October 2019, 10:09:31 UTC |
| 5725bb0 | Jonathan Protzenko | 04 October 2019, 10:01:03 UTC | WIP; a small optimization to generate less declarations | 04 October 2019, 10:01:03 UTC |
| fd78aa7 | Chris Hawblitzel | 03 October 2019, 21:15:11 UTC | Merge branch 'fstar-master' into ckh_instr-reordering-aesgcm-rebased | 03 October 2019, 21:15:11 UTC |
| d8b7f01 | Chris Hawblitzel | 03 October 2019, 20:37:34 UTC | In Vale.Transformers, increase z3rlimits and add decreases clause | 03 October 2019, 20:37:34 UTC |
| 328a7bd | Chris Hawblitzel | 03 October 2019, 18:41:50 UTC | Update Vale.Transformers to use Type u#1 heap and replace "assume val lemma_to_of" with Vale.X64.StateLemmas.lemma_to_of | 03 October 2019, 18:41:50 UTC |
| c11311e | Jonathan Protzenko | 03 October 2019, 15:51:26 UTC | WIP; need to re-run the tactic and add the right inline_for_extraction | 03 October 2019, 15:51:26 UTC |
| 327a3d3 | Jonathan Protzenko | 03 October 2019, 14:23:12 UTC | WIP; individual specializations will have to friend the Meta module, too | 03 October 2019, 14:23:12 UTC |
| ad56b59 | Jonathan Protzenko | 03 October 2019, 13:50:28 UTC | WIP; stuck because of a friend | 03 October 2019, 13:50:28 UTC |
| e2a1fc0 | Jonathan Protzenko | 03 October 2019, 13:17:44 UTC | Merge branch 'afromher_meta_chachapoly' into fstar-master | 03 October 2019, 13:17:44 UTC |
| d0f3e3c | Jonathan Protzenko | 03 October 2019, 13:11:44 UTC | Fix benchmarks | 03 October 2019, 13:11:44 UTC |
| 95018aa | Jonathan Protzenko | 03 October 2019, 12:31:01 UTC | Fix the tactic and other things to get separate versions for chachapoly, too | 03 October 2019, 12:31:01 UTC |
| 26ec65f | Jonathan Protzenko | 03 October 2019, 09:13:52 UTC | Don't swallow errors... replace try-catch with match | 03 October 2019, 09:13:52 UTC |
| 070fb21 | Dzomo the everest Yak | 03 October 2019, 08:27:20 UTC | [CI] regenerate hints | 03 October 2019, 08:27:20 UTC |
| 93f92ad | Aymeric Fromherz | 02 October 2019, 21:29:53 UTC | Try to inline chacha20 call in chachapoly | 02 October 2019, 21:29:53 UTC |
| cb8bf3e | Aymeric Fromherz | 02 October 2019, 21:04:48 UTC | Missing file | 02 October 2019, 21:04:48 UTC |
| 74b99f1 | Aymeric Fromherz | 02 October 2019, 21:04:13 UTC | Use tactic for chachapoly specialization | 02 October 2019, 21:04:13 UTC |
| 424003e | Aymeric Fromherz | 02 October 2019, 19:55:14 UTC | Propagate vectorized chachapoly to EverCrypt | 02 October 2019, 19:55:14 UTC |
| 882ffe7 | Aymeric Fromherz | 02 October 2019, 19:38:28 UTC | Add vectorized chachapoly from _dev | 02 October 2019, 19:38:28 UTC |
| ce6ef09 | Chris Hawblitzel | 02 October 2019, 15:57:35 UTC | Update AESopt.vaf to reflect changes to AESGCM.vaf | 02 October 2019, 15:57:35 UTC |
| 30efa99 | Chris Hawblitzel | 02 October 2019, 15:57:15 UTC | Merge branch 'ckh-fstar-master' into ckh_instr-reordering-aesgcm-rebased | 02 October 2019, 15:57:15 UTC |
| 00b3fb3 | Jonathan Protzenko | 02 October 2019, 15:43:46 UTC | Remove inline_for_extraction from Hacl.Impl.Chacha20.Vec Now that the tactic is rewriting the call-graph of Impl.Chacha20.Vec, the wrapper pattern is gone, meaning that inline_for_extraction (in the Impl file) applies for the entire call-graph. This is very expensive at extraction-time, and not necessary, since the tactic will automatically rewrite each function of Impl in the right style, and add the noextract inline_for_extraction qualifiers automatically. A corner-case is for leaves of the call-graph, which the tactic does not re-check: for those, the tactic statically asserts that they have been marked with inline_for_extraction already, and fails otherwise. This brings the extraction time of Hacl.Impl.Chacha20.Vec.fst to 42s (down from 8+ minutes without this fix). | 02 October 2019, 15:43:46 UTC |
| e6b8e70 | Marina Polubelova | 02 October 2019, 12:53:42 UTC | fix salsa20 bundle | 02 October 2019, 12:53:42 UTC |
| c28b119 | Marina Polubelova | 02 October 2019, 12:16:59 UTC | bump rlimit | 02 October 2019, 12:16:59 UTC |
| 7521e7e | Marina Polubelova | 02 October 2019, 09:35:09 UTC | remove duplicate files | 02 October 2019, 09:35:09 UTC |
| 98b7db2 | Dzomo the everest Yak | 02 October 2019, 08:27:34 UTC | [CI] regenerate hints | 02 October 2019, 08:27:34 UTC |
| f02c66f | Chris Hawblitzel | 01 October 2019, 00:03:03 UTC | Merge branch 'fstar-master' into ckh_instr-reordering-aesgcm-rebased | 01 October 2019, 00:03:03 UTC |
| 410184f | Chris Hawblitzel | 30 September 2019, 23:53:48 UTC | Update Vale version | 30 September 2019, 23:53:48 UTC |
| 8094914 | Jay Bosamiya | 01 July 2019, 18:34:29 UTC | Introduce [PossiblyMonad] module | 30 September 2019, 22:23:25 UTC |
| 7fdcd63 | Dzomo the everest Yak | 29 September 2019, 08:28:23 UTC | [CI] regenerate hints | 29 September 2019, 08:28:23 UTC |
| b91e08b | Jonathan Protzenko | 27 September 2019, 20:12:46 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 27 September 2019, 20:12:46 UTC |
| 16cdc59 | Jonathan Protzenko | 27 September 2019, 19:04:42 UTC | One optimization for the tactic (don't copy leaves of the call-graph). | 27 September 2019, 19:04:42 UTC |
| 6626cf1 | Jonathan Protzenko | 27 September 2019, 18:48:24 UTC | a note on agility and higher-order | 27 September 2019, 18:48:24 UTC |
| 73f2905 | Santiago Zanella-Beguelin | 27 September 2019, 15:19:40 UTC | Free hash state after freeing internal buffers | 27 September 2019, 15:19:40 UTC |
| dd5ae44 | Jonathan Protzenko | 27 September 2019, 12:54:10 UTC | Fixup C++ benchmark that was relying on a private variable (by copying its declaration). Don't have executable mode for source files in benchmarks | 27 September 2019, 12:54:10 UTC |
| 8483699 | Jonathan Protzenko | 27 September 2019, 03:54:49 UTC | rlimit | 27 September 2019, 03:54:49 UTC |
| 37b0690 | Jonathan Protzenko | 26 September 2019, 20:58:46 UTC | missing hints | 26 September 2019, 20:58:46 UTC |
| b6a8267 | Jonathan Protzenko | 26 September 2019, 20:58:13 UTC | Merge branch 'protz_meta_interfaces' of pro.github.com:mitls/hacl-star into protz_meta_interfaces | 26 September 2019, 20:58:13 UTC |
| 277b109 | Jonathan Protzenko | 26 September 2019, 20:11:50 UTC | hints | 26 September 2019, 20:11:50 UTC |
| 3ed4cd3 | Jonathan Protzenko | 26 September 2019, 19:36:11 UTC | Merge branch 'protz_meta_interfaces' of pro.github.com:mitls/hacl-star into protz_meta_interfaces | 26 September 2019, 19:36:11 UTC |
| 6f9a9c1 | Jonathan Protzenko | 26 September 2019, 19:36:01 UTC | Fix bundles | 26 September 2019, 19:36:01 UTC |
| 6cd2d47 | Jonathan Protzenko | 26 September 2019, 19:33:08 UTC | Fix Makefile | 26 September 2019, 19:33:08 UTC |
| 6ab7b03 | Jonathan Protzenko | 26 September 2019, 19:28:30 UTC | Merge branch 'protz_meta_interfaces' of pro.github.com:mitls/hacl-star into protz_meta_interfaces | 26 September 2019, 19:28:30 UTC |
| 9ec251b | Jonathan Protzenko | 26 September 2019, 19:28:15 UTC | The equal_stack_domains and equal_domains predicate seem to break unexplicably, often, and I don't understand why | 26 September 2019, 19:28:15 UTC |
| 297f5eb | Jonathan Protzenko | 26 September 2019, 19:05:57 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_meta_interfaces | 26 September 2019, 19:05:57 UTC |
| fd38f78 | Jonathan Protzenko | 26 September 2019, 18:59:29 UTC | Fix some inexplicably broken proofs | 26 September 2019, 18:59:29 UTC |
| 9f2e493 | Jonathan Protzenko | 26 September 2019, 17:31:17 UTC | Some TODOs | 26 September 2019, 17:32:53 UTC |
| 860ba16 | Jonathan Protzenko | 26 September 2019, 17:23:31 UTC | A working version of the auto-mk tactic | 26 September 2019, 17:23:31 UTC |
| 0b1611a | Jonathan Protzenko | 26 September 2019, 16:32:56 UTC | Even smaller repro | 26 September 2019, 16:32:56 UTC |
| 1304afe | Jonathan Protzenko | 26 September 2019, 15:28:46 UTC | Document the new bug | 26 September 2019, 15:28:46 UTC |
| 88c8ec0 | Jonathan Protzenko | 26 September 2019, 14:26:57 UTC | Isolated the bug | 26 September 2019, 14:26:57 UTC |
| 7b9dcb7 | Nikhil Swamy | 26 September 2019, 04:09:27 UTC | switch back to using F* master | 26 September 2019, 04:09:27 UTC |
| 07d74b1 | Jonathan Protzenko | 26 September 2019, 00:06:44 UTC | Attempt on chacha20... loops, or perhaps never terminates? | 26 September 2019, 00:06:47 UTC |
| 8bc2944 | Jonathan Protzenko | 25 September 2019, 23:38:17 UTC | Haha, works | 25 September 2019, 23:38:17 UTC |
| a1541fe | Jonathan Protzenko | 25 September 2019, 23:32:28 UTC | Work on a set of improvements. | 25 September 2019, 23:32:28 UTC |
| 5c3a44e | Aymeric Fromherz | 25 September 2019, 21:41:51 UTC | Hints | 25 September 2019, 21:41:54 UTC |
| 9d99876 | Aymeric Fromherz | 25 September 2019, 20:05:27 UTC | Fix Chacha.Equiv | 25 September 2019, 20:05:27 UTC |
| 05638d1 | Nikhil Swamy | 25 September 2019, 04:43:54 UTC | tweak config.json to pick the nik_1566 branch of F* since that contains the ulib/.cache directory used in the makefile now | 25 September 2019, 04:43:54 UTC |
| 4b998af | Nikhil Swamy | 25 September 2019, 04:31:57 UTC | patching valedepend.py to look for .checked files in the include path; adding ulib/.cache to its include path | 25 September 2019, 04:31:57 UTC |
| f869d29 | Nikhil Swamy | 25 September 2019, 03:40:13 UTC | a makefile tweak to deal with new check file locations | 25 September 2019, 03:40:13 UTC |
| bf9a1e0 | Jonathan Protzenko | 24 September 2019, 21:06:03 UTC | WIP tactic for higher-order rewriting; need to enable the specialization argument | 24 September 2019, 21:06:03 UTC |
| 3d209f8 | Jonathan Protzenko | 24 September 2019, 19:38:43 UTC | Add two admits and a beautiful hack to unblock more files | 24 September 2019, 19:38:43 UTC |
| cc3569b | Jonathan Protzenko | 24 September 2019, 19:14:18 UTC | Struggle to get a working build | 24 September 2019, 19:14:18 UTC |
| b9ebe81 | Jonathan Protzenko | 24 September 2019, 18:45:48 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_meta_interfaces | 24 September 2019, 18:45:48 UTC |
| 44d4dbe | Jonathan Protzenko | 24 September 2019, 18:43:28 UTC | WIP; import Chacha20/vec from _dev; fixup a couple things; use flags in the tactic | 24 September 2019, 18:43:28 UTC |
| ec36290 | Guido Martínez | 24 September 2019, 16:18:37 UTC | Hacl.Impl.Poly1305: bump some rlimits | 24 September 2019, 16:43:01 UTC |
| 1eb14e4 | Jonathan Protzenko | 23 September 2019, 20:17:10 UTC | Merge branch 'protz_meta_interfaces' of pro.github.com:mitls/hacl-star into protz_meta_interfaces | 23 September 2019, 20:17:10 UTC |
| 3aadeed | Jonathan Protzenko | 23 September 2019, 20:16:54 UTC | Merge branch 'fstar-master' into protz_meta_interfaces | 23 September 2019, 20:16:54 UTC |
| a11ffe3 | Jonathan Protzenko | 23 September 2019, 20:16:40 UTC | nit | 23 September 2019, 20:16:40 UTC |
| 7184501 | Jonathan Protzenko | 23 September 2019, 20:12:11 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_meta_interfaces | 23 September 2019, 20:12:11 UTC |
| 1fd1b76 | Dzomo the everest Yak | 22 September 2019, 08:26:25 UTC | [CI] regenerate hints | 22 September 2019, 08:26:25 UTC |
| 429ad03 | Dzomo the everest Yak | 21 September 2019, 08:26:39 UTC | [CI] regenerate hints | 21 September 2019, 08:26:39 UTC |
| 4211b64 | Aymeric Fromherz | 19 September 2019, 23:30:01 UTC | bump rlimit + Hints | 20 September 2019, 00:19:44 UTC |
| f43215b | Aymeric Fromherz | 19 September 2019, 20:19:45 UTC | Rename Spec.{Hash, HMAC, HKDF} to Spec.Agile.{..} | 19 September 2019, 20:19:45 UTC |
| c86ae22 | Aymeric Fromherz | 19 September 2019, 19:09:24 UTC | Use <= instead of < for hash specs | 19 September 2019, 19:09:24 UTC |
| a447e5c | Dzomo the everest Yak | 18 September 2019, 08:26:11 UTC | [CI] regenerate hints | 18 September 2019, 08:26:11 UTC |
| 8dd4105 | Dzomo the everest Yak | 17 September 2019, 08:26:11 UTC | [CI] regenerate hints | 17 September 2019, 08:26:11 UTC |
| d7b1997 | Guido Martínez | 16 September 2019, 19:33:56 UTC | bump an rlimit | 16 September 2019, 19:33:56 UTC |
