| 01a2b16 | Son HO | 04 March 2020, 16:14:54 UTC | Add a refinement on the type of from_string | 04 March 2020, 16:14:54 UTC |
| a798ee5 | Son HO | 04 March 2020, 15:41:32 UTC | Remove the admit from Lib.StringSequence.fst | 04 March 2020, 15:41:32 UTC |
| 2551235 | Marina Polubelova | 02 February 2020, 16:53:05 UTC | fix preconditions for ctr_equivalence | 02 February 2020, 16:53:05 UTC |
| 7ce67bc | Marina Polubelova | 02 February 2020, 16:36:50 UTC | update spec equiv proof of poly | 02 February 2020, 16:36:50 UTC |
| 6e6dc65 | Marina Polubelova | 02 February 2020, 14:52:33 UTC | update spec equiv proof of ctr | 02 February 2020, 14:52:33 UTC |
| adea233 | Marina Polubelova | 02 February 2020, 14:29:34 UTC | update spec equiv proof of gf128 | 02 February 2020, 14:29:34 UTC |
| 94e8965 | Marina Polubelova | 02 February 2020, 14:24:44 UTC | Merge branch 'polubelova_ci' into _dev | 02 February 2020, 14:24:44 UTC |
| 593571a | Marina Polubelova | 02 February 2020, 13:34:25 UTC | checkout Spec.Agile.AEAD.fsti from _dev | 02 February 2020, 13:34:25 UTC |
| 774ae94 | Marina Polubelova | 02 February 2020, 12:46:37 UTC | Merge remote-tracking branch 'origin/master' into _dev_merge_master | 02 February 2020, 12:46:37 UTC |
| 52afcf1 | Marina Polubelova | 02 February 2020, 12:24:34 UTC | reset hints and dist | 02 February 2020, 12:24:34 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 |
| 17fc958 | Marina Polubelova | 31 January 2020, 15:08:06 UTC | Merge branch 'master' into polubelova_ci | 31 January 2020, 15:08:06 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 |
| aeabd02 | Marina Polubelova | 30 January 2020, 13:11:23 UTC | fix ci? | 30 January 2020, 13:11:23 UTC |
| 806b253 | Marina Polubelova | 30 January 2020, 10:50:25 UTC | Merge remote-tracking branch 'origin/master' into polubelova_ci | 30 January 2020, 10:50:25 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 |
| ccb36b2 | Marina Polubelova | 29 January 2020, 23:06:32 UTC | hints | 29 January 2020, 23:06:32 UTC |
| a6a52ac | Marina Polubelova | 29 January 2020, 23:05:57 UTC | bump rlimit | 29 January 2020, 23:05:57 UTC |
| e873802 | Marina Polubelova | 29 January 2020, 22:00:42 UTC | Merge remote-tracking branch 'origin/master' into polubelova_ci | 29 January 2020, 22:00:42 UTC |
| 26b4e0a | Marina Polubelova | 29 January 2020, 21:59:19 UTC | reset hints and dist | 29 January 2020, 21:59:19 UTC |
| d3ce03a | Marina Polubelova | 29 January 2020, 21:50:28 UTC | simplify preconditions for repeat_blocks_multi_vec lemma | 29 January 2020, 21:50:28 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 |
| 0bfc61b | Marina Polubelova | 26 January 2020, 13:28:11 UTC | hints | 26 January 2020, 13:28:11 UTC |
| 36d6c0e | Marina Polubelova | 26 January 2020, 13:27:45 UTC | add map_blocks_ctr_vec lemma | 26 January 2020, 13:27:45 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 |
| 6206b65 | Marina Polubelova | 23 January 2020, 13:31:22 UTC | hints | 23 January 2020, 13:31:22 UTC |
| f32fdf1 | Marina Polubelova | 23 January 2020, 13:30:46 UTC | simplify preconditions for lemma_map_blocks_multi_vec | 23 January 2020, 13:30:46 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 |
