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