[
  "­OÎSù\\.ã¯Z }¢\u0004Îý",
  [
    [
      "Spec.Blake2.alg_inversion_lemma",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok",
        "fuel_guarded_inversion_Spec.Blake2.alg"
      ],
      0,
      "b95d48dad96cdad70a35e710ca8678f3"
    ],
    [
      "Spec.Blake2.wt",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "projection_inverse_BoxBool_proj_0", "typing_Lib.IntTypes.unsigned",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "21e7c8f3abf66595c574b01afd72764b"
    ],
    [
      "Spec.Blake2.rounds",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "fuel_guarded_inversion_Spec.Blake2.alg"
      ],
      0,
      "cb7bf525733bd835da90643fe64f8623"
    ],
    [
      "Spec.Blake2.size_hash_w",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "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,
      "13aa6a7abe3650471279216e26f3c8d1"
    ],
    [
      "Spec.Blake2.size_block_w",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "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,
      "ce0ded28d4a88cb41e28825ac9492f7d"
    ],
    [
      "Spec.Blake2.size_word",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.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",
        "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", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "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,
      "25c4ecc482ea93fa185b18c25cd0f8df"
    ],
    [
      "Spec.Blake2.size_block",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.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",
        "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", "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Blake2.alg", "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",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f1832d691b3a7a66bf4fc8c3278524fb"
    ],
    [
      "Spec.Blake2.size_ivTable",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "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,
      "3ede6eec66b5cb2ac5a63682e5ea439e"
    ],
    [
      "Spec.Blake2.size_sigmaTable",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "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,
      "2c114dac5909135592fe2f99db4cce94"
    ],
    [
      "Spec.Blake2.max_key",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "fuel_guarded_inversion_Spec.Blake2.alg"
      ],
      0,
      "925020cee3bd58ba84842a8c3ab78bdb"
    ],
    [
      "Spec.Blake2.max_output",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "fuel_guarded_inversion_Spec.Blake2.alg"
      ],
      0,
      "48d5df46537722c1df62fbbc56d4044c"
    ],
    [
      "Spec.Blake2.limb_inttype",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg"
      ],
      0,
      "180295c0b74c89c3c1782de74676950a"
    ],
    [
      "Spec.Blake2.zero",
      1,
      2,
      1,
      [
        "@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_Spec.Blake2.Blake2B",
        "constructor_distinct_Spec.Blake2.Blake2S",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "98f3643e6204907d2346fce4a9cc8e15"
    ],
    [
      "Spec.Blake2.row",
      1,
      2,
      1,
      [
        "@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.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,
      "36c82b71c6596aabe55329f29674afd0"
    ],
    [
      "Spec.Blake2.zero_row",
      1,
      2,
      1,
      [
        "@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.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,
      "a40d396d62a550237e66458cc009d51a"
    ],
    [
      "Spec.Blake2.load_row",
      1,
      2,
      1,
      [
        "@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.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,
      "c0214e54b5a51f2f60005f288d682128"
    ],
    [
      "Spec.Blake2.load_row",
      2,
      8,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@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_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Nil@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Blake2.wt",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.int_t",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c0ac1341cb7978ea8be5259b5e6bc29e"
    ],
    [
      "Spec.Blake2.create_row",
      1,
      8,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.wt",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.int_t",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5c89c1374d09a1d40dd88888c0c6ab1e"
    ],
    [
      "Spec.Blake2.state",
      1,
      2,
      1,
      [
        "@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.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,
      "d46b3118b0ac718e08aac48bfe4fc473"
    ],
    [
      "Spec.Blake2.limb_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.wt"
      ],
      0,
      "a47c2618279a2846bf5a3a885899462c"
    ],
    [
      "Spec.Blake2.nat_to_word",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "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",
        "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Spec.Blake2.alg", "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_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f57c247648098ff29754a115811219af"
    ],
    [
      "Spec.Blake2.nat_to_limb",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "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",
        "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@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.int_t",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.op_At_Percent_Dot",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Spec.Blake2.alg", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.shift_left_lemma",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "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",
        "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
        "refinement_interpretation_Tm_refine_23d9c37b01d6158fcfa6197588fa0e41",
        "refinement_interpretation_Tm_refine_27f0a9428ddc1636d61756c9573914b3",
        "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_437536e2c8d142f943f725987f6e627c",
        "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
        "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a",
        "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53",
        "typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.unsigned",
        "typing_Lib.IntTypes.v", "typing_Prims.pow2",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "7455f5aa9c764768674ad502896f79d1"
    ],
    [
      "Spec.Blake2.word_to_limb",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "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",
        "disc_equation_Lib.IntTypes.SEC", "disc_equation_Lib.IntTypes.U32",
        "disc_equation_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@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.to_u128",
        "equation_Lib.IntTypes.to_u64", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Blake2.alg", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.v_injective",
        "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_2d2223d734048d55d30762c56874ad10",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
        "refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast",
        "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned",
        "typing_Lib.IntTypes.v", "typing_Spec.Blake2.wt",
        "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "642f0d6053c3f4e01144737d1a8cd984"
    ],
    [
      "Spec.Blake2.limb_to_word",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.wt"
      ],
      0,
      "3234ed923303e1d6e658edea07a5e38d"
    ],
    [
      "Spec.Blake2.rtable_t",
      1,
      2,
      1,
      [
        "@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.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,
      "a89211e5ac2b4d0f5c9b1c8038fdc97a"
    ],
    [
      "Spec.Blake2.rTable_list_S",
      1,
      8,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@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_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Nil@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.rotval",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "typing_FStar.List.Tot.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.rotval",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "9338cfb363e1cf0fe617f5123a148f3f"
    ],
    [
      "Spec.Blake2.rTable_list_B",
      1,
      8,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_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_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Nil@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.rotval",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Prims.nat",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "typing_FStar.List.Tot.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.rotval",
        "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "cd54ca7c11782a46093eb1e2585ed066"
    ],
    [
      "Spec.Blake2.rTable",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Spec.Blake2.Blake2B",
        "constructor_distinct_Spec.Blake2.Blake2S", "data_elim_Prims.Cons",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok",
        "equation_FStar.List.Tot.Properties.llist",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.rotval",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.Blake2.wt",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "fuel_guarded_inversion_Prims.list",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
        "refinement_interpretation_Tm_refine_1e953f2d5946486a5238378f4635f5c8",
        "refinement_interpretation_Tm_refine_4fad4f0e6a4f281ff364679821c5e308",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.rotval",
        "typing_Spec.Blake2.rTable_list_B",
        "typing_Spec.Blake2.rTable_list_S", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a6d6e0aaff27224cded93d20758a2692"
    ],
    [
      "Spec.Blake2.list_iv_S",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "9f8494c2de0c5be33abc74092f7f9ef3"
    ],
    [
      "Spec.Blake2.list_iv_B",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "4e8170efcbac47a551c0a3dcaa48545c"
    ],
    [
      "Spec.Blake2.list_iv",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Blake2.Blake2B",
        "constructor_distinct_Spec.Blake2.Blake2S",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok",
        "equation_Spec.Blake2.pub_word_t", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg"
      ],
      0,
      "418c77108f540540343b28c449d18276"
    ],
    [
      "Spec.Blake2.ivTable",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@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_Spec.Blake2.Blake2B",
        "constructor_distinct_Spec.Blake2.Blake2S",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok",
        "equation_FStar.List.Tot.Properties.llist",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.Blake2.pub_word_t",
        "equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4ae53dbeb83c66a28889660f564654ad",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_950fff121f14bb62cc276cf7ccaa3ff5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d",
        "typing_Lib.IntTypes.bits", "typing_Spec.Blake2.list_iv_B",
        "typing_Spec.Blake2.list_iv_S", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "6dcb12a05601dc867821ae69b8a8fddb"
    ],
    [
      "Spec.Blake2.list_sigma",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@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",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
        "typing_Lib.IntTypes.v", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "ce0ed9b20bae8c860a2b25b9eef7bcbd"
    ],
    [
      "Spec.Blake2.sigmaTable",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "typing_Spec.Blake2.size_sigmaTable"
      ],
      0,
      "cb009946ff55aac47b5e223c3af1fca3"
    ],
    [
      "Spec.Blake2.block_w",
      1,
      2,
      1,
      [
        "@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.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,
      "e83699cff10d6529879827ee2d293a5c"
    ],
    [
      "Spec.Blake2.op_Hat_Bar",
      1,
      2,
      1,
      [
        "@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.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,
      "2030eb5238986c9aa1f45db58447674e"
    ],
    [
      "Spec.Blake2.op_Plus_Bar",
      1,
      2,
      1,
      [
        "@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.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,
      "440877a8f83a962f467dcfa5ab33f275"
    ],
    [
      "Spec.Blake2.op_Greater_Greater_Greater_Bar",
      1,
      2,
      1,
      [
        "@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.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.wt", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_Spec.Blake2.wt",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b4c2d245698bf6c13dbd95e186e4ed52"
    ],
    [
      "Spec.Blake2.rotr",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus",
        "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,
      "28fe13e02af41ab73234b346d846e251"
    ],
    [
      "Spec.Blake2.g1",
      1,
      2,
      1,
      [
        "@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.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.row_idx", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e842195112d29f57633c993141d591ce"
    ],
    [
      "Spec.Blake2.g2",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.row_idx", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "d8715be9836bb278f430ea51959fe1be"
    ],
    [
      "Spec.Blake2.g2z",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.row_idx", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "0a745c631ec97bb5096f8b82a37ec9a3"
    ],
    [
      "Spec.Blake2.blake2_mixing",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "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",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "1bea05f1d1e144daf58462631fcc9920"
    ],
    [
      "Spec.Blake2.diag",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_17c51effd816c32ad167d45f4a9381be",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9eaf04168d52dbc17d7a6818208841b4",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "e8fb7346c394d6cb8622fb7dcb0c197f"
    ],
    [
      "Spec.Blake2.undiag",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822b3b64558f9bb55599a4aaaebfaad3",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_f8570330b38a7f953a1e818b1d7fe008",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5774b86c8fea28a0c879a7a95aece800"
    ],
    [
      "Spec.Blake2.gather_row",
      1,
      2,
      1,
      [
        "@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.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@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",
        "equation_Spec.Blake2.sigma_elt_t", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_361d0715b9ad9ccd6ef6a39d84f817c3",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "058edb7984931d4210f0fee8d617097d"
    ],
    [
      "Spec.Blake2.gather_state",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "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_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.Blake2.sigma_elt_t",
        "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_sigmaTable",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.word_index",
        "equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg",
        "int_inversion", "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_01c5e94ff20e162404ed1970e03453cd",
        "refinement_interpretation_Tm_refine_17fc3b2091bdbf7f8db11b96cc6c1dd5",
        "refinement_interpretation_Tm_refine_2ae121561989b39eef8c171dce49c388",
        "refinement_interpretation_Tm_refine_34e8205be48ddeff1999834b3f4adcea",
        "refinement_interpretation_Tm_refine_361d0715b9ad9ccd6ef6a39d84f817c3",
        "refinement_interpretation_Tm_refine_385fffdfb8d3eaca12163c56c02c9bbc",
        "refinement_interpretation_Tm_refine_4e2c809c7c5a937204cd004b0673352f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_69f236e3cb5cb57e71cf3fabf87c9ede",
        "refinement_interpretation_Tm_refine_8aec142d4cb5c946067ebf3dd5257382",
        "refinement_interpretation_Tm_refine_8c8802bdcd8f71504c01b9792d5c281b",
        "refinement_interpretation_Tm_refine_98ced31caf69cff161b216d0c23f9d79",
        "refinement_interpretation_Tm_refine_aa7402783ceb0779e702eb460adf4724",
        "refinement_interpretation_Tm_refine_ab6ebba55451db7cdbeca164959474e1",
        "refinement_interpretation_Tm_refine_afe49d516f3a72a82c5bc4b0e855e0ba",
        "refinement_interpretation_Tm_refine_b70228936c34d6502ee8d7a773ab329a",
        "refinement_interpretation_Tm_refine_b7d67cefc84d92914af10fc9752cf4ae",
        "refinement_interpretation_Tm_refine_bb1f82ee76e01b1e284118c7c219d4ca",
        "refinement_interpretation_Tm_refine_e38c486bc668397e8ca355d2ae47eb1d",
        "refinement_interpretation_Tm_refine_e72d22bd05280c31cd04985da25ed43b",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f277e482ef67177cff281b206eae44b2"
    ],
    [
      "Spec.Blake2.blake2_round",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Spec.Blake2.size_sigmaTable", "int_inversion",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.Blake2.size_sigmaTable"
      ],
      0,
      "bccc463850587884c7de21432900c1c5"
    ],
    [
      "Spec.Blake2.blake2_compress0",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U1",
        "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.unsigned", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.size_block_w",
        "typing_Spec.Blake2.wt"
      ],
      0,
      "d4d578a905403af1e1f6578f56218ffd"
    ],
    [
      "Spec.Blake2.blake2_compress1",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@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.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "acdedc005ffa67ba154d2ae36ebe9ecf"
    ],
    [
      "Spec.Blake2.blake2_compress2",
      1,
      2,
      1,
      [
        "@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.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.rounds",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "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,
      "6758df96c16ff61e18eecd69c8714401"
    ],
    [
      "Spec.Blake2.blake2_compress3",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_93f50f0b71b52dbb3b11ff3de54d00fc",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c36011be82a9932a862baae4f94fec2a"
    ],
    [
      "Spec.Blake2.blake2_update_block",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg",
        "refinement_interpretation_Tm_refine_23d9c37b01d6158fcfa6197588fa0e41",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.wt"
      ],
      0,
      "beb4f19acd674946ca3bad47f5348072"
    ],
    [
      "Spec.Blake2.blake2_update1",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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.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.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "3759b5a7f6978397acc47c58700df2c4"
    ],
    [
      "Spec.Blake2.get_blocki",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "d4d0e912cbdac16d79855cc3f661c6b8"
    ],
    [
      "Spec.Blake2.get_blocki",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
        "equation_Prims.nat", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2ce8c7b4dfc50547b9909cb7df44a470",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_66de5bb0aba58911f0c137ad784fa679",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Blake2.wt"
      ],
      0,
      "4d5ab55c98d328c6ababc047eb5218e7"
    ],
    [
      "Spec.Blake2.blake2_update1",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "d4f7bd50117bc911234798991102b4f0"
    ],
    [
      "Spec.Blake2.blake2_update1",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "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",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ca14e2da9b8d1ca948d80ada44d6fb08",
        "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length",
        "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt",
        "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "7cc362dfbad6cf5c41dfbcae57798467"
    ],
    [
      "Spec.Blake2.blake2_update_last",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "7007691725118ec37072f41246f9bd82"
    ],
    [
      "Spec.Blake2.get_last_padded_block",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "27b31113d8af27f1b5d8729766ea82b1"
    ],
    [
      "Spec.Blake2.get_last_padded_block",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "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.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.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.wt",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2ca63b474b7fe41a1c5e08b83da550ed",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8fa940f184823396dcd60a792f610891",
        "refinement_interpretation_Tm_refine_c85364e35a6e5494767f5baa5dab6bd6",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
        "typing_Lib.IntTypes.unsigned", "typing_Lib.Sequence.length",
        "typing_Prims.pow2", "typing_Spec.Blake2.size_block",
        "typing_Spec.Blake2.size_block_w", "typing_Spec.Blake2.wt",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "8fb1f6a01b2df48411959b1d6a62d479"
    ],
    [
      "Spec.Blake2.blake2_update_last",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "9f60a21635110c94b7798eea08ac8b62"
    ],
    [
      "Spec.Blake2.blake2_update_last",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.Blake2.wt",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2675635261b40c4136c00e0e9da0b67c",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.wt"
      ],
      0,
      "ba833cba5607a47deed02c1252a4422c"
    ],
    [
      "Spec.Blake2.blake2_update_blocks",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "956732e9dad04ff9c03ed56b863fb715"
    ],
    [
      "Spec.Blake2.split",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
        "equation_Prims.nonzero", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "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_0766302b68bb44ab7aff8c4d8be0b46f",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.Blake2.size_block"
      ],
      0,
      "5868d683a6eec9a3b1f2d53eff1887fe"
    ],
    [
      "Spec.Blake2.blake2_update_blocks",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "92b7f20db3bda041e67355c593ba8e4f"
    ],
    [
      "Spec.Blake2.blake2_update_blocks",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length",
        "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem",
        "equation_Lib.UpdateMulti.split_at_last_nb_rem",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split",
        "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "function_token_typing_Lib.IntTypes.uint8", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_48433331ccd8c5a34e435d330953a412",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_606f6a246ea8a192b740aa2a00b2d32b",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7",
        "typing_Lib.IntTypes.unsigned", "typing_Lib.Sequence.length",
        "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem",
        "typing_Lib.UpdateMulti.split_at_last_nb_rem",
        "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt"
      ],
      0,
      "2bcc7860f1ae516ba0c1914db5648745"
    ],
    [
      "Spec.Blake2.blake2_init_hash",
      1,
      8,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "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_Prims.Cons", "constructor_distinct_Prims.Nil",
        "data_typing_intro_Prims.Cons@tok",
        "data_typing_intro_Prims.Nil@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "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.int_t", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Blake2.alg", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_0f3d1ef8ae53868e98858a6338b1449e",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_4ab9dee008d9c2de5582fdcbe189201d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5b99ff88a6394c3ca45673530f33f64f",
        "refinement_interpretation_Tm_refine_5e5bec36d0b93f21cc8af433c4814c28",
        "refinement_interpretation_Tm_refine_61e760ad0ee65d2a80c7c324d0c088a4",
        "refinement_interpretation_Tm_refine_68846648ced36d149301da3485ba2619",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_80138754f56cd45de15379a479c14182",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_aebf0a5a4cc5a0edddd5cedf26878e34",
        "refinement_interpretation_Tm_refine_c78aebbbb097cec11b60fdae700a97b2",
        "refinement_kinding_Tm_refine_d8d83307254a8900dd20598654272e42",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.logxor",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.create_row",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "14ff15b86917286023b119c15b576c1f"
    ],
    [
      "Spec.Blake2.blake2_update_key",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "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",
        "equality_tok_Lib.IntTypes.U128@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.numbytes", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Blake2.max_key",
        "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Blake2.alg", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_2ca63b474b7fe41a1c5e08b83da550ed",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8fa940f184823396dcd60a792f610891",
        "refinement_interpretation_Tm_refine_ba7cbc92596cc8d5fc8576c12380380c",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
        "typing_Prims.pow2", "typing_Spec.Blake2.size_block",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
        "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "94959e0619cdf08e1ceff805594b8dc1"
    ],
    [
      "Spec.Blake2.blake2_update",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "7a26cbb03e9f98c051c6708e7820dd25"
    ],
    [
      "Spec.Blake2.blake2_update",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d8fea79d079c0141c715290043943c38"
    ],
    [
      "Spec.Blake2.blake2_update",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.wt",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6dc5a77fa672ca1a894a17f09cd1c9b4",
        "refinement_interpretation_Tm_refine_c3843a26e25ce7e9f9117f2eceef1554",
        "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.size_block",
        "typing_Spec.Blake2.wt"
      ],
      0,
      "776486d8ce1e98a5448e18c4176cdde2"
    ],
    [
      "Spec.Blake2.blake2_finish",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.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",
        "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_Prims.nat", "equation_Spec.Blake2.max_output",
        "equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg",
        "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",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_aebf0a5a4cc5a0edddd5cedf26878e34",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "74bdac60560e9c2626007dce2f568a82"
    ],
    [
      "Spec.Blake2.blake2",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "33f19a627d84e325ffa8f6876420212e"
    ],
    [
      "Spec.Blake2.blake2",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a5c9d74a4a28900fd5b21526207b88a9"
    ],
    [
      "Spec.Blake2.blake2",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Lib.IntTypes.numbytes", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Spec.Blake2.compute_prev0",
        "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_26aea1c67e5d1f78039985ffdac548eb",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.Blake2.size_block"
      ],
      0,
      "b5876b25b191906d4fe2b3a09edd3739"
    ],
    [
      "Spec.Blake2.blake2s",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "94b0209420a5f0ad2f2769645a3fdc6d"
    ],
    [
      "Spec.Blake2.blake2s",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "78bf573654cb5ba756833a3d9a8c2d31"
    ],
    [
      "Spec.Blake2.blake2s",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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.Blake2.Blake2S",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.Blake2.max_key",
        "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output",
        "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.size_block_w",
        "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_88a96d9787797f77a8f9f0d6d5ce01c3",
        "refinement_interpretation_Tm_refine_edeb59baa0f82f232d2e3a513d60ceba"
      ],
      0,
      "8ff299de816bd7c2cb66288010b3952c"
    ],
    [
      "Spec.Blake2.blake2b",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "08e27a1eb22825be1c9db94c9e8e2c8a"
    ],
    [
      "Spec.Blake2.blake2b",
      2,
      2,
      1,
      [
        "@query", "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "8a8a9b30063edbaec7730f2323399b3e"
    ],
    [
      "Spec.Blake2.blake2b",
      3,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "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.Blake2.Blake2B",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Blake2.Blake2B@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_limb",
        "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.size_block",
        "equation_Spec.Blake2.wt",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_3907277996ab16fe2e1063243689aafc",
        "refinement_interpretation_Tm_refine_4e807db89561415dba8de5423d095948",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_Spec.Blake2.size_block",
        "typing_tok_Lib.IntTypes.U128@tok",
        "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Spec.Blake2.Blake2B@tok"
      ],
      0,
      "7a4746fa4897038bf4537c238a9646c6"
    ]
  ]
]