7b9dcb7 | Nikhil Swamy | 26 September 2019, 04:09:27 UTC | switch back to using F* master | 26 September 2019, 04:09:27 UTC |
05638d1 | Nikhil Swamy | 25 September 2019, 04:43:54 UTC | tweak config.json to pick the nik_1566 branch of F* since that contains the ulib/.cache directory used in the makefile now | 25 September 2019, 04:43:54 UTC |
4b998af | Nikhil Swamy | 25 September 2019, 04:31:57 UTC | patching valedepend.py to look for .checked files in the include path; adding ulib/.cache to its include path | 25 September 2019, 04:31:57 UTC |
f869d29 | Nikhil Swamy | 25 September 2019, 03:40:13 UTC | a makefile tweak to deal with new check file locations | 25 September 2019, 03:40:13 UTC |
ec36290 | Guido MartÃnez | 24 September 2019, 16:18:37 UTC | Hacl.Impl.Poly1305: bump some rlimits | 24 September 2019, 16:43:01 UTC |
1fd1b76 | Dzomo the everest Yak | 22 September 2019, 08:26:25 UTC | [CI] regenerate hints | 22 September 2019, 08:26:25 UTC |
429ad03 | Dzomo the everest Yak | 21 September 2019, 08:26:39 UTC | [CI] regenerate hints | 21 September 2019, 08:26:39 UTC |
4211b64 | Aymeric Fromherz | 19 September 2019, 23:30:01 UTC | bump rlimit + Hints | 20 September 2019, 00:19:44 UTC |
f43215b | Aymeric Fromherz | 19 September 2019, 20:19:45 UTC | Rename Spec.{Hash, HMAC, HKDF} to Spec.Agile.{..} | 19 September 2019, 20:19:45 UTC |
c86ae22 | Aymeric Fromherz | 19 September 2019, 19:09:24 UTC | Use <= instead of < for hash specs | 19 September 2019, 19:09:24 UTC |
a447e5c | Dzomo the everest Yak | 18 September 2019, 08:26:11 UTC | [CI] regenerate hints | 18 September 2019, 08:26:11 UTC |
8dd4105 | Dzomo the everest Yak | 17 September 2019, 08:26:11 UTC | [CI] regenerate hints | 17 September 2019, 08:26:11 UTC |
d7b1997 | Guido MartÃnez | 16 September 2019, 19:33:56 UTC | bump an rlimit | 16 September 2019, 19:33:56 UTC |
4ecb6b8 | Dzomo the everest Yak | 15 September 2019, 08:26:08 UTC | [CI] regenerate hints | 15 September 2019, 08:26:08 UTC |
542f8f4 | Dzomo the everest Yak | 14 September 2019, 08:26:31 UTC | [CI] regenerate hints | 14 September 2019, 08:26:31 UTC |
2223824 | Dzomo the everest Yak | 13 September 2019, 08:28:14 UTC | [CI] regenerate hints | 13 September 2019, 08:28:14 UTC |
e881372 | Nikhil Swamy | 13 September 2019, 03:50:57 UTC | Merge remote-tracking branch 'origin/nik_erasable' into fstar-master | 13 September 2019, 03:50:57 UTC |
c213271 | Nikhil Swamy | 12 September 2019, 22:01:30 UTC | enabling nl arith in a wrapper proof | 12 September 2019, 22:01:30 UTC |
88c983a | Dzomo the everest Yak | 12 September 2019, 08:27:18 UTC | [CI] regenerate hints | 12 September 2019, 08:27:18 UTC |
c25ec5e | Dzomo the everest Yak | 11 September 2019, 08:27:03 UTC | [CI] regenerate hints | 11 September 2019, 08:27:03 UTC |
ae15f16 | Dzomo the everest Yak | 10 September 2019, 09:38:59 UTC | [CI] regenerate hints | 10 September 2019, 09:38:59 UTC |
4d370d9 | Dzomo the everest Yak | 09 September 2019, 08:27:20 UTC | [CI] regenerate hints | 09 September 2019, 08:27:20 UTC |
8f9dcfb | Dzomo the everest Yak | 08 September 2019, 08:27:24 UTC | [CI] regenerate hints | 08 September 2019, 08:27:24 UTC |
dc0d7ad | Dzomo the everest Yak | 07 September 2019, 08:28:19 UTC | [CI] regenerate hints | 07 September 2019, 08:28:19 UTC |
6831bc6 | Chris Hawblitzel | 06 September 2019, 23:18:03 UTC | Restore "--use_extracted_interfaces true" to vale directories | 06 September 2019, 23:18:03 UTC |
0b19c5a | Dzomo the everest Yak | 06 September 2019, 08:31:12 UTC | [CI] regenerate hints | 06 September 2019, 08:31:12 UTC |
32a0666 | Chris Hawblitzel | 05 September 2019, 23:51:37 UTC | Add "open FStar.Mul" to every fst/fsti file in vale/ | 05 September 2019, 23:51:37 UTC |
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 |