[
  "S]\u0011y¼–ž2…ŸÛ¹{HAV",
  [
    [
      "Hacl.SHA2.Vec256.sha224_update8",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "2c19afd9ecf10d717f236185a7c3919e"
    ],
    [
      "Hacl.SHA2.Vec256.sha224_update8",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "3ae7b2af970caf4e4573efec8a3d4eb8"
    ],
    [
      "Hacl.SHA2.Vec256.sha224_update8",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "2129d24cc620c67b9d3825e54d71bba0"
    ],
    [
      "Hacl.SHA2.Vec256.sha224_8",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.maxint", "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_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.bytes",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_a7fddc095f2b8d97b9171ed3eca5bb0e",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.Agile.Hash.hash",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.Buffer.MUT@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_224@tok"
      ],
      0,
      "07ed3e368d0fd8347bc97a6635f05987"
    ],
    [
      "Hacl.SHA2.Vec256.sha224_8",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "b2t_def", "bool_inversion",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Hash.Definitions.hash_len",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.MultiBuffer.as_seq_multi",
        "equation_Lib.MultiBuffer.internally_disjoint",
        "equation_Lib.MultiBuffer.internally_disjoint8",
        "equation_Lib.MultiBuffer.live8",
        "equation_Lib.MultiBuffer.live_multi",
        "equation_Lib.MultiBuffer.modifies_multi",
        "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.Buffer.as_seq",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.MultiBuffer.as_seq_multi_lemma",
        "lemma_Lib.NTuple.ntup8_lemma",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "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_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_1821bb125f421b67809195ad37eb533a",
        "refinement_interpretation_Tm_refine_20436933fe7a8b4fffe6120ab1cc514f",
        "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_a7fddc095f2b8d97b9171ed3eca5bb0e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
        "typing_Hacl.Hash.Definitions.hash_len",
        "typing_Lib.Buffer.lbuffer_t", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint",
        "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.AES.irred",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Hash.Definitions.hash_word_length",
        "typing_Spec.Hash.Definitions.word_length",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U8@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_224@tok"
      ],
      0,
      "99fa03cd7eaa22a54e68f2ead8fa562a"
    ],
    [
      "Hacl.SHA2.Vec256.sha256_update8",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "3af169ef167b572e074753d1a5cd3f4c"
    ],
    [
      "Hacl.SHA2.Vec256.sha256_update8",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "621dea980abc107a9d85a3ac4e31ad47"
    ],
    [
      "Hacl.SHA2.Vec256.sha256_update8",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M128",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "cbd06327d048522ed46524379744b533"
    ],
    [
      "Hacl.SHA2.Vec256.sha256_8",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "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.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.maxint", "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_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.bytes",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Spec.AES.elem", "int_inversion",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ab2d15b4c5486f56c5e7ed32a067391e",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.Agile.Hash.hash",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Hash.Definitions.hash_length",
        "typing_tok_Lib.Buffer.MUT@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "d7d52cb78f2a7b2a698f77c8c37b0a5e"
    ],
    [
      "Hacl.SHA2.Vec256.sha256_8",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Hacl.Hash.Definitions.hash_len",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.MultiBuffer.as_seq_multi",
        "equation_Lib.MultiBuffer.internally_disjoint",
        "equation_Lib.MultiBuffer.internally_disjoint8",
        "equation_Lib.MultiBuffer.live8",
        "equation_Lib.MultiBuffer.live_multi",
        "equation_Lib.MultiBuffer.modifies_multi",
        "equation_Lib.NTuple.ntup8", "equation_Lib.NTuple.ntuple",
        "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.Buffer.as_seq",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.MultiBuffer.as_seq_multi_lemma",
        "lemma_Lib.NTuple.ntup8_lemma",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "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.Mktuple2__b",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_1821bb125f421b67809195ad37eb533a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ab2d15b4c5486f56c5e7ed32a067391e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_e5df16edfaa19fd72c2c2a000fed3ea9",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_Hacl.Hash.Definitions.hash_len",
        "typing_Lib.Buffer.lbuffer_t", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint",
        "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Hash.Definitions.word_length",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "df489202ef4784509fb7d3d8fc369fd7"
    ],
    [
      "Hacl.SHA2.Vec256.sha384_update4",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "859cdead26ca44cc0864acf754970b1e"
    ],
    [
      "Hacl.SHA2.Vec256.sha384_update4",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M128",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "2c6d7961ec2ada59f2e17b93f7d009dc"
    ],
    [
      "Hacl.SHA2.Vec256.sha384_update4",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M128",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "b0847d816cdfd61870fe41c0cb436e82"
    ],
    [
      "Hacl.SHA2.Vec256.sha384_4",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.maxint", "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_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.bytes",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_717d8302485f4332a8b3020e05fe237f",
        "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.Agile.Hash.hash",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.Buffer.MUT@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_384@tok"
      ],
      0,
      "3269ef7f8dc6f48c879f7412ddcef51c"
    ],
    [
      "Hacl.SHA2.Vec256.sha384_4",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "bool_inversion", "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Hacl.Hash.Definitions.hash_len",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
        "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.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.MultiBuffer.internally_disjoint",
        "equation_Lib.MultiBuffer.internally_disjoint4",
        "equation_Lib.MultiBuffer.live4",
        "equation_Lib.MultiBuffer.live_multi",
        "equation_Lib.MultiBuffer.modifies_multi",
        "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.MultiBuffer.as_seq_multi_lemma",
        "lemma_Lib.NTuple.ntup4_lemma",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_union_comm",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_1821bb125f421b67809195ad37eb533a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_717d8302485f4332a8b3020e05fe237f",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9c4071d199825dbbe7ffb5ac03ad5d31",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_Hacl.Hash.Definitions.hash_len",
        "typing_Lib.Buffer.lbuffer_t", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
        "typing_Lib.Buffer.union", "typing_Lib.IntTypes.minint",
        "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_384@tok"
      ],
      0,
      "9db01f13de3520df84adbc4bd36a55c4"
    ],
    [
      "Hacl.SHA2.Vec256.sha512_update4",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "8b7faf540310ecc73ec58cbfc73f4157"
    ],
    [
      "Hacl.SHA2.Vec256.sha512_update4",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "42e7a589fcf39555010512cb80c6ede0"
    ],
    [
      "Hacl.SHA2.Vec256.sha512_update4",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M128",
        "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_sha2",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok"
      ],
      0,
      "40a20a880ef7ccde035ae7f8ffe1be8e"
    ],
    [
      "Hacl.SHA2.Vec256.sha512_4",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.maxint", "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_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.bytes",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_8479239213cbc2fbdf621581bf1c49e7",
        "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.Agile.Hash.hash",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.Buffer.MUT@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_512@tok"
      ],
      0,
      "60fed616520c2aef83c0b1b51fd6e5bb"
    ],
    [
      "Hacl.SHA2.Vec256.sha512_4",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Hacl.Spec.SHA2.Vec_pretyping_ef9d7cf021ba37864f0e1ecf8fb737f1",
        "bool_inversion", "constructor_distinct_Hacl.Spec.SHA2.Vec.M256",
        "constructor_distinct_Lib.Buffer.CONST",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M256@tok",
        "equality_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Hacl.Hash.Definitions.hash_len",
        "equation_Hacl.Spec.SHA2.Vec.is_supported",
        "equation_Hacl.Spec.SHA2.Vec.lanes", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
        "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.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.MultiBuffer.internally_disjoint",
        "equation_Lib.MultiBuffer.internally_disjoint4",
        "equation_Lib.MultiBuffer.live4",
        "equation_Lib.MultiBuffer.live_multi",
        "equation_Lib.MultiBuffer.modifies_multi",
        "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.is_sha2",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv",
        "lemma_Lib.MultiBuffer.as_seq_multi_lemma",
        "lemma_Lib.NTuple.ntup4_lemma",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_union_comm",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_1821bb125f421b67809195ad37eb533a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_62bc5deb42438405dbafd05199efbc58",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_8479239213cbc2fbdf621581bf1c49e7",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_Hacl.Hash.Definitions.hash_len",
        "typing_Lib.Buffer.lbuffer_t", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
        "typing_Lib.Buffer.union", "typing_Lib.IntTypes.minint",
        "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Hacl.Spec.SHA2.Vec.M32@tok",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok",
        "typing_tok_Spec.Hash.Definitions.SHA2_512@tok"
      ],
      0,
      "e36f3cb04f2e8c946e1906779d6cc468"
    ]
  ]
]