Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Vale.X64.Lemmas.fst.hints
[
"��;�V5\u0007e\\7�`����",
[
[
"Vale.X64.Lemmas.eval_ins",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"Vale.X64.State_pretyping_eb96f2119e19317ec6e3b596d5a46609",
"constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Ins", "equation_Prims.nat",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.StateLemmas.state_of_S",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_ok",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"e104c1e79eac34e96f5f994410c2fd77"
],
[
"Vale.X64.Lemmas.eval_while_eq_all",
1,
2,
0,
[ "@query" ],
0,
"884c8e4a186fee95475905b32f9e7927"
],
[
"Vale.X64.Lemmas.eval_code_eq_all",
1,
2,
0,
[ "@query" ],
0,
"edbedf47976d091404bbd57f2e8642f7"
],
[
"Vale.X64.Lemmas.eval_code_eq_all",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@query", "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
"Vale.X64.Machine_Semantics_s_pretyping_65b491a3aaa0023c48ae2461669f28bd",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Block",
"constructor_distinct_Vale.X64.Machine_s.IfElse",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_Vale.X64.Bytes_Code_s.OEq",
"data_elim_Vale.X64.Bytes_Code_s.OGe",
"data_elim_Vale.X64.Bytes_Code_s.OGt",
"data_elim_Vale.X64.Bytes_Code_s.OLe",
"data_elim_Vale.X64.Bytes_Code_s.OLt",
"data_elim_Vale.X64.Bytes_Code_s.ONe",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.flags_t",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.machine_heap",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.regs_t",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.memTaint_t",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.unit",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"int_inversion", "int_typing",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.observation@tok",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"subterm_ordering_Vale.X64.Machine_s.Block",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_memTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"unit_typing", "well-founded-ordering-on-nat"
],
0,
"9a51309c25ce6a795cdb05227a2b650f"
],
[
"Vale.X64.Lemmas.eval_code_eq_all",
3,
2,
0,
[ "@query" ],
0,
"61e89ec72b0f4df56281392bcefc6c0f"
],
[
"Vale.X64.Lemmas.eval_code_eq_all",
4,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_codes"
],
0,
"534dd4f43376edaff8fa80d4c6db68cb"
],
[
"Vale.X64.Lemmas.eval_code_eq_all",
5,
2,
0,
[ "@query" ],
0,
"27e940705579fd2284a5a0eb6f1270ea"
],
[
"Vale.X64.Lemmas.eval_code_eq_all",
6,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.X64.Bytes_Code_s.OEq",
"data_elim_Vale.X64.Bytes_Code_s.OGe",
"data_elim_Vale.X64.Bytes_Code_s.OGt",
"data_elim_Vale.X64.Bytes_Code_s.OLe",
"data_elim_Vale.X64.Bytes_Code_s.OLt",
"data_elim_Vale.X64.Bytes_Code_s.ONe",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"disc_equation_Vale.X64.Machine_s.While",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "int_typing",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"kinding_Vale.X64.Machine_s.observation@tok",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_Negation",
"primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ae5b5cb1a546cfab29c9d4cf1d39c2de",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_memTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace",
"typing_Vale.X64.Machine_Semantics_s.eval_ocmp",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_while",
"typing_Vale.X64.Machine_Semantics_s.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.Machine_s.uu___is_While", "unit_inversion",
"unit_typing", "well-founded-ordering-on-nat"
],
0,
"232835df55f89e58abe06ab742a790e9"
],
[
"Vale.X64.Lemmas.eval_code_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Lemmas.state_eq_S",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state"
],
0,
"e2358bbce654c1b91d01628cd3eb6bb4"
],
[
"Vale.X64.Lemmas.eval_codes_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Lemmas.state_eq_S",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state"
],
0,
"b48295087f60e198a7fe0d9fa348d6f4"
],
[
"Vale.X64.Lemmas.eval_while_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"45b08593a48eb4f94aff8ea9118f0b0c"
],
[
"Vale.X64.Lemmas.increase_fuel",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"binder_x_8afd38cc1321157644dafce503e55d5a_1",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.IfElse",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.X64.Bytes_Code_s.OEq",
"data_elim_Vale.X64.Bytes_Code_s.OGe",
"data_elim_Vale.X64.Bytes_Code_s.OGt",
"data_elim_Vale.X64.Bytes_Code_s.OLe",
"data_elim_Vale.X64.Bytes_Code_s.OLt",
"data_elim_Vale.X64.Bytes_Code_s.ONe",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.eval_code_ts",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_s.observation@tok",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"lemma_Vale.X64.Lemmas.eval_while_eq", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation", "primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_2dc313a427ca7d8dbc5ee93de70c50ce",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"subterm_ordering_Vale.X64.Machine_s.Block",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_memTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stack",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_Semantics_s.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"unit_inversion", "unit_typing", "well-founded-ordering-on-nat"
],
0,
"b1039e4e8465bb9b9053ffca0a6b9b89"
],
[
"Vale.X64.Lemmas.increase_fuel",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_8afd38cc1321157644dafce503e55d5a_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Machine_s.Block",
"data_elim_FStar.Pervasives.Native.Some",
"data_typing_intro_Vale.X64.Machine_s.Block@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Lemmas.eval_code_ts",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"lemma_Vale.X64.Lemmas.eval_codes_eq",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code"
],
0,
"fcab82161ecdb2fe0301235b79e51397"
],
[
"Vale.X64.Lemmas.lemma_cmp_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"db07f2e5edf84231a5abbfba8e1f821a"
],
[
"Vale.X64.Lemmas.lemma_cmp_eq",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d39e12025532b76ea40a0ec2190196b4"
],
[
"Vale.X64.Lemmas.lemma_cmp_eq",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_src_operand",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.OEq_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OEq_o2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.eval_operand",
"typing_Vale.X64.StateLemmas.state_to_S", "unit_typing"
],
0,
"9e297c4b876600bf6b36403092bcea17"
],
[
"Vale.X64.Lemmas.lemma_cmp_ne",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"e41b9a4d2cd7c31f44293b1cfc41b81e"
],
[
"Vale.X64.Lemmas.lemma_cmp_ne",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"ca6595244ab61f69b02d8579246f7d17"
],
[
"Vale.X64.Lemmas.lemma_cmp_ne",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
"bool_inversion", "constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Bytes_Code_s.ONe",
"data_typing_intro_Vale.X64.Bytes_Code_s.ONe@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_src_operand",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.unit",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"int_inversion",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.ONe_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.ONe_o2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp", "typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.eval_operand",
"typing_Vale.X64.StateLemmas.state_to_S", "unit_typing"
],
0,
"d189c8972475a334ce4d0d8069f165f8"
],
[
"Vale.X64.Lemmas.lemma_cmp_le",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"312470308216c4053ec434be38498876"
],
[
"Vale.X64.Lemmas.lemma_cmp_le",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"47ec45e71ba2ae5874c07554dbfef7cd"
],
[
"Vale.X64.Lemmas.lemma_cmp_le",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Bytes_Code_s.OLe",
"data_typing_intro_Vale.X64.Bytes_Code_s.OLe@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_src_operand",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.OLe_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OLe_o2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp", "typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.State.eval_operand", "unit_typing"
],
0,
"cf84f4d810c9ed06bee236485d2b8de9"
],
[
"Vale.X64.Lemmas.lemma_cmp_ge",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"50de5ba4bfceed64a9cb5d3621a91a91"
],
[
"Vale.X64.Lemmas.lemma_cmp_ge",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"195f936e7ca482050630613ed9ce7f2d"
],
[
"Vale.X64.Lemmas.lemma_cmp_ge",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Bytes_Code_s.OGe",
"data_typing_intro_Vale.X64.Bytes_Code_s.OGe@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_src_operand",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.OGe_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OGe_o2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp", "typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.State.eval_operand", "unit_typing"
],
0,
"f8b46e5775d8865b55ee86a210c478c0"
],
[
"Vale.X64.Lemmas.lemma_cmp_lt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"815e1891ddb1d1f922e8e421a016838b"
],
[
"Vale.X64.Lemmas.lemma_cmp_lt",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"6c2241bd74a2d5087bdeb08078f3bdf2"
],
[
"Vale.X64.Lemmas.lemma_cmp_lt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Bytes_Code_s.OLt",
"data_typing_intro_Vale.X64.Bytes_Code_s.OLt@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_src_operand",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_LessThan",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.OLt_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OLt_o2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp", "typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.State.eval_operand", "unit_typing"
],
0,
"d24430262f3ce96358f74083bdbb55a2"
],
[
"Vale.X64.Lemmas.lemma_cmp_gt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"3ddf7f7a145358e75f75ad7c6485a632"
],
[
"Vale.X64.Lemmas.lemma_cmp_gt",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"a9d963612c4e2ffba78e679d8ab8657c"
],
[
"Vale.X64.Lemmas.lemma_cmp_gt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Bytes_Code_s.OGt",
"data_typing_intro_Vale.X64.Bytes_Code_s.OGt@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_src_operand",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"lemma_Vale.X64.StateLemmas.lemma_to_eval_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_GreaterThan",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.OGt_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OGt_o2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp", "typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.State.eval_operand", "unit_typing"
],
0,
"966b33289eac0f8e587c9f4743f7e46b"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"cfff85772ed1b75ea11e356a4ab974c6"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_eq",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"086e10c1c923ccd55c1febf9da0059f4"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_eq",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Bytes_Code_s.OEq_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OEq_o2",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"ce5271427690ce9dd79b100dafeaf02a"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_ne",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"b8506f8072479a221a5984b22073cdf7"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_ne",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"bd8a8225067d5704975fe9b15c86e3c3"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_ne",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.Bytes_Code_s.ONe",
"data_typing_intro_Vale.X64.Bytes_Code_s.ONe@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Bytes_Code_s.ONe_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.ONe_o2",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"1a21e6f9ded86df40cb77a5735cab371"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_le",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"262046e86fe03e8f027ef7da9bbe4668"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_le",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"cccf660681a06ff3d5be991d2722c84d"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_le",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.Bytes_Code_s.OLe",
"data_typing_intro_Vale.X64.Bytes_Code_s.OLe@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Bytes_Code_s.OLe_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OLe_o2",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"cb25577b9cc1e70b781f2d3342e6cfe4"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_ge",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"2f1fa9772c15a46db08d5ba4df0952ed"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_ge",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"47dd31fa525ccf3dd7d110293ebc5115"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_ge",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.Bytes_Code_s.OGe",
"data_typing_intro_Vale.X64.Bytes_Code_s.OGe@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Bytes_Code_s.OGe_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OGe_o2",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"fd88408211ac558dbf6a05457695c93f"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_lt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"2c6e352bbca3f978028302e5425c67d1"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_lt",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"dddc202bb94797f8778a838e62f019eb"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_lt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.Bytes_Code_s.OLt",
"data_typing_intro_Vale.X64.Bytes_Code_s.OLt@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Bytes_Code_s.OLt_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OLt_o2",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"dc1063cc66f9ae7411225e43efd56fb5"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_gt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"e46480a461bc2cafce076348e4941537"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_gt",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4f8c91579c1e400c0f0a3dc0ee6040c9"
],
[
"Vale.X64.Lemmas.lemma_valid_cmp_gt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Vale.X64.Bytes_Code_s.OGt",
"data_typing_intro_Vale.X64.Bytes_Code_s.OGt@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.StateLemmas.state_to_S",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Bytes_Code_s.OGt_o1",
"projection_inverse_Vale.X64.Bytes_Code_s.OGt_o2",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"7236ee0a2bfa6ae8e84b43d2cb37a0dc"
],
[
"Vale.X64.Lemmas.lemma_merge_total",
1,
2,
0,
[ "@query" ],
0,
"c5dbddc27b37d6fe4323f739a4fa89eb"
],
[
"Vale.X64.Lemmas.lemma_merge_total",
2,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"@query", "constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Vale.X64.Machine_s.Block",
"data_typing_intro_Vale.X64.Machine_s.Block@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Lemmas.compute_merge_total",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.eval_code_ts",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"lemma_Vale.X64.Lemmas.eval_codes_eq",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_ok",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_GreaterThan",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Prims.__proj__Cons__item__hd",
"typing_Prims.__proj__Cons__item__tl",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"958c3abc664f18b38b9f9f50272482e5"
],
[
"Vale.X64.Lemmas.lemma_empty_total",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Machine_s.Block",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.X64.Machine_s.Block@tok",
"equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented",
"function_token_typing_Vale.X64.Machine_Semantics_s.code",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_typing", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"1512587c3f17f41771b791b659b29947"
],
[
"Vale.X64.Lemmas.lemma_ifElse_total",
1,
2,
0,
[
"@query", "equation_Prims.nat",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__2"
],
0,
"c84fb898b2cc41f1a32502ac38db5d61"
],
[
"Vale.X64.Lemmas.lemma_ifElseTrue_total",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"bool_inversion", "constructor_distinct_Vale.X64.Machine_s.IfElse",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok",
"data_typing_intro_Vale.X64.Machine_s.IfElse@tok",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"kinding_Vale.X64.Machine_s.observation@tok",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_ok",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace",
"typing_Vale.X64.Stack_Sems.stack_to_s",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_memTaint",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
"typing_Vale.X64.StateLemmas.state_to_S", "unit_typing"
],
0,
"9bb5e8bb05cbec0054a87e12f8a95dd3"
],
[
"Vale.X64.Lemmas.lemma_ifElseFalse_total",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"bool_inversion", "constructor_distinct_Vale.X64.Machine_s.IfElse",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok",
"data_typing_intro_Vale.X64.Machine_s.IfElse@tok",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"kinding_Vale.X64.Machine_s.observation@tok",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_ok",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_trace",
"typing_Vale.X64.Stack_Sems.stack_to_s",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_memTaint",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
"typing_Vale.X64.StateLemmas.state_to_S", "unit_typing"
],
0,
"47264a7c9779fa78fef91aba46a782dc"
],
[
"Vale.X64.Lemmas.eval_while_inv_temp",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f5706e78e8676ef1f10ed44f4562bcc5"
],
[
"Vale.X64.Lemmas.lemma_while_total",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "data_typing_intro_Vale.X64.Machine_s.While@tok",
"equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.eval_while_inv",
"equation_Vale.X64.Lemmas.eval_while_inv_temp",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.StateLemmas.state_to_S",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.StateLemmas.state_to_S"
],
0,
"ca415adce3b1960c2723141f92ff3281"
],
[
"Vale.X64.Lemmas.lemma_whileTrue_total",
1,
2,
0,
[
"@query", "equation_Prims.nat",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2"
],
0,
"e520c5017adf71fbd72bbab9709bbd6a"
],
[
"Vale.X64.Lemmas.lemma_whileFalse_total",
1,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.State_pretyping_eb96f2119e19317ec6e3b596d5a46609",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_typing_intro_Vale.X64.Machine_s.While@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.While",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Lemmas.eval_while_inv",
"equation_Vale.X64.Lemmas.eval_while_inv_temp",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_typing",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.StateLemmas.state_to_S", "unit_typing"
],
0,
"c32d0478bccddf66a3232d8dff5a1092"
],
[
"Vale.X64.Lemmas.lemma_whileMerge_total",
1,
2,
0,
[ "@query" ],
0,
"3686c52c4842eeb07d83f541e1a6fa58"
],
[
"Vale.X64.Lemmas.lemma_whileMerge_total",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Bytes_Code_s_pretyping_8d8114524e962c921a106571a277b146",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.While",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"data_typing_intro_Vale.X64.Machine_s.BranchPredicate@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.While",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Lemmas.eval_code",
"equation_Vale.X64.Lemmas.eval_code_ts",
"equation_Vale.X64.Lemmas.eval_ocmp",
"equation_Vale.X64.Lemmas.eval_while_inv",
"equation_Vale.X64.Lemmas.eval_while_inv_temp",
"equation_Vale.X64.Lemmas.state_eq_S",
"equation_Vale.X64.Lemmas.state_eq_opt",
"equation_Vale.X64.Lemmas.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Memory.memtaint",
"equation_Vale.X64.StateLemmas.state_to_S",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.X64.Machine_Semantics_s.ins",
"int_inversion", "int_typing",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Bytes_Code_s.ocmp@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.observation@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_Vale.X64.Lemmas.eval_code_eq",
"lemma_Vale.X64.Lemmas.eval_while_eq",
"lemma_Vale.X64.StateLemmas.lemma_to_memTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_ok",
"lemma_Vale.X64.StateLemmas.lemma_to_stackTaint",
"lemma_Vale.X64.StateLemmas.lemma_to_trace",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_Negation",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"proj_equation_Vale.X64.Machine_s.While_whileBody",
"proj_equation_Vale.X64.Machine_s.While_whileCond",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"refinement_interpretation_Tm_refine_39e65cc0f27229d531211e7cb29a0691",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8d7684ca1be7acf48e31bf17f1a9fe2b",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"typing_Vale.X64.Lemmas.eval_ocmp",
"typing_Vale.X64.Lemmas.valid_ocmp",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
"typing_Vale.X64.Machine_s.__proj__While__item__whileBody",
"typing_Vale.X64.Machine_s.__proj__While__item__whileCond",
"typing_Vale.X64.Stack_Sems.stack_to_s",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_memTaint",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
"typing_Vale.X64.StateLemmas.state_to_S", "unit_typing"
],
0,
"c6eebc0f5e2bd0ba78c7fd7fc7b64dc1"
]
]
]
Computing file changes ...
