| 5547401 | Jay Bosamiya | 05 June 2019, 20:24:27 UTC | Remove [unchanged] and [unchanged_all] | 05 June 2019, 20:24:35 UTC |
| a789041 | Jay Bosamiya | 05 June 2019, 19:56:18 UTC | Progress on proof of [lemma_instr_write_output_explicit_only_affects_write_aux2] | 05 June 2019, 19:56:18 UTC |
| aaea69e | Jay Bosamiya | 05 June 2019, 19:53:39 UTC | Progress on proof for [lemma_instr_write_output_implicit_only_affects_write_aux2] | 05 June 2019, 19:53:39 UTC |
| 70ffe35 | Jay Bosamiya | 05 June 2019, 18:11:49 UTC | Remove old comment | 05 June 2019, 18:11:49 UTC |
| 2b85ce4 | Jay Bosamiya | 05 June 2019, 00:42:30 UTC | Add to the equiv_states sanity check | 05 June 2019, 00:42:30 UTC |
| 9c9e1b9 | Jay Bosamiya | 05 June 2019, 00:36:27 UTC | We can thus now remove [unchanged_upon_both_non_disjoint] which was unprovable before | 05 June 2019, 00:36:27 UTC |
| 51ba03c | Jay Bosamiya | 05 June 2019, 00:35:11 UTC | And with that, we have proven [lemma_equiv_states_when_except_none] | 05 June 2019, 00:35:11 UTC |
| 2a69fff | Jay Bosamiya | 05 June 2019, 00:34:30 UTC | Make it easier to skip out on some parts of the state | 05 June 2019, 00:34:30 UTC |
| 5850a1f | Jay Bosamiya | 05 June 2019, 00:27:57 UTC | Introduce [lemma_locations_complete] | 05 June 2019, 00:27:57 UTC |
| 8d1d69c | Jay Bosamiya | 05 June 2019, 00:16:46 UTC | Finish proving [lemma_unchanged_at_and_except] | 05 June 2019, 00:16:46 UTC |
| 229a784 | Jay Bosamiya | 05 June 2019, 00:13:22 UTC | Fix another admit by reproving [lemma_unchanged_at_combine] | 05 June 2019, 00:13:22 UTC |
| 9239eb1 | Jay Bosamiya | 04 June 2019, 23:56:17 UTC | Fix a bunch of [admit ()]s and remove [unchanged_at_extended] | 04 June 2019, 23:56:17 UTC |
| f44171c | Jay Bosamiya | 04 June 2019, 23:54:33 UTC | Move a sanity check out; fix minor things up | 04 June 2019, 23:56:10 UTC |
| 299cacf | Jay Bosamiya | 04 June 2019, 23:48:39 UTC | Auto trigger lemma upon [!!(disjoint_location a1 a2)] | 04 June 2019, 23:48:58 UTC |
| 11e8f1b | Jay Bosamiya | 04 June 2019, 23:36:44 UTC | Get the file verifying again by adding admits / removing stuff | 04 June 2019, 23:36:44 UTC |
| f4ab205 | Jay Bosamiya | 04 June 2019, 23:36:36 UTC | Split away the sanity checks | 04 June 2019, 23:36:36 UTC |
| b9bec81 | Jay Bosamiya | 04 June 2019, 23:19:09 UTC | Remove unnecessary dependency | 04 June 2019, 23:19:09 UTC |
| d6f2d26 | Jay Bosamiya | 04 June 2019, 23:18:40 UTC | Rename the module itself | 04 June 2019, 23:18:40 UTC |
| 0707b53 | Jay Bosamiya | 04 June 2019, 23:16:07 UTC | Change return types to better match with expected intentions | 04 June 2019, 23:16:07 UTC |
| 1829603 | Jay Bosamiya | 04 June 2019, 23:14:04 UTC | Perform a massive renaming [access_location] -> [location] | 04 June 2019, 23:14:04 UTC |
| ce16bcb | Jay Bosamiya | 04 June 2019, 23:11:26 UTC | Add documentation; clean up some lemmas | 04 June 2019, 23:11:26 UTC |
| d5ba176 | Jay Bosamiya | 04 June 2019, 22:58:27 UTC | Cleanup to mark things exposed by the fsti better | 04 June 2019, 22:58:27 UTC |
| 9d44d45 | Jay Bosamiya | 04 June 2019, 22:50:55 UTC | Introduce updates and "truly disjoint" lemma | 04 June 2019, 22:50:55 UTC |
| a33d00c | Jay Bosamiya | 04 June 2019, 22:50:07 UTC | Copy all the [access_locations] and disjointness stuff into a separate module | 04 June 2019, 22:50:07 UTC |
| 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 |
