Skip to main content

Browse the archive

https://github.com/project-everest/hacl-star
01 October 2021, 10:10:28 UTC
sort by:
Revision Author Date Message Commit Date
493d130 Aymeric Fromherz 24 March 2020, 14:39:08 UTC Merge branch 'master' into afromher_hpke 24 March 2020, 14:39:08 UTC
24d3821 Aymeric Fromherz 24 March 2020, 14:38:40 UTC Remove incorrect (but unused) order for Spec.Agile.DH 24 March 2020, 14:38:40 UTC
26c43ab Dzomo the everest Yak 24 March 2020, 08:28:21 UTC [CI] regenerate hints and dist 24 March 2020, 08:28:21 UTC
40a5343 Jonathan Protzenko 23 March 2020, 22:18:05 UTC Merge pull request #263 from project-everest/protz_ci Fix executable mode 23 March 2020, 22:18:05 UTC
3dc9422 Jonathan Protzenko 23 March 2020, 17:45:03 UTC Merge branch 'master' into protz_ci 23 March 2020, 17:45:03 UTC
ce514ab Guido Martínez 23 March 2020, 17:25:15 UTC Merge pull request #259 from project-everest/guido_math tidy up lemma_mult_{le,lt}_right calls 23 March 2020, 17:25:15 UTC
1a239d2 Aymeric Fromherz 23 March 2020, 16:52:32 UTC Merge branch 'master' into afromher_hpke 23 March 2020, 16:52:32 UTC
d3b16b4 Aymeric Fromherz 23 March 2020, 16:51:08 UTC Clean Makefile 23 March 2020, 16:51:08 UTC
0f273d1 Jonathan Protzenko 23 March 2020, 16:41:10 UTC Sigh, more executable files 23 March 2020, 16:41:10 UTC
7dc7007 Guido Martínez 23 March 2020, 16:20:29 UTC Merge branch 'master' into guido_math 23 March 2020, 16:20:29 UTC
fce7e1c Jonathan Protzenko 23 March 2020, 15:13:19 UTC Fix executable mode 23 March 2020, 15:13:19 UTC
a728ccf Aseem Rastogi 22 March 2020, 13:06:38 UTC Merge pull request #260 from project-everest/fstar-steel Some proof tweaks before merging F* steel branch to master 22 March 2020, 13:06:38 UTC
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
4d1fb49 Aymeric Fromherz 21 March 2020, 00:12:44 UTC Parametrize over Curve vale precondition, following @protz advice 21 March 2020, 00:12:44 UTC
2838467 Aymeric Fromherz 20 March 2020, 22:45:19 UTC Parametrize over predicate for curve assembly features 20 March 2020, 22:45:19 UTC
528371b Aymeric Fromherz 20 March 2020, 21:48:43 UTC Rename Generic files into HPKE.Interface 20 March 2020, 21:48:43 UTC
f2dab0f Aymeric Fromherz 20 March 2020, 20:04:34 UTC Fix HPKE instantiations 20 March 2020, 20:04:34 UTC
9687d60 Aymeric Fromherz 20 March 2020, 17:57:44 UTC Move HPKE impl to Stack effect 20 March 2020, 17:57:59 UTC
5348dab Aymeric Fromherz 20 March 2020, 16:50:25 UTC Merge branch 'master' into afromher_hpke 20 March 2020, 16:50:25 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
07b887d Guido Martínez 18 March 2020, 20:17:48 UTC Merge branch 'master' into guido_math 18 March 2020, 20:17:48 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
732ec66 Santiago Zanella-Beguelin 18 March 2020, 14:29:03 UTC Merge branch 'master' into guido_math 18 March 2020, 14:29:03 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
d555faa Guido Martínez 18 March 2020, 11:41:05 UTC Merge branch 'master' into guido_math 18 March 2020, 11:41:05 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
17177ef Guido Martínez 18 March 2020, 01:07:42 UTC tidy up lemma_mult_{le,lt}_right calls There is a mistake in FStar.Math.Lemmas where lemma_mult_lt_right is actually a subcase of lemma_mult_le_right (since it ensures `b * a <= c * a` instead of `b * a < c * a`). This will be fixed soon, so call lemma_mult_le_right instead. One file, vale/code/arch/x64/interop/Vale.AsLowStar.MemoryHelpers.fst, even defines and uses the correct version. I'm keeping that one for now so we can commit these changes before fixing F*, but once that's done this should just call the F* lemma. 18 March 2020, 01:32:17 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
c203e2b Aymeric Fromherz 12 March 2020, 21:27:27 UTC More rlimits 12 March 2020, 21:27:27 UTC
fef598a Aymeric Fromherz 12 March 2020, 20:44:20 UTC Bump rlimit 12 March 2020, 20:44:20 UTC
c43fd08 Aymeric Fromherz 12 March 2020, 19:58:10 UTC Fix HPKE with new spec 12 March 2020, 19:58:10 UTC
930e8f9 Aymeric Fromherz 12 March 2020, 19:10:04 UTC Modify HPKE spec to support representation for P-256 12 March 2020, 19:10:04 UTC
5505016 Aymeric Fromherz 12 March 2020, 17:13:35 UTC Disable HPKE test failing because of assumed vals in Vale specs 12 March 2020, 17:13:35 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
c9d6633 Aymeric Fromherz 11 March 2020, 18:35:43 UTC Add decryption test 11 March 2020, 18:35:43 UTC
de26d72 Aymeric Fromherz 11 March 2020, 18:27:34 UTC HPKE: Add encryption test 11 March 2020, 18:27:34 UTC
cbdb975 Aymeric Fromherz 11 March 2020, 16:57:39 UTC Add first encryption test data 11 March 2020, 16:57:39 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
c08f1fd Aymeric Fromherz 10 March 2020, 17:53:02 UTC Remove now unneeded condition on DH_P256 key from HPKE 10 March 2020, 17:53:02 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
557f82b Aymeric Fromherz 10 March 2020, 15:15:19 UTC Merge branch 'master' into afromher_hpke 10 March 2020, 15:15:19 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
a302e4f Aymeric Fromherz 09 March 2020, 21:20:13 UTC Bump rlimit 09 March 2020, 21:20:13 UTC
cf42cfc Aymeric Fromherz 09 March 2020, 21:16:09 UTC HPKE test: Add setupBaseR 09 March 2020, 21:16:09 UTC
1f5eb60 Aymeric Fromherz 09 March 2020, 21:03:38 UTC Update HPKE code to match new spec 09 March 2020, 21:03:38 UTC
806ccad Aymeric Fromherz 09 March 2020, 20:16:47 UTC Add empty interface for HPKE test to friend spec 09 March 2020, 20:16:47 UTC
63bd294 Aymeric Fromherz 09 March 2020, 20:09:53 UTC HPKE spec: Fix build_context to match RFC 09 March 2020, 20:09:53 UTC
24fa28f Aymeric Fromherz 09 March 2020, 19:57:25 UTC HPKE spec: Modify id_of_cs to match RFC 09 March 2020, 19:57:25 UTC
d8c225b Aymeric Fromherz 09 March 2020, 18:47:09 UTC Update test vectors for HPKE 09 March 2020, 18:47:09 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
back to top