[
  "�/Cc�糷Lk�����k",
  [
    [
      "Hacl.SolinasReduction.Lemmas.c8_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b411ace451b110816740573f9f077886"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c8_reduction",
      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",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "11645b6357ab2bbdc6da2dcce4e5fcf5"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c8_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "6ec980bf6e990fe9fcbf5ac331557663"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c9_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "e4e513d3986b27c30218a2792259d719"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c9_reduction",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "fa37c569c5d470a655adce7e3201954d"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c9_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "ea1e33b36f7ae89b9b37e687cccdc22a"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c10_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "7f5d6fc6e45d61ef2e08be9594c509fe"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c10_reduction",
      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",
        "equation_Hacl.SolinasReduction.Lemmas.prime",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "ebe6fbef850b07ccebfa07de4c9f5fde"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c10_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "962cd13aa07b9570b417ff43ca63665d"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c11_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "83367282fed26dfed55dbce1c16bf1c9"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c11_reduction",
      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",
        "equation_Hacl.SolinasReduction.Lemmas.prime",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "2ec8dcd680f12d3c5c3402dd6bc46196"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c11_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "7edf302eb8f3b4aa15ffa01639d72b2d"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c12_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "f02d2a0fb6267f440f8472aaeba817c3"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c12_reduction",
      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",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "b1bc4cfcb85f32a77c2eb1101ad866f2"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c12_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "33424a04b74d2fbcaa33c21ad2b8bec9"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c13_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "ccda54bb466bcba27a4aad2cc9c27dca"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c13_reduction",
      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",
        "equation_Hacl.SolinasReduction.Lemmas.prime",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "3e9f7efcdadefb884b5d55a547c6087c"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c13_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "713475ebe372b0bebae373c85c099e77"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c14_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "abe926da81d42a11c5017709e005070e"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c14_reduction",
      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",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "5142365ad1b7521d11d2fd4547a58726"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c14_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "34cee6e9d869214c185e15f202f7a1cd"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c15_reduction",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "c304174f29f986a49130e9e94df1d726"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c15_reduction",
      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",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "8107b5243aaf7dfc1eeb7f09f1631d46"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.c15_reduction",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "c722318f184e649b1ab3e9fc28b4a71d"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.inside_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1"
      ],
      0,
      "69ffee182373e3ca5828d391e1ae95fb"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.inside_mod",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1"
      ],
      0,
      "7f6b0ce214ddff066e7903cbc148f59a"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.inside_mod1",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1"
      ],
      0,
      "b1c4ba8350c64a2967bef996b59edea4"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.inside_mod1",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "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_0c4926e33a4dc1c024a6bb2210141ee1"
      ],
      0,
      "152f19c1407cd7d1916e3d3d95b3f0b0"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.solinas_reduction_nat",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "ef577d68ddc9eaad91cd2f6b8498f9df"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.solinas_reduction_nat",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.SolinasReduction.Lemmas.prime", "equation_Prims.pos",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Minus",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_02baf468de6d2058f5681c08ad70ab27",
        "refinement_interpretation_Tm_refine_07769634373704e21d8e3229f02e26ee",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_4972ae19de163144b1563f5897049e01",
        "refinement_interpretation_Tm_refine_546bffe8079f1836b8d8e9fd1a20cc2a",
        "refinement_interpretation_Tm_refine_54e4d69efb9c3be455ede71fc30479ed",
        "refinement_interpretation_Tm_refine_67ee90e76e457943b4c6064159ff5049",
        "refinement_interpretation_Tm_refine_6ed473a820bfab2ef124fe7df89777b6",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a0e74d9303fb762dcf3cd69669b30bc7",
        "refinement_interpretation_Tm_refine_f8f96139cc63a25850e4207994141359",
        "true_interp", "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "872cc9823c4b1da5cc01ed317445e6cf"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.solinas_reduction_mod",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.SolinasReduction.Lemmas.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "910307b71b8a35ff18a794c38cd452f5"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.solinas_reduction_mod",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.SolinasReduction.Lemmas.prime", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "ceaa83f2d3c55ea79e000142a728ea88"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.solinas_reduction_mod",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.SolinasReduction.Lemmas.prime", "equation_Prims.pos",
        "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_12978dd6958e32a92967efd3d823c129",
        "refinement_interpretation_Tm_refine_258ceab906c70faee92f8b2ddee2f900",
        "refinement_interpretation_Tm_refine_5334c6ac80e35985f24a70c4c5063175",
        "refinement_interpretation_Tm_refine_55959d072108f5ecf8ae7624385aec4e",
        "refinement_interpretation_Tm_refine_6057e8999c6a8b2ee5f386b0fc1363aa",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_9406355969cddb8c4e9e60fa27a4f92f",
        "refinement_interpretation_Tm_refine_9b78234fb38defd17f7aa6b28256bf75",
        "refinement_interpretation_Tm_refine_a1be018a393102a7d9a26e61ced2b46b",
        "refinement_interpretation_Tm_refine_e17834d142f50f7d6fe0cf3e2ef28645",
        "typing_Hacl.SolinasReduction.Lemmas.prime"
      ],
      0,
      "93311a5f02bdfd94254e65a806ff2464"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.reduce_brackets",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "d92a85cc8e5df2d3c7aee3199563bc96"
    ],
    [
      "Hacl.SolinasReduction.Lemmas.reduce_brackets",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Minus",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "344f8e98f4df355782cadb5311ddcfe0"
    ]
  ]
]