| 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 |
| 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 |
| 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 |
| 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 |
| 220ec38 | Aymeric Fromherz | 13 March 2019, 22:49:09 UTC | First draft of new stack semantics | 13 March 2019, 22:49:09 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 991081c | Jonathan Protzenko | 11 March 2019, 23:18:14 UTC | Merge branch 'sn_evercrypt_integration' into fstar-master | 11 March 2019, 23:18:14 UTC |
| a116dd6 | Jonathan Protzenko | 11 March 2019, 21:15:17 UTC | haack | 11 March 2019, 21:15:17 UTC |
| a503de5 | Chris Hawblitzel | 11 March 2019, 15:03:04 UTC | In Vale, direct QuickCode support for while loops | 11 March 2019, 15:03:04 UTC |
| 7f94474 | Dzomo the everest Yak | 11 March 2019, 08:29:43 UTC | [CI] regenerate hints | 11 March 2019, 08:29:43 UTC |
| 33aacf8 | Aymeric Fromherz | 11 March 2019, 00:17:20 UTC | Hints | 11 March 2019, 00:17:20 UTC |
| 344d4a9 | Aymeric Fromherz | 11 March 2019, 00:17:07 UTC | Postcondition for gcmencrypt, not proven | 11 March 2019, 00:17:07 UTC |
| 13b4536 | Aymeric Fromherz | 10 March 2019, 23:33:47 UTC | Hints | 10 March 2019, 23:33:47 UTC |
| a1e937b | Aymeric Fromherz | 10 March 2019, 23:33:39 UTC | GCM encrypt wrapper without postcondition | 10 March 2019, 23:33:39 UTC |
| 5f27eea | Dzomo the everest Yak | 10 March 2019, 08:23:33 UTC | [CI] regenerate hints | 10 March 2019, 08:23:33 UTC |
| f3faae4 | Dzomo the everest Yak | 09 March 2019, 08:23:07 UTC | [CI] regenerate hints | 09 March 2019, 08:23:07 UTC |
| 6742d50 | Jonathan Protzenko | 08 March 2019, 22:51:26 UTC | Merge branch 'sn_evercrypt_integration' of pro.github.com:mitls/hacl-star into sn_evercrypt_integration | 08 March 2019, 22:51:26 UTC |
| 3bbd064 | Jonathan Protzenko | 08 March 2019, 22:28:26 UTC | Merge branch 'sn_evercrypt_integration' of pro.github.com:mitls/hacl-star into sn_evercrypt_integration | 08 March 2019, 22:28:26 UTC |
| 9536e96 | Jonathan Protzenko | 08 March 2019, 22:28:02 UTC | Abandon inline_for_extraction for now. (see FStarLang/kremlin#130) | 08 March 2019, 22:28:02 UTC |
| b71cf0c | Jonathan Protzenko | 08 March 2019, 22:17:35 UTC | Slight tweak to multiplexing | 08 March 2019, 22:17:35 UTC |
| c425222 | Jonathan Protzenko | 08 March 2019, 00:05:58 UTC | Leverage big hack in KreMLin to get properly guarded calls into Curve/64 | 08 March 2019, 22:15:35 UTC |
| aab7d38 | Aymeric Fromherz | 08 March 2019, 21:10:17 UTC | Hints | 08 March 2019, 21:10:17 UTC |
| 69988ae | Aymeric Fromherz | 08 March 2019, 19:42:02 UTC | Merge branch 'sn_evercrypt_integration' into afromher_sn_integration | 08 March 2019, 19:42:02 UTC |
| 07f204f | Jonathan Protzenko | 08 March 2019, 19:40:29 UTC | Changes for upstream F* changes; eliminates a void** while we're at it. Also fixup bundling for the COMPACT variant | 08 March 2019, 19:40:29 UTC |
| 5faebe9 | Jonathan Protzenko | 08 March 2019, 19:40:10 UTC | hints | 08 March 2019, 19:40:10 UTC |
| 40b4aaf | Jonathan Protzenko | 08 March 2019, 18:39:25 UTC | Merge remote-tracking branch 'origin/fstar-master' into sn_evercrypt_integration | 08 March 2019, 18:39:25 UTC |
| a91ad39 | Aymeric Fromherz | 08 March 2019, 18:14:58 UTC | Remove unfold slowing down verification from interop wrappers | 08 March 2019, 18:14:58 UTC |
| dd18c90 | Aymeric Fromherz | 08 March 2019, 17:32:07 UTC | Merge branch 'sn_evercrypt_integration' into afromher_sn_integration | 08 March 2019, 17:32:07 UTC |
| 9d8bca3 | Aymeric Fromherz | 08 March 2019, 17:27:57 UTC | Merge branch 'sn_evercrypt_integration' into _interop_stack | 08 March 2019, 17:27:57 UTC |
| 23d23d0 | Dzomo the everest Yak | 08 March 2019, 08:27:34 UTC | [CI] regenerate hints | 08 March 2019, 08:27:34 UTC |
| c21a280 | Jonathan Protzenko | 07 March 2019, 23:12:56 UTC | Fix tests? | 07 March 2019, 23:12:56 UTC |
| ae8838a | Jonathan Protzenko | 07 March 2019, 22:17:01 UTC | Disable -flto. Expose more CPU flags in AutoConfig2 | 07 March 2019, 22:17:01 UTC |
| 3f002e8 | Jonathan Protzenko | 07 March 2019, 21:31:03 UTC | ordering | 07 March 2019, 21:31:03 UTC |
| 4ab0fb7 | Jonathan Protzenko | 07 March 2019, 21:11:11 UTC | ordering | 07 March 2019, 21:11:11 UTC |
| 6c32c91 | Jonathan Protzenko | 07 March 2019, 20:03:59 UTC | An infrastructure for hand-written tests | 07 March 2019, 20:03:59 UTC |
| 42146ba | Nikhil Swamy | 07 March 2019, 06:09:07 UTC | Merge branch 'fstar-master' of github.com:mitls/hacl-star into fstar-master | 07 March 2019, 06:09:07 UTC |
| d8fc8d9 | Nikhil Swamy | 07 March 2019, 06:08:47 UTC | missing `inline_for_extraction` on a couple of key types in Lib.Buffer | 07 March 2019, 06:08:47 UTC |
| 3079f85 | Aymeric Fromherz | 07 March 2019, 04:43:48 UTC | Merge branch 'sn_evercrypt_integration' into afromher_sn_integration | 07 March 2019, 04:43:48 UTC |
| 887f132 | Aymeric Fromherz | 07 March 2019, 04:43:03 UTC | Minor tweak to verify file with make | 07 March 2019, 04:43:03 UTC |
| 93e7d78 | Aymeric Fromherz | 07 March 2019, 04:42:32 UTC | hints | 07 March 2019, 04:42:32 UTC |
| 2f13f9f | Aymeric Fromherz | 07 March 2019, 04:23:36 UTC | Complete ChaChaPoly, no admit left | 07 March 2019, 04:23:36 UTC |
| 8a21c81 | Aymeric Fromherz | 07 March 2019, 03:57:47 UTC | Prove Poly spec correspondance required for AEAD | 07 March 2019, 03:57:47 UTC |
| 9f5196d | Jonathan Protzenko | 07 March 2019, 03:43:47 UTC | Add test files in the tree (no build for now) | 07 March 2019, 03:43:47 UTC |
| 7e11540 | Jonathan Protzenko | 07 March 2019, 02:16:21 UTC | ci | 07 March 2019, 02:16:21 UTC |
| f38b2c7 | Chris Hawblitzel | 07 March 2019, 02:08:08 UTC | Small improvement to QuickCode normalization | 07 March 2019, 02:08:08 UTC |
| 4c108ee | Jonathan Protzenko | 07 March 2019, 01:09:24 UTC | Fix bundling error | 07 March 2019, 01:09:24 UTC |
| 8c7729e | Jonathan Protzenko | 07 March 2019, 00:53:29 UTC | hints | 07 March 2019, 00:53:29 UTC |
| a2d62ee | Aymeric Fromherz | 07 March 2019, 00:34:45 UTC | Finish ChachaPoly implementation | 07 March 2019, 00:34:45 UTC |
| d750f90 | Aymeric Fromherz | 06 March 2019, 23:56:08 UTC | Lowstarize AEAD | 06 March 2019, 23:56:08 UTC |
| 03da416 | Chris Hawblitzel | 06 March 2019, 23:29:26 UTC | Update Vale version | 06 March 2019, 23:29:26 UTC |
| 8781e60 | Chris Hawblitzel | 06 March 2019, 23:27:08 UTC | Upgrade vale directory to latest F* master | 06 March 2019, 23:27:08 UTC |
| 01a9b19 | Aymeric Fromherz | 06 March 2019, 23:14:05 UTC | hints | 06 March 2019, 23:14:05 UTC |
| fd670aa | Aymeric Fromherz | 06 March 2019, 23:13:57 UTC | Add chachaPoly to Makefile, kremlin failing | 06 March 2019, 23:13:57 UTC |
| 553291c | Aymeric Fromherz | 06 March 2019, 23:04:33 UTC | Strengthen poly spec, and remove an assume | 06 March 2019, 23:04:33 UTC |
| 6f39ab6 | Aymeric Fromherz | 06 March 2019, 21:07:34 UTC | ChachaPoly: Call Poly implementations | 06 March 2019, 21:07:34 UTC |
| 419f160 | Aymeric Fromherz | 06 March 2019, 16:57:31 UTC | Test Marina's fix for push_frame assume | 06 March 2019, 16:57:31 UTC |
| 23b7fc1 | Aymeric Fromherz | 06 March 2019, 15:26:51 UTC | Core of ChachaPoly with Actual calls to Hacl.Impl.Poly1305 assumed | 06 March 2019, 15:26:51 UTC |
| 87e70f5 | Dzomo the everest Yak | 06 March 2019, 08:26:12 UTC | [CI] regenerate hints | 06 March 2019, 08:26:12 UTC |
| 554d35a | Aymeric Fromherz | 06 March 2019, 06:01:59 UTC | Merge branch 'sn_evercrypt_integration' into afromher_sn_integration | 06 March 2019, 06:01:59 UTC |
| c0b705f | Aymeric Fromherz | 06 March 2019, 06:00:37 UTC | Implement key derivation | 06 March 2019, 06:00:37 UTC |
| 9ccb151 | Aymeric Fromherz | 06 March 2019, 04:34:24 UTC | ChachaPoly decrypt, Poly admitted | 06 March 2019, 04:34:24 UTC |
| 1e12e65 | Aymeric Fromherz | 06 March 2019, 02:31:23 UTC | ChachaPoly encrypt, Poly admitted | 06 March 2019, 02:31:23 UTC |
| fdf7f9f | Jonathan Protzenko | 06 March 2019, 01:06:01 UTC | fix Makefile | 06 March 2019, 01:06:01 UTC |
| 856c90a | Jonathan Protzenko | 06 March 2019, 00:58:59 UTC | Fix name collisions | 06 March 2019, 00:58:59 UTC |
