| fb86df9 | Jay Bosamiya | 18 June 2019, 18:03:00 UTC | Updates | 18 June 2019, 18:03:00 UTC |
| 3abe39c | Jay Bosamiya | 17 June 2019, 18:10:27 UTC | Expose [lemma_locations_same_with_filter] | 17 June 2019, 18:10:27 UTC |
| f3304a0 | Jay Bosamiya | 17 June 2019, 17:13:36 UTC | First pass implementation of live-variable analysis | 17 June 2019, 17:14:38 UTC |
| 5cea4df | Jay Bosamiya | 17 June 2019, 17:10:59 UTC | Expose [locations_of_ocmp] | 17 June 2019, 17:10:59 UTC |
| 8b38015 | Jay Bosamiya | 17 June 2019, 15:30:09 UTC | Merge remote-tracking branch 'origin/fstar-master' into _jay-instr-reordering-eqcode | 17 June 2019, 15:30:09 UTC |
| e0d3b8e | Chris Hawblitzel | 14 June 2019, 21:30:18 UTC | Update Vale version | 14 June 2019, 21:30:18 UTC |
| ccaa1ee | Jay Bosamiya | 14 June 2019, 20:17:45 UTC | Split away the actual part that needs to be shown | 14 June 2019, 20:17:45 UTC |
| f6f2aa6 | Jay Bosamiya | 14 June 2019, 19:42:17 UTC | Start work on non-eqtype permutation finding. See msg. We are not going to make the [ins] into an [eqtype], since it internally contains functions. Instead, a function equivalent to the [eq_code] in the new code will be exposed by Chris, which will allow one to know if the evaluation of two [code]s is the same. Since we do _not_ care about the actual instructions but we care only about their behavior, this should be sufficient. A small parts of the final proof breaks due to this change, but this should be fixed up in the upcoming commits. | 14 June 2019, 19:53:49 UTC |
| 01011a5 | Jay Bosamiya | 14 June 2019, 18:29:36 UTC | Merge remote-tracking branch 'origin/fstar-master' into _jay-instr-reordering | 14 June 2019, 18:29:36 UTC |
| 6962c8c | Jay Bosamiya | 14 June 2019, 18:21:44 UTC | Explicitly disallow [bounded_effects] on non-generic instructions rather than them being [admit()]s | 14 June 2019, 18:21:44 UTC |
| d5381d0 | Jay Bosamiya | 14 June 2019, 18:17:41 UTC | Fix the rwset definitions of non-generic instructions | 14 June 2019, 18:17:41 UTC |
| 958aa56 | Jay Bosamiya | 13 June 2019, 23:58:24 UTC | ...and finishes off [lemma_machine_eval_ins_st_unchanged_behavior] | 13 June 2019, 23:58:24 UTC |
| 2161320 | Jay Bosamiya | 13 June 2019, 23:56:26 UTC | Updrade [lemma_eval_instr_ok] into stronger theorem [lemma_eval_instr_unchanged_at'] | 13 June 2019, 23:56:26 UTC |
| 66d6124 | Jay Bosamiya | 13 June 2019, 23:39:37 UTC | Finish proving [lemma_eval_instr_ok] !!! | 13 June 2019, 23:39:37 UTC |
| 4f1f5d7 | Jay Bosamiya | 13 June 2019, 23:34:30 UTC | Finish proving [lemma_instr_write_outputs_only_writes] !!! | 13 June 2019, 23:34:30 UTC |
| 7e4f664 | Jay Bosamiya | 13 June 2019, 23:20:56 UTC | Some more progress. This proof has become unweildy :/ | 13 June 2019, 23:21:11 UTC |
| e49349e | Jay Bosamiya | 13 June 2019, 22:55:57 UTC | Strengthen the statement of [lemma_instr_write_outputs_only_affects_write_extend] | 13 June 2019, 22:55:57 UTC |
| f426a3b | Jay Bosamiya | 13 June 2019, 22:38:18 UTC | More progress. Weaken preconditions regarding the new [s1] and [s2] | 13 June 2019, 22:44:58 UTC |
| f2b0117 | Jay Bosamiya | 13 June 2019, 22:22:01 UTC | More progress on [lemma_instr_write_outputs_only_writes]. | 13 June 2019, 22:22:01 UTC |
| ecc6a3c | Jay Bosamiya | 13 June 2019, 21:48:24 UTC | Progress on [lemma_instr_write_outputs_only_writes]. | 13 June 2019, 21:48:24 UTC |
| 141f758 | Jay Bosamiya | 13 June 2019, 17:55:56 UTC | Fix the reads of stack operations | 13 June 2019, 17:55:56 UTC |
| 4a38b24 | Aseem Rastogi | 13 June 2019, 06:46:12 UTC | annotating recall in Lib.Buffer | 13 June 2019, 06:46:12 UTC |
| cc50e6f | Jay Bosamiya | 13 June 2019, 01:49:37 UTC | Progress. | 13 June 2019, 01:49:46 UTC |
| 84285fc | Jay Bosamiya | 13 June 2019, 01:45:25 UTC | Since the memory is an entire unbreakable block (for now), it must be read to be written into | 13 June 2019, 01:45:54 UTC |
| 0449b39 | Jay Bosamiya | 13 June 2019, 01:18:17 UTC | Finish proving [lemma_instr_apply_eval_inouts_same_read] & [lemma_instr_apply_eval_args_same_read] | 13 June 2019, 01:18:17 UTC |
| 06b4d11 | Jay Bosamiya | 13 June 2019, 01:01:03 UTC | Progress! Now working on showing that the reads are correctly bounded | 13 June 2019, 01:12:00 UTC |
| 78b2810 | Jay Bosamiya | 13 June 2019, 00:26:26 UTC | Some progress on [lemma_machine_eval_ins_st_ok] | 13 June 2019, 00:31:42 UTC |
| 9fd3a88 | Jay Bosamiya | 13 June 2019, 00:20:43 UTC | Make [bounded_effects] stricter | 13 June 2019, 00:20:43 UTC |
| 7d77016 | Jay Bosamiya | 12 June 2019, 23:27:21 UTC | Fix the targets of [BoundedInstructioneffects] | 12 June 2019, 23:27:21 UTC |
| 4b27c9d | Jay Bosamiya | 12 June 2019, 23:24:06 UTC | Finish proving [lemma_bubble_to_top]. | 12 June 2019, 23:24:06 UTC |
| c0984b5 | Jonathan Protzenko | 12 June 2019, 20:46:06 UTC | alg_of_state, requested by Cédric | 12 June 2019, 20:46:06 UTC |
| e3bc159 | Jay Bosamiya | 12 June 2019, 20:43:42 UTC | Minor restructuring | 12 June 2019, 20:43:42 UTC |
| d12dd00 | Jay Bosamiya | 12 June 2019, 20:40:54 UTC | Partial progress | 12 June 2019, 20:40:54 UTC |
| c192518 | Jay Bosamiya | 12 June 2019, 20:33:32 UTC | Fix the sanity checks by importing the right modules | 12 June 2019, 20:33:32 UTC |
| 2321e1c | Jay Bosamiya | 12 June 2019, 20:27:53 UTC | Work towards a fix of the not-ok executions diverging | 12 June 2019, 20:28:18 UTC |
| 69781a7 | Jonathan Protzenko | 12 June 2019, 18:22:49 UTC | hints | 12 June 2019, 18:22:49 UTC |
| ef8a65f | Jonathan Protzenko | 12 June 2019, 18:12:54 UTC | hints | 12 June 2019, 18:12:54 UTC |
| b7ba379 | Jonathan Protzenko | 12 June 2019, 18:12:46 UTC | Add CTR agile specs from _dev in preparation for libquiccrypto landing and EverCrypt.Cipher API | 12 June 2019, 18:12:46 UTC |
| 5b0e6f0 | Jonathan Protzenko | 12 June 2019, 17:05:19 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_ccf | 12 June 2019, 17:05:19 UTC |
| ec4d751 | Jonathan Protzenko | 12 June 2019, 16:18:56 UTC | Add an EverCrypt.Ed25519 to be extended later with multiplexing over Ed25519 | 12 June 2019, 16:18:56 UTC |
| 0dfbc8e | Jonathan Protzenko | 12 June 2019, 16:08:09 UTC | Trim massively the distribution for CCF -- avoid kludges related to libintvector.h | 12 June 2019, 16:08:09 UTC |
| 5a215c5 | Chris Hawblitzel (Microsoft) | 12 June 2019, 01:24:53 UTC | Merge pull request #164 from project-everest/jay-trivalue-flags To havoc or not to havoc, that is the question. Use [option bool], that is the answer. | 12 June 2019, 01:24:53 UTC |
| 9c5b7cb | Chris Hawblitzel | 11 June 2019, 23:08:37 UTC | Merge branch 'fstar-master' into jay-trivalue-flags | 11 June 2019, 23:08:37 UTC |
| 4ad87c5 | Jonathan Protzenko | 11 June 2019, 22:41:24 UTC | WIP: customizations of the CCF build | 11 June 2019, 22:41:24 UTC |
| a778679 | Chris Hawblitzel | 11 June 2019, 22:06:21 UTC | Merge branch 'fstar-master' into jay-trivalue-flags | 11 June 2019, 22:06:21 UTC |
| 49fe761 | Jay Bosamiya | 11 June 2019, 21:56:26 UTC | Make change Chris suggested | Perf Improvemets by s/opaque/abstract/ | 11 June 2019, 21:56:57 UTC |
| 855bc8b | Jay Bosamiya | 11 June 2019, 21:33:57 UTC | Fix up [lemma_locations_complete]. See msg. Previously, we had an assumption in proof of [lemma_locations_complete] that was unprovable since it was false. By refining the statement that the lemma proves, we no longer need this false assumption, and are able to prove things. This does come with the additional cost of a few "observe" assertions in the [InstrReordering] proofs, but all is well and good :) | 11 June 2019, 21:33:57 UTC |
| 06e0fc8 | Jonathan Protzenko | 11 June 2019, 20:36:59 UTC | Tweak | 11 June 2019, 20:36:59 UTC |
| f3ec0c6 | Jay Bosamiya | 11 June 2019, 18:41:29 UTC | Finish proving [lemma_machine_eval_ins_st_only_affects_write_aux] | 11 June 2019, 18:41:29 UTC |
| 0e8a8e6 | Jonathan Protzenko | 11 June 2019, 18:38:57 UTC | Bump rlimit | 11 June 2019, 18:38:57 UTC |
| 9917128 | Jay Bosamiya | 11 June 2019, 18:32:49 UTC | Finish moving relevant parts over | 11 June 2019, 18:32:49 UTC |
| 9b97a64 | Jay Bosamiya | 11 June 2019, 18:16:14 UTC | Move the bounded effects lemma into its correct expected place | 11 June 2019, 18:19:17 UTC |
| e125b8c | Jay Bosamiya | 11 June 2019, 18:09:32 UTC | Move [bounded_effects] over, and document all the exposed functions. | 11 June 2019, 18:09:32 UTC |
| 7432a02 | Jay Bosamiya | 11 June 2019, 18:02:52 UTC | Split away BoundedInstructionEffects into a new module | 11 June 2019, 18:02:52 UTC |
| 8d88b79 | Jonathan Protzenko | 11 June 2019, 16:24:49 UTC | hints | 11 June 2019, 16:24:49 UTC |
| bd3196d | Jonathan Protzenko | 11 June 2019, 16:19:18 UTC | hints | 11 June 2019, 16:19:18 UTC |
| 38d5554 | Chris Hawblitzel | 11 June 2019, 15:16:58 UTC | Increase z3rlimit in Hacl.Impl.Poly1305 | 11 June 2019, 15:16:58 UTC |
| 39b66cf | Jonathan Protzenko | 11 June 2019, 14:52:56 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_crf | 11 June 2019, 14:52:56 UTC |
| 5698523 | Chris Hawblitzel | 11 June 2019, 13:52:24 UTC | Merge branch 'fstar-master' into jay-trivalue-flags-hints | 11 June 2019, 13:52:24 UTC |
| 337fa4f | Jonathan Protzenko | 11 June 2019, 03:47:32 UTC | Fixes for incremental builds | 11 June 2019, 03:47:32 UTC |
| 44660d0 | Jay Bosamiya | 11 June 2019, 02:47:21 UTC | Finish [lemma_machine_eval_ins_st_exchange] | 11 June 2019, 02:47:21 UTC |
| 0441a81 | Jay Bosamiya | 11 June 2019, 01:36:13 UTC | Get rid of an unnecessary indirection | 11 June 2019, 01:36:13 UTC |
| 73ea75b | Jay Bosamiya | 11 June 2019, 01:34:23 UTC | Some parts of the [lemma_machine_eval_ins_st_exchange] are trivial | 11 June 2019, 01:34:23 UTC |
| 1b51e30 | Jay Bosamiya | 11 June 2019, 01:33:11 UTC | Fix the proof for [lemma_code_exchange] | 11 June 2019, 01:33:11 UTC |
| 1b0d381 | Chris Hawblitzel | 11 June 2019, 01:22:47 UTC | Don't use mod pow2_64 in Sub64Wrap, Sbb64 | 11 June 2019, 01:22:47 UTC |
| 8c522b2 | Jay Bosamiya | 11 June 2019, 01:00:07 UTC | Fix the proof for [lemma_machine_eval_ins_st_equiv_states] which had broken due to recent merge | 11 June 2019, 01:03:37 UTC |
| 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 |
| e2ff9ec | Jonathan Protzenko | 10 June 2019, 22:24:49 UTC | More hints, successful build | 10 June 2019, 22:24:49 UTC |
| d70a40b | Jonathan Protzenko | 10 June 2019, 22:10:12 UTC | Hints, battling with an unexplicably tough proof | 10 June 2019, 22:10:12 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 |
| 3a445c5 | Jonathan Protzenko | 10 June 2019, 20:57:34 UTC | Merge remote-tracking branch 'origin/fstar-master' into protz_crf | 10 June 2019, 20:57:34 UTC |
| 693c7f5 | Jonathan Protzenko | 10 June 2019, 20:51:33 UTC | Fixup tests | 10 June 2019, 20:51:33 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 |
| 5aa3b4a | Jonathan Protzenko | 10 June 2019, 19:49:05 UTC | Start erasing a bunch of arguments | 10 June 2019, 19:49:05 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 |
| 01bafa0 | Chris Hawblitzel | 10 June 2019, 04:34:56 UTC | Update hints | 10 June 2019, 04:34:56 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 |
| 1e0853c | Jonathan Protzenko | 07 June 2019, 21:07:22 UTC | Update the discussion; strengthen post-condition since we now allocate and initialize in one go | 07 June 2019, 21:07:22 UTC |
| c0db36d | Jay Bosamiya | 07 June 2019, 21:00:28 UTC | Fix [Vale.Curve25519.X64.FastUtil] vaf | 07 June 2019, 21:00:28 UTC |
| 120699c | Jonathan Protzenko | 07 June 2019, 20:58:53 UTC | Switch to a function for the incremental ghost API, following discussions with Nik. Document the discussions as comments in the code. Update the implementation. Fix hopefully the last fragile proof in this module with another very explicit proof.3 | 07 June 2019, 20:58:53 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 |
