| 8f87ee0 | Jonathan Protzenko | 01 April 2019, 20:56:43 UTC | Add some comments near admits | 01 April 2019, 20:56:43 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| fa3b78c | Aymeric Fromherz | 01 April 2019, 05:06:08 UTC | Integrate gcm256_encrypt into Evercrypt | 01 April 2019, 05:06:08 UTC |
| 1068d4a | Aymeric Fromherz | 01 April 2019, 04:39:20 UTC | Hints | 01 April 2019, 04:39:20 UTC |
| d7fe03c | Aymeric Fromherz | 01 April 2019, 04:18:28 UTC | Low* wrapper for optimized gcm256_encrypt | 01 April 2019, 04:30:36 UTC |
| 8fd123f | Aymeric Fromherz | 01 April 2019, 03:53:31 UTC | GCMencrypt with AES256 | 01 April 2019, 03:53:31 UTC |
| 16d761f | Aymeric Fromherz | 01 April 2019, 01:20:34 UTC | Hints | 01 April 2019, 01:20:34 UTC |
| 7dd89d2 | Aymeric Fromherz | 01 April 2019, 00:45:01 UTC | another missing disjointess precondition | 01 April 2019, 00:45:01 UTC |
| c8a509c | Aymeric Fromherz | 01 April 2019, 00:01:57 UTC | Missing disjointness precondition for AEAD | 01 April 2019, 00:01:57 UTC |
| 49cc140 | Aymeric Fromherz | 31 March 2019, 23:58:45 UTC | Merge branch '_vale_aes' into afromher_sn_integration | 31 March 2019, 23:58:45 UTC |
| 2cdd614 | Aymeric Fromherz | 31 March 2019, 23:22:11 UTC | Merge branch 'fstar-master' into afromher_sn_integration | 31 March 2019, 23:22:11 UTC |
| 9d5e7f7 | Jonathan Protzenko | 31 March 2019, 23:03:20 UTC | Had renamed the wrong wrappers | 31 March 2019, 23:03:20 UTC |
| 4d62590 | Aymeric Fromherz | 31 March 2019, 22:48:12 UTC | Finish integration of aesgcm key hashing | 31 March 2019, 22:48:12 UTC |
| 1926f89 | Chris Hawblitzel | 31 March 2019, 22:30:22 UTC | Add additional postcondition to lemma_call_poly1305 | 31 March 2019, 22:30:22 UTC |
| e17e656 | Jonathan Protzenko | 31 March 2019, 21:58:47 UTC | Ensure the generated .h files contain the original F* signatures as comments | 31 March 2019, 21:58:47 UTC |
| 7a68064 | Jonathan Protzenko | 31 March 2019, 21:33:09 UTC | More test vectors | 31 March 2019, 21:33:09 UTC |
| bba4dc7 | Jonathan Protzenko | 31 March 2019, 21:26:04 UTC | hints | 31 March 2019, 21:26:04 UTC |
| de428f7 | Jonathan Protzenko | 31 March 2019, 21:00:28 UTC | Also add Curve vector tests | 31 March 2019, 21:00:28 UTC |
| de5d5fd | Jonathan Protzenko | 31 March 2019, 20:48:41 UTC | Fix the json tool that dumps F* syntax for test vectors; hook up poly1305 tests to the main test driver in evercrypt | 31 March 2019, 20:48:41 UTC |
| da1b06c | Bryan Parno | 31 March 2019, 20:38:50 UTC | stdcall still fails in the larger context, even with manual framing and lots of rlimit | 31 March 2019, 20:38:50 UTC |
| ebf54f2 | Jonathan Protzenko | 31 March 2019, 19:44:55 UTC | Tighter precondition (hadn't saved my buffer) | 31 March 2019, 19:44:55 UTC |
| 3ef8bf8 | Jonathan Protzenko | 31 March 2019, 19:44:17 UTC | Bring in test vectors for AEAD and Curve while we're at it | 31 March 2019, 19:44:17 UTC |
| f82792a | Jonathan Protzenko | 31 March 2019, 19:37:14 UTC | A script to generate test vectors following the meta-programming slowdown | 31 March 2019, 19:37:14 UTC |
| cd936fd | Aymeric Fromherz | 31 March 2019, 19:30:00 UTC | Add pre-hashing of key for aesgcm (Vale code assumed) | 31 March 2019, 19:30:00 UTC |
| fe336f0 | Jonathan Protzenko | 31 March 2019, 18:00:16 UTC | Hints missing Makefile | 31 March 2019, 18:00:16 UTC |
| 38b3062 | Jonathan Protzenko | 31 March 2019, 17:49:28 UTC | A painful and inefficient copy of the whole input buffer. Modulo dances to have a buffer of the right size. Removes one assume. | 31 March 2019, 17:49:28 UTC |
| 2481aa1 | Aymeric Fromherz | 31 March 2019, 17:24:12 UTC | Disable verification of faulty proof | 31 March 2019, 17:24:12 UTC |
| 799d1ce | Aymeric Fromherz | 31 March 2019, 17:05:57 UTC | Update wrapper | 31 March 2019, 17:05:57 UTC |
| 63c2ee2 | Jonathan Protzenko | 31 March 2019, 17:02:16 UTC | Try renaming ASM symbols to unblock windows build | 31 March 2019, 17:02:16 UTC |
| 765db86 | Jonathan Protzenko | 31 March 2019, 16:22:50 UTC | Fix up one lemma on the Poly side. Lib.Unlib to be able to state the signature of EverCrypt.Poly1305. Attempted to use Chris' lemma -- still needs work to derive the proper post-condition | 31 March 2019, 16:22:50 UTC |
| f55a141 | Aymeric Fromherz | 31 March 2019, 15:02:34 UTC | Merge branch '_vale_aes' into afromher_sn_integration | 31 March 2019, 15:02:34 UTC |
| 0a9a311 | Dzomo the everest Yak | 31 March 2019, 08:19:32 UTC | [CI] regenerate hints | 31 March 2019, 08:19:32 UTC |
| 808d94d | Aymeric Fromherz | 31 March 2019, 07:41:45 UTC | Merge branch '_vale_aes' into afromher_sn_integration | 31 March 2019, 07:41:45 UTC |
| c71aebf | Bryan Parno | 31 March 2019, 05:29:32 UTC | Fix the precondition on hkeys_b and clean up other small issues in the file. Unfortunately, stdcall goes through in isolation but not as part of the entire file | 31 March 2019, 05:29:32 UTC |
| efc6b0e | Aymeric Fromherz | 31 March 2019, 04:17:22 UTC | Hints | 31 March 2019, 04:17:22 UTC |
| 68c7bef | Aymeric Fromherz | 31 March 2019, 04:15:02 UTC | Simplify precondition on hkeys for aesgcm | 31 March 2019, 04:15:02 UTC |
| 681c6db | Bryan Parno | 31 March 2019, 04:08:56 UTC | Stdcall goes through | 31 March 2019, 04:08:56 UTC |
| 106c43f | Bryan Parno | 31 March 2019, 04:02:02 UTC | Semantics go through without the framing | 31 March 2019, 04:02:02 UTC |
| 1ff398a | Bryan Parno | 31 March 2019, 03:57:46 UTC | Framing goes through. | 31 March 2019, 03:57:46 UTC |
| 14ff14d | Bryan Parno | 31 March 2019, 03:52:47 UTC | At the cost of much tediousness, factor out stack operations | 31 March 2019, 03:52:47 UTC |
| cefdeaf | Aymeric Fromherz | 31 March 2019, 03:41:45 UTC | Integrate aesgcm128 (with one assume about hashed keys) | 31 March 2019, 03:41:45 UTC |
| 9b9d343 | Aymeric Fromherz | 31 March 2019, 02:30:33 UTC | Simplify key expansion conditions for aesgcm | 31 March 2019, 02:30:33 UTC |
| 1158548 | Chris Hawblitzel | 30 March 2019, 22:21:54 UTC | Coerce arguments to bytes in poly1305 lemma calls | 30 March 2019, 22:21:54 UTC |
| 22a487a | Chris Hawblitzel | 30 March 2019, 21:34:10 UTC | Insert Vale poly1305 proofs into EverCrypt.Poly1305 | 30 March 2019, 21:34:10 UTC |
| 506bf20 | Bryan Parno | 30 March 2019, 21:23:06 UTC | Nice clean postconditions | 30 March 2019, 21:23:06 UTC |
| 99ddbeb | Bryan Parno | 30 March 2019, 21:12:16 UTC | Successfully call the uber lemma | 30 March 2019, 21:12:16 UTC |
| 68e3ea4 | Aymeric Fromherz | 30 March 2019, 20:32:15 UTC | Prove remaining lemma for gcm_encrypt wrapper | 30 March 2019, 20:32:15 UTC |
| b42834b | Jonathan Protzenko | 30 March 2019, 16:05:23 UTC | Backwards-compatible bundling to fix the windows build | 30 March 2019, 16:05:23 UTC |
| 4a3a128 | Dzomo the everest Yak | 30 March 2019, 08:21:19 UTC | [CI] regenerate hints | 30 March 2019, 08:21:19 UTC |
| 6fcc6f0 | Bryan Parno | 30 March 2019, 04:59:38 UTC | Clean up the postconditions | 30 March 2019, 04:59:38 UTC |
| 9178461 | Bryan Parno | 30 March 2019, 04:21:20 UTC | Top-level lemma goes through! | 30 March 2019, 04:21:20 UTC |
| b02b1fc | Bryan Parno | 30 March 2019, 02:42:52 UTC | Progress pushing results up to gcm_encrypt_LE. Still need to handle the extra bytes cases | 30 March 2019, 02:42:52 UTC |
| e53b98b | Aymeric Fromherz | 29 March 2019, 22:16:33 UTC | Finish gcm wrapper, with one lemma still admitted | 29 March 2019, 22:16:33 UTC |
| dd79743 | Bryan Parno | 29 March 2019, 19:39:22 UTC | Encrypt results go through as well | 29 March 2019, 19:39:22 UTC |
| 8848387 | Bryan Parno | 29 March 2019, 19:35:24 UTC | Hash result goes through | 29 March 2019, 19:35:24 UTC |
| ec9153d | Bryan Parno | 29 March 2019, 18:36:59 UTC | Possible fix? | 29 March 2019, 18:36:59 UTC |
| fd12664 | Jonathan Protzenko | 29 March 2019, 18:36:11 UTC | hints | 29 March 2019, 18:36:11 UTC |
| b73b166 | Jonathan Protzenko | 29 March 2019, 18:35:59 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 29 March 2019, 18:35:59 UTC |
| 479a79a | Bryan Parno | 29 March 2019, 18:35:43 UTC | Progress narrowing down the problem with final auth ensures | 29 March 2019, 18:35:43 UTC |
| 1a8f19f | Jonathan Protzenko | 29 March 2019, 18:00:03 UTC | Merge remote-tracking branch 'origin/afromher_sn_integration' into fstar-master | 29 March 2019, 18:00:03 UTC |
| 6262989 | Chris Hawblitzel | 29 March 2019, 17:33:52 UTC | Merge branch 'fstar-master' into _vale_poly1305 | 29 March 2019, 17:33:52 UTC |
| 37edd89 | Chris Hawblitzel | 29 March 2019, 17:32:06 UTC | Remove some admits from SHA_helpers | 29 March 2019, 17:32:06 UTC |
| 9cd15f2 | Aymeric Fromherz | 29 March 2019, 17:19:51 UTC | Fix impl for chachapoly | 29 March 2019, 17:19:51 UTC |
| a9b1f8f | Aymeric Fromherz | 29 March 2019, 17:07:44 UTC | Fix chachapoly spec | 29 March 2019, 17:07:44 UTC |
| b9cf6c8 | Bryan Parno | 29 March 2019, 17:02:18 UTC | Progress summarizing hashing | 29 March 2019, 17:02:18 UTC |
| 5f1bf4a | Bryan Parno | 29 March 2019, 15:56:54 UTC | Working towards hashing results. rlimit is already creeping up alarmingly | 29 March 2019, 15:56:54 UTC |
| 5d670b2 | Aymeric Fromherz | 29 March 2019, 15:40:17 UTC | Add spec test for chachapoly decrypt | 29 March 2019, 15:40:17 UTC |
| 56d2948 | Bryan Parno | 29 March 2019, 15:15:06 UTC | Encryption results go through with rlimit 55, but without the memory framing. | 29 March 2019, 15:21:05 UTC |
| a966abc | Bryan Parno | 29 March 2019, 15:12:50 UTC | Proving simple memory framing requires bumping rlimit from 24 to 60. Not impressed. | 29 March 2019, 15:12:50 UTC |
| 85249b3 | Jonathan Protzenko | 29 March 2019, 15:11:51 UTC | Fix calling convention mismatch | 29 March 2019, 15:11:51 UTC |
| 52b4a72 | Bryan Parno | 29 March 2019, 15:07:56 UTC | Factor out the computations over the auth data. Reduces rlimit from 82 to 24 | 29 March 2019, 15:07:56 UTC |
| c80e70b | Jonathan Protzenko | 29 March 2019, 14:55:47 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 29 March 2019, 14:55:47 UTC |
| c8c705f | Jonathan Protzenko | 29 March 2019, 14:55:42 UTC | Update EverCrypt external headers + a temporary interface for Chacha20Poly1305 in EverCrypt in preparation for multiplexing of this algorithm | 29 March 2019, 14:55:42 UTC |
| 46a26a7 | Bryan Parno | 29 March 2019, 14:29:22 UTC | Binary search for a minimal rlimit | 29 March 2019, 14:29:22 UTC |
| 273bed3 | Bryan Parno | 29 March 2019, 14:18:35 UTC | Adding postconditions leads to time outs and confusion | 29 March 2019, 14:18:35 UTC |
| eb1ea71 | Dzomo the everest Yak | 29 March 2019, 08:18:52 UTC | [CI] regenerate hints | 29 March 2019, 08:18:52 UTC |
| 69b5441 | Bryan Parno | 29 March 2019, 05:26:57 UTC | Handle extra plain/cipher bytes properly too. Sadly, the rlimit needed several bumps to get the body going through. Still need to work on postconditions. | 29 March 2019, 05:27:51 UTC |
| e67b123 | Aymeric Fromherz | 29 March 2019, 04:49:03 UTC | Getting closer to nice spec for gcm encrypt wrapper | 29 March 2019, 04:49:03 UTC |
| 49fa03a | Jonathan Protzenko | 29 March 2019, 04:09:03 UTC | another disclaimer | 29 March 2019, 04:09:03 UTC |
| 5df9230 | Jonathan Protzenko | 29 March 2019, 03:32:27 UTC | Further simplifications, fix tests | 29 March 2019, 03:32:27 UTC |
| 043b01a | Jonathan Protzenko | 29 March 2019, 03:26:19 UTC | Strengthen post-condition in hacl impl chachapoly. Make AEAD encryption / decryption take separate arguments for cipher & tag | 29 March 2019, 03:26:19 UTC |
| ad493bc | Jonathan Protzenko | 29 March 2019, 02:08:58 UTC | Implement AEAD decryption | 29 March 2019, 02:08:58 UTC |
| 9c0735f | Jonathan Protzenko | 29 March 2019, 01:42:18 UTC | Removal of obsolete code. This removes: - everything in code/old except for ed25519 and its dependencies (bignum, lib, curve25519, sha), along with ancient aesgcm in code/old/experimental - apps/ - obsolete specs in specs/old - secure_api ("record layer") development. | 29 March 2019, 01:42:18 UTC |
| c4296f1 | Jonathan Protzenko | 29 March 2019, 00:53:56 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_remove_old | 29 March 2019, 00:53:56 UTC |
| 422d17d | Chris Hawblitzel | 28 March 2019, 23:09:23 UTC | Update GHash code inside X64.AESGCM.vaf | 28 March 2019, 23:10:02 UTC |
| 270137e | Bryan Parno | 28 March 2019, 21:06:43 UTC | Clean up | 28 March 2019, 21:07:06 UTC |
| 5615e11 | Bryan Parno | 28 March 2019, 21:06:02 UTC | Prove a custom version of gctr_encrypt + hash for extra bytes | 28 March 2019, 21:06:51 UTC |
