sort by:
Revision Author Date Message Commit Date
aafbd0a Aligned F* paths and flags in Makefiles 08 May 2017, 14:50:37 UTC
e850d7a [CI] regenerate hints 08 May 2017, 10:44:03 UTC
7fa5d21 [CI] regenerate hints 08 May 2017, 07:32:29 UTC
ea886c1 [CI] regenerate hints 07 May 2017, 10:39:46 UTC
5ad614a [CI] regenerate hints 06 May 2017, 11:25:16 UTC
c19ea30 [CI] regenerate hints 05 May 2017, 10:41:59 UTC
109eae2 [CI] regenerate hints 05 May 2017, 07:32:10 UTC
e5597fa Build fix 04 May 2017, 16:32:43 UTC
c8ac2cb [CI] regenerate hints 04 May 2017, 10:38:48 UTC
6966d1f [CI] regenerate hints 04 May 2017, 07:32:07 UTC
4a66226 [CI] regenerate hints 03 May 2017, 10:55:50 UTC
232cc11 [CI] regenerate hints 03 May 2017, 07:39:31 UTC
315d5f3 [CI] regenerate hints 02 May 2017, 10:38:46 UTC
61fa427 [CI] regenerate hints 02 May 2017, 07:41:13 UTC
85d0175 [CI] regenerate hints 01 May 2017, 10:38:49 UTC
89a464b [CI] regenerate hints 01 May 2017, 07:41:52 UTC
cc6c791 [CI] regenerate hints 30 April 2017, 10:40:12 UTC
59fa36c [CI] regenerate hints 29 April 2017, 11:17:44 UTC
1838485 typo 28 April 2017, 14:22:12 UTC
f01afca [CI] regenerate hints 28 April 2017, 10:38:57 UTC
38b10a5 [CI] regenerate hints 28 April 2017, 07:38:55 UTC
357bf7e [CI] regenerate hints 27 April 2017, 10:38:21 UTC
daf485c [CI] regenerate hints 27 April 2017, 07:32:35 UTC
f5c1b76 [CI] regenerate hints 26 April 2017, 10:38:14 UTC
c936f78 [CI] regenerate hints 26 April 2017, 07:41:36 UTC
82c94d9 merge with master 25 April 2017, 19:57:43 UTC
449fade moving dependencies to master of F* and Kremlin 25 April 2017, 19:49:06 UTC
0f74418 kremlin update 25 April 2017, 18:57:31 UTC
be40a43 reverting some makefile changes 25 April 2017, 18:49:28 UTC
279d399 submodule update for F* 25 April 2017, 18:41:29 UTC
dc72c5b [CI] regenerate hints 25 April 2017, 17:18:54 UTC
a3cfbcf Try again 25 April 2017, 15:29:26 UTC
3c45bbb Sequentialize compcert/msvc extraction 25 April 2017, 13:31:24 UTC
9349423 removing one assume, by carrying the precondition that the region of CMA state is AEAD state.prf.mac_rgn 25 April 2017, 08:22:26 UTC
23cb92b merge with hacl master 25 April 2017, 07:51:45 UTC
c8da71b [CI] regenerate hints 25 April 2017, 07:38:14 UTC
d931cae Merge branch 'protz_bump_fstar' 24 April 2017, 23:22:00 UTC
26ffe2a Remove --hint_info 24 April 2017, 23:20:42 UTC
b461259 Workaround Z3 4.5.0 not respecting rlimit 24 April 2017, 22:54:41 UTC
ce999b6 strengthening definition of Heap.equal_dom, code/ verifies without the assumes now 24 April 2017, 19:24:55 UTC
4f26748 some hints 24 April 2017, 17:31:27 UTC
c346286 Debug with --hint_info 24 April 2017, 15:25:30 UTC
18b36d7 fixing assertion failures in code, for 2 of them assumes remain that need to be debugged 24 April 2017, 14:37:40 UTC
52f89bb Merge branch 'protz_bump_fstar' 24 April 2017, 13:30:27 UTC
a615eb0 [CI] regenerate hints 24 April 2017, 13:16:17 UTC
71321b7 Update FStar and kremlin submodules to latest master 24 April 2017, 12:45:27 UTC
7bba95a hints, and making one more proof go through 24 April 2017, 11:47:47 UTC
16bc09b secure_api goes through with targeted assumes for separation of regions, these surfaced probably because in the new heap model there is no injectivity axiom 24 April 2017, 11:11:32 UTC
1f238f6 some proof fixes and hints 24 April 2017, 10:35:20 UTC
4fb85a1 Bump fstar, fix Wrappers.CMA regression (with aseem) 24 April 2017, 10:32:53 UTC
92d6708 [CI] regenerate hints 24 April 2017, 07:43:27 UTC
79444e5 debugging more failures in code and secure_api 22 April 2017, 13:27:27 UTC
b0c2882 wip on the new heap model 21 April 2017, 13:57:59 UTC
04b7008 [CI] regenerate hints 21 April 2017, 07:44:14 UTC
7f260da [CI] regenerate hints 20 April 2017, 07:44:43 UTC
4754c73 [CI] regenerate hints 19 April 2017, 07:50:49 UTC
e11c5eb Workaround for #490 18 April 2017, 12:45:00 UTC
cb15296 Use Crypto.Plain in AEAD interface 18 April 2017, 12:36:22 UTC
63ed87d [CI] regenerate hints 18 April 2017, 07:42:12 UTC
c771955 [CI] regenerate hints 17 April 2017, 07:44:48 UTC
a8b403d removed more 'inline_for_extraction' keyworks on stateful functions 16 April 2017, 09:56:56 UTC
c4fe4bb fixed Hacl.Impl.Xor.Lemmas and fixed verify target in the Makefile to make it fail properly 16 April 2017, 09:45:59 UTC
183d1ba fixed visibility issue for Hacl.SecureAPI.Chacha20 15 April 2017, 11:31:15 UTC
3882a0c Merge branch 'master' into jk_uint32s_loops 15 April 2017, 11:20:58 UTC
22fdbe7 cleaning up the chacha and salsa impl files 15 April 2017, 11:20:14 UTC
de734c7 moving all of salsa-family to loops 14 April 2017, 21:26:36 UTC
ae5a260 Merge branch 'protz_bump_fstar' of https://www.github.com/mitls/hacl-star into protz_bump_fstar 14 April 2017, 17:14:59 UTC
73c6269 Fix regressions in UF1CMA (works for me, let's see CI) 14 April 2017, 17:10:29 UTC
90a37e5 Merge branch 'master' of github.com:mitls/hacl-star 14 April 2017, 16:16:22 UTC
4807ddd ct nits 14 April 2017, 15:44:11 UTC
c186817 turned load32_bytes into loops 14 April 2017, 15:33:11 UTC
7b9f974 [CI] regenerate hints 14 April 2017, 07:37:24 UTC
b6acea0 refreshed hints after merge with master 13 April 2017, 15:47:21 UTC
d237240 refreshed hints for hacl code 13 April 2017, 15:06:36 UTC
e1191e9 Merge branch 'master' of github.com:mitls/hacl-star 13 April 2017, 15:05:15 UTC
fa07469 removed inline_for_extraction where it was triggering verbose warnings 13 April 2017, 14:50:55 UTC
094eb64 Merge branch 'master' of github.com:mitls/hacl-star 13 April 2017, 14:44:44 UTC
5cd285d more whitespace 13 April 2017, 14:37:13 UTC
f1ef86b whitespace cleanup 13 April 2017, 14:36:35 UTC
8cc7691 Merge branch 'master' of github.com:mitls/hacl-star 13 April 2017, 14:32:49 UTC
22f9fc2 hints and fuel changes 13 April 2017, 14:26:59 UTC
94e5fc6 removed spurious assume 13 April 2017, 10:27:18 UTC
87c1d14 bumped timeout for Hacl.Bignum.Crecip.fst 13 April 2017, 08:45:08 UTC
6fa7758 [CI] regenerate hints 13 April 2017, 07:38:28 UTC
c74bc68 Refresh hints in secure_api too 13 April 2017, 06:47:55 UTC
1eb4369 perm 12 April 2017, 23:58:24 UTC
e86e0cc adding a "dumb" top-level interface Crypto.AEAD.Main 12 April 2017, 23:58:08 UTC
29a6427 Another fix 12 April 2017, 22:13:01 UTC
4677cca Blind fix in the hope of getting a green... 12 April 2017, 22:03:01 UTC
363c395 Refresh all hints 12 April 2017, 21:51:52 UTC
21648d9 fresh hints for Hacl.Spec.Bignum.Fproduct 12 April 2017, 18:04:01 UTC
8b94770 fresh hints for Hacl.Spec.Bignum.Fproduct 12 April 2017, 18:00:48 UTC
abbaa13 green ? 12 April 2017, 17:56:31 UTC
a3dafe7 updated kremlin submodule 12 April 2017, 17:30:23 UTC
57b1a2e fixed unmerged file 12 April 2017, 17:24:38 UTC
f197c01 merge of master and hints 12 April 2017, 17:21:01 UTC
d1dd3c6 hints 12 April 2017, 17:18:43 UTC
5bd4167 nits 12 April 2017, 17:00:17 UTC
5ac3c02 propagating loop changes to higher modules 12 April 2017, 16:26:59 UTC
7c6dcfa Move Indexing to separate subdirectory 12 April 2017, 14:33:10 UTC
back to top