| b5e8596 | Jay Bosamiya | 04 June 2019, 18:24:09 UTC | File at least verifies now; some lemmas broke though which we need to fix | 04 June 2019, 18:24:09 UTC |
| 2a5defc | Jay Bosamiya | 04 June 2019, 17:50:55 UTC | Handle memory locations more precisely. See msg. For example, the following instruction actually _reads_ from RAX and writes to some location in memory. Previously this would've been considered to not really be a read from RAX but we were relying upon the conservative behavior of the [disjoint] operation to be correct; now it is baked into the definition of the read-write sets. ``` mov [rax + 5], 10 ``` | 04 June 2019, 17:50:55 UTC |
| c5133c8 | Jay Bosamiya | 04 June 2019, 17:50:24 UTC | Access locations now handle all memory as one huge block, and all stack as another huge block | 04 June 2019, 17:50:24 UTC |
| 4cd53cc | Jay Bosamiya | 04 June 2019, 17:03:40 UTC | Demonstrate counter-example showing my intuition of lemma being wrong is correct | 04 June 2019, 17:03:40 UTC |
| 87ca739 | Jay Bosamiya | 04 June 2019, 01:01:12 UTC | Some progress | 04 June 2019, 01:20:06 UTC |
| 4a340d9 | Jay Bosamiya | 04 June 2019, 00:19:22 UTC | Some progress towards [unchanged_upon_both_non_disjoint]. See msg. In order to prove [unchanged_upon_both_non_disjoint], we need to show that our notion of [disjoint_access_locations] is _actually_ conservative. On the way to showing this, we need to additionally introduce the notion of an [access_location] that is [always_constant] since otherwise, it messes with the way the lists work and how disjoint-ness works. | 04 June 2019, 00:19:22 UTC |
| 68e526f | Jay Bosamiya | 03 June 2019, 23:22:10 UTC | Move towards using [unchanged_at_extended]. See msg. The issue with the previous approach is because we need to be conservative. This in particular means that if we have both [unchanged_at locs s1 s2] and [unchanged_except locs s1 s2], we **DO NOT** have [unchanged_except Nil s1 s2], even thought it might seem like we should. An example that demonstrates this is if we assume that XMM1 is not disjoint from RAX. This is a conservative assumption and is correct and sound. However, at this point, we face our conundrum. Assume the [locs] above is the singleton set [RAX]. Since [unchanged_at] looks **only** at the locations within the [locs] and [unchanged_except] looks at locations which are _strictly_ disjoint from the [locs], the [XMM1] is not talked about whatsoever. This means that with this definition, we have a situation where the [XMM1] register _could_ have different values, and thus this is a counter-example. We fix this by extending [unchanged_at], to get [unchanged_at_extended]. This new extended definition takes into account everything that is not provably disjoint. This means that it is more difficult to prove, but it provides much more if it were to exist in the precondition. Additionally, it properly encodes the notion of conservatively equal. Thus, with this definition, we can now (trivially) show that [unchanged_at_extended locs s1 s2] and [unchanged_except locs s1 s2] implies [unchanged_except Nil s1 s2]. It does throw some extra stuff into the picture; in particular, we can no longer as easily show the behavior upon two operations that are commuted. We need to introduce a new notion of [unchanged_upon_both_non_disjoint] which allows one to talk about two different sets of access locations; and is true only if their intersection is maintained across both states. It remains to be seen how much extra effort this new approach will take up for proving things from [untainted_eval_ins] though. | 03 June 2019, 23:22:10 UTC |
| 7b31fab | Jay Bosamiya | 03 June 2019, 22:21:34 UTC | Demonstrate the exact case of failure for the current [unchanged_at] definition | 03 June 2019, 22:21:34 UTC |
| aa1ca86 | Jay Bosamiya | 03 June 2019, 21:51:38 UTC | Get to work on proving write-behavior for instructions | 03 June 2019, 21:51:38 UTC |
| 6055e85 | Jay Bosamiya | 03 June 2019, 18:27:30 UTC | Now that we've got commutativity in general, we have to work on specializing it | 03 June 2019, 18:41:34 UTC |
| df20b0f | Jay Bosamiya | 03 June 2019, 17:10:47 UTC | Remove the old style | 03 June 2019, 17:10:47 UTC |
| 271ac8d | Jay Bosamiya | 01 June 2019, 01:13:30 UTC | Maintain same [valid_addr] mapping between [unchanged_except] | 01 June 2019, 01:13:30 UTC |
| 4e7eca3 | Jay Bosamiya | 01 June 2019, 01:01:59 UTC | Propagate to stack proof | 01 June 2019, 01:01:59 UTC |
| 37929aa | Jay Bosamiya | 01 June 2019, 00:59:36 UTC | Progress on [lemma_equiv_states_when_except_none] for mem and memTaint | 01 June 2019, 01:01:54 UTC |
| 5466b7f | Jay Bosamiya | 01 June 2019, 00:17:29 UTC | Finish handling [initial_rsp] too | 01 June 2019, 00:17:29 UTC |
| 6dc0345 | Jay Bosamiya | 01 June 2019, 00:12:19 UTC | Finish handling the [ms_ok]s | 01 June 2019, 00:12:19 UTC |
| 9a4d374 | Jay Bosamiya | 01 June 2019, 00:07:17 UTC | Fix up issue wrt ok-equivalence | 01 June 2019, 00:07:17 UTC |
| 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 |
