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