[
  "¸‚3}\u0000\t&˜6¨\u000f@‰ÔÉÀ",
  [
    [
      "Vale.SHA.SHA_helpers.vv",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "482bea1fae40a0a7d071a17906d980e7"
    ],
    [
      "Vale.SHA.SHA_helpers.to_uint32",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "dd5879bb7f2bd9286711e50a6d111e50"
    ],
    [
      "Vale.SHA.SHA_helpers.k",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.List.Tot.Properties.llist",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.SHA2.k0",
        "equation_Spec.SHA2.size_k_w", "equation_Vale.SHA.SHA_helpers.word",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
        "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
        "typing_Spec.SHA2.Constants.k224_256",
        "typing_Spec.SHA2.Constants.k224_256_l"
      ],
      0,
      "df32e51be9cdba9b8f55766a926c3d00"
    ],
    [
      "Vale.SHA.SHA_helpers.reveal_word",
      1,
      0,
      0,
      [ "@query", "equation_Vale.SHA.SHA_helpers.word" ],
      0,
      "c4f5ed082b8af39e9f3f4f518ecc5d1b"
    ],
    [
      "Vale.SHA.SHA_helpers.bytes_blocks",
      1,
      0,
      0,
      [
        "@query", "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "fba41a2c7990d6d026a819d4d761c0f3"
    ],
    [
      "Vale.SHA.SHA_helpers.add_mod_lemma",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.unsigned", "primitive_Prims.op_AmpAmp",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v"
      ],
      0,
      "32dd5b8c0e7f1e5588f4be05362e7441"
    ],
    [
      "Vale.SHA.SHA_helpers.add_mod_lemma",
      2,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.add_mod"
      ],
      0,
      "6738cf9f68d1c6d1773013d34e432719"
    ],
    [
      "Vale.SHA.SHA_helpers.ws_opaque",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413"
      ],
      0,
      "74a92e9fdd687bc1b5a2a267b29d52e3"
    ],
    [
      "Vale.SHA.SHA_helpers.shuffle_core_opaque",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "1e61bbc96649ccfc168dfa0db2106efb"
    ],
    [
      "Vale.SHA.SHA_helpers.update_multi_reveal",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "6a4809b1aeb5d2b41897f2cb8b95394c"
    ],
    [
      "Vale.SHA.SHA_helpers.update_multi_opaque",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.byte",
        "equation_Vale.SHA.SHA_helpers.bytes_blocks",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3891824b4d5874bf21bffea346ced817",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "487ecf01da390f83f23c6a3e480e6d72"
    ],
    [
      "Vale.SHA.SHA_helpers.update_multi_transparent",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.byte",
        "equation_Vale.SHA.SHA_helpers.bytes_blocks",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3891824b4d5874bf21bffea346ced817",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "17771551420630e2854c0a385700bcb3"
    ],
    [
      "Vale.SHA.SHA_helpers.byte_to_nat8",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "c90958f929ad1ff6506764f601da7efd"
    ],
    [
      "Vale.SHA.SHA_helpers.nat8_to_byte",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "0ea66905159dac3c22971e2610c391ab"
    ],
    [
      "Vale.SHA.SHA_helpers.repeat_range_vale",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6c6633917f79a67f4eaac4ed70320fc6"
      ],
      0,
      "79dfc39a975efbeadc7a41b889b4797e"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_repeat_range_0_vale",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "827ee9722ddce001365384d9b639669e"
    ],
    [
      "Vale.SHA.SHA_helpers.update_multi_opaque_vale",
      1,
      0,
      0,
      [
        "@query", "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "a1334c6dc90cd3a6ecfb990cbd1563eb"
    ],
    [
      "Vale.SHA.SHA_helpers.make_hash_def",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.empty", "typing_Spec.Hash.Definitions.word",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "4320ed9b7e590c5e2f790c763816053c"
    ],
    [
      "Vale.SHA.SHA_helpers.make_hash",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "b0d160a93a809baf916bc58ea5fc0de8"
    ],
    [
      "Vale.SHA.SHA_helpers.make_hash",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_7c31e8b82bdef68848aee4f5c92045ff",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "8366a566daa0f5ec46cad0b736118777"
    ],
    [
      "Vale.SHA.SHA_helpers.make_hash_reveal",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_7c31e8b82bdef68848aee4f5c92045ff",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "893a2fdc888823840db44306994e2e26"
    ],
    [
      "Vale.SHA.SHA_helpers.make_ordered_hash_def",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.empty", "typing_Spec.Hash.Definitions.word",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "5beb13b9555ccd7c5265fb8402352bd8"
    ],
    [
      "Vale.SHA.SHA_helpers.make_ordered_hash",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "ed7240597c39125a3e0e5df2d60eff39"
    ],
    [
      "Vale.SHA.SHA_helpers.make_ordered_hash",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_28077cf21ba34de77aad8edd9839b194",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "95b9f77f42cd68f7bdda02fd427c7f48"
    ],
    [
      "Vale.SHA.SHA_helpers.make_ordered_hash_reveal",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_28077cf21ba34de77aad8edd9839b194",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "bfae298827cd304fc895424f1ebf72c0"
    ],
    [
      "Vale.SHA.SHA_helpers.shuffle_core_properties",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.List.Tot.Properties.llist",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2.Lemmas.shuffle_core_", "equation_Spec.SHA2.k0",
        "equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.shuffle_core_opaque",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Prims.int",
        "function_token_typing_Spec.SHA2.Lemmas.shuffle_core",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Spec.SHA2.Lemmas.shuffle_core_",
        "token_correspondence_Spec.SHA2.op_Plus_Dot",
        "typing_Spec.SHA2.Constants.k224_256",
        "typing_Spec.SHA2.Constants.k224_256_l",
        "typing_Vale.SHA.SHA_helpers.shuffle_core_opaque"
      ],
      0,
      "8795c1388e2a23b282000985e73d4fc6"
    ],
    [
      "Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
      1,
      0,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "062789b9e6ea66dcfe464792440df9e2"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_rnds2_spec_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v", "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
        "equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
        "equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op_Amp_Dot",
        "equation_Spec.SHA2.op_Hat_Dot", "equation_Spec.SHA2.op_Tilde_Dot",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_quad32",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_def",
        "equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.logand",
        "function_token_typing_Lib.IntTypes.logxor",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec",
        "lemma_Lib.IntTypes.v_injective",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.lognot",
        "token_correspondence_Lib.IntTypes.logxor",
        "token_correspondence_Spec.SHA2.op_Amp_Dot",
        "token_correspondence_Spec.SHA2.op_Hat_Dot",
        "token_correspondence_Spec.SHA2.op_Tilde_Dot",
        "token_correspondence_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_def",
        "typing_FStar.UInt32.add_mod", "typing_Lib.IntTypes.logand",
        "typing_Lib.IntTypes.lognot", "typing_Lib.IntTypes.logxor",
        "typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2._Sigma0",
        "typing_Spec.SHA2._Sigma1",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.make_hash",
        "typing_Vale.SHA.SHA_helpers.nat32_to_word",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_Vale.SHA.SHA_helpers.vv", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "251ab2db8bd08a79ef94b11df38ebf89"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_mod_commutes",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.add_mod",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "typing_FStar.UInt32.add_mod"
      ],
      0,
      "de3812a7237eb47b1c821449e69da1e3"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_mod_associates_U32",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.add_mod",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.add_mod", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.add_mod", "typing_FStar.UInt32.v",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5d635e552baca400b25940b7cb3fa741"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_wrap_is_add_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.add_mod",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv", "int_inversion", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add_mod",
        "typing_FStar.UInt32.v", "typing_Lib.IntTypes.mk_int",
        "typing_Lib.IntTypes.v", "typing_Vale.Def.Types_s.add_wrap",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "954057f6c1bae1c7d7ffbabba964307f"
    ],
    [
      "Vale.SHA.SHA_helpers.add_wrap_commutes",
      1,
      0,
      0,
      [ "@query", "equation_Vale.Def.Types_s.add_wrap" ],
      0,
      "d594fe662736558b33a0daa9c783d3df"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_mod_a",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.is_sha2",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "6a03328e767de80681bd41680be83822"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_mod_e",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.UInt.add_mod", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
        "equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op_Hat_Dot",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "token_correspondence_Spec.SHA2.op_Hat_Dot",
        "typing_FStar.UInt32.add_mod"
      ],
      0,
      "4edd063cb03afdcc8b4dd4802519c250"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_rnds2_spec_update_is_shuffle_core",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
        "Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb",
        "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7",
        "b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2.Lemmas.shuffle_core_", "equation_Spec.SHA2._Ch",
        "equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
        "equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.block_w",
        "equation_Spec.SHA2.counter", "equation_Spec.SHA2.k0",
        "equation_Spec.SHA2.op_Amp_Dot", "equation_Spec.SHA2.op_Hat_Dot",
        "equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.op_Tilde_Dot",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.add_mod32",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.shuffle_core_opaque",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Prims.int",
        "function_token_typing_Spec.SHA2.Lemmas.shuffle_core",
        "function_token_typing_Spec.SHA2.op_Plus_Dot",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "l_and-interp", "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.IntTypes.v_injective",
        "lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.lognot",
        "token_correspondence_Lib.IntTypes.logxor",
        "token_correspondence_Spec.SHA2.Lemmas.shuffle_core_",
        "token_correspondence_Spec.SHA2.op_Amp_Dot",
        "token_correspondence_Spec.SHA2.op_Hat_Dot",
        "token_correspondence_Spec.SHA2.op_Plus_Dot",
        "token_correspondence_Spec.SHA2.op_Tilde_Dot",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
        "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.lognot",
        "typing_Lib.IntTypes.logxor", "typing_Spec.Hash.Definitions.word",
        "typing_Spec.SHA2.Constants.k224_256", "typing_Spec.SHA2.Lemmas.ws",
        "typing_Spec.SHA2._Ch", "typing_Spec.SHA2._Maj",
        "typing_Spec.SHA2._Sigma0", "typing_Spec.SHA2._Sigma1",
        "typing_Spec.SHA2.k0", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "2318aa4c8de4a42db02f5597c0304ebf"
    ],
    [
      "Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_core_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.hash256", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "typing_Vale.SHA.SHA_helpers.shuffle_core_opaque"
      ],
      0,
      "0669ddf0586167c7f7e9b8bb0c52ef1a"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_rnds_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.size_k_w",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_core_quad32",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413"
      ],
      0,
      "895a7e3decc6b6e9066f280400268e42"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_rnds2_spec_quad32_is_shuffle_core_x2",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "FStar.UInt32_pretyping_041e3a67a2d2b51fd702f1f88cfc3b44",
        "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
        "equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
        "equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.k0",
        "equation_Spec.SHA2.op_Amp_Dot", "equation_Spec.SHA2.op_Hat_Dot",
        "equation_Spec.SHA2.op_Tilde_Dot", "equation_Spec.SHA2.size_k_w",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.SHA.SHA_helpers.add_mod32",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.make_hash",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_core_quad32",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.logand",
        "function_token_typing_Lib.IntTypes.logxor",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.IntTypes.pow2_2", "lemma_Lib.IntTypes.v_injective",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "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.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_32e0b1133cc20cfb6af3882a041b827f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
        "refinement_interpretation_Tm_refine_d60a0e9fdf52cedb444de54cc40036f8",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.lognot",
        "token_correspondence_Lib.IntTypes.logxor",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "token_correspondence_Spec.SHA2.op_Amp_Dot",
        "token_correspondence_Spec.SHA2.op_Hat_Dot",
        "token_correspondence_Spec.SHA2.op_Tilde_Dot",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
        "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.lognot",
        "typing_Lib.IntTypes.logxor", "typing_Lib.IntTypes.minint",
        "typing_Spec.Hash.Definitions.word",
        "typing_Spec.SHA2.Constants.k224_256", "typing_Spec.SHA2._Sigma0",
        "typing_Spec.SHA2._Sigma1", "typing_Spec.SHA2.k0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.make_hash",
        "typing_Vale.SHA.SHA_helpers.nat32_to_word",
        "typing_Vale.SHA.SHA_helpers.shuffle_core_opaque",
        "typing_Vale.SHA.SHA_helpers.vv", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "c20265aabfb55854da324966a59039d0"
    ],
    [
      "Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32_x2_shifts",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.UInt32_pretyping_2ab3c8ba2d08b0172817fc70b5994868",
        "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2._Ch",
        "equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0",
        "equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op_Amp_Dot",
        "equation_Spec.SHA2.op_Hat_Dot", "equation_Spec.SHA2.op_Tilde_Dot",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_update_quad32",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.X64.CryptoInstructions_s.sha256_rnds2_spec_update",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.logand",
        "function_token_typing_Lib.IntTypes.logxor",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "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.Mktuple8__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
        "projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.lognot",
        "token_correspondence_Lib.IntTypes.logxor",
        "token_correspondence_Spec.SHA2.op_Amp_Dot",
        "token_correspondence_Spec.SHA2.op_Hat_Dot",
        "token_correspondence_Spec.SHA2.op_Tilde_Dot",
        "typing_FStar.UInt32.add_mod", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.logand", "typing_Lib.IntTypes.lognot",
        "typing_Lib.IntTypes.logxor", "typing_Spec.SHA2._Sigma0",
        "typing_Spec.SHA2._Sigma1",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.make_hash",
        "typing_Vale.SHA.SHA_helpers.nat32_to_word",
        "typing_Vale.SHA.SHA_helpers.vv", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "72cb9bec644305c4522ce7f93182e169"
    ],
    [
      "Vale.SHA.SHA_helpers.sha256_rnds2_spec_quad32_is_shuffle_core_x2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2.k0",
        "equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.add_mod32",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.sha256_rnds2_spec_quad32",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
        "int_typing", "lemma_Lib.IntTypes.v_injective",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
        "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.k0",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_Vale.SHA.SHA_helpers.ws_opaque",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "e3500725e849d3e11279158b8251b6ca"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_rnds2_two_steps",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t", "equation_Spec.SHA2.k0",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.add_mod32",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.ws_opaque", "int_inversion",
        "l_and-interp", "lemma_Lib.IntTypes.v_injective",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5494aa3f3c3c4fca99b5c3d124e91c21"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_rnds2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.k", "l_and-interp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "e2deb576212433073b50043a5a697b46"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_rnds2",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.k",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.word_to_nat32", "int_inversion",
        "l_and-interp", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8fa272fbd11b66f1fa37b370a73f60ae",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "9ac414236af54eeeb65823197bf87f52"
    ],
    [
      "Vale.SHA.SHA_helpers.ws_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d5ebce27800130bae02c16de70a95900"
    ],
    [
      "Vale.SHA.SHA_helpers._sigma0_quad32",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.is_sha2",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "46f1652edc1e95da1a526095faab8525"
    ],
    [
      "Vale.SHA.SHA_helpers._sigma1_quad32",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.is_sha2",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d6e2b2123c85dca9191b06725087747a"
    ],
    [
      "Vale.SHA.SHA_helpers.ws_partial_def",
      1,
      0,
      0,
      [
        "@query", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "0756bf8ff14fc870fde6591969e077e0"
    ],
    [
      "Vale.SHA.SHA_helpers.ws_partial_reveal",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "1ea4fd0836ff16b1f5375637f5b676ad"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_wrap_quad32_is_add_mod_quad32",
      1,
      0,
      0,
      [
        "@query", "equation_Vale.Arch.Types.add_wrap_quad32",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.add_mod_quad32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
      ],
      0,
      "738eaec8f234cf585feb6c09b9aec75e"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_msg1",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "8ecbf5f51fdf753a78faaa053820a9af"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_msg1",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2._sigma0", "equation_Spec.SHA2.size_k_w",
        "equation_Vale.Arch.Types.add_wrap_quad32",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers._sigma0_quad32",
        "equation_Vale.SHA.SHA_helpers.add_mod_quad32",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.ws_partial_def",
        "equation_Vale.SHA.SHA_helpers.ws_quad32",
        "equation_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.SHA.SHA_helpers.ws_partial",
        "function_token_typing_Vale.X64.CryptoInstructions_s.sha256_msg1_spec",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.uv_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_Vale.SHA.SHA_helpers.ws_partial_def",
        "token_correspondence_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
        "typing_Spec.SHA2._sigma0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "13d006cbf74b5c4ca9671ad3e46c5f40"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_add_mod_ws_rearrangement",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.add_mod",
        "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "32ba2029ff4a4724a6757a0fddd8d370"
    ],
    [
      "Vale.SHA.SHA_helpers.ws_computed",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.is_sha2",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "31f716c7204d664640b11644150b177c"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_ws_computed_is_ws",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
        "@fuel_irrelevance_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
        "@query", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.add_mod", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.v",
        "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2._sigma1", "equation_Spec.SHA2.block_w",
        "equation_Spec.SHA2.counter", "equation_Spec.SHA2.op_Plus_Dot",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.ws_computed",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "equation_with_fuel_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
        "function_token_typing_Spec.SHA2.Lemmas.ws", "int_inversion",
        "lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.v_injective",
        "lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Spec.SHA2.Lemmas.ws_aux",
        "token_correspondence_Spec.SHA2.op_Plus_Dot",
        "typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2.Lemmas.ws",
        "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "c34cbd551a782205d8177e707c0a4ad9"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_ws_computed_is_ws_opaque",
      1,
      0,
      0,
      [ "@query", "equation_Vale.SHA.SHA_helpers.ws_opaque" ],
      0,
      "c7e76b55fd2c9ba8011577f95665ddca"
    ],
    [
      "Vale.SHA.SHA_helpers.ws_computed_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3e5c61bca107489f496b1a6560516d19",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "703721f89c964e38066e3ff40a09d6c2"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_ws_computed_is_ws_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.ws_computed_quad32",
        "equation_Vale.SHA.SHA_helpers.ws_quad32",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_3e5c61bca107489f496b1a6560516d19",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7812b633ae44323d25421dd434781485"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_ws_computed_quad32",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2._sigma0", "equation_Spec.SHA2._sigma1",
        "equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
        "equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers._sigma0_quad32",
        "equation_Vale.SHA.SHA_helpers._sigma1_quad32",
        "equation_Vale.SHA.SHA_helpers.add_mod_quad32",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.ws_computed",
        "equation_Vale.SHA.SHA_helpers.ws_computed_quad32",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "equation_Vale.SHA.SHA_helpers.ws_quad32",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.IntTypes.v_injective",
        "lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8606f8c053de9c08417ea96222333455",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
        "refinement_interpretation_Tm_refine_d60a0e9fdf52cedb444de54cc40036f8",
        "typing_FStar.UInt32.add_mod", "typing_Lib.IntTypes.add_mod",
        "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2._sigma0",
        "typing_Spec.SHA2._sigma1", "typing_Spec.SHA2.ws",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers._sigma0_quad32",
        "typing_Vale.SHA.SHA_helpers.add_mod_quad32",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_Vale.SHA.SHA_helpers.ws_quad32",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "50eff1e30f0213ba3425a21f39bce723"
    ],
    [
      "Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb"
      ],
      0,
      "43140e5bd23cadca86815634f0277bf7"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_msg1_spec_t_partial",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.ws_partial_def",
        "function_token_typing_Vale.SHA.SHA_helpers.ws_partial",
        "int_inversion", "l_and-interp", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_Vale.SHA.SHA_helpers.ws_partial_def"
      ],
      0,
      "e73358755275cf2bd4baf7ef154791aa"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_msg1_spec_t",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.v",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2._sigma0", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers._sigma0_quad32",
        "equation_Vale.SHA.SHA_helpers.add_mod_quad32",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "equation_Vale.SHA.SHA_helpers.ws_quad32",
        "equation_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.X64.CryptoInstructions_s.sha256_msg1_spec",
        "int_inversion", "l_and-interp", "lemma_Lib.IntTypes.v_injective",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_Vale.X64.CryptoInstructions_s.sha256_msg1_spec_def",
        "typing_Spec.SHA2._sigma0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "c37c8d24f8ee907c02ea3039342de998"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_step2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
        "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2._sigma0", "equation_Spec.SHA2._sigma1",
        "equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
        "equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers._sigma0_quad32",
        "equation_Vale.SHA.SHA_helpers.add_mod_quad32",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.sha256_msg1_spec_t",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.ws_computed",
        "equation_Vale.SHA.SHA_helpers.ws_computed_quad32",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "equation_Vale.SHA.SHA_helpers.ws_quad32",
        "equation_Vale.X64.CryptoInstructions_s.sha256_msg2_spec_def",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.X64.CryptoInstructions_s.sha256_msg2_spec",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_Lib.IntTypes.v_injective",
        "lemma_Vale.SHA.SHA_helpers.add_mod_lemma",
        "primitive_Prims.op_LessThan",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "refinement_interpretation_Tm_refine_f37ee689c16f706f07433a193ce49ccb",
        "token_correspondence_Vale.X64.CryptoInstructions_s.sha256_msg2_spec_def",
        "typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2.Lemmas.ws",
        "typing_Spec.SHA2._sigma0", "typing_Spec.SHA2._sigma1",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.to_uint32",
        "typing_Vale.SHA.SHA_helpers.ws_opaque",
        "typing_Vale.SHA.SHA_helpers.ws_quad32",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "61f2906d90a5da6dc9e43667784de3b9"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_msg2",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "9ac88491120d5c84cf5d4364a8f267cb"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_sha256_msg2",
      2,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.SHA2.size_k_w", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "2742aebd3ac3e63a04fc078816b8cc57"
    ],
    [
      "Vale.SHA.SHA_helpers.k_reqs",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.SHA.SHA_helpers.k",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_07420f653b2652e2852306d7d9338f6d",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "f431711420a40b87f5e085beb135346c"
    ],
    [
      "Vale.SHA.SHA_helpers.quads_to_block",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint32",
        "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Lib.IntTypes.uint32", "int_typing",
        "lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
      ],
      0,
      "46fcf1db8baee5164ed07f0c8aee997f"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_quads_to_block",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_2b5485809f7439c44769748bbc713872"
      ],
      0,
      "a4f975731e9526e2185cd78dc6bc73db"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_quads_to_block",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1606e1a7da0583d7bad9677dcf38161d",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.UInt.max_int", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.sha2_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.SHA2.block_w", "equation_Spec.SHA2.counter",
        "equation_Spec.SHA2.size_k_w", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_select",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.quads_to_block",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "equation_Vale.SHA.SHA_helpers.ws_opaque",
        "equation_Vale.SHA.SHA_helpers.ws_quad32",
        "equation_with_fuel_Spec.SHA2.Lemmas.ws_aux.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Spec.SHA2.Lemmas.ws",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
        "interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
        "interpretation_Tm_abs_d324b025050975942eed8e4180033924",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2b5485809f7439c44769748bbc713872",
        "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a",
        "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_c7fd27793ec1dae0cb682593d434ce63",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_de9bcf2948058d985b33116f51918413",
        "refinement_interpretation_Tm_refine_f403a81b4216eb73ad8a1c1c2f0a1d83",
        "token_correspondence_Spec.SHA2.Lemmas.ws_aux",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_Spec.Hash.Definitions.word_t", "typing_Spec.SHA2.Lemmas.ws",
        "typing_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
        "typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
        "typing_Tm_abs_d324b025050975942eed8e4180033924",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.SHA.SHA_helpers.quads_to_block",
        "typing_Vale.SHA.SHA_helpers.ws_opaque",
        "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "f26d0af0179cedcbfe6bc25684f45564"
    ],
    [
      "Vale.SHA.SHA_helpers.translate_hash_update",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.add_mod",
        "equation_Lib.IntTypes.add_mod", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.op_At_Percent_Dot",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.sec_int_v", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Arch.Types.add_wrap_quad32",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.vv",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_229a5e8eb8bb5562044d0cd62fb30564",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d60a0e9fdf52cedb444de54cc40036f8",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
        "typing_Lib.IntTypes.mk_int",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.SHA.SHA_helpers.nat32_to_word",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "8358469f090d8cc997fbbe0d046aa4bd"
    ],
    [
      "Vale.SHA.SHA_helpers.update_block",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e"
      ],
      0,
      "6f98ec37a02f0d42409e2b99feffcede"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_block_equiv",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.Pervasives.Native.fst", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.Agile.Hash.update",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.extra_state",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.update_pre",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.byte",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.update_block",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Spec.SHA2.update", "int_typing",
        "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_ad4645cb8569689f853f888e7ce500b7",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_Spec.Agile.Hash.update",
        "token_correspondence_Spec.SHA2.update_pre",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "103bd3d6b26b716dc3a28b9d992f5a43"
    ],
    [
      "Vale.SHA.SHA_helpers.update_lemma",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
        "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.UInt.add_mod", "equation_Lib.IntTypes.add_mod",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Spec.SHA2.Lemmas.shuffle_aux",
        "equation_Spec.SHA2.size_k_w",
        "equation_Vale.Arch.Types.add_wrap_quad32",
        "equation_Vale.Def.Types_s.add_wrap",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.shuffle_core_opaque",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.update_block",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_4303d0c89988fe82aadcf16754a5b20f",
        "refinement_interpretation_Tm_refine_516841552c075993547f605f17f21002",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6cccb4299df91104be7587f626369415",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cb97368574c6f45cf8ffde116eb30689",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_edc8fb7e909853d860d4ab445ef31337",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_Lib.IntTypes.add_mod",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt32.add_mod",
        "typing_Spec.Hash.Definitions.word_t", "typing_Spec.Loops.seq_map2",
        "typing_Vale.Def.Types_s.add_wrap",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.SHA.SHA_helpers.make_hash",
        "typing_Vale.SHA.SHA_helpers.update_block",
        "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "5dcf0e13ec983298de907a6ea41c0e7f"
    ],
    [
      "Vale.SHA.SHA_helpers.update_multi_quads",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_0",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_e7547d4e3bc4c2d7d07f503e85b9b717",
        "typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
      ],
      0,
      "28e1a671152f421da49d698745eab195"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_le_bytes_to_seq_quad32_empty",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "eq2-interp", "equation_Prims.eq2", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "d5848e415a87f2db9b44673746d9487f"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_le_bytes_to_seq_quad32_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Prims.eq2", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "aea72ba27711ebc55f15f46f192fbbf5"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_slice_commutes_reverse_bytes_nat32_quad32_seq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq"
      ],
      0,
      "4c66f99c791910909868cc5d8af76f3d"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_quads_unfold",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "@fuel_irrelevance_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "@query", "b2t_def", "equation_Prims.squash",
        "equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "0517047a532fa0b01b0bde0ce04e6ecc"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_quads_short",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption",
        "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "@query",
        "equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "6ad4c495e1286c38ed41f43ec3c49b17"
    ],
    [
      "Vale.SHA.SHA_helpers.update_multi_one",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.Seq.Properties.split",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.size_t", "equation_Lib.Sequence.seq",
        "equation_Prims.eqtype",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.bytes",
        "equation_Spec.Hash.Definitions.bytes_block",
        "equation_Spec.Hash.Definitions.bytes_blocks",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.byte",
        "equation_Vale.SHA.SHA_helpers.bytes",
        "equation_Vale.SHA.SHA_helpers.bytes_blocks",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.size_t", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_Spec.Hash.Lemmas.update_multi_update",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_7540e34d933027d9a3465a151eb57527",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_b08c21a5805b9ea145285da72ddb1ea9",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_FStar.UInt8.t", "typing_Spec.Agile.Hash.update_multi",
        "typing_Spec.Hash.Definitions.block_length",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "9f220991496abe72f90929d2f9a181d8"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_be_to_n_4",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Seq.Properties.last", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.ByteSequence.nat_from_bytes_be",
        "equation_Lib.ByteSequence.nat_from_intseq_be",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.sec_int_v",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Types_s.be_bytes_to_nat32",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_with_fuel_Lib.ByteSequence.nat_from_intseq_be_.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "interpretation_Tm_abs_2bb29967df4c7f51a83f5fb98944d5d2",
        "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_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.vu_inv",
        "lemma_Lib.IntTypes.pow2_3", "lemma_Lib.IntTypes.pow2_4",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_40635fb096fd2f76bb3d32d45a9d3d4a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d3f3b0326a40b22c084e873c3571a01",
        "refinement_interpretation_Tm_refine_6017c6d7f5d6f16aa02c5de0bae953ad",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_83452a5d8515fc994ff43c85b1b18e18",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_FStar.UInt8.uint_to_t",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_FStar.UInt.fits", "typing_FStar.UInt8.v",
        "typing_Lib.ByteSequence.nat_from_intseq_be_",
        "typing_Lib.IntTypes.v", "typing_Lib.Sequence.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "typing_Vale.Def.Words_s.int_to_natN",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "1d5b64efddb76df242487ae75e32b9a2"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_endian_relation",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_ccb4d7c44e4c8e6e26bfd3461142de18",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Tm_unit", "disc_equation_Lib.IntTypes.U1",
        "eq2-interp", "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.ByteSequence.nat_from_bytes_be",
        "equation_Lib.ByteSequence.uint_from_bytes_be",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mk_int",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_of_bytes",
        "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32",
        "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
        "equation_Vale.Def.Types_s.be_bytes_to_nat32",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
        "equation_Vale.Def.Types_s.nat32_to_be_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
        "equation_Vale.Def.Words.Four_s.four_select",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.reverse_seq",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.SHA.SHA_helpers.block_w",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.quads_to_block",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.to_uint32",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32",
        "function_token_typing_Vale.Def.Words.Four_s.nat_to_four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "interpretation_Tm_abs_4f03474956a6a2311e7d7bb19e902da5",
        "interpretation_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
        "interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
        "interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
        "interpretation_Tm_abs_d324b025050975942eed8e4180033924",
        "interpretation_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_164c3a661e54954c7dffc0eba5297a30",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_342c9cca61362b433980438d26ded5b2",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_36761decbc261e6443324da875d9d5c2",
        "refinement_interpretation_Tm_refine_386cc03d241e5f4a0a84f0ca50489700",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_79d1f88e3feaf4f011c530ae4970c006",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_830fcadbd451dad13f5a1d292e9e4412",
        "refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_a4161c172123906d0f0ca043dff400f6",
        "refinement_interpretation_Tm_refine_be21a78039e791db0e843dbd3b1f77f6",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_Lib.ByteSequence.uints_from_bytes_be",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "token_correspondence_Spec.Hash.Definitions.words_of_bytes",
        "token_correspondence_Vale.Arch.Types.reverse_bytes_nat32_quad32",
        "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
        "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index",
        "typing_Lib.Sequence.sub",
        "typing_Spec.Hash.Definitions.word_length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Tm_abs_5baa6a3a8d2445451c959fd307cdcb76",
        "typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
        "typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
        "typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "typing_Vale.SHA.SHA_helpers.quads_to_block",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "fef62da8c2f012c7cb486446aae14b7d"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_mod_transform",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Prims.eqtype",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "d43fc47de2fbdc77d827363e71c82918"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_equiv_vale",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_3",
        "binder_x_6efd6f1848d6dc888dd6a85a4fabc17f_4",
        "binder_x_b5ecdf6b68431b1ae5a51ce9723a824d_5",
        "binder_x_e5783cd4c27820e67b27bc7b42ce4f40_0",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.Seq.Properties.split",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.size_t", "equation_Lib.Sequence.seq",
        "equation_Lib.UpdateMulti.split_block",
        "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.extra_state",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state",
        "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.byte",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.update_multi_opaque",
        "equation_Vale.SHA.SHA_helpers.update_multi_opaque_vale",
        "equation_Vale.SHA.SHA_helpers.word",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_FStar.Seq.Base.index",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.Agile.Hash.update_multi",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32_seq",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_a9e181f2b4db9770dc5da297b02d21b8",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c70800497694fd7a03bdc0b39878a9c4",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_Vale.SHA.SHA_helpers.update_multi_opaque_aux",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Spec.Hash.Definitions.block_length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
        "typing_Vale.SHA.SHA_helpers.update_multi_quads",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "unit_inversion",
        "well-founded-ordering-on-nat"
      ],
      0,
      "0c3dbdb54c98f24c185e7ce22aaa6352"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_quads",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8117376fa751a9089be3b927d5831062",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "95216f1ac86341beb34f1bb845ed158e"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_quads",
      2,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c5f90d486d7e89262afd3a07d65023c5",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "b4875b0dc065948faeda9bebcafc374d"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_quads",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "@fuel_irrelevance_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_0",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
        "binder_x_e5783cd4c27820e67b27bc7b42ce4f40_1",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_with_fuel_Vale.SHA.SHA_helpers.update_multi_quads.fuel_instrumented",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_46ff6445a55ccc12cce752faeb810bb5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c8528cd6408f39eb28756c48c55356a8",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq"
      ],
      0,
      "1868fd68a6e27ddff41cb83803e8f8f9"
    ],
    [
      "Vale.SHA.SHA_helpers.le_bytes_to_hash",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1ce1f604e3636d4aefb8e634e669999e",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
        "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "primitive_Prims.op_disEquality", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_35a56cb7608bf4720ad612ec0cf582b4",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Tm_abs_25aa5013196fbd0a35c92458222d0340",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "6fd5452ffd1f6893a6e24760c36a2618"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_le_bytes_to_hash_quads_part1",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
        "equation_Vale.SHA.SHA_helpers.le_bytes_to_hash",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def"
      ],
      0,
      "3c5929329f81531d6464492a8b3aecb8"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_le_bytes_to_hash_quads",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_1606e1a7da0583d7bad9677dcf38161d",
        "Vale.SHA.SHA_helpers_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
        "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_select",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.le_bytes_to_hash",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Lib.IntTypes.size_t",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
        "interpretation_Tm_abs_d324b025050975942eed8e4180033924",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f403a81b4216eb73ad8a1c1c2f0a1d83",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_Vale.SHA.SHA_helpers.nat32_to_word",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
        "typing_Tm_abs_d324b025050975942eed8e4180033924",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.SHA.SHA_helpers.le_bytes_to_hash"
      ],
      0,
      "d70a93da5cb0532fa476363fa1e721ad"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_hash_to_bytes",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
        "equation_Prims.squash", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "ccf688e2dea56b65e34f359204f6ecb4"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_hash_to_bytes",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC", "eq2-interp",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint32",
        "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.SHA.SHA_helpers.hash256",
        "equation_Vale.SHA.SHA_helpers.le_bytes_to_hash",
        "equation_Vale.SHA.SHA_helpers.nat32_to_word",
        "equation_Vale.SHA.SHA_helpers.word",
        "function_token_typing_Lib.IntTypes.uint32",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_ff221e859aaa7c48bcc66955577d6f8e",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.SHA.SHA_helpers.le_bytes_to_hash"
      ],
      0,
      "8074e7343bae110d3f60d38930a3d237"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_opaque_vale_is_update_multi",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "de76b212b062de91b1ac997b27a81178"
    ],
    [
      "Vale.SHA.SHA_helpers.lemma_update_multi_opaque_vale_is_update_multi",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Prims.squash",
        "equation_Vale.SHA.SHA_helpers.block_length",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256",
        "equation_Vale.SHA.SHA_helpers.update_multi_opaque",
        "equation_Vale.SHA.SHA_helpers.update_multi_opaque_vale",
        "equation_Vale.SHA.SHA_helpers.update_multi_transparent",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.Agile.Hash.update_multi",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "token_correspondence_Vale.SHA.SHA_helpers.update_multi_opaque_aux"
      ],
      0,
      "30bf5684370dc9fcab937e9822cc28a5"
    ]
  ]
]