Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
Spec.Blake2.fst.hints
[
"i\u001f�\u001d�\t����/\u0016\u0007�t�",
[
[
"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,
"9c2023169bf107d7895b554fc0ee317c"
],
[
"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,
"47213c19048797b79c86819d71172e3b"
],
[
"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,
"19dd371b29849da7a3469d8b98d3ea92"
],
[
"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,
"80ffe48fd11927c1a4ecd8c42a2c1e0f"
],
[
"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,
"41201522f087942408559dd67f1c85c3"
],
[
"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,
"7627671247e73cdc1fcb0c715bf0608c"
],
[
"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,
"25d6a2cbf9d7abf2e8bd744694557137"
],
[
"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,
"52cb2ff1d962f0fb402094477a4ff174"
],
[
"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,
"01065c015923028449ff9d2bf9c3582a"
],
[
"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,
"6b8fbe36658f87654ff9f53bfec23f1b"
],
[
"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,
"b8d95f5993c652413cafe76839b4c43e"
],
[
"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",
"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.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_BoxBool_proj_0",
"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,
"b7a0975c99a3f29d8bd5da08a916ce72"
],
[
"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,
"6af7069dd17af57a6e0475ea67086689"
],
[
"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,
"5ef9e785d668e5d61e3d69a532b436d2"
],
[
"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,
"296da4671388577ab44cd1764be55c55"
],
[
"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,
"f06016c9e6923cf6e8aeb84f3450dd6c"
],
[
"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,
"fdc7eea08fc281329105e5e210858a61"
],
[
"Spec.Blake2.gather_row",
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",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.Blake2.size_word", "equation_Spec.Blake2.word_index",
"equation_Spec.Blake2.wt", "fuel_guarded_inversion_Spec.Blake2.alg",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_3cd4c85c6263b279b491272c687f2da6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_69f236e3cb5cb57e71cf3fabf87c9ede",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.v", "typing_Spec.Blake2.size_word",
"typing_Spec.Blake2.wt", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"45308f5ecfe1d38a61d78d642dc378c6"
],
[
"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,
"c9c922fe1cce3d5e15fe594add18efd0"
],
[
"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,
"08d0bde160f4f1d81ddb58696430098e"
],
[
"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,
"1257e427acf01a2d68671165715a35f3"
],
[
"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,
"7d86bf7fff6cc36364d84889bf10aa25"
],
[
"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,
"d7290968a0b7df7ef5066358192b2c49"
],
[
"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,
"00b91d7beea73d9567b64237074e7950"
],
[
"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,
"2d9c3fe249969565bc90edb63881078d"
],
[
"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,
"f1f8f63b63366e23960e90503333435a"
],
[
"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,
"918fcf19ce439d9657597a01e6fb9a06"
],
[
"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",
"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_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_1e953f2d5946486a5238378f4635f5c8",
"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,
"bbc16dc7ce11e8031b0ade2544ca82cc"
],
[
"Spec.Blake2.list_iv_S",
1,
2,
1,
[ "@query" ],
0,
"b89db387d46faa182c1fb74dd0697462"
],
[
"Spec.Blake2.list_iv_B",
1,
2,
1,
[ "@query" ],
0,
"29b4cff698ccb746cb52b1a669acb8d2"
],
[
"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",
"equation_Spec.Blake2.pub_word_t", "equation_Spec.Blake2.wt",
"fuel_guarded_inversion_Spec.Blake2.alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"c3434f967dc10098a0d59d326786b9c0"
],
[
"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",
"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_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4ae53dbeb83c66a28889660f564654ad",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"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,
"f9cd801f2692e6d4bd6592476f53c214"
],
[
"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,
"5fec99314e9bb9657e208f32e319f5e0"
],
[
"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,
"0473f38d4e07fdaa45a1965300c384ce"
],
[
"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,
"35850a8425a396c15f855920771e9227"
],
[
"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,
"9372485472835cc3b3d1e7719bac1049"
],
[
"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,
"7dde70283f823e3aeb0473790ca98965"
],
[
"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,
"f55dc945e4d28b5a4b7b4a9cc6271735"
],
[
"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,
"a1f654e52570e7d98cc7724f98539c00"
],
[
"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,
"b831595bce8900c8395948cf65e29152"
],
[
"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,
"2e486a78258db256d1dc42530aa4725c"
],
[
"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,
"dc47e664172b8f17e386d7fdd52b6816"
],
[
"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,
"60a85a1d9c03cbb8244094e79ac82d1b"
],
[
"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,
"2857f59305aa9d47d8b77252bb945044"
],
[
"Spec.Blake2.blake2_round",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.Blake2.size_block_w", "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_block_w"
],
0,
"adfd94369b0b3c9d33f662393f3d206d"
],
[
"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,
"f59a8767e40f89b2d0a2a76efda328b9"
],
[
"Spec.Blake2.blake2_compress2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Blake2.rounds",
"equation_Spec.Blake2.size_block_w",
"fuel_guarded_inversion_Spec.Blake2.alg",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Blake2.size_block_w"
],
0,
"9c56939a04ed6678be492ad9fc39964a"
],
[
"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,
"add1a9cd31d9deed9bbec7d37817f2bc"
],
[
"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,
"1abe407c4e4dd73d3567132f598c44b9"
],
[
"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,
"18fc7592d56b6f1c67390e9cada3e8bb"
],
[
"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,
"79e2aae8a5c976378e08edeacabf76e0"
],
[
"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,
"f12ff7ac601117ef7cfdd68de6e06036"
],
[
"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,
"4d7d794298d3be85a1826dac6225ed13"
],
[
"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,
"63d9ae239003e31af3bcb7abcb3daf93"
],
[
"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,
"1679b3655e5086d87f28fb534672a351"
],
[
"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,
"67e17e55f9e31b65fbdbe5981bf17539"
],
[
"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,
"508169af7a972c47582fa48bfaa44fe7"
],
[
"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,
"df93cfcb748efeb626c736496b6fbc13"
],
[
"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,
"846aa756e39cbdf8ceccf1bd82d12c47"
],
[
"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,
"3571b845d6b34a91ae06088305f12e6b"
],
[
"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,
"d2328e5346ef8cff659a5ed0ec4f9836"
],
[
"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,
"59aba1bf46502603da98444c9ab49109"
],
[
"Spec.Blake2.blake2_update_blocks",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "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.unsigned", "equation_Lib.Sequence.length",
"equation_Prims.nat", "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_Prims.__cache_version_number__",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"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_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_48433331ccd8c5a34e435d330953a412",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_606f6a246ea8a192b740aa2a00b2d32b",
"typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.size_block",
"typing_Spec.Blake2.wt"
],
0,
"b9c55085bfedde27e38a11a6c2693a65"
],
[
"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,
"d9ef0ef8cb6e271a45da1d0379deb18e"
],
[
"Spec.Blake2.blake2_init",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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.length",
"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",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2ca63b474b7fe41a1c5e08b83da550ed",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_73d0b0b464df1adafbcbfb54c10358d3",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8fa940f184823396dcd60a792f610891",
"refinement_interpretation_Tm_refine_aebf0a5a4cc5a0edddd5cedf26878e34",
"refinement_interpretation_Tm_refine_c3843a26e25ce7e9f9117f2eceef1554",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Blake2.size_block", "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,
"22f5bd16b931da8db782580cfa01eb16"
],
[
"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,
"ad8054663442e2204d255c7e0ca02329"
],
[
"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,
"4cf3e15bd06c4420ba66f2cc0ee9a64d"
],
[
"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,
"b4e74c5ebecf82271e6eb02566b27e45"
],
[
"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,
"db5939044f5077f7d14cb438a6d179e6"
],
[
"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,
"a0e069990a55c6ef991e7df60ca3b53a"
],
[
"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,
"bd818c00dd342f622c60a395ed27adc4"
],
[
"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,
"cbec9c4bc911de05f04535fdf31d2bf9"
],
[
"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,
"c56e234eb99ae00b116fa9dbf624a099"
],
[
"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,
"985c1c12125af75f995757b47fb63b8d"
],
[
"Spec.Blake2.blake2b",
3,
2,
1,
[
"@MaxIFuel_assumption", "@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.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_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_4e807db89561415dba8de5423d095948",
"refinement_interpretation_Tm_refine_b2f401c86b1ac09121e85d42b2a60dca"
],
0,
"c07b74b528c48566a9390ed5f4d91cb8"
]
]
]
Computing file changes ...
