[ "4\nhN\u0011\u001ag", [ [ "Vale.X64.Leakage.normalize_taints", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.FunctionalExtensionality.feq", "equation_Vale.X64.Leakage_Helpers.is_map_of", "equation_Vale.X64.Leakage_Helpers.map_to_regs", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "refinement_interpretation_Tm_refine_62740a77efccb19542fb67a4c3691e31" ], 0, "980f8260831c31816d258fd8dc1f3356" ], [ "Vale.X64.Leakage.eq_regs_file", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "binder_x_25f4b27a20f72ed456cefba9461105d5_2", "binder_x_9bc66468c4c7ad1611e8748185d6e29f_3", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.reg_file_id", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_46e1d323f68f206e5b156d1cf36df4aa", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "well-founded-ordering-on-nat" ], 0, "5a14300795869480e88661df1b9716db" ], [ "Vale.X64.Leakage.eq_regs", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "binder_x_b86c2548ce36a17f03fdb05cdd982de7_2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage_s.reg_taint", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "well-founded-ordering-on-nat" ], 0, "e525521cc5f61f315c06b1b63efe8680" ], [ "Vale.X64.Leakage.lemma_eq_regs_file", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_f28e87d0ee6421255c335311a8a84b75" ], 0, "1d64be069c3e457a213c0b634a8eb354" ], [ "Vale.X64.Leakage.lemma_eq_regs_file", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.eq_regs_file.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.eq_regs_file.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "binder_x_25f4b27a20f72ed456cefba9461105d5_2", "binder_x_9bc66468c4c7ad1611e8748185d6e29f_3", "binder_x_f95b232514c0666976149fc048b4ee0d_0", "binder_x_f95b232514c0666976149fc048b4ee0d_1", "bool_inversion", "constructor_distinct_Tm_unit", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_with_fuel_Vale.X64.Leakage.eq_regs_file.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_46e1d323f68f206e5b156d1cf36df4aa", "refinement_interpretation_Tm_refine_4cd2cd249de1c01a346e065af2ec7c1e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d73aed6819b8b1c98297560d1b9668ed", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "token_correspondence_Vale.X64.Leakage.eq_regs_file.fuel_instrumented", "typing_Vale.X64.Leakage.eq_regs_file", "typing_Vale.X64.Machine_s.n_regs", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "well-founded-ordering-on-nat" ], 0, "3d36e60dd7a75108d88321fd1923baa8" ], [ "Vale.X64.Leakage.lemma_eq_regs", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_8cea2e4b617b80cf60f40936cb37b63b" ], 0, "0498dbf2b65854d0016db72c61a25252" ], [ "Vale.X64.Leakage.lemma_eq_regs", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.eq_regs.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.eq_regs_file.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.eq_regs.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_b86c2548ce36a17f03fdb05cdd982de7_2", "binder_x_f95b232514c0666976149fc048b4ee0d_0", "binder_x_f95b232514c0666976149fc048b4ee0d_1", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_with_fuel_Vale.X64.Leakage.eq_regs.fuel_instrumented", "equation_with_fuel_Vale.X64.Leakage.eq_regs_file.fuel_instrumented", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_4cd2cd249de1c01a346e065af2ec7c1e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_e66ea0c882782f9094b0cbc1194ba71f", "typing_Vale.X64.Leakage.eq_regs", "typing_Vale.X64.Leakage.eq_regs_file", "well-founded-ordering-on-nat" ], 0, "8e1842bc9fd4aad7e1e8b677a6627e37" ], [ "Vale.X64.Leakage.eq_registers", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "bool_inversion", "data_elim_Vale.X64.Machine_s.Reg", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.nat", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "int_inversion", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Tm_abs_307d576cc835c0420dfededd9ce6b286" ], 0, "681f48f19c4abfa6c10f242a843cf127" ], [ "Vale.X64.Leakage.eq_leakage_taints", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6", "equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Vale.X64.Leakage.eq_registers", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_cfFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_f0ac051651fa0e095f1b2c1241fd6a3f", "typing_Vale.X64.Leakage.eq_registers", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "typing_tok_Vale.X64.Machine_s.Public@tok" ], 0, "b507b8f74cbb506f5b0cda0175a196ad" ], [ "Vale.X64.Leakage.taintstate_monotone_trans", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "fuel_guarded_inversion_Vale.X64.Leakage_s.analysis_taints" ], 0, "6d117fbeb72b90246176f8453461eca9" ], [ "Vale.X64.Leakage.isConstant_monotone", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "constructor_distinct_Vale.Arch.HeapTypes_s.Public", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Arch.HeapTypes_s.Public", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_s.constTimeInvariant", "equation_Vale.X64.Leakage_s.isConstantTimeGivenStates", "equation_Vale.X64.Leakage_s.publicCfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicOfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicRegisterValuesAreSame", "equation_Vale.X64.Leakage_s.publicValuesAreSame", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "projection_inverse_BoxBool_proj_0" ], 0, "f1581595db7069b8e63080d6fff6350d" ], [ "Vale.X64.Leakage.isExplicit_monotone", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.Public", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Arch.HeapTypes_s.Public", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.nat", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_s.isExplicitLeakageFreeGivenStates", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_lhs", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_rhs", "equation_Vale.X64.Leakage_s.publicCfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicOfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicRegisterValuesAreSame", "equation_Vale.X64.Leakage_s.publicValuesAreSame", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "int_inversion", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok" ], 0, "b66581f3a98bdece046326690e74929b" ], [ "Vale.X64.Leakage.isExplicit_monotone2", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.Public", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Arch.HeapTypes_s.Public", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equation_Prims.nat", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_s.constTimeInvariant", "equation_Vale.X64.Leakage_s.isExplicitLeakageFreeGivenStates", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_lhs", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_rhs", "equation_Vale.X64.Leakage_s.publicCfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicOfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicRegisterValuesAreSame", "equation_Vale.X64.Leakage_s.publicValuesAreSame", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "int_inversion", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code" ], 0, "299475e360bdc655b3726581df92f8be" ], [ "Vale.X64.Leakage.combine_analysis_taints", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Lib.MapTree_interpretation_Tm_arrow_6c9cf9481699be8541b47b0f2a7e6435", "Vale.X64.Leakage_interpretation_Tm_arrow_2f6c833369e35055127dbd1439006a7b", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "assumption_Vale.X64.Machine_s.reg__uu___haseq", "constructor_distinct_Vale.Arch.HeapTypes_s.Public", "constructor_distinct_Vale.Arch.HeapTypes_s.Secret", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "disc_equation_Vale.Arch.HeapTypes_s.Public", "disc_equation_Vale.Arch.HeapTypes_s.Secret", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.eqtype", "equation_Vale.X64.Leakage.combine_leakage_taints", "equation_Vale.X64.Leakage.combine_reg_taints", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_Helpers.is_map_of", "equation_Vale.X64.Leakage_Helpers.map_to_regs", "equation_Vale.X64.Leakage_Helpers.merge_taint", "equation_Vale.X64.Leakage_Helpers.regmap", "equation_Vale.X64.Leakage_s.reg_taint", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint", "function_token_typing_Vale.Lib.MapTree.sel", "interpretation_Tm_abs_307d576cc835c0420dfededd9ce6b286", "interpretation_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_BarBar", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_cfFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_cfFlagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_regTaint", "refinement_interpretation_Tm_refine_3e7d771a7450fcc18c8a6784192b51e0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "typing_Tm_abs_307d576cc835c0420dfededd9ce6b286", "typing_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b", "typing_Vale.X64.Leakage_Helpers.map_to_regs" ], 0, "55a11a19dd328b6f06ffef499f7ab6c1" ], [ "Vale.X64.Leakage.count_public_registers_file", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "binder_x_25f4b27a20f72ed456cefba9461105d5_1", "binder_x_dcbc15ec84993a13a5c8adbe4a462e70_2", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage.count_public_register", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.reg_file_id", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1dfac30f9bdb35d4448b600989375c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "well-founded-ordering-on-nat" ], 0, "54015a0ff789d5d0877b487bf39b6cca" ], [ "Vale.X64.Leakage.lemma_count_public_registers_file", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_ce801b332eeec7f68d5f37edf560ed63" ], 0, "ff79f293d358004b8f5178a1c7c08d63" ], [ "Vale.X64.Leakage.lemma_count_public_registers_file", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.count_public_registers_file.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.count_public_registers_file.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "binder_x_25f4b27a20f72ed456cefba9461105d5_2", "binder_x_9bc66468c4c7ad1611e8748185d6e29f_3", "binder_x_f95b232514c0666976149fc048b4ee0d_0", "binder_x_f95b232514c0666976149fc048b4ee0d_1", "bool_inversion", "bool_typing", "constructor_distinct_Tm_unit", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_Vale.Arch.HeapTypes_s.Public", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage.count_public_register", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_with_fuel_Vale.X64.Leakage.count_public_registers_file.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_307d576cc835c0420dfededd9ce6b286", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_GreaterThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_46e1d323f68f206e5b156d1cf36df4aa", "refinement_interpretation_Tm_refine_4cd2cd249de1c01a346e065af2ec7c1e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_cff8c70a69b33d31f739b88e10e7d233", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.X64.Leakage.count_public_register", "typing_Vale.X64.Leakage.count_public_registers_file", "typing_Vale.X64.Machine_s.n_regs", "well-founded-ordering-on-nat" ], 0, "07488fba926e72e6ae0380cd9857238d" ], [ "Vale.X64.Leakage.count_public_registers", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "binder_x_b86c2548ce36a17f03fdb05cdd982de7_1", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage_s.reg_taint", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "well-founded-ordering-on-nat" ], 0, "111bbf48102b4be330d32358dc391963" ], [ "Vale.X64.Leakage.lemma_count_public_registers", 1, 1, 0, [ "@query" ], 0, "9503f0c8d4c7012ec7f4362595c883d1" ], [ "Vale.X64.Leakage.lemma_count_public_registers", 2, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_b86c2548ce36a17f03fdb05cdd982de7_2", "binder_x_f95b232514c0666976149fc048b4ee0d_0", "binder_x_f95b232514c0666976149fc048b4ee0d_1", "constructor_distinct_Tm_unit", "data_elim_Vale.X64.Machine_s.Reg", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_with_fuel_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_GreaterThanOrEqual", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "typing_Vale.X64.Leakage.count_public_registers", "typing_Vale.X64.Machine_s.__proj__Reg__item__rf", "well-founded-ordering-on-nat" ], 0, "38e9689fde17b3d772115f336372566d" ], [ "Vale.X64.Leakage.count_publics", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.X64.Leakage.count_cfFlagTaint", "equation_Vale.X64.Leakage.count_flagTaint", "equation_Vale.X64.Leakage.count_ofFlagTaint", "equation_Vale.X64.Machine_s.n_reg_files", "fuel_guarded_inversion_Vale.X64.Leakage_s.analysis_taints", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Vale.X64.Leakage.count_cfFlagTaint", "typing_Vale.X64.Leakage.count_flagTaint", "typing_Vale.X64.Leakage.count_ofFlagTaint" ], 0, "3c3b15d4add8bf307b996c4f95dce29a" ], [ "Vale.X64.Leakage.monotone_decreases_count", 1, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "bool_inversion", "disc_equation_Vale.Arch.HeapTypes_s.Public", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.nat", "equation_Vale.X64.Leakage.count_cfFlagTaint", "equation_Vale.X64.Leakage.count_flagTaint", "equation_Vale.X64.Leakage.count_ofFlagTaint", "equation_Vale.X64.Leakage.count_publics", "equation_Vale.X64.Leakage.eq_leakage_taints", "equation_Vale.X64.Leakage.eq_registers", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.reg_file_id", "equation_with_fuel_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "int_inversion", "int_typing", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_cfFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "proj_equation_Vale.X64.Machine_s.Reg_rf", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f0ac051651fa0e095f1b2c1241fd6a3f", "typing_Tm_abs_307d576cc835c0420dfededd9ce6b286", "typing_Vale.Arch.HeapTypes_s.uu___is_Public", "typing_Vale.X64.Leakage.count_cfFlagTaint", "typing_Vale.X64.Leakage.count_flagTaint", "typing_Vale.X64.Leakage.count_ofFlagTaint", "typing_Vale.X64.Leakage.eq_leakage_taints", "typing_Vale.X64.Leakage.eq_registers", "typing_Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__lts", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__cfFlagsTaint", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__flagsTaint", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__ofFlagsTaint", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "typing_Vale.X64.Machine_s.__proj__Reg__item__rf" ], 0, "23cb44bb36a61e95f449500ecaa9239e" ], [ "Vale.X64.Leakage.check_if_block_consumes_fixed_time", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "binder_x_69b3af25a4334715774d1242034fc6f2_0", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons" ], 0, "ce2587b3fb9f04414d6201a5684f17a8" ], [ "Vale.X64.Leakage.check_if_block_consumes_fixed_time", 2, 1, 1, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_27cbc7f3c05302ce277bcd7aa3471f2f_1", "binder_x_97ef5ff619e486c846fe112d821f649f_0", "constructor_distinct_Vale.X64.Machine_s.While", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.IfElse", "disc_equation_Vale.X64.Machine_s.Ins", "disc_equation_Vale.X64.Machine_s.While", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Leakage.count_publics", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Machine_s.precode", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Machine_s.While_t_ins", "projection_inverse_Vale.X64.Machine_s.While_t_ocmp", "projection_inverse_Vale.X64.Machine_s.While_whileBody", "projection_inverse_Vale.X64.Machine_s.While_whileCond", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "subterm_ordering_Vale.X64.Machine_s.Block", "subterm_ordering_Vale.X64.Machine_s.IfElse", "well-founded-ordering-on-nat" ], 0, "ac744b7b347f6298658bf475d619b1b6" ], [ "Vale.X64.Leakage.check_if_block_consumes_fixed_time", 3, 1, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "@query", "binder_x_27cbc7f3c05302ce277bcd7aa3471f2f_1", "binder_x_79caa643a1f84363a39118336c0fa141_0", "bool_inversion", "data_elim_Vale.X64.Leakage_Helpers.AnalysisTaints", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Leakage.combine_analysis_taints", "equation_Vale.X64.Leakage.count_cfFlagTaint", "equation_Vale.X64.Leakage.count_flagTaint", "equation_Vale.X64.Leakage.count_ofFlagTaint", "equation_Vale.X64.Leakage.count_publics", "equation_Vale.X64.Leakage.eq_leakage_taints", "equation_Vale.X64.Leakage.normalize_taints", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.reg_64", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_typing", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9624fa14d86811de82228da4c47ef33b", "refinement_interpretation_Tm_refine_be712bac0d59aa5c3e46d732802ef0b6", "refinement_interpretation_Tm_refine_f0ac051651fa0e095f1b2c1241fd6a3f", "subterm_ordering_Vale.X64.Machine_s.While", "typing_Vale.X64.Leakage.combine_analysis_taints", "typing_Vale.X64.Leakage.count_cfFlagTaint", "typing_Vale.X64.Leakage.count_flagTaint", "typing_Vale.X64.Leakage.count_ofFlagTaint", "typing_Vale.X64.Leakage.count_public_registers", "typing_Vale.X64.Leakage.count_publics", "typing_Vale.X64.Leakage.eq_leakage_taints", "typing_Vale.X64.Leakage.normalize_taints", "typing_Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__lts", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "well-founded-ordering-on-nat" ], 0, "f985bd943c4e824c65252ff7cb75fbdb" ], [ "Vale.X64.Leakage.monotone_ok_eval", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_97ef5ff619e486c846fe112d821f649f_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_Vale.X64.Machine_s.Block", "constructor_distinct_Vale.X64.Machine_s.IfElse", "constructor_distinct_Vale.X64.Machine_s.Ins", "constructor_distinct_Vale.X64.Machine_s.While", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.IfElse", "disc_equation_Vale.X64.Machine_s.Ins", "disc_equation_Vale.X64.Machine_s.While", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "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_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "fuel_guarded_inversion_Vale.X64.Machine_s.precode", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins", "int_inversion", "interpretation_Tm_abs_342cdb3350d9f379a7c34e7ae187d821", "interpretation_Tm_abs_431565cf08dbebf07925447f42184424", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "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_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_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "projection_inverse_Vale.X64.Machine_s.IfElse_ifCond", "projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse", "projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue", "projection_inverse_Vale.X64.Machine_s.IfElse_t_ins", "projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp", "projection_inverse_Vale.X64.Machine_s.Ins_ins", "projection_inverse_Vale.X64.Machine_s.Ins_t_ins", "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp", "projection_inverse_Vale.X64.Machine_s.While_t_ins", "projection_inverse_Vale.X64.Machine_s.While_t_ocmp", "projection_inverse_Vale.X64.Machine_s.While_whileBody", "projection_inverse_Vale.X64.Machine_s.While_whileCond", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Vale.X64.Machine_s.Block", "subterm_ordering_Vale.X64.Machine_s.IfElse", "subterm_ordering_Vale.X64.Machine_s.While", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st", "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "unit_inversion", "unit_typing" ], 0, "4e0de9eb7f5a60bc0bf5bdb4fe8e44cf" ], [ "Vale.X64.Leakage.monotone_ok_eval", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "Prims_pretyping_e4836109f73687024ac3edd113084865", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "binder_x_69b3af25a4334715774d1242034fc6f2_0", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Tm_unit", "data_elim_FStar.Pervasives.Native.Some", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equality_tok_Prims.LexTop@tok", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "int_inversion", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok", "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", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Machine_Semantics_s.machine_eval_codes", "typing_tok_Prims.LexTop@tok" ], 0, "d373ad944262131804118b3669cb0256" ], [ "Vale.X64.Leakage.monotone_ok_eval_while", 1, 2, 0, [ "@MaxIFuel_assumption", "@query", "disc_equation_Vale.X64.Machine_s.While", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae" ], 0, "705d49b6d3fb18a7b463778a2db6d179" ], [ "Vale.X64.Leakage.monotone_ok_eval_while", 2, 2, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "bool_inversion", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.X64.Machine_s.While", "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "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_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "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.Machine_Semantics_s.Mkmachine_state_ms_ok", "projection_inverse_Vale.X64.Machine_s.While_t_ins", "projection_inverse_Vale.X64.Machine_s.While_t_ocmp", "projection_inverse_Vale.X64.Machine_s.While_whileBody", "projection_inverse_Vale.X64.Machine_s.While_whileCond", "refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_FStar.Pervasives.Native.uu___is_None", "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.machine_eval_code", "typing_Vale.X64.Machine_s.uu___is_While", "unit_inversion", "unit_typing" ], 0, "60d6a8d1796f64188d19040b30203896" ], [ "Vale.X64.Leakage.lemma_loop_taintstate_monotone", 1, 2, 1, [ "@query" ], 0, "518de8ab821576b4287d608027386dde" ], [ "Vale.X64.Leakage.lemma_loop_taintstate_monotone", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "@query", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.X64.Leakage_Helpers_pretyping_27cbc7f3c05302ce277bcd7aa3471f2f", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "assumption_Vale.X64.Machine_s.reg__uu___haseq", "binder_x_27cbc7f3c05302ce277bcd7aa3471f2f_0", "binder_x_79caa643a1f84363a39118336c0fa141_1", "bool_inversion", "constructor_distinct_Prims.unit", "constructor_distinct_Vale.X64.Machine_s.Public", "constructor_distinct_Vale.X64.Machine_s.Secret", "constructor_distinct_Vale.X64.Machine_s.taint", "data_elim_Vale.X64.Leakage_Helpers.AnalysisTaints", "data_elim_Vale.X64.Machine_s.OReg", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "data_typing_intro_Vale.X64.Machine_s.Secret@tok", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "disc_equation_Vale.X64.Machine_s.Public", "disc_equation_Vale.X64.Machine_s.While", "equality_tok_Prims.LexTop@tok", "equality_tok_Vale.X64.Machine_s.Public@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Leakage.combine_analysis_taints", "equation_Vale.X64.Leakage.count_cfFlagTaint", "equation_Vale.X64.Leakage.count_flagTaint", "equation_Vale.X64.Leakage.count_ofFlagTaint", "equation_Vale.X64.Leakage.count_publics", "equation_Vale.X64.Leakage.eq_leakage_taints", "equation_Vale.X64.Leakage.normalize_taints", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_Helpers.is_map_of", "equation_Vale.X64.Leakage_Helpers.map_to_regs", "equation_Vale.X64.Leakage_Helpers.merge_taint", "equation_Vale.X64.Leakage_Helpers.operand_does_not_use_secrets", "equation_Vale.X64.Leakage_Helpers.operand_taint", "equation_Vale.X64.Leakage_Helpers.regmap", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.get_fst_ocmp", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "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", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_with_fuel_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "equation_with_fuel_Vale.X64.Leakage.count_public_registers.fuel_instrumented", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "fuel_guarded_inversion_Vale.X64.Machine_s.operand", "fuel_guarded_inversion_Vale.X64.Machine_s.taint", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "int_typing", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_s.reg@tok", "kinding_Vale.X64.Machine_s.taint@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_cfFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "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_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_cfFlagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_regTaint", "projection_inverse_Vale.X64.Machine_s.While_t_ins", "projection_inverse_Vale.X64.Machine_s.While_t_ocmp", "projection_inverse_Vale.X64.Machine_s.While_whileBody", "projection_inverse_Vale.X64.Machine_s.While_whileCond", "refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_0d7abd59d64d4ac197ae128854a17b2f", "refinement_interpretation_Tm_refine_2a316e6bb489c60c1e3c65d294e230ff", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_62740a77efccb19542fb67a4c3691e31", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_83edcd5383b4192a26d2cf9296a55ae4", "refinement_interpretation_Tm_refine_901ef9a157d6e581ccfdb2ea4624d7c8", "refinement_interpretation_Tm_refine_be712bac0d59aa5c3e46d732802ef0b6", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f0ac051651fa0e095f1b2c1241fd6a3f", "typing_Tm_abs_a356ee6fc4458d630d8101a85a9a6019", "typing_Vale.Lib.MapTree.sel", "typing_Vale.X64.Leakage.combine_analysis_taints", "typing_Vale.X64.Leakage.count_cfFlagTaint", "typing_Vale.X64.Leakage.count_flagTaint", "typing_Vale.X64.Leakage.count_public_registers", "typing_Vale.X64.Leakage.count_publics", "typing_Vale.X64.Leakage.eq_leakage_taints", "typing_Vale.X64.Leakage.normalize_taints", "typing_Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__lts", "typing_Vale.X64.Leakage_Helpers.map_to_regs", "typing_Vale.X64.Leakage_Helpers.regs_to_map", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__cfFlagsTaint", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__flagsTaint", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__ofFlagsTaint", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "typing_Vale.X64.Machine_Semantics_s.get_fst_ocmp", "typing_Vale.X64.Machine_s.uu___is_Public", "typing_Vale.X64.Machine_s.uu___is_While", "unit_typing", "well-founded-ordering-on-nat" ], 0, "54348ae886c2fa6d023104b55c3431fc" ], [ "Vale.X64.Leakage.lemma_code_explicit_leakage_free", 1, 1, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.check_if_block_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_block_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Lib.MapTree_interpretation_Tm_arrow_6c9cf9481699be8541b47b0f2a7e6435", "Vale.X64.Leakage_Helpers_pretyping_27cbc7f3c05302ce277bcd7aa3471f2f", "Vale.X64.Leakage_interpretation_Tm_arrow_2f6c833369e35055127dbd1439006a7b", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "assumption_Vale.X64.Machine_s.reg__uu___haseq", "binder_x_27cbc7f3c05302ce277bcd7aa3471f2f_0", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_8afd38cc1321157644dafce503e55d5a_3", "binder_x_97ef5ff619e486c846fe112d821f649f_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion", "constructor_distinct_BoxBool", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Arch.HeapTypes_s.Public", "constructor_distinct_Vale.Arch.HeapTypes_s.Secret", "constructor_distinct_Vale.X64.Machine_s.Block", "constructor_distinct_Vale.X64.Machine_s.IfElse", "constructor_distinct_Vale.X64.Machine_s.Ins", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Bytes_Code_s.OEq", "data_elim_Vale.X64.Bytes_Code_s.OGe", "data_elim_Vale.X64.Bytes_Code_s.OGt", "data_elim_Vale.X64.Bytes_Code_s.OLe", "data_elim_Vale.X64.Bytes_Code_s.OLt", "data_elim_Vale.X64.Bytes_Code_s.ONe", "data_elim_Vale.X64.Leakage_Helpers.AnalysisTaints", "data_elim_Vale.X64.Leakage_s.LeakageTaints", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_elim_Vale.X64.Machine_s.IfElse", "data_elim_Vale.X64.Machine_s.OReg", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Arch.HeapTypes_s.Public", "disc_equation_Vale.Arch.HeapTypes_s.Secret", "disc_equation_Vale.X64.Machine_s.Block", "disc_equation_Vale.X64.Machine_s.IfElse", "disc_equation_Vale.X64.Machine_s.Ins", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "disc_equation_Vale.X64.Machine_s.While", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.Def.Words_s.nat64", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Leakage.combine_analysis_taints", "equation_Vale.X64.Leakage.combine_reg_taints", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_Helpers.is_map_of", "equation_Vale.X64.Leakage_Helpers.map_to_regs", "equation_Vale.X64.Leakage_Helpers.merge_taint", "equation_Vale.X64.Leakage_Helpers.operand_taint", "equation_Vale.X64.Leakage_Helpers.regmap", "equation_Vale.X64.Leakage_s.constTimeInvariant", "equation_Vale.X64.Leakage_s.isConstantTime", "equation_Vale.X64.Leakage_s.isConstantTimeGivenStates", "equation_Vale.X64.Leakage_s.isExplicitLeakageFree", "equation_Vale.X64.Leakage_s.isExplicitLeakageFreeGivenStates", "equation_Vale.X64.Leakage_s.isLeakageFree", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_lhs", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_rhs", "equation_Vale.X64.Leakage_s.publicCfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicMemValuesAreSame", "equation_Vale.X64.Leakage_s.publicOfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicRegisterValuesAreSame", "equation_Vale.X64.Leakage_s.publicStackValuesAreSame", "equation_Vale.X64.Leakage_s.publicValuesAreSame", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.get_fst_ocmp", "equation_Vale.X64.Machine_Semantics_s.get_snd_ocmp", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.n_reg_files", "equation_Vale.X64.Machine_s.n_regs", "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_id", "equation_with_fuel_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint", "fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "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.precode", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Lib.MapTree.sel", "function_token_typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "int_inversion", "int_typing", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_307d576cc835c0420dfededd9ce6b286", "interpretation_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "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_hd", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_regTaint", "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", "projection_inverse_Vale.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "projection_inverse_Vale.X64.Machine_s.BranchPredicate_pred", "projection_inverse_Vale.X64.Machine_s.IfElse_ifCond", "projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse", "projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue", "projection_inverse_Vale.X64.Machine_s.IfElse_t_ins", "projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp", "projection_inverse_Vale.X64.Machine_s.Ins_ins", "projection_inverse_Vale.X64.Machine_s.Ins_t_ins", "projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp", "projection_inverse_Vale.X64.Machine_s.While_whileBody", "projection_inverse_Vale.X64.Machine_s.While_whileCond", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_62740a77efccb19542fb67a4c3691e31", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_83edcd5383b4192a26d2cf9296a55ae4", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_be712bac0d59aa5c3e46d732802ef0b6", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f7310932e39ab0d875bcebe7584f986b", "subterm_ordering_Vale.X64.Machine_s.Block", "subterm_ordering_Vale.X64.Machine_s.IfElse", "token_correspondence_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "typing_FStar.FunctionalExtensionality.on_domain", "typing_FStar.Pervasives.Native.__proj__Some__item__v", "typing_Tm_abs_307d576cc835c0420dfededd9ce6b286", "typing_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b", "typing_Vale.Lib.MapTree.sel", "typing_Vale.X64.Leakage.check_if_code_consumes_fixed_time", "typing_Vale.X64.Leakage.combine_analysis_taints", "typing_Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__lts", "typing_Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__rts", "typing_Vale.X64.Leakage_Helpers.map_to_regs", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.get_fst_ocmp", "typing_Vale.X64.Machine_Semantics_s.get_snd_ocmp", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "well-founded-ordering-on-nat" ], 0, "648e726ee325dfb59a817da84522f5bf" ], [ "Vale.X64.Leakage.lemma_code_explicit_leakage_free", 2, 2, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.check_if_block_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_block_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "@query", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Vale.X64.Leakage_Helpers_pretyping_27cbc7f3c05302ce277bcd7aa3471f2f", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "binder_x_27cbc7f3c05302ce277bcd7aa3471f2f_0", "binder_x_69b3af25a4334715774d1242034fc6f2_1", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_8afd38cc1321157644dafce503e55d5a_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil", "constructor_distinct_Vale.X64.Machine_s.Block", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Leakage_Helpers.AnalysisTaints", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_typing_intro_Vale.X64.Machine_s.Block@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Bytes_Code_s.codes_t", "equation_Vale.X64.Leakage_s.constTimeInvariant", "equation_Vale.X64.Leakage_s.isConstantTimeGivenStates", "equation_Vale.X64.Leakage_s.isExplicitLeakageFreeGivenStates", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_lhs", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_rhs", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.codes", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_with_fuel_Vale.X64.Leakage.check_if_block_consumes_fixed_time.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_codes.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Prims.list", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state", "function_token_typing_Vale.X64.Machine_Semantics_s.ins", "int_inversion", "kinding_Vale.X64.Bytes_Code_s.ocmp@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_BarBar", "primitive_Prims.op_Negation", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "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__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.X64.Machine_s.Block_block", "projection_inverse_Vale.X64.Machine_s.Block_t_ins", "projection_inverse_Vale.X64.Machine_s.Block_t_ocmp", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "subterm_ordering_Prims.Cons", "typing_Vale.X64.Leakage.check_if_block_consumes_fixed_time", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "unit_inversion", "unit_typing" ], 0, "e4ada4a9066ad41733d11a79c274031d" ], [ "Vale.X64.Leakage.lemma_code_explicit_leakage_free", 3, 2, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "@fuel_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "@fuel_irrelevance_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a", "Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e", "Vale.Lib.MapTree_interpretation_Tm_arrow_6c9cf9481699be8541b47b0f2a7e6435", "Vale.X64.Bytes_Code_s_pretyping_8d8114524e962c921a106571a277b146", "Vale.X64.Leakage_Helpers_pretyping_27cbc7f3c05302ce277bcd7aa3471f2f", "Vale.X64.Leakage_interpretation_Tm_arrow_2f6c833369e35055127dbd1439006a7b", "Vale.X64.Leakage_s_pretyping_4717468dbe91703716dc7cf6a63e88f2", "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_eabe638ef4af4b0ec65b4cf7bbb2dc65", "Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a", "Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0", "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3", "Vale.X64.Machine_s_pretyping_8a3a692892c8a0ea1c9a86a6a3b7d69f", "assumption_Vale.X64.Machine_s.reg__uu___haseq", "binder_x_27cbc7f3c05302ce277bcd7aa3471f2f_0", "binder_x_79caa643a1f84363a39118336c0fa141_1", "binder_x_8afd38cc1321157644dafce503e55d5a_2", "binder_x_8afd38cc1321157644dafce503e55d5a_3", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion", "bool_typing", "constructor_distinct_BoxBool", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.Arch.HeapTypes_s.Public", "constructor_distinct_Vale.Arch.HeapTypes_s.Secret", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_elim_FStar.Pervasives.Native.Some", "data_elim_Vale.X64.Bytes_Code_s.OEq", "data_elim_Vale.X64.Bytes_Code_s.OGe", "data_elim_Vale.X64.Bytes_Code_s.OGt", "data_elim_Vale.X64.Bytes_Code_s.OLe", "data_elim_Vale.X64.Bytes_Code_s.OLt", "data_elim_Vale.X64.Bytes_Code_s.ONe", "data_elim_Vale.X64.Leakage_Helpers.AnalysisTaints", "data_elim_Vale.X64.Leakage_s.LeakageTaints", "data_elim_Vale.X64.Machine_Semantics_s.Mkmachine_state", "data_elim_Vale.X64.Machine_s.OReg", "data_elim_Vale.X64.Machine_s.While", "data_typing_intro_Vale.Arch.HeapTypes_s.Secret@tok", "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "disc_equation_Vale.Arch.HeapTypes_s.Public", "disc_equation_Vale.Arch.HeapTypes_s.Secret", "disc_equation_Vale.X64.Machine_s.OMem", "disc_equation_Vale.X64.Machine_s.OStack", "disc_equation_Vale.X64.Machine_s.While", "equality_tok_Vale.Arch.HeapTypes_s.Public@tok", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_FStar.FunctionalExtensionality.is_restricted", "equation_FStar.FunctionalExtensionality.restricted_t", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Pervasives.pattern", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_Vale.X64.Bytes_Code_s.code_t", "equation_Vale.X64.Leakage.combine_analysis_taints", "equation_Vale.X64.Leakage.combine_reg_taints", "equation_Vale.X64.Leakage.eq_leakage_taints", "equation_Vale.X64.Leakage.normalize_taints", "equation_Vale.X64.Leakage.taintstate_monotone", "equation_Vale.X64.Leakage.taintstate_monotone_regs", "equation_Vale.X64.Leakage_Helpers.is_map_of", "equation_Vale.X64.Leakage_Helpers.map_to_regs", "equation_Vale.X64.Leakage_Helpers.merge_taint", "equation_Vale.X64.Leakage_Helpers.operand_does_not_use_secrets", "equation_Vale.X64.Leakage_Helpers.operand_taint", "equation_Vale.X64.Leakage_Helpers.regmap", "equation_Vale.X64.Leakage_s.constTimeInvariant", "equation_Vale.X64.Leakage_s.isConstantTimeGivenStates", "equation_Vale.X64.Leakage_s.isExplicitLeakageFreeGivenStates", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_lhs", "equation_Vale.X64.Leakage_s.is_explicit_leakage_free_rhs", "equation_Vale.X64.Leakage_s.publicCfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicMemValuesAreSame", "equation_Vale.X64.Leakage_s.publicOfFlagValuesAreSame", "equation_Vale.X64.Leakage_s.publicRegisterValuesAreSame", "equation_Vale.X64.Leakage_s.publicStackValuesAreSame", "equation_Vale.X64.Leakage_s.publicValuesAreSame", "equation_Vale.X64.Leakage_s.reg_taint", "equation_Vale.X64.Machine_Semantics_s.cf", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_Semantics_s.eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.eval_operand", "equation_Vale.X64.Machine_Semantics_s.flags_none", "equation_Vale.X64.Machine_Semantics_s.get_fst_ocmp", "equation_Vale.X64.Machine_Semantics_s.get_snd_ocmp", "equation_Vale.X64.Machine_Semantics_s.havoc_flags", "equation_Vale.X64.Machine_Semantics_s.machine_eval_ocmp", "equation_Vale.X64.Machine_Semantics_s.ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_ocmp", "equation_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "equation_Vale.X64.Machine_s.flag", "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", "equation_Vale.X64.Machine_s.reg_file_id", "equation_Vale.X64.Machine_s.reg_id", "equation_with_fuel_Vale.X64.Leakage.check_if_code_consumes_fixed_time.fuel_instrumented", "equation_with_fuel_Vale.X64.Leakage.check_if_loop_consumes_fixed_time.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented", "equation_with_fuel_Vale.X64.Machine_Semantics_s.machine_eval_while.fuel_instrumented", "fuel_guarded_inversion_FStar.Pervasives.Native.option", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.Arch.HeapTypes_s.taint", "fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp", "fuel_guarded_inversion_Vale.X64.Leakage_Helpers.analysis_taints", "fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints", "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.precode", "fuel_guarded_inversion_Vale.X64.Machine_s.reg", "function_token_typing_FStar.Pervasives.pattern", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Lib.MapTree.sel", "function_token_typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "function_token_typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "function_token_typing_Vale.X64.Machine_Semantics_s.eval_ocmp_opaque", "function_token_typing_Vale.X64.Machine_Semantics_s.flags_none", "function_token_typing_Vale.X64.Machine_Semantics_s.valid_ocmp_opaque", "int_inversion", "int_typing", "interpretation_Tm_abs_275a4a20fec2a36f25eb34b853a79209", "interpretation_Tm_abs_307d576cc835c0420dfededd9ce6b286", "interpretation_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b", "interpretation_Tm_abs_b085815e1140e9a069ea4cab83d07665", "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d", "interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366", "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "kinding_Vale.Arch.HeapTypes_s.taint@tok", "kinding_Vale.X64.Machine_Semantics_s.machine_state@tok", "kinding_Vale.X64.Machine_s.reg@tok", "lemma_FStar.FunctionalExtensionality.extensionality", "lemma_FStar.FunctionalExtensionality.feq_on_domain", "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "proj_equation_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_ofFlagsTaint", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "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_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Prims.Cons_tl", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_lts", "projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_rts", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_flagsTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_regTaint", "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", "projection_inverse_Vale.X64.Machine_s.While_whileBody", "projection_inverse_Vale.X64.Machine_s.While_whileCond", "refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae", "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81", "refinement_interpretation_Tm_refine_2a316e6bb489c60c1e3c65d294e230ff", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_62740a77efccb19542fb67a4c3691e31", "refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64", "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e", "refinement_interpretation_Tm_refine_83edcd5383b4192a26d2cf9296a55ae4", "refinement_interpretation_Tm_refine_ba365082b22759c5ffc3f70184bff703", "refinement_interpretation_Tm_refine_be712bac0d59aa5c3e46d732802ef0b6", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64", "refinement_interpretation_Tm_refine_f0ac051651fa0e095f1b2c1241fd6a3f", "refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64", "token_correspondence_Vale.Lib.MapTree.sel", "token_correspondence_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_regs", "token_correspondence_Vale.X64.Machine_Semantics_s.flags_none", "typing_FStar.FunctionalExtensionality.on_domain", "typing_FStar.Pervasives.Native.snd", "typing_FStar.Pervasives.Native.uu___is_None", "typing_FStar.Pervasives.Native.uu___is_Some", "typing_Tm_abs_307d576cc835c0420dfededd9ce6b286", "typing_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b", "typing_Tm_abs_f086d77986b470aab4bfebc171e6c366", "typing_Tm_abs_ff856a54708216dbc469f39ac4b5748e", "typing_Vale.Lib.MapTree.sel", "typing_Vale.X64.Leakage.check_if_code_consumes_fixed_time", "typing_Vale.X64.Leakage.check_if_loop_consumes_fixed_time", "typing_Vale.X64.Leakage.combine_analysis_taints", "typing_Vale.X64.Leakage.eq_leakage_taints", "typing_Vale.X64.Leakage.normalize_taints", "typing_Vale.X64.Leakage_Helpers.__proj__AnalysisTaints__item__lts", "typing_Vale.X64.Leakage_Helpers.map_to_regs", "typing_Vale.X64.Leakage_Helpers.regs_to_map", "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint", "typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_ok", "typing_Vale.X64.Machine_Semantics_s.eval_operand", "typing_Vale.X64.Machine_Semantics_s.get_fst_ocmp", "typing_Vale.X64.Machine_Semantics_s.get_snd_ocmp", "typing_Vale.X64.Machine_Semantics_s.machine_eval_code", "typing_Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint", "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "unit_inversion", "unit_typing", "well-founded-ordering-on-nat" ], 0, "61c5eb39e91e55b065e9d5e09d0aa3ed" ], [ "Vale.X64.Leakage.lemma_code_leakage_free", 1, 1, 2, [ "@MaxIFuel_assumption", "@query", "equation_Vale.X64.Leakage_s.isConstantTime", "equation_Vale.X64.Leakage_s.isExplicitLeakageFree", "equation_Vale.X64.Leakage_s.isLeakageFree", "fuel_guarded_inversion_Vale.X64.Leakage_s.analysis_taints" ], 0, "d41d48d0e1d39d02d9fef9a35de3082c" ], [ "Vale.X64.Leakage.check_if_code_is_leakage_free'", 1, 1, 2, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Vale.X64.Leakage_s.isLeakageFree", "fuel_guarded_inversion_Vale.X64.Leakage_s.analysis_taints" ], 0, "0eacd2e7f843d6be1ed47ea281cb81d7" ], [ "Vale.X64.Leakage.check_if_code_is_leakage_free", 1, 1, 2, [ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ], 0, "cfd6f92ff3d8974f5273e0afb94fb88d" ], [ "Vale.X64.Leakage.mk_analysis_taints", 1, 1, 2, [ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.FunctionalExtensionality.feq", "equation_Vale.X64.Leakage_Helpers.is_map_of", "proj_equation_Vale.X64.Leakage_s.LeakageTaints_regTaint", "projection_inverse_Vale.X64.Leakage_s.LeakageTaints_regTaint" ], 0, "071ecff9b2176047beea2480add5a22f" ] ] ]