| 3f48d4b | Chris Hawblitzel | 03 February 2020, 19:02:57 UTC | Merge branch 'master' into vale | 03 February 2020, 19:02:57 UTC |
| 48286ae | Jonathan Protzenko | 03 February 2020, 16:46:50 UTC | typo | 03 February 2020, 16:46:50 UTC |
| bc7378f | Dzomo the everest Yak | 03 February 2020, 08:19:57 UTC | [CI] regenerate hints and dist | 03 February 2020, 08:19:57 UTC |
| 240c0cc | Dzomo the everest Yak | 02 February 2020, 08:19:38 UTC | [CI] regenerate hints and dist | 02 February 2020, 08:19:38 UTC |
| 3f27a5e | Dzomo the everest Yak | 01 February 2020, 08:20:14 UTC | [CI] regenerate hints and dist | 01 February 2020, 08:20:14 UTC |
| bbd729f | Chris Hawblitzel | 01 February 2020, 02:36:29 UTC | Merge branch 'master' into vale | 01 February 2020, 02:36:29 UTC |
| a99113d | Jonathan Protzenko | 31 January 2020, 13:00:57 UTC | Don't corrupt the .git folder with sed? | 31 January 2020, 13:00:57 UTC |
| 1dc8cf6 | Dzomo the everest Yak | 31 January 2020, 08:19:44 UTC | [CI] regenerate hints and dist | 31 January 2020, 08:19:44 UTC |
| d6b2687 | Jonathan Protzenko | 30 January 2020, 22:04:26 UTC | Refresh documentation on hacl-star.github.io | 30 January 2020, 22:04:26 UTC |
| 4cad23b | Dzomo the everest Yak | 30 January 2020, 08:23:33 UTC | [CI] regenerate hints and dist | 30 January 2020, 08:23:33 UTC |
| 6d5b80e | Dzomo the everest Yak | 29 January 2020, 08:19:55 UTC | [CI] regenerate hints and dist | 29 January 2020, 08:19:55 UTC |
| a60fb65 | Chris Hawblitzel | 28 January 2020, 16:29:48 UTC | Fix formatting that broke during merge | 28 January 2020, 16:29:48 UTC |
| 8ae42d4 | Dzomo the everest Yak | 28 January 2020, 08:23:37 UTC | [CI] regenerate hints and dist | 28 January 2020, 08:23:37 UTC |
| 14dcfb1 | Chris Hawblitzel | 28 January 2020, 04:51:00 UTC | Update Vale version | 28 January 2020, 04:51:00 UTC |
| ea0eddd | Chris Hawblitzel | 28 January 2020, 02:45:40 UTC | Merge branch 'master' into _vale_heap_record | 28 January 2020, 02:45:40 UTC |
| 24797c9 | Dzomo the everest Yak | 26 January 2020, 08:22:07 UTC | [CI] regenerate hints and dist | 26 January 2020, 08:22:07 UTC |
| ba63701 | Dzomo the everest Yak | 24 January 2020, 08:21:16 UTC | [CI] regenerate hints and dist | 24 January 2020, 08:21:16 UTC |
| 0aa21df | Chris Hawblitzel | 24 January 2020, 00:17:08 UTC | Restore code in Vale.AES.X64.AESCTR | 24 January 2020, 00:17:08 UTC |
| d7de00c | Santiago Zanella-Beguelin | 23 January 2020, 15:08:35 UTC | Merge pull request #224 from project-everest/protz_ci Fix specs Makefile | 23 January 2020, 15:08:35 UTC |
| 29a5a66 | Santiago Zanella-Beguelin | 23 January 2020, 14:07:45 UTC | Merge branch 'master' into protz_ci | 23 January 2020, 14:07:45 UTC |
| 48b3eb1 | Dzomo the everest Yak | 23 January 2020, 08:20:02 UTC | [CI] regenerate hints and dist | 23 January 2020, 08:20:02 UTC |
| c46d667 | Chris Hawblitzel | 23 January 2020, 05:15:47 UTC | Use heaplets in Vale AES-GCM | 23 January 2020, 05:15:47 UTC |
| c7b19c1 | Jonathan Protzenko | 22 January 2020, 13:57:27 UTC | Also enforce gmake for local makefiles | 22 January 2020, 13:57:27 UTC |
| e3b5828 | Jonathan Protzenko | 22 January 2020, 13:55:11 UTC | Fix specs Makefile | 22 January 2020, 13:55:11 UTC |
| 7e5f32a | Dzomo the everest Yak | 22 January 2020, 08:20:33 UTC | [CI] regenerate hints and dist | 22 January 2020, 08:20:33 UTC |
| 7521ad9 | Aymeric Fromherz | 22 January 2020, 03:49:29 UTC | Add precision regarding constraint on scalar inside Vale fmul inline asm | 22 January 2020, 03:49:29 UTC |
| f6d2a4d | Chris Hawblitzel | 22 January 2020, 02:27:55 UTC | In Vale.Poly1305.X64, use heap0 for readonly buffer and heap1 for mutable buffer | 22 January 2020, 02:27:55 UTC |
| 35dbb11 | Chris Hawblitzel | 22 January 2020, 02:10:50 UTC | Remove redundant postconditions from Vale Store procedures (postconditions were already implied by buffer_write properties) | 22 January 2020, 02:10:50 UTC |
| ddf7896 | Dzomo the everest Yak | 21 January 2020, 08:21:14 UTC | [CI] regenerate hints and dist | 21 January 2020, 08:21:14 UTC |
| 2219f17 | Chris Hawblitzel | 21 January 2020, 05:55:25 UTC | Clean up some Vale memory definitions | 21 January 2020, 05:55:25 UTC |
| 66b1a8b | Chris Hawblitzel | 21 January 2020, 02:15:51 UTC | Create all 16 Vale heaplets | 21 January 2020, 02:15:51 UTC |
| dd3e7f9 | Chris Hawblitzel | 20 January 2020, 22:36:20 UTC | Prove that heap updates maintain Vale heaplet invariants | 20 January 2020, 22:36:20 UTC |
| edd3aab | Chris Hawblitzel | 20 January 2020, 21:34:25 UTC | Rename some functions in Vale.Arch.MachineHeap | 20 January 2020, 21:34:25 UTC |
| 63c5bb2 | Aymeric Fromherz | 20 January 2020, 20:28:30 UTC | Merge pull request #219 from project-everest/afromher_nicer_asm Nicer inline assembly generation for Curve procedures | 20 January 2020, 20:28:30 UTC |
| 8107081 | Aymeric Fromherz | 20 January 2020, 19:47:03 UTC | Merge branch 'master' into afromher_nicer_asm | 20 January 2020, 19:47:03 UTC |
| d3bbb2f | Aymeric Fromherz | 20 January 2020, 19:45:50 UTC | Clean dist/ | 20 January 2020, 19:45:50 UTC |
| 7110038 | Dzomo the everest Yak | 20 January 2020, 08:19:59 UTC | [CI] regenerate hints and dist | 20 January 2020, 08:19:59 UTC |
| 1150255 | Chris Hawblitzel | 20 January 2020, 05:26:08 UTC | Remove vale_heap_data_eq from requires/ensures | 20 January 2020, 05:26:08 UTC |
| 2cf46f6 | Chris Hawblitzel | 20 January 2020, 03:27:30 UTC | Add heaplet argument to Vale loads, stores | 20 January 2020, 03:27:30 UTC |
| 09852ad | Chris Hawblitzel | 19 January 2020, 20:07:32 UTC | Merge branch 'master' into _vale_heap_record | 19 January 2020, 20:07:32 UTC |
| 4ca1bc2 | Chris Hawblitzel | 19 January 2020, 15:06:06 UTC | Add requires/ensures to Vale CreateHeaplets/DestroyHeaplets, remove mem_eq_all | 19 January 2020, 15:06:06 UTC |
| a00a0ad | Dzomo the everest Yak | 19 January 2020, 08:19:07 UTC | [CI] regenerate hints and dist | 19 January 2020, 08:19:07 UTC |
| 5dc9a8d | Chris Hawblitzel | 18 January 2020, 23:13:44 UTC | Vale DestroyHeaplets now ensures modifies_mem | 18 January 2020, 23:13:44 UTC |
| 50fe3ac | Aymeric Fromherz | 18 January 2020, 18:56:47 UTC | Hints + dist | 18 January 2020, 18:56:47 UTC |
| 2f3e4e9 | Aymeric Fromherz | 18 January 2020, 18:25:46 UTC | Merge branch 'master' into afromher_nicer_asm | 18 January 2020, 18:25:46 UTC |
| a9f14c2 | Chris Hawblitzel | 18 January 2020, 17:42:04 UTC | Refactor definition of vale_heap_layout_inner | 18 January 2020, 17:42:04 UTC |
| 72b67c0 | Chris Hawblitzel | 18 January 2020, 15:39:57 UTC | Add "modifies" invariant for Vale heaplets | 18 January 2020, 15:39:57 UTC |
| 845c47c | Dzomo the everest Yak | 18 January 2020, 08:19:21 UTC | [CI] regenerate hints and dist | 18 January 2020, 08:19:21 UTC |
| 121a662 | Chris Hawblitzel | 17 January 2020, 23:47:29 UTC | Establish valid_layout_buffer invariant for Vale buffers | 17 January 2020, 23:47:29 UTC |
| 995b5b4 | Chris Hawblitzel | 17 January 2020, 22:22:34 UTC | Call CreateHeaplets in all Vale code that uses the heap | 17 January 2020, 22:22:34 UTC |
| 8820123 | Aymeric Fromherz | 17 January 2020, 22:05:21 UTC | Merge branch 'master' into afromher_nicer_asm | 17 January 2020, 22:05:21 UTC |
| ec11b48 | Aymeric Fromherz | 17 January 2020, 22:00:01 UTC | Adding more tests for Vale inline asm printer | 17 January 2020, 22:00:01 UTC |
| 8d2ceb7 | Aymeric Fromherz | 17 January 2020, 21:18:54 UTC | Adding Vale inline printer tests to CI | 17 January 2020, 21:18:54 UTC |
| f4a8271 | Aymeric Fromherz | 17 January 2020, 20:51:08 UTC | Merge branch '_afromher_nicer_asm' into afromher_nicer_asm | 17 January 2020, 20:51:08 UTC |
| d16d18e | Aymeric Fromherz | 17 January 2020, 18:57:05 UTC | Make add1/add_scalar and fmul1/fmul_scalar names match for Linux distribution hack | 17 January 2020, 18:57:05 UTC |
| 42af4a8 | Chris Hawblitzel | 17 January 2020, 18:55:51 UTC | Revise Vale CreateHeaplets to take list of buffer_info | 17 January 2020, 18:55:51 UTC |
| 71f38f9 | Aymeric Fromherz | 17 January 2020, 18:46:10 UTC | Saner argument ordering for Vale inline fmul(2) and fsqr(2) | 17 January 2020, 18:46:10 UTC |
| caa8c23 | Aymeric Fromherz | 17 January 2020, 17:49:55 UTC | Merge branch '_afromher_test' into afromher_nicer_asm | 17 January 2020, 17:49:55 UTC |
| 4847588 | Aymeric Fromherz | 17 January 2020, 15:45:55 UTC | Clarify comment in cswap regarding handling of bit argument | 17 January 2020, 15:45:55 UTC |
| f46c7ef | Aymeric Fromherz | 17 January 2020, 15:40:55 UTC | Remove _inline from generated inline asm functions for Curve | 17 January 2020, 15:40:55 UTC |
| 33f6eaa | Aymeric Fromherz | 17 January 2020, 15:23:57 UTC | Start renaming of Curve asm: remove _inline from procedures names | 17 January 2020, 15:23:57 UTC |
| 8922d1b | Aymeric Fromherz | 17 January 2020, 12:41:25 UTC | Vale inline printer: Do not insert newline before asm volatile if there is not return var or explicit register allocation | 17 January 2020, 12:41:25 UTC |
| 53e2274 | Aymeric Fromherz | 17 January 2020, 02:54:02 UTC | Vale inline printer: explicitly allocated return values should have a value type, not a pointer type | 17 January 2020, 02:54:02 UTC |
| 95467d2 | Chris Hawblitzel | 16 January 2020, 19:33:19 UTC | Add more regression tests for Vale inline assembly printer | 16 January 2020, 19:33:19 UTC |
| 340f4cc | Chris Hawblitzel | 16 January 2020, 17:21:58 UTC | Fix regs_mod in regression test for Vale inline assembly printer | 16 January 2020, 17:21:58 UTC |
| 701ddb7 | Dzomo the everest Yak | 16 January 2020, 08:25:55 UTC | [CI] regenerate hints and dist | 16 January 2020, 08:25:55 UTC |
| f29ca7d | Chris Hawblitzel | 16 January 2020, 07:41:06 UTC | Slight cleanup for regression test for Vale inline assembly printer | 16 January 2020, 07:41:06 UTC |
| 3457c62 | Chris Hawblitzel | 16 January 2020, 07:30:44 UTC | Add an initial regression test for Vale inline assembly printer | 16 January 2020, 07:30:44 UTC |
| 47453f9 | Aymeric Fromherz | 15 January 2020, 23:16:24 UTC | More formatting of Curve inline assembly | 15 January 2020, 23:16:24 UTC |
| c132eb9 | Aymeric Fromherz | 15 January 2020, 21:24:42 UTC | Save a few instructions in inline fmul and fsqr by passing args in non-clobbered regs | 15 January 2020, 21:24:42 UTC |
| 1a56758 | Aymeric Fromherz | 15 January 2020, 20:52:43 UTC | Use open FStar.Mul in vale printers | 15 January 2020, 20:52:43 UTC |
| 23d45c1 | Jonathan Protzenko | 15 January 2020, 19:59:59 UTC | Merge branch 'master' into _doc_link | 15 January 2020, 19:59:59 UTC |
| afe8ef3 | Bryan Parno | 15 January 2020, 19:09:45 UTC | Replace doc source with a link to GitHub | 15 January 2020, 19:09:45 UTC |
| 7c03bfa | Jonathan Protzenko | 15 January 2020, 18:51:30 UTC | documentation automation | 15 January 2020, 18:51:30 UTC |
| 8232ba2 | Benjamin Beurdouche | 15 January 2020, 18:09:42 UTC | Merge pull request #217 from project-everest/karthikbhargavan-patch-1 Update README.md | 15 January 2020, 18:09:42 UTC |
| c220a5e | Benjamin Beurdouche | 15 January 2020, 16:47:18 UTC | Merge branch 'master' into karthikbhargavan-patch-1 | 15 January 2020, 16:47:18 UTC |
| 9fd7353 | Benjamin Beurdouche | 15 January 2020, 16:47:00 UTC | Merge pull request #220 from project-everest/beurdouche-patch-1 Update README.md | 15 January 2020, 16:47:00 UTC |
| c43d330 | Benjamin Beurdouche | 15 January 2020, 16:34:11 UTC | Merge branch 'master' into karthikbhargavan-patch-1 | 15 January 2020, 16:34:11 UTC |
| 553cf0e | Benjamin Beurdouche | 15 January 2020, 16:02:29 UTC | Update README.md | 15 January 2020, 16:02:29 UTC |
| 9398c62 | Benjamin Beurdouche | 15 January 2020, 16:01:25 UTC | Update README.md | 15 January 2020, 16:01:25 UTC |
| 415b000 | Jonathan Protzenko | 15 January 2020, 14:56:10 UTC | Fixup auto-refresh of documentation following Karthik's move from doc/reference to doc | 15 January 2020, 14:56:39 UTC |
| 868fd8d | Dzomo the everest Yak | 15 January 2020, 08:20:46 UTC | [CI] regenerate hints and dist | 15 January 2020, 08:20:46 UTC |
| 233d776 | Chris Hawblitzel | 15 January 2020, 06:00:48 UTC | Add valid_layout_buffer to Vale.X64.Decls memory predicates | 15 January 2020, 06:00:48 UTC |
| 04ec2f8 | Aymeric Fromherz | 14 January 2020, 23:49:21 UTC | Vale: Remove Noop node, use generic instructions for formatting instead | 14 January 2020, 23:49:21 UTC |
| aed1b8c | Jonathan Protzenko | 14 January 2020, 19:21:25 UTC | Better codegen for Linux | 14 January 2020, 19:21:25 UTC |
| 6542a99 | Jonathan Protzenko | 14 January 2020, 16:18:46 UTC | Merge remote-tracking branch 'origin/afromher_nicer_asm' | 14 January 2020, 16:18:46 UTC |
| 59248d3 | Jonathan Protzenko | 14 January 2020, 16:14:50 UTC | Merge remote-tracking branch 'origin/fstar-master' | 14 January 2020, 16:14:50 UTC |
| 1fcf185 | Chris Hawblitzel | 14 January 2020, 15:43:15 UTC | Add definitions of Vale heaplet initialization and invariants | 14 January 2020, 15:43:15 UTC |
| a0db260 | Dzomo the everest Yak | 14 January 2020, 08:19:32 UTC | [CI] regenerate hints and dist | 14 January 2020, 08:19:32 UTC |
| feb8a00 | Aymeric Fromherz | 14 January 2020, 04:20:39 UTC | Improve comments in add1 and fmul | 14 January 2020, 04:20:39 UTC |
| 271e07c | Aymeric Fromherz | 14 January 2020, 03:31:37 UTC | Add hints and generated files | 14 January 2020, 03:31:37 UTC |
| 26ca271 | Aymeric Fromherz | 14 January 2020, 03:31:29 UTC | Format add1 and fmul | 14 January 2020, 03:31:29 UTC |
| f6364fe | Aymeric Fromherz | 14 January 2020, 02:59:09 UTC | Vale: Add more formatting options for inline assembly | 14 January 2020, 02:59:09 UTC |
| 547d4ee | Aymeric Fromherz | 14 January 2020, 01:54:37 UTC | Vale: Refactor comment into a generic Noop instruction | 14 January 2020, 01:54:37 UTC |
| fc69743 | Aymeric Fromherz | 14 January 2020, 00:39:15 UTC | Semantically meaningful arg names for Vale inline asm | 14 January 2020, 00:39:15 UTC |
| 518f524 | Aymeric Fromherz | 14 January 2020, 00:11:16 UTC | Add procedure comments to Vale inline asm | 14 January 2020, 00:11:16 UTC |
| 41c8521 | Aymeric Fromherz | 13 January 2020, 23:59:51 UTC | Unify argument order in fmul, ... for extraction to Hacl_Curve25519_64 | 13 January 2020, 23:59:51 UTC |
| 71d4c58 | Aymeric Fromherz | 13 January 2020, 23:31:51 UTC | Vale inline asm: Minor cosmetic modifications | 13 January 2020, 23:31:51 UTC |
| 9d6cc5f | Aymeric Fromherz | 13 January 2020, 23:18:58 UTC | Vale inline asm: Use implicit allocation, except for registers implicitly used by code | 13 January 2020, 23:18:58 UTC |
| 086e79a | Dzomo the everest Yak | 13 January 2020, 08:19:44 UTC | [CI] regenerate hints and dist | 13 January 2020, 08:19:44 UTC |
