Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.X64.Leakage.fst.hints
[
"ư\u0013\u0016\u001e��\u001eN(\u001a{��",
[
[
"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,
"d8a1a24e08672446e8d0a5d65b274688"
],
[
"Vale.X64.Leakage.eq_regs_file",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_25f4b27a20f72ed456cefba9461105d5_2",
"binder_x_9bc66468c4c7ad1611e8748185d6e29f_3",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"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,
"82a9f1ad6057d96fc1a279b5a79394e9"
],
[
"Vale.X64.Leakage.eq_regs",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_b86c2548ce36a17f03fdb05cdd982de7_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"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,
"4b86c26adeb03e38722e246f5c79869a"
],
[
"Vale.X64.Leakage.lemma_eq_regs_file",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_05a30d0ade8c6c0091e9413c657014a5"
],
0,
"413e09fc0fed41215a3cc87080840428"
],
[
"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.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"binder_x_25f4b27a20f72ed456cefba9461105d5_2",
"binder_x_9bc66468c4c7ad1611e8748185d6e29f_3",
"binder_x_f95b232514c0666976149fc048b4ee0d_0",
"binder_x_f95b232514c0666976149fc048b4ee0d_1", "bool_inversion",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
"equation_Vale.X64.Leakage_s.reg_taint",
"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_d9979b96a3f2b18961b3dd63a2783b64",
"refinement_interpretation_Tm_refine_f21b705850dd99cd47914be8e228c25c",
"typing_Vale.X64.Leakage.eq_regs_file",
"typing_tok_Vale.X64.Machine_s.Public@tok",
"well-founded-ordering-on-nat"
],
0,
"07acb07d82616944592d7ea3413c6a3d"
],
[
"Vale.X64.Leakage.lemma_eq_regs",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_41417e2bce755e946fbf0de9fb4be971"
],
0,
"ee0a7050c2f14941b5618f32c77afd4e"
],
[
"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", "equality_tok_Prims.LexTop@tok",
"equation_Prims.nat", "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,
"a959ed7198556d333f4934d4b946dc83"
],
[
"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_a356ee6fc4458d630d8101a85a9a6019"
],
0,
"b6feac7ed4f1ac3c81c73b735ca173a8"
],
[
"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,
"d32153af936f21e954552a2f9d5ddc5c"
],
[
"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,
"4684cbb8b3882a37044be8388dacf618"
],
[
"Vale.X64.Leakage.isConstant_monotone",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"constructor_distinct_Vale.X64.Machine_s.Public",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Public",
"equality_tok_Vale.X64.Machine_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,
"949ff1c3d6bd4f0e32a19e689cd277fe"
],
[
"Vale.X64.Leakage.isExplicit_monotone",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"bool_inversion", "constructor_distinct_Vale.X64.Machine_s.Public",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Public",
"equality_tok_Vale.X64.Machine_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,
"a8437e4e19dc8a6954d132860c90f11d"
],
[
"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.X64.Machine_s.Public",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Public",
"equality_tok_Vale.X64.Machine_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,
"855d51352dc8db7eb2382743cdb2db7e"
],
[
"Vale.X64.Leakage.combine_analysis_taints",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.Lib.MapTree_interpretation_Tm_arrow_6c9cf9481699be8541b47b0f2a7e6435",
"Vale.X64.Leakage_interpretation_Tm_arrow_dafd0fd94fe6025dc9e2cc7dfb03cd02",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"assumption_Vale.X64.Machine_s.reg__uu___haseq",
"constructor_distinct_Vale.X64.Machine_s.Public",
"constructor_distinct_Vale.X64.Machine_s.Secret",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_Vale.X64.Machine_s.Public",
"disc_equation_Vale.X64.Machine_s.Secret",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equality_tok_Vale.X64.Machine_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.X64.Machine_s.taint",
"function_token_typing_Vale.Lib.MapTree.sel",
"interpretation_Tm_abs_2c843006472a19cdcec8325c8a6a91a4",
"interpretation_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"kinding_Vale.X64.Machine_s.reg@tok",
"kinding_Vale.X64.Machine_s.taint@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_2c843006472a19cdcec8325c8a6a91a4",
"typing_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"typing_Vale.X64.Leakage_Helpers.map_to_regs"
],
0,
"74cc2fc549e29f9bde18faf13c330a79"
],
[
"Vale.X64.Leakage.count_public_registers_file",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_25f4b27a20f72ed456cefba9461105d5_1",
"binder_x_dcbc15ec84993a13a5c8adbe4a462e70_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"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,
"b93a0736925ca8aa81e44ae3d304400e"
],
[
"Vale.X64.Leakage.lemma_count_public_registers_file",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_988d466cfe4591206c49030513719ab1"
],
0,
"8085b228966c0f112e9f02c7e80f4de1"
],
[
"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.X64.Machine_s.Public",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_Prims.nat",
"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.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.Machine_s.taint",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"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_c5088922aab857ddcdcdfb467d53a09f",
"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,
"06f4c7b88aea242a648e71ff1cc1abff"
],
[
"Vale.X64.Leakage.count_public_registers",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_b86c2548ce36a17f03fdb05cdd982de7_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"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,
"b8f349d5f2b48e32a19a09fe2b05d4ca"
],
[
"Vale.X64.Leakage.lemma_count_public_registers",
1,
1,
0,
[ "@query" ],
0,
"761f0f67ea01d4541d5ca04024c35f5a"
],
[
"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",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"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,
"ea34bfc03f331f326c7d1972ae19030a"
],
[
"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,
"0a53aa4ff3bae6f5997bd2af61fcc508"
],
[
"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.X64.Machine_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.X64.Leakage_Helpers.analysis_taints",
"fuel_guarded_inversion_Vale.X64.Leakage_s.leakage_taints",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"fuel_guarded_inversion_Vale.X64.Machine_s.taint",
"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_a356ee6fc4458d630d8101a85a9a6019",
"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",
"typing_Vale.X64.Machine_s.uu___is_Public"
],
0,
"599b8dd5d436561c3e5c207999302fed"
],
[
"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,
"4311a5b493b51357594ae7e4e627b814"
],
[
"Vale.X64.Leakage.check_if_block_consumes_fixed_time",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"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",
"equality_tok_Prims.LexTop@tok", "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.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.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",
"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,
"1e553d9c835d0ce5ba1da197a213fb80"
],
[
"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",
"disc_equation_Vale.X64.Machine_s.While", "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.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_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_lts",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"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,
"0b58c8e2bcd363e6ae5ce7288cc98a68"
],
[
"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",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"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_ins",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
"equation_Vale.X64.Machine_Semantics_s.machine_eval_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__",
"int_inversion",
"interpretation_Tm_abs_1f233bb62d19e8ce94de2fc1626a49a7",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"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_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_flags",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifCond",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifFalse",
"projection_inverse_Vale.X64.Machine_s.IfElse_ifTrue",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ins",
"projection_inverse_Vale.X64.Machine_s.IfElse_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.Ins_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ins",
"projection_inverse_Vale.X64.Machine_s.Ins_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_t_ins",
"projection_inverse_Vale.X64.Machine_s.While_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.While_whileBody",
"projection_inverse_Vale.X64.Machine_s.While_whileCond",
"refinement_interpretation_Tm_refine_00a7f4f660dc1fda2a82818f3e83adae",
"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_ins_st",
"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,
"31a0aa364759b079b05daa1de3e07cb4"
],
[
"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",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"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_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.machine_eval_code"
],
0,
"063251f73070e6cbe1a60a7f49106abc"
],
[
"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,
"f27edf1a650072c8d86e5f15688bfe53"
],
[
"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", "bool_typing",
"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_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,
"b0855753f8ae0d1d61791f6c52b89069"
],
[
"Vale.X64.Leakage.lemma_loop_taintstate_monotone",
1,
2,
1,
[ "@query" ],
0,
"3f241d5f3321517f576013c1c7fe0412"
],
[
"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,
"d240cb2158d992bce1c99efacf4f87c9"
],
[
"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_e4836109f73687024ac3edd113084865",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Lib.MapTree_interpretation_Tm_arrow_6c9cf9481699be8541b47b0f2a7e6435",
"Vale.X64.Leakage_Helpers_pretyping_27cbc7f3c05302ce277bcd7aa3471f2f",
"Vale.X64.Leakage_interpretation_Tm_arrow_dafd0fd94fe6025dc9e2cc7dfb03cd02",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"Vale.X64.Machine_s_interpretation_Tm_arrow_a3d9ef307178ed6e6eb0fe5485c5ade0",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"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",
"bool_typing", "constructor_distinct_BoxBool",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Block",
"constructor_distinct_Vale.X64.Machine_s.IfElse",
"constructor_distinct_Vale.X64.Machine_s.Ins",
"constructor_distinct_Vale.X64.Machine_s.Public",
"constructor_distinct_Vale.X64.Machine_s.Secret",
"constructor_distinct_Vale.X64.Machine_s.While",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_Vale.X64.Bytes_Code_s.OEq",
"data_elim_Vale.X64.Bytes_Code_s.OGe",
"data_elim_Vale.X64.Bytes_Code_s.OGt",
"data_elim_Vale.X64.Bytes_Code_s.OLe",
"data_elim_Vale.X64.Bytes_Code_s.OLt",
"data_elim_Vale.X64.Bytes_Code_s.ONe",
"data_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.X64.Machine_s.Reg@tok",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OStack",
"disc_equation_Vale.X64.Machine_s.Public",
"disc_equation_Vale.X64.Machine_s.Secret",
"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.feq",
"equation_FStar.FunctionalExtensionality.is_restricted",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.snd", "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.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.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.taint",
"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",
"int_inversion", "int_typing",
"interpretation_Tm_abs_2c843006472a19cdcec8325c8a6a91a4",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"kinding_Vale.X64.Machine_s.taint@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_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_hd",
"projection_inverse_Prims.Cons_tl",
"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_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.Block_block",
"projection_inverse_Vale.X64.Machine_s.Block_t_ins",
"projection_inverse_Vale.X64.Machine_s.Block_t_ocmp",
"projection_inverse_Vale.X64.Machine_s.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_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_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_FStar.Pervasives.Native.uu___is_Some",
"typing_Tm_abs_2c843006472a19cdcec8325c8a6a91a4",
"typing_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"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_Prims.LexTop@tok",
"typing_tok_Vale.X64.Machine_s.Public@tok", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"3b1aac10831f16b9308c2d84b5303535"
],
[
"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",
"constructor_distinct_FStar.Pervasives.Native.None",
"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_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.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_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_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Vale.X64.Leakage.check_if_block_consumes_fixed_time",
"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,
"677930cbf33b457cb9e0b9edcd3b9a7a"
],
[
"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_e4836109f73687024ac3edd113084865",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Lib.MapTree_interpretation_Tm_arrow_6c9cf9481699be8541b47b0f2a7e6435",
"Vale.X64.Bytes_Code_s_pretyping_8d8114524e962c921a106571a277b146",
"Vale.X64.Leakage_Helpers_pretyping_27cbc7f3c05302ce277bcd7aa3471f2f",
"Vale.X64.Leakage_s_pretyping_4717468dbe91703716dc7cf6a63e88f2",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"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",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_8afd38cc1321157644dafce503e55d5a_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.X64.Machine_s.Public",
"constructor_distinct_Vale.X64.Machine_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.X64.Machine_s.Reg@tok",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"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.Secret",
"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.feq",
"equation_FStar.FunctionalExtensionality.is_restricted",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.Pervasives.Native.snd", "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.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.code",
"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.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.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.reg",
"fuel_guarded_inversion_Vale.X64.Machine_s.taint",
"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",
"int_inversion", "int_typing",
"interpretation_Tm_abs_4185c7ad5dc50a20deee59c126b9b37b",
"interpretation_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"kinding_Vale.X64.Machine_s.reg@tok",
"kinding_Vale.X64.Machine_s.taint@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_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_Semantics_s.Mkmachine_state_ms_flags",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_heap",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_memTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"proj_equation_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_lts",
"projection_inverse_Vale.X64.Leakage_Helpers.AnalysisTaints_rts",
"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_memTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_ok",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_regs",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stack",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_stackTaint",
"projection_inverse_Vale.X64.Machine_Semantics_s.Mkmachine_state_ms_trace",
"projection_inverse_Vale.X64.Machine_s.While_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_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_f0ac051651fa0e095f1b2c1241fd6a3f",
"token_correspondence_Vale.Lib.MapTree.sel",
"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",
"token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
"typing_FStar.FunctionalExtensionality.on_domain",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Tm_abs_a356ee6fc4458d630d8101a85a9a6019",
"typing_Vale.Lib.MapTree.sel",
"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__cfFlagsTaint",
"typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__ofFlagsTaint",
"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_Prims.LexTop@tok",
"typing_tok_Vale.X64.Machine_s.Public@tok", "unit_inversion",
"unit_typing", "well-founded-ordering-on-nat"
],
0,
"a09c68366a8e871032b37be7eb1a31b6"
],
[
"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,
"9f038df3a58f425882bbcfc547fe0641"
],
[
"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,
"ec878c5d5903004067bab84c47f4e9e0"
],
[
"Vale.X64.Leakage.check_if_code_is_leakage_free",
1,
1,
2,
[ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ],
0,
"2c458d537e2c4e5f67296fd9f93d3878"
],
[
"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,
"e79aa41ddce6551a2dea7f40cb78ae2a"
]
]
]
Computing file changes ...
