| 871c398 | Nikhil Swamy | 20 March 2019, 22:27:16 UTC | trying out a dependence analysis change in F* | 20 March 2019, 22:27:16 UTC |
| d1a2056 | Jonathan Protzenko | 20 March 2019, 19:24:10 UTC | and more hints | 20 March 2019, 19:24:10 UTC |
| 472bb6c | Jonathan Protzenko | 20 March 2019, 19:09:48 UTC | more hints | 20 March 2019, 19:09:48 UTC |
| d965639 | Jonathan Protzenko | 20 March 2019, 19:08:47 UTC | hints | 20 March 2019, 19:08:47 UTC |
| 99229c0 | Jonathan Protzenko | 20 March 2019, 18:23:44 UTC | Remove frameOf restrictions on MUT and IMMUT; rely on new lemma instead. Only one usage: not worth a pattern (for now) | 20 March 2019, 18:23:44 UTC |
| c5827e5 | Jonathan Protzenko | 20 March 2019, 13:23:38 UTC | NOVALE variable for HACL-only verification targets | 20 March 2019, 13:23:38 UTC |
| 9002f32 | Aseem Rastogi | 20 March 2019, 12:15:23 UTC | Merge branch 'fstar-master' of github.com:mitls/hacl-star into fstar-master | 20 March 2019, 12:15:23 UTC |
| 8b2dfae | Aseem Rastogi | 20 March 2019, 12:15:07 UTC | hint | 20 March 2019, 12:15:07 UTC |
| 7dcb3f3 | Aseem Rastogi | 20 March 2019, 12:15:00 UTC | setting a lower rlimit for a proof, reduces the overall verification time of Incremental.Hash by about a third | 20 March 2019, 12:15:00 UTC |
| fa44e2d | Dzomo the everest Yak | 20 March 2019, 10:26:27 UTC | [CI] regenerate hints | 20 March 2019, 10:26:27 UTC |
| 07660e0 | Dzomo the everest Yak | 19 March 2019, 08:25:10 UTC | [CI] regenerate hints | 19 March 2019, 08:25:10 UTC |
| 6abc740 | Jonathan Protzenko | 18 March 2019, 20:20:28 UTC | try again | 18 March 2019, 20:20:28 UTC |
| 19a389c | Jonathan Protzenko | 18 March 2019, 19:51:52 UTC | try again | 18 March 2019, 19:51:52 UTC |
| 7e8473f | Jonathan Protzenko | 18 March 2019, 19:28:09 UTC | try again | 18 March 2019, 19:28:09 UTC |
| a07479c | Jonathan Protzenko | 18 March 2019, 19:06:57 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 18 March 2019, 19:06:57 UTC |
| 43be176 | Jonathan Protzenko | 18 March 2019, 19:03:52 UTC | More testing infrastructure | 18 March 2019, 19:03:52 UTC |
| 2957f79 | Dzomo the everest Yak | 18 March 2019, 10:23:32 UTC | [CI] regenerate hints | 18 March 2019, 10:23:32 UTC |
| ba56d2a | Dzomo the everest Yak | 17 March 2019, 08:24:24 UTC | [CI] regenerate hints | 17 March 2019, 08:24:24 UTC |
| acc9d24 | Dzomo the everest Yak | 16 March 2019, 08:25:42 UTC | [CI] regenerate hints | 16 March 2019, 08:25:42 UTC |
| 0fc1756 | Aymeric Fromherz | 15 March 2019, 23:32:52 UTC | Hints | 15 March 2019, 23:32:52 UTC |
| fe719b3 | Aymeric Fromherz | 15 March 2019, 23:22:01 UTC | Bump rlimit + reset to fstar-master version of taint analysis | 15 March 2019, 23:22:01 UTC |
| 837b884 | Aymeric Fromherz | 15 March 2019, 22:30:03 UTC | Add new instructions to taint semantics | 15 March 2019, 22:30:03 UTC |
| 8375c51 | Aymeric Fromherz | 15 March 2019, 19:55:06 UTC | Merge branch 'fstar-master' into afromher_stack_aes | 15 March 2019, 19:55:06 UTC |
| 40b430a | Aymeric Fromherz | 15 March 2019, 18:44:58 UTC | Add new aes to Makefile + verifying state | 15 March 2019, 18:44:58 UTC |
| 2b7220a | Aymeric Fromherz | 15 March 2019, 17:18:46 UTC | Merge branch '_vale_aes' into _vale_stack_aes | 15 March 2019, 17:18:46 UTC |
| e472057 | Aymeric Fromherz | 15 March 2019, 17:16:50 UTC | Simplify SConstruct options | 15 March 2019, 17:16:50 UTC |
| 81ccd29 | Bryan Parno | 15 March 2019, 15:57:15 UTC | Starting to string together encryption results | 15 March 2019, 15:57:15 UTC |
| 68b6717 | Aymeric Fromherz | 15 March 2019, 15:41:11 UTC | Remove Vale makefile debug hack | 15 March 2019, 15:41:11 UTC |
| 72adb0a | Bryan Parno | 15 March 2019, 15:30:32 UTC | Clean up | 15 March 2019, 15:30:32 UTC |
| 2b387cb | Bryan Parno | 15 March 2019, 15:29:38 UTC | Prove we did encrypt the hash correctly | 15 March 2019, 15:29:38 UTC |
| 0e13607 | Bryan Parno | 15 March 2019, 14:57:40 UTC | Take advantage of 128-bit memory operands to remove the need for specialized _buffer procedures | 15 March 2019, 14:58:00 UTC |
| 5f6ae20 | Bryan Parno | 15 March 2019, 14:51:13 UTC | Work on proving that we encrypted the hash value | 15 March 2019, 14:51:13 UTC |
| ea273b9 | Dzomo the everest Yak | 15 March 2019, 08:35:34 UTC | [CI] regenerate hints | 15 March 2019, 08:35:34 UTC |
| 2517799 | Aymeric Fromherz | 15 March 2019, 08:33:49 UTC | Remove Wno-error option from dist Makefile | 15 March 2019, 08:33:49 UTC |
| dee580a | Aymeric Fromherz | 15 March 2019, 08:31:49 UTC | Hints | 15 March 2019, 08:31:49 UTC |
| 072f603 | Aymeric Fromherz | 15 March 2019, 06:19:15 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 15 March 2019, 07:03:27 UTC |
| 6bbc15b | Aymeric Fromherz | 15 March 2019, 06:11:50 UTC | Hints | 15 March 2019, 06:11:50 UTC |
| 3b282bc | Aymeric Fromherz | 15 March 2019, 06:11:17 UTC | Merge branch 'afromher_sn_integration' into _vale_stack_model | 15 March 2019, 06:11:17 UTC |
| a234556 | Aymeric Fromherz | 15 March 2019, 06:09:58 UTC | Finish proving untrusted interop wrapper | 15 March 2019, 06:09:58 UTC |
| 9666605 | Aymeric Fromherz | 15 March 2019, 04:34:39 UTC | Prove Vale view of stack | 15 March 2019, 04:34:39 UTC |
| 3bd3d7a | Aymeric Fromherz | 15 March 2019, 04:04:09 UTC | Hints | 15 March 2019, 04:04:09 UTC |
| 21d3d7a | Aymeric Fromherz | 15 March 2019, 04:00:49 UTC | Update all interop wrappers with new stack model | 15 March 2019, 04:00:49 UTC |
| d4fa1d6 | Bryan Parno | 15 March 2019, 00:56:05 UTC | Stitch together all of the ghashes | 15 March 2019, 00:56:05 UTC |
| 3e2cf1b | Aymeric Fromherz | 15 March 2019, 00:07:04 UTC | Verify all Vale files with new stack model | 15 March 2019, 00:07:04 UTC |
| 96c05ca | Aymeric Fromherz | 14 March 2019, 23:56:39 UTC | Modify trusted interop semantics for new stack model | 14 March 2019, 23:56:39 UTC |
| bf91ca0 | Aymeric Fromherz | 14 March 2019, 22:34:03 UTC | Disable taint analysis | 14 March 2019, 22:34:03 UTC |
| 04ae493 | Aymeric Fromherz | 14 March 2019, 22:12:50 UTC | Separate file for Vale stack instructions + use stack instructions in all Vale files (not verifying yet) | 14 March 2019, 22:12:50 UTC |
| 49dd6c3 | Aymeric Fromherz | 14 March 2019, 21:54:11 UTC | Specify Vale view of stack + Start removing occurences of stack_b + Remove unused Vale stdcalls | 14 March 2019, 21:54:24 UTC |
| 4ac138e | Aymeric Fromherz | 14 March 2019, 20:13:24 UTC | Modify trusted semantics with Bryan's comments | 14 March 2019, 20:13:24 UTC |
| ccf8c5a | Aymeric Fromherz | 14 March 2019, 18:17:35 UTC | Dummy: test CI | 14 March 2019, 18:17:35 UTC |
| 1bf1686 | Bryan Parno | 14 March 2019, 17:57:31 UTC | Prove we can call all of the necessary operations | 14 March 2019, 17:57:31 UTC |
| 654b622 | Aymeric Fromherz | 14 March 2019, 09:36:19 UTC | Hints | 14 March 2019, 09:36:19 UTC |
| 8ee1f33 | Aymeric Fromherz | 14 March 2019, 09:36:08 UTC | Specify + Prove X64.Vale.InsMem | 14 March 2019, 09:36:08 UTC |
| 0051439 | Aymeric Fromherz | 14 March 2019, 09:35:31 UTC | Semantics: Hoist functions + minor corrections | 14 March 2019, 09:35:31 UTC |
| 22bfaa2 | Aymeric Fromherz | 14 March 2019, 06:12:24 UTC | Makefile: temporary workaround for errors in Vale files | 14 March 2019, 06:12:24 UTC |
| 2cadc32 | Aymeric Fromherz | 14 March 2019, 06:11:22 UTC | InsBasic reverifying new stack model | 14 March 2019, 06:11:22 UTC |
| d3dbea8 | Aymeric Fromherz | 14 March 2019, 06:10:33 UTC | Updates to trusted printer and taint semantics for new stack model | 14 March 2019, 06:10:33 UTC |
| 4d41d4e | Chris Hawblitzel | 14 March 2019, 05:53:02 UTC | Disable X64.Leakage_Ins* to enable merge | 14 March 2019, 05:53:02 UTC |
| 5bfb770 | Chris Hawblitzel | 14 March 2019, 04:40:29 UTC | Comment out file before merging | 14 March 2019, 04:40:29 UTC |
| 6d6d9c1 | Chris Hawblitzel | 14 March 2019, 04:11:51 UTC | Comment out file before merging | 14 March 2019, 04:11:51 UTC |
| 0904b0c | Chris Hawblitzel | 14 March 2019, 03:31:34 UTC | Merge branch '_vale_aes' of https://github.com/project-everest/hacl-star into _vale_aes | 14 March 2019, 03:31:34 UTC |
| 80a5bd1 | Chris Hawblitzel | 14 March 2019, 03:28:46 UTC | Post-merge fixes | 14 March 2019, 03:28:46 UTC |
| 093b6a4 | Aymeric Fromherz | 14 March 2019, 03:13:16 UTC | Second draft of semantics with new stack model | 14 March 2019, 03:13:16 UTC |
| 392b324 | Bryan Parno | 14 March 2019, 02:05:57 UTC | Slowly stitching subroutines together. | 14 March 2019, 02:05:57 UTC |
| a698c94 | Chris Hawblitzel | 14 March 2019, 00:02:02 UTC | Merge branch 'fstar-master' into _vale_aes | 14 March 2019, 00:02:02 UTC |
| 220ec38 | Aymeric Fromherz | 13 March 2019, 22:49:09 UTC | First draft of new stack semantics | 13 March 2019, 22:49:09 UTC |
| 45f7d5f | Bryan Parno | 13 March 2019, 21:54:35 UTC | Fix ups so that we can provably call AES_GCM_encrypt_6mult | 13 March 2019, 21:54:35 UTC |
| 13a2bf6 | Bryan Parno | 13 March 2019, 21:33:09 UTC | Bug with Vale public? | 13 March 2019, 21:33:09 UTC |
| d0a90dd | Jonathan Protzenko | 13 March 2019, 21:00:15 UTC | Use the newest lemmas to remove two assumes | 13 March 2019, 21:00:15 UTC |
| f392791 | Aymeric Fromherz | 13 March 2019, 20:02:18 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 13 March 2019, 20:02:18 UTC |
| eeaab83 | Aymeric Fromherz | 13 March 2019, 20:01:20 UTC | Hints | 13 March 2019, 20:01:20 UTC |
| e7ddf63 | Aymeric Fromherz | 13 March 2019, 20:00:37 UTC | Prove admits in X64.BufferViewStore | 13 March 2019, 20:00:37 UTC |
| aa3515e | Bryan Parno | 13 March 2019, 17:59:56 UTC | Revert changes to the test | 13 March 2019, 17:59:56 UTC |
| c6d6edd | Dzomo the everest Yak | 13 March 2019, 08:36:06 UTC | [CI] regenerate hints | 13 March 2019, 08:36:06 UTC |
| 569302c | Aymeric Fromherz | 13 March 2019, 08:20:16 UTC | Cleanup old files | 13 March 2019, 08:20:16 UTC |
| c2e2780 | Aymeric Fromherz | 13 March 2019, 06:13:48 UTC | Thread has_bmi2/adx throughout Curve call graph | 13 March 2019, 06:13:48 UTC |
| 1db3375 | Aymeric Fromherz | 13 March 2019, 05:11:13 UTC | Missing files | 13 March 2019, 05:11:13 UTC |
| aa5cbfc | Aymeric Fromherz | 13 March 2019, 04:55:50 UTC | Complete missing proofs in Hacl.Curve.Field64.Core | 13 March 2019, 04:55:50 UTC |
| 6930e8e | Bryan Parno | 13 March 2019, 04:41:44 UTC | Remove byte-level operations | 13 March 2019, 04:41:44 UTC |
| fbc178b | Bryan Parno | 12 March 2019, 21:42:02 UTC | Small clean up | 12 March 2019, 21:42:02 UTC |
| db92f23 | Bryan Parno | 12 March 2019, 21:39:31 UTC | Add a lemma to handle the empty sequence case | 12 March 2019, 21:39:31 UTC |
| 9499f97 | Aymeric Fromherz | 12 March 2019, 18:25:12 UTC | Hints | 12 March 2019, 18:25:12 UTC |
| bfd8e14 | Aymeric Fromherz | 12 March 2019, 18:25:07 UTC | Bump z3rlimit for GCMencrypt | 12 March 2019, 18:25:07 UTC |
| 7cbcf27 | Bryan Parno | 12 March 2019, 18:03:29 UTC | Simplify and verify handling of bytes | 12 March 2019, 18:03:29 UTC |
| c0e1e79 | Aymeric Fromherz | 12 March 2019, 17:36:56 UTC | Modify Vale inline printer to remove gcc warnings + Remove Makefile hacks | 12 March 2019, 17:59:14 UTC |
| 6996d77 | Bryan Parno | 12 March 2019, 16:27:37 UTC | Use a smaller rlimit | 12 March 2019, 17:01:24 UTC |
| d68fcee | Aymeric Fromherz | 12 March 2019, 16:59:39 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 12 March 2019, 16:59:39 UTC |
| a29440a | Jonathan Protzenko | 12 March 2019, 16:29:13 UTC | specific targets for: chacha20, poly1305, curve25519 | 12 March 2019, 16:29:13 UTC |
| 69e1649 | Aymeric Fromherz | 12 March 2019, 16:05:55 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 12 March 2019, 16:05:55 UTC |
| afb07d0 | Aymeric Fromherz | 12 March 2019, 16:05:10 UTC | Hints | 12 March 2019, 16:05:10 UTC |
| 7ac1082 | Aymeric Fromherz | 12 March 2019, 16:04:28 UTC | Proved relation of be/le_bytes_to_quad32 | 12 March 2019, 16:04:28 UTC |
| 1672111 | Aymeric Fromherz | 12 March 2019, 14:02:25 UTC | Hints | 12 March 2019, 14:02:25 UTC |
| 3f4d64c | Aymeric Fromherz | 12 March 2019, 14:02:07 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 12 March 2019, 14:02:07 UTC |
| 03e9523 | Chris Hawblitzel | 12 March 2019, 13:47:15 UTC | Add Mem128 operand constructor | 12 March 2019, 13:47:15 UTC |
| e7035ba | Dzomo the everest Yak | 12 March 2019, 08:35:41 UTC | [CI] regenerate hints | 12 March 2019, 08:35:41 UTC |
| ebb203a | Aymeric Fromherz | 12 March 2019, 08:03:09 UTC | gcm256_encrypt wrapper | 12 March 2019, 08:03:09 UTC |
| 0d8c867 | Aymeric Fromherz | 12 March 2019, 07:52:52 UTC | Finish proof for gcm128_encrypt wrappe | 12 March 2019, 07:52:52 UTC |
| 17f07d7 | Bryan Parno | 12 March 2019, 06:08:39 UTC | While loop now goes through properly | 12 March 2019, 06:08:39 UTC |
| 3914ec2 | Chris Hawblitzel | 11 March 2019, 15:03:04 UTC | In Vale, direct QuickCode support for while loops | 12 March 2019, 05:45:19 UTC |
| ac56b96 | Bryan Parno | 12 March 2019, 05:29:58 UTC | Fill in two TODO items with somewhat inefficient alternatives | 12 March 2019, 05:29:58 UTC |
