| 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 |
