[
  "q��Q��η�\fA\u0013\n���",
  [
    [
      "X64.SHA.va_lemma_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Tm_unit",
        "constructor_distinct_X64.Machine_s.Rax",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.l_and", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_SHA_helpers.hash256", "equation_Types_s.byte_to_twobits",
        "equation_Types_s.quad32", "equation_Types_s.select_word",
        "equation_Words.Four_s.four_select", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_SHA_helpers.word",
        "function_token_typing_Words_s.nat32", "int_inversion",
        "interpretation_Tm_abs_033c986f28fa90d27d2ea96e5cb797c4",
        "interpretation_Tm_abs_26b78bca4f221b4c469edd213f71ebef",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_4309c8fc5805d1cd049b287c438261e3",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_SHA_helpers.make_hash",
        "typing_SHA_helpers.make_ordered_hash",
        "typing_Words_s.__proj__Mkfour__item__hi2",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_tok_X64.Machine_s.Rdi@tok", "unit_typing"
      ],
      0,
      "ccc5aa276c1c9b986f8da3e6c02cd98c"
    ],
    [
      "X64.SHA.va_wpMonotone_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equality_tok_X64.Machine_s.Rax@tok", "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_preamble",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "818a9824aba08c21d94cef0b7c26ab27"
    ],
    [
      "X64.SHA.va_wpCompute_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_preamble",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "3bc1d220fd129e0cadaf0201f1bb3b11"
    ],
    [
      "X64.SHA.va_wpProof_preamble",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "e636ed08214ab3c31a6fb188f90bea36"
    ],
    [
      "X64.SHA.va_wpProof_preamble",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equality_tok_X64.Machine_s.Rax@tok",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_preamble",
        "equation_X64.SHA.va_wp_preamble",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_preamble",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_X64.Machine_s.Rax@tok", "unit_typing"
      ],
      0,
      "9c8748f480c25777146fa77b42b3f30e"
    ],
    [
      "X64.SHA.va_qcode_loop_rounds_0_15",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "44190ac31409e31693c8e04b7773026b"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_0_15",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Loops.repeat_range.fuel_instrumented",
        "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Spec.Loops_interpretation_Tm_arrow_4141e6858c055a47126e62563c8ecb9c",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Tm_unit", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Arch.Types.add_wrap_quad32",
        "equation_Arch.Types.reverse_bytes_quad32_seq",
        "equation_Collections.Seqs_s.compose",
        "equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_SHA_helpers.hash256", "equation_SHA_helpers.k_reqs",
        "equation_SHA_helpers.quads_to_block",
        "equation_SHA_helpers.size_block_w_256",
        "equation_SHA_helpers.ws_quad32",
        "equation_Spec.Hash.Definitions.init_t",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.words_state",
        "equation_Types_s.bits_of_byte", "equation_Types_s.byte_to_twobits",
        "equation_Types_s.quad32", "equation_Types_s.select_word",
        "equation_Types_s.twobits", "equation_Words.Four_s.four_select",
        "equation_Words_s.nat2", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_Words_s.natN", "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.State.state_eq",
        "equation_with_fuel_Spec.Loops.repeat_range.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_SHA_helpers.hash256",
        "function_token_typing_Types_s.reverse_bytes_quad32",
        "function_token_typing_Words_s.nat2", "int_inversion", "int_typing",
        "interpretation_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "l_and-interp", "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_30705d7617ba881840faafa6e12d5005",
        "refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_78ade0fed5734dbdc55c73a07ba22845",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_e8985fc4d83b1f11adbf3a9b5b8bb8f2",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_FStar.Seq.Base.index",
        "typing_Arch.Types.reverse_bytes_quad32_seq",
        "typing_FStar.Seq.Base.length", "typing_SHA_helpers.make_hash",
        "typing_Spec.Hash.Definitions.word", "typing_Spec.MD5.init",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
        "typing_Words_s.__proj__Mkfour__item__lo0",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_Workarounds.index_work_around_quad32",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.base_typ_as_vale_type",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "eddf14efe461e9ca6835fa241d73cca1"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_rounds_0_15",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_loop_rounds_0_15",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "4536631121058007f542c2319dac983a"
    ],
    [
      "X64.SHA.va_wpCompute_loop_rounds_0_15",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_loop_rounds_0_15",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "ff7e50e41a13ffd4c75f18e6dfbf953c"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_0_15",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "222e07f7510bc42165ce88e53231410e"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_0_15",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "SHA_helpers_interpretation_Tm_arrow_af8564461477e639a5a8f6610a3b082e",
        "bool_inversion", "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Arch.Types.reverse_bytes_quad32_seq", "equation_Prims.nat",
        "equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
        "equation_SHA_helpers.k_reqs", "equation_SHA_helpers.quads_to_block",
        "equation_SHA_helpers.size_block_w_256",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_loop_rounds_0_15",
        "equation_X64.SHA.va_wp_loop_rounds_0_15",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_SHA_helpers.word",
        "function_token_typing_SHA_helpers.ws_partial_def", "int_inversion",
        "int_typing", "kinding_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_1101de7a497235789e427aeb0d9938cc",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_Opaque_s.make_opaque",
        "token_correspondence_X64.SHA.va_wpCompute_loop_rounds_0_15",
        "typing_Arch.Types.add_wrap_quad32", "typing_FStar.Seq.Base.init",
        "typing_SHA_helpers.ws_quad32",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_Tm_abs_816ee0e7bd96edebfd201652f1c6c72e",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "cbcd73d614cd0c84e84e778ec49b6aee"
    ],
    [
      "X64.SHA.va_qcode_loop_rounds_16_51_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "a263bd33058bf6daa4f17cf2d6aad4a1"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_16_51_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
        "equation_SHA_helpers.hash256", "equation_Types_s.quad32",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_bb2789de94cd069ecaf5fcc28df052aa"
      ],
      0,
      "8a291e11ded05416796ab494914af18d"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_16_51_body",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Tm_unit", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Arch.Types.add_wrap_quad32", "equation_Prims.eq2",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_SHA_helpers.hash256",
        "equation_SHA_helpers.k_reqs",
        "equation_SHA_helpers.size_block_w_256",
        "equation_SHA_helpers.ws_quad32",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.bits_of_byte", "equation_Types_s.byte_to_twobits",
        "equation_Types_s.quad32", "equation_Types_s.select_word",
        "equation_Types_s.twobits", "equation_Words.Four_s.four_select",
        "equation_Words_s.nat2", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_Words_s.natN", "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat2", "int_inversion", "int_typing",
        "l_and-interp", "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_30705d7617ba881840faafa6e12d5005",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_78ade0fed5734dbdc55c73a07ba22845",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_Spec.Hash.Definitions.state_word_length",
        "typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_Workarounds.index_work_around_quad32",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rcx@tok", "unit_typing"
      ],
      0,
      "2d6dc0347fab45d80b167ed58e684c7b"
    ],
    [
      "X64.SHA.va_wp_loop_rounds_16_51_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
      ],
      0,
      "f574e4e27afde6156ee9a1a41b7808d7"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_rounds_16_51_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_loop_rounds_16_51_body",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
      ],
      0,
      "a8c1cb65857bbbab91feb7f09d4cb677"
    ],
    [
      "X64.SHA.va_wpCompute_loop_rounds_16_51_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_loop_rounds_16_51_body",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "8e0570fb037259856d53f01e423aef80"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_16_51_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "19af30b8727155b2fe0a75b62a42cf3e"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_16_51_body",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok", "equation_Prims.nat",
        "equation_SHA_helpers.counter",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_loop_rounds_16_51_body",
        "equation_X64.SHA.va_wp_loop_rounds_16_51_body",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_loop_rounds_16_51_body",
        "typing_SHA_helpers.ws_quad32",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
      ],
      0,
      "8a2187d02ae53d6a4fcdad23ef2d154a"
    ],
    [
      "X64.SHA.va_lemma_msg_shift",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.logical",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.l_and", "int_typing",
        "kinding_Prims.equals@tok", "l_and-interp",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "string_typing", "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_Prims.squash",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_Types_s.quad32", "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok", "unit_typing"
      ],
      0,
      "aa27ba5d65861449944c28ff25fc4f60"
    ],
    [
      "X64.SHA.va_wpMonotone_msg_shift",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_msg_shift",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
      ],
      0,
      "9a9fcae00e55589e631dfb5faccd2210"
    ],
    [
      "X64.SHA.va_wpCompute_msg_shift",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_msg_shift",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "97b8ccb3b7e0bbc843fee95cd56e0f7b"
    ],
    [
      "X64.SHA.va_wpProof_msg_shift",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "8f3a50dd2390e22b54bca0bb32fff3a0"
    ],
    [
      "X64.SHA.va_wpProof_msg_shift",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_msg_shift",
        "equation_X64.SHA.va_wp_msg_shift",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_msg_shift",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok", "unit_typing"
      ],
      0,
      "9646e7f0b2720a083d4900483b8a9e22"
    ],
    [
      "X64.SHA.va_transparent_code_loop_rounds_16_51_recursive",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_0", "equation_Prims.nat",
        "int_inversion", "int_typing", "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "well-founded-ordering-on-nat"
      ],
      0,
      "392de9d578018f99306944d82bab646e"
    ],
    [
      "X64.SHA.va_transparent_code_loop_rounds_16_51_recursive",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
        "equation_Prims.nat", "int_typing",
        "projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
      ],
      0,
      "2e8a7b6aaf2c91888e57303df0ccc025"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_16_51_recursive",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
        "equation_SHA_helpers.hash256",
        "refinement_interpretation_Tm_refine_4c2a6cf89c770d3d5ae1539757c4bf6f"
      ],
      0,
      "e5eaed11db3baba29917e386ee209a40"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_16_51_recursive",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
        "equation_SHA_helpers.hash256",
        "refinement_interpretation_Tm_refine_4c2a6cf89c770d3d5ae1539757c4bf6f"
      ],
      0,
      "3b7b1bc7a1a79274802f01a9a7a3d4e4"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_16_51_recursive",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_X64.SHA.va_code_loop_rounds_16_51_recursive.fuel_instrumented",
        "@fuel_correspondence_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive.fuel_instrumented",
        "@fuel_irrelevance_X64.SHA.va_code_loop_rounds_16_51_recursive.fuel_instrumented",
        "@fuel_irrelevance_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_661f8a7e3bd81eb0a2bc263395f5dddc_1",
        "binder_x_e22ba7a032a73f6d0678d3d186686631_2",
        "binder_x_fc86bc8eb8e2bf328df1838e1072996e_4", "bool_inversion",
        "constructor_distinct_Prims.Cons",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_X64.Machine_s.Block",
        "disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
        "eq2-interp", "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Prims.nat", "equation_SHA_helpers.block_w",
        "equation_SHA_helpers.counter",
        "equation_SHA_helpers.size_block_w_256",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "equation_with_fuel_X64.SHA.va_code_loop_rounds_16_51_recursive.fuel_instrumented",
        "equation_with_fuel_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive.fuel_instrumented",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_SHA_helpers.word", "int_inversion",
        "int_typing", "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_upd_eq",
        "lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_GreaterThan",
        "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
        "proj_equation_X64.Machine_s.Block_block",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_X64.Machine_s.Block_block",
        "projection_inverse_X64.Machine_s.Block_t_ins",
        "projection_inverse_X64.Machine_s.Block_t_ocmp",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "subterm_ordering_Prims.Cons",
        "subterm_ordering_X64.Machine_s.Block",
        "typing_FStar.Seq.Base.length", "typing_SHA_helpers.ws_quad32",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.SHA.va_transparent_code_loop_rounds_16_51_recursive",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
        "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok"
      ],
      0,
      "fd5892f8b2e430fa2ae4abedb272ab42"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_16_51",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Prims.Cons",
        "constructor_distinct_X64.Machine_s.Block",
        "disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
        "eq2-interp", "equation_X64.SHA.va_code_loop_rounds_16_51",
        "equation_X64.SHA.va_transparent_code_loop_rounds_16_51",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
        "proj_equation_X64.Machine_s.Block_block",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_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_X64.Machine_s.Block_block",
        "projection_inverse_X64.Machine_s.Block_t_ins",
        "projection_inverse_X64.Machine_s.Block_t_ocmp",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok"
      ],
      0,
      "4b4678b4f774780ae0dd48dd66383316"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_rounds_16_51",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_loop_rounds_16_51",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
      ],
      0,
      "728fba1ceba73a5400c2fb6d5fd6d813"
    ],
    [
      "X64.SHA.va_wpCompute_loop_rounds_16_51",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_code_loop_rounds_16_51",
        "equation_X64.SHA.va_wp_loop_rounds_16_51",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "8e232540bd6a12dca535cea2d28f7647"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_16_51",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "a296210b137a0759b945bd8154b78c47"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_16_51",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok", "equation_Prims.nat",
        "equation_SHA_helpers.block_w", "equation_SHA_helpers.counter",
        "equation_SHA_helpers.hash256",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_code_loop_rounds_16_51",
        "equation_X64.SHA.va_wpCompute_loop_rounds_16_51",
        "equation_X64.SHA.va_wp_loop_rounds_16_51",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f28dc85b4b10d4fff3b43739c58e4784",
        "token_correspondence_X64.SHA.va_wpCompute_loop_rounds_16_51",
        "typing_SHA_helpers.ws_quad32",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.SHA.va_code_loop_rounds_16_51",
        "typing_X64.SHA.va_lemma_loop_rounds_16_51",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok", "unit_typing"
      ],
      0,
      "c8cddd234c8861ff4267845b6e4702ff"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds_52_64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Tm_unit", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Arch.Types.add_wrap_quad32", "equation_Prims.eq2",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_SHA_helpers.hash256",
        "equation_SHA_helpers.k_reqs", "equation_SHA_helpers.ws_quad32",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.bits_of_byte", "equation_Types_s.byte_to_twobits",
        "equation_Types_s.quad32", "equation_Types_s.select_word",
        "equation_Types_s.twobits", "equation_Words.Four_s.four_select",
        "equation_Words_s.nat2", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.nat8",
        "equation_Words_s.natN", "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat2", "int_inversion", "int_typing",
        "l_and-interp", "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_30705d7617ba881840faafa6e12d5005",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_78ade0fed5734dbdc55c73a07ba22845",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_Spec.Hash.Definitions.state_word_length",
        "typing_Types_s.byte_to_twobits", "typing_Types_s.select_word",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_Workarounds.index_work_around_quad32",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdx@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "bf2706762cb5a52fa0b034688b6bf384"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_rounds_52_64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_loop_rounds_52_64",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
      ],
      0,
      "28580f2bbe96f435f572eccf3cc29c2d"
    ],
    [
      "X64.SHA.va_wpCompute_loop_rounds_52_64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_loop_rounds_52_64",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "8b2a5799ef3c33b3331fa6e67c3bd4eb"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_52_64",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "e0e6433f2c3e4af3f804ca8bd46d6795"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds_52_64",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_loop_rounds_52_64",
        "equation_X64.SHA.va_wp_loop_rounds_52_64",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_loop_rounds_52_64",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
      ],
      0,
      "2d73a628edd9374fad1b4cbcf8e4c898"
    ],
    [
      "X64.SHA.va_qcode_loop_rounds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Types_s.quad32",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_337cdcfacffc90745df0e3b2954dd394",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "88940b133d54699702098d0cf02a2224"
    ],
    [
      "X64.SHA.va_lemma_loop_rounds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Collections.Seqs_s.compose",
        "equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.logical",
        "equation_Prims.nat", "equation_SHA_helpers.hash256",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.l_and",
        "function_token_typing_SHA_helpers.hash256",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "kinding_Prims.equals@tok", "kinding_Words_s.four@tok",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
        "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_Prims.l_and", "typing_Prims.squash",
        "typing_SHA_helpers.make_hash",
        "typing_SHA_helpers.update_multi_quads",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "736211cd140c71757d1d7f21b4dd3dea"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_rounds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop_rounds",
        "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "114944520df64762dad84ce95709afb7"
    ],
    [
      "X64.SHA.va_wpCompute_loop_rounds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_loop_rounds",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "563b9de6bf7c320622241624a2804a1f"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "318f2dfe34a129bfb76a43eecc88c6c7"
    ],
    [
      "X64.SHA.va_wpProof_loop_rounds",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_loop_rounds",
        "equation_X64.SHA.va_wp_loop_rounds",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_loop_rounds",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "346483dbab60d3dd988073ec158e19cc"
    ],
    [
      "X64.SHA.va_qcode_loop_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "fe891c038529e22b7ebbfad807907a0a"
    ],
    [
      "X64.SHA.va_lemma_loop_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Prims.LexTop@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Collections.Seqs_s.compose",
        "equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.logical",
        "equation_Prims.nat", "equation_SHA_helpers.hash256",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrsOffset128",
        "equation_X64.Vale.QuickCodes.lexCons",
        "equation_X64.Vale.QuickCodes.precedes_wrap",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.state_eta",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_SHA_helpers.hash256",
        "function_token_typing_Words_s.nat32",
        "function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
        "kinding_Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Regs.lemma_eta",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
        "typing_FStar.Seq.Base.length", "typing_Prims.eq2",
        "typing_SHA_helpers.make_hash",
        "typing_SHA_helpers.update_multi_quads",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Vale.Decls.validSrcAddrs128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.lexCons",
        "typing_X64.Vale.QuickCodes.precedes_wrap",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Prims.LexTop@tok", "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "3bf80e88c2dabda986ce11ba16cd531d"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop_body",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "0862acdb9ad4f21688d140534447e426"
    ],
    [
      "X64.SHA.va_wpCompute_loop_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_loop_body",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "025e7dd3edef1d7825308935c5f24fa4"
    ],
    [
      "X64.SHA.va_wpProof_loop_body",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "70710eb7bfe9a562268bc214d93407d5"
    ],
    [
      "X64.SHA.va_wpProof_loop_body",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_loop_body",
        "equation_X64.SHA.va_wp_loop_body",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_loop_body",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "b4e17dda0c481b230a114a8a764a208a"
    ],
    [
      "X64.SHA.va_lemma_loop_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "eq2-interp", "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Prims.LexTop@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_False",
        "equation_Prims.l_imp", "equation_Prims.l_not",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_SHA_helpers.hash256",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.QuickCodes.lexCons",
        "equation_X64.Vale.QuickCodes.precedes_wrap",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.state_eta",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_SHA_helpers.hash256",
        "function_token_typing_Words_s.nat32", "int_typing",
        "kinding_Words_s.four@tok", "l_not-interp",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Regs.lemma_eta",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_GreaterThan",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
        "typing_Prims.eq2", "typing_SHA_helpers.make_hash",
        "typing_SHA_helpers.update_multi_quads",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Vale.Decls.validSrcAddrs128",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
      ],
      0,
      "0f2e057fe339ab73b72184720c3b74e8"
    ],
    [
      "X64.SHA.va_wpMonotone_loop_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop_while",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "e64ca6f55fb12ad9737503b76a75ac34"
    ],
    [
      "X64.SHA.va_wpCompute_loop_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_code_loop_while",
        "equation_X64.SHA.va_wp_loop_while",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "7e0c5789b53512be0f261e982edb881f"
    ],
    [
      "X64.SHA.va_wpProof_loop_while",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "970db240b1784d699342b21c15d4b4fb"
    ],
    [
      "X64.SHA.va_wpProof_loop_while",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_code_loop_while",
        "equation_X64.SHA.va_wpCompute_loop_while",
        "equation_X64.SHA.va_wp_loop_while",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_loop_while",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "d20935ca6611842375cfc80d7bce25a9"
    ],
    [
      "X64.SHA.va_lemma_loop",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_SHA_helpers.update_multi_quads.fuel_instrumented",
        "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
        "Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Spec.Hash.Definitions.MD5", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok",
        "equation_Arch.Types.reverse_bytes_quad32_seq",
        "equation_Collections.Seqs_s.compose",
        "equation_Collections.Seqs_s.seq_map", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.logical",
        "equation_Prims.nat", "equation_SHA_helpers.hash256",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_Words_s.nat32",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.State.state_eq",
        "equation_with_fuel_SHA_helpers.update_multi_quads.fuel_instrumented",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_Prims.l_and",
        "function_token_typing_SHA_helpers.hash256", "int_inversion",
        "int_typing", "kinding_Prims.equals@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Prims.eq2", "typing_Prims.squash",
        "typing_SHA_helpers.make_hash",
        "typing_SHA_helpers.update_multi_quads",
        "typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.base_typ_as_vale_type",
        "typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Memory.buffer_length",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "49d6846facb52146ef8283f5a4f76df9"
    ],
    [
      "X64.SHA.va_wpMonotone_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_loop",
        "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "75738f3fd9e6050b70f8e2df2468f023"
    ],
    [
      "X64.SHA.va_wpCompute_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_loop",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "68f9a0901f421a20b1425d6db77573f8"
    ],
    [
      "X64.SHA.va_wpProof_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "639744b45b1ad3f15372ec432ce9bd1e"
    ],
    [
      "X64.SHA.va_wpProof_loop",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wpCompute_loop",
        "equation_X64.SHA.va_wp_loop",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_loop",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "28d0da53d99201f5a5913a68106e3f25"
    ],
    [
      "X64.SHA.va_lemma_epilogue",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Tm_unit", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prop_s.prop0",
        "equation_SHA_helpers.hash256", "equation_Types_s.bits_of_byte",
        "equation_Types_s.byte_to_twobits", "equation_Types_s.quad32",
        "equation_Types_s.select_word", "equation_Types_s.twobits",
        "equation_Words.Four_s.four_select", "equation_Words_s.nat2",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_SHA_helpers.word",
        "function_token_typing_Words_s.nat2",
        "function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
        "interpretation_Tm_abs_468206d1e1978da391344670f4f23403",
        "interpretation_Tm_abs_6d69aedb2edc4e3d4a0c9a18d04d64d6",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "proj_equation_Words_s.Mkfour_hi2",
        "proj_equation_Words_s.Mkfour_hi3",
        "proj_equation_Words_s.Mkfour_lo0",
        "proj_equation_Words_s.Mkfour_lo1",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_Words_s.Mkfour_hi2",
        "projection_inverse_Words_s.Mkfour_hi3",
        "projection_inverse_Words_s.Mkfour_lo0",
        "projection_inverse_Words_s.Mkfour_lo1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4309c8fc5805d1cd049b287c438261e3",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_90829fc0fedd6c06cca9e3be6cec3223",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.l_and", "typing_SHA_helpers.make_hash",
        "typing_SHA_helpers.make_ordered_hash",
        "typing_Types_s.byte_to_twobits", "typing_Types_s.quad32",
        "typing_Types_s.select_word",
        "typing_Words_s.__proj__Mkfour__item__hi2",
        "typing_Words_s.__proj__Mkfour__item__hi3",
        "typing_Words_s.__proj__Mkfour__item__lo1",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Memory.modifies", "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rdi@tok", "unit_typing"
      ],
      0,
      "f5b2b496d7ede8d967a62c062c1154e1"
    ],
    [
      "X64.SHA.va_wpMonotone_epilogue",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_epilogue",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_xmm", "unit_typing"
      ],
      0,
      "75fe7a2c4036de16443cede368a4fca8"
    ],
    [
      "X64.SHA.va_wpCompute_epilogue",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_epilogue",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "b97f89a73651c276d93874c64012e0b5"
    ],
    [
      "X64.SHA.va_wpProof_epilogue",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "b4bbe6188ba4b4ef25dac8332d483aa9"
    ],
    [
      "X64.SHA.va_wpProof_epilogue",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_epilogue",
        "equation_X64.SHA.va_wp_epilogue",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_epilogue",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd", "unit_typing"
      ],
      0,
      "1282edb1427a479d4d1a19e36af5735a"
    ],
    [
      "X64.SHA.va_lemma_sha_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eqtype",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prop_s.prop0", "equation_SHA_helpers.hash256",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.State.state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_SHA_helpers.hash256", "int_typing",
        "l_and-interp", "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4309c8fc5805d1cd049b287c438261e3",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "string_typing", "typing_Arch.Types.reverse_bytes_quad32_seq",
        "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_SHA_helpers.make_ordered_hash",
        "typing_SHA_helpers.update_multi_quads",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.base_typ_as_vale_type",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.loc_buffer", "typing_X64.Memory.modifies",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "9e8bdb08040336cadd97851ca287543c"
    ],
    [
      "X64.SHA.va_wpMonotone_sha_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm", "equation_X64.SHA.va_wp_sha_update",
        "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "f1d7832778bc82c9532558dc54db4fb4"
    ],
    [
      "X64.SHA.va_wpCompute_sha_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_sha_update",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "312908ab99f1192ae111228d707834ea"
    ],
    [
      "X64.SHA.va_wpProof_sha_update",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "460a57d4c415b45d48a1da3686e8c0c1"
    ],
    [
      "X64.SHA.va_wpProof_sha_update",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_sha_update",
        "equation_X64.SHA.va_wp_sha_update",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_sha_update",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "3cab84c4874b4c5590865b4ac9840111"
    ],
    [
      "X64.SHA.va_qcode_sha_update_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
        "equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "ce3c40fb054466fb401e58e2908a719c"
    ],
    [
      "X64.SHA.va_qcode_sha_update_bytes",
      2,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "c68037992b67f03b5e2d831660025f6d"
    ],
    [
      "X64.SHA.va_qcode_sha_update_bytes",
      3,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "51f763fa943e6d0528ea1301813da923"
    ],
    [
      "X64.SHA.va_qcode_sha_update_bytes",
      4,
      1,
      0,
      [
        "@query", "equation_SHA_helpers.block_length",
        "equation_SHA_helpers.size_block_w_256",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "4ace864f9144784e632988905f131b24"
    ],
    [
      "X64.SHA.va_lemma_sha_update_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.logical", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prop_s.prop0",
        "equation_SHA_helpers.byte", "equation_SHA_helpers.hash256",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Types_s.quad32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.state_eta",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "function_token_typing_SHA_helpers.hash256", "int_inversion",
        "int_typing", "l_and-interp",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Regs.lemma_eta",
        "lemma_X64.Vale.Xmms.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_63d8ee4775e7b68bb741190dd73c78c8",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "typing_Prims.eq2", "typing_Prims.l_and",
        "typing_SHA_helpers.le_bytes_to_hash",
        "typing_Types_s.le_seq_quad32_to_bytes",
        "typing_Workarounds.slice_workaround",
        "typing_X64.CPU_Features_s.sha_enabled",
        "typing_X64.Memory.base_typ_as_vale_type",
        "typing_X64.Memory.buffer_as_seq", "typing_X64.Memory.buffer_length",
        "typing_X64.Memory.buffer_read", "typing_X64.Memory.loc_buffer",
        "typing_X64.Memory.modifies", "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_inversion", "unit_typing"
      ],
      0,
      "1eac22e896267f307e1faa2000840ecb"
    ],
    [
      "X64.SHA.va_wpMonotone_sha_update_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_sha_update_bytes",
        "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "1cb190f88916c6182137b5fa5666ccfd"
    ],
    [
      "X64.SHA.va_wpCompute_sha_update_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_X64.SHA.va_wp_sha_update_bytes",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state"
      ],
      0,
      "3c113e7234b69beb39be07ac0c831556"
    ],
    [
      "X64.SHA.va_wpProof_sha_update_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "937fc356621361dc9617f7f629f05d09"
    ],
    [
      "X64.SHA.va_wpProof_sha_update_bytes",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_SHA_helpers.byte",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_sha_update_bytes",
        "equation_X64.SHA.va_wp_sha_update_bytes",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "primitive_Prims.op_Equality",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_sha_update_bytes",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_ok",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "3df984b2c6fa56f3d3af1fd8e3da1ff7"
    ],
    [
      "X64.SHA.va_req_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "4d2f8d16a4f79a52457f651e153bc232"
    ],
    [
      "X64.SHA.va_ens_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prims.subtype_of", "equation_SHA_helpers.block_length",
        "equation_SHA_helpers.byte", "equation_SHA_helpers.size_block_w_256",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.SHA.va_req_sha_update_bytes_stdcall",
        "equation_X64.Vale.Decls.va_state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok", "unit_typing"
      ],
      0,
      "0e77eb17ee8f28464b6a6b84710151d6"
    ],
    [
      "X64.SHA.va_qcode_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.block_length",
        "equation_SHA_helpers.size_block_w_256", "equation_Words_s.nat64",
        "equation_Words_s.natN", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
      ],
      0,
      "7561da3f94cf9daa4c214e7fa484a41d"
    ],
    [
      "X64.SHA.va_qcode_sha_update_bytes_stdcall",
      2,
      1,
      0,
      [
        "@query", "equation_SHA_helpers.block_length",
        "equation_SHA_helpers.size_block_w_256",
        "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "5cdcb039a4ac447a4e767c4ca71cae42"
    ],
    [
      "X64.SHA.va_lemma_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
        "equation_SHA_helpers.block_length", "equation_SHA_helpers.byte",
        "equation_SHA_helpers.size_block_w_256", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Memory.buffer128",
        "equation_X64.Memory.vuint128",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_X64.CPU_Features_s.sha_enabled",
        "function_token_typing_X64.Memory.vuint128", "int_inversion",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
        "refinement_interpretation_X64.SHA_Tm_refine_bef743ed8e583a213aacac0db17045bb",
        "typing_X64.Memory.buffer_length", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok"
      ],
      0,
      "2623997970b570e93b1bcf1e65e85fcc"
    ],
    [
      "X64.SHA.va_lemma_sha_update_bytes_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
        "Prims_interpretation_Tm_arrow_fa4e3ee4a3dfa402363cd0693fcbfca4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
        "bool_inversion", "constructor_distinct_Interop.Types.TUInt128",
        "constructor_distinct_Interop.Types.TUInt64",
        "constructor_distinct_X64.Machine_s.OReg",
        "constructor_distinct_X64.Machine_s.Rax",
        "constructor_distinct_X64.Vale.Decls.TReg",
        "disc_equation_X64.Machine_s.Rsp", "eq2-interp",
        "equality_tok_Interop.Types.TUInt128@tok",
        "equality_tok_Interop.Types.TUInt64@tok",
        "equality_tok_X64.Machine_s.Public@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Arch.Types.hi64",
        "equation_Arch.Types.lo64", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.l_and",
        "equation_Prims.l_imp", "equation_Prims.logical",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Prop_s.prop0", "equation_SHA_helpers.block_length",
        "equation_SHA_helpers.byte", "equation_SHA_helpers.hash256",
        "equation_SHA_helpers.k_reqs",
        "equation_SHA_helpers.size_block_w_256",
        "equation_Types_s.le_seq_quad32_to_bytes", "equation_Types_s.quad32",
        "equation_Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Words_s.nat32", "equation_Words_s.nat64",
        "equation_Words_s.nat8", "equation_Words_s.natN",
        "equation_X64.Machine_s.xmm",
        "equation_X64.Memory.base_typ_as_vale_type",
        "equation_X64.Memory.buffer128", "equation_X64.Memory.buffer64",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_operand_dst_opr64",
        "equation_X64.Vale.Decls.va_upd_operand_reg_opr64",
        "equation_X64.Vale.Decls.va_upd_operand_xmm",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.Decls.validDstAddrs128",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "equation_X64.Vale.Decls.valid_stack_slots",
        "equation_X64.Vale.QuickCodes.range1",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.state_eta",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_Words_s.four",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Arch.Types.hi64_def",
        "function_token_typing_Arch.Types.lo64_def",
        "function_token_typing_Opaque_s.make_opaque",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_SHA_helpers.word",
        "function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
        "kinding_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b", "l_and-interp",
        "l_imp-interp", "l_not-interp",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "lemma_X64.Memory.buffer_length_buffer_as_seq",
        "lemma_X64.Memory.loc_includes_refl",
        "lemma_X64.Memory.loc_includes_union_l_buffer",
        "lemma_X64.Memory.modifies_buffer_addr",
        "lemma_X64.Memory.modifies_buffer_elim",
        "lemma_X64.Memory.modifies_buffer_readable",
        "lemma_X64.Memory.modifies_goal_directed_refl",
        "lemma_X64.Memory.modifies_goal_directed_trans",
        "lemma_X64.Memory.modifies_goal_directed_trans2",
        "lemma_X64.Memory.modifies_valid_taint128",
        "lemma_X64.Memory.modifies_valid_taint64",
        "lemma_X64.Vale.QuickCodes.lemma_label_bool",
        "lemma_X64.Vale.Regs.lemma_equal_intro",
        "lemma_X64.Vale.Xmms.lemma_equal_intro",
        "primitive_Prims.op_Equality", "proj_equation_X64.Machine_s.OReg_r",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_X64.Machine_s.OReg_r",
        "projection_inverse_X64.Vale.Decls.TReg_r",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
        "refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
        "refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1",
        "refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
        "refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "string_typing", "token_correspondence_Opaque_s.make_opaque",
        "typing_Arch.Types.hi64", "typing_Arch.Types.lo64",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.upd",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_Prims.l_and", "typing_SHA_helpers.le_bytes_to_hash",
        "typing_Types_s.le_seq_quad32_to_bytes", "typing_Types_s.quad32",
        "typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
        "typing_X64.Memory.buffer_length", "typing_X64.Memory.buffer_read",
        "typing_X64.Memory.buffer_readable",
        "typing_X64.Memory.buffer_write",
        "typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
        "typing_X64.Memory.loc_union", "typing_X64.Memory.modifies",
        "typing_X64.Vale.QuickCodes.label",
        "typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.Xmms.eta_sel",
        "typing_tok_Interop.Types.TUInt128@tok",
        "typing_tok_Interop.Types.TUInt64@tok",
        "typing_tok_X64.Machine_s.Public@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok",
        "typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
        "unit_typing"
      ],
      0,
      "9700413f1d9e5925549cc3a094ef318f"
    ],
    [
      "X64.SHA.va_wp_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.nat", "equation_SHA_helpers.block_length",
        "equation_SHA_helpers.byte", "equation_SHA_helpers.size_block_w_256",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Words_s.nat64",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
        "typing_X64.SHA_Tm_abs_33c3994de7d754283ab0cc7b2921b72e",
        "typing_X64.SHA_Tm_abs_b1e1a7fb7a7968d210062719315e71c2",
        "typing_X64.SHA_Tm_abs_c2631d9abab9b993938b087d5057f4af",
        "typing_X64.SHA_Tm_abs_c2bb5b1221b8afc9d05888f8b139b633",
        "typing_X64.Vale.Decls.va_if", "unit_typing"
      ],
      0,
      "3c4b37293dc982db8320d6e9040a0d19"
    ],
    [
      "X64.SHA.va_wpMonotone_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wp_sha_update_bytes_stdcall",
        "equation_X64.Vale.Decls.va_upd_reg",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm",
        "typing_X64.Vale.State.update_reg",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "b2bdc96980c0619abe52623c19c0e327"
    ],
    [
      "X64.SHA.va_wpCompute_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "eq2-interp", "equation_Words_s.nat64",
        "equation_X64.SHA.va_wp_sha_update_bytes_stdcall",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
        "interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
        "interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
        "interpretation_Tm_abs_37e6950d37c672ed920358e612e03225",
        "interpretation_Tm_abs_50c23f9cc303c7ea6b4d93bbc25b4c06",
        "interpretation_Tm_abs_5e1158cd2d105ad253ac372e98cd91e5",
        "interpretation_Tm_abs_b6f39720dc3d793091496036edf9db50",
        "interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
        "unit_typing"
      ],
      0,
      "74b8bb4e7f0cf9054aa84f9f3a1bc9c9"
    ],
    [
      "X64.SHA.va_wpProof_sha_update_bytes_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "7cd3bb48edea6060e6c3b09b73801259"
    ],
    [
      "X64.SHA.va_wpProof_sha_update_bytes_stdcall",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1", "eq2-interp",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_X64.Machine_s.R10@tok",
        "equality_tok_X64.Machine_s.R11@tok",
        "equality_tok_X64.Machine_s.R12@tok",
        "equality_tok_X64.Machine_s.R13@tok",
        "equality_tok_X64.Machine_s.R14@tok",
        "equality_tok_X64.Machine_s.R15@tok",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.R9@tok",
        "equality_tok_X64.Machine_s.Rax@tok",
        "equality_tok_X64.Machine_s.Rbp@tok",
        "equality_tok_X64.Machine_s.Rbx@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Rsp@tok",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Words_s.nat64", "equation_X64.Machine_s.xmm",
        "equation_X64.SHA.va_wpCompute_sha_update_bytes_stdcall",
        "equation_X64.SHA.va_wp_sha_update_bytes_stdcall",
        "equation_X64.Vale.Decls.va_ensure_total",
        "equation_X64.Vale.Decls.va_if",
        "equation_X64.Vale.Decls.va_require_total",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.va_upd_flags",
        "equation_X64.Vale.Decls.va_upd_mem",
        "equation_X64.Vale.Decls.va_upd_ok",
        "equation_X64.Vale.Decls.va_upd_reg",
        "equation_X64.Vale.Decls.va_upd_xmm",
        "equation_X64.Vale.QuickCode.t_ensure",
        "equation_X64.Vale.State.state_eq",
        "equation_X64.Vale.State.update_reg",
        "equation_X64.Vale.State.update_xmm",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "interpretation_Tm_abs_11b846de738c2179f7d8a25fd5d8134c",
        "interpretation_Tm_abs_1a66d9ca182b0d13ee08d2b4b97bb5fc",
        "interpretation_Tm_abs_1d56deaaa71b4a0e09272738adc9090f",
        "interpretation_Tm_abs_37e6950d37c672ed920358e612e03225",
        "interpretation_Tm_abs_50c23f9cc303c7ea6b4d93bbc25b4c06",
        "interpretation_Tm_abs_5e1158cd2d105ad253ac372e98cd91e5",
        "interpretation_Tm_abs_b6f39720dc3d793091496036edf9db50",
        "interpretation_Tm_abs_cf511aacfa266870cb915fb5be9ad81d",
        "lemma_X64.Vale.Regs.lemma_equal_elim",
        "lemma_X64.Vale.Xmms.lemma_equal_elim",
        "proj_equation_X64.Vale.State.Mkstate_flags",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "proj_equation_X64.Vale.State.Mkstate_ok",
        "proj_equation_X64.Vale.State.Mkstate_regs",
        "proj_equation_X64.Vale.State.Mkstate_xmms",
        "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_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_X64.Vale.State.Mkstate_flags",
        "projection_inverse_X64.Vale.State.Mkstate_mem",
        "projection_inverse_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_X64.Vale.State.Mkstate_ok",
        "projection_inverse_X64.Vale.State.Mkstate_regs",
        "projection_inverse_X64.Vale.State.Mkstate_xmms",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "token_correspondence_X64.SHA.va_wpCompute_sha_update_bytes_stdcall",
        "typing_Spec.Hash.Definitions.state_word_length",
        "typing_X64.Vale.Decls.va_upd_flags",
        "typing_X64.Vale.Decls.va_upd_mem",
        "typing_X64.Vale.Decls.va_upd_reg",
        "typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.Regs.upd",
        "typing_X64.Vale.State.__proj__Mkstate__item__flags",
        "typing_X64.Vale.State.__proj__Mkstate__item__mem",
        "typing_X64.Vale.State.__proj__Mkstate__item__ok",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_X64.Vale.State.__proj__Mkstate__item__xmms",
        "typing_X64.Vale.State.update_reg", "typing_X64.Vale.Xmms.sel",
        "typing_tok_Spec.Hash.Definitions.MD5@tok",
        "typing_tok_Spec.Hash.Definitions.SHA1@tok",
        "typing_tok_X64.Machine_s.R10@tok",
        "typing_tok_X64.Machine_s.R11@tok",
        "typing_tok_X64.Machine_s.R12@tok",
        "typing_tok_X64.Machine_s.R13@tok",
        "typing_tok_X64.Machine_s.R14@tok",
        "typing_tok_X64.Machine_s.R15@tok",
        "typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
        "typing_tok_X64.Machine_s.Rax@tok",
        "typing_tok_X64.Machine_s.Rbp@tok",
        "typing_tok_X64.Machine_s.Rbx@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok",
        "typing_tok_X64.Machine_s.Rsp@tok", "unit_typing"
      ],
      0,
      "749a23609b2dfd6f87504c69ee737be3"
    ]
  ]
]