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
8a5e266 Aseem Rastogi 03 December 2018, 11:22:18 UTC hints for two files that succeed locally but fail on CI 03 December 2018, 11:22:18 UTC
f4649f6 Aseem Rastogi 03 December 2018, 09:24:47 UTC tweaking a 3000 rlimit proof to prune its context 03 December 2018, 09:24:47 UTC
8c88bff Nikhil Swamy 01 December 2018, 05:46:07 UTC revert needless changes 01 December 2018, 05:46:07 UTC
6e9175e Nikhil Swamy 01 December 2018, 05:43:48 UTC fixing a regression in Interop.fst; bumping an rlimit in fastmul 01 December 2018, 05:43:48 UTC
2220ab8 Nikhil Swamy 30 November 2018, 23:20:22 UTC adding a couple of calls to monotonicity in the proof of wp_sound 30 November 2018, 23:20:22 UTC
39a7b31 Nikhil Swamy 30 November 2018, 18:20:14 UTC temporary admit to go further in Everest CI 30 November 2018, 18:20:14 UTC
33ea052 Dzomo the everest Yak 30 November 2018, 08:40:37 UTC [CI] regenerate hints 30 November 2018, 08:40:37 UTC
c419e5c Nikhil Swamy 29 November 2018, 23:08:55 UTC bumping rlimit on a proof that could use a bit of work 29 November 2018, 23:08:55 UTC
291320e Guido Martínez 29 November 2018, 17:10:23 UTC Revert latest commits until I can make the proof go through 29 November 2018, 17:10:57 UTC
1b9aa19 Dzomo the everest Yak 29 November 2018, 08:52:56 UTC Merge commit '09459668c32ac0472cb7aaf591ec6974fee8f465' into fstar-master 29 November 2018, 08:52:56 UTC
0945966 Dzomo the everest Yak 29 November 2018, 08:52:55 UTC [CI] regenerate hints 29 November 2018, 08:52:55 UTC
c712029 Guido Martínez 28 November 2018, 13:08:39 UTC hints 29 November 2018, 08:18:18 UTC
e1ac7ec Guido Martínez 28 November 2018, 16:00:56 UTC bump rlimit 29 November 2018, 08:18:18 UTC
790e594 Guido Martínez 28 November 2018, 16:00:31 UTC vale: Types_s: make `le_seq_quad32_to_bytes_def` ensure the length of its result 29 November 2018, 08:18:18 UTC
45a1786 Guido Martínez 28 November 2018, 14:37:36 UTC FastMul_helpers: lemma_sub3 now requires a proof 29 November 2018, 08:18:18 UTC
cbe6f23 Dzomo the everest Yak 28 November 2018, 08:42:29 UTC [CI] regenerate hints 28 November 2018, 08:42:29 UTC
c4faa52 Christoph M. Wintersteiger 27 November 2018, 14:57:03 UTC EverCrypt module reference fix. 27 November 2018, 14:57:03 UTC
17688f7 Christoph M. Wintersteiger 27 November 2018, 14:49:40 UTC Added 'everest' config to EverCrypt. 27 November 2018, 14:49:40 UTC
c949588 Dzomo the everest Yak 27 November 2018, 08:48:08 UTC [CI] regenerate hints 27 November 2018, 08:48:08 UTC
67d3d87 Dzomo the everest Yak 26 November 2018, 08:49:38 UTC [CI] regenerate hints 26 November 2018, 08:49:38 UTC
9952498 Dzomo the everest Yak 25 November 2018, 08:34:44 UTC [CI] regenerate hints 25 November 2018, 08:34:44 UTC
0580c10 Dzomo the everest Yak 24 November 2018, 08:35:39 UTC [CI] regenerate hints 24 November 2018, 08:35:39 UTC
e6ad098 Dzomo the everest Yak 23 November 2018, 08:34:53 UTC [CI] regenerate hints 23 November 2018, 08:34:53 UTC
48ea462 Dzomo the everest Yak 22 November 2018, 08:35:15 UTC [CI] regenerate hints 22 November 2018, 08:35:15 UTC
2316092 Dzomo the everest Yak 21 November 2018, 08:36:35 UTC [CI] regenerate hints 21 November 2018, 08:36:35 UTC
a1e0623 Dzomo the everest Yak 20 November 2018, 08:35:53 UTC [CI] regenerate hints 20 November 2018, 08:35:53 UTC
8b17525 Dzomo the everest Yak 19 November 2018, 08:42:00 UTC [CI] regenerate hints 19 November 2018, 08:42:00 UTC
e555105 Dzomo the everest Yak 18 November 2018, 08:34:08 UTC [CI] regenerate hints 18 November 2018, 08:34:08 UTC
5a6799d Dzomo the everest Yak 17 November 2018, 08:39:47 UTC [CI] regenerate hints 17 November 2018, 08:39:47 UTC
8e20e26 Dzomo the everest Yak 16 November 2018, 08:37:36 UTC [CI] regenerate hints 16 November 2018, 08:37:36 UTC
08abf5a Dzomo the everest Yak 15 November 2018, 09:02:43 UTC [CI] regenerate hints 15 November 2018, 09:02:43 UTC
8bef9f8 Jonathan Protzenko 15 November 2018, 05:04:43 UTC Restore old target for the sake of CI 15 November 2018, 05:04:43 UTC
7e1e728 Jonathan Protzenko 15 November 2018, 02:19:32 UTC One more Makefile update 15 November 2018, 02:19:32 UTC
6352a52 Jonathan Protzenko 15 November 2018, 02:12:39 UTC --cmi in the specs directory as well 15 November 2018, 02:12:39 UTC
8d8d63a Jonathan Protzenko 15 November 2018, 01:43:38 UTC Need to pass more variables from the environment 15 November 2018, 01:43:38 UTC
5a2a1b4 Jonathan Protzenko 15 November 2018, 01:15:33 UTC Revert "Temporary workaround" This reverts commit 1294da6c926c5b09b06c224354e897b70dc1e2ee. 15 November 2018, 01:15:33 UTC
1294da6 Jonathan Protzenko 15 November 2018, 01:12:53 UTC Temporary workaround 15 November 2018, 01:12:53 UTC
07e81cf Jonathan Protzenko 14 November 2018, 19:25:08 UTC hints 14 November 2018, 19:25:08 UTC
d98741c Jonathan Protzenko 14 November 2018, 19:03:27 UTC Merge remote-tracking branch 'origin/_vale' into protz_hash_integration 14 November 2018, 19:03:27 UTC
fe3199a Jonathan Protzenko 14 November 2018, 19:02:27 UTC Spec-hintst 14 November 2018, 19:02:27 UTC
3c72768 Jonathan Protzenko 14 November 2018, 18:51:30 UTC Merge branch 'protz_hash_integration' of pro.github.com:mitls/hacl-star into protz_hash_integration 14 November 2018, 18:51:30 UTC
2a243e8 Jonathan Protzenko 14 November 2018, 18:51:14 UTC Fix a Makefile bug 14 November 2018, 18:51:14 UTC
5ff6acd Jonathan Protzenko 14 November 2018, 18:07:05 UTC Hints 14 November 2018, 18:07:05 UTC
970d3c6 Jonathan Protzenko 14 November 2018, 17:32:00 UTC Rlimit 14 November 2018, 17:32:00 UTC
aa5df91 Bryan Parno 14 November 2018, 16:59:30 UTC Add a special case for sha256rnds2 on Windows 14 November 2018, 16:59:30 UTC
0cacfff Jonathan Protzenko 14 November 2018, 16:57:42 UTC Remove a couple noextract 14 November 2018, 16:57:42 UTC
132332b Dzomo the everest Yak 14 November 2018, 09:04:50 UTC [CI] regenerate hints 14 November 2018, 09:04:50 UTC
6ff1092 Jonathan Protzenko 13 November 2018, 23:27:59 UTC Windows 13 November 2018, 23:27:59 UTC
e043178 Jonathan Protzenko 13 November 2018, 21:47:05 UTC Merge remote-tracking branch 'origin/fstar-master' into _vale 13 November 2018, 21:47:05 UTC
048d26e Jonathan Protzenko 13 November 2018, 19:02:36 UTC More hints + remove HMAC/HKDF from secure_api 13 November 2018, 19:02:36 UTC
2a7b6f2 Jonathan Protzenko 13 November 2018, 18:46:18 UTC Some names and aliases for miTLS to facilitate the merge 13 November 2018, 18:46:18 UTC
b065aa0 Gustavo Varo 13 November 2018, 05:17:36 UTC replace sed slash with @ 13 November 2018, 05:17:36 UTC
eb9fb4e Jonathan Protzenko 13 November 2018, 04:56:44 UTC More Makefile fixes 13 November 2018, 04:56:44 UTC
b87d364 Jonathan Protzenko 13 November 2018, 04:21:08 UTC Makefile fixes 13 November 2018, 04:21:08 UTC
45dceee Gustavo Varo 13 November 2018, 04:16:03 UTC Improve how we export home path to enhance debug. 13 November 2018, 04:16:03 UTC
042c0a8 Jonathan Protzenko 13 November 2018, 03:39:43 UTC Order-only dependency 13 November 2018, 03:39:43 UTC
4edb140 Jonathan Protzenko 13 November 2018, 03:11:45 UTC Missing dependency edge in the Makefile 13 November 2018, 03:11:45 UTC
d9ea08c Jonathan Protzenko 13 November 2018, 00:38:56 UTC First interop for the CPUID functions 13 November 2018, 00:38:56 UTC
93abcc5 Jonathan Protzenko 13 November 2018, 00:25:13 UTC Merge branch '_vale_extract_cpuid' into protz_hash_integration 13 November 2018, 00:25:13 UTC
22f5dfd Jonathan Protzenko 13 November 2018, 00:21:15 UTC Merge branch '_vale_extract_cpuid' of pro.github.com:mitls/hacl-star into _vale_extract_cpuid 13 November 2018, 00:21:15 UTC
07cfb6a Jonathan Protzenko 13 November 2018, 00:14:40 UTC Remove empty C file 13 November 2018, 00:14:40 UTC
84e1ef1 Aymeric Fromherz 12 November 2018, 23:54:39 UTC Add assume false in FastSqr + Extract cpuid 12 November 2018, 23:54:39 UTC
f8e0f67 Jonathan Protzenko 12 November 2018, 23:51:32 UTC Merge remote-tracking branch 'origin/fstar-master' into _vale_extract_cpuid 12 November 2018, 23:51:32 UTC
afefb3b Jonathan Protzenko 12 November 2018, 23:43:45 UTC Hints 12 November 2018, 23:43:45 UTC
ee3647c Jonathan Protzenko 12 November 2018, 23:43:27 UTC Restore old names, test vectors, enable run-time tests for all hash algorithms 12 November 2018, 23:43:27 UTC
81767e5 Aymeric Fromherz 12 November 2018, 23:17:38 UTC Add Cpuid extraction 12 November 2018, 23:17:38 UTC
6cb0393 Jonathan Protzenko 12 November 2018, 22:46:52 UTC Further simplify the Makefile thanks to proper packaging of the code/ directory, use KreMLin's new [rename=...] feature to generate cleaner code 12 November 2018, 22:46:52 UTC
c5c962f Jonathan Protzenko 12 November 2018, 21:41:51 UTC Remove a symbol and remove an entire file altogether (more compact build). Extract all targets when running vale under CI 12 November 2018, 21:41:51 UTC
9aed4e7 Jonathan Protzenko 12 November 2018, 19:54:07 UTC More work on vale/hacl integration. - More meaningful names for the generated .S and .asm files - Better bundling for the code/ directory - Makefile updates - Get rid of ValeGlue - Remove un-necessary steps in the Makefile - Make the names in the wrappers match the assembly symbols - Etc. etc. etc. 12 November 2018, 19:54:07 UTC
300985c Jonathan Protzenko 12 November 2018, 18:02:16 UTC Merge remote-tracking branch 'origin/fstar-master' into protz_hash_integration 12 November 2018, 18:02:16 UTC
b790bfb Jonathan Protzenko 12 November 2018, 18:02:08 UTC Everest layout 12 November 2018, 18:02:08 UTC
ac91c5b Jonathan Protzenko 12 November 2018, 17:50:51 UTC Hints and noextract 12 November 2018, 17:50:51 UTC
70f18d0 Aseem Rastogi 12 November 2018, 08:36:22 UTC Merge branch 'protz_hash_integration' of github.com:mitls/hacl-star into protz_hash_integration 12 November 2018, 08:36:22 UTC
337eea6 Aseem Rastogi 12 November 2018, 08:35:42 UTC tweaking the proof of hmac_core 12 November 2018, 08:35:42 UTC
6a7a438 Jonathan Protzenko 12 November 2018, 06:49:05 UTC Honor OTHERFLAGS, as reported by Aseem 12 November 2018, 06:49:05 UTC
707938e Jonathan Protzenko 12 November 2018, 06:24:21 UTC Don't use symlinks on windows 12 November 2018, 06:24:21 UTC
b01fd40 Chris Hawblitzel 12 November 2018, 01:34:20 UTC Upgrade vale directory to latest F* master 12 November 2018, 01:34:20 UTC
ba447f9 Jonathan Protzenko 11 November 2018, 22:22:14 UTC Hints, blocked 11 November 2018, 22:22:14 UTC
dbf14ac Jonathan Protzenko 11 November 2018, 20:53:42 UTC Nits and hints 11 November 2018, 20:53:42 UTC
b7b2742 Jonathan Protzenko 11 November 2018, 20:01:16 UTC Eliminate a couple instances of friends now that we have inline_for_extraction behind interfaces 11 November 2018, 20:01:16 UTC
8d95345 Jonathan Protzenko 11 November 2018, 19:48:57 UTC Merge remote-tracking branch 'origin/_vale' into protz_hash_integration 11 November 2018, 19:48:57 UTC
9e134e8 Aymeric Fromherz 11 November 2018, 03:46:26 UTC Add CMovc and Sbb in taint analysis 11 November 2018, 04:51:18 UTC
fa179ca Bryan Parno 11 November 2018, 02:34:28 UTC Add sample extern 11 November 2018, 02:34:28 UTC
706fe3e Bryan Parno 11 November 2018, 02:33:47 UTC Extract sub routines 11 November 2018, 02:33:47 UTC
ec4c7d0 Bryan Parno 11 November 2018, 02:32:14 UTC Fix SConstruct so that C test file for ECC code will compile and run 11 November 2018, 02:32:14 UTC
904a1e4 Bryan Parno 11 November 2018, 01:58:41 UTC Tweak rlimits to get two recalcitrant lemmas through and temporarily disable X64.Leakage_Ins.fst 11 November 2018, 01:58:41 UTC
2fb2aeb Bryan Parno 10 November 2018, 02:56:02 UTC Merge branch '_vale' into _fast_mul 10 November 2018, 02:56:02 UTC
a67d97a Bryan Parno 10 November 2018, 02:17:54 UTC Add sub and sub1 routines with stdcall interfaces all verifying 10 November 2018, 02:17:54 UTC
b15f8bd Bryan Parno 09 November 2018, 21:27:27 UTC Sketch in sub1 and stdcall wrappers for sub and sub1 09 November 2018, 21:27:27 UTC
2e32a98 Bryan Parno 09 November 2018, 17:01:05 UTC Update test file for ECC 09 November 2018, 17:01:05 UTC
ca1fa4e Bryan Parno 09 November 2018, 16:57:39 UTC Upgrade to latest F* master 09 November 2018, 16:57:39 UTC
884a181 Bryan Parno 09 November 2018, 16:11:17 UTC Remove some unnecessary asserts to try to stabilize a proof 09 November 2018, 16:11:17 UTC
6241943 Bryan Parno 09 November 2018, 07:13:13 UTC Push 4-way subtraction through 09 November 2018, 07:13:13 UTC
e9e9435 Bryan Parno 09 November 2018, 05:30:14 UTC Fix order of operations 09 November 2018, 05:30:14 UTC
605097c Bryan Parno 09 November 2018, 04:58:19 UTC Add printing and Hoare rules 09 November 2018, 04:58:19 UTC
447c92f Bryan Parno 09 November 2018, 03:34:13 UTC Enrich the spec for sub, and add specs for SBB and CMOVC 09 November 2018, 04:08:31 UTC
59f03ba Jonathan Protzenko 08 November 2018, 00:14:03 UTC Minor Makefile changes 08 November 2018, 00:14:03 UTC
def71e9 Bryan Parno 07 November 2018, 21:01:10 UTC Merge branch '_vale' into _fast_mul 07 November 2018, 21:01:10 UTC
c813676 Aymeric Fromherz 07 November 2018, 15:53:49 UTC Fix Sha compilation 07 November 2018, 15:53:49 UTC
1fdb762 Aymeric Fromherz 07 November 2018, 05:10:21 UTC Fix extraction of AesGcm 07 November 2018, 05:10:28 UTC
back to top