[
  "\u0010×`\u00173á›i‰ýSÁ+÷rJ",
  [
    [
      "Spec.ECDSA.lemma_scalar_ith",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "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_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "8c2780ae4da447baa17424e632c2181f"
    ],
    [
      "Spec.ECDSA.lemma_scalar_ith",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "168f4696db7c1378b61077feade7328a"
    ],
    [
      "Spec.ECDSA.lemma_scalar_ith",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_14e58bf2ebe4b8342ba0b27074cab16f",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_bb84afa4849f0438d8727a4675761e52",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length",
        "typing_Lib.ByteSequence.nat_from_intseq_le",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
        "typing_Lib.Sequence.index", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "7f8b1af7b764a95dc3e26fba11d3dfa8"
    ],
    [
      "Spec.ECDSA.lemma_euclidian_for_ithbit",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "66136002555adbb757c857ffca7d6bea"
    ],
    [
      "Spec.ECDSA.lemma_euclidian_for_ithbit",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "89caa17cab84c6e91975642acbae8ea9"
    ],
    [
      "Spec.ECDSA.ith_bit",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f0b868cdf4c2fb862e834be496d469b7"
    ],
    [
      "Spec.ECDSA.ith_bit",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "6e83849e5290086dee6559087f6ff762"
    ],
    [
      "Spec.ECDSA.ith_bit",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.op_At_Percent_Dot",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
        "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", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.shift_right_lemma",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_27dc038cce58e6a175dcb6195f80808a",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
        "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
        "refinement_interpretation_Tm_refine_756fcf1fd8e14d13d6d06129e86ad1d3",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_8505facf9381abcc9efff183e73f44b0",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.op_At_Percent_Dot",
        "typing_Lib.IntTypes.v", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "650b5527f0121526f7a90262acae2d21"
    ],
    [
      "Spec.ECDSA.op_Star_Percent",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "a3967433ab36ca0c37ccf6441d0fff99"
    ],
    [
      "Spec.ECDSA._exp_step0",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSA.op_Star_Percent", "equation_Spec.ECDSA.prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4c3b134a8f0bde9ce770094d08b60f84",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "cca755e05dac160124b4a98279e65fcd"
    ],
    [
      "Spec.ECDSA._exp_step1",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSA.op_Star_Percent", "equation_Spec.ECDSA.prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "int_inversion", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4c3b134a8f0bde9ce770094d08b60f84",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "e6783983c034b4aee32de73ce33a02a6"
    ],
    [
      "Spec.ECDSA.lemma_swaped_steps",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.ECDSA._exp_step0", "equation_Spec.ECDSA._exp_step1",
        "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSA.op_Star_Percent", "equation_Spec.ECDSA.swap",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_4c3b134a8f0bde9ce770094d08b60f84",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "e3a40fc5015b8817858356c00fb3ee38"
    ],
    [
      "Spec.ECDSA._exp_step",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "46e9b50dc8bd53d30294167df0a0f283"
    ],
    [
      "Spec.ECDSA._exp_step",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "3fd3a711faa93d9ddf84356edc4b034c"
    ],
    [
      "Spec.ECDSA._exp_step",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_inversion",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "19d3aab0e35fb05017673ccacf689356"
    ],
    [
      "Spec.ECDSA._exponent_spec",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "8e32aa56ebcd18f275ea256ebdea321a"
    ],
    [
      "Spec.ECDSA._exponent_spec",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "c0698ab373849afed744669676d3f353"
    ],
    [
      "Spec.ECDSA.lemma_even",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cf1b97833340cf7687e7b411efdb7198",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e359d069f709954f6ea0b59d1c2db6f8",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "bb8910b64996a3fb56ebe39fbe972ff2"
    ],
    [
      "Spec.ECDSA.lemma_even",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "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_cf1b97833340cf7687e7b411efdb7198",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a2233355afef4acb4efc7c7b4fb6dddb"
    ],
    [
      "Spec.ECDSA.lemma_even",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_FStar.Math.Lib.div",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.ECDSA.ith_bit", "int_inversion",
        "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b69e90b97d8991e731f0f059afb1344",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_86bac8d7b801765697c794e57f270ab8",
        "refinement_interpretation_Tm_refine_cf1b97833340cf7687e7b411efdb7198",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_e359d069f709954f6ea0b59d1c2db6f8",
        "typing_Spec.ECDSA.ith_bit"
      ],
      0,
      "953665d39f005d4364d246e101aad6be"
    ],
    [
      "Spec.ECDSA.lemma_odd",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_32ab291d88b0f6b5cb5f78e7fc27a2b6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cf1b97833340cf7687e7b411efdb7198",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "3ea3673fa62a7824c9005ec5eeca6ad2"
    ],
    [
      "Spec.ECDSA.lemma_odd",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_cf1b97833340cf7687e7b411efdb7198",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f50e78d84008c870246869ad0aabf60f"
    ],
    [
      "Spec.ECDSA.lemma_odd",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_FStar.Math.Lib.div",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.ECDSA.ith_bit", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_32ab291d88b0f6b5cb5f78e7fc27a2b6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b69e90b97d8991e731f0f059afb1344",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_86bac8d7b801765697c794e57f270ab8",
        "refinement_interpretation_Tm_refine_cf1b97833340cf7687e7b411efdb7198",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Spec.ECDSA.ith_bit"
      ],
      0,
      "39efd9fee9cd2cf499919816681a456e"
    ],
    [
      "Spec.ECDSA.lemma_exponen_spec",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_20243dce370bae2ae7be17fef94a36a1",
        "refinement_interpretation_Tm_refine_2a75ac9e9041407930877285ccf479d9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b69e90b97d8991e731f0f059afb1344",
        "refinement_interpretation_Tm_refine_d131d4ef716432e3a8862dae7df47aab",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Math.Lib.div", "typing_Lib.IntTypes.bits",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "2438c51c20ea23da8155f81987b1bb1e"
    ],
    [
      "Spec.ECDSA.lemma_exponen_spec_0",
      1,
      1,
      0,
      [
        "@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",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_20243dce370bae2ae7be17fef94a36a1",
        "refinement_interpretation_Tm_refine_2a75ac9e9041407930877285ccf479d9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b69e90b97d8991e731f0f059afb1344",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Math.Lib.div", "typing_Lib.IntTypes.bits",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "34c4eae8226191e836b009cc5d9e917f"
    ],
    [
      "Spec.ECDSA.lemma_exponen_spec_0",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "cb862a580dec7d82f99c40138539e4d7"
    ],
    [
      "Spec.ECDSA.lemma_exponen_spec_0",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
        "@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_FStar.Math.Lib.div", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSA.prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "equation_with_fuel_Spec.P256.Lemmas.pow.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_20243dce370bae2ae7be17fef94a36a1",
        "refinement_interpretation_Tm_refine_2a75ac9e9041407930877285ccf479d9",
        "refinement_interpretation_Tm_refine_4c3b134a8f0bde9ce770094d08b60f84",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b69e90b97d8991e731f0f059afb1344",
        "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Math.Lib.div", "typing_Prims.pow2",
        "typing_Spec.ECDSA.prime", "typing_Spec.P256.Lemmas.pow"
      ],
      0,
      "fc8d7c44f7a127233dea2eaf1badb8c0"
    ],
    [
      "Spec.ECDSA.lemma_exponen_spec",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_20243dce370bae2ae7be17fef94a36a1",
        "refinement_interpretation_Tm_refine_24708fa37a4bec7ea20abaf0c93d67cc",
        "refinement_interpretation_Tm_refine_2a75ac9e9041407930877285ccf479d9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b69e90b97d8991e731f0f059afb1344",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Math.Lib.div", "typing_Lib.IntTypes.bits",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "3851aa9cdbb08ad91d1917a4422873fb"
    ],
    [
      "Spec.ECDSA.lemma_exponen_spec",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_04c65e5061064a6641b678085a12f5eb_0",
        "binder_x_1efb0e89ea25f58465eaf8e8ea325655_2",
        "binder_x_d89c10393b27a21bd3a1e94de59df219_1",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Spec.ECDSA._exp_step", "equation_Spec.ECDSA._exp_step0",
        "equation_Spec.ECDSA._exp_step1", "equation_Spec.ECDSA.ith_bit",
        "equation_Spec.ECDSA.nat_prime",
        "equation_Spec.ECDSA.op_Star_Percent", "equation_Spec.ECDSA.prime",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_20243dce370bae2ae7be17fef94a36a1",
        "refinement_interpretation_Tm_refine_2a75ac9e9041407930877285ccf479d9",
        "refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_86bac8d7b801765697c794e57f270ab8",
        "refinement_interpretation_Tm_refine_9f8f6290ae5c5057ec2ec3d3fc190a93",
        "refinement_interpretation_Tm_refine_ab3a3d81ac8671ea932e607c31c24256",
        "refinement_interpretation_Tm_refine_d131d4ef716432e3a8862dae7df47aab",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f69cd9e64c7c87b398cfced2167229ae",
        "typing_FStar.Math.Lib.div", "typing_Lib.RawIntTypes.uint_to_nat",
        "typing_Prims.pow2", "typing_Spec.ECDSA.ith_bit",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "unit_inversion", "unit_typing", "well-founded-ordering-on-nat"
      ],
      0,
      "6af5fd8ad00a05ce1b3e736f76990b48"
    ],
    [
      "Spec.ECDSA.prime_p256_order_inverse_list",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "52570dcad07412172173b937ce707071"
    ],
    [
      "Spec.ECDSA.prime_p256_order_inverse_seq",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "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.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint",
        "typing_Lib.IntTypes.mk_int", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "cc0defa6eb1fb8415b4a49fc28fb5d43"
    ],
    [
      "Spec.ECDSA.prime_p256_order_list",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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.U8@tok"
      ],
      0,
      "bcc32cf9fc92d2f9218c66b93ea49155"
    ],
    [
      "Spec.ECDSA.prime_p256_order_seq",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "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.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "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_Prims.nat",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "9b0af56e0d5ee75ab0c22a691f03b4bd"
    ],
    [
      "Spec.ECDSA.exponent_spec",
      1,
      0,
      0,
      [
        "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "f904d410a3e7c67c16bd67a7cf9b4361"
    ],
    [
      "Spec.ECDSA.exponent_spec",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equation_FStar.Math.Lib.arithmetic_shift_right",
        "equation_FStar.Math.Lib.div",
        "equation_Lib.ByteSequence.nat_from_bytes_le",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.ECDSA._exponent_spec",
        "equation_Spec.ECDSA.nat_prime", "equation_Spec.ECDSA.prime",
        "equation_Spec.ECDSA.prime_p256_order_inverse_seq",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_2a75ac9e9041407930877285ccf479d9",
        "refinement_interpretation_Tm_refine_4c3b134a8f0bde9ce770094d08b60f84",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff90cbee741451094b79a20a5df503e5",
        "typing_FStar.Math.Lib.div", "typing_Prims.pow2",
        "typing_Spec.ECDSA.prime_p256_order_inverse_seq"
      ],
      0,
      "ccf4773c279ee4bfba18205dade3967f"
    ],
    [
      "Spec.ECDSA.changeEndian",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.ECDSAP256.Definition.felem_seq",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1e8eeffca924aa802eb298c60f0cfec",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_fa0479a5b790ae1b826feadf76d92d8e",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "d2d6d6d5d06c1710a70fe89b2c6a12b4"
    ],
    [
      "Spec.ECDSA.changeEndianLemma",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f9554dbee460d20b87768151f2fd9c07"
    ],
    [
      "Spec.ECDSA.changeEndianLemma",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "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,
      "e681b4eb09cd24996718b55e54fdb5bd"
    ],
    [
      "Spec.ECDSA.changeEndianLemma",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "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.ECDSA.changeEndian",
        "equation_Spec.P256.Definitions.felem_seq",
        "function_token_typing_Lib.IntTypes.uint64", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.Seq.Properties.slice_upd",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c9433aa247ca429fb93e0c284f98bfd",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_1e848ed9fc65de08c8bb8e2d0978738b",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_2c9a56acd398d01dc8e638fdcc712147",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_3c2b792145025db72c2db5c70268f5ac",
        "refinement_interpretation_Tm_refine_4f7b2020df058a9a740dfa2e147d32f8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_782420a2054fd965084564ef5ff53609",
        "refinement_interpretation_Tm_refine_7dc8e0d08618e3f9f72ae91cd1eded34",
        "refinement_interpretation_Tm_refine_85d976c88c35a3ad167ae3cf88c621ee",
        "refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
        "refinement_interpretation_Tm_refine_9b9b3140dac3eb0c26eb2bf380066c73",
        "refinement_interpretation_Tm_refine_9e7b7ec534a2a9a23ec52880cc32ece2",
        "refinement_interpretation_Tm_refine_a940d9ade205d65bb2a60b48e0817bff",
        "refinement_interpretation_Tm_refine_d12216928f2bb188757799ee2d87a878",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_da88653d361d2d2ebe31bf0627352566",
        "refinement_interpretation_Tm_refine_e5bdc61d271036420dddec78a6a271d5",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.Sequence.index", "typing_Lib.Sequence.slice",
        "typing_Lib.Sequence.to_seq", "typing_Lib.Sequence.upd",
        "typing_Spec.ECDSA.changeEndian", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "a089f7a8bb19892a719297b1eb2f169c"
    ],
    [
      "Spec.ECDSA.changeEndianLemmaI",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f9afb8e1fe29a73ea03f3322cb227eb5"
      ],
      0,
      "eb41816ca969c60c8cecde9b332dea35"
    ],
    [
      "Spec.ECDSA.changeEndianLemmaI",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.min_int",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Spec.ECDSA.changeEndian",
        "equation_Spec.P256.Definitions.felem_seq",
        "function_token_typing_Lib.IntTypes.uint64", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_177932ae27bb622da89916ff70731255",
        "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626",
        "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_450c5fab5899e44e63db869bd0c9eec0",
        "refinement_interpretation_Tm_refine_4eccd30c84686fcefe0c76dd60d3c3b8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
        "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
        "refinement_interpretation_Tm_refine_be9f3762ef829e4292fadae5bee9b36d",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_df8882fb83fe7a4d84f35dfcf46555d7",
        "refinement_interpretation_Tm_refine_e501edd7240f5ad652d8ca337aeb8bfa",
        "refinement_interpretation_Tm_refine_f9afb8e1fe29a73ea03f3322cb227eb5",
        "refinement_interpretation_Tm_refine_fbb325fb706a850f59e1f0467ff334d8",
        "typing_Lib.ByteSequence.nat_to_intseq_be",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index",
        "typing_Lib.Sequence.upd", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "c430c9a5e37a412b42004fdba0b406b6"
    ],
    [
      "Spec.ECDSA.changeEndian_le_be",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "36c569a9c20f738ebc198b6998f3bdc2"
    ],
    [
      "Spec.ECDSA.changeEndian_le_be",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_be9f3762ef829e4292fadae5bee9b36d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "1782d69884b1f316797dbacbbbae55a1"
    ],
    [
      "Spec.ECDSA.verifyQValidCurvePointSpec",
      1,
      0,
      0,
      [
        "@query", "equation_Prims.nat", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3"
      ],
      0,
      "8bdd3d9a3e653a6dd71095b5fe65b70a"
    ],
    [
      "Spec.ECDSA.hash_alg_ecdsa",
      1,
      0,
      0,
      [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
      0,
      "766a7600c60d697e205e607bdda513df"
    ],
    [
      "Spec.ECDSA.__proj__Hash__item___0",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Spec.ECDSA.Hash",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_c7a73210445bd39cd87a9cd5a7b972aa"
      ],
      0,
      "e32f632f63bde7eba93f65fade7afd11"
    ],
    [
      "Spec.ECDSA.min_input_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "disc_equation_Spec.ECDSA.Hash",
        "disc_equation_Spec.ECDSA.NoHash",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa",
        "inversion-interp", "lemma_Spec.ECDSA.invert_state_s"
      ],
      0,
      "037cec94cf1fa3ded4a966e34db519ac"
    ],
    [
      "Spec.ECDSA.hashSpec",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.ECDSA.Hash",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.ECDSA.min_input_length",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa",
        "inversion-interp", "lemma_FStar.UInt.pow2_values",
        "lemma_Spec.ECDSA.invert_state_s", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.ECDSA.Hash__0",
        "refinement_interpretation_Tm_refine_2420de9f68a4c2a48b6f2796a459baf9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "8738c8375cafbb1bdc856cb12d6d1c5b"
    ],
    [
      "Spec.ECDSA.hashSpec",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.ECDSA.Hash",
        "constructor_distinct_Spec.ECDSA.NoHash",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "disc_equation_Spec.ECDSA.Hash", "disc_equation_Spec.ECDSA.NoHash",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.ECDSA.NoHash@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.ECDSA.min_input_length",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.max_input_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa", "int_typing",
        "inversion-interp", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.ECDSA.Hash__0",
        "refinement_interpretation_Tm_refine_2420de9f68a4c2a48b6f2796a459baf9",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_ff8d51d518adead938b5914c7a8dbcd8"
      ],
      0,
      "aa68cc9e90ad1fe6b460636a9d624842"
    ],
    [
      "Spec.ECDSA.ecdsa_verification_agile",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.Pervasives.Native.tuple3__uu___haseq",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.ECDSA.Hash",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "data_elim_Spec.ECDSA.Hash", "disc_equation_Spec.ECDSA.Hash",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.ECDSA.hashSpec",
        "equation_Spec.ECDSA.min_input_length",
        "equation_Spec.ECDSA.prime_p256_order_seq",
        "equation_Spec.ECDSA.verifyQValidCurvePointSpec",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.P256.Definitions.point_nat",
        "equation_Spec.P256.Definitions.point_nat_prime",
        "equation_Spec.P256.bCoordinateP256",
        "equation_Spec.P256.isPointAtInfinity", "equation_Spec.P256.scalar",
        "equation_Spec.P256.toJacobianCoordinates",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqTm_refine_3952aa58162b0446b1249aba52d1eb89",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "inversion-interp", "lemma_FStar.UInt.pow2_values",
        "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_Negation",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
        "projection_inverse_Spec.ECDSA.Hash__0",
        "refinement_interpretation_Tm_refine_2420de9f68a4c2a48b6f2796a459baf9",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_562ff0d1f6682f6c9709b622af466ac0",
        "refinement_interpretation_Tm_refine_6eeac991301bace2d87f9caddf5ce8ac",
        "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
        "refinement_interpretation_Tm_refine_9f909af992651b106a7804f4d5a6ef5d",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_ff2b90c8f94db4f4bcfea92159681cf1",
        "refinement_interpretation_Tm_refine_ff87a0b6edd7d117b18cc3d5116b5cf5",
        "refinement_interpretation_Tm_refine_ff8d51d518adead938b5914c7a8dbcd8",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.length",
        "typing_Spec.ECDSA.prime_p256_order_seq",
        "typing_Spec.ECDSAP256.Definition.prime_p256_order",
        "typing_Spec.P256.bCoordinateP256"
      ],
      0,
      "34a2a5e84fec91e1d2abdf83ef4e7bfa"
    ],
    [
      "Spec.ECDSA.ecdsa_signature_agile",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.ECDSA.min_input_length",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa",
        "inversion-interp", "lemma_FStar.UInt.pow2_values",
        "lemma_Spec.ECDSA.invert_state_s", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff8d51d518adead938b5914c7a8dbcd8",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "341da57adceba83d85e1a59810954905"
    ],
    [
      "Spec.ECDSA.ecdsa_signature_agile",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.ECDSA.min_input_length",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa",
        "inversion-interp", "lemma_FStar.UInt.pow2_values",
        "lemma_Spec.ECDSA.invert_state_s", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ff8d51d518adead938b5914c7a8dbcd8",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "6ff12fe1dfd6b34d672398e1e64786c2"
    ],
    [
      "Spec.ECDSA.ecdsa_signature_agile",
      3,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.ECDSA.Hash",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "data_elim_Spec.ECDSA.Hash", "disc_equation_Spec.ECDSA.Hash",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.ECDSA.hashSpec",
        "equation_Spec.ECDSA.min_input_length",
        "equation_Spec.ECDSAP256.Definition.prime_p256_order",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.P256.Definitions.prime256",
        "equation_Spec.P256._norm",
        "fuel_guarded_inversion_Spec.ECDSA.hash_alg_ecdsa",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "inversion-interp", "lemma_FStar.UInt.pow2_values",
        "lemma_Spec.ECDSA.invert_state_s", "primitive_Prims.op_Addition",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_Spec.ECDSA.Hash__0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_2420de9f68a4c2a48b6f2796a459baf9",
        "refinement_interpretation_Tm_refine_40b6df1dde53871107e7b51f8cc2d867",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_ff87a0b6edd7d117b18cc3d5116b5cf5",
        "refinement_interpretation_Tm_refine_ff8d51d518adead938b5914c7a8dbcd8",
        "typing_FStar.Seq.Base.length", "typing_Prims.pow2",
        "typing_Spec.P256.Definitions.prime256"
      ],
      0,
      "12f71a359b574d56ce6cef1b88b4c623"
    ]
  ]
]