[
  "�\u001e.3n�D�ъn�5J��",
  [
    [
      "Spec.AEAD.uu___4",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "3477d650968ee975d1fe87f463315dbb"
    ],
    [
      "Spec.AEAD.key_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.AEAD.AES128_CCM",
        "disc_equation_Spec.AEAD.AES128_CCM8",
        "disc_equation_Spec.AEAD.AES128_GCM",
        "disc_equation_Spec.AEAD.AES256_CCM",
        "disc_equation_Spec.AEAD.AES256_CCM8",
        "disc_equation_Spec.AEAD.AES256_GCM",
        "disc_equation_Spec.AEAD.CHACHA20_POLY1305",
        "fuel_guarded_inversion_Spec.AEAD.alg"
      ],
      0,
      "0ffc438ac6e6769af05da585df89c604"
    ],
    [
      "Spec.AEAD.tag_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.AEAD.AES128_CCM",
        "disc_equation_Spec.AEAD.AES128_CCM8",
        "disc_equation_Spec.AEAD.AES128_GCM",
        "disc_equation_Spec.AEAD.AES256_CCM",
        "disc_equation_Spec.AEAD.AES256_CCM8",
        "disc_equation_Spec.AEAD.AES256_GCM",
        "disc_equation_Spec.AEAD.CHACHA20_POLY1305",
        "fuel_guarded_inversion_Spec.AEAD.alg"
      ],
      0,
      "932612b567ac984804db58b716592006"
    ],
    [
      "Spec.AEAD.ekv_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "disc_equation_Spec.AEAD.AES128_GCM",
        "disc_equation_Spec.AEAD.AES256_GCM",
        "disc_equation_Spec.AEAD.CHACHA20_POLY1305",
        "equation_Spec.AEAD.is_supported_alg",
        "equation_Spec.AEAD.supported_alg",
        "refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
        "typing_Spec.AEAD.is_supported_alg"
      ],
      0,
      "11e80a613f5f63b0580be87900de2a94"
    ],
    [
      "Spec.AEAD.max_length",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_FStar.Integers.Signed",
        "constructor_distinct_FStar.Integers.Winfinite",
        "disc_equation_Spec.AEAD.AES128_GCM",
        "disc_equation_Spec.AEAD.AES256_GCM",
        "disc_equation_Spec.AEAD.CHACHA20_POLY1305",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equation_FStar.Integers.int_t", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.AEAD.is_supported_alg",
        "equation_Spec.AEAD.supported_alg", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Prims.pow2", "typing_Spec.AEAD.is_supported_alg"
      ],
      0,
      "aec426ccd03af7c74c3ad5c56f5dd344"
    ],
    [
      "Spec.AEAD.lbytes",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "a493af353400b881034af887f1c181d6"
    ],
    [
      "Spec.AEAD.correctness",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.Unsigned",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_FStar.Integers.int_t", "equation_Spec.AEAD.cipher_length",
        "equation_Spec.AEAD.encrypted", "equation_Spec.AEAD.max_length",
        "equation_Spec.AEAD.plain", "equation_Spec.AEAD.tag_length",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_67a684ae2cdcea98c0a7a1a09bcb3247",
        "refinement_interpretation_Tm_refine_7001d717117afb7669cd45b51ad3dc27",
        "typing_Spec.AEAD.encrypt"
      ],
      0,
      "3597d723165ee335ddc615415e5baa26"
    ]
  ]
]