[
  "栛韾茶矩菅5茻"嫖9",
  [
    [
      "Spec.Hash.Lemmas.extra_state_add_nat_bound_lem1",
      1,
      0,
      0,
      [ "@query", "equation_Spec.Hash.Definitions.max_extra_state" ],
      0,
      "eec04e8dea18c15b60183425aa40b871"
    ],
    [
      "Spec.Hash.Lemmas.extra_state_add_nat_bound_lem2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.extra_state_v",
        "equation_Spec.Hash.Definitions.max_extra_state",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1",
        "typing_Spec.Hash.Definitions.extra_state_v"
      ],
      0,
      "fb51362b88b32507ff786a4bf43d8e98"
    ],
    [
      "Spec.Hash.Lemmas.extra_state_add_nat_bound_associative_lem",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.squash",
        "equation_Spec.Hash.Definitions.extra_state_int_type",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.max_extra_state",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_8a540bd64b8123f5d68c785aa9b43b6e",
        "typing_Spec.Hash.Definitions.is_blake"
      ],
      0,
      "c5b35b734a9e5289ae30f9f307a6c506"
    ],
    [
      "Spec.Hash.Lemmas.extra_state_v_of_nat",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "4ee7175485ce8d3c52f543bac10e6c09"
    ],
    [
      "Spec.Hash.Lemmas.update_multi_zero",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "ab2e74958730720b1ca2be088ff10a0a"
    ],
    [
      "Spec.Hash.Lemmas.update_multi_update",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "a52279a5f0f31a62e7d62c1a9bca9752"
    ],
    [
      "Spec.Hash.Lemmas.update_multi_associative",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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",
        "equation_Lib.IntTypes.uint8",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.bytes",
        "equation_Spec.Hash.Definitions.bytes_blocks",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "function_token_typing_Lib.IntTypes.uint8",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004"
      ],
      0,
      "d5ecf703e736c5e8f466e6e6c453e63f"
    ],
    [
      "Spec.Hash.Lemmas.pad_invariant_block",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "3a735c4a12f4720ba856b5f25d62c428"
    ],
    [
      "Spec.Hash.Lemmas.max_input_size_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.len_length",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e",
        "typing_Spec.Hash.Definitions.len_length"
      ],
      0,
      "4189afb8feec9f50e3c768e343b539b8"
    ],
    [
      "Spec.Hash.Lemmas.pad_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Tm_unit", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.len_length",
        "equation_Spec.Hash.Definitions.word_length", "int_inversion",
        "primitive_Prims.op_Addition", "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_2043fe1d818aaeaa104a717402baf403",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.Hash.Definitions.block_length",
        "typing_Spec.Hash.Definitions.is_md",
        "typing_Spec.Hash.Definitions.len_length",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "6bf7fdd6c1d91d8d0dc20e031d18bdd3"
    ]
  ]
]