| fe73838 | Jay Bosamiya | 11 June 2019, 00:46:50 UTC | Woohoo! With the flags changes, these now work! | 11 June 2019, 00:46:50 UTC |
| 38dd77b | Jay Bosamiya | 10 June 2019, 21:29:48 UTC | For some reason [fast_multiply_a1b] requires this observation. | 10 June 2019, 21:29:48 UTC |
| f572960 | Jay Bosamiya | 10 June 2019, 20:18:54 UTC | Updates due to most recent merge. Some parts of the proofs broke. | 10 June 2019, 20:20:21 UTC |
| bb80a79 | Jay Bosamiya | 10 June 2019, 19:23:32 UTC | I don't believe we need this MConst->MReg change anymore. Reverting for making life easier. | 10 June 2019, 19:23:32 UTC |
| dd9b55b | Jay Bosamiya | 10 June 2019, 17:50:01 UTC | Minor updates due to latest merge | 10 June 2019, 17:50:01 UTC |
| ea9b345 | Jay Bosamiya | 10 June 2019, 17:39:13 UTC | Merge branch 'jay-trivalue-flags' into _jay-instr-reordering | 10 June 2019, 17:39:13 UTC |
| f35ad2a | Jay Bosamiya | 10 June 2019, 17:38:53 UTC | Merge remote-tracking branch 'origin/fstar-master' into _jay-instr-reordering | 10 June 2019, 17:38:53 UTC |
| 807fcd0 | Jay Bosamiya | 09 June 2019, 21:01:06 UTC | Minor fix due to recent merge | 09 June 2019, 21:01:06 UTC |
| b31f1ba | Jay Bosamiya | 09 June 2019, 19:15:17 UTC | Minor fix due to module alias no longer existing | 09 June 2019, 19:16:01 UTC |
| 71fca92 | Jay Bosamiya | 09 June 2019, 06:52:01 UTC | Merge remote-tracking branch 'origin/fstar-master' into jay-trivalue-flags The following files had conflicts that had to be manually resolved: vale/code/arch/x64/Vale.X64.Decls.fsti vale/code/arch/x64/Vale.X64.InsBasic.vaf vale/code/arch/x64/Vale.X64.QuickCodes.fsti vale/code/arch/x64/Vale.X64.State.fsti vale/code/arch/x64/Vale.X64.StateLemmas.fst vale/code/arch/x64/Vale.X64.StateLemmas.fsti vale/code/arch/x64/interop/Vale.AsLowStar.LowStarSig.fst vale/specs/hardware/Vale.X64.Machine_Semantics_s.fst vale/specs/hardware/Vale.X64.Machine_s.fst vale/specs/interop/Vale.Interop.X64.fsti | 09 June 2019, 06:52:01 UTC |
| 4f5bf84 | Chris Hawblitzel | 08 June 2019, 21:44:43 UTC | Update hints | 08 June 2019, 21:44:43 UTC |
| 1424dca | Chris Hawblitzel | 08 June 2019, 20:06:07 UTC | Make QuickCode and taint analysis more polymorphic over operand types | 08 June 2019, 20:06:07 UTC |
| 29824e9 | Jay Bosamiya | 08 June 2019, 03:26:07 UTC | Bump up rlimit ; No idea why the proof needs such a massive rlimit! | 08 June 2019, 03:41:30 UTC |
| 4157ccb | Jay Bosamiya | 08 June 2019, 01:51:29 UTC | Fix [Vale.Curve25519.X64.FastHybrid] vaf | 08 June 2019, 01:51:29 UTC |
| d05d97c | Jay Bosamiya | 07 June 2019, 23:55:32 UTC | Fix [Vale.Curve25519.FastHybrid] vaf | 07 June 2019, 23:55:32 UTC |
| bb89a21 | Jay Bosamiya | 07 June 2019, 21:47:39 UTC | Fix [Vale.Curve25519.X64.FastHybrid] vaf | 07 June 2019, 21:47:39 UTC |
| 34aea7b | Chris Hawblitzel | 07 June 2019, 21:35:34 UTC | Update hints | 07 June 2019, 21:35:34 UTC |
| c0db36d | Jay Bosamiya | 07 June 2019, 21:00:28 UTC | Fix [Vale.Curve25519.X64.FastUtil] vaf | 07 June 2019, 21:00:28 UTC |
| b52a48e | Jay Bosamiya | 07 June 2019, 20:53:38 UTC | Update flags to use an FStar.Map rather than the map16 | 07 June 2019, 20:54:24 UTC |
| 148f1a8 | Chris Hawblitzel | 07 June 2019, 19:42:58 UTC | Rename various mem and stack types to machine_heap, vale_heap, etc. | 07 June 2019, 19:42:58 UTC |
| 2bfabd1 | Jay Bosamiya | 07 June 2019, 19:12:22 UTC | Fix [Vale.AsLowStar.Wrapper] | 07 June 2019, 19:12:22 UTC |
| e06c887 | Jay Bosamiya | 07 June 2019, 17:58:58 UTC | Split [update_*_maintain_*] into [updated_*] and [maintained_*] | 07 June 2019, 18:04:56 UTC |
| 48bc33e | Chris Hawblitzel | 07 June 2019, 16:52:40 UTC | Merge branch 'fstar-master' into _vale_generic | 07 June 2019, 16:52:40 UTC |
| 4d87357 | Chris Hawblitzel | 07 June 2019, 16:48:52 UTC | Replace regs/xmms register file fields with single register file field | 07 June 2019, 16:48:52 UTC |
| 20c09c2 | Jay Bosamiya | 07 June 2019, 01:47:05 UTC | Fix [Vale.AsLowStar.LowStarSig] | 07 June 2019, 01:47:05 UTC |
| 296f932 | Jay Bosamiya | 07 June 2019, 01:40:14 UTC | Fix [Vale.X64.Leakage_Ins] | 07 June 2019, 01:40:14 UTC |
| f2e8b35 | Jay Bosamiya | 07 June 2019, 01:28:39 UTC | Change [update_*] into [updated_*] | 07 June 2019, 01:28:39 UTC |
| 78428e5 | Jay Bosamiya | 07 June 2019, 01:06:49 UTC | Fix [Vale.Interop.X64] | 07 June 2019, 01:06:49 UTC |
| 5940ca2 | Jay Bosamiya | 07 June 2019, 01:03:32 UTC | Fix [Vale.Interop.Assumptions] | 07 June 2019, 01:04:58 UTC |
| 0e22855 | Jay Bosamiya | 07 June 2019, 00:59:29 UTC | Fix [Vale.X64.Leakage_s] | 07 June 2019, 00:59:29 UTC |
| d9ca920 | Jay Bosamiya | 07 June 2019, 00:42:41 UTC | Fix [val_get_flags] | 07 June 2019, 00:42:41 UTC |
| e292f89 | Jay Bosamiya | 07 June 2019, 00:26:22 UTC | Update to [update_*_maintain_*] from [update_*]; add new [update_*]s | 07 June 2019, 00:34:42 UTC |
| f7d7872 | Jay Bosamiya | 07 June 2019, 00:20:49 UTC | Add [valid_cf] and [valid_of] preconditions to instructions that read them | 07 June 2019, 00:20:49 UTC |
| 7c0a519 | Jay Bosamiya | 07 June 2019, 00:14:34 UTC | Fix the type for efl | 07 June 2019, 00:17:33 UTC |
| 7e42ccc | Jay Bosamiya | 07 June 2019, 00:12:33 UTC | Introduce [valid_cf] and [valid_of] | 07 June 2019, 00:12:33 UTC |
| dd545aa | Jay Bosamiya | 07 June 2019, 00:10:12 UTC | Make it consistent | 07 June 2019, 00:10:12 UTC |
| b467c33 | Jay Bosamiya | 06 June 2019, 23:22:04 UTC | This feels wrong to do, but decls need to return bools to use in the vafs | 06 June 2019, 23:22:04 UTC |
| 0f6411c | Jay Bosamiya | 06 June 2019, 23:07:46 UTC | Stop using register names inside Flags | 06 June 2019, 23:07:46 UTC |
| 7f091cb | Jay Bosamiya | 06 June 2019, 23:07:37 UTC | More updates | 06 June 2019, 23:07:37 UTC |
| 6847bc9 | Jay Bosamiya | 06 June 2019, 22:55:33 UTC | Update [Vale.X64.Lemmas] due to latest changes | 06 June 2019, 22:55:33 UTC |
| 0182a09 | Jay Bosamiya | 06 June 2019, 22:51:44 UTC | Dangit! It wasn't working due to a damn typo! | 06 June 2019, 22:51:44 UTC |
| 773e148 | Jay Bosamiya | 06 June 2019, 22:50:05 UTC | Fix confusing typo :P | 06 June 2019, 22:50:05 UTC |
| 61edaee | Jay Bosamiya | 06 June 2019, 22:45:06 UTC | Update [Vale.X64.QuickCodes] due to latest changes | 06 June 2019, 22:45:06 UTC |
| fc4375c | Jay Bosamiya | 06 June 2019, 00:48:58 UTC | Update [Vale.X64.Decls] due to latest changes | 06 June 2019, 00:52:05 UTC |
| 2d17135 | Jay Bosamiya | 06 June 2019, 00:41:49 UTC | Update StateLemmas; For some reason [lemma_to_flags] doesn't work though. :/ | 06 June 2019, 00:41:49 UTC |
| 990bfa6 | Jay Bosamiya | 06 June 2019, 00:36:23 UTC | Update [State] using the new [Flags] module | 06 June 2019, 00:36:23 UTC |
| d328e71 | Jay Bosamiya | 06 June 2019, 00:33:37 UTC | Introduce [Vale.X64.Flags] module; similar to [Vale.X64.Regs] | 06 June 2019, 00:33:37 UTC |
| 35a3d7e | Jay Bosamiya | 06 June 2019, 00:14:59 UTC | The machine state should store the flags as a [flags_t] | 06 June 2019, 00:14:59 UTC |
| 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 |
| 13450b8 | Jay Bosamiya | 05 June 2019, 20:43:17 UTC | Merge branch '_jay-instr-reordering-common-memory' into _jay-instr-reordering | 05 June 2019, 20:43:17 UTC |
| 5a7d9e1 | Jay Bosamiya | 05 June 2019, 20:26:17 UTC | Remove stuff due to recent cleanup | 05 June 2019, 20:26:17 UTC |
| 7d58d7f | Jay Bosamiya | 05 June 2019, 20:24:44 UTC | Clean up [unchanged_except] | 05 June 2019, 20:24:44 UTC |
| 5547401 | Jay Bosamiya | 05 June 2019, 20:24:27 UTC | Remove [unchanged] and [unchanged_all] | 05 June 2019, 20:24:35 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 660994b | Jonathan Protzenko | 04 June 2019, 00:33:38 UTC | Minor tweak | 04 June 2019, 00:33:38 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 9581f28 | Chris Hawblitzel | 02 June 2019, 00:17:42 UTC | Switch operand64 to nat64, switch MemAccess to int | 02 June 2019, 00:17:42 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 |
