| 4fe607b | Joonwon Choi | 10 April 2019, 01:47:28 UTC | Merkle tree: add hints | 10 April 2019, 01:47:28 UTC |
| b8d232f | Joonwon Choi | 09 April 2019, 23:28:19 UTC | Merge branch 'fstar-master' into joonwonc_merkle_tree_fix | 09 April 2019, 23:28:19 UTC |
| 0cd56b4 | Joonwon Choi | 09 April 2019, 23:27:01 UTC | Merge branch 'fstar-master' into joonwonc_merkle_tree_fix | 09 April 2019, 23:27:01 UTC |
| 2e97ee1 | Jonathan Protzenko | 09 April 2019, 20:14:01 UTC | Remove the generic distribution and do a temporary fix for poly1305 / compiler flags | 09 April 2019, 21:10:28 UTC |
| fc182c3 | Joonwon Choi | 09 April 2019, 20:29:38 UTC | Merge branch 'fstar-master' into joonwonc_merkle_tree_fix | 09 April 2019, 20:29:38 UTC |
| 91ef175 | Jonathan Protzenko | 09 April 2019, 19:48:20 UTC | A free function for AEAD | 09 April 2019, 19:48:20 UTC |
| d40922f | Joonwon Choi | 09 April 2019, 19:34:54 UTC | Merkle tree: trying to fix proofs again (by not using some smt patterns) | 09 April 2019, 19:34:54 UTC |
| beadac7 | Nikhil Swamy | 09 April 2019, 16:17:02 UTC | Merge remote-tracking branch 'origin/fstar-master' into nik_validity_axioms | 09 April 2019, 16:17:02 UTC |
| 3f979cc | Aseem Rastogi | 09 April 2019, 11:31:34 UTC | hints | 09 April 2019, 11:31:34 UTC |
| 74a8710 | Aseem Rastogi | 09 April 2019, 09:43:51 UTC | Merge branch 'fstar-master' into _aseem_heap_patterns | 09 April 2019, 09:43:51 UTC |
| c203525 | Aseem Rastogi | 09 April 2019, 09:31:07 UTC | Merge branch 'fstar-master' into _aseem_heap_patterns | 09 April 2019, 09:31:07 UTC |
| 184ce63 | Aseem Rastogi | 09 April 2019, 09:27:34 UTC | adding a local lemma to account for added patterns in heap | 09 April 2019, 09:27:34 UTC |
| 0dea41d | Aseem Rastogi | 09 April 2019, 09:27:10 UTC | using calc for an unstable proof | 09 April 2019, 09:27:10 UTC |
| b383b41 | Dzomo the everest Yak | 09 April 2019, 08:27:01 UTC | [CI] regenerate hints | 09 April 2019, 08:27:01 UTC |
| 2f522b7 | Nikhil Swamy | 09 April 2019, 01:03:16 UTC | fixing a proof after updating validity axioms (similar proofs failed before for other unrelated reasons) | 09 April 2019, 01:03:16 UTC |
| 0c01c78 | Nikhil Swamy | 09 April 2019, 00:26:00 UTC | revising FastMul_helpers.lemma_sqr to use calc | 09 April 2019, 00:26:00 UTC |
| d502136 | Joonwon Choi | 08 April 2019, 21:49:55 UTC | Merkle tree: increase rlimits for some proofs | 08 April 2019, 21:49:55 UTC |
| 9938907 | Joonwon Choi | 08 April 2019, 20:44:28 UTC | Merge branch 'fstar-master' into joonwonc_merkle_tree_fix | 08 April 2019, 20:44:28 UTC |
| 2a7a39e | Joonwon Choi | 08 April 2019, 20:40:21 UTC | Merkle tree: trying to fix a proof by providing more hints | 08 April 2019, 20:40:21 UTC |
| cefa9fa | Jonathan Protzenko | 08 April 2019, 12:10:46 UTC | Merge pull request #151 from jhwohlgemuth/patch-1 Simple grammar fix | 08 April 2019, 12:10:46 UTC |
| 7b35b6f | Jason Wohlgemuth | 08 April 2019, 10:10:48 UTC | Simple grammar fix Remove unnecessary "a" | 08 April 2019, 10:10:48 UTC |
| 3783f3f | Dzomo the everest Yak | 08 April 2019, 08:27:07 UTC | [CI] regenerate hints | 08 April 2019, 08:27:07 UTC |
| 23f27d0 | Dzomo the everest Yak | 07 April 2019, 08:25:58 UTC | [CI] regenerate hints | 07 April 2019, 08:25:58 UTC |
| 5df89c9 | Gustavo Varo | 06 April 2019, 20:08:01 UTC | Adding compression | 06 April 2019, 20:08:01 UTC |
| 69f8dd5 | Dzomo the everest Yak | 06 April 2019, 08:25:41 UTC | [CI] regenerate hints | 06 April 2019, 08:25:41 UTC |
| 5ed4eee | Jonathan Protzenko | 05 April 2019, 19:13:16 UTC | Merge remote-tracking branch 'refs/remotes/origin/fstar-master' into fstar-master | 05 April 2019, 19:13:16 UTC |
| 4e554a6 | Dzomo the everest Yak | 05 April 2019, 08:25:28 UTC | [CI] regenerate hints | 05 April 2019, 08:25:28 UTC |
| 9aea2f4 | Jonathan Protzenko | 04 April 2019, 23:56:00 UTC | fix test | 04 April 2019, 23:56:00 UTC |
| 74a4cf3 | Jonathan Protzenko | 04 April 2019, 23:41:47 UTC | fix build | 04 April 2019, 23:41:47 UTC |
| e934347 | Jonathan Protzenko | 04 April 2019, 23:16:19 UTC | New stateful API for decrypt, too... still need to write free, copy, etc. | 04 April 2019, 23:16:19 UTC |
| 26106f7 | Jonathan Protzenko | 04 April 2019, 21:51:08 UTC | missing pre | 04 April 2019, 21:51:08 UTC |
| 42e9be5 | Jonathan Protzenko | 04 April 2019, 21:43:52 UTC | New stateful API for AEAD, per discussions with Cédric, Antoine and others. Works for create_in and encrypt. | 04 April 2019, 21:43:52 UTC |
| df12eb9 | Jonathan Protzenko | 04 April 2019, 19:44:24 UTC | Remove code duplication in key expansion via meta-programming | 04 April 2019, 19:44:24 UTC |
| cb7f052 | Dzomo the everest Yak | 04 April 2019, 08:25:40 UTC | [CI] regenerate hints | 04 April 2019, 08:25:40 UTC |
| fc81123 | Nikhil Swamy | 04 April 2019, 04:14:34 UTC | tighten a modifies clause of Hash.create_in | 04 April 2019, 04:14:34 UTC |
| 130a617 | Santiago Zanella-Beguelin | 03 April 2019, 16:42:43 UTC | Port while combinator from _dev | 03 April 2019, 16:42:43 UTC |
| 4d57ffa | Bryan Parno | 03 April 2019, 14:39:32 UTC | Merge pull request #148 from dorisxx/fstar-master-typofix Update README.md to fix F* link | 03 April 2019, 14:39:32 UTC |
| 0e7a986 | dorisxx | 03 April 2019, 14:33:17 UTC | Update README.md | 03 April 2019, 14:33:17 UTC |
| d3b64c5 | Dzomo the everest Yak | 03 April 2019, 09:39:01 UTC | [CI] regenerate hints | 03 April 2019, 09:39:01 UTC |
| c0ccfa6 | Jonathan Protzenko | 02 April 2019, 19:46:18 UTC | A signature for SHA2-512 compatible with HACL-lib in preparation for Ed25519 | 02 April 2019, 19:46:18 UTC |
| 5296e9b | Jonathan Protzenko | 02 April 2019, 19:32:10 UTC | Drop Lib.Unlib in favor of Chris' Arch.BufferFriend | 02 April 2019, 19:32:10 UTC |
| 14d5b10 | Aymeric Fromherz | 02 April 2019, 19:22:15 UTC | Fix spacing in readme | 02 April 2019, 19:22:15 UTC |
| 74b341f | Aymeric Fromherz | 02 April 2019, 19:21:13 UTC | Update list of algorithms supported | 02 April 2019, 19:21:13 UTC |
| 325b727 | Jonathan Protzenko | 02 April 2019, 13:27:49 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 02 April 2019, 13:27:49 UTC |
| c3c2349 | Jonathan Protzenko | 02 April 2019, 13:27:39 UTC | tidbits | 02 April 2019, 13:27:39 UTC |
| 9bf461c | Christoph M. Wintersteiger | 01 April 2019, 18:16:46 UTC | Simplified Merkle tree serialization specs | 02 April 2019, 09:37:40 UTC |
| a4ce9f9 | Dzomo the everest Yak | 02 April 2019, 08:32:00 UTC | [CI] regenerate hints | 02 April 2019, 08:32:00 UTC |
| 3227cba | Jonathan Protzenko | 02 April 2019, 05:58:40 UTC | Unfortunate placement of spaces in the Makefile | 02 April 2019, 05:58:40 UTC |
| f386e89 | Jonathan Protzenko | 02 April 2019, 05:44:11 UTC | Trim distribution for the Everest config | 02 April 2019, 05:44:11 UTC |
| 653fa73 | Jonathan Protzenko | 02 April 2019, 05:39:34 UTC | Fix bundle | 02 April 2019, 05:39:34 UTC |
| ebe5737 | Jonathan Protzenko | 02 April 2019, 05:35:49 UTC | Fix bundle | 02 April 2019, 05:35:49 UTC |
| 9c1bef7 | Jonathan Protzenko | 02 April 2019, 04:46:11 UTC | Finish cleaning up tests | 02 April 2019, 04:46:11 UTC |
| 0282202 | Jonathan Protzenko | 02 April 2019, 04:29:12 UTC | Merge remote-tracking branch 'origin/afromher_sn_integration' into fstar-master | 02 April 2019, 04:29:12 UTC |
| 80fb341 | Jonathan Protzenko | 02 April 2019, 04:29:07 UTC | Rewire tests | 02 April 2019, 04:29:07 UTC |
| de42e37 | Aymeric Fromherz | 02 April 2019, 03:51:57 UTC | Remove assumes for integrated gcm_decrypt + Hints | 02 April 2019, 03:57:40 UTC |
| 46c7dd5 | Aymeric Fromherz | 02 April 2019, 02:22:18 UTC | Integrate gcm_decrypt with a few assumes left | 02 April 2019, 02:22:18 UTC |
| e11a58a | Aymeric Fromherz | 02 April 2019, 00:54:37 UTC | Hints | 02 April 2019, 00:54:37 UTC |
| 88f8768 | Aymeric Fromherz | 02 April 2019, 00:54:02 UTC | stdcall + Low* wrapper for gcm_decrypt | 02 April 2019, 00:54:02 UTC |
| 51f6aa0 | Aymeric Fromherz | 01 April 2019, 22:56:35 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 01 April 2019, 22:56:35 UTC |
| be7d97f | Aymeric Fromherz | 01 April 2019, 22:55:48 UTC | Hints + Fix extraction | 01 April 2019, 22:55:48 UTC |
| f83471a | Joonwon Choi | 01 April 2019, 22:34:08 UTC | Merkle tree: trying to fix a proof with larger rlimit | 01 April 2019, 22:34:08 UTC |
| ca81e81 | Aymeric Fromherz | 01 April 2019, 22:13:50 UTC | Remove gcmdecryptopt from extraction | 01 April 2019, 22:13:50 UTC |
| 01c3117 | Aymeric Fromherz | 01 April 2019, 22:11:01 UTC | Finish integration of gcm_encrypt | 01 April 2019, 22:11:01 UTC |
| ba29867 | Aymeric Fromherz | 01 April 2019, 20:56:57 UTC | Remove some assumes in EverCrypt.AEAD | 01 April 2019, 20:56:57 UTC |
| 8f87ee0 | Jonathan Protzenko | 01 April 2019, 20:56:43 UTC | Add some comments near admits | 01 April 2019, 20:56:43 UTC |
| 83610ad | Aymeric Fromherz | 01 April 2019, 20:45:53 UTC | Remove extra unneeded slots in aes hashed key | 01 April 2019, 20:45:53 UTC |
| d74e3a9 | Jonathan Protzenko | 01 April 2019, 20:45:22 UTC | README update | 01 April 2019, 20:45:22 UTC |
| 445495c | Jonathan Protzenko | 01 April 2019, 20:30:06 UTC | Remove warnings about FStar.Endianness | 01 April 2019, 20:30:06 UTC |
| 06b81c2 | Aymeric Fromherz | 01 April 2019, 20:00:58 UTC | Integrate gcmencrypt into EverCrypt with a few assumes left | 01 April 2019, 20:00:58 UTC |
| f9e0525 | Jonathan Protzenko | 01 April 2019, 19:53:18 UTC | Sketched a proof that can be done right now without any additional lemmas | 01 April 2019, 19:53:18 UTC |
| 9ab1d7e | Joonwon Choi | 01 April 2019, 19:11:06 UTC | Merge branch 'fstar-master' into joonwonc_merkle_tree_fix | 01 April 2019, 19:11:06 UTC |
| 2f0c789 | Aymeric Fromherz | 01 April 2019, 19:09:30 UTC | Update aes hashed keys wrapper | 01 April 2019, 19:09:30 UTC |
| 68f5e24 | Joonwon Choi | 01 April 2019, 19:08:33 UTC | Merge branch 'fstar-master' into joonwonc_merkle_tree_fix | 01 April 2019, 19:08:33 UTC |
| 92f44fe | Aymeric Fromherz | 01 April 2019, 18:17:13 UTC | Merge branch '_vale_aes' into afromher_sn_integration | 01 April 2019, 18:17:13 UTC |
| 24c0816 | Aymeric Fromherz | 01 April 2019, 18:15:46 UTC | Hints | 01 April 2019, 18:15:46 UTC |
| 8343751 | Aymeric Fromherz | 01 April 2019, 18:15:17 UTC | gcm encrypt low* wrappers with new hkeys requirements | 01 April 2019, 18:15:17 UTC |
| 3de8968 | Joonwon Choi | 01 April 2019, 18:00:11 UTC | Merkle tree: fix a lemma that took a few hours (now in two minutes). | 01 April 2019, 18:00:11 UTC |
| 45c6f0b | Jonathan Protzenko | 01 April 2019, 17:59:00 UTC | Merge remote-tracking branch 'origin/_vale_poly1305' into fstar-master | 01 April 2019, 17:59:00 UTC |
| a4ed4ae | Chris Hawblitzel | 01 April 2019, 17:55:11 UTC | Merge branch 'fstar-master' into _vale_poly1305 | 01 April 2019, 17:55:11 UTC |
| 80959a6 | Jonathan Protzenko | 01 April 2019, 17:13:35 UTC | Merge remote-tracking branch 'origin/_vale_poly1305' into fstar-master | 01 April 2019, 17:13:35 UTC |
| 5213e8f | Jonathan Protzenko | 01 April 2019, 16:56:09 UTC | tabs | 01 April 2019, 16:57:47 UTC |
| cf6ee73 | Bryan Parno | 01 April 2019, 16:54:25 UTC | Make Keyhash_init promise hkeys_reqs_pub | 01 April 2019, 16:54:25 UTC |
| 06a210d | Chris Hawblitzel | 01 April 2019, 16:32:29 UTC | Fix lemma calls to EverCrypt.Poly1305.fst, remove assume | 01 April 2019, 16:32:29 UTC |
| 107c394 | Aymeric Fromherz | 01 April 2019, 16:22:05 UTC | Simplify hkeys_reqs predicate | 01 April 2019, 16:22:05 UTC |
| c4076a7 | Bryan Parno | 01 April 2019, 15:49:51 UTC | Fix SConstruct to bring in more dependencies | 01 April 2019, 15:49:51 UTC |
| b6fab4f | Aymeric Fromherz | 01 April 2019, 15:46:21 UTC | Correct vale include | 01 April 2019, 15:46:21 UTC |
| 34f1de6 | Aymeric Fromherz | 01 April 2019, 15:33:30 UTC | Merge branch '_vale_aes' into afromher_sn_integration | 01 April 2019, 15:33:30 UTC |
| 5c9592c | Aymeric Fromherz | 01 April 2019, 15:32:51 UTC | Unsimplified wrapper for gcmdecrypt | 01 April 2019, 15:32:51 UTC |
| 2fd16cc | Bryan Parno | 01 April 2019, 15:28:33 UTC | Merge branch 'afromher_sn_integration' into _vale_aes | 01 April 2019, 15:28:33 UTC |
| 4fc9d48 | Bryan Parno | 01 April 2019, 15:15:22 UTC | Abstract out the requirements for hkeys_b, so we can hide them from the interop layer | 01 April 2019, 15:17:30 UTC |
| 8952b2e | Chris Hawblitzel | 01 April 2019, 15:12:47 UTC | Add more lemma calls to EverCrypt.Poly1305.fst | 01 April 2019, 15:12:47 UTC |
| 4d3ac69 | Chris Hawblitzel | 01 April 2019, 15:03:07 UTC | Merge branch 'fstar-master' into _vale_poly1305 | 01 April 2019, 15:03:07 UTC |
| cf5e723 | Chris Hawblitzel | 01 April 2019, 15:01:51 UTC | Add lemma_le_to_n_is_nat_from_bytes and lemma_n_to_le_is_nat_to_bytes | 01 April 2019, 15:01:51 UTC |
| 6684fc8 | Aymeric Fromherz | 01 April 2019, 14:43:58 UTC | Signature for gcmdecryptopt, implem assumed | 01 April 2019, 14:43:58 UTC |
| b9fadec | Aymeric Fromherz | 01 April 2019, 14:24:05 UTC | Merge branch '_vale_aes' into afromher_sn_integration | 01 April 2019, 14:24:05 UTC |
| d1028e9 | Aseem Rastogi | 01 April 2019, 09:22:14 UTC | Merge branch 'fstar-master' into _aseem_merkle_tree | 01 April 2019, 09:22:14 UTC |
| 127494c | Aseem Rastogi | 01 April 2019, 09:21:34 UTC | fixing assumes in MerkleTree.Serialization, many tweaks to the specs in that file | 01 April 2019, 09:21:34 UTC |
| c4c5b5a | Dzomo the everest Yak | 01 April 2019, 08:28:03 UTC | [CI] regenerate hints | 01 April 2019, 08:28:03 UTC |
| 86d0214 | Bryan Parno | 01 April 2019, 08:13:58 UTC | Propagate preconditions through GCMencryptOpt | 01 April 2019, 08:20:43 UTC |
| 3b5a528 | Bryan Parno | 01 April 2019, 08:02:15 UTC | Proof goes all the way through AESGCM's AES_GCM_encrypt_6mult | 01 April 2019, 08:13:50 UTC |
