| 9139f06 | Bryan Parno | 29 July 2019, 15:49:23 UTC | Merge branch 'fstar-master' into _vale_opt_ghash | 29 July 2019, 15:49:23 UTC |
| 34381bc | Bryan Parno | 29 July 2019, 15:43:29 UTC | Hints | 29 July 2019, 15:43:29 UTC |
| a0c4b09 | Bryan Parno | 29 July 2019, 15:43:00 UTC | Update several places to use the right XMM register | 29 July 2019, 15:43:00 UTC |
| e3ec620 | Bryan Parno | 27 July 2019, 02:57:15 UTC | Make compute_iv_stdcall and gcm_blocks_stdcall public again | 29 July 2019, 13:56:34 UTC |
| 716f3e9 | Christoph M. Wintersteiger | 29 July 2019, 09:50:04 UTC | Fix cygwin build? | 29 July 2019, 09:50:04 UTC |
| 59fe9e7 | Aymeric Fromherz | 28 July 2019, 22:30:18 UTC | Fix interop for gcmdecrypt | 28 July 2019, 22:30:18 UTC |
| 2a7e9d4 | Aymeric Fromherz | 28 July 2019, 22:14:44 UTC | Fix interop for gcmencrypt | 28 July 2019, 22:14:44 UTC |
| 0b9c329 | Aymeric Fromherz | 28 July 2019, 21:38:55 UTC | Correct spec for gcm_iv wrapper | 28 July 2019, 21:38:55 UTC |
| 90cd3e0 | Aymeric Fromherz | 28 July 2019, 03:21:49 UTC | Fix GCM_IV interop | 28 July 2019, 03:21:49 UTC |
| 955a641 | Aymeric Fromherz | 28 July 2019, 02:28:07 UTC | Start fixing interop for GCM_IV | 28 July 2019, 02:28:07 UTC |
| bb66002 | Aymeric Fromherz | 27 July 2019, 21:33:44 UTC | Merge branch 'fstar-master' into afromher_opt_ghash | 27 July 2019, 21:33:44 UTC |
| 6e144d1 | Bryan Parno | 27 July 2019, 00:36:49 UTC | Reduce the number of required 6-blocks for decrypt from 3 to 1 | 27 July 2019, 00:36:49 UTC |
| 9cc8f4a | Bryan Parno | 26 July 2019, 23:23:46 UTC | Fix capitalization | 26 July 2019, 23:23:46 UTC |
| d9a00e1 | Christoph M. Wintersteiger | 26 July 2019, 14:35:44 UTC | More benchmarking | 26 July 2019, 14:35:44 UTC |
| 16b6dfe | Bryan Parno | 25 July 2019, 21:23:29 UTC | Assume false in a couple of places to temporarily work around framing issues | 25 July 2019, 21:23:29 UTC |
| aa027d8 | Bryan Parno | 25 July 2019, 21:20:34 UTC | Update decryption path to parallel encryption changes | 25 July 2019, 21:20:34 UTC |
| 01c0390 | Bryan Parno | 25 July 2019, 16:39:40 UTC | Bring back stdcall interface. Seems to be hitting the same issue as gcm_blocks_wrapped | 25 July 2019, 16:39:40 UTC |
| bb860db | Bryan Parno | 25 July 2019, 05:41:55 UTC | Gcm_blocks_wrapped should go through but is hung up on the framing | 25 July 2019, 05:41:55 UTC |
| bb9c724 | Bryan Parno | 25 July 2019, 04:32:18 UTC | Fix some bugs in the wrapper's signature | 25 July 2019, 04:32:18 UTC |
| 1820f9e | Bryan Parno | 25 July 2019, 04:09:44 UTC | Clean up | 25 July 2019, 04:09:44 UTC |
| c36f5a8 | Bryan Parno | 25 July 2019, 00:50:09 UTC | Gcm_blocks verifies | 25 July 2019, 04:08:00 UTC |
| 73e1412 | Bryan Parno | 24 July 2019, 23:34:10 UTC | Add a custom Gctr_register that better aligns with our register allocation and reversal status | 24 July 2019, 23:34:10 UTC |
| fb885dc | Bryan Parno | 24 July 2019, 23:05:12 UTC | Specialize Gcm_extra_bytes to use the same buffer for reading and writing | 24 July 2019, 23:05:12 UTC |
| 9595ea5 | Bryan Parno | 24 July 2019, 22:29:38 UTC | Gcm_extra_bytes goes through | 24 July 2019, 22:29:38 UTC |
| eb1c58b | Bryan Parno | 24 July 2019, 22:04:34 UTC | Gcm_blocks128 verifies | 24 July 2019, 22:06:46 UTC |
| 58ee90d | Bryan Parno | 24 July 2019, 21:34:24 UTC | Create a dedicated gctr procedure | 24 July 2019, 21:34:24 UTC |
| 84be295 | Bryan Parno | 24 July 2019, 20:47:11 UTC | Save some work in AESGCM and verify the first half of gcm_blocks | 24 July 2019, 20:47:11 UTC |
| f20b7c8 | Bryan Parno | 24 July 2019, 19:54:36 UTC | Fix up compute_iv_stdcall | 24 July 2019, 19:54:36 UTC |
| 15eff79 | Bryan Parno | 24 July 2019, 19:44:32 UTC | Compute_iv goes through | 24 July 2019, 19:44:32 UTC |
| 0185931 | Bryan Parno | 24 July 2019, 17:22:16 UTC | Remove an unnecessary precondition | 24 July 2019, 17:22:16 UTC |
| 65b5611 | Bryan Parno | 24 July 2019, 17:13:30 UTC | Prove that reversing 0 is still 0 | 24 July 2019, 17:13:30 UTC |
| ed313e5 | Bryan Parno | 23 July 2019, 20:44:26 UTC | Get gcm_blocks_auth verifying | 23 July 2019, 20:44:51 UTC |
| de51a78 | Bryan Parno | 23 July 2019, 19:45:35 UTC | Clean up | 23 July 2019, 19:45:35 UTC |
| 466774c | Bryan Parno | 23 July 2019, 19:43:40 UTC | Start aligning registers and invariants | 23 July 2019, 19:43:40 UTC |
| 0a91070 | Bryan Parno | 23 July 2019, 17:45:17 UTC | Update register usage to better align with GCMencrypt | 23 July 2019, 17:45:17 UTC |
| 7ab3841 | Bryan Parno | 23 July 2019, 15:54:54 UTC | Ghash_buffer verifies | 23 July 2019, 15:54:54 UTC |
| cd5d184 | Bryan Parno | 23 July 2019, 15:27:23 UTC | Loop finally goes through | 23 July 2019, 15:27:23 UTC |
| 832835f | Christoph M. Wintersteiger | 23 July 2019, 13:29:52 UTC | Benchmarks: Chacha/Poly tweaks. Disable EverCrypt Poly1305 to help appease cygwin. | 23 July 2019, 13:29:52 UTC |
| 3ae65c7 | Christoph M. Wintersteiger | 23 July 2019, 09:22:15 UTC | Attempt at fixing the Cygwin CI | 23 July 2019, 09:22:15 UTC |
| f2d70ca | Bryan Parno | 23 July 2019, 02:55:44 UTC | Some progress on the loop but error messages are now puzzling/misleading. | 23 July 2019, 02:55:44 UTC |
| 216c0b2 | Bryan Parno | 22 July 2019, 21:16:07 UTC | Propagate a ptr ensures | 22 July 2019, 21:16:07 UTC |
| a36de7b | Bryan Parno | 22 July 2019, 19:56:43 UTC | Get the loop body going through. Still need to work on inductiveness | 22 July 2019, 19:56:43 UTC |
| 07e3961 | Bryan Parno | 22 July 2019, 18:22:04 UTC | Version with exactly 6 passes | 22 July 2019, 18:22:04 UTC |
| 1c1994a | Bryan Parno | 22 July 2019, 18:20:12 UTC | Fix up pointer in call to GhashUnroll_n | 22 July 2019, 18:20:12 UTC |
| b3131eb | Bryan Parno | 22 July 2019, 18:07:47 UTC | Merge branch 'fstar-master' into _vale_opt_ghash | 22 July 2019, 18:07:47 UTC |
| 3ea2d03 | Christoph M. Wintersteiger | 22 July 2019, 17:07:03 UTC | Benchmarks: Added something akin to ChachaPoly via libjc | 22 July 2019, 17:07:39 UTC |
| 092ca4b | Christoph M. Wintersteiger | 22 July 2019, 15:08:53 UTC | Benchmarks: fix cygwin build | 22 July 2019, 17:07:39 UTC |
| 1c8fdd2 | Christoph M. Wintersteiger | 22 July 2019, 13:08:19 UTC | Clean up Chacha20 libjc stub | 22 July 2019, 17:07:38 UTC |
| 10c3b8d | Christoph M. Wintersteiger | 22 July 2019, 12:36:16 UTC | Reenable cipher and mac benchmarks | 22 July 2019, 17:07:37 UTC |
| 818c5a8 | Christoph M. Wintersteiger | 22 July 2019, 12:31:30 UTC | Fix kremlib path in benchmark build | 22 July 2019, 17:07:36 UTC |
| 465d2b5 | Christoph M. Wintersteiger | 22 July 2019, 12:09:54 UTC | Fixed OpenSSL ChaCha20 benchmark | 22 July 2019, 17:07:36 UTC |
| c78a178 | Chris Hawblitzel | 22 July 2019, 15:45:56 UTC | Add optimized n=6 case to GhashUnroll_n | 22 July 2019, 15:45:56 UTC |
| e7818e7 | Bryan Parno | 22 July 2019, 14:43:57 UTC | Ghash_buffer verifies (when we only have 1-5 blocks) | 22 July 2019, 14:43:57 UTC |
| ae85710 | Bryan Parno | 22 July 2019, 14:41:30 UTC | Merge branch 'fstar-master' into _vale_opt_ghash | 22 July 2019, 14:41:30 UTC |
| 3617ac1 | Bryan Parno | 22 July 2019, 14:37:55 UTC | Revert "Start attempting to un-reverse MulAdd" This reverts commit a1f864a54c0bc4c2f36d4f9e2ce040d11dc3a201. | 22 July 2019, 14:37:55 UTC |
| 5fe63b4 | Aseem Rastogi | 22 July 2019, 09:55:16 UTC | hints | 22 July 2019, 09:55:16 UTC |
| f8ca318 | Aseem Rastogi | 22 July 2019, 05:46:59 UTC | Merge branch 'fstar-master' into _aseem_effect_combinators_cleanup | 22 July 2019, 05:46:59 UTC |
| 878f03c | Aseem Rastogi | 22 July 2019, 05:46:30 UTC | hints | 22 July 2019, 05:46:30 UTC |
| e70927e | Aseem Rastogi | 22 July 2019, 05:46:19 UTC | tweak to a proof | 22 July 2019, 05:46:19 UTC |
| 802e4ab | Chris Hawblitzel | 21 July 2019, 19:40:31 UTC | Parameterize byte reversal and block reversal in GhashUnroll_n | 21 July 2019, 19:40:31 UTC |
| a1f864a | Bryan Parno | 21 July 2019, 01:23:39 UTC | Start attempting to un-reverse MulAdd | 21 July 2019, 01:23:39 UTC |
| 069f651 | Bryan Parno | 21 July 2019, 00:59:56 UTC | Call to GhashUnroll_n goes through, but everything is backwards, so postconditions don't line up | 21 July 2019, 00:59:56 UTC |
| b39f7ce | Bryan Parno | 21 July 2019, 00:33:12 UTC | Merge branch 'fstar-master' into _vale_opt_ghash | 21 July 2019, 00:33:12 UTC |
| 0cefef0 | Chris Hawblitzel | 20 July 2019, 01:27:09 UTC | Pass scratch_ptr in register to GhashUnroll_n | 20 July 2019, 01:27:09 UTC |
| b44f5cc | Chris Hawblitzel | 20 July 2019, 01:03:51 UTC | Make scratch_len parameter to GhashUnroll_n ghost | 20 July 2019, 01:03:51 UTC |
| 5a3cd62 | Bryan Parno | 20 July 2019, 00:39:08 UTC | Merge branch 'fstar-master' into _vale_opt_ghash | 20 July 2019, 00:39:08 UTC |
| 8c99684 | Bryan Parno | 19 July 2019, 20:21:50 UTC | Reminder for later | 19 July 2019, 20:21:50 UTC |
| 1ab5ad0 | Chris Hawblitzel | 19 July 2019, 19:37:28 UTC | Add scratch_len parameter to GhashUnroll_n | 19 July 2019, 19:37:28 UTC |
| 1d3f47e | Bryan Parno | 19 July 2019, 18:27:08 UTC | Add a register-only version of Ghash | 19 July 2019, 18:27:08 UTC |
| 24621d8 | Bryan Parno | 19 July 2019, 03:06:27 UTC | Start sketching in an optimized ghash. Satisfying scratch_b_data is a nuisance. | 19 July 2019, 03:06:27 UTC |
| 5f88d9f | Nikhil Swamy | 18 July 2019, 18:26:50 UTC | kick build | 18 July 2019, 18:26:50 UTC |
| 7e1100e | Nikhil Swamy | 18 July 2019, 15:31:16 UTC | Merge remote-tracking branch 'origin/fstar-master' into nik_1815 | 18 July 2019, 15:31:16 UTC |
| 85b0140 | Nikhil Swamy | 18 July 2019, 15:30:58 UTC | hints | 18 July 2019, 15:30:58 UTC |
| 397f9e7 | Tahina Ramananandro | 18 July 2019, 12:54:22 UTC | disable cipher, mac for now | 18 July 2019, 12:54:22 UTC |
| 147135e | Tahina Ramananandro | 18 July 2019, 12:48:00 UTC | Revert "Disable jc for now" This reverts commit 39379c5ed4c3c3c072feef5765461eaa6aeb0151. | 18 July 2019, 12:48:00 UTC |
| 39379c5 | Tahina Ramananandro | 18 July 2019, 04:36:01 UTC | Disable jc for now | 18 July 2019, 04:36:01 UTC |
| 88be1e4 | Tahina Ramananandro | 18 July 2019, 04:35:28 UTC | Revert "attempt fix" This reverts commit 74babd198d954f7c7a67231300e53722714bfe65. | 18 July 2019, 04:35:28 UTC |
| 2ea5ab3 | Nikhil Swamy | 18 July 2019, 01:45:46 UTC | Merge remote-tracking branch 'origin/fstar-master' into nik_1815 | 18 July 2019, 01:45:46 UTC |
| c7e0cbe | Nikhil Swamy | 18 July 2019, 01:45:07 UTC | hints | 18 July 2019, 01:45:07 UTC |
| 74babd1 | Tahina Ramananandro | 17 July 2019, 23:19:37 UTC | attempt fix | 17 July 2019, 23:19:37 UTC |
| 5a23913 | Tahina Ramananandro | 17 July 2019, 20:03:02 UTC | Fix OPENSSL_LIB, OPENSSL_INC similarly | 17 July 2019, 20:03:02 UTC |
| 5942202 | Tahina Ramananandro | 17 July 2019, 19:56:11 UTC | Merge branch 'fstar-master' of github.com:mitls/hacl-star into taramana_test_benchmark | 17 July 2019, 19:56:11 UTC |
| 34e9540 | Tahina Ramananandro | 17 July 2019, 19:14:58 UTC | fix KREMLIN_INC path, needed by Cygwin | 17 July 2019, 19:14:58 UTC |
| a240a01 | Christoph M. Wintersteiger | 17 July 2019, 16:48:06 UTC | Benchmarks: added ChaCha20 and Poly1305 and libjc | 17 July 2019, 16:51:24 UTC |
| 606bfad | Christoph M. Wintersteiger | 12 July 2019, 17:12:13 UTC | Added chacha20 and poly1305 benchmarks | 17 July 2019, 16:51:22 UTC |
| 505946b | Tahina Ramananandro | 16 July 2019, 19:53:32 UTC | Merge branch 'fstar-master' of github.com:mitls/hacl-star into taramana_test_benchmark | 16 July 2019, 19:53:32 UTC |
| 32de512 | Aseem Rastogi | 16 July 2019, 04:31:20 UTC | Merge branch 'fstar-master' into aseem_top_level_null_wp | 16 July 2019, 04:31:20 UTC |
| 80a4f25 | Jay Bosamiya | 15 July 2019, 22:18:48 UTC | Merge pull request #175 from project-everest/jay_tighterocamlextract Provide tighter arguments for extraction to OCaml | 15 July 2019, 22:18:48 UTC |
| 53c96b9 | Jay Bosamiya | 15 July 2019, 18:29:18 UTC | Provide tighter arguments for extraction to ocaml | 15 July 2019, 18:30:53 UTC |
| d8a7913 | Aseem Rastogi | 15 July 2019, 11:54:39 UTC | Merge branch 'fstar-master' into aseem_top_level_null_wp | 15 July 2019, 11:54:39 UTC |
| 92dc7f7 | Aseem Rastogi | 15 July 2019, 11:54:08 UTC | hints | 15 July 2019, 11:54:08 UTC |
| d3d8d8d | Aseem Rastogi | 15 July 2019, 11:53:58 UTC | tweak | 15 July 2019, 11:53:58 UTC |
| 449c167 | Chris Hawblitzel | 13 July 2019, 23:56:51 UTC | Add vale/code/lib/math/Vale.Math.Poly2.Galois.* to connect Spec.GaloisField to Vale.Math.Poly2* (adapted from _dev_ckh_aes branch commit 9477f4b442a8ee4fbf6d13cc9a7aeb7eaa153b0d) | 13 July 2019, 23:56:51 UTC |
| 3f58d45 | Chris Hawblitzel | 13 July 2019, 13:48:15 UTC | Use one fewer register in GhashUnroll_n | 13 July 2019, 13:48:15 UTC |
| 22af8cf | Chris Hawblitzel | 13 July 2019, 01:54:07 UTC | Add GhashUnroll_n | 13 July 2019, 01:54:07 UTC |
| 4c76d28 | Aseem Rastogi | 12 July 2019, 12:04:12 UTC | switch off the top-level trivial preconditions flag | 12 July 2019, 12:04:12 UTC |
| 04d26cf | Christoph M. Wintersteiger | 10 July 2019, 15:34:58 UTC | Fixed misleading parameter name | 10 July 2019, 15:34:58 UTC |
| cead021 | Jonathan Protzenko | 09 July 2019, 17:06:24 UTC | Merge branch 'protz_ctr' into fstar-master | 09 July 2019, 17:06:24 UTC |
| ad96443 | Jonathan Protzenko | 09 July 2019, 16:18:23 UTC | Some degree of testing of chacha20 via the CTR API | 09 July 2019, 16:18:23 UTC |
| 63d5592 | Jonathan Protzenko | 09 July 2019, 15:17:20 UTC | Fix regression | 09 July 2019, 15:17:20 UTC |
