[
  "��%=6=x�4�\u00112�\u001ei�",
  [
    [
      "Spec.SHA3.Constants.rotc_list",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.rotval",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Spec.SHA3.Constants.rotc_t",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cdc36a88bd3b51d8ada6273fa2e8c71d",
        "typing_FStar.UInt32.uint_to_t"
      ],
      0,
      "f3340b3bc6fa629249c9a87cb06bdf48"
    ],
    [
      "Spec.SHA3.Constants.keccak_rotc",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e3ff3cadf1c18c89ef829ea2a2ce9d5d"
    ],
    [
      "Spec.SHA3.Constants.sizes_v",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.SHA3.Constants.piln_t",
        "refinement_interpretation_Tm_refine_a162028ca3205a66395c8d9e4bfa2fbf"
      ],
      0,
      "1d232e949ef51e9902e9084dba00c9a2"
    ],
    [
      "Spec.SHA3.Constants.piln_list",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "eee0b92e7bfcea6ed4d9e0d2082baf1c"
    ],
    [
      "Spec.SHA3.Constants.keccak_piln",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "fa2ff00786837710303105b1a507ea11"
    ],
    [
      "Spec.SHA3.Constants.keccak_rndc",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f8d5d18c903937a35d8c7b697d4cd88f"
    ]
  ]
]