[
  "/\u0003´VÀS\u0016xòð|Î~Ò#ó",
  [
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fast_mul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eq2", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "function_token_typing_Prims.__cache_version_number__",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "true_interp"
      ],
      0,
      "310489decdc5aaacb8bb7c8cfcd2669c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fast_mul1",
      2,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "d3faa1dec5cc1371ed1e96ad48220b04"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fast_mul1",
      3,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "e248d2049db3b7a71f798becf434eb52"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_mul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "true_interp",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.Curve25519.Fast_defs.pow2_three",
        "typing_Vale.Def.Types_s.add_wrap",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.updated_cf",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "unit_inversion", "unit_typing"
      ],
      0,
      "e374a5c41ed1a607053afe6e651b0c08"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_mul1",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.map2", "equation_Vale.Lib.Map16.map4",
        "equation_Vale.Lib.Map16.map8", "equation_Vale.Lib.Map16.upd8",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a608a89bbc0a207d5920d37d906f7f40",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "7f5edf5a987572baadf159b514032608"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_mul1",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "6209a73ce8eda8371722c6e9852fe81f"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fast_mul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fast_mul1",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "429974329cf4895e73f29257cf325d75"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fast_mul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "1affdd720d6fbdf4ae27aae1a05f062f"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_add_after_mul1_regs",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_06f471b640e66fa9f9320f2424ae861f",
        "interpretation_Tm_abs_207f8356df8fbf9b97e4afb9bc968f31",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_1d611ab70e7b74556741b4d59722e097",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Types_s.add_wrap",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.overflow", "typing_Vale.X64.Decls.updated_of",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "unit_typing"
      ],
      0,
      "152aa33a28de2c9b9bd9c19e8a6ec119"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fast_add_after_mul1_regs",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fast_add_after_mul1_regs",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "b0c8950387006eb41c779f1db0a783db"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fast_add_after_mul1_regs",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "3288d1d9829253fcfaa7147ecdd373a2"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fast_mul1_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.add_carry",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing", "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
      ],
      0,
      "68604e3aeb297c91f498bd63525c3858"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_mul1_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.Decls_interpretation_Tm_ghost_arrow_30853e489012f08e714eeb8d6ec738ed",
        "Vale.X64.Decls_interpretation_Tm_ghost_arrow_f5ddc73608a3b8e7289a113e43b8c18b",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_Vale.X64.Machine_s.OReg@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.add_carry",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Decls.valid_buf_maddr64",
        "equation_Vale.X64.Decls.valid_mem_operand64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.state_eta",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_06f471b640e66fa9f9320f2424ae861f",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_207f8356df8fbf9b97e4afb9bc968f31",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.Lib.Map16.lemma_eta",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_r",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_1d611ab70e7b74556741b4d59722e097",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_449c6217aeda38f4b46138844d86130d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_91b21bda257faf7d7870e0299e500a49",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_c365eb902b454950de62fba701d9049d",
        "string_typing", "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.Def.Types_s.add_wrap", "typing_Vale.Lib.Map16.sel",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.cf", "typing_Vale.X64.Decls.maintained_cf",
        "typing_Vale.X64.Decls.maintained_of",
        "typing_Vale.X64.Decls.overflow", "typing_Vale.X64.Decls.updated_cf",
        "typing_Vale.X64.Decls.updated_of", "typing_Vale.X64.Decls.va_if",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "typing_Vale.X64.Decls.valid_cf", "typing_Vale.X64.Decls.valid_of",
        "typing_Vale.X64.Memory.base_typ_as_vale_type",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.load_mem64",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.state_eta",
        "typing_Vale.X64.State.update_reg",
        "typing_Vale.X64.State.update_reg_64",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "5d7a5e2e5aba08f272007bed7e09b93d"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fast_mul1_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fast_mul1_add",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "6b1fae5fb73edd1e20a451d9ed2b3e5c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fast_mul1_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "c69878ae5f217c6fdc06a1291fec58cd"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Store4",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.InsMem.buffer64_write",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_buffer_write",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_typing",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_valid_taint",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Decls.validSrcAddrs64",
        "typing_Vale.X64.Memory.buffer_addr",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing"
      ],
      0,
      "6c7af20f9f362241168c41c6bb9fe79f"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Store4",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Store4",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing"
      ],
      0,
      "b069752d9edb8e89aaedeb1cbb894101"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Store4",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "151c2000c3c76e0ac65696796cd49509"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_times_38",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "69c7e381dda1f6e2b1269006fe19040e"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_times_38",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.X64.Machine_s_pretyping_518a4fb262eb27362824d01da01681c3",
        "bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons",
        "constructor_distinct_Vale.X64.Machine_s.Block",
        "constructor_distinct_Vale.X64.Machine_s.OConst",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_elim_Vale.X64.Machine_s.OReg",
        "data_elim_Vale.X64.State.Mkvale_state",
        "data_typing_intro_Vale.X64.Machine_s.OReg@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "disc_equation_Prims.Cons", "disc_equation_Vale.X64.Machine_s.Block",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.state_inv",
        "equation_Vale.X64.Decls.update_operand",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.valid_operand",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_Vale.X64.State.valid_src_operand",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.Machine_s.operand",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_upd_ne", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Negation", "proj_equation_Prims.Cons_hd",
        "proj_equation_Prims.Cons_tl",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Block_block",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Vale.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.OConst_n",
        "projection_inverse_Vale.X64.Machine_s.OConst_tc",
        "projection_inverse_Vale.X64.Machine_s.OConst_tr",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_r",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "true_interp",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.update_operand",
        "typing_Vale.X64.Decls.va_is_dst_opr64",
        "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Decls.valid_cf",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.eval_operand"
      ],
      0,
      "5cb66b06317ba7f32a1016c116f50f61"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wp_Carry_times_38",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.reg_64",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "228c191163cf606a2d7008e3dc8bfe8d"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Carry_times_38",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.X64.QuickCode_pretyping_7a2122c20d44fc80e093f4f4614be2e2",
        "bool_inversion", "constructor_distinct_Prims.Nil",
        "constructor_distinct_Vale.X64.QuickCode.Mod_reg",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.X64.QuickCode.Mod_None@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Carry_times_38",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.update_operand",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_is_dst_opr64",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.eval_operand",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_with_fuel_Vale.X64.QuickCode.update_state_mods.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "kinding_Vale.X64.QuickCode.mod_t@tok",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Flags.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Prims.Nil_a",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.QuickCode.Mod_reg__0",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.update_operand",
        "typing_Vale.X64.Decls.va_is_dst_opr64",
        "typing_Vale.X64.Decls.va_upd_ok", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.eval_operand",
        "typing_tok_Vale.X64.QuickCode.Mod_None@tok", "unit_typing"
      ],
      0,
      "4734202efaa747b39b63f7b8348840f7"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Carry_times_38",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "25309580bf09277c35bc4036d8e6c2c3"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Carry_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_if",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "interpretation_Tm_abs_1125c467b0c0b7360cf160a90f8a1b38",
        "interpretation_Tm_abs_478b1d23d550a134e4d1a598053d9a60",
        "interpretation_Tm_abs_48425db314e91376b77df96308926367",
        "interpretation_Tm_abs_f4e3633694d58f72d8b4f09c2d0c9bce",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.X64.Decls.cf", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
      ],
      0,
      "cdd2e5e8c68f565704efd38d62ccb405"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "1c453a2664550aa93c834a1b488f5a6b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_pass",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Prop_s.prop0",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.modifies_buffer_specific",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.InsMem.buffer64_write",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_buffer_write",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_1125c467b0c0b7360cf160a90f8a1b38",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_478b1d23d550a134e4d1a598053d9a60",
        "interpretation_Tm_abs_48425db314e91376b77df96308926367",
        "interpretation_Tm_abs_4ceabf569fd259b9447b243205fceb17",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "interpretation_Tm_abs_8a46e2d6a879c4179d4760d40c5949b3",
        "interpretation_Tm_abs_b78e0d5a9e9331eba0d219af16de1103",
        "interpretation_Tm_abs_dee29111c549430168450de1701b4d46",
        "interpretation_Tm_abs_edc864a3bc5a329067bd4c97f1a0c76f",
        "interpretation_Tm_abs_f4e3633694d58f72d8b4f09c2d0c9bce",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "lemma_Vale.X64.Memory.loc_includes_refl",
        "lemma_Vale.X64.Memory.modifies_buffer_addr",
        "lemma_Vale.X64.Memory.modifies_goal_directed_refl",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans",
        "lemma_Vale.X64.Memory.modifies_goal_directed_trans2",
        "lemma_Vale.X64.Memory.modifies_valid_taint",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_211facd8812fd94e95b65d3b8891b14a",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_41db9fdf9444e7dc3929e8f963c015c7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
        "refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing", "typing_FStar.Seq.Base.upd", "typing_Prims.eq2",
        "typing_Prims.l_and",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.Def.Types_s.add_wrap", "typing_Vale.Lib.Map16.sel",
        "typing_Vale.X64.Decls.cf",
        "typing_Vale.X64.Decls.modifies_buffer_specific",
        "typing_Vale.X64.Decls.updated_cf",
        "typing_Vale.X64.Decls.validSrcAddrs64",
        "typing_Vale.X64.Decls.valid_cf",
        "typing_Vale.X64.Memory.buffer_as_seq",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.buffer_write",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "83565061b28e2c524123fbc15b65c9f8"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wp_Carry_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "interpretation_Tm_abs_1125c467b0c0b7360cf160a90f8a1b38",
        "interpretation_Tm_abs_478b1d23d550a134e4d1a598053d9a60",
        "interpretation_Tm_abs_48425db314e91376b77df96308926367",
        "interpretation_Tm_abs_f4e3633694d58f72d8b4f09c2d0c9bce",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs"
      ],
      0,
      "b05de306259af457b74b6d8a4adcd99d"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Carry_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Carry_pass",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "interpretation_Tm_abs_1125c467b0c0b7360cf160a90f8a1b38",
        "interpretation_Tm_abs_478b1d23d550a134e4d1a598053d9a60",
        "interpretation_Tm_abs_48425db314e91376b77df96308926367",
        "interpretation_Tm_abs_f4e3633694d58f72d8b4f09c2d0c9bce",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "5e93b3de193ab83e7537c9f0ff63e503"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Carry_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "128083733d165619ed57e72d2ec42079"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_code_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "e20605f3c185a79fb2017e92cb313ff3"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_codegen_success_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "238bbc6d1b6157d5df590da4c23b52e4"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "80696892bbd73fb17b965b2c3c59bfc0"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "fb06342788f388137a50c00b26a53e90"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_wide",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_83918874eb4bcd3da17bdcc6b11a9c15",
        "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Curve25519.Fast_defs.pow2_four",
        "typing_Vale.Lib.Map16.sel",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.modifies_buffer_specific",
        "typing_Vale.X64.Decls.validSrcAddrs64",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "d9b3cf693adb8a33b1925588889cafc1"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wp_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "4474ebb4cd68a0178c9d253050fb87da"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Carry_wide",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "bd496809f001a41fb0472564090a8b56"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Carry_wide",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "c9b32bb86466bbf3486b89a7389e2ca3"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Carry_sub_pass",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "a50ac06bd7e3840332f78a89790e193b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Carry_sub_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Types_s.sub_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "interpretation_Tm_abs_8a46e2d6a879c4179d4760d40c5949b3",
        "interpretation_Tm_abs_b78e0d5a9e9331eba0d219af16de1103",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.cf", "typing_Vale.X64.Decls.updated_cf",
        "typing_Vale.X64.Decls.valid_cf", "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "unit_inversion", "unit_typing"
      ],
      0,
      "0ae4e3ae76a46773566ab6f62094b81c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Carry_sub_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Carry_sub_pass",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_ok",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "fcb8f6d19005da0a7bbea38ef8fe1d2c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Carry_sub_pass",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "33aeaf932aed1a3f8a2cae2df89e00dd"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fast_add",
      1,
      1,
      0,
      [ "@MaxIFuel_assumption", "@query", "unit_inversion", "unit_typing" ],
      0,
      "86a2aef5c79ba9dbd743e141fee10007"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.Def.Types_s.add_wrap",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.updated_cf", "typing_Vale.X64.Decls.valid_cf",
        "typing_Vale.X64.Memory.load_mem64",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "unit_inversion", "unit_typing"
      ],
      0,
      "21c1f154f2a9d83a72c6050634583655"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fast_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fast_add",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_reg64",
        "typing_Vale.X64.Decls.valid_cf", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "1878df8ad4136f79c65ce8fc25c68ebd"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fast_add",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "faf88234558732d6de121fda71b884e5"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fast_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "haseqTm_refine_c365eb902b454950de62fba701d9049d",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "6b8f1eca1dbf466ac8aa2e0a189f691b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fast_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "bool_typing", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
        "constructor_distinct_Vale.X64.Machine_s.OReg",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.FastUtil_helpers.sub_carry",
        "equation_Vale.Curve25519.Fast_defs.bit",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Curve25519.Fast_defs.pow2_four",
        "equation_Vale.Curve25519.Fast_defs.pow2_three",
        "equation_Vale.Curve25519.Fast_defs.pow2_two",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Types_s.sub_wrap",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.get",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Machine_s.t_reg_to_int",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_buffer_read",
        "equation_Vale.X64.Memory.valid_layout_buffer",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.state_eta",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "l_and-interp", "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.Lib.Map16.lemma_eta",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Regs.lemma_eta", "lemma_Vale.X64.Regs.lemma_upd_eq",
        "lemma_Vale.X64.Regs.lemma_upd_ne",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.OReg_r",
        "projection_inverse_Vale.X64.Machine_s.OReg_tc",
        "projection_inverse_Vale.X64.Machine_s.OReg_tr",
        "projection_inverse_Vale.X64.Machine_s.Reg_r",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_b51b45ce195a33a465eab411d92fdae9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f5b7985bc3c2bc5a5dee962352a41f5d",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Curve25519.Fast_defs.bool_bit",
        "typing_Vale.Def.Types_s.add_wrap", "typing_Vale.Lib.Map16.get",
        "typing_Vale.X64.Decls.updated_cf",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.valid_cf",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.load_mem64",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.upd",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.state_eta",
        "typing_Vale.X64.State.update_reg_64",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "da0ea7c84c2e6195164055f51c546f3c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fast_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fast_sub",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_reg64",
        "typing_Vale.X64.Decls.valid_cf", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "3c1bdc6edd56c8f39c5b4f1bdbba1e42"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fast_sub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "bd4154c6b79b24f50e030d19e5a9d904"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_req_Fadd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "fe7a4ac6859ef7404bc6d8b74be8260d"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_ens_Fadd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Vale.X64.Decls.va_state_eq",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "f307388b36a0fa7e161be3c501b4321f"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eq2", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "function_token_typing_Prims.__cache_version_number__",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "true_interp"
      ],
      0,
      "ec6402c56081ff5f0bb2c2d389fed9a2"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd",
      2,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "a7adce56237bc4bee58f7fb5e40031ad"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd",
      3,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "4e8c5d8939746077397de4430314a68b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd",
      4,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "1c80d3e2d81d0d5df74ed3945d5bfa55"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd",
      5,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "ee551c44695427c643f146462d5ed435"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd",
      6,
      1,
      0,
      [
        "@query", "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "0e58889b2fce3866db61e16e88ae3e06"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42",
        "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2",
        "Vale.Curve25519.X64.FastHybrid_interpretation_Tm_ghost_arrow_0683e41e0b27393fa354e5df20561443",
        "bool_inversion", "constructor_distinct_Prims.Cons",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapImpl.Immutable@tok",
        "equality_tok_Vale.Arch.HeapImpl.Mutable@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.bool_bit",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2",
        "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.InsMem.create_post",
        "equation_Vale.X64.InsMem.heaplet_id_is_some",
        "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_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.buffer_info_disjoint",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.init_heaplets_req",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_122888157b956147e034801c5272e7bf",
        "interpretation_Tm_abs_5163d80e40f141069b7bb90539a021e8",
        "interpretation_Tm_abs_c88955b7b005fff8d8ceb683c3fd9d59",
        "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.lemma_heaps_match",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "true_interp", "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_Prims.l_and",
        "typing_Tm_abs_c88955b7b005fff8d8ceb683c3fd9d59",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
        "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2",
        "typing_Vale.Lib.Seqs.list_to_seq",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Decls.cf", "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.layout_buffers",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapImpl.Immutable@tok",
        "typing_tok_Vale.Arch.HeapImpl.Mutable@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "0facb90b0fa2e8240af425d17f4e255f"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.map16", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.map8",
        "equation_Vale.Lib.Map16.upd8",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a608a89bbc0a207d5920d37d906f7f40",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "79b0f63b81607f012ca67cc82b510afa"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd",
      3,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "5cc2c5946284bf23c574576ad27799b5"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd",
      4,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "3781242d694c8b581f7273bf8e72fe3b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd",
      5,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "8193a20e586f262bd10032037d5350f1"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd",
      6,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Map16.map16", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.map8",
        "equation_Vale.Lib.Map16.sel16", "equation_Vale.Lib.Map16.upd8",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__b",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a608a89bbc0a207d5920d37d906f7f40",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "2530adf575d66fa0732fd47aa3e8af22"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fadd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fadd",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_mem_layout",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "3cb71d55ebc988265a9f7977a30492e5"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fadd",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "25df5674d744ec2c901fa47f1577fd9b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_req_Fadd_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "aac1c369418ad0e9807f2e9ad4e4f539"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_ens_Fadd_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "4a6360f348c781ff0a01d579d4160fd8"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fadd_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "7e312d020e05937d7179b76dd6a6405c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "refinement_interpretation_Tm_refine_fb65271e56146759a2680db7a287897b"
      ],
      0,
      "4ae96d934be9904e039a07685edcfc4b"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fadd_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
        "int_typing", "l_and-interp", "l_imp-interp", "l_not-interp",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
        "lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
        "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing"
      ],
      0,
      "f85fd72211843432b9c1d05ccb6824ae"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wp_Fadd_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8141158eff370183f097d08df394249c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fadd_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fadd_stdcall",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8",
        "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
        "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62",
        "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
        "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe",
        "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_mem_layout",
        "typing_Vale.X64.Decls.va_upd_reg64",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "748b40780498ea34648aeedd359646c3"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fadd_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "759b2f281784e8efb1e3a6d27914b301"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_req_Fsub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "bee02502ddc791529e6e7cf44ddf75fc"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_ens_Fsub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Vale.X64.Decls.va_state_eq",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "48a792be8bf37432441b114e67098df2"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fsub",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42",
        "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2",
        "bool_inversion", "constructor_distinct_Prims.Cons",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapImpl.Immutable@tok",
        "equality_tok_Vale.Arch.HeapImpl.Mutable@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2",
        "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.InsMem.create_post",
        "equation_Vale.X64.InsMem.heaplet_id_is_some",
        "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_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.buffer_info_disjoint",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.init_heaplets_req",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.lemma_heaps_match",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_Prims.l_and",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
        "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2",
        "typing_Vale.Lib.Seqs.list_to_seq",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.layout_buffers",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapImpl.Immutable@tok",
        "typing_tok_Vale.Arch.HeapImpl.Mutable@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing"
      ],
      0,
      "41f9e5fc25602aab963f4744e97a3b3d"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fsub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fsub",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_mem_layout",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "cf7766f3f271f5972b7ad0f04a077cfe"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fsub",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "19e52eae6b9dff52152c5d4b5eed4933"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_req_Fsub_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "7d16633ec9e01fb3cd4997749bb6d225"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_ens_Fsub_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "4fbdf761eb1a6dd66ef9085fce0650c0"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fsub_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d2cce9f473969a32905c0403b845d25a"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fsub_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "refinement_interpretation_Tm_refine_055ce2a08dafba0f815c9fa2b1a08218"
      ],
      0,
      "67a1fb7cb1716912ad5e33c4949dead6"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fsub_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
        "int_typing", "l_and-interp", "l_imp-interp", "l_not-interp",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
        "lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
        "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing"
      ],
      0,
      "da4cd96bb7369963b207ba3e4114abb9"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wp_Fsub_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "19c29de6bebd387679c5017455d1bdd4"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fsub_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fsub_stdcall",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8",
        "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
        "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62",
        "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
        "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe",
        "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_mem_layout",
        "typing_Vale.X64.Decls.va_upd_reg64",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "aab3067ac2644ec7006764c4793aa7cf"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fsub_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "0d722a4b93cf8a1e994e233ef1a18fce"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_req_Fmul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "bad54b1c2cae6f3403cbe93f411c6041"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_ens_Fmul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Vale.X64.Decls.va_state_eq",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "12bd8758a9fe11744d008c5642144643"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fmul1",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "cdce583f35a09fcd57d8aa8e21c745ae"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fmul1",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Vale.Arch.HeapImpl_pretyping_4aa61432b04e23a2d66ceb8d22171f42",
        "Vale.Arch.HeapImpl_pretyping_6646ba4902a38c8f85d79301e07488b2",
        "bool_inversion", "constructor_distinct_Prims.Cons",
        "constructor_distinct_Vale.Arch.HeapImpl.Immutable",
        "constructor_distinct_Vale.Arch.HeapImpl.Mutable",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "data_typing_intro_Vale.Arch.HeapImpl.Mkbuffer_info@tok",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "eq2-interp",
        "equality_tok_Vale.Arch.HeapImpl.Immutable@tok",
        "equality_tok_Vale.Arch.HeapImpl.Mutable@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.Fast_defs.pow2_five",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Map16.map2",
        "equation_Vale.Lib.Map16.map4", "equation_Vale.Lib.Map16.sel2",
        "equation_Vale.Lib.Map16.sel4", "equation_Vale.Lib.Map16.sel8",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.InsMem.create_post",
        "equation_Vale.X64.InsMem.heaplet_id_is_some",
        "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_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.buffer_info_disjoint",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.init_heaplets_req",
        "equation_Vale.X64.Memory.memtaint",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.Memory.valid_taint_buf64",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_heap_layout",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_83918874eb4bcd3da17bdcc6b11a9c15",
        "kinding_Vale.Arch.HeapImpl.buffer_info@tok", "l_and-interp",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.Memory.lemma_heaps_match",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
        "proj_equation_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_heap_layout_vl_taint",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_buffer",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_heaplet",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_mutable",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_taint",
        "projection_inverse_Vale.Arch.HeapImpl.Mkbuffer_info_bi_typ",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_8de17eec3c1f64d75609148b2dff3180",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "string_typing",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_inner",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_heap_layout__item__vl_taint",
        "typing_Vale.Lib.Map16.get", "typing_Vale.Lib.Map16.sel2",
        "typing_Vale.Lib.Seqs.list_to_seq",
        "typing_Vale.X64.CPU_Features_s.bmi2_enabled",
        "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.layout_buffers",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_tok_Vale.Arch.HeapImpl.Immutable@tok",
        "typing_tok_Vale.Arch.HeapImpl.Mutable@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "a8d0075ac4f74dc11e5aeb7b89070b86"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fmul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok", "equation_Prims.nat",
        "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fmul1",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_mem_layout",
        "typing_Vale.X64.Decls.va_upd_reg64", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "8c24f8e389c5fe827ef7c8aa375870ba"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fmul1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "d634b2928d189d802f34fc96958e31eb"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_req_Fmul1_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "unit_typing"
      ],
      0,
      "6642cdf52f936b50e0480b9f3edb61e1"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_ens_Fmul1_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_Vale.X64.Decls.va_state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "fce6dc470a94fa06b1fd990ce163468a"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_qcode_Fmul1_stdcall",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "51a6f32722217cae4af93f5054c8594c"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fmul1_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d37bbc3649ad9fab6bd8e2b4be084013"
      ],
      0,
      "013d55d69150b79079c2eba8e05acf72"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_lemma_Fmul1_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.l_and", "equation_Prims.l_imp",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Prop_s.prop0", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "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_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.buffer64",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat64", "int_inversion",
        "int_typing", "l_and-interp", "l_imp-interp", "l_not-interp",
        "lemma_Vale.Lib.Map16.lemma_equal_intro",
        "lemma_Vale.X64.Flags.lemma_equal_intro",
        "lemma_Vale.X64.QuickCodes.lemma_label_bool",
        "lemma_Vale.X64.Regs.lemma_equal_intro",
        "lemma_Vale.X64.Stack_i.lemma_compose_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_correct_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_stack64",
        "lemma_Vale.X64.Stack_i.lemma_frame_store_load_taint_stack64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_load64",
        "lemma_Vale.X64.Stack_i.lemma_free_stack_same_valid64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_free_stack64",
        "lemma_Vale.X64.Stack_i.lemma_same_init_rsp_store_stack64",
        "lemma_Vale.X64.Stack_i.lemma_store_new_valid64",
        "lemma_Vale.X64.Stack_i.lemma_store_stack_same_valid64",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "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.Mktuple3__1",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "refinement_interpretation_Tm_refine_f9ad94596474231e26a90e389b8461f6",
        "refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "string_typing", "typing_Prims.eq2",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.Memory.get_vale_heap",
        "typing_Vale.X64.Memory.loc_buffer",
        "typing_Vale.X64.Memory.modifies",
        "typing_Vale.X64.QuickCodes.label",
        "typing_Vale.X64.QuickCodes.va_range1",
        "typing_Vale.X64.Regs.eta_sel", "typing_Vale.X64.Regs.sel",
        "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.Stack_i.valid_src_stack64",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok", "unit_typing"
      ],
      0,
      "6e4c2c47e514d5d04a04460901462a5d"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wp_Fmul1_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c400277626146bf53d0257ea6e6b83f0"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_wpProof_Fmul1_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "data_typing_intro_Vale.X64.Machine_s.Reg@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
        "equation_Prims.nat", "equation_Vale.Arch.HeapImpl.heaplet_id",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Curve25519.X64.FastHybrid.va_wp_Fmul1_stdcall",
        "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.X64.Decls.upd_register",
        "equation_Vale.X64.Decls.va_ensure_total",
        "equation_Vale.X64.Decls.va_if",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.va_state_eq",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_mem_layout",
        "equation_Vale.X64.Decls.va_upd_ok",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_stack",
        "equation_Vale.X64.Decls.va_upd_stackTaint",
        "equation_Vale.X64.Decls.validDstAddrs",
        "equation_Vale.X64.Decls.validDstAddrs64",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs64",
        "equation_Vale.X64.Machine_s.n_reg_files",
        "equation_Vale.X64.Machine_s.n_regs",
        "equation_Vale.X64.Machine_s.reg_64",
        "equation_Vale.X64.Machine_s.reg_file_id",
        "equation_Vale.X64.Machine_s.reg_id",
        "equation_Vale.X64.Machine_s.t_reg",
        "equation_Vale.X64.Machine_s.t_reg_file",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.Memory.vale_full_heap_equal",
        "equation_Vale.X64.QuickCode.t_require",
        "equation_Vale.X64.QuickCode.va_t_ensure",
        "equation_Vale.X64.State.state_eq",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "fuel_guarded_inversion_Vale.Arch.HeapImpl.vale_full_heap",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "interpretation_Tm_abs_7112983baaa4c9ef04184f03828d86e8",
        "interpretation_Tm_abs_7ea5bd633d40850615341220b89135e8",
        "interpretation_Tm_abs_8eaffd6bd22e15c2d46f8e73ccf4da62",
        "interpretation_Tm_abs_ce1a0300ac998db3015a4397c104a2fd",
        "interpretation_Tm_abs_dc5afce1f3a4c6ae9eb55e201e289cbe",
        "interpretation_Tm_abs_e51c7d7b4f244bf176c4178b097c4b0e",
        "lemma_Vale.Lib.Map16.lemma_equal_elim",
        "lemma_Vale.X64.Regs.lemma_equal_elim",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.Machine_s.Reg_rf",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_flags",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stack",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.Machine_s.Reg_rf",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_flags",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_stackTaint",
        "refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.Lib.Map16.upd",
        "typing_Vale.X64.Decls.va_upd_flags",
        "typing_Vale.X64.Decls.va_upd_mem",
        "typing_Vale.X64.Decls.va_upd_mem_heaplet",
        "typing_Vale.X64.Decls.va_upd_mem_layout",
        "typing_Vale.X64.Decls.va_upd_reg64",
        "typing_Vale.X64.Decls.va_upd_stack",
        "typing_Vale.X64.Decls.va_upd_stackTaint",
        "typing_Vale.X64.Regs.sel", "typing_Vale.X64.Stack_i.init_rsp",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_flags",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_regs",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stack",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_stackTaint",
        "typing_Vale.X64.State.update_reg", "unit_typing"
      ],
      0,
      "b6681fa0eccd4280d9232f7381937d31"
    ],
    [
      "Vale.Curve25519.X64.FastHybrid.va_quick_Fmul1_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "4166262b19f30d26004c639a651bafc4"
    ]
  ]
]