[
  "�\u001fhʢq�y��[�uM\\\u000f",
  [
    [
      "Vale.Poly1305.Equiv.block_fun",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.Poly1305.size_block",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "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_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "435c0daef1890f3b040471bafd922732"
    ],
    [
      "Vale.Poly1305.Equiv.lemma_poly1305_equiv_rec",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.Poly1305.size_block",
        "primitive_Prims.op_LessThanOrEqual",
        "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_1bac668dddcac6fb0e52f0c9514b035e",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_449625ce4ad52aa2ec0cbe0bec458d86",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "09550c46421893869aab85c5495ea746"
    ],
    [
      "Vale.Poly1305.Equiv.lemma_poly1305_equiv_rec",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Vale.Poly1305.Spec_s.poly1305_hash_blocks.fuel_instrumented",
        "@fuel_irrelevance_Vale.Poly1305.Spec_s.poly1305_hash_blocks.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.Poly1305.Equiv_interpretation_Tm_arrow_750b542a74c0f6cef7bc9c9174882097",
        "Vale.Poly1305.Spec_s_interpretation_Tm_arrow_6c528cb178c0356159679935f3a11594",
        "b2t_def", "binder_x_11f88ae15b1e5de7ff355bd1d7c52426_0",
        "binder_x_2d0bd80df28aa2f2169bec182f0e740d_1",
        "binder_x_2d0bd80df28aa2f2169bec182f0e740d_2",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.encode",
        "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem",
        "equation_Spec.Poly1305.poly1305_update1",
        "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block",
        "equation_Vale.Def.Words_s.nat128", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Poly1305.Equiv.block_fun",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "equation_with_fuel_Vale.Poly1305.Spec_s.poly1305_hash_blocks.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.AES.elem",
        "function_token_typing_Vale.Poly1305.Equiv.block_fun",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "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_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_1bac668dddcac6fb0e52f0c9514b035e",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_2df60152c11f8fa3e12a9a666c0e23b7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "token_correspondence_Spec.Poly1305.poly1305_update1",
        "typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Vale.Poly1305.Equiv.block_fun",
        "well-founded-ordering-on-nat"
      ],
      0,
      "0a470b0eec34085852736d78aac9af6f"
    ],
    [
      "Vale.Poly1305.Equiv.lemma_poly1305_equiv_last",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd",
        "equation_Spec.Poly1305.felem",
        "equation_Spec.Poly1305.poly1305_update1",
        "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block",
        "equation_Vale.Poly1305.Equiv.block_fun",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "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_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_3fd10d79e1f4b0d8069ab6e203bd2713",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Lib.Sequence.length", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Poly1305.size_block"
      ],
      0,
      "e6ee5dfb0ce500eadc0ff6b2e00bd77d"
    ],
    [
      "Vale.Poly1305.Equiv.lemma_poly1305_equiv_r",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "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.logand_v",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.Poly1305.key", "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key", "equation_Spec.Poly1305.to_felem",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Poly1305.Math.lowerUpper128_def",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Spec.AES.elem",
        "function_token_typing_Vale.Poly1305.Math.lowerUpper128",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "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_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_153bfbd15dbb4a9c413275083059c752",
        "refinement_interpretation_Tm_refine_2897f455bd1a2e7bd7f8f1aa6ce63472",
        "refinement_interpretation_Tm_refine_3e9d04c89ab3a202cd1b97a76ce93dbd",
        "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_Vale.Poly1305.Math.lowerUpper128_def",
        "typing_FStar.UInt.fits",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
        "typing_Lib.Sequence.length", "typing_Prims.pow2",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Poly1305.size_block", "typing_Vale.Def.Types_s.iand",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b1ab9efa896868b8262761db87c35ff9"
    ],
    [
      "Vale.Poly1305.Equiv.lemma_poly1305_equiv",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "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.Poly1305.key",
        "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_LessThanOrEqual",
        "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_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "2f468604069243eba0b018fc4732d9ba"
    ],
    [
      "Vale.Poly1305.Equiv.lemma_poly1305_equiv",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.slice",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.fmul",
        "equation_Spec.Poly1305.from_felem", "equation_Spec.Poly1305.key",
        "equation_Spec.Poly1305.poly1305_finish",
        "equation_Spec.Poly1305.poly1305_init",
        "equation_Spec.Poly1305.poly1305_mac",
        "equation_Spec.Poly1305.poly1305_update",
        "equation_Spec.Poly1305.poly1305_update1",
        "equation_Spec.Poly1305.poly1305_update_last",
        "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block",
        "equation_Spec.Poly1305.size_key", "equation_Spec.Poly1305.to_felem",
        "equation_Spec.Poly1305.zero",
        "equation_Vale.Poly1305.Spec_s.make_r",
        "equation_Vale.Poly1305.Spec_s.poly1305_hash",
        "equation_Vale.Poly1305.Spec_s.poly1305_hash_all",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Spec.AES.elem",
        "function_token_typing_Vale.Poly1305.Equiv.block_fun",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Lib.IntTypes.pow2_127", "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_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_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
        "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
        "refinement_interpretation_Tm_refine_1bac668dddcac6fb0e52f0c9514b035e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_63efca340ea10f520d98d30b7bd6d230",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_7f16c7b57ef8bef37e694fdc293f58a5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
        "refinement_interpretation_Tm_refine_f1f3a6a6d3da045b35e7ba130c8b362a",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.nat_from_bytes_le",
        "typing_Lib.ByteSequence.nat_to_bytes_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
        "typing_Lib.Sequence.length", "typing_Lib.Sequence.slice",
        "typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "923a5db0d38409a1e4aab09e4133b709"
    ]
  ]
]