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
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
back to top