| 027cee4 | Aseem Rastogi | 22 March 2020, 07:14:03 UTC | kick in CI | 22 March 2020, 07:14:03 UTC |
| df0c85e | Aseem Rastogi | 21 March 2020, 16:20:31 UTC | kick in CI | 21 March 2020, 16:20:31 UTC |
| ac94cdf | Aseem Rastogi | 20 March 2020, 09:42:46 UTC | reverting F* branch | 20 March 2020, 09:42:46 UTC |
| 136d240 | Aseem Rastogi | 20 March 2020, 07:23:18 UTC | explaining a proof more | 20 March 2020, 07:23:18 UTC |
| 5c2c8b2 | Aseem Rastogi | 20 March 2020, 07:01:09 UTC | hint and tweaks to config.json | 20 March 2020, 07:01:09 UTC |
| 55ea532 | Aseem Rastogi | 20 March 2020, 05:11:52 UTC | using retry for a merkle tree proof | 20 March 2020, 05:11:52 UTC |
| a00b8da | Aseem Rastogi | 19 March 2020, 10:50:47 UTC | Merge branch 'master' into fstar-steel | 19 March 2020, 10:50:47 UTC |
| 89be444 | Aseem Rastogi | 19 March 2020, 10:50:16 UTC | tweaks | 19 March 2020, 10:50:16 UTC |
| 4cc3817 | Anna Weine | 18 March 2020, 18:33:02 UTC | Squaring for MM (#254) * sq at 0 * U: Sq P0 * unfold square * unfold sq * 0th squaring part * P256 to square, TODO: check for ecdsa * Squaring round 1 * Square 2nd round * Square 2nd round * Sq round 3 * Memory postcon for sq0 * Sq 0 * memory for sq1 * Square 1 * sq 2 mem * sq2 * sq 3 * QED * Sq a b -> sq a * God invented CI, so why should I check it by hand? * not used buffer * same as previous * decreased the timing for heavy functions * rlimit * Anya vs Function 0:1 * reproven the failing lemma * just in case reproved something looked unstable Co-authored-by: Santiago Zanella-Beguelin <s-zanella@users.noreply.github.com> | 18 March 2020, 18:33:02 UTC |
| 24aa5a4 | Aseem Rastogi | 18 March 2020, 16:25:13 UTC | F* branch | 18 March 2020, 16:25:13 UTC |
| 674f798 | Aseem Rastogi | 18 March 2020, 15:51:30 UTC | Merge branch 'master' into fstar-steel | 18 March 2020, 15:51:30 UTC |
| 97d4f4d | Santiago Zanella-Beguelin | 18 March 2020, 14:25:14 UTC | Merge pull request #253 from project-everest/karthik_blake2_fixspec Fixed Blake2 spec and implementation. | 18 March 2020, 14:25:14 UTC |
| 680c260 | karthikbhargavan | 18 March 2020, 11:24:24 UTC | restored salloc1 and lifted allocation of wv | 18 March 2020, 11:24:24 UTC |
| fd0bd7e | Santiago Zanella-Beguelin | 18 March 2020, 09:31:26 UTC | Merge branch 'master' into karthik_blake2_fixspec | 18 March 2020, 09:31:26 UTC |
| 906c6b6 | Santiago Zanella-Beguelin | 18 March 2020, 09:29:52 UTC | Merge pull request #257 from project-everest/guido_1905 Anticipate fixing FStarLang/FStar#1905 | 18 March 2020, 09:29:52 UTC |
| 00edb47 | Santiago Zanella-Beguelin | 18 March 2020, 09:29:39 UTC | Merge pull request #258 from project-everest/protz_ci fix build breakage in EverCrypt.Hash.Incremental | 18 March 2020, 09:29:39 UTC |
| dfdad40 | Jonathan Protzenko | 17 March 2020, 23:05:35 UTC | kick CI | 17 March 2020, 23:05:35 UTC |
| 626c316 | Guido MartÃnez | 17 March 2020, 21:58:29 UTC | Merge remote-tracking branch 'origin/protz_ci' | 17 March 2020, 21:58:29 UTC |
| 55d0641 | Jonathan Protzenko | 17 March 2020, 21:47:22 UTC | Attempt to make hints replayable to fix CI in HACL* | 17 March 2020, 21:47:22 UTC |
| 5cbf2f3 | Guido MartÃnez | 17 March 2020, 15:08:04 UTC | bump an rlimit | 17 March 2020, 15:08:04 UTC |
| 7ee24ba | Guido MartÃnez | 17 March 2020, 13:21:35 UTC | fixes in anticipation of FStarLang/FStar#1905 | 17 March 2020, 14:53:29 UTC |
| 39ffd4e | Jonathan Protzenko | 16 March 2020, 20:36:19 UTC | Work around FStarLang/FStar#1651 | 16 March 2020, 20:36:19 UTC |
| 48089eb | karthikbhargavan | 16 March 2020, 18:28:01 UTC | changed last_block to last_padded_block, fixed test file | 16 March 2020, 18:28:01 UTC |
| 6e7d1e1 | Aseem Rastogi | 16 March 2020, 03:58:27 UTC | Try steel branch of F* | 16 March 2020, 03:58:27 UTC |
| 9ffd876 | karthikbhargavan | 15 March 2020, 19:50:06 UTC | added c files | 15 March 2020, 19:50:06 UTC |
| 8e3a4d8 | karthikbhargavan | 15 March 2020, 18:35:01 UTC | fixed uint_to_t bug | 15 March 2020, 18:35:01 UTC |
| b2af2d3 | karthikbhargavan | 15 March 2020, 16:13:31 UTC | Merge branch 'master' into karthik_blake2_fixspec | 15 March 2020, 16:13:31 UTC |
| e491753 | karthikbhargavan | 15 March 2020, 16:04:28 UTC | cleaned up finish extracted code | 15 March 2020, 16:04:28 UTC |
| 9baeb30 | karthikbhargavan | 15 March 2020, 15:45:00 UTC | Fixed Blake2 Implementation to Conform to new Spec | 15 March 2020, 15:45:00 UTC |
| 49c3b6f | karthikbhargavan | 15 March 2020, 13:51:28 UTC | moved blake2 test to /tests | 15 March 2020, 13:51:28 UTC |
| e69ece6 | karthikbhargavan | 15 March 2020, 13:51:10 UTC | fixes to blake2 code | 15 March 2020, 13:51:10 UTC |
| d6ae711 | karthikbhargavan | 15 March 2020, 13:02:17 UTC | fixed blake2 spec | 15 March 2020, 13:02:17 UTC |
| 909eb49 | karthikbhargavan | 15 March 2020, 12:36:11 UTC | added more blake2 tests | 15 March 2020, 12:36:11 UTC |
| abbc506 | Santiago Zanella-Beguelin | 13 March 2020, 11:12:56 UTC | Merge pull request #252 from project-everest/afromher_ci Fix HACL code following issue #1940 on F* | 13 March 2020, 11:12:56 UTC |
| 62f15d9 | Aymeric Fromherz | 12 March 2020, 22:55:41 UTC | Fix the rest of Curve files | 12 March 2020, 22:55:41 UTC |
| 47d854c | Aymeric Fromherz | 12 March 2020, 22:36:45 UTC | Correct too agressive fix | 12 March 2020, 22:36:45 UTC |
| b3c1d7f | Aymeric Fromherz | 12 March 2020, 22:16:39 UTC | Fix Fields.Core | 12 March 2020, 22:16:39 UTC |
| a417365 | Dzomo the everest Yak | 12 March 2020, 08:22:12 UTC | [CI] regenerate hints and dist | 12 March 2020, 08:22:12 UTC |
| 94b22c3 | Benjamin Beurdouche | 11 March 2020, 16:12:03 UTC | Restore Spec.Agile.DH | 11 March 2020, 16:12:03 UTC |
| 9ddad1b | Benjamin Beurdouche | 11 March 2020, 16:11:28 UTC | Curve25519 - Restore decode_scalar in Spec.Curve25519 | 11 March 2020, 16:11:28 UTC |
| 851c929 | Dzomo the everest Yak | 11 March 2020, 08:22:35 UTC | [CI] regenerate hints and dist | 11 March 2020, 08:22:35 UTC |
| c246edd | Aymeric Fromherz | 10 March 2020, 22:23:26 UTC | Merge pull request #250 from project-everest/afromher_inline Use failwith in Vale assembly printer to avoid tricky corner cases leading to gcc bugs | 10 March 2020, 22:23:26 UTC |
| 80a01a4 | Aymeric Fromherz | 10 March 2020, 21:22:35 UTC | Fix vale inline tests | 10 March 2020, 21:22:35 UTC |
| 872f95a | Aymeric Fromherz | 10 March 2020, 19:56:48 UTC | Fix vale inline printer tests | 10 March 2020, 19:57:34 UTC |
| e18964a | Aymeric Fromherz | 10 March 2020, 19:47:27 UTC | Forbid Vale inline printer case that hits a gcc bug | 10 March 2020, 19:47:27 UTC |
| 11b3012 | Aymeric Fromherz | 10 March 2020, 19:29:25 UTC | Inline asm printer now fails when inputs and output variable register allocation clashes | 10 March 2020, 19:29:33 UTC |
| 065bf26 | Jonathan Protzenko | 10 March 2020, 17:14:16 UTC | Merge remote-tracking branch 'origin/master' into protz_pre | 10 March 2020, 17:14:16 UTC |
| 99ab6c8 | Jonathan Protzenko | 10 March 2020, 16:30:47 UTC | Fresh hints | 10 March 2020, 16:30:47 UTC |
| 2cfaa6f | Santiago Zanella-Beguelin | 10 March 2020, 16:17:05 UTC | Only override CC and CXX on Windows | 10 March 2020, 16:17:05 UTC |
| 4f6c111 | Jonathan Protzenko | 10 March 2020, 14:18:36 UTC | Merge branch 'master' into protz_pre | 10 March 2020, 14:18:36 UTC |
| afe04c9 | Santiago Zanella-Beguelin | 10 March 2020, 10:16:06 UTC | Remove unnecessary pre-conditions for P256 DH | 10 March 2020, 10:17:08 UTC |
| 1c387ed | Dzomo the everest Yak | 10 March 2020, 08:22:20 UTC | [CI] regenerate hints and dist | 10 March 2020, 08:22:20 UTC |
| 25e19b1 | Dzomo the everest Yak | 09 March 2020, 08:59:32 UTC | [CI] regenerate hints and dist | 09 March 2020, 08:59:32 UTC |
| 036d1c0 | Dzomo the everest Yak | 08 March 2020, 08:55:09 UTC | [CI] regenerate hints and dist | 08 March 2020, 08:55:09 UTC |
| c54ff40 | Dzomo the everest Yak | 07 March 2020, 08:24:06 UTC | [CI] regenerate hints and dist | 07 March 2020, 08:24:06 UTC |
| 86631d7 | Jonathan Protzenko | 06 March 2020, 21:15:40 UTC | Merge branch 'master' into protz_pre | 06 March 2020, 21:15:40 UTC |
| 159fad7 | Jonathan Protzenko | 06 March 2020, 15:45:50 UTC | Makefile bug was causing the dist directory to not be refreshed | 06 March 2020, 15:50:18 UTC |
| c86ff61 | Jonathan Protzenko | 06 March 2020, 15:50:07 UTC | Merge pull request #249 from project-everest/son_revert_blake2s revert blake2s 256 | 06 March 2020, 15:50:07 UTC |
| d032c2d | Anna Weine | 06 March 2020, 14:55:02 UTC | Merge branch 'master' into son_revert_blake2s | 06 March 2020, 14:55:02 UTC |
| 079854e | Benjamin Beurdouche | 06 March 2020, 10:43:27 UTC | Regenerate dist/ | 06 March 2020, 10:43:27 UTC |
| 908c341 | Benjamin Beurdouche | 06 March 2020, 10:02:49 UTC | Fix for clang-cl-9, restore Firefox build. | 06 March 2020, 10:04:25 UTC |
| 478b5d6 | Jonathan Protzenko | 05 March 2020, 17:26:43 UTC | Merge branch 'master' into son_revert_blake2s | 05 March 2020, 17:26:43 UTC |
| c8df466 | Tahina Ramananandro | 04 March 2020, 23:01:33 UTC | ci: disable ssh-agent | 04 March 2020, 23:01:33 UTC |
| 3d597fd | Santiago Zanella-Beguelin | 04 March 2020, 18:43:26 UTC | Stabilize proofs | 04 March 2020, 18:43:26 UTC |
| e0a88e2 | Son HO | 04 March 2020, 16:22:20 UTC | Merge branch 'master' into son_revert_blake2s | 04 March 2020, 16:22:20 UTC |
| d667a94 | Christoph M. Wintersteiger | 04 March 2020, 11:49:20 UTC | Merge branch 'cwinter_merkle_path_hash_sizes' | 04 March 2020, 11:49:20 UTC |
| 83bb482 | Christoph M. Wintersteiger | 03 March 2020, 18:01:46 UTC | Updated snapshots and hints | 04 March 2020, 10:19:22 UTC |
| 75c606e | Christoph M. Wintersteiger | 28 February 2020, 20:17:08 UTC | Merkle tree hash sizes and path interface cleanup | 04 March 2020, 10:19:19 UTC |
| b73deae | Jonathan Protzenko | 28 February 2020, 16:29:40 UTC | other fix | 04 March 2020, 10:19:19 UTC |
| 7daa2f7 | Benjamin Lipp (blipp) | 12 December 2019, 18:00:39 UTC | Improve error messages in Makefile concerning Vale | 04 March 2020, 10:19:19 UTC |
| b1f9c07 | Son HO | 04 March 2020, 08:38:11 UTC | Revert "Blake2s/256 for Son" This reverts commit a77b9ef72489df3eb1abd6c7bbb9aecfafb2593e. | 04 March 2020, 08:38:11 UTC |
| 81084d0 | Son HO | 04 March 2020, 08:37:57 UTC | Revert "rlimit" This reverts commit 6e91afbd9af00cfa15d45df54f655bf652726d1b. | 04 March 2020, 08:37:57 UTC |
| bfaf0ff | Son HO | 04 March 2020, 08:37:33 UTC | Revert "Indicate in dist/Makefile.tmpl that Hacl_Blake2s_256.o needs -mavx" This reverts commit fa442c96363bd35663717e7f453c7f2fc8b42f8e. | 04 March 2020, 08:37:33 UTC |
| 3cb6235 | Son HO | 04 March 2020, 08:37:18 UTC | Revert "Deactivate the use of blake2s_256 in Mozilla" This reverts commit b90019d66bcfccc42fca6892d6280c8ab5532754. | 04 March 2020, 08:37:18 UTC |
| 2e40c92 | Jonathan Protzenko | 02 March 2020, 22:42:35 UTC | Update other algorithms too This updated tactic seems to yield code that type-checks slower, possibly owing to type abbrevations being less shared between various variants of the function. | 02 March 2020, 22:42:35 UTC |
| 447128b | Jonathan Protzenko | 02 March 2020, 22:03:11 UTC | Adapt the code to the updated tactic. There are some unpleasant side-effects; for instance, type abbreviations normally wouldn't need to mention the extra precondition that gets inserted by the tactic; however, in the interest of sharing types between precondition-unaware, generic code and specialized instances of base combinators that *do* require a precondition, I added the parameter to a few types. Other than that, works fine. | 02 March 2020, 22:03:11 UTC |
| e480431 | Jonathan Protzenko | 02 March 2020, 21:18:14 UTC | Merge branch 'master' into protz_pre | 02 March 2020, 21:18:14 UTC |
| b2a282c | Jonathan Protzenko | 02 March 2020, 21:18:10 UTC | Revert "Make the Curve25519 call-graph indexed over a predicate" This reverts commit 19added6d2465f4bd2be462bff25d62b22aad132. | 02 March 2020, 21:18:10 UTC |
| 6d73fab | Jonathan Protzenko | 02 March 2020, 21:15:29 UTC | Rewrite higher-order tactic to insert preconditions. This follows Santiago's suggestion in https://github.com/project-everest/hacl-star/pull/243 Essentially, the tactic, upon encountering a node in the call-graph, unfolds its type (because most declarations are of the form `let f: #i:index -> f_t i`), then pushes a precondition `p` in its requires clause, which then gets threaded all throughout the call-graph. This generates code that type-checks slower than before, owing to the need to unfold and refold types; furthermore, situations where a type could be left as-is because no extra parameters were needed now gets rewritten systematically. | 02 March 2020, 21:17:56 UTC |
| fd80a4f | Jonathan Protzenko | 02 March 2020, 16:05:22 UTC | Merge pull request #246 from project-everest/blipp_makefile_vale Improve error messages in Makefile concerning Vale | 02 March 2020, 16:05:22 UTC |
| 16044af | Benjamin Lipp | 02 March 2020, 13:57:21 UTC | Merge branch 'master' into blipp_makefile_vale | 02 March 2020, 13:57:21 UTC |
| 846fda8 | Jonathan Protzenko | 28 February 2020, 16:29:40 UTC | other fix | 28 February 2020, 16:29:40 UTC |
| 8c4118b | Jonathan Protzenko | 28 February 2020, 15:56:34 UTC | ci | 28 February 2020, 15:56:34 UTC |
| 5e1d7fb | Jonathan Protzenko | 28 February 2020, 06:54:19 UTC | Revert "see if this helps" This reverts commit fae3b1685c14f8a65b2779dfffdcdfbf2122542e. | 28 February 2020, 06:54:19 UTC |
| fae3b16 | Jonathan Protzenko | 28 February 2020, 03:27:36 UTC | see if this helps | 28 February 2020, 03:27:36 UTC |
| cd12ca9 | Jonathan Protzenko | 28 February 2020, 03:26:44 UTC | need 7 | 28 February 2020, 03:26:44 UTC |
| 6ccf41d | Jonathan Protzenko | 28 February 2020, 03:25:26 UTC | Revert "disable lto for the sake of unbreaking the build" This reverts commit fb3a23cd52bf5f7edc1deaa67725ed3b1682790e. | 28 February 2020, 03:25:26 UTC |
| fb3a23c | Jonathan Protzenko | 27 February 2020, 21:08:18 UTC | disable lto for the sake of unbreaking the build | 27 February 2020, 21:08:18 UTC |
| d90750a | Jonathan Protzenko | 27 February 2020, 20:28:22 UTC | typo | 27 February 2020, 20:28:22 UTC |
| 9cd894b | Jonathan Protzenko | 27 February 2020, 20:27:20 UTC | Try with a newer gcc on ci only | 27 February 2020, 20:27:20 UTC |
| 4d3e155 | Christoph M. Wintersteiger | 27 February 2020, 19:45:54 UTC | Fix dependency of MerkleTree.fsti on EverCrypt | 27 February 2020, 19:45:54 UTC |
| 4e4db3f | Christoph M. Wintersteiger | 27 February 2020, 19:30:45 UTC | Fix Merkle tree tests | 27 February 2020, 19:30:45 UTC |
| bc7fec9 | Jonathan Protzenko | 27 February 2020, 02:31:12 UTC | fix header | 27 February 2020, 02:31:12 UTC |
| 0c72130 | Jonathan Protzenko | 27 February 2020, 01:50:15 UTC | Fix prefix | 27 February 2020, 01:50:15 UTC |
| 5146847 | Jonathan Protzenko | 27 February 2020, 01:30:49 UTC | Merge remote-tracking branch 'origin/protz_ci' | 27 February 2020, 01:30:49 UTC |
| 6963ab1 | Jonathan Protzenko | 27 February 2020, 01:27:34 UTC | fix benchmarks | 27 February 2020, 01:27:34 UTC |
| afa5d9c | Jonathan Protzenko | 27 February 2020, 01:26:41 UTC | Merge remote-tracking branch 'origin/son_blake2s_256' | 27 February 2020, 01:26:41 UTC |
| 7014fba | Jonathan Protzenko | 26 February 2020, 22:37:35 UTC | Merge remote-tracking branch 'origin/son_blake2s_256' | 26 February 2020, 22:37:35 UTC |
| 7fbaf41 | Jonathan Protzenko | 26 February 2020, 21:40:23 UTC | Merge branch 'cwinter_merkle_hashes' | 26 February 2020, 21:40:23 UTC |
| 849d861 | Jonathan Protzenko | 26 February 2020, 21:34:53 UTC | missing file | 26 February 2020, 21:34:53 UTC |
