| 90fb001 | Jay Bosamiya | 31 May 2019, 23:49:31 UTC | It should be up to caller to show equal init_rsp | 31 May 2019, 23:49:31 UTC |
| df2a6de | Jay Bosamiya | 31 May 2019, 23:25:15 UTC | Actually ensure that havoc'd flags are added into the write sets | 31 May 2019, 23:25:15 UTC |
| d9cc3f1 | Jay Bosamiya | 31 May 2019, 22:51:06 UTC | Conservatively disallow instruction exchanges between non-generic instr | 31 May 2019, 22:51:06 UTC |
| 833c283 | Jay Bosamiya | 31 May 2019, 22:46:47 UTC | We use this taint better progress [equiv_states] upon [unchanged] | 31 May 2019, 22:47:14 UTC |
| bc54d9a | Jay Bosamiya | 31 May 2019, 22:46:18 UTC | The value of an [access_location] should _also_ refer to its taint | 31 May 2019, 22:46:18 UTC |
| 03f5d8d | Jay Bosamiya | 31 May 2019, 22:14:52 UTC | Minor rlimit/fuel/ifuel fixes for speed!! | 31 May 2019, 22:14:52 UTC |
| ba13d29 | Jay Bosamiya | 31 May 2019, 22:11:22 UTC | Fix [lemma_eval_instr_equiv_states] | 31 May 2019, 22:11:22 UTC |
| c91197f | Jay Bosamiya | 31 May 2019, 22:07:52 UTC | Fix some minor regressions due to recent [equiv_states] changes | 31 May 2019, 22:07:52 UTC |
| 5af35dc | Jay Bosamiya | 31 May 2019, 20:58:35 UTC | That was one annoying proof; [lemma_unchanged_at_combine] done. | 31 May 2019, 20:58:35 UTC |
| 10e8a2a | Jay Bosamiya | 31 May 2019, 20:10:30 UTC | Fix precondition of [lemma_unchanged_at_combine] | 31 May 2019, 20:10:30 UTC |
| 107d3e4 | Jay Bosamiya | 31 May 2019, 20:06:36 UTC | Some progress on [lemma_unchanged_at_and_except] | 31 May 2019, 20:06:36 UTC |
| ed86aa1 | Jay Bosamiya | 31 May 2019, 19:39:05 UTC | Progress on [lemma_equiv_states_when_except_none] | 31 May 2019, 19:39:05 UTC |
| a58ad1c | Jay Bosamiya | 31 May 2019, 19:38:44 UTC | Stop being so strict for the equivalence-of-flags check | 31 May 2019, 19:38:44 UTC |
| 9b455f8 | Jay Bosamiya | 31 May 2019, 18:22:20 UTC | Finish up [lemma_commute] (lots of sub-lemmas yet to be proven though) | 31 May 2019, 18:22:20 UTC |
| a43c84d | Jay Bosamiya | 31 May 2019, 18:21:59 UTC | The effect of [ok] should also be dependent only upon the reads | 31 May 2019, 18:21:59 UTC |
| cb19a95 | Jay Bosamiya | 31 May 2019, 18:11:51 UTC | Some more progress | 31 May 2019, 18:11:51 UTC |
| 891afc4 | Jay Bosamiya | 30 May 2019, 22:49:20 UTC | Some progress using this new generic style | 30 May 2019, 22:49:20 UTC |
| 59e7f9b | Jay Bosamiya | 30 May 2019, 22:03:09 UTC | A new approach towards generically proving things | 30 May 2019, 22:46:11 UTC |
| 52cd98b | Jay Bosamiya | 30 May 2019, 21:22:54 UTC | Introduce [valid_dst_access_location] | 30 May 2019, 21:22:54 UTC |
| c7e3ea5 | Jay Bosamiya | 30 May 2019, 21:22:38 UTC | Split up [disjoint_access_locations] | 30 May 2019, 21:22:38 UTC |
| bb99f72 | Jay Bosamiya | 30 May 2019, 00:38:13 UTC | Yay! And now we have it proven for [_inouts] too! | 30 May 2019, 00:38:13 UTC |
| 427a54e | Jay Bosamiya | 30 May 2019, 00:34:27 UTC | No need to special case on [Some?] anymore :) | 30 May 2019, 00:34:27 UTC |
| 2a8079d | Jay Bosamiya | 30 May 2019, 00:33:44 UTC | Remove the [temp_] from the name since we are now diving down this route | 30 May 2019, 00:33:44 UTC |
| 27728d9 | Jay Bosamiya | 30 May 2019, 00:32:39 UTC | Progress! We now have unchanged read for args! | 30 May 2019, 00:32:39 UTC |
| 5199ba4 | Jay Bosamiya | 29 May 2019, 23:15:11 UTC | Get started, on the way to proving [lemma_untainted_eval_ins_exchange] | 29 May 2019, 23:24:33 UTC |
| be43456 | Jay Bosamiya | 29 May 2019, 20:59:48 UTC | Make sure to note down the thoughts on [eq_code] | 29 May 2019, 20:59:48 UTC |
| 9a323b9 | Jay Bosamiya | 29 May 2019, 20:32:48 UTC | Update to new proof strategy to make life easier; document things :) | 29 May 2019, 20:34:35 UTC |
| 394c4de | Jay Bosamiya | 29 May 2019, 20:11:59 UTC | Fix the broken proof; damn rlimits | 29 May 2019, 20:11:59 UTC |
| 7506278 | Jay Bosamiya | 29 May 2019, 20:09:06 UTC | Finish up proof for [lemma_ins_exchange_allowed_symmetric] | 29 May 2019, 20:09:06 UTC |
| 8449690 | Jay Bosamiya | 29 May 2019, 18:57:20 UTC | Finish proving its symmetry | 29 May 2019, 18:57:20 UTC |
| a0aff2f | Jay Bosamiya | 29 May 2019, 18:56:51 UTC | Cleaner-to-read definition of [disjoint_access_locations] | 29 May 2019, 18:56:51 UTC |
| 74e59ae | Jay Bosamiya | 29 May 2019, 18:36:40 UTC | A slightly fragile proof broke due to latest change | 29 May 2019, 18:37:48 UTC |
| ff43f5c | Jay Bosamiya | 29 May 2019, 18:33:49 UTC | Fix the definition of [disjoint_access_location] | 29 May 2019, 18:33:49 UTC |
| c3938bb | Jay Bosamiya | 29 May 2019, 18:31:52 UTC | [ins_exchange_allowed] can now be shown to be symmetric | 29 May 2019, 18:31:52 UTC |
| c062b33 | Jay Bosamiya | 29 May 2019, 18:31:31 UTC | Split away the [disjoint] and prove some things about it | 29 May 2019, 18:31:31 UTC |
| fa540fa | Jay Bosamiya | 29 May 2019, 18:08:40 UTC | Split away the [&&.] and the [for_all] | 29 May 2019, 18:08:40 UTC |
| bded0f7 | Jay Bosamiya | 29 May 2019, 01:47:09 UTC | Add a docstring to the module | 29 May 2019, 01:47:09 UTC |
| ee94a91 | Jay Bosamiya | 29 May 2019, 01:39:06 UTC | Add comment for review | 29 May 2019, 01:39:06 UTC |
| 1ee236e | Jay Bosamiya | 29 May 2019, 01:35:51 UTC | Finish proving [lemma_eval_instr_equiv_states] | 29 May 2019, 01:35:51 UTC |
| a1e9524 | Jay Bosamiya | 29 May 2019, 01:19:34 UTC | Finish [lemma_untainted_eval_ins_equiv_states]; progress on [lemma_eval_instr_equiv_states] | 29 May 2019, 01:19:34 UTC |
| 3301861 | Jay Bosamiya | 29 May 2019, 00:31:48 UTC | Finish [lemma_eval_code_equiv_states], [lemma_eval_codes_equiv_states], etc | 29 May 2019, 00:31:48 UTC |
| 575707e | Jay Bosamiya | 29 May 2019, 00:13:28 UTC | Finish proof of [lemma_eval_ins_equiv_states] | 29 May 2019, 00:13:28 UTC |
| 1d64254 | Jay Bosamiya | 29 May 2019, 00:04:51 UTC | Progress on [lemma_eval_ins_equiv_states] | 29 May 2019, 00:04:51 UTC |
| c9ae34d | Jay Bosamiya | 28 May 2019, 23:46:32 UTC | Keep track of memTaint and stackTaint in the state equivalence | 28 May 2019, 23:46:32 UTC |
| 147bf35 | Jay Bosamiya | 28 May 2019, 23:33:49 UTC | Progress on proof of [lemma_untainted_eval_ins_equiv_states] | 28 May 2019, 23:33:49 UTC |
| f730bd8 | Jay Bosamiya | 28 May 2019, 22:21:36 UTC | Define [equiv_states_ext] to help F* "think harder"; progress on [lemma_untainted_eval_ins_equiv_states] | 28 May 2019, 22:21:36 UTC |
| 9361251 | Jay Bosamiya | 28 May 2019, 22:09:31 UTC | Progress on [lemma_untainted_eval_ins_equiv_states] | 28 May 2019, 22:09:31 UTC |
| 91a3f1d | Jay Bosamiya | 28 May 2019, 20:47:22 UTC | Progress on [lemma_eval_ins_equiv_states] | 28 May 2019, 20:47:22 UTC |
| f50dc30 | Jay Bosamiya | 28 May 2019, 20:32:04 UTC | Progress on [lemma_instruction_exchange] | 28 May 2019, 20:32:04 UTC |
| 1658085 | Jay Bosamiya | 28 May 2019, 19:50:15 UTC | Finish proving [lemma_bubble_to_top] | 28 May 2019, 19:50:15 UTC |
| e6259ce | Jay Bosamiya | 28 May 2019, 19:40:24 UTC | Add some convenience wrappers | 28 May 2019, 19:44:15 UTC |
| 5a1e021 | Jay Bosamiya | 28 May 2019, 19:31:09 UTC | Introduce [lemma_eval_codes_equiv_states] | 28 May 2019, 19:31:09 UTC |
| 7cfca8e | Jay Bosamiya | 28 May 2019, 19:16:07 UTC | Progress on [lemma_bubble_to_top] | 28 May 2019, 19:18:04 UTC |
| 0602506 | Jay Bosamiya | 28 May 2019, 18:13:47 UTC | Prove [lemma_code_exchange] | 28 May 2019, 18:13:47 UTC |
| 6a7d628 | Jay Bosamiya | 28 May 2019, 18:13:26 UTC | Bring in state filtering, to remove taint related stuff | 28 May 2019, 18:13:26 UTC |
| ea8fb65 | Jay Bosamiya | 24 May 2019, 23:34:10 UTC | Use a specific definition for [equiv_states] | 24 May 2019, 23:34:10 UTC |
| f36ecd2 | Jay Bosamiya | 24 May 2019, 22:18:38 UTC | Get started on [lemma_reordering] | 24 May 2019, 23:01:43 UTC |
| 2166cbe | Jay Bosamiya | 24 May 2019, 21:59:38 UTC | With the updated [untainted_eval_ins] we can now reconcile it well | 24 May 2019, 21:59:38 UTC |
| ac711ca | Jay Bosamiya | 24 May 2019, 21:55:22 UTC | Update [untainted_eval_ins] to do the stack update better. See msg. The tainted semantics use [MReg rRsp (-8)] and something similar would be needed for the instruction reorderer as well; keeping it as a [MConst] would lead to more difficulties later on, and this change should not affect anything, hopefully. Had a discussion with @R1kM about this, and the older version existed only for legacy reasons. | 24 May 2019, 21:55:22 UTC |
| c1d874a | Jay Bosamiya | 24 May 2019, 21:53:06 UTC | Use [&] instead of [*] for product type | 24 May 2019, 21:53:06 UTC |
| 248bfd7 | Jay Bosamiya | 24 May 2019, 21:52:39 UTC | Rename modules | 24 May 2019, 21:52:39 UTC |
| 4883f16 | Jay Bosamiya | 24 May 2019, 01:38:23 UTC | Some progress on the proofs | 24 May 2019, 01:38:23 UTC |
| 4f7dfc2 | Jay Bosamiya | 24 May 2019, 01:07:50 UTC | Implement larger scale reordering check | 24 May 2019, 01:34:47 UTC |
| 3a70c4e | Jay Bosamiya | 23 May 2019, 23:53:12 UTC | Add warning | 23 May 2019, 23:53:12 UTC |
| de94870 | Jay Bosamiya | 23 May 2019, 22:27:28 UTC | Add some sanity checks | 23 May 2019, 22:27:28 UTC |
| 4578081 | Jay Bosamiya | 23 May 2019, 22:16:16 UTC | Minor typos | 23 May 2019, 22:26:23 UTC |
| dc02d39 | Jay Bosamiya | 23 May 2019, 22:05:11 UTC | Fix issue with write-set for implicits | 23 May 2019, 22:05:11 UTC |
| eea2b9a | Jay Bosamiya | 23 May 2019, 21:47:48 UTC | More precise [disjoint_access_locations] | 23 May 2019, 21:47:48 UTC |
| b9560b7 | Jay Bosamiya | 23 May 2019, 21:37:59 UTC | rw_set for push/pop | 23 May 2019, 21:37:59 UTC |
| b78f0a2 | Jay Bosamiya | 23 May 2019, 21:30:32 UTC | Some minor restructuring | 23 May 2019, 21:30:32 UTC |
| 2ef1f06 | Jay Bosamiya | 23 May 2019, 21:24:00 UTC | Get the write set from an instruction | 23 May 2019, 21:24:00 UTC |
| d96e038 | Jay Bosamiya | 23 May 2019, 21:19:30 UTC | Be able to get read-set from an instruction | 23 May 2019, 21:21:49 UTC |
| 5bdd33f | Jay Bosamiya | 23 May 2019, 01:26:48 UTC | Minor updates | 23 May 2019, 02:02:58 UTC |
| 46a2823 | Jay Bosamiya | 23 May 2019, 01:18:45 UTC | Set up some targets to work on for the InstructionReorder xformer | 23 May 2019, 01:21:04 UTC |
| 0fc4e02 | Jay Bosamiya | 23 May 2019, 01:07:36 UTC | Add a [possibly] monad, to make it easier to keep track of reasons | 23 May 2019, 01:13:13 UTC |
| 7ed4e6d | Jay Bosamiya | 23 May 2019, 00:02:55 UTC | Get started with instruction reorderer transformer | 23 May 2019, 00:02: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 |
