[ "$\u0006d?O^Cϐm", [ [ "Vale.Transformers.BoundedInstructionEffects.rw_set", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "kinding_Vale.Transformers.Locations.location@tok", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt", "typing_tok_Vale.Transformers.Locations.ALocMem@tok" ], 0, "665f1468deeceddd9839bcf527392ad6" ], [ "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, "f690ab5d6716d6c5a17f4d53df1a6e83" ], [ "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, "f99a04749048c603203564c8cf58c5aa" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5ac03f3dbd47c28b1ddf6245e0480621" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f391aab0cc9988f1b03591cb3a820fe6" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "c4d122af37b2f7e725d6e2ef20ef483b" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "9adbea2991b1d5dae5ef8d0f3d070406" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 6, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "7ebd219ebf636f1a1686b18c94aeec66" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 7, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "2cceb1b5e3d00ea5611f38a51e07dc18" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 8, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "3de8febd10cdc66b26fe75965bb1311f" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand64", 9, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "48cb4350d692939341980686418f3a00" ], [ "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, "1c8214c6981e024fa5c67a034f519594" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand128", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "535f03e255d5723b75e0cb9fa740ba69" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand128", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "4b2d2b99100170b41304ef2eef70f278" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand128", 4, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d566b7e25adcf016f03c1e08f33a074e" ], [ "Vale.Transformers.BoundedInstructionEffects.locations_of_operand128", 5, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "832970a88efe7b38b34da34d8b7f805d" ], [ "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, "9a0ab0c6a9379162e3428b17a75c61a6" ], [ "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, "86d6b3e75f883ae8532d8c8b73fee3a8" ], [ "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, "9ba98462d72c07cc9aa5fe27ba1dadd1" ], [ "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.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", "primitive_Prims.op_AmpAmp", "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__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, "f8f9acb0c2a64f005ee5ffc96846ffc8" ], [ "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, "6c4f80a2942fb559e6fc773e4846fb5c" ], [ "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, "2276865a3817908978842a811ebd29f8" ], [ "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, "5ef5bef4f86f0ddca9b42be0270305dd" ], [ "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, "63d236658b5d9bf781d4ded32f035e9e" ], [ "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, "ee5de9f61106b907d8b4348032454d23" ], [ "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, "8174b2a92e98fc9b84efed7714101aca" ], [ "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, "331b47675fdf0a01d50dc11a68e013cf" ], [ "Vale.Transformers.BoundedInstructionEffects.bounded_effects", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "8b916d9fccae60e4f9c0828902aaabc6" ], [ "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, "ecc9628ba449e9973584e862d0400851" ], [ "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, "304455f404d66b9355adbef65fae14ed" ], [ "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, "a66cd23187fd7bec94ff6c4240a201e7" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_ins_st_only_affects_write", 1, 1, 0, [ "@query", "equation_Vale.Transformers.BoundedInstructionEffects.unchanged_except" ], 0, "19d2a7ec361fddb4220aeb29f12d0138" ], [ "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, "caba13f7b28f515e313d30d39b34f14c" ], [ "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, "3efd94268d5a19c25b609f8114e7ed5d" ], [ "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, "f3131864b9875d898a319c80e29f6a05" ], [ "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", "constructor_distinct_Vale.X64.Instruction_s.IOpIm", "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_Prims.op_Equals_Equals_Equals", "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_FStar.Pervasives.Native.option", "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, "a40c7ef202c0dec29bb58faf6f265c99" ], [ "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", "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", "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.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.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_Prims.op_Equals_Equals_Equals", "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.eval_maddr", "equation_Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "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.option", "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", "function_token_typing_Vale.Transformers.Locations.locations", "int_inversion", "int_typing", "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", "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_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, "af243693930c4f50516dc408a27ca818" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_instr_apply_eval_same_read", 1, 1, 0, [ "@query", "equation_Vale.X64.Machine_Semantics_s.instr_apply_eval" ], 0, "e06ecd270a7937a28edc502732143544" ], [ "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, "929e74320a945156758c92c07b728738" ], [ "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, "4112b3b1d281082eb7d06d2b06f9f512" ], [ "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, "b51b02a03ac7648016c69186d00aefe7" ], [ "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, "3414b349a04ecc16537de48d2293a3a1" ], [ "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, "08d32a7029f0f4dc4b950237260904a8" ], [ "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", "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", "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.pattern", "equation_Prims.eqtype", "equation_Prims.op_Equals_Equals_Equals", "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", "fuel_guarded_inversion_Vale.Transformers.Locations.location", "function_token_typing_FStar.Pervasives.pattern", "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.append", "typing_Tm_abs_7b764ec327b3dd0ec2b72c5139c0f8d5", "typing_Vale.Def.PossiblyMonad.op_Amp_Amp_Dot", "typing_Vale.Def.PossiblyMonad.uu___is_Ok", "typing_Vale.Transformers.Locations.disjoint_location_from_locations", "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" ], 0, "540712de37abfeac22afa88e0a3ff647" ], [ "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, "8750d1e4d73937a6956064de2d7cfa14" ], [ "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, "65e57d807a0317a2209415cc88948982" ], [ "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, "d07c36d925039c8936ea537f0575c7fa" ], [ "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, "0a3fdac49830e681cee649a6cb599361" ], [ "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, "9eed56c59e19c298e062498cd164ccb9" ], [ "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, "27e4aa0da9d5b9f6c41791ba80ee8541" ], [ "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, "435958206bfc8a7b30f2b379b2e3942b" ], [ "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, "994d36312a10342e29d3d746e8849634" ], [ "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.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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.X64.Machine_Semantics_s.machine_eval_ins_st", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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", "typing_FStar.List.Tot.Base.mem", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.BoundedInstructionEffects.aux_write_set", "typing_Vale.Transformers.BoundedInstructionEffects.constant_writes", "typing_Vale.Transformers.BoundedInstructionEffects.write_set", "typing_Vale.Transformers.Locations.location_val_eqt", "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, "bce1e3d5187f739660c1a3161e0dcbcf" ], [ "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, "fac1f6b94f068bf413fdefd217d81114" ], [ "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, "9a061883188ee4b693d8e1d4b4c4d0a3" ], [ "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, "27e356ca85fc23a74fa1e254f428d5c1" ], [ "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, "0bde3dfe6df7f58952284ec18ef0b42e" ], [ "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, "5dcd467075b89906984fd2d492e2a8d4" ], [ "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, "507110dfc1ea34cc44b5e9dd4b22aef7" ], [ "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, "9983555e9521e01493232a4dece4f2ab" ], [ "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.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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", "typing_FStar.List.Tot.Base.mem", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "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.Transformers.Locations.location_val_eqt", "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, "8ed3acc8f2dc50adbcdd1a4fb5d766ed" ], [ "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, "e849f1ffc1b0abe4455cef3a65ab529a" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_machine_eval_code_Ins_bounded_effects", 2, 1, 0, [ "@query", "equation_Vale.Transformers.BoundedInstructionEffects.machine_eval_code_Ins" ], 0, "610b1de11ad034d047466d925f4f7b70" ], [ "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, "af51aa4fc8eea8fcca59f1e505949f91" ], [ "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", "equation_Prims.op_Equals_Equals_Equals", "fuel_guarded_inversion_Prims.list", "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, "0cce139294249c02f86ad22dc56ec1f9" ], [ "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", "equation_Prims.op_Equals_Equals_Equals", "fuel_guarded_inversion_Prims.list", "projection_inverse_BoxBool_proj_0", "subterm_ordering_Prims.Cons" ], 0, "f9ef4c2c0c6c76f7b5501044e06fbba1" ], [ "Vale.Transformers.BoundedInstructionEffects.rw_set_in_parallel", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "cfcb81c653de0a66e586384f44af0836" ], [ "Vale.Transformers.BoundedInstructionEffects.rw_set_in_series", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "24c38ce8e2ee06ae47136e4c921f828a" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_constant_on_execution_mem", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "cf1a55f56345a4e9c90cf74b95d842a3" ], [ "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.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit", "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_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.Transformers.BoundedInstructionEffects.location_with_value", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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_a", "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", "typing_FStar.List.Tot.Base.mem", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "3eacd90315009931dea2552d72472abf" ], [ "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, "de45bf96700c0d0ecfe8f1f0c53775ca" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_constant_intersect_belongs_to_writes_union", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "34f20e844f7fd3762d96789b317ffe0a" ], [ "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.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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", "typing_FStar.List.Tot.Base.mem", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.BoundedInstructionEffects.intersect", "typing_Vale.Transformers.Locations.location_val_eqt", "unit_inversion", "unit_typing" ], 0, "4e936e62063669c434cea230740f7a7a" ], [ "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, "4889bb4e038657b5e9b3c09ad217fe71" ], [ "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, "5dd54279b2cc5d7e2c307afa46a031f4" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_unchanged_at_sym_diff_implies_difference", 1, 1, 0, [ "@query", "equation_Vale.Transformers.BoundedInstructionEffects.sym_difference" ], 0, "8219cc122bf4bada0a4e53610d85a7ff" ], [ "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, "749c544f444a653ce5e37e44225a96ce" ], [ "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, "cbe8213168359a703e821d486e4518ae" ], [ "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, "d01900974921f3c51d1b5fa96b02e873" ], [ "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, "9be2c19fc3c884a5ce6807b540e18267" ], [ "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, "6d59a1dc1e66223670e26304fb750631" ], [ "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, "a2a885f5787d922d2f4c46ec75bf1011" ], [ "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.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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.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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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", "true_interp", "typing_FStar.List.Tot.Base.mem", "typing_FStar.Pervasives.Native.snd", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.BoundedInstructionEffects.intersect", "typing_Vale.Transformers.Locations.location_val_eqt", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "unit_inversion", "unit_typing" ], 0, "c33f8a9682f86a91d43b65fbf393178a" ], [ "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, "e28fa7e499c4b253fc2d0453fca3ba76" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series_aux2", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "refinement_interpretation_Tm_refine_392b51d468236060fcf180188eadbab2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_Tm_refine_392b51d468236060fcf180188eadbab2", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "4361f1b21af0ac6647e5c3ce0f51d974" ], [ "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.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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", "true_interp", "typing_FStar.Pervasives.Native.snd", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Tm_abs_5c87c3d4a65a170b4b2411e823cba378", "typing_Vale.Transformers.BoundedInstructionEffects.intersect", "typing_Vale.Transformers.Locations.location_val_eqt", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "unit_inversion", "unit_typing" ], 0, "1829384b3570603df8d0a3d431cc39ed" ], [ "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, "a1ea62e8d47f7f9e485b1cfb50e9b9a0" ], [ "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, "900778c55fd4f83f9267008744da56f7" ], [ "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, "4193959e40ba3fd020515259bb9d8e28" ], [ "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, "fa1f7085cfb47547a00000f3a81dd0cd" ], [ "Vale.Transformers.BoundedInstructionEffects.lemma_bounded_effects_series", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Transformers.BoundedInstructionEffects_interpretation_Tm_arrow_e620a04edac012a53c47403a0ec32e8b", "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", "haseqTm_refine_392b51d468236060fcf180188eadbab2", "interpretation_Tm_abs_452830438df0c858dc7aff64408b4299", "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", "typing_Tm_abs_452830438df0c858dc7aff64408b4299", "typing_Vale.Transformers.Locations.location_val_eqt" ], 0, "0f04a54c7453cf0833bd49fcc8636547" ] ] ]