13e7271 | Aymeric Fromherz | 31 July 2019, 08:57:48 UTC | Ed: Finish proving barrett reduction | 31 July 2019, 08:57:48 UTC |
fb598f5 | Aymeric Fromherz | 31 July 2019, 07:39:26 UTC | Ed: Verify two multiplications in BignumQ | 31 July 2019, 07:39:26 UTC |
a1bbc7d | Aymeric Fromherz | 31 July 2019, 02:00:47 UTC | Merge branch '_dev' into _afromher_dev | 31 July 2019, 02:00:47 UTC |
0d31cc5 | Marina Polubelova | 30 July 2019, 23:18:23 UTC | wip: add proof of sub_mod_264 | 30 July 2019, 23:18:23 UTC |
9aebd46 | Marina Polubelova | 30 July 2019, 22:12:26 UTC | wip: add proof of mod_264 | 30 July 2019, 22:12:26 UTC |
e17528d | Marina Polubelova | 30 July 2019, 21:22:57 UTC | wip: add proof of div_264 | 30 July 2019, 21:22:57 UTC |
2f16ba5 | Marina Polubelova | 30 July 2019, 19:58:10 UTC | wip: fix postconditon of add_modq | 30 July 2019, 19:58:10 UTC |
19f1f52 | Marina Polubelova | 30 July 2019, 15:09:10 UTC | wip: functional correctness of bignumQ | 30 July 2019, 15:09:10 UTC |
e91ddeb | Santiago Zanella-Beguelin | 30 July 2019, 13:49:25 UTC | Hints | 30 July 2019, 13:49:25 UTC |
1c788ba | Santiago Zanella-Beguelin | 30 July 2019, 13:43:03 UTC | Fix extraction of code/hash and add it to the CI target | 30 July 2019, 13:43:03 UTC |
a945514 | Santiago Zanella-Beguelin | 30 July 2019, 13:42:26 UTC | Whitespace cleanup | 30 July 2019, 13:42:26 UTC |
cef3e13 | Santiago Zanella-Beguelin | 30 July 2019, 13:34:23 UTC | Elaborate a flaky proof in Hacl.Hash.MD; decrease fuel and ifuel to minimum required | 30 July 2019, 13:34:40 UTC |
45e9c77 | Marina Polubelova | 29 July 2019, 12:15:16 UTC | wip: start proving bignumQ | 29 July 2019, 12:15:16 UTC |
f848c50 | Aymeric Fromherz | 29 July 2019, 04:16:38 UTC | Ed: Split spec into key generation + sign expanded, and link implementations to spec | 29 July 2019, 04:16:38 UTC |
a62052e | Aymeric Fromherz | 29 July 2019, 03:12:05 UTC | Ed: Prove SwapConditional | 29 July 2019, 03:12:05 UTC |
88d4bb9 | Aymeric Fromherz | 29 July 2019, 02:04:44 UTC | Ed: admit in bignumQ.mul for makefile | 29 July 2019, 02:04:44 UTC |
ff697e2 | Aymeric Fromherz | 29 July 2019, 01:55:04 UTC | Ed: Prove Sha512.Modq | 29 July 2019, 01:55:04 UTC |
ee5cac9 | Marina Polubelova | 28 July 2019, 19:48:21 UTC | wip: add low-level spec for BignumQ | 28 July 2019, 19:48:21 UTC |
7855a67 | Marina Polubelova | 28 July 2019, 11:17:04 UTC | wip: spec equiv proof of gf128 | 28 July 2019, 11:17:04 UTC |
a61479b | Aymeric Fromherz | 28 July 2019, 01:38:31 UTC | Ed: Work towards barrett reduction | 28 July 2019, 01:38:31 UTC |
75b71ca | Marina Polubelova | 27 July 2019, 23:20:09 UTC | hints | 27 July 2019, 23:20:09 UTC |
da20547 | Marina Polubelova | 27 July 2019, 23:17:13 UTC | use lemma_repeat_blocks_multi_vec in spec equiv proof of poly1305 | 27 July 2019, 23:17:13 UTC |
3ddab4d | Benjamin Lipp (blipp) | 27 July 2019, 18:55:03 UTC | Merge branch '_dev' of github.com:project-everest/hacl-star into _dev | 27 July 2019, 18:55:03 UTC |
089a8cd | Benjamin Lipp (blipp) | 27 July 2019, 18:52:29 UTC | Create .hints directory for aes-256-cbc | 27 July 2019, 18:52:29 UTC |
10d5889 | Marina Polubelova | 27 July 2019, 16:21:39 UTC | wip: add repeat_blocks_vec lemma | 27 July 2019, 16:21:39 UTC |
a93241a | Aymeric Fromherz | 27 July 2019, 07:22:20 UTC | Ed: Restore sign steps + specify add/mul_modq | 27 July 2019, 07:22:20 UTC |
de25fcd | Aymeric Fromherz | 27 July 2019, 06:58:01 UTC | Ed: Prove store 56 | 27 July 2019, 06:58:01 UTC |
756a17b | Aymeric Fromherz | 27 July 2019, 04:01:39 UTC | Ed: Fix precondition for store_56 | 27 July 2019, 04:01:39 UTC |
4127725 | Aymeric Fromherz | 27 July 2019, 03:38:46 UTC | Ed: Stabilize more proofs | 27 July 2019, 03:38:46 UTC |
ce73806 | Aymeric Fromherz | 27 July 2019, 00:40:37 UTC | Stabilize some proofs | 27 July 2019, 00:40:37 UTC |
b9c89fa | Aymeric Fromherz | 27 July 2019, 00:40:29 UTC | Ed: Proof of Load | 27 July 2019, 00:40:29 UTC |
60773d2 | Aymeric Fromherz | 26 July 2019, 22:11:42 UTC | Merge branch '_dev' into _afromher_dev | 26 July 2019, 22:11:42 UTC |
dc046f9 | Aymeric Fromherz | 17 July 2019, 05:45:10 UTC | Ed25519: Assuming correctness of sign_steps, prove sign | 26 July 2019, 21:31:06 UTC |
de10381 | Aymeric Fromherz | 26 July 2019, 20:46:03 UTC | Ed: Finish proving bignum25519 | 26 July 2019, 20:46:03 UTC |
59da9e2 | Benjamin Beurdouche | 26 July 2019, 13:30:32 UTC | Merge branch '_dev' of github.com:project-everest/hacl-star into _dev | 26 July 2019, 13:30:32 UTC |
f228a85 | Benjamin Beurdouche | 26 July 2019, 13:30:27 UTC | Progress on FC for Blake2.Incremental | 26 July 2019, 13:30:27 UTC |
f2150d3 | Marina Polubelova | 26 July 2019, 10:04:50 UTC | wip: add lemmas about vectorization | 26 July 2019, 10:04:50 UTC |
7cfeba0 | Marina Polubelova | 26 July 2019, 09:35:22 UTC | wip: spec equiv proof of gf128 | 26 July 2019, 09:35:22 UTC |
90d907a | Marina Polubelova | 25 July 2019, 22:41:58 UTC | cleanup | 25 July 2019, 22:41:58 UTC |
9e1f17b | Marina Polubelova | 25 July 2019, 22:22:05 UTC | add repeat_blocks_multi_split lemma | 25 July 2019, 22:22:05 UTC |
c211b6e | Marina Polubelova | 25 July 2019, 21:47:32 UTC | add repeat_blocks_split lemma | 25 July 2019, 21:47:32 UTC |
58c994b | Aymeric Fromherz | 25 July 2019, 21:30:08 UTC | Ed: Prove Load/Store51 | 25 July 2019, 21:30:08 UTC |
2ba975f | Aymeric Fromherz | 25 July 2019, 18:27:46 UTC | Ed: Proof of verify | 25 July 2019, 18:27:46 UTC |
2953923 | Benjamin Beurdouche | 25 July 2019, 13:33:48 UTC | Progress on FC for Blake2 incremental update | 25 July 2019, 13:33:48 UTC |
40599c4 | Benjamin Beurdouche | 25 July 2019, 12:15:08 UTC | Restore extraction of Incremental Blake2 | 25 July 2019, 12:15:08 UTC |
c647190 | Benjamin Beurdouche | 25 July 2019, 12:08:27 UTC | Merge branch '_dev' of github.com:project-everest/hacl-star into _dev | 25 July 2019, 12:08:27 UTC |
e99612e | Benjamin Beurdouche | 25 July 2019, 12:08:15 UTC | Restore extraction of Blake2b | 25 July 2019, 12:08:15 UTC |
1bb1984 | Marina Polubelova | 25 July 2019, 10:16:07 UTC | fix normalize4 | 25 July 2019, 10:16:07 UTC |
2e05426 | Benjamin Beurdouche | 24 July 2019, 23:59:33 UTC | Progress on FC for Blake2 incremental | 24 July 2019, 23:59:33 UTC |
5e60e03 | Benjamin Beurdouche | 24 July 2019, 23:13:17 UTC | Remove a branching in incremental Blake2 | 24 July 2019, 23:13:17 UTC |
a13a1ce | Benjamin Beurdouche | 24 July 2019, 23:06:36 UTC | Progress on FC for Blake2 incremental | 24 July 2019, 23:06:36 UTC |
26169df | Benjamin Beurdouche | 24 July 2019, 21:18:57 UTC | Progress on FC for Blake2 incremental | 24 July 2019, 21:18:57 UTC |
10230d6 | Benjamin Beurdouche | 24 July 2019, 20:53:24 UTC | Progress on FC for Blake2 incremental | 24 July 2019, 20:53:24 UTC |
ed8f839 | Benjamin Beurdouche | 24 July 2019, 20:06:42 UTC | Merge branch '_dev' of github.com:project-everest/hacl-star into _dev | 24 July 2019, 20:06:42 UTC |
d27f35b | Benjamin Beurdouche | 24 July 2019, 20:06:04 UTC | Progress on Blake2 experiment | 24 July 2019, 20:06:04 UTC |
2262cae | Marina Polubelova | 24 July 2019, 17:01:22 UTC | fix Makefile | 24 July 2019, 17:01:22 UTC |
3b28e3a | Marina Polubelova | 24 July 2019, 15:04:02 UTC | hints | 24 July 2019, 15:04:02 UTC |
9af69d4 | Marina Polubelova | 24 July 2019, 15:03:30 UTC | add nacl-box to `make ci` | 24 July 2019, 15:03:30 UTC |
48803f7 | Marina Polubelova | 24 July 2019, 14:43:50 UTC | update test for nacl-box | 24 July 2019, 14:43:50 UTC |
aa4e71f | Benjamin Beurdouche | 24 July 2019, 14:33:49 UTC | MS for Blake2 experiment | 24 July 2019, 14:33:49 UTC |
635c72e | Marina Polubelova | 24 July 2019, 12:32:38 UTC | add precomputed interface for Box and clean up test file | 24 July 2019, 12:32:38 UTC |
750d27f | Santiago Zanella-Beguelin | 23 July 2019, 11:06:16 UTC | Add commit missed missed by merge: Decrease fuel and ifuel settings to increase proof stability | 24 July 2019, 10:03:02 UTC |
01abf80 | Aymeric Fromherz | 24 July 2019, 05:18:47 UTC | Ed: Prove PointEqual + almost complete verify | 24 July 2019, 05:18:47 UTC |
84b3efb | Aymeric Fromherz | 24 July 2019, 04:39:37 UTC | Ed: Prove eq in pointEqual | 24 July 2019, 04:39:37 UTC |
ec469f0 | Benjamin Beurdouche | 24 July 2019, 01:14:16 UTC | More folders in .gitignore | 24 July 2019, 01:14:16 UTC |
579f97d | Benjamin Beurdouche | 24 July 2019, 01:12:59 UTC | Refresh hints | 24 July 2019, 01:12:59 UTC |
c7a6d29 | Benjamin Beurdouche | 24 July 2019, 01:05:56 UTC | Fix GF128 after changes in Lib | 24 July 2019, 01:05:56 UTC |
07e0961 | Benjamin Beurdouche | 24 July 2019, 00:09:40 UTC | Merge branch '_dev_inttypes' into _dev | 24 July 2019, 00:09:40 UTC |
743de07 | Benjamin Beurdouche | 24 July 2019, 00:07:06 UTC | Implement a code test for experimental Blake2 | 24 July 2019, 00:07:06 UTC |
e7d22b7 | Benjamin Beurdouche | 23 July 2019, 23:45:29 UTC | Fix extraction of code for Blake2 experiment | 23 July 2019, 23:45:29 UTC |
9d5e0a2 | Benjamin Beurdouche | 23 July 2019, 21:59:40 UTC | Some renaming in code for Blake2 experiment | 23 July 2019, 21:59:40 UTC |
08bb37a | Benjamin Beurdouche | 23 July 2019, 21:53:35 UTC | Progress on code for Blake2 experiment | 23 July 2019, 21:53:35 UTC |
c023ac5 | Benjamin Beurdouche | 23 July 2019, 21:40:54 UTC | Reorganize code for Blake2 experiement | 23 July 2019, 21:40:54 UTC |
004f2b9 | Benjamin Beurdouche | 23 July 2019, 21:39:25 UTC | Progress on updating Low* for Blake2 experiment | 23 July 2019, 21:39:25 UTC |
35d9bbe | Benjamin Beurdouche | 23 July 2019, 20:34:13 UTC | Minor improvement for Blake2 experiment | 23 July 2019, 20:34:13 UTC |
72a0890 | Benjamin Beurdouche | 23 July 2019, 20:32:02 UTC | Simplify Blake2 experiment | 23 July 2019, 20:32:02 UTC |
8460916 | Benjamin Beurdouche | 23 July 2019, 20:28:32 UTC | Improvement for Blake2 experiment | 23 July 2019, 20:28:32 UTC |
554fc1e | Benjamin Beurdouche | 23 July 2019, 20:18:28 UTC | Horrible but fixed Blake2 experiment | 23 July 2019, 20:18:28 UTC |
e8d451a | Benjamin Beurdouche | 23 July 2019, 16:59:45 UTC | Makefile for experiemental Blake2 | 23 July 2019, 16:59:45 UTC |
412565d | Benjamin Beurdouche | 23 July 2019, 16:07:51 UTC | Progress on debugging Blake2 experiment | 23 July 2019, 16:07:51 UTC |
95dcd37 | Aymeric Fromherz | 22 July 2019, 20:57:47 UTC | Ed: Prove PointDecompress | 22 July 2019, 20:57:47 UTC |
ee69093 | Aymeric Fromherz | 22 July 2019, 18:38:19 UTC | Ed: Proof of recover x | 22 July 2019, 18:38:19 UTC |
cb62edf | Santiago Zanella-Beguelin | 22 July 2019, 16:24:24 UTC | Hints | 22 July 2019, 16:24:24 UTC |
fe1946b | Santiago Zanella-Beguelin | 22 July 2019, 15:30:55 UTC | Remove Spec.AES{128,256}_GCM and corresponding tests, superseded by Spec.Agile.AEAD Remove an admit in Spec.Agile.AEAD | 22 July 2019, 15:30:55 UTC |
b7d63ca | Marina Polubelova | 22 July 2019, 14:24:26 UTC | wip: gf128 | 22 July 2019, 14:24:26 UTC |
1c7bc33 | Benjamin Beurdouche | 22 July 2019, 13:57:37 UTC | Improve Spec.Blake2.Incremental testing (find errors) | 22 July 2019, 13:57:37 UTC |
15be11a | Santiago Zanella-Beguelin | 22 July 2019, 13:38:10 UTC | Hints | 22 July 2019, 13:38:10 UTC |
daf41d5 | Santiago Zanella-Beguelin | 22 July 2019, 13:36:33 UTC | Stabilize a proof | 22 July 2019, 13:36:33 UTC |
f5d36e7 | Benjamin Beurdouche | 22 July 2019, 13:27:56 UTC | Minor improvement for tests/Spec.Blake2.Incremental.Test.fst | 22 July 2019, 13:27:56 UTC |
5c34aa3 | Benjamin Beurdouche | 22 July 2019, 13:27:21 UTC | Fix debug function in Blake2 experiment | 22 July 2019, 13:27:21 UTC |
0590951 | Benjamin Beurdouche | 22 July 2019, 13:08:27 UTC | Helpful debug function for Blake2 experiment | 22 July 2019, 13:08:27 UTC |
b766649 | Benjamin Beurdouche | 22 July 2019, 12:44:56 UTC | More testing of Spec.Blake2.Incremental | 22 July 2019, 12:44:56 UTC |
8a8898c | Benjamin Beurdouche | 22 July 2019, 12:44:23 UTC | Progress on Blake2 experiment | 22 July 2019, 12:44:23 UTC |
0d25b8f | Benjamin Beurdouche | 22 July 2019, 12:43:59 UTC | Minor coding style change | 22 July 2019, 12:43:59 UTC |
81093ce | Santiago Zanella-Beguelin | 22 July 2019, 12:21:03 UTC | Hints | 22 July 2019, 12:21:03 UTC |
4c17e83 | Santiago Zanella-Beguelin | 22 July 2019, 12:20:50 UTC | Allow experimental AES-GCM test to fail in Cygwin | 22 July 2019, 12:20:50 UTC |
890b003 | Santiago Zanella-Beguelin | 22 July 2019, 12:02:05 UTC | Elaborate a fragile proof using calc | 22 July 2019, 12:02:05 UTC |
0c8ed77 | Benjamin Beurdouche | 22 July 2019, 11:53:42 UTC | Progress on Blake2 experiement | 22 July 2019, 11:53:42 UTC |
01a4f0b | Santiago Zanella-Beguelin | 22 July 2019, 09:48:23 UTC | Replace let ... in by irrefutable pattern; remove stray admit | 22 July 2019, 09:48:23 UTC |
17d3b66 | Santiago Zanella-Beguelin | 22 July 2019, 09:16:30 UTC | Equivalent but easier to type check specification for shift_left | 22 July 2019, 09:16:30 UTC |