Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Vale.Transformers.BoundedInstructionEffects.fst.hints
[
"$�\u0006d?��O^Cϐ���m",
[
[
"Vale.Transformers.BoundedInstructionEffects.rw_set",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Prims.list__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"kinding_Vale.Transformers.Locations.location@tok",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"typing_tok_Vale.Transformers.Locations.ALocMem@tok"
],
0,
"58b612864b7b78ad4884ce59ec07fdce"
],
[
"Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MConst",
"disc_equation_Vale.X64.Machine_s.MIndex",
"disc_equation_Vale.X64.Machine_s.MReg",
"fuel_guarded_inversion_Vale.X64.Machine_s.maddr"
],
0,
"af9ae6e52aa11204609ebdba164566e0"
],
[
"Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"projection_inverse_BoxInt_proj_0"
],
0,
"f1fb595044971a66399eb4ba2f5fcdca"
],
[
"Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"projection_inverse_BoxInt_proj_0"
],
0,
"55693427a04e0434aab074fbe3a36093"
],
[
"Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOp64",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equality_tok_Vale.X64.Instruction_s.IOp64@tok",
"equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit"
],
0,
"bd836a2034bb8d56cb8c8809c0d5bbb4"
],
[
"Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit"
],
0,
"64bf80d009747a3ad02dcdf212597078"
],
[
"Vale.Transformers.BoundedInstructionEffects.aux_read_set0",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@query", "binder_x_5b8a55910a662c783b1ed3212549410e_0",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"kinding_Vale.X64.Instruction_s.instr_operand@tok",
"proj_equation_Prims.Cons_hd", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
"subterm_ordering_Prims.Cons", "typing_Prims.__proj__Cons__item__hd"
],
0,
"83dabcd1ea75844b8f594bf1da6f8114"
],
[
"Vale.Transformers.BoundedInstructionEffects.aux_read_set1",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_67735fae8b4e79dde4eed727828e245d_2",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"data_elim_Prims.Cons",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Vale.X64.Instruction_s.InOut",
"disc_equation_Vale.X64.Instruction_s.Out",
"equality_tok_Vale.X64.Instruction_s.InOut@tok",
"equality_tok_Vale.X64.Instruction_s.Out@tok",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_inout",
"kinding_Vale.X64.Instruction_s.instr_operand@tok",
"kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Prims.Cons_hd",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
],
0,
"1331df43fd897203090b936aa21486a9"
],
[
"Vale.Transformers.BoundedInstructionEffects.aux_write_set",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"data_elim_Prims.Cons",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"kinding_Vale.X64.Instruction_s.instr_operand@tok",
"kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Prims.Cons_hd",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2"
],
0,
"2d90b608814275da95646d882011c3d7"
],
[
"Vale.Transformers.BoundedInstructionEffects.write_set",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs"
],
0,
"2f68264732266a5f5221b5fb97cd44ca"
],
[
"Vale.Transformers.BoundedInstructionEffects.constant_writes",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Transformers.Locations.ALocCf",
"constructor_distinct_Vale.Transformers.Locations.ALocOf",
"disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equation_Vale.Transformers.Locations.location_val_eqt",
"equation_Vale.Transformers.Locations.location_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs"
],
0,
"aad2dbcb9071d46087eddbcf5e05fa75"
],
[
"Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.Alloc",
"disc_equation_Vale.X64.Bytes_Code_s.Dealloc",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"disc_equation_Vale.X64.Bytes_Code_s.Noop",
"disc_equation_Vale.X64.Bytes_Code_s.Pop",
"disc_equation_Vale.X64.Bytes_Code_s.Push",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.instruction_t",
"projection_inverse_BoxInt_proj_0"
],
0,
"8352a511ed193cac1c6b0ab82dbd3de1"
],
[
"Vale.Transformers.BoundedInstructionEffects.locations_of_ocmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp"
],
0,
"c1eeb05a4e05f138951e1d675f1efafd"
],
[
"Vale.Transformers.BoundedInstructionEffects.unchanged_at",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"c26f228f654acb4643470cf0ce05589d"
],
[
"Vale.Transformers.BoundedInstructionEffects.constant_on_execution",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_01ff889393c4884064895df8d812ac8f_0",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"66d4bf815a54786d766834b1dd214a4b"
],
[
"Vale.Transformers.BoundedInstructionEffects.bounded_effects",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"6a417fabeef53b0887c7085f1e4b563c"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_write_outputs_only_affects_write",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"FStar.Pervasives.Native_pretyping_4894c30cf477acf9a27e7a844279eb08",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"Vale.X64.Instruction_s_pretyping_dfa9c2e22fe11011bf212d55e07ed9db",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_Semantics_s_pretyping_65b491a3aaa0023c48ae2461669f28bd",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"binder_x_44c6303725e907c3759d9004241619c7_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_67735fae8b4e79dde4eed727828e245d_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"binder_x_f6ab80eb5ffc2f5a5eff56ec5e04f3b2_6", "bool_inversion",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Def.PossiblyMonad.Err",
"constructor_distinct_Vale.Transformers.Locations.ALocCf",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocOf",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.Transformers.Locations.ALocStack",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Transformers.Locations.ALocReg",
"data_elim_Vale.X64.Instruction_s.IOp64One",
"data_elim_Vale.X64.Instruction_s.IOpIm",
"data_elim_Vale.X64.Instruction_s.IOpXmmOne",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Instruction_s.IOpFlagsCf@tok",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.Locations.disjoint_location",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.locations",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.cf",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"equation_Vale.X64.Machine_Semantics_s.flags_t",
"equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
"equation_Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
"equation_Vale.X64.Machine_Semantics_s.overflow",
"equation_Vale.X64.Machine_Semantics_s.state_or_fail",
"equation_Vale.X64.Machine_Semantics_s.update_cf_",
"equation_Vale.X64.Machine_Semantics_s.update_mem128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_of_",
"equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_reg_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
"equation_Vale.X64.Machine_Semantics_s.update_stack128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_stack_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"equation_Vale.X64.Machine_s.flag",
"equation_Vale.X64.Machine_s.memTaint_t",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"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.operand",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.bool",
"function_token_typing_Vale.Transformers.Locations.locations",
"function_token_typing_Vale.X64.Instruction_s.instr_out",
"function_token_typing_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"interpretation_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"interpretation_Tm_abs_ef75e83a7935cecf289204005443b376",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Vale.Transformers.Locations.location@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_stack@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.Pervasives.invertOption",
"lemma_FStar.Universe.downgrade_val_raise_val",
"lemma_Vale.Transformers.Locations.auto_lemma_disjoint_location",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_Equality", "primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_kinding_Tm_refine_ecc48c71754f7b5abdcddeebd08f827a",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"token_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"token_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"token_correspondence_Vale.X64.Machine_s.t_reg",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
"typing_FStar.Pervasives.Native.fst",
"typing_FStar.Pervasives.Native.snd", "typing_Prims.uu___is_Nil",
"typing_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"typing_Vale.X64.Instruction_s.instr_operand_t",
"typing_Vale.X64.Instruction_s.instr_operands_t",
"typing_Vale.X64.Instruction_s.instr_val_t",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"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.cf",
"typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
"typing_Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
"typing_Vale.X64.Machine_Semantics_s.instr_write_outputs",
"typing_Vale.X64.Machine_Semantics_s.overflow",
"typing_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"typing_tok_Vale.Transformers.Locations.ALocCf@tok",
"typing_tok_Vale.Transformers.Locations.ALocMem@tok",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok",
"typing_tok_Vale.Transformers.Locations.ALocStack@tok",
"unit_inversion", "unit_typing"
],
0,
"2ff0a957df19541829a618e5fd411cce"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_eval_instr_only_affects_write",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocStack",
"constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.Def.PossiblyMonad.Ok",
"disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equation_FStar.Option.mapTot", "equation_Prims.eqtype",
"equation_Prims.squash",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"equation_Vale.Transformers.BoundedInstructionEffects.write_set",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.X64.Instruction_s.instr_eval_t",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Machine_Semantics_s.eval_instr",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_t_record",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"lemma_Vale.Transformers.Locations.auto_lemma_disjoint_location",
"primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"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.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.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"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",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"typing_FStar.List.Tot.Base.mem",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set",
"typing_Vale.Transformers.BoundedInstructionEffects.write_set",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs",
"typing_Vale.X64.Instruction_s.instr_eval",
"typing_tok_Vale.Transformers.Locations.ALocCf@tok",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok",
"unit_inversion", "unit_typing"
],
0,
"b35480ad9a86571b98ac972ee4b62e8c"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_only_affects_write_aux",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.Def.PossiblyMonad.Ok",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.X64.Machine_Semantics_s.apply_option",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
"interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
"interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_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__2",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
"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",
"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_86ec844a3c36c1a0f27f4ffcf6aec277",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_Vale.X64.Machine_Semantics_s.eval_instr", "unit_typing"
],
0,
"350ddc8f4d3681956ebbdf928457ae01"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_only_affects_write",
1,
1,
0,
[
"@query",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except"
],
0,
"dd87a1c6500c318cff18bf341ca688e4"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_eval_operand_explicit_same_read_both",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_pretyping_65b491a3aaa0023c48ae2461669f28bd",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.Transformers.Locations.ALocStack",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.Transformers.Locations.ALocReg",
"data_elim_Vale.X64.Machine_Semantics_s.Machine_stack",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.OMem",
"data_elim_Vale.X64.Machine_s.OStack",
"data_elim_Vale.X64.Machine_s.Reg",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"eq2-interp", "equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Transformers.BoundedInstructionEffects.both",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.eval_maddr",
"equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
"equation_Vale.X64.Machine_Semantics_s.regs_t",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_Vale.X64.Machine_s.tmaddr",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"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.operand",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Vale.Def.Words_s.nat64",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing", "kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Vale.Transformers.Locations.location@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_stack@tok",
"l_and-interp",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_AmpAmp",
"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_s.Reg_rf",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
"refinement_interpretation_Tm_refine_a51eae56a5c39d95827d04b5f0544d43",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c2c488db3214c38826155caf10d30036",
"token_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg",
"typing_Vale.Arch.Heap.heap_get", "typing_Vale.Arch.Heap.heap_taint",
"typing_Vale.Arch.MachineHeap_s.valid_addr128",
"typing_Vale.Arch.MachineHeap_s.valid_addr64",
"typing_Vale.Transformers.BoundedInstructionEffects.both",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"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.eval_maddr",
"typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
"typing_Vale.X64.Machine_Semantics_s.match_n",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.Machine_s.t_reg_file",
"typing_tok_Vale.Transformers.Locations.ALocStack@tok"
],
0,
"806d3b4afe97357e739098d7b9816848"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_eval_operand_implicit_same_read_both",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_pretyping_65b491a3aaa0023c48ae2461669f28bd",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Prims.list", "constructor_distinct_Prims.unit",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Transformers.Locations.ALocCf",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocOf",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.Transformers.Locations.ALocStack",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some", "data_elim_Prims.Cons",
"data_elim_Vale.Transformers.Locations.ALocReg",
"data_elim_Vale.X64.Instruction_s.IOp64One",
"data_elim_Vale.X64.Instruction_s.IOpXmmOne",
"data_elim_Vale.X64.Machine_Semantics_s.Machine_stack",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"eq2-interp", "equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Transformers.BoundedInstructionEffects.both",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.eval_maddr",
"equation_Vale.X64.Machine_Semantics_s.eval_mov128_op",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit",
"equation_Vale.X64.Machine_Semantics_s.regs_t",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_stack",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.Def.Words_s.nat64",
"function_token_typing_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing", "kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Vale.Transformers.Locations.location@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_stack@tok",
"l_and-interp",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_AmpAmp",
"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_s.Reg_rf",
"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_v",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c2c488db3214c38826155caf10d30036",
"token_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.Arch.MachineHeap_s.valid_addr128",
"typing_Vale.Arch.MachineHeap_s.valid_addr64",
"typing_Vale.Transformers.BoundedInstructionEffects.both",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"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_stack",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_stackTaint",
"typing_Vale.X64.Machine_Semantics_s.cf",
"typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit",
"typing_Vale.X64.Machine_Semantics_s.overflow",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
"typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_Vale.X64.Machine_s.t_reg",
"typing_Vale.X64.Machine_s.t_reg_file",
"typing_tok_Vale.Transformers.Locations.ALocStack@tok", "unit_typing"
],
0,
"1d787d3a64b133a3a037d573ab131241"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_append",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.eqtype",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "true_interp",
"typing_FStar.List.Tot.Base.append"
],
0,
"7cfe25a197018b614ba4b6c8beb49071"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_apply_eval_args_same_read",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
"@query", "binder_x_38287ca2033f50691479ff837e9de132_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_87dc12526be5fec62ede2129096a7dae_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.bind_option",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"interpretation_Tm_abs_b3dcbda6729ac4972bdb25a8abf77eb0",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_FStar.Pervasives.Native.None_a",
"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.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons",
"typing_Vale.X64.Instruction_s.instr_val_t", "unit_inversion",
"unit_typing"
],
0,
"90a216c39d0a12185b332302b1d98ef9"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_apply_eval_inouts_same_read",
1,
6,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
"@query", "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_093c08543626f27b65f30658d7fc39bc_4",
"binder_x_5b8a55910a662c783b1ed3212549410e_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_8afd38cc1321157644dafce503e55d5a_6",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"binder_x_9480187c8e85713ad9eae72e33c57410_1",
"binder_x_f5c27ac55c99c39df8fbe4adb077bc73_3", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Prims.list", "constructor_distinct_Prims.unit",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.InOut",
"constructor_distinct_Vale.X64.Instruction_s.Out",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.X64.Instruction_s.IOp64One",
"data_elim_Vale.X64.Instruction_s.IOpEx",
"data_elim_Vale.X64.Instruction_s.IOpIm",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Vale.X64.Instruction_s.InOut",
"disc_equation_Vale.X64.Instruction_s.Out",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equality_tok_Vale.X64.Instruction_s.InOut@tok",
"equality_tok_Vale.X64.Instruction_s.Out@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Transformers.BoundedInstructionEffects.both",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.Locations.locations",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Machine_Semantics_s.bind_option",
"equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit",
"equation_Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"function_token_typing_Vale.Transformers.Locations.locations",
"function_token_typing_Vale.X64.Instruction_s.instr_out",
"interpretation_Tm_abs_c7148522b68166228dab1bc5afbb5dd9",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Prims.Cons_hd", "projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_FStar.Pervasives.Native.None_a",
"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.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7aac12c24449a22c34d98a0ea8ed4a32",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"true_interp", "typing_FStar.Pervasives.Native.fst",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Prims.__proj__Cons__item__hd",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_read_set1",
"typing_Vale.Transformers.BoundedInstructionEffects.both",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"typing_Vale.X64.Instruction_s.instr_val_t", "unit_inversion",
"unit_typing"
],
0,
"cbb4f7a40c94da05ed548ed7f5d24202"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_apply_eval_same_read",
1,
1,
0,
[ "@query", "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval" ],
0,
"e0f746cb657e0fbb45d94146fffafb7e"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_write_output_explicit_only_writes",
1,
4,
3,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_Semantics_s_pretyping_65b491a3aaa0023c48ae2461669f28bd",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Def.PossiblyMonad.Err",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.Transformers.Locations.ALocStack",
"constructor_distinct_Vale.X64.Instruction_s.IOp64",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Transformers.Locations.ALocReg",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.MIndex",
"data_elim_Vale.X64.Machine_s.MReg",
"data_elim_Vale.X64.Machine_s.OMem",
"data_elim_Vale.X64.Machine_s.OStack",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equality_tok_Vale.X64.Instruction_s.IOp64@tok",
"equality_tok_Vale.X64.Instruction_s.IOpXmm@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.disjoint_location",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_Vale.Transformers.Locations.locations",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.eval_maddr",
"equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
"equation_Vale.X64.Machine_Semantics_s.regs_t",
"equation_Vale.X64.Machine_Semantics_s.state_or_fail",
"equation_Vale.X64.Machine_Semantics_s.update_mem128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_reg_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
"equation_Vale.X64.Machine_Semantics_s.update_stack128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_stack_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.tmaddr",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"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.maddr",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Vale.Transformers.Locations.locations",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Vale.Transformers.Locations.location@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_stack@tok",
"kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_Vale.Transformers.Locations.auto_lemma_disjoint_location",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"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",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"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",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c2c488db3214c38826155caf10d30036",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
"typing_FStar.Pervasives.Native.fst",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.Arch.MachineHeap_s.valid_addr64",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"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.eval_maddr",
"typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
"typing_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"typing_Vale.X64.Machine_s.t_reg",
"typing_tok_Vale.X64.Instruction_s.IOp64@tok",
"typing_tok_Vale.X64.Instruction_s.IOpXmm@tok", "unit_inversion",
"unit_typing"
],
0,
"e162c2b11f386af636862a855ac8b61f"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_write_output_implicit_only_writes",
1,
4,
4,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_ef1cb164cb5e999e95914068a32c6a77",
"Vale.X64.Machine_Semantics_s_pretyping_65b491a3aaa0023c48ae2461669f28bd",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Def.PossiblyMonad.Err",
"constructor_distinct_Vale.Transformers.Locations.ALocCf",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocOf",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.Transformers.Locations.ALocStack",
"constructor_distinct_Vale.X64.Instruction_s.IOpFlagsCf",
"constructor_distinct_Vale.X64.Instruction_s.IOpFlagsOf",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmmOne",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Transformers.Locations.ALocReg",
"data_elim_Vale.X64.Instruction_s.IOp64One",
"data_elim_Vale.X64.Instruction_s.IOpXmmOne",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_elim_Vale.X64.Machine_s.MIndex",
"data_elim_Vale.X64.Machine_s.MReg",
"data_elim_Vale.X64.Machine_s.OMem",
"data_elim_Vale.X64.Machine_s.OStack",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equality_tok_Vale.X64.Instruction_s.IOpFlagsCf@tok",
"equality_tok_Vale.X64.Instruction_s.IOpFlagsOf@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Arch.HeapTypes_s.memTaint_t",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.disjoint_location",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_Vale.Transformers.Locations.locations",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.cf",
"equation_Vale.X64.Machine_Semantics_s.eval_maddr",
"equation_Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
"equation_Vale.X64.Machine_Semantics_s.overflow",
"equation_Vale.X64.Machine_Semantics_s.regs_t",
"equation_Vale.X64.Machine_Semantics_s.state_or_fail",
"equation_Vale.X64.Machine_Semantics_s.update_cf_",
"equation_Vale.X64.Machine_Semantics_s.update_mem128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_of_",
"equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_reg_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
"equation_Vale.X64.Machine_Semantics_s.update_stack128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_stack_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"equation_Vale.X64.Machine_s.flag",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_to_int",
"equation_Vale.X64.Machine_s.tmaddr",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"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.maddr",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Vale.Transformers.Locations.locations",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"interpretation_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"interpretation_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"kinding_Vale.Transformers.Locations.location@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_stack@tok",
"kinding_Vale.X64.Machine_s.reg@tok", "l_and-interp",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_Vale.Transformers.Locations.auto_lemma_disjoint_location",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"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",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Instruction_s.IOpXmmOne_o",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_initial_rsp",
"projection_inverse_Vale.X64.Machine_Semantics_s.Machine_stack_stack_mem",
"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",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
"refinement_interpretation_Tm_refine_8d120609b670b63ede004faaeb0472fc",
"refinement_interpretation_Tm_refine_987329c062a4003a690a0fb724173992",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_kinding_Tm_refine_c2c488db3214c38826155caf10d30036",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg", "true_interp",
"typing_FStar.Pervasives.Native.fst",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"typing_Tm_abs_6e92038f4a88fb2f84b2d65491e2a749",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.Arch.MachineHeap_s.valid_addr64",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"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_ok",
"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.eval_maddr",
"typing_Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
"typing_Vale.X64.Machine_Semantics_s.update_cf_",
"typing_Vale.X64.Machine_Semantics_s.update_of_",
"typing_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"typing_Vale.X64.Machine_s.t_reg",
"typing_tok_Vale.Transformers.Locations.ALocCf@tok",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok",
"typing_tok_Vale.Transformers.Locations.ALocStack@tok",
"typing_tok_Vale.X64.Instruction_s.IOpFlagsCf@tok",
"typing_tok_Vale.X64.Instruction_s.IOpFlagsOf@tok", "unit_inversion",
"unit_typing"
],
0,
"6d34973c34c5bb60b718cf685a064957"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at'_mem",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_f6ab80eb5ffc2f5a5eff56ec5e04f3b2_1", "bool_inversion",
"constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "eq2-interp", "equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.mem",
"unit_inversion", "unit_typing"
],
0,
"50fd82f739ece932d5945a177f9b3810"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_except_not_mem",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_f6ab80eb5ffc2f5a5eff56ec5e04f3b2_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"kinding_Vale.Transformers.Locations.location@tok",
"lemma_Vale.Transformers.Locations.auto_lemma_disjoint_location",
"primitive_Prims.op_Equality", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.mem",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5", "unit_inversion",
"unit_typing"
],
0,
"6f642635ff3ea7dca3b22cf27be2c5e6"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at'_maintained",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"l_and-interp", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"subterm_ordering_Prims.Cons", "true_interp",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"unit_inversion", "unit_typing"
],
0,
"b13d97a7c3a35bb05fa07ba1dca62481"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_disjoint_location_from_locations_append",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_1",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_2",
"binder_x_f6ab80eb5ffc2f5a5eff56ec5e04f3b2_0", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"kinding_Vale.Transformers.Locations.location@tok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"typing_FStar.List.Tot.Base.append",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"unit_inversion", "unit_typing"
],
0,
"ddd8ea57a8b960ef3003cd99aa9df12b"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_except_extend",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state"
],
0,
"2cf5c7e6bdb01303c043b09f640495ec"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_write_outputs_only_affects_write_extend",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state"
],
0,
"d90d93075112da432e5964662223d6ce"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_instr_write_outputs_only_writes",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"@query", "Prims_pretyping_3862c4e8ff39bfc3871b6a47e7ff5b2e",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Def.PossiblyMonad_pretyping_45711eeb8a66f863c2b04f3fc2748fc3",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_44c6303725e907c3759d9004241619c7_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_67735fae8b4e79dde4eed727828e245d_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_8afd38cc1321157644dafce503e55d5a_6",
"binder_x_8afd38cc1321157644dafce503e55d5a_7",
"binder_x_9480187c8e85713ad9eae72e33c57410_0", "bool_inversion",
"constructor_distinct_BoxBool",
"constructor_distinct_FStar.Pervasives.Native.Mktuple2",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Prims.list", "constructor_distinct_Prims.unit",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Def.PossiblyMonad.Err",
"constructor_distinct_Vale.Def.PossiblyMonad.Ok",
"constructor_distinct_Vale.Def.PossiblyMonad.possibly",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"data_elim_Prims.Cons", "data_elim_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.X64.Instruction_s.IOp64One",
"data_elim_Vale.X64.Instruction_s.IOpXmmOne",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Def.PossiblyMonad.Ok@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.Transformers.Locations.ALocStack@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2",
"equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Transformers.BoundedInstructionEffects.both",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_maddr",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand128",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.disjoint_location",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_Vale.Transformers.Locations.locations",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
"equation_Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
"equation_Vale.X64.Machine_Semantics_s.state_or_fail",
"equation_Vale.X64.Machine_Semantics_s.update_mem128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_mem_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"equation_Vale.X64.Machine_Semantics_s.update_reg_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_64_",
"equation_Vale.X64.Machine_Semantics_s.update_reg_xmm_",
"equation_Vale.X64.Machine_Semantics_s.update_stack128_and_taint",
"equation_Vale.X64.Machine_Semantics_s.update_stack_and_taint",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"equation_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_inout",
"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.operand",
"function_token_typing_Prims.unit",
"function_token_typing_Vale.Transformers.Locations.locations",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"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_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok_v",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"token_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"token_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"true_interp", "typing_FStar.List.Tot.Base.append",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
"typing_FStar.Pervasives.Native.fst",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_read_set0",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_read_set1",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set",
"typing_Vale.Transformers.BoundedInstructionEffects.both",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_explicit",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_implicit",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"typing_Vale.X64.Instruction_s.instr_operand_t",
"typing_Vale.X64.Instruction_s.instr_operands_t",
"typing_Vale.X64.Instruction_s.instr_val_t",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
"typing_Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
"typing_Vale.X64.Machine_Semantics_s.instr_write_outputs",
"typing_Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags__",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand128",
"typing_Vale.X64.Machine_Semantics_s.valid_dst_operand64",
"typing_tok_Vale.Transformers.Locations.ALocCf@tok",
"typing_tok_Vale.Transformers.Locations.ALocMem@tok",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok",
"typing_tok_Vale.Transformers.Locations.ALocStack@tok",
"unit_inversion", "unit_typing"
],
0,
"06fe9138200f48923d5436c67dad7b93"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at'_maintained_upon_flag_update",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_200e3c8b74d2d22cfcb25a87c76b4a0a_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_1",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"l_and-interp",
"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_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",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp",
"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"
],
0,
"ccc96438dec4b3e978202f061da147bb"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_eval_instr_unchanged_at'",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_bfcb0d33d97ed19f4887940e22e6a365",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Instruction_s_pretyping_4fc965f8d013cae627c1c220e2784859",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"assumption_Vale.X64.Instruction_s.flag_havoc__uu___haseq",
"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.Transformers.Locations.ALocCf",
"constructor_distinct_Vale.Transformers.Locations.ALocOf",
"constructor_distinct_Vale.X64.Bytes_Code_s.Instr",
"constructor_distinct_Vale.X64.Instruction_s.HavocFlags",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Instruction_s.PreserveFlags@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.Def.PossiblyMonad.Ok",
"disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags", "eq2-interp",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.X64.Instruction_s.HavocFlags@tok",
"equation_FStar.Option.mapTot", "equation_Prims.eqtype",
"equation_Prims.l_True",
"equation_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.BoundedInstructionEffects.read_set",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.BoundedInstructionEffects.write_set",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_Vale.X64.Instruction_s.instr_eval_t",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Machine_Semantics_s.bind_option",
"equation_Vale.X64.Machine_Semantics_s.eval_instr",
"equation_Vale.X64.Machine_Semantics_s.instr_apply_eval",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_read_set0.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_read_set1.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_args.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts.fuel_instrumented",
"equation_with_fuel_Vale.X64.Machine_Semantics_s.instr_write_outputs.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_t_record",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"interpretation_Tm_abs_8f4843a84a8d845f9c0f8fa12759a24b",
"interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"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.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"true_interp", "typing_FStar.List.Tot.Base.mem",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set",
"typing_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"typing_Vale.Transformers.BoundedInstructionEffects.read_set",
"typing_Vale.Transformers.BoundedInstructionEffects.write_set",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs",
"typing_Vale.X64.Instruction_s.instr_eval",
"typing_Vale.X64.Machine_Semantics_s.instr_write_outputs",
"typing_tok_Vale.Transformers.Locations.ALocCf@tok",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok",
"unit_inversion", "unit_typing"
],
0,
"c514ba164c1fb80a72b1fac2faff4ef3"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_ok",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"bool_inversion", "disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.X64.Machine_Semantics_s.apply_option",
"equation_Vale.X64.Machine_Semantics_s.eval_instr",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
"interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
"interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_86ec844a3c36c1a0f27f4ffcf6aec277",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.X64.Machine_Semantics_s.eval_instr", "unit_typing"
],
0,
"8f465532995024670bc2c3ae5506e8c6"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_unchanged_behavior",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"bool_inversion", "disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"equation_FStar.Pervasives.Native.snd",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_at_",
"equation_Vale.X64.Machine_Semantics_s.apply_option",
"equation_Vale.X64.Machine_Semantics_s.eval_instr",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
"interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
"interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"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",
"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__2",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_86ec844a3c36c1a0f27f4ffcf6aec277",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.eval_instr", "unit_typing"
],
0,
"368c3a5a2e48b7d09e2ada6131cda3a0"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_constant_on_execution",
1,
3,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_798f93baee047c0793beddf8ae4ab551",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_b72d599fc3c0eb1fc86c5d80a692be46",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
"Vale.X64.Machine_Semantics_s_pretyping_7f316a64c6b19122da0b07b3da3efe26",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"b2t_def", "binder_x_8afd38cc1321157644dafce503e55d5a_1",
"binder_x_a1849aa29f35dd5f98105753b17a02e0_0", "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.Transformers.Locations.ALocCf",
"constructor_distinct_Vale.Transformers.Locations.ALocOf",
"constructor_distinct_Vale.X64.Instruction_s.HavocFlags",
"constructor_distinct_Vale.X64.Instruction_s.PreserveFlags",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.X64.Bytes_Code_s.Instr",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags", "eq2-interp",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equality_tok_Vale.X64.Instruction_s.HavocFlags@tok",
"equality_tok_Vale.X64.Instruction_s.PreserveFlags@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.Option.mapTot",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.l_True",
"equation_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.Transformers.Locations.location_val_eqt",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_Vale.Transformers.Locations.raise_location_val_eqt",
"equation_Vale.X64.Instruction_s.instr_eval_t",
"equation_Vale.X64.Machine_Semantics_s.apply_option",
"equation_Vale.X64.Machine_Semantics_s.cf",
"equation_Vale.X64.Machine_Semantics_s.eval_instr",
"equation_Vale.X64.Machine_Semantics_s.flag_val_t",
"equation_Vale.X64.Machine_Semantics_s.flags_none",
"equation_Vale.X64.Machine_Semantics_s.havoc_flags",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"equation_Vale.X64.Machine_Semantics_s.overflow",
"equation_Vale.X64.Machine_Semantics_s.st",
"equation_Vale.X64.Machine_s.flag",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_t_record",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.X64.Machine_Semantics_s.flag_val_t",
"function_token_typing_Vale.X64.Machine_Semantics_s.flags_none",
"int_typing",
"interpretation_Tm_abs_0f87f222e83677072ac6914068ad4659",
"interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"interpretation_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
"interpretation_Tm_abs_d7e539669515a49f97544a169303f779",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
"kinding_Vale.Transformers.Locations.location@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"l_and-interp", "l_imp-interp",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"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",
"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__2",
"projection_inverse_FStar.Pervasives.Native.None_a",
"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.Mkdtuple2__1",
"projection_inverse_Prims.Mkdtuple2__2",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_a",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_annotation",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_i",
"projection_inverse_Vale.X64.Bytes_Code_s.Instr_oprs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_havoc_flags",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_i",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_interpretation_Tm_refine_86ec844a3c36c1a0f27f4ffcf6aec277",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"token_correspondence_Vale.X64.Machine_Semantics_s.flags_none",
"token_correspondence_Vale.X64.Machine_Semantics_s.instr_annotation@tok",
"true_interp", "typing_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"typing_Tm_abs_9eb749ea9eba2cc8524aad77bce1df7e",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"typing_Vale.Transformers.BoundedInstructionEffects.__proj__Mkrw_set__item__loc_constant_writes",
"typing_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"typing_Vale.X64.Instruction_s.instr_eval",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_flags",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"typing_Vale.X64.Machine_Semantics_s.apply_option",
"typing_Vale.X64.Machine_Semantics_s.cf",
"typing_Vale.X64.Machine_Semantics_s.eval_instr",
"typing_Vale.X64.Machine_Semantics_s.havoc_flags",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"typing_Vale.X64.Machine_Semantics_s.overflow",
"typing_tok_Vale.Transformers.Locations.ALocCf@tok",
"typing_tok_Vale.X64.Instruction_s.HavocFlags@tok", "unit_inversion",
"unit_typing"
],
0,
"494f054cb593560cbe79033225dd2cbe"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_bounded_effects_Instr",
1,
3,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Instruction_s_pretyping_3f42fef2c19ae51071f07b756c9d8230",
"Vale.X64.Instruction_s_pretyping_4fc965f8d013cae627c1c220e2784859",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_elim_Prims.Cons",
"data_elim_Vale.X64.Bytes_Code_s.Instr",
"data_elim_Vale.X64.Instruction_s.InstrTypeRecord",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Mkdtuple2@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Instruction_s.PreserveFlags@tok",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"equation_Vale.Transformers.BoundedInstructionEffects.write_set",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_t_record",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"kinding_Vale.Transformers.Locations.location@tok",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_86ec844a3c36c1a0f27f4ffcf6aec277",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"typing_FStar.List.Tot.Base.mem",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set",
"typing_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"typing_Vale.Transformers.BoundedInstructionEffects.write_set",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok"
],
0,
"022a211ed477b1672ed6f2d7c915e0b3"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_bounded_effects",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"typing_Vale.Transformers.BoundedInstructionEffects.safely_bounded"
],
0,
"a1afce2de7547fbd36bdea4c3c152c42"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_trace",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_1",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_f14190903d9ed42c0fb68609dedb27ea_3",
"binder_x_f14190903d9ed42c0fb68609dedb27ea_4", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"l_and-interp",
"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_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_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"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"
],
0,
"1d6a6aa7558b614ed29429dabcdec154"
],
[
"Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
1,
1,
0,
[
"@query", "constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v"
],
0,
"da9f784a81c3a2b674657d3144999b29"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects_aux1",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"equation_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"int_inversion",
"interpretation_Tm_abs_b418e68ecc69cb35cd6788241c1edce1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"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_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_FStar.Pervasives.Native.Mktuple2__2",
"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_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"unit_typing"
],
0,
"d34e3acbc4aac3e956dc3513d1be8ee9"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects_aux2",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"b2t_def", "bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.X64.Machine_Semantics_s.Mkmachine_state@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.nat",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"equation_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.Transformers.Locations.raise_location_val_eqt",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Transformers.Locations.location",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"int_inversion",
"interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"interpretation_Tm_abs_b418e68ecc69cb35cd6788241c1edce1",
"kinding_Vale.X64.Machine_s.observation@tok", "l_and-interp",
"l_imp-interp", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_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__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Mkdtuple2__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_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",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"true_interp",
"typing_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"typing_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"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_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.machine_eval_ins_st",
"unit_inversion", "unit_typing"
],
0,
"1e7416fb4c2a9852ad9ee11fc20bf0c2"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects_aux3",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"equation_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"int_inversion",
"interpretation_Tm_abs_b418e68ecc69cb35cd6788241c1edce1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"unit_typing"
],
0,
"f1e42dc521d9e37c19265a7567dfbf39"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects_aux4",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"bool_inversion", "equation_FStar.Pervasives.Native.snd",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"equation_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Prims.unit",
"interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821",
"interpretation_Tm_abs_b418e68ecc69cb35cd6788241c1edce1",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"token_correspondence_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_b418e68ecc69cb35cd6788241c1edce1",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"unit_typing"
],
0,
"3cd7b2fe817d319ab984b17ad9794bf4"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects_aux",
1,
3,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.aux_write_set.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Instruction_s_pretyping_3f42fef2c19ae51071f07b756c9d8230",
"Vale.X64.Instruction_s_pretyping_4fc965f8d013cae627c1c220e2784859",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_elim_Prims.Cons",
"data_elim_Vale.X64.Bytes_Code_s.Instr",
"data_elim_Vale.X64.Instruction_s.InstrTypeRecord",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Mkdtuple2@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"data_typing_intro_Vale.X64.Instruction_s.PreserveFlags@tok",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"equality_tok_Vale.Transformers.Locations.ALocCf@tok",
"equality_tok_Vale.Transformers.Locations.ALocOf@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"equation_Vale.Transformers.BoundedInstructionEffects.safely_bounded",
"equation_Vale.Transformers.BoundedInstructionEffects.write_set",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_t_record",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"kinding_Vale.Transformers.Locations.location@tok",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"typing_FStar.List.Tot.Base.mem",
"typing_Vale.Transformers.BoundedInstructionEffects.__proj__Mkrw_set__item__loc_constant_writes",
"typing_Vale.Transformers.BoundedInstructionEffects.__proj__Mkrw_set__item__loc_writes",
"typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set",
"typing_Vale.Transformers.BoundedInstructionEffects.constant_writes",
"typing_Vale.Transformers.BoundedInstructionEffects.rw_set_of_ins",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__args",
"typing_Vale.X64.Instruction_s.__proj__InstrTypeRecord__item__outs",
"typing_tok_Vale.Transformers.Locations.ALocOf@tok"
],
0,
"0052ea325d11c325e8e32df5773eb835"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects",
1,
1,
0,
[
"@query", "constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v"
],
0,
"3f2f5d49a120e8c9e5a606d3363707de"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects",
2,
1,
0,
[
"@query",
"equation_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins"
],
0,
"66561bfe623ff3a4b51a9ccd49fa1d3c"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_locations_of_ocmp",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
"bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Transformers.Locations.ALocMem",
"constructor_distinct_Vale.Transformers.Locations.ALocReg",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.Transformers.Locations.ALocReg",
"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_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack", "eq2-interp",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Transformers.BoundedInstructionEffects.both",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_ocmp",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"equation_Vale.Transformers.Locations.eval_location",
"equation_Vale.X64.Machine_Semantics_s.eval_ocmp",
"equation_Vale.X64.Machine_Semantics_s.eval_operand",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_Semantics_s.regs_t",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.Def.Words_s.nat64",
"function_token_typing_Vale.X64.Machine_s.t_reg", "int_inversion",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"lemma_Vale.Transformers.Locations.downgrade_val_raise_val_u0_u1",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_disEquality",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Transformers.Locations.ALocReg__0",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
"refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs",
"token_correspondence_Vale.X64.Machine_s.t_reg",
"typing_Vale.Transformers.BoundedInstructionEffects.both",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_ocmp",
"typing_Vale.Transformers.BoundedInstructionEffects.locations_of_operand64",
"typing_Vale.X64.Machine_Semantics_s.eval_ocmp",
"typing_Vale.X64.Machine_Semantics_s.eval_operand",
"typing_Vale.X64.Machine_s.t_reg"
],
0,
"4866603be51ddc094fcb644e546ed98b"
],
[
"Vale.Transformers.BoundedInstructionEffects.intersect",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_374b44ccfcb77ed85d505dbc44265913_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.eqtype", "fuel_guarded_inversion_Prims.list",
"subterm_ordering_Prims.Cons"
],
0,
"53401a7248191da70964ca8a855c060d"
],
[
"Vale.Transformers.BoundedInstructionEffects.difference",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_374b44ccfcb77ed85d505dbc44265913_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.eqtype", "fuel_guarded_inversion_Prims.list",
"subterm_ordering_Prims.Cons"
],
0,
"365bef4ff789610aaab5555a2111b6c4"
],
[
"Vale.Transformers.BoundedInstructionEffects.rw_set_in_parallel",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"d9ea86ea595aa3f1c277fad1e1a2ea49"
],
[
"Vale.Transformers.BoundedInstructionEffects.rw_set_in_series",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"901a985a2341486c371c4e076be1e368"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_constant_on_execution_mem",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"19af16e47a1d2ed1d94b81dce94fbd7c"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_constant_on_execution_mem",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"b2t_def", "binder_x_01ff889393c4884064895df8d812ac8f_0",
"binder_x_67f7b34c719e998a87ec9e762d311ba1_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_da136b17f883af6b3eed3ef05c6ff6b6_4",
"binder_x_f5fd149b4092a02f69e2db9e5a7d6c58_1", "bool_inversion",
"data_typing_intro_Prims.Mkdtuple2@tok", "disc_equation_Prims.Cons",
"eq2-interp", "equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.Transformers.Locations.location_val_eqt",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2", "l_and-interp",
"l_imp-interp", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Mkdtuple2__2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"typing_FStar.List.Tot.Base.mem"
],
0,
"ea6f448874a2a64d9dcf3b0c52947f69"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_add_r_to_rw_set",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"equality_tok_Vale.Transformers.Locations.ALocMem@tok",
"equation_Vale.Transformers.BoundedInstructionEffects.add_r_to_rw_set",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"fuel_guarded_inversion_Vale.Transformers.BoundedInstructionEffects.rw_set",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"typing_tok_Vale.Transformers.Locations.ALocMem@tok"
],
0,
"2d62fe8858812298a1bdd2d4d5542352"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_constant_intersect_belongs_to_writes_union",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"a84cd414da75f2c5f641087c9b28c8af"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_constant_intersect_belongs_to_writes_union",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"binder_x_01ff889393c4884064895df8d812ac8f_0",
"binder_x_01ff889393c4884064895df8d812ac8f_1",
"binder_x_67f7b34c719e998a87ec9e762d311ba1_4",
"binder_x_e4a4ea0953f4dbc000caa72a8e52b33a_5", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Mkdtuple2@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_FStar.List.Tot.Base.op_At", "equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.Locations.location_eq",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"typing_FStar.List.Tot.Base.mem",
"typing_Vale.Transformers.BoundedInstructionEffects.intersect",
"unit_inversion", "unit_typing"
],
0,
"5fb9a544e0be4f04fb91e0360269823b"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_mem",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_f6ab80eb5ffc2f5a5eff56ec5e04f3b2_1", "bool_inversion",
"constructor_distinct_Prims.Nil", "data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "eq2-interp", "equation_Prims.eqtype",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.mem",
"unit_inversion", "unit_typing"
],
0,
"eb2074b431e162718fbaf8436230be72"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_difference_elim",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_Prims.eq2",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"subterm_ordering_Prims.Cons",
"typing_Vale.Transformers.BoundedInstructionEffects.difference",
"unit_inversion", "unit_typing"
],
0,
"2cc35a105a5c3519c213271c66320edb"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_sym_diff_implies_difference",
1,
1,
0,
[
"@query",
"equation_Vale.Transformers.BoundedInstructionEffects.sym_difference"
],
0,
"df74310a4a08ba3f564067695d5ce0e6"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_disjoint_location_from_locations_not_mem",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_f6ab80eb5ffc2f5a5eff56ec5e04f3b2_1", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.Locations.disjoint_location_from_locations",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"interpretation_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"kinding_Vale.Transformers.Locations.location@tok",
"lemma_Vale.Transformers.Locations.auto_lemma_disjoint_location",
"primitive_Prims.op_Equality", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.mem",
"typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"unit_inversion", "unit_typing"
],
0,
"7b0fe149f52799f44fbe27f2d568bf13"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_difference_disjoint",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.Def.PossiblyMonad.Ok",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.Locations.disjoint_locations",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"interpretation_Tm_abs_0aead85000f7cb97bdedd109c8bf8424",
"kinding_Vale.Transformers.Locations.location@tok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok__a",
"projection_inverse_Vale.Def.PossiblyMonad.Ok_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.mem",
"typing_Tm_abs_0aead85000f7cb97bdedd109c8bf8424",
"typing_Vale.Transformers.BoundedInstructionEffects.difference",
"typing_Vale.Transformers.Locations.disjoint_location_from_locations",
"unit_inversion", "unit_typing"
],
0,
"ac670f8a08263d4b4c572094cb400eb7"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_except_to_at_difference",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.disjoint_locations",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.difference.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"interpretation_Tm_abs_0aead85000f7cb97bdedd109c8bf8424",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "true_interp",
"typing_Tm_abs_0aead85000f7cb97bdedd109c8bf8424",
"typing_Vale.Transformers.BoundedInstructionEffects.difference",
"unit_typing"
],
0,
"5e61cd3806441bfe6f6e0a4b1ac6322c"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_maintained",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"l_and-interp", "projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"subterm_ordering_Prims.Cons", "unit_inversion", "unit_typing"
],
0,
"3e9891d71a9744c88be07fe2622e89b8"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_parallel_aux1",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_parallel",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes"
],
0,
"31c73b6bbeb72d455108111ff41f3922"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_parallel_aux2",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_parallel",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes"
],
0,
"5ca4ae416138832a53e340da87059a82"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_parallel",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"b2t_def", "bool_inversion", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil", "data_elim_Prims.Mkdtuple2",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equation_FStar.Pervasives.Native.snd",
"equation_FStar.Pervasives.dfst", "equation_FStar.Pervasives.dsnd",
"equation_FStar.Pervasives.pattern", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_imp",
"equation_Prims.squash",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_parallel",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.X64.Machine_Semantics_s.st",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"fuel_guarded_inversion_Prims.dtuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Transformers.BoundedInstructionEffects.rw_set",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_FStar.Pervasives.pattern",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"l_and-interp", "l_imp-interp", "primitive_Prims.op_AmpAmp",
"proj_equation_Prims.Mkdtuple2__1",
"proj_equation_Prims.Mkdtuple2__2",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"true_interp", "typing_FStar.List.Tot.Base.mem",
"typing_FStar.Pervasives.Native.snd",
"typing_Vale.Transformers.BoundedInstructionEffects.intersect",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"unit_inversion", "unit_typing"
],
0,
"d1761e9e7686d8d46609b63a57ad5c38"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series_aux1",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
"bool_inversion", "disc_equation_Vale.Def.PossiblyMonad.Ok",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_series",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.X64.Machine_Semantics_s.st",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Prims.unit",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"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__2",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
"typing_FStar.Pervasives.Native.snd",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok"
],
0,
"3846e6aa5902a58927a163ddd53f4050"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series_aux2",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.Locations.location_eq",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"6598964ac018805a929abfc628da8bca"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series_aux2",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.mem.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_2eb22b38a6da10fb966327d892d8131d",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_eabe638ef4af4b0ec65b4cf7bbb2dc65",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"b2t_def", "binder_x_01ff889393c4884064895df8d812ac8f_0",
"binder_x_01ff889393c4884064895df8d812ac8f_1",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_f5fd149b4092a02f69e2db9e5a7d6c58_2",
"binder_x_f5fd149b4092a02f69e2db9e5a7d6c58_3", "bool_inversion",
"bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_Prims.Cons",
"data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_FStar.Pervasives.Native.snd",
"equation_FStar.Pervasives.pattern", "equation_Prims.eqtype",
"equation_Prims.l_True",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.locations_with_values",
"equation_Vale.Transformers.Locations.location_eq",
"equation_Vale.X64.Machine_Semantics_s.st",
"equation_with_fuel_FStar.List.Tot.Base.mem.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.constant_on_execution.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.intersect.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_FStar.Pervasives.pattern",
"function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"interpretation_Tm_abs_5c87c3d4a65a170b4b2411e823cba378",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"l_and-interp", "l_imp-interp", "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_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__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Mkdtuple2__2",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt",
"true_interp", "typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_5c87c3d4a65a170b4b2411e823cba378",
"typing_Vale.Transformers.BoundedInstructionEffects.intersect",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"unit_inversion", "unit_typing"
],
0,
"0cd421f003e95c384a142277639de952"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_except_disjoint",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.PossiblyMonad_interpretation_Tm_arrow_25069aaab7418caef2268a811fbde7da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_8dd1fd5b71cc5876f5829f120278e7c6",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_Vale.Def.PossiblyMonad.Ok",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equation_Prims.eqtype",
"equation_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.disjoint_locations",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_with_fuel_Vale.Def.PossiblyMonad.for_all.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"interpretation_Tm_abs_0aead85000f7cb97bdedd109c8bf8424",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons",
"typing_Tm_abs_0aead85000f7cb97bdedd109c8bf8424", "unit_inversion",
"unit_typing"
],
0,
"d10609939cd7c99b422798bb079d93d8"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series_aux3",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"bool_inversion", "equation_FStar.Pervasives.Native.snd",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_series",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok",
"unit_typing"
],
0,
"0df17359c420d7d651a6796da3596ecd"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_extend_append",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_irrelevance_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Transformers.Locations_pretyping_f6ab80eb5ffc2f5a5eff56ec5e04f3b2",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_8afd38cc1321157644dafce503e55d5a_4",
"binder_x_8afd38cc1321157644dafce503e55d5a_5",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_0",
"binder_x_a1d98a77e9eb6b7c546519b69ee90a88_1", "bool_inversion",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_typing_intro_Vale.Transformers.Locations.ALocStack@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Def.PossiblyMonad.Ok", "eq2-interp",
"equation_Prims.eqtype",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.location_val_t",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_Vale.Transformers.BoundedInstructionEffects.unchanged_at.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"kinding_Vale.Transformers.Locations.location@tok", "l_and-interp",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.append",
"unit_typing"
],
0,
"5edb933e1faf38c2ddb57ed2abe6b059"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series_aux4",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@query", "bool_inversion", "equation_FStar.Pervasives.Native.snd",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_series",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"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.Transformers.BoundedInstructionEffects.Mkrw_set_loc_reads",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok"
],
0,
"b7d6f3236974040484da3f11334947df"
],
[
"Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Transformers.Locations_interpretation_Tm_arrow_ab8903c152e18dfd3499672837d545e9",
"assumption_Prims.dtuple2__uu___haseq",
"assumption_Vale.Transformers.Locations.location__uu___haseq",
"b2t_def", "equation_Prims.eqtype", "equation_Prims.l_imp",
"equation_Prims.squash",
"equation_Vale.Transformers.BoundedInstructionEffects.bounded_effects",
"equation_Vale.Transformers.BoundedInstructionEffects.location_with_value",
"equation_Vale.Transformers.BoundedInstructionEffects.only_affects",
"equation_Vale.Transformers.BoundedInstructionEffects.rw_set_in_series",
"equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except",
"equation_Vale.Transformers.Locations.location_eq",
"fuel_guarded_inversion_Vale.Transformers.BoundedInstructionEffects.rw_set",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"function_token_typing_Vale.Transformers.Locations.location_val_eqt",
"haseqTm_refine_392b51d468236060fcf180188eadbab2",
"interpretation_Tm_abs_bb432d4e89d856bae603c4ee24fa9054",
"l_imp-interp",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"proj_equation_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_constant_writes",
"projection_inverse_Vale.Transformers.BoundedInstructionEffects.Mkrw_set_loc_writes",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2",
"token_correspondence_Vale.Transformers.Locations.location_val_eqt"
],
0,
"2db6a9da1278eec968a61ad43cfc0c5a"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...