afc5973 | Chris Hawblitzel | 05 September 2019, 15:36:51 UTC | Tweak some options for recent Makefile change | 05 September 2019, 15:36:51 UTC |
ac17e8d | Chris Hawblitzel | 05 September 2019, 13:00:05 UTC | Simplify Makefile by moving custom options out of Makefile into individual files inside vale directory | 05 September 2019, 13:00:05 UTC |
b8e3da5 | Dzomo the everest Yak | 05 September 2019, 08:29:03 UTC | [CI] regenerate hints | 05 September 2019, 08:29:03 UTC |
90008dd | Chris Hawblitzel | 04 September 2019, 20:33:41 UTC | Don't say "friend Vale.Arch.BufferFriend", because that transitively friends many other modules and greatly slows verification | 04 September 2019, 20:33:41 UTC |
1ac2ff9 | Chris Hawblitzel | 04 September 2019, 18:35:11 UTC | Merge branch 'fstar-master' into _vale_heap | 04 September 2019, 18:35:11 UTC |
4caa04f | Chris Hawblitzel | 04 September 2019, 18:26:05 UTC | Add unfolded view_n to make verification of "% view_n t" faster | 04 September 2019, 18:26:05 UTC |
6beadeb | Dzomo the everest Yak | 04 September 2019, 08:26:51 UTC | [CI] regenerate hints | 04 September 2019, 08:26:51 UTC |
cc61acf | Dzomo the everest Yak | 03 September 2019, 08:30:38 UTC | [CI] regenerate hints | 03 September 2019, 08:30:38 UTC |
d846520 | Dzomo the everest Yak | 02 September 2019, 08:27:29 UTC | [CI] regenerate hints | 02 September 2019, 08:27:29 UTC |
f919215 | Dzomo the everest Yak | 01 September 2019, 08:27:12 UTC | [CI] regenerate hints | 01 September 2019, 08:27:12 UTC |
9564cbc | Dzomo the everest Yak | 31 August 2019, 08:27:37 UTC | [CI] regenerate hints | 31 August 2019, 08:27:37 UTC |
6db4efc | Chris Hawblitzel | 30 August 2019, 21:37:52 UTC | Simplify Vale.Arch.Heap slightly | 30 August 2019, 21:37:52 UTC |
3040331 | Chris Hawblitzel | 30 August 2019, 18:00:11 UTC | Bring vale_state and machine_state closer together. Rather than considering vale_state and machine_state to be fundamentally different, treat them as two interchangeable views of the same underlying data (except for ms_trace, which only exists in machine_state). For example, there are now functions that convert back and forth between the two views and a round-trip lemma "lemma_to_of" that goes from machine_state to vale_state back to machine_state. The major change is that machine_state and vale_state now share the same heap type (Vale.Arch.Heap.heap_impl == Vale.Arch.HeapImpl.vale_heap_impl). | 30 August 2019, 18:00:11 UTC |
e660623 | Dzomo the everest Yak | 30 August 2019, 08:27:27 UTC | [CI] regenerate hints | 30 August 2019, 08:27:27 UTC |
0318dd9 | Dzomo the everest Yak | 29 August 2019, 08:29:36 UTC | [CI] regenerate hints | 29 August 2019, 08:29:36 UTC |
c7c22bd | Dzomo the everest Yak | 27 August 2019, 08:28:05 UTC | [CI] regenerate hints | 27 August 2019, 08:28:05 UTC |
7128ba5 | Dzomo the everest Yak | 26 August 2019, 08:27:30 UTC | [CI] regenerate hints | 26 August 2019, 08:27:30 UTC |
926528e | Dzomo the everest Yak | 25 August 2019, 08:28:02 UTC | [CI] regenerate hints | 25 August 2019, 08:28:02 UTC |
df8f424 | Dzomo the everest Yak | 24 August 2019, 08:26:24 UTC | [CI] regenerate hints | 24 August 2019, 08:26:24 UTC |
5c1ba25 | Dzomo the everest Yak | 23 August 2019, 08:27:21 UTC | [CI] regenerate hints | 23 August 2019, 08:27:21 UTC |
37c3310 | Dzomo the everest Yak | 22 August 2019, 08:27:24 UTC | [CI] regenerate hints | 22 August 2019, 08:27:24 UTC |
8c0f34a | Jonathan Protzenko | 21 August 2019, 12:15:04 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 21 August 2019, 12:15:04 UTC |
1ee04f2 | Jonathan Protzenko | 21 August 2019, 09:42:10 UTC | Also lift the length restriction for HKDF | 21 August 2019, 09:42:10 UTC |
00e7770 | Jonathan Protzenko | 21 August 2019, 09:36:21 UTC | Lift restriction on input length for HMAC | 21 August 2019, 09:36:21 UTC |
7af0972 | Dzomo the everest Yak | 21 August 2019, 08:27:21 UTC | [CI] regenerate hints | 21 August 2019, 08:27:21 UTC |
414118e | Santiago Zanella-Beguelin | 20 August 2019, 09:19:51 UTC | Merge branch 'santiago_merkle' into fstar-master | 20 August 2019, 09:19:51 UTC |
b8d4d15 | Jonathan Protzenko | 20 August 2019, 08:03:21 UTC | Deeply rooted evil bug. ocamldep generated an entry with a backslash which from the GNU make point of view was a different production | 20 August 2019, 08:03:21 UTC |
5e0e44a | Santiago Zanella-Beguelin | 19 August 2019, 23:12:26 UTC | Simplify sequence comparison | 19 August 2019, 23:12:26 UTC |
14182d1 | Santiago Zanella-Beguelin | 19 August 2019, 23:11:00 UTC | Fixed one-char typo in MD5 specification: logxor -> logor | 19 August 2019, 23:11:00 UTC |
d50718d | Santiago Zanella-Beguelin | 19 August 2019, 18:24:49 UTC | Hints | 19 August 2019, 18:24:49 UTC |
70a824b | Santiago Zanella-Beguelin | 19 August 2019, 18:24:18 UTC | Non-constant time comparison alternative | 19 August 2019, 18:24:18 UTC |
a3e0a96 | Santiago Zanella-Beguelin | 19 August 2019, 16:53:21 UTC | Hints | 19 August 2019, 16:53:21 UTC |
1dc9a98 | Santiago Zanella-Beguelin | 19 August 2019, 16:13:23 UTC | Get rid of annoying warning | 19 August 2019, 16:13:23 UTC |
73ec644 | Santiago Zanella-Beguelin | 19 August 2019, 16:12:51 UTC | Port MerkleTree to new EverCrypt hash using Lib.IntTypes | 19 August 2019, 16:12:51 UTC |
8f64795 | Santiago Zanella-Beguelin | 19 August 2019, 16:11:09 UTC | Lib.RawBuffer module implementing blit from public to secret bytes | 19 August 2019, 16:11:09 UTC |
8c7762a | Chris Hawblitzel | 19 August 2019, 15:41:40 UTC | Use balanced binary search tree for taints in Vale.X64.Leakage | 19 August 2019, 15:41:40 UTC |
05ce38f | Dzomo the everest Yak | 19 August 2019, 08:27:11 UTC | [CI] regenerate hints | 19 August 2019, 08:27:11 UTC |
736d4df | Dzomo the everest Yak | 18 August 2019, 08:27:05 UTC | [CI] regenerate hints | 18 August 2019, 08:27:05 UTC |
a7f9fdd | Dzomo the everest Yak | 17 August 2019, 08:28:07 UTC | [CI] regenerate hints | 17 August 2019, 08:28:07 UTC |
463a2c2 | Aymeric Fromherz | 16 August 2019, 20:45:30 UTC | Update poly semiring tactic wrt F* master | 16 August 2019, 20:45:30 UTC |
d9948ca | Aymeric Fromherz | 16 August 2019, 20:38:39 UTC | rlimits | 16 August 2019, 20:38:39 UTC |
0dcabce | Aymeric Fromherz | 16 August 2019, 18:47:00 UTC | Start addressing Santiago's comments | 16 August 2019, 18:47:00 UTC |
3676f21 | Aymeric Fromherz | 16 August 2019, 17:38:37 UTC | Fix flaky Spec.BignumQ.Lemmas proof | 16 August 2019, 17:38:37 UTC |
726a060 | Santiago Zanella-Beguelin | 16 August 2019, 17:30:48 UTC | Simplify proofs | 16 August 2019, 17:30:48 UTC |
5e37959 | Jonathan Protzenko | 16 August 2019, 15:07:13 UTC | one last fix | 16 August 2019, 15:07:13 UTC |
d00bce5 | Jonathan Protzenko | 16 August 2019, 13:36:57 UTC | Try fix | 16 August 2019, 13:36:57 UTC |
b89225b | Jonathan Protzenko | 16 August 2019, 13:00:12 UTC | Merge remote-tracking branch 'origin/santiago_fix' into fstar-master | 16 August 2019, 13:00:12 UTC |
c5827ab | Santiago Zanella-Beguelin | 16 August 2019, 12:58:33 UTC | Use canon_semiring instead of canon_semiring_with | 16 August 2019, 12:58:33 UTC |
6d9599e | Jonathan Protzenko | 16 August 2019, 12:15:47 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 16 August 2019, 12:15:47 UTC |
71ea08a | Jonathan Protzenko | 16 August 2019, 12:15:23 UTC | Cleanup the bundle variables in the Makefile and add a Mozilla distribution | 16 August 2019, 12:15:23 UTC |
1bea24d | Jonathan Protzenko | 16 August 2019, 12:14:55 UTC | hints | 16 August 2019, 12:14:55 UTC |
500f2ab | Dzomo the everest Yak | 16 August 2019, 08:27:09 UTC | [CI] regenerate hints | 16 August 2019, 08:27:09 UTC |
5ec25bb | Aymeric Fromherz | 16 August 2019, 05:15:34 UTC | Merge branch 'fstar-master' into afromher_ed | 16 August 2019, 05:15:34 UTC |
82e1aed | Aymeric Fromherz | 16 August 2019, 03:16:32 UTC | Work towards merkle trees | 16 August 2019, 03:16:32 UTC |
2ea5339 | Chris Hawblitzel | 16 August 2019, 02:28:17 UTC | Add small SymCrypt example and make fast_sqr_part2 verify faster | 16 August 2019, 02:28:17 UTC |
dc2f5b7 | Aymeric Fromherz | 15 August 2019, 21:25:17 UTC | Merge branch 'fstar-master' into afromher_ed | 15 August 2019, 21:25:17 UTC |
187617f | Aymeric Fromherz | 15 August 2019, 21:17:04 UTC | Fix gcmencryptOpt interop | 15 August 2019, 21:17:04 UTC |
b187043 | Santiago Zanella-Beguelin | 15 August 2019, 16:46:25 UTC | Trying with fuel = 0 | 15 August 2019, 17:00:21 UTC |
0525b55 | Santiago Zanella-Beguelin | 15 August 2019, 14:34:43 UTC | Tighter modifies clause and reduced ifuel for fast_sqr_part2 | 15 August 2019, 14:34:43 UTC |
caaee96 | Dzomo the everest Yak | 14 August 2019, 12:21:12 UTC | [CI] regenerate hints | 14 August 2019, 12:21:12 UTC |
345754c | Santiago Zanella-Beguelin | 14 August 2019, 11:50:09 UTC | Merge pull request #183 from project-everest/santiago_hints BuildHints- workflow | 14 August 2019, 11:50:09 UTC |
4ce06f9 | Dzomo the everest Yak | 14 August 2019, 10:33:57 UTC | [CI] regenerate hints | 14 August 2019, 10:33:57 UTC |
bf0fa99 | Santiago Zanella-Beguelin | 14 August 2019, 09:56:34 UTC | Refresh hints through BuildHints- pipeline | 14 August 2019, 09:56:34 UTC |
b2c12e3 | Santiago Zanella-Beguelin | 13 August 2019, 21:51:11 UTC | Merge pull request #182 from project-everest/santiago_ring Port to FStar.Tactics.CanonCommSemiring in FStar@santiago_ring | 13 August 2019, 21:51:11 UTC |
eb81734 | Santiago Zanella-Beguelin | 13 August 2019, 17:34:14 UTC | Merge branch 'fstar-master' into santiago_ring | 13 August 2019, 17:34:14 UTC |
568dfc7 | Santiago Zanella-Beguelin | 13 August 2019, 14:41:33 UTC | Simplify lemma | 13 August 2019, 14:41:33 UTC |
ea0bdef | Santiago Zanella-Beguelin | 13 August 2019, 13:20:30 UTC | Unfold definitions before canon_semiring; the previous tactic unfolded them unintendedly | 13 August 2019, 13:20:30 UTC |
6b770c1 | Jonathan Protzenko | 13 August 2019, 12:26:36 UTC | Kick CI | 13 August 2019, 12:26:36 UTC |
54a1b6c | Jonathan Protzenko | 13 August 2019, 12:06:37 UTC | Try a different fix | 13 August 2019, 12:06:37 UTC |
86709dd | Jonathan Protzenko | 13 August 2019, 09:40:56 UTC | Update Changelog | 13 August 2019, 09:40:56 UTC |
6c65aef | Jonathan Protzenko | 13 August 2019, 09:32:32 UTC | Missing LDFLAGS when creating the OCaml library | 13 August 2019, 09:32:32 UTC |
c0e3933 | Jonathan Protzenko | 13 August 2019, 09:21:33 UTC | OSX fixes | 13 August 2019, 09:21:33 UTC |
bd407a6 | Aymeric Fromherz | 13 August 2019, 07:17:02 UTC | Fix Sha interop | 13 August 2019, 07:17:02 UTC |
118b12f | Aymeric Fromherz | 13 August 2019, 05:53:42 UTC | Restore tests + hints | 13 August 2019, 05:53:42 UTC |
43ee2c3 | Aymeric Fromherz | 13 August 2019, 05:36:21 UTC | Restore evercrypt.hkdf, hmac, and hash.incremental | 13 August 2019, 05:36:21 UTC |
326ab6d | Aymeric Fromherz | 13 August 2019, 05:35:57 UTC | Better bound on size of data for hmac/hkdf | 13 August 2019, 05:35:57 UTC |
921e2d4 | Aymeric Fromherz | 13 August 2019, 05:12:55 UTC | Reprove Sha_helpers | 13 August 2019, 05:12:55 UTC |
f500ecd | Aymeric Fromherz | 13 August 2019, 04:49:17 UTC | More work towards inttypes for hashes | 13 August 2019, 04:49:17 UTC |
118c8de | Santiago Zanella-Beguelin | 12 August 2019, 14:16:19 UTC | Revert unintentional change | 12 August 2019, 14:16:19 UTC |
ad4a916 | Santiago Zanella-Beguelin | 12 August 2019, 11:03:50 UTC | Poly1305 lemmas using new semiring tactic from FStar@santiago_ring | 12 August 2019, 11:03:50 UTC |
4bede34 | Jonathan Protzenko | 12 August 2019, 07:06:50 UTC | hints | 12 August 2019, 07:06:50 UTC |
95c3246 | Aymeric Fromherz | 10 August 2019, 06:51:19 UTC | IntTypes for hash implementations | 10 August 2019, 06:51:19 UTC |
8d8b46e | Aymeric Fromherz | 10 August 2019, 01:42:25 UTC | more inttypes | 10 August 2019, 01:42:25 UTC |
041bff2 | Aymeric Fromherz | 09 August 2019, 22:49:08 UTC | Finish updating specs + Start updating code/hash | 09 August 2019, 22:49:08 UTC |
97e9890 | Tahina Ramananandro (professional account) | 09 August 2019, 19:55:17 UTC | Merge pull request #181 from project-everest/taramana_aead Stronger postconditions for AEAD: freeable, as_kv, g_is_null... | 09 August 2019, 19:55:17 UTC |
cc4b3e2 | Aymeric Fromherz | 09 August 2019, 18:45:53 UTC | More specs modifications towards lib.inttypes for hashes | 09 August 2019, 18:45:53 UTC |
76cb65f | Jonathan Protzenko | 09 August 2019, 18:45:23 UTC | Merge branch 'fstar-master' into taramana_aead | 09 August 2019, 18:45:23 UTC |
40797b3 | Jonathan Protzenko | 09 August 2019, 17:57:48 UTC | Merge remote-tracking branch 'origin/fstar-master' into polubelova_ci | 09 August 2019, 17:57:48 UTC |
542c702 | Tahina Ramananandro | 09 August 2019, 16:00:02 UTC | AEAD: preserve freeable, as_kv | 09 August 2019, 16:00:02 UTC |
6fea52a | Marina Polubelova | 09 August 2019, 14:18:44 UTC | hints | 09 August 2019, 14:18:44 UTC |
60b2e78 | Marina Polubelova | 09 August 2019, 14:16:49 UTC | copy nacl-box from _dev | 09 August 2019, 14:16:49 UTC |
31b311d | Marina Polubelova | 09 August 2019, 13:19:37 UTC | hints | 09 August 2019, 13:19:37 UTC |
87aa585 | Marina Polubelova | 09 August 2019, 13:18:47 UTC | copy salsa20 from _dev | 09 August 2019, 13:18:47 UTC |
06157f7 | Aymeric Fromherz | 09 August 2019, 06:15:22 UTC | Start reviving Karthik's work on using IntTypes in hashes | 09 August 2019, 06:15:22 UTC |
cf42634 | Jonathan Protzenko | 08 August 2019, 20:36:38 UTC | Merge remote-tracking branch 'origin/fstar-master' into polubelova_ci | 08 August 2019, 20:36:38 UTC |
03e6ced | Marina Polubelova | 08 August 2019, 18:53:30 UTC | hints | 08 August 2019, 18:53:30 UTC |
4441eac | Marina Polubelova | 08 August 2019, 18:50:50 UTC | update poly1305 | 08 August 2019, 18:50:50 UTC |
24c8b13 | Jonathan Protzenko | 08 August 2019, 18:37:54 UTC | Merge pull request #180 from project-everest/polubelova_ci Refresh in-tree versions of curve25519 | 08 August 2019, 18:37:54 UTC |
bdf3d14 | Marina Polubelova | 08 August 2019, 10:53:27 UTC | hints | 08 August 2019, 10:53:27 UTC |
5c971bb | Marina Polubelova | 08 August 2019, 10:50:16 UTC | update curve25519 | 08 August 2019, 10:50:16 UTC |