5338817 | Nikhil Swamy | 17 May 2017, 19:27:06 UTC | Merge remote-tracking branch 'origin/master' into nik_private | 17 May 2017, 19:27:06 UTC |
5587916 | Nikhil Swamy | 17 May 2017, 19:27:02 UTC | adding a targeted assume in ChaCha20Poly1305.fst | 17 May 2017, 19:27:02 UTC |
cea2e72 | Antoine Delignat-Lavaud | 17 May 2017, 14:04:13 UTC | Fix typo | 17 May 2017, 14:05:33 UTC |
99ae1ce | Dzomo the everest Yak | 17 May 2017, 10:56:27 UTC | [CI] regenerate hints | 17 May 2017, 10:56:27 UTC |
d187e74 | Dzomo the everest Yak | 17 May 2017, 07:36:28 UTC | [CI] regenerate hints | 17 May 2017, 07:36:28 UTC |
18291a1 | Nikhil Swamy | 17 May 2017, 05:42:33 UTC | upgrading F* | 17 May 2017, 05:42:33 UTC |
4259c8a | Nikhil Swamy | 17 May 2017, 05:40:33 UTC | reverting unnecessary changes | 17 May 2017, 05:40:33 UTC |
97b865a | Nikhil Swamy | 17 May 2017, 05:33:59 UTC | regen hints | 17 May 2017, 05:33:59 UTC |
39e67a7 | Nikhil Swamy | 17 May 2017, 05:01:47 UTC | Merge branch 'nik_private' of github.com:mitls/hacl-star into nik_private | 17 May 2017, 05:01:47 UTC |
051ddb6 | Nikhil Swamy | 17 May 2017, 05:01:40 UTC | fixing a bad set-options, cf F* issue #1029; regen a few hints | 17 May 2017, 05:01:40 UTC |
2048118 | Nikhil Swamy | 17 May 2017, 04:49:34 UTC | fixing Crypto.Symmetric.Bytes, cf F* issue #1028 | 17 May 2017, 04:49:34 UTC |
5847be2 | Nikhil Swamy | 16 May 2017, 22:32:08 UTC | new hints etc. trying to move forward to the latest f* | 16 May 2017, 22:32:08 UTC |
c4802c0 | Nikhil Swamy | 16 May 2017, 21:21:25 UTC | Merge remote-tracking branch 'origin/master' into nik_private | 16 May 2017, 21:21:25 UTC |
2aeda05 | Dzomo the everest Yak | 16 May 2017, 19:19:43 UTC | [CI] regenerate hints | 16 May 2017, 19:19:43 UTC |
e430fe9 | Dzomo the everest Yak | 16 May 2017, 07:38:38 UTC | [CI] regenerate hints | 16 May 2017, 07:38:38 UTC |
dde7217 | Dzomo the everest Yak | 15 May 2017, 10:47:07 UTC | [CI] regenerate hints | 15 May 2017, 10:47:07 UTC |
92cb0c9 | Dzomo the everest Yak | 15 May 2017, 07:40:23 UTC | [CI] regenerate hints | 15 May 2017, 07:40:23 UTC |
55bc441 | Dzomo the everest Yak | 14 May 2017, 10:45:06 UTC | [CI] regenerate hints | 14 May 2017, 10:45:06 UTC |
33f992b | Dzomo the everest Yak | 13 May 2017, 11:17:58 UTC | [CI] regenerate hints | 13 May 2017, 11:17:58 UTC |
1b33b74 | Antoine Delignat-Lavaud | 12 May 2017, 13:34:11 UTC | -fPIC | 12 May 2017, 13:35:44 UTC |
42ef844 | Dzomo the everest Yak | 12 May 2017, 10:42:19 UTC | [CI] regenerate hints | 12 May 2017, 10:42:19 UTC |
b2cf2e8 | Dzomo the everest Yak | 12 May 2017, 07:39:57 UTC | [CI] regenerate hints | 12 May 2017, 07:39:57 UTC |
17efaea | Nikhil Swamy | 11 May 2017, 23:11:13 UTC | regen hints | 11 May 2017, 23:11:13 UTC |
40ad5a1 | Nikhil Swamy | 11 May 2017, 19:41:58 UTC | reverting changes from the makefile | 11 May 2017, 19:41:58 UTC |
c5e1c55 | Nikhil Swamy | 11 May 2017, 19:39:47 UTC | Merge remote-tracking branch 'origin/master' into nik_private | 11 May 2017, 19:39:47 UTC |
acc4c59 | Santiago Zanella-Beguelin | 11 May 2017, 14:23:10 UTC | Nit | 11 May 2017, 14:23:32 UTC |
9ee3a6f | Dzomo the everest Yak | 11 May 2017, 11:04:21 UTC | Merge commit '277c5451adce016714890f4ad5bdcf8b0558dda9' | 11 May 2017, 11:04:21 UTC |
277c545 | Dzomo the everest Yak | 11 May 2017, 11:04:19 UTC | [CI] regenerate hints | 11 May 2017, 11:04:19 UTC |
19d8a40 | Santiago Zanella-Beguelin | 11 May 2017, 10:49:41 UTC | Rename target | 11 May 2017, 10:49:56 UTC |
1b415d2 | Dzomo the everest Yak | 11 May 2017, 07:42:19 UTC | [CI] regenerate hints | 11 May 2017, 07:42:19 UTC |
20cf80d | Santiago Zanella-Beguelin | 10 May 2017, 23:04:23 UTC | Revert adding tmp directory | 10 May 2017, 23:04:23 UTC |
3ee6c56 | Santiago Zanella-Beguelin | 10 May 2017, 22:29:10 UTC | Ignore tmp | 10 May 2017, 22:29:10 UTC |
39d90ef | Santiago Zanella-Beguelin | 10 May 2017, 22:26:40 UTC | Add empty tmp directory for Kremlin build | 10 May 2017, 22:26:40 UTC |
84e3ceb | Nikhil Swamy | 10 May 2017, 14:15:34 UTC | merging master in | 10 May 2017, 14:15:34 UTC |
58c5c7e | Santiago Zanella-Beguelin | 10 May 2017, 14:13:29 UTC | Missing dependency | 10 May 2017, 14:13:45 UTC |
8527df2 | Dzomo the everest Yak | 10 May 2017, 10:59:48 UTC | [CI] regenerate hints | 10 May 2017, 10:59:48 UTC |
52b2108 | Santiago Zanella-Beguelin | 10 May 2017, 09:17:19 UTC | Compile Vale AES | 10 May 2017, 09:17:19 UTC |
58f504d | Dzomo the everest Yak | 10 May 2017, 07:40:57 UTC | [CI] regenerate hints | 10 May 2017, 07:40:57 UTC |
3678563 | Nikhil Swamy | 10 May 2017, 06:19:03 UTC | missing sep | 10 May 2017, 06:19:03 UTC |
0b7094e | Nikhil Swamy | 10 May 2017, 06:15:10 UTC | trying to actually try verification regression test | 10 May 2017, 06:15:10 UTC |
ddba04d | Nikhil Swamy | 10 May 2017, 06:05:26 UTC | moving kremlin | 10 May 2017, 06:05:26 UTC |
2137df4 | Nikhil Swamy | 10 May 2017, 05:29:14 UTC | silly edit to trigger a build | 10 May 2017, 05:29:14 UTC |
7f76b51 | Nikhil Swamy | 09 May 2017, 15:25:34 UTC | trying an f* upgrade | 09 May 2017, 15:25:34 UTC |
eb82e97 | Dzomo the everest Yak | 09 May 2017, 10:40:12 UTC | [CI] regenerate hints | 09 May 2017, 10:40:12 UTC |
6f6a062 | Dzomo the everest Yak | 09 May 2017, 07:32:36 UTC | [CI] regenerate hints | 09 May 2017, 07:32:36 UTC |
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 |
678ae6e | Nikhil Swamy | 25 April 2017, 00:07:24 UTC | trying to optimize a proof counterblocks_snoc | 25 April 2017, 00:07:24 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 |