[
  "�(�\u001de�����\u0017^7C\nq",
  [
    [
      "Spec.AEAD.uu___2",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "de4d3b4a8ef2d659ca98cb2eaf79ba75"
    ],
    [
      "Spec.AEAD.cipher_alg_of_supported_alg",
      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,
      "4a2e13bbf0dbd05cc0f1934ac739f480"
    ],
    [
      "Spec.AEAD.key_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U8",
        "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",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Pervasives.inversion",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.AEAD.is_supported_alg", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "fuel_guarded_inversion_Spec.AEAD.alg", "inversion-interp",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AEAD.is_supported_alg", "typing_Spec.AES.gf8",
        "typing_Spec.GaloisField.__proj__GF__item__t"
      ],
      0,
      "14ff6885a18e153208535164643c6f4c"
    ],
    [
      "Spec.AEAD.tag_length",
      1,
      0,
      0,
      [
        "@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",
        "equation_FStar.Pervasives.inversion",
        "fuel_guarded_inversion_Spec.AEAD.alg", "inversion-interp"
      ],
      0,
      "ef061b81fbdb5c31b2dedae0aa6f1b2b"
    ],
    [
      "Spec.AEAD.iv_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_FStar.Integers.Signed",
        "constructor_distinct_FStar.Integers.W128",
        "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.W128@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equation_FStar.Integers.width_of_sw",
        "equation_Spec.AEAD.is_supported_alg",
        "equation_Spec.AEAD.supported_alg",
        "projection_inverse_FStar.Integers.Signed__0",
        "refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
        "typing_Spec.AEAD.is_supported_alg"
      ],
      0,
      "370141f6da8bb4d2ab8ee855735beeda"
    ],
    [
      "Spec.AEAD.max_length",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "disc_equation_Spec.AEAD.AES128_GCM",
        "disc_equation_Spec.AEAD.AES256_GCM",
        "disc_equation_Spec.AEAD.CHACHA20_POLY1305", "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",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
        "typing_Prims.pow2", "typing_Spec.AEAD.is_supported_alg"
      ],
      0,
      "cd93909b3dfa5d3117d01a2bd4851e80"
    ],
    [
      "Spec.AEAD.lbytes",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "20f6f6683d0c830a273e99acd00a99a3"
    ],
    [
      "Spec.AEAD.correctness",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "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",
        "refinement_interpretation_Tm_refine_064506d56a6af7ceef8b06aef3cb54e5",
        "refinement_interpretation_Tm_refine_ff4fb9e743a804b2a539fcf5d276f129",
        "typing_Spec.AEAD.encrypt"
      ],
      0,
      "155c84d2d1c0d8b3d3eecb5b50e55eab"
    ]
  ]
]