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