[
  "�bI�sY�w!\u00041�A�\u0003\r",
  [
    [
      "Spec.Agile.DH.size_key",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Spec.Agile.DH.DH_Curve25519",
        "disc_equation_Spec.Agile.DH.DH_P256",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "fuel_guarded_inversion_Spec.Agile.DH.algorithm",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "34140d2d30749da0c4d0b5d61a28f865"
    ],
    [
      "Spec.Agile.DH.size_public",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Spec.Agile.DH.DH_Curve25519",
        "disc_equation_Spec.Agile.DH.DH_P256",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat",
        "fuel_guarded_inversion_Spec.Agile.DH.algorithm",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "324be0ca08e7b639b78e42272e09ce0c"
    ],
    [
      "Spec.Agile.DH.prime",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Agile.DH.DH_Curve25519",
        "disc_equation_Spec.Agile.DH.DH_P256",
        "fuel_guarded_inversion_Spec.Agile.DH.algorithm"
      ],
      0,
      "1b659837e5e4e644e751fe00356eb487"
    ],
    [
      "Spec.Agile.DH.clamp",
      1,
      2,
      1,
      [ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
      0,
      "9e5767b55be7a85b029c278e5f962d2a"
    ],
    [
      "Spec.Agile.DH.clamp",
      2,
      2,
      1,
      [ "@query", "assumption_Spec.Agile.DH.algorithm__uu___haseq" ],
      0,
      "c3d356db67107ef70edeea10d41f92a7"
    ],
    [
      "Spec.Agile.DH.clamp",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Agile.DH.DH_Curve25519",
        "disc_equation_Spec.Agile.DH.DH_Curve25519",
        "equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
        "equation_Lib.Sequence.lseq", "equation_Spec.Agile.DH.scalar",
        "equation_Spec.Agile.DH.size_key",
        "refinement_interpretation_Tm_refine_348df7b05282e4d51c99c6591007846e",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "535bca074614451a25ffa7eec1826aa0"
    ],
    [
      "Spec.Agile.DH.dh",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Agile.DH.DH_Curve25519",
        "constructor_distinct_Spec.Agile.DH.DH_P256",
        "disc_equation_Spec.Agile.DH.DH_Curve25519",
        "disc_equation_Spec.Agile.DH.DH_P256",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
        "equality_tok_Spec.Agile.DH.DH_P256@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Agile.DH.scalar",
        "equation_Spec.Agile.DH.serialized_point",
        "equation_Spec.Agile.DH.size_key",
        "equation_Spec.Agile.DH.size_public", "equation_Spec.Curve25519.one",
        "equation_Spec.Curve25519.serialized_point",
        "equation_Spec.Curve25519.zero",
        "fuel_guarded_inversion_Spec.Agile.DH.algorithm",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.Agile.DH.size_public", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "b5cd841980d73c20092654e07a505940"
    ],
    [
      "Spec.Agile.DH.secret_to_public",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Agile.DH.DH_Curve25519",
        "constructor_distinct_Spec.Agile.DH.DH_P256",
        "disc_equation_Spec.Agile.DH.DH_Curve25519",
        "disc_equation_Spec.Agile.DH.DH_P256",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
        "equality_tok_Spec.Agile.DH.DH_P256@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "equation_Spec.Agile.DH.scalar", "equation_Spec.Agile.DH.size_key",
        "equation_Spec.Agile.DH.size_public",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Agile.DH.size_key",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "37515e7eb43ee6e25a1861dbc894a0a1"
    ]
  ]
]