[
  "<≤T%»|˜¶ý±\u001b\u0004ôÖýê",
  [
    [
      "Crypto.AEAD.Main.iv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_Crypto.AEAD.Main.ivlen", "typing_FStar.UInt32.v"
      ],
      0,
      "df1f099d4a0d34398e0097478b97eddf"
    ],
    [
      "Crypto.AEAD.Main.aadmax",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "642d9da2554c725d6a820dc44dd64cd3"
    ],
    [
      "Crypto.AEAD.Main.cipher",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Crypto.AEAD.Main.taglen", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_Prims.nat",
        "function_token_typing_Crypto.AEAD.Main.taglen",
        "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_Addition",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.UInt32.v"
      ],
      0,
      "48559d8e54184283841781dc0c2b02d2"
    ],
    [
      "Crypto.AEAD.Main.entry_injective",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Crypto.AEAD.Main.bytes",
        "equation_Crypto.AEAD.Main.cipher",
        "equation_Crypto.AEAD.Main.lbytes", "equation_FStar.UInt32.n",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_9aee3aac1eb9d8609150582ee17d75c8",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Bytes.reveal", "typing_FStar.Seq.Base.length"
      ],
      0,
      "fa50c65629cf7c14698c138c9b8cefa0"
    ],
    [
      "Crypto.AEAD.Main.ok_plain_len_32",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "504c3a1b4cec6474ae95871b9e0ac9ca"
    ],
    [
      "Crypto.AEAD.Main.as_set",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_0a56e3de562c08d8ab59f4ac6f626a98_2",
        "disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
        "fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
      ],
      0,
      "b5bde3e074cc0371c8aeceedcf089b79"
    ],
    [
      "Crypto.AEAD.Main.coerce",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_Crypto.AEAD.Main.keylen", "typing_FStar.UInt32.v"
      ],
      0,
      "391f5c73bb683cb659322d49033f11be"
    ],
    [
      "Crypto.AEAD.Main.leak",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.n", "int_inversion",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_Crypto.AEAD.Main.statelen", "typing_FStar.UInt32.v"
      ],
      0,
      "8c2d4ebce787064bded65a2b407d9e87"
    ],
    [
      "Crypto.AEAD.Main.entry_of",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Crypto.AEAD.Main.aadlen_32",
        "equation_Crypto.AEAD.Main.aadmax",
        "equation_Crypto.AEAD.Main.lbuffer",
        "equation_Crypto.AEAD.Main.ok_plain_len_32",
        "equation_Crypto.AEAD.Main.taglen", "equation_Crypto.Plain.as_bytes",
        "equation_Crypto.Plain.plainLen", "equation_Crypto.Plain.sel_plain",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.length",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.lte", "equation_FStar.UInt32.n",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_Crypto.AEAD.Main.taglen",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t", "int_inversion",
        "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Bytes.reveal_hide",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_21fa21200df20774cb0091062ddbefd3",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Bytes_Tm_refine_55a09564bd638637b3e90a918ab57130",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Crypto.Plain.as_bytes",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.UInt32.v"
      ],
      0,
      "a76a88d601f4e8ca36f870ba3e9a855f"
    ],
    [
      "Crypto.AEAD.Main.entry_of",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Crypto.AEAD.Main.aadlen_32",
        "equation_Crypto.AEAD.Main.aadmax",
        "equation_Crypto.AEAD.Main.lbuffer",
        "equation_Crypto.AEAD.Main.ok_plain_len_32",
        "equation_Crypto.Plain.as_bytes", "equation_Crypto.Plain.plainLen",
        "equation_Crypto.Plain.sel_plain",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.length",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lte",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.lte", "equation_FStar.UInt32.n",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t", "int_inversion",
        "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Bytes.reveal_hide",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_21fa21200df20774cb0091062ddbefd3",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Bytes_Tm_refine_55a09564bd638637b3e90a918ab57130",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Crypto.Plain.as_bytes",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.UInt32.v"
      ],
      0,
      "aef4189ff6d95e1a94ca6022566a2ff8"
    ],
    [
      "Crypto.AEAD.Main.entry_for_nonce",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Crypto.AEAD.Main.iv",
        "equation_Crypto.AEAD.Main.nonce",
        "equation_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt128.t",
        "haseqCrypto.AEAD.Main_Tm_refine_4a4d35a7ce2fc546c6d8d77b0ced3602",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_f8f93931baf7de624bdfd6a4521b10d1",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "ab68f1557873af6517e56855fecc3826"
    ],
    [
      "Crypto.AEAD.Main.encrypt",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Crypto.AEAD.Main.aadlen_32",
        "equation_Crypto.AEAD.Main.aadmax",
        "equation_Crypto.AEAD.Main.ok_plain_len_32",
        "equation_Crypto.AEAD.Main.taglen", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_Crypto.AEAD.Main.taglen",
        "function_token_typing_FStar.UInt32.n", "int_inversion",
        "lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_21fa21200df20774cb0091062ddbefd3",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "8aa70fdbac9a5187db7a1aa58bee132d"
    ],
    [
      "Crypto.AEAD.Main.decrypt",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Crypto.AEAD.Main.aadlen_32",
        "equation_Crypto.AEAD.Main.aadmax",
        "equation_Crypto.AEAD.Main.ok_plain_len_32",
        "equation_Crypto.AEAD.Main.safeId",
        "equation_Crypto.AEAD.Main.taglen", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Flag.safeId",
        "function_token_typing_Crypto.AEAD.Main.taglen",
        "function_token_typing_FStar.UInt32.n", "int_inversion",
        "lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_21fa21200df20774cb0091062ddbefd3",
        "refinement_interpretation_Crypto.AEAD.Main_Tm_refine_e295d1a089abf8fd7758b0cf33f12cde",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "88b7d5b6db5876f13f94d079f4f20270"
    ]
  ]
]