[
  "��4�\nh��N�\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,
      "058e35f4eba349984d8a9cbfa43b9940"
    ],
    [
      "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,
      "62225cdfd040d6a56e96c47340045858"
    ],
    [
      "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,
      "205fecb3bed2572ba597a26d377d404c"
    ],
    [
      "Vale.X64.Leakage.lemma_eq_regs_file",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_05a30d0ade8c6c0091e9413c657014a5"
      ],
      0,
      "123b882616bbe8d4d8868a9e2a9a857a"
    ],
    [
      "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,
      "8ea6917644f49749fcd9d9e27c647b8b"
    ],
    [
      "Vale.X64.Leakage.lemma_eq_regs",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_41417e2bce755e946fbf0de9fb4be971"
      ],
      0,
      "2ca8e20c87abc28fd30d519cb809449f"
    ],
    [
      "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,
      "04c3565a20e1e3aeadfd53ef0e0abf5d"
    ],
    [
      "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,
      "df2efac1f8f3f83320277be726b1e3ca"
    ],
    [
      "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,
      "4d3d4b88b6c89805ee068a1622a8e628"
    ],
    [
      "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,
      "03d31beacc8080ad7706f2c3fd6f07a4"
    ],
    [
      "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,
      "e6729ce8c3650659b86a3c4eb93a246a"
    ],
    [
      "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,
      "15f67ae62549d99e13860b44bf427efd"
    ],
    [
      "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,
      "0347ac2e0611a4a8fe53ab025e947fd5"
    ],
    [
      "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,
      "3305abaedd37380f53628bfb48bf42d4"
    ],
    [
      "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,
      "588ebb71eb2dfb84ed8e4054f29b5b35"
    ],
    [
      "Vale.X64.Leakage.lemma_count_public_registers_file",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_988d466cfe4591206c49030513719ab1"
      ],
      0,
      "dccc3845cf2612f91305679d6c4d256c"
    ],
    [
      "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", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Vale.Arch.HeapTypes_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.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_260756dd6a32464ce58c705280416287",
        "refinement_interpretation_Tm_refine_46e1d323f68f206e5b156d1cf36df4aa",
        "refinement_interpretation_Tm_refine_4cd2cd249de1c01a346e065af2ec7c1e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7e4a6c5999db731b5d17d0418dfeea3e",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.X64.Leakage.count_public_registers_file",
        "well-founded-ordering-on-nat"
      ],
      0,
      "0050dda1d6b8b7cef2f0d92d8a6ae310"
    ],
    [
      "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,
      "1fc17a44d90b42d56c785d3e2c3d4808"
    ],
    [
      "Vale.X64.Leakage.lemma_count_public_registers",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e3fda938b58705113b395f978ffaea7d"
    ],
    [
      "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,
      "0423eeb5fec068ae77a6460089daf36a"
    ],
    [
      "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,
      "85fdbcb136b893461a7e68f5549d0882"
    ],
    [
      "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,
      "f06e96992c98e5517b8e219d8d04f15a"
    ],
    [
      "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,
      "1c5625c519dae18f5babe5bd01423900"
    ],
    [
      "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,
      "f89c4c132b887c55fb838b50b115cab7"
    ],
    [
      "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,
      "ac79f7d5e40fd03b209e56ca54a84c09"
    ],
    [
      "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_e4836109f73687024ac3edd113084865",
        "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_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",
        "equality_tok_Prims.LexTop@tok",
        "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",
        "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_ins_def",
        "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
        "typing_Vale.X64.Machine_Semantics_s.machine_eval_code",
        "typing_tok_Prims.LexTop@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "b93500e47b69ad1a0451356a3b86700e"
    ],
    [
      "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,
      "1262a885a3b136740ab1ee2389b1f0dd"
    ],
    [
      "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,
      "fc422a90fd50698234bb57adf1d13374"
    ],
    [
      "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,
      "20dad6833d262729166b035a29b17685"
    ],
    [
      "Vale.X64.Leakage.lemma_loop_taintstate_monotone",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "e1108c63478ccd5839855cd5f8996a17"
    ],
    [
      "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,
      "c1847683f0868e6c4a70ac782b5bad41"
    ],
    [
      "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",
        "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",
        "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.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_Prims.LexTop@tok",
        "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_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_307d576cc835c0420dfededd9ce6b286",
        "interpretation_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b",
        "interpretation_Tm_abs_d0af518286461c15a8fc086575bc787d",
        "interpretation_Tm_abs_ff856a54708216dbc469f39ac4b5748e",
        "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_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_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_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",
        "token_correspondence_Vale.X64.Machine_Semantics_s.eval_ocmp",
        "token_correspondence_Vale.X64.Machine_Semantics_s.valid_ocmp",
        "typing_FStar.FunctionalExtensionality.on_domain",
        "typing_Tm_abs_307d576cc835c0420dfededd9ce6b286",
        "typing_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b",
        "typing_Vale.Arch.HeapTypes_s.uu___is_Public",
        "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__ofFlagsTaint",
        "typing_Vale.X64.Leakage_s.__proj__LeakageTaints__item__regTaint",
        "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.Arch.HeapTypes_s.Public@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "c5fc61b31c6592743ef630c846d43b7e"
    ],
    [
      "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,
      "2675f6f1f4fad51be0c60038ca9bb894"
    ],
    [
      "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",
        "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_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_Prims.LexTop@tok",
        "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_307d576cc835c0420dfededd9ce6b286",
        "interpretation_Tm_abs_602c7daad96f0f1f2edbcf613fcc444b",
        "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_4d5241eb6fe198666a8101195bbd4a2a",
        "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.eval_ocmp",
        "token_correspondence_Vale.X64.Machine_Semantics_s.flags_none",
        "token_correspondence_Vale.X64.Machine_Semantics_s.machine_eval_code.fuel_instrumented",
        "token_correspondence_Vale.X64.Machine_Semantics_s.valid_ocmp",
        "typing_FStar.FunctionalExtensionality.on_domain",
        "typing_FStar.Pervasives.Native.__proj__Some__item__v",
        "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_Prims.LexTop@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.Public@tok", "unit_inversion",
        "unit_typing", "well-founded-ordering-on-nat"
      ],
      0,
      "8bdca36c6d13e5996ca283753cf64dce"
    ],
    [
      "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,
      "8f8c11937302b6f0feb58f8fc7a17102"
    ],
    [
      "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,
      "02a20437e02cec703371995eac8f11a2"
    ],
    [
      "Vale.X64.Leakage.check_if_code_is_leakage_free",
      1,
      1,
      2,
      [ "@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq" ],
      0,
      "862213c86836806f1d50c9b452be5a89"
    ],
    [
      "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,
      "318c0b68696062be8ac4251ff5335000"
    ]
  ]
]