| acc8d8e | Jay Bosamiya | 06 June 2019, 00:13:16 UTC | We want the value of a flag to be a [option bool] | 06 June 2019, 00:13:16 UTC |
| 8c7fa77 | Jay Bosamiya | 06 June 2019, 00:12:11 UTC | Introduce [flag] type to be a refinement on integers. Introduce aliases for carry and overflow flags. | 06 June 2019, 00:12:36 UTC |
| a0d15c1 | Chris Hawblitzel | 05 June 2019, 20:08:04 UTC | Increase z3rlimit in Hacl.Spec.Poly1305.Equiv | 05 June 2019, 20:08:04 UTC |
| a6d7e27 | Chris Hawblitzel | 05 June 2019, 17:58:05 UTC | Small z3rlimit changes for Z3 4.8.5 | 05 June 2019, 17:58:05 UTC |
| 820d22d | Jonathan Protzenko | 04 June 2019, 20:29:06 UTC | Eliminate duplicated terminology in favor of a single, arbitrary one | 04 June 2019, 20:29:06 UTC |
| e7f36a9 | Jonathan Protzenko | 04 June 2019, 20:28:47 UTC | hints | 04 June 2019, 20:28:47 UTC |
| 660994b | Jonathan Protzenko | 04 June 2019, 00:33:38 UTC | Minor tweak | 04 June 2019, 00:33:38 UTC |
| 31133eb | Jonathan Protzenko | 03 June 2019, 22:43:24 UTC | Resume work on EverCrypt.Hash.Incremental, while waiting to work on CTR | 03 June 2019, 22:43:24 UTC |
| f2706a7 | Jonathan Protzenko | 03 June 2019, 22:43:10 UTC | hints | 03 June 2019, 22:43:10 UTC |
| d39021d | Jonathan Protzenko | 03 June 2019, 21:21:23 UTC | Merge remote-tracking branch 'origin/protz_fstar_loop' into protz_ctr | 03 June 2019, 21:21:23 UTC |
| 8e08993 | Chris Hawblitzel | 01 June 2019, 21:03:13 UTC | Merge branch 'fstar-master' into _vale_generic | 01 June 2019, 21:03:13 UTC |
| 86ec68e | Chris Hawblitzel | 01 June 2019, 21:02:27 UTC | Rename state to vale_state | 01 June 2019, 21:02:27 UTC |
| 133c7d5 | Jonathan Protzenko | 01 June 2019, 03:40:36 UTC | Merge branch 'fstar-master' of pro.github.com:mitls/hacl-star into fstar-master | 01 June 2019, 03:40:36 UTC |
| a5229cd | Chris Hawblitzel | 01 June 2019, 01:40:36 UTC | Merge branch 'fstar-master' into _vale_generic | 01 June 2019, 01:40:36 UTC |
| b90d477 | Chris Hawblitzel | 01 June 2019, 01:36:03 UTC | Merge machine_eval_ins operations (including taint operations) into single pass | 01 June 2019, 01:36:03 UTC |
| fe2d4c7 | Jonathan Protzenko | 01 June 2019, 01:35:42 UTC | A more precise .depend invocation that will solve some broken builds but not all (see FStarLang/FStar#1657) | 01 June 2019, 01:35:42 UTC |
| b4a200d | Jonathan Protzenko | 01 June 2019, 01:34:56 UTC | hints | 01 June 2019, 01:34:56 UTC |
| 898df2e | Jonathan Protzenko | 31 May 2019, 20:17:15 UTC | Fix UTF-8 that got botched during Vale's mass-renaming | 31 May 2019, 20:17:15 UTC |
| ea2ecb6 | Jonathan Protzenko | 31 May 2019, 20:17:10 UTC | Disable benchmarking tests since i) failures to build or run them are not caught and ii) the cmake invocation fails under the conditions of the everest upgrade | 31 May 2019, 20:17:10 UTC |
| dd4877b | Chris Hawblitzel | 31 May 2019, 18:35:43 UTC | Merge branch 'fstar-master' into _vale_generic | 31 May 2019, 18:35:43 UTC |
| 0398ba4 | Chris Hawblitzel | 31 May 2019, 18:33:58 UTC | Share common operand type between operand64 and operand128 | 31 May 2019, 18:33:58 UTC |
| 52ffdad | Aymeric Fromherz | 30 May 2019, 15:15:34 UTC | Merge branch 'fstar-master' into afromher_readme | 30 May 2019, 15:15:34 UTC |
| 1033e42 | Aymeric Fromherz | 29 May 2019, 20:34:19 UTC | README: Update list of verified algorithms | 30 May 2019, 15:15:00 UTC |
| e516669 | Aymeric Fromherz | 29 May 2019, 20:28:25 UTC | README: Update list of algs supported | 30 May 2019, 15:15:00 UTC |
| c1ca708 | Chris Hawblitzel | 30 May 2019, 13:51:12 UTC | Merge branch 'fstar-master' into _vale_generic | 30 May 2019, 13:51:12 UTC |
| 84a3c95 | Christoph M. Wintersteiger | 30 May 2019, 12:21:20 UTC | Made gnuplot optional for benchmark runs. | 30 May 2019, 12:21:20 UTC |
| 9e03cd9 | Chris Hawblitzel | 30 May 2019, 05:53:56 UTC | Remove Vale.Lib.Workarounds | 30 May 2019, 05:53:56 UTC |
| 9267a83 | Chris Hawblitzel | 30 May 2019, 00:18:42 UTC | Update to latest Vale version and switch to --use_two_phase_tc true | 30 May 2019, 00:18:42 UTC |
| bf2f5f3 | Aymeric Fromherz | 29 May 2019, 20:34:19 UTC | README: Update list of verified algorithms | 29 May 2019, 20:34:19 UTC |
| 5dc2a04 | Aymeric Fromherz | 29 May 2019, 20:28:25 UTC | README: Update list of algs supported | 29 May 2019, 20:28:25 UTC |
| 5f823a9 | Christoph M. Wintersteiger | 29 May 2019, 15:49:33 UTC | Benchmarks build fix | 29 May 2019, 15:49:33 UTC |
| 2af50b3 | Christoph M. Wintersteiger | 29 May 2019, 14:23:17 UTC | Benchmark build fixes | 29 May 2019, 14:23:17 UTC |
| 7bd70bf | Christoph M. Wintersteiger | 28 May 2019, 14:50:56 UTC | Benchmark script tweaks | 28 May 2019, 14:51:04 UTC |
| 206b8d2 | Christoph M. Wintersteiger | 08 May 2019, 07:28:15 UTC | Fix benchmark CI makefile | 28 May 2019, 14:51:03 UTC |
| 28dc010 | Christoph M. Wintersteiger | 07 May 2019, 20:03:02 UTC | debug benchmarks in CI | 28 May 2019, 14:51:03 UTC |
| fbb5ed9 | Christoph M. Wintersteiger | 07 May 2019, 17:50:46 UTC | Fix directory search paths for benchmarks | 28 May 2019, 14:51:02 UTC |
| 2276f2b | Christoph M. Wintersteiger | 07 May 2019, 14:33:41 UTC | Benchmark script fixes | 28 May 2019, 14:51:02 UTC |
| 5466b57 | Christoph M. Wintersteiger | 07 May 2019, 14:32:04 UTC | Try CMake 3.5 for benchmarks | 28 May 2019, 14:51:01 UTC |
| f86de77 | Chris Hawblitzel | 25 May 2019, 13:10:54 UTC | Use allow_inversion even more in Leakage_Ins | 25 May 2019, 13:10:54 UTC |
| 086fa5f | Chris Hawblitzel | 25 May 2019, 00:28:26 UTC | Use allow_inversion in Leakage_Ins | 25 May 2019, 00:28:26 UTC |
| 60790c8 | Aymeric Fromherz | 23 May 2019, 22:02:08 UTC | Make cpuid constant time | 23 May 2019, 22:02:08 UTC |
| 18bbf23 | Aymeric Fromherz | 23 May 2019, 18:43:23 UTC | Fix OCaml extraction | 23 May 2019, 18:43:23 UTC |
| 6c4b104 | Aymeric Fromherz | 23 May 2019, 18:01:00 UTC | Return val for taint analysis | 23 May 2019, 18:01:00 UTC |
| 3642e32 | Aymeric Fromherz | 23 May 2019, 16:58:01 UTC | Taint analysis: Check that return value does not leak secrets | 23 May 2019, 16:58:01 UTC |
| a7ffc19 | Aymeric Fromherz | 22 May 2019, 17:37:35 UTC | Merge branch 'fstar-master' into afromher_run_taint | 22 May 2019, 17:37:35 UTC |
| 88a34d8 | Aymeric Fromherz | 22 May 2019, 17:37:02 UTC | Taint analysis: Only Rsp and the args are now public. Everything passes the analysis | 22 May 2019, 17:37:02 UTC |
| f254e30 | Aymeric Fromherz | 22 May 2019, 03:12:29 UTC | Secret stack instructions + Secret store/restore registers for gcm | 22 May 2019, 03:12:29 UTC |
| 83eef39 | Aymeric Fromherz | 21 May 2019, 23:15:43 UTC | Make xmm comparison constant time | 21 May 2019, 23:15:43 UTC |
| a47f71e | Santiago Zanella-Beguelin | 21 May 2019, 20:50:53 UTC | Add a portable distribution that uses -mtune=generic instead of -march=native -mtune=native | 21 May 2019, 20:50:53 UTC |
| 4ec808c | Aymeric Fromherz | 21 May 2019, 20:43:55 UTC | Reenable taint analysis at extraction | 21 May 2019, 20:43:55 UTC |
| e907c1f | Chris Hawblitzel | 19 May 2019, 13:11:22 UTC | Remove tab characters and trailing whitespace from files in vale directory | 19 May 2019, 13:11:22 UTC |
| 5f3f81d | Chris Hawblitzel | 18 May 2019, 23:58:09 UTC | Update hints | 18 May 2019, 23:58:09 UTC |
| a0b9e04 | Chris Hawblitzel | 18 May 2019, 19:59:58 UTC | Merge branch 'fstar-master' into _vale_generic | 18 May 2019, 19:59:58 UTC |
| f55b1f3 | Chris Hawblitzel | 18 May 2019, 19:00:44 UTC | Rename modules in vale directory | 18 May 2019, 19:00:44 UTC |
| 191a53c | Santiago Zanella-Beguelin | 16 May 2019, 16:32:52 UTC | Fix maximum length of ciphertext in Spec.AEAD.decrypt and state correctness lemma | 16 May 2019, 16:32:52 UTC |
| f2c8b60 | Chris Hawblitzel | 16 May 2019, 03:08:25 UTC | Merge Taint_Semantics_s into Bytes_Semantics_s, remove Taint_Semantics_s module | 16 May 2019, 03:08:25 UTC |
| ac19640 | Chris Hawblitzel | 15 May 2019, 23:17:37 UTC | Remove tainted_code and tainted_codes | 15 May 2019, 23:17:37 UTC |
| 954dc53 | Chris Hawblitzel | 15 May 2019, 22:43:38 UTC | Remove tainted_ocmp | 15 May 2019, 22:43:38 UTC |
| dbeb034 | Chris Hawblitzel | 15 May 2019, 18:52:31 UTC | Move taint to operands, and remove tainted_ins | 15 May 2019, 18:52:31 UTC |
| ebaa66c | Chris Hawblitzel | 14 May 2019, 22:58:15 UTC | Trace observations for both out and inout operands | 14 May 2019, 22:58:15 UTC |
| 5f5fc9d | Chris Hawblitzel | 14 May 2019, 17:16:48 UTC | Fix some Bytes_Semantics proofs | 14 May 2019, 17:16:48 UTC |
| 6c2afd3 | Chris Hawblitzel | 14 May 2019, 15:39:29 UTC | Merge branch 'fstar-master' into _vale_generic | 14 May 2019, 15:39:29 UTC |
| e89539f | Chris Hawblitzel | 14 May 2019, 15:37:27 UTC | Merge state and taintState into single type, machine_state | 14 May 2019, 15:37:27 UTC |
| 81620b1 | Aymeric Fromherz | 14 May 2019, 00:59:33 UTC | Merge branch 'fstar-master' into afromher_big_aesgcm | 14 May 2019, 00:59:33 UTC |
| 0423092 | Aymeric Fromherz | 14 May 2019, 00:58:50 UTC | Remove aesgcm length restriction from evercrypt | 14 May 2019, 00:58:50 UTC |
| d73eacf | Aymeric Fromherz | 14 May 2019, 00:43:52 UTC | Low* wrappers for relaxed aesgcm + hints | 14 May 2019, 00:43:52 UTC |
| a7ade35 | Aymeric Fromherz | 14 May 2019, 00:24:23 UTC | Remove restriction on length for optimised gcmencrypt | 14 May 2019, 00:24:23 UTC |
| 373cc75 | Aymeric Fromherz | 13 May 2019, 23:44:46 UTC | Remove restriction on length for optimised gcmdecrypt | 13 May 2019, 23:44:46 UTC |
| 324069f | Aymeric Fromherz | 13 May 2019, 20:22:19 UTC | Fix decrypt + hints | 13 May 2019, 20:22:19 UTC |
| 8525f15 | Aymeric Fromherz | 13 May 2019, 18:03:38 UTC | Fix optimised aes-gcm | 13 May 2019, 18:03:38 UTC |
| 8265630 | Aymeric Fromherz | 13 May 2019, 17:47:26 UTC | WIP: Relax length requirement for gcmencrypt/decrypt | 13 May 2019, 17:47:26 UTC |
| 1be3f76 | Chris Hawblitzel | 12 May 2019, 16:53:34 UTC | Change x64 reg type from datatype to integer type | 12 May 2019, 16:53:34 UTC |
| 9101826 | Chris Hawblitzel | 10 May 2019, 20:34:05 UTC | Merge branch 'fstar-master' into _vale_leakage | 10 May 2019, 20:34:05 UTC |
| cda4145 | Chris Hawblitzel | 10 May 2019, 19:34:29 UTC | Merge branch 'fstar-master' of https://github.com/project-everest/hacl-star into fstar-master | 10 May 2019, 19:34:29 UTC |
| c9f3915 | Chris Hawblitzel | 10 May 2019, 19:32:15 UTC | In Makefile, make FSTAR_NO_FLAGS and PYTHON3 configurable | 10 May 2019, 19:32:15 UTC |
| f247528 | Chris Hawblitzel | 10 May 2019, 18:02:31 UTC | Merge branch 'fstar-master' into _vale_leakage | 10 May 2019, 18:02:31 UTC |
| cb75580 | Jonathan Protzenko | 10 May 2019, 16:50:54 UTC | More customizations for CCF | 10 May 2019, 16:50:54 UTC |
| b04c00a | Santiago Zanella-Beguelin | 10 May 2019, 14:46:19 UTC | Hints | 10 May 2019, 14:46:19 UTC |
| 039f5de | Aymeric Fromherz | 10 May 2019, 14:27:09 UTC | Merge branch 'fstar-master' into afromher_big_aesgcm | 10 May 2019, 14:27:26 UTC |
| f4a74d4 | Santiago Zanella-Beguelin | 10 May 2019, 12:35:24 UTC | Add function to free state in EverCrypt.Hash.Incremental | 10 May 2019, 12:35:24 UTC |
| ca3e12f | Jonathan Protzenko | 09 May 2019, 19:01:18 UTC | Fix two assumes added at the interface between Ed25519 / SHA512 when the connection was made | 09 May 2019, 19:01:18 UTC |
| a6b22a4 | Jonathan Protzenko | 09 May 2019, 19:01:02 UTC | Remove antediluvian code that became unreachable when we landed the WIP ed25519 | 09 May 2019, 19:01:02 UTC |
| 74a1f51 | Jonathan Protzenko | 08 May 2019, 14:51:31 UTC | hints | 08 May 2019, 14:51:31 UTC |
| f0001a0 | Jonathan Protzenko | 08 May 2019, 14:49:22 UTC | temporary fix: z3refresh + a couple small changes to get this proof to go through | 08 May 2019, 14:49:22 UTC |
| 55dd80a | Jonathan Protzenko | 08 May 2019, 14:31:57 UTC | Some work on proof quality. rlimit 200 --> rlimit 50 + replayable hints | 08 May 2019, 14:31:57 UTC |
| fdd1ea9 | Aymeric Fromherz | 08 May 2019, 03:54:13 UTC | Hints | 08 May 2019, 03:54:13 UTC |
| e3eab20 | Aymeric Fromherz | 08 May 2019, 03:37:12 UTC | Merge branch '_vale_leakage' into _vale_leakage_stack | 08 May 2019, 03:37:12 UTC |
| 599a854 | Aymeric Fromherz | 08 May 2019, 02:59:40 UTC | StackTaint: Fix GCM{de,en}cryptOpt | 08 May 2019, 02:59:40 UTC |
| 69d7fa2 | Aymeric Fromherz | 08 May 2019, 01:24:33 UTC | Fix stackTaint interop | 08 May 2019, 01:24:33 UTC |
| ad6adb3 | Aymeric Fromherz | 08 May 2019, 01:18:06 UTC | More refactoring for stack taint | 08 May 2019, 01:18:06 UTC |
| d4f1bbf | Chris Hawblitzel | 07 May 2019, 21:33:57 UTC | Update Vale version to prepare for new F* version | 07 May 2019, 21:33:57 UTC |
| df98277 | Aymeric Fromherz | 07 May 2019, 19:58:28 UTC | Taint analysis for stack instructions | 07 May 2019, 19:58:28 UTC |
| 31d74b5 | Jonathan Protzenko | 07 May 2019, 15:24:59 UTC | Merge pull request #159 from project-everest/taramana_tests Taramana tests | 07 May 2019, 15:24:59 UTC |
| f310596 | Jonathan Protzenko | 07 May 2019, 13:44:33 UTC | Merge branch 'fstar-master' into taramana_tests | 07 May 2019, 13:44:33 UTC |
| 4a583e2 | Christoph M. Wintersteiger | 07 May 2019, 13:02:01 UTC | Merge pull request #158 from project-everest/cwinter-benchmark More benchmarking improvements. | 07 May 2019, 13:02:01 UTC |
| 3c9eb3e | Christoph M. Wintersteiger | 01 May 2019, 15:57:54 UTC | Benchmarks: clean up compiler options | 07 May 2019, 12:13:09 UTC |
| 06117bc | Christoph M. Wintersteiger | 01 May 2019, 15:45:04 UTC | Benchmarks: use -flto where possible | 07 May 2019, 12:13:08 UTC |
| 975392e | Christoph M. Wintersteiger | 01 May 2019, 15:44:41 UTC | Fix benchmark timing problem | 07 May 2019, 12:13:08 UTC |
| 944eae6 | Christoph M. Wintersteiger | 01 May 2019, 14:26:32 UTC | Benchmark plot tweaks. | 07 May 2019, 12:13:07 UTC |
| 613c2dd | Christoph M. Wintersteiger | 01 May 2019, 14:15:53 UTC | Benchmark build fixes. Added BCrypt x25519. | 07 May 2019, 12:13:07 UTC |
