[ "7IHdًg^_", [ [ "Spec.Hash.Incremental.blake2_init", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_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.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", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "disc_equation_Spec.Hash.Definitions.Blake2B", "disc_equation_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_uint64", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.ivTable", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.pub_word_t", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.pub_uint64", "int_typing", "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_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e", "refinement_interpretation_Tm_refine_d66783e0fb2301562e51a7d0c9630d91", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_Prims.pow2", "typing_Spec.Blake2.ivTable", "typing_Spec.Blake2.pub_word_t", "typing_Spec.Hash.Definitions.uu___is_Blake2B", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Spec.Blake2.Blake2B@tok" ], 0, "9ae0192aa665127005aa8e063ffd82fc" ], [ "Spec.Hash.Incremental.last_split_blake", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "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.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.block_s", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "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_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", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_09630c7d170f75d893f43322b29ffb46", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.split", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.word_length", "unit_typing" ], 0, "5e3bdfce45df7c305f298b035d84a8b2" ], [ "Spec.Hash.Incremental.update_last_blake", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "typing_Spec.Hash.Definitions.word_length" ], 0, "6bc8d0ae939eb49befbd277317c1a4bc" ], [ "Spec.Hash.Incremental.update_last_blake", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "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_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.block_s", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.Hash.Incremental.last_split_blake", "function_token_typing_Lib.IntTypes.uint8", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_0dd7d82d89ad57ee72279b3caed814b3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b40fcd8f119b500a437777dd70ce3945", "refinement_interpretation_Tm_refine_c85364e35a6e5494767f5baa5dab6bd6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Pervasives.Native.fst", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Spec.Blake2.get_last_padded_block", "typing_Spec.Hash.Definitions.extra_state", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.words_state_", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "unit_typing" ], 0, "ee94077a44e1c24b8374dffbc41cba08" ], [ "Spec.Hash.Incremental.update_last", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.word_length" ], 0, "68a761a4800e4ef4f04e45d9bafeea8d" ], [ "Spec.Hash.Incremental.update_last", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "equation_FStar.Seq.Base.op_At_Bar", "equation_Lib.IntTypes.uint8", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0dd7d82d89ad57ee72279b3caed814b3", "refinement_interpretation_Tm_refine_422c2869ebae5b3d7328a98714ce88bc", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_b40fcd8f119b500a437777dd70ce3945", "typing_FStar.Seq.Base.length", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.word_length" ], 0, "e2b2398b5d115e74d3adc401adc5f749" ], [ "Spec.Hash.Incremental.pad", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.is_md", "typing_Spec.Hash.Definitions.word_length" ], 0, "431aafd8f32400a14dac33cd51e13a0e" ], [ "Spec.Hash.Incremental.split_blocks", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Tm_unit", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Spec.Hash.Definitions.max_input_length" ], 0, "cd2c1842d30ae6952bbed772b1d9ce41" ], [ "Spec.Hash.Incremental.hash_incremental_body", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8", "equation_Spec.Hash.Definitions.bytes", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929" ], 0, "bc7921bd12bff6174ab2fc4dc82c3765" ], [ "Spec.Hash.Incremental.hash_incremental", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Tm_unit", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_076defedcc784372ac2411e8a227ef46", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "typing_FStar.Seq.Base.length", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word_length" ], 0, "524af871cc8f24e7da5ae160565f5d84" ], [ "Spec.Hash.Incremental.blake2_size_block_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Tm_unit", "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.numbytes", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "typing_Spec.Blake2.wt", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "53ad06579b78177e1f6c5d99d31d6ebd" ], [ "Spec.Hash.Incremental.blake2_split_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.numbytes", "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", "int_inversion", "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_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "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.split", "typing_Spec.Blake2.wt", "unit_typing" ], 0, "9d3f0338fa3844ae494fb9e95a4d1106" ], [ "Spec.Hash.Incremental.split_blocks_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "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.Seq.Properties.split", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Incremental.split_blocks", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_cc936e5a549dcdc2e3f9713145143490", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.UpdateMulti.split_at_last_lazy", "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.split", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "c7313b020b49c0d0538ed5f9628608f4" ], [ "Spec.Hash.Incremental.last_split_blake_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@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.numbytes", "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_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.block_s", "equation_Spec.Blake2.get_last_padded_block", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Incremental.last_split_blake", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_6ea94f8752d20755f3d2f50e2c16714f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c85364e35a6e5494767f5baa5dab6bd6", "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.Sequence.create", "typing_Lib.Sequence.sub", "typing_Lib.Sequence.update_sub", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Prims.pow2", "typing_Spec.Blake2.get_last_padded_block", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.size_block_w", "typing_Spec.Blake2.split", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Incremental.last_split_blake", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_typing" ], 0, "5b211e0501b991348c9a966d8f33da8e" ], [ "Spec.Hash.Incremental.last_split_blake_get_last_padded_block_eq", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "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.Seq.Properties.split", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Blake2.block_s", "equation_Spec.Blake2.get_last_padded_block", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Incremental.last_split_blake", "equation_Spec.Hash.Incremental.split_blocks", "function_token_typing_Lib.IntTypes.uint8", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c85364e35a6e5494767f5baa5dab6bd6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Spec.Blake2.get_last_padded_block", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.split", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "0d20946dbf3603482f9d19047d20ebc9" ], [ "Spec.Hash.Incremental.blake2_update_multi_one_block_eq", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@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.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Spec.Agile.Hash.update", "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_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.bytes_block", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.size_block", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Definitions.words_state_", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.Agile.Hash.update", "int_inversion", "interpretation_Tm_abs_0a22db5cb809bc71916ebf6a3b18cd56", "interpretation_Tm_abs_e3e4e6e500ae76ff6ad28ada6503a771", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "lemma_Spec.Hash.Lemmas.update_multi_update", "lemma_Spec.Hash.Lemmas.update_multi_zero", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f6a2a98bf731c95efe12337157aef9ed", "typing_FStar.Seq.Base.length", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.SEC@tok", "unit_typing" ], 0, "98392d36b0821f10d9bd16ad4566d738" ], [ "Spec.Hash.Incremental.nb_blocks_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_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.numbytes", "equation_Prims.nat", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.word_length", "unit_typing" ], 0, "fc4dad8e418fad8b50f3dd0140d1d3a2" ], [ "Spec.Hash.Incremental.nb_blocks_props", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "equality_tok_Lib.IntTypes.U128@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Prims.nat", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "int_typing", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "typing_Spec.Blake2.size_block", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_typing" ], 0, "ec01e5959bb88a4fcce12245ded047b4" ], [ "Spec.Hash.Incremental.nb_nonzero_blocks_props", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_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.numbytes", "equation_Prims.nat", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Blake2.size_block", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "d6238a86041edbab36bda1e779bd388a" ], [ "Spec.Hash.Incremental.repeati_blake2_update1_eq", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Blake2.blake2_update1", "equation_Spec.Blake2.get_blocki", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_27600e7e7507ea7fbfaf9e251ef45a73", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "typing_FStar.Seq.Base.length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "unit_typing" ], 0, "2dbab5f8b543ff7fefdb05e74df90407" ], [ "Spec.Hash.Incremental.blake2_update_multi_associate_eq1", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "b2t_def", "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", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U128@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.Seq.Properties.split", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_076defedcc784372ac2411e8a227ef46", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_4ceb21009547645f163efe2223c6ebcb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U64@tok", "unit_typing" ], 0, "9b35f00e4e42f5cb65b28822ffb06712" ], [ "Spec.Hash.Incremental.repeati_blake2_update1_is_update_multi_aux", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "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", "refinement_interpretation_Tm_refine_076defedcc784372ac2411e8a227ef46", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "typing_Spec.Hash.Definitions.extra_state_int_type", "unit_typing" ], 0, "0b0be840ea0d6905d9a3ecbdfa094d12" ], [ "Spec.Hash.Incremental.repeati_blake2_update1_is_update_multi_aux", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "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", "refinement_interpretation_Tm_refine_076defedcc784372ac2411e8a227ef46", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "typing_Spec.Hash.Definitions.extra_state_int_type", "unit_typing" ], 0, "4fe2cf638baa709aa7615a037a24455b" ], [ "Spec.Hash.Incremental.repeati_blake2_update1_is_update_multi_aux", 3, 1, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "binder_x_6e097ef851a9e5e4d94613887cb6e84c_0", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_c230bc14f5b76230f719e4273030cc0c_3", "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.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_block", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Spec.Agile.Hash.update", "equation_Spec.Blake2.blake2_update1", "equation_Spec.Blake2.get_blocki", "equation_Spec.Blake2.limb_t", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.nat_to_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.bytes_block", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Spec.Agile.Hash.update", "int_inversion", "int_typing", "interpretation_Tm_abs_0a22db5cb809bc71916ebf6a3b18cd56", "interpretation_Tm_abs_e3e4e6e500ae76ff6ad28ada6503a771", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "lemma_Spec.Hash.Lemmas.update_multi_update", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "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_017f92a89265e68b0b873cddf703b02d", "refinement_interpretation_Tm_refine_076defedcc784372ac2411e8a227ef46", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_23d9c37b01d6158fcfa6197588fa0e41", "refinement_interpretation_Tm_refine_2c24ef93ea8f4fd62f66f6f456e5713c", "refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_80c81b6f576b5df50b0d5422474506ba", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.nat_to_limb", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.wt", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Spec.Hash.Definitions.Blake2B@tok", "typing_tok_Spec.Hash.Definitions.Blake2S@tok", "unit_typing", "well-founded-ordering-on-nat" ], 0, "9dea826e94678ec05783701e4f324f99" ], [ "Spec.Hash.Incremental.repeati_blake2_update1_is_update_multi", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "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", "refinement_interpretation_Tm_refine_076defedcc784372ac2411e8a227ef46", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "typing_Spec.Hash.Definitions.extra_state_int_type", "unit_typing" ], 0, "fd0811d006a9cfdcb5f40cfed56998c3" ], [ "Spec.Hash.Incremental.blake2_state_types_equalities", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "disc_equation_Spec.Hash.Definitions.Blake2B", "disc_equation_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Prims.nat", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.Blake2.wt", "typing_Spec.Hash.Definitions.uu___is_Blake2B", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok" ], 0, "bcff13caa2ed412149d7a6efc303cd0c" ], [ "Spec.Hash.Incremental.extra_state_v_nat_to_extra_state_is_id", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.nat_to_extra_state", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "lemma_Lib.IntTypes.v_mk_int", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "unit_typing" ], 0, "0a5813a8097898ae4dea9a44c10438d7" ], [ "Spec.Hash.Incremental.blake2'", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@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_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.blake2", "equation_Spec.Blake2.blake2_update", "equation_Spec.Blake2.blake2_update_blocks", "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.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_blake_alg", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "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_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "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.split", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "397339299852b878b4c8b400c76fa2eb" ], [ "Spec.Hash.Incremental.blake2_hash_incremental'", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Incremental.blake2_hash_incremental", "equation_Spec.Hash.Incremental.blake2_init", "equation_Spec.Hash.Incremental.hash_incremental_body", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.is_blake", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "bdd6d789caaf812330506c9e2528c3f1" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux1", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "constructor_distinct_Lib.IntTypes.S16", "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.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "a91a443c9aca3a5869d4ac2c29eafb00" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux1", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.Blake2.compute_prev0", "equation_Spec.Blake2.ivTable", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.pub_word_t", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.init_t", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.nat_to_extra_state", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Incremental.blake2_init", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective", "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_17b5c82e827d21e595c1a46cf8137822", "refinement_interpretation_Tm_refine_21d1498522ebc385ccedc0382e85c06e", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.u128", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_Spec.Blake2.ivTable", "typing_Spec.Blake2.max_output", "typing_Spec.Blake2.pub_word_t", "typing_Spec.Blake2.size_block", "typing_Spec.Blake2.size_block_w", "typing_Spec.Blake2.size_word", "typing_Spec.Blake2.wt", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Incremental.blake2_init", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "cf0763aff76d57d064075f7853867bcf" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U128@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Spec.Blake2.split", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "c411dbcecb2a17d50e3b48224ce6dde8" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U128@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Incremental.split_blocks", "function_token_typing_Lib.IntTypes.uint8", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Spec.Blake2.split", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "d56db54d61e7f174ca4c66317e737dd3" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux3", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U128@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.size_word", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Incremental.split_blocks", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "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_19daddf86323ca762702438524546abe", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_cc936e5a549dcdc2e3f9713145143490", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.maxint", "typing_Lib.UpdateMulti.split_at_last_lazy", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Spec.Blake2.split", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.max_input_length", "typing_Spec.Hash.Definitions.to_blake_alg", "unit_typing" ], 0, "c54375f7f0dfe3aeef3cc984dacd088e" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux3", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "equality_tok_Lib.IntTypes.U128@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.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.uint8", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Agile.Hash.update_multi", "equation_Spec.Blake2.blake2_update_last", "equation_Spec.Blake2.block_s", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.size_block_w", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Incremental.last_split_blake", "equation_Spec.Hash.Incremental.split_blocks", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.Incremental.update_last_blake", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__1", "projection_inverse_FStar.Pervasives.Native.Mktuple3__2", "projection_inverse_FStar.Pervasives.Native.Mktuple3__3", "refinement_interpretation_Tm_refine_3012f1d35c5c0da20fe268338b44903b", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_6ea94f8752d20755f3d2f50e2c16714f", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.empty", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Incremental.last_split_blake", "unit_typing" ], 0, "332bfa30ccfc1514e91dcd7dd477b191" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux4", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "constructor_distinct_Spec.Hash.Definitions.Blake2B", "constructor_distinct_Spec.Hash.Definitions.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "equation_Spec.Hash.Definitions.row", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_21d1498522ebc385ccedc0382e85c06e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Spec.Blake2.max_key", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.max_extra_state", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "9f1080fbda18c5b6c13b4d5dd57dd499" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental_aux4", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_FStar.Pervasives.Native.fst", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.finish_blake", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "typing_Spec.Hash.Definitions.is_blake" ], 0, "4b174b72ef673d9085033998a23c0f35" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_blake_alg", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "ed1e90d90146f21bd3c4a0db4a0fca3a" ], [ "Spec.Hash.Incremental.blake2_is_hash_incremental", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "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", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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.blake2", "equation_Spec.Blake2.blake2_update", "equation_Spec.Blake2.blake2_update_blocks", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output", "equation_Spec.Blake2.size_block", "equation_Spec.Blake2.split", "equation_Spec.Blake2.wt", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Incremental.blake2_hash_incremental", "equation_Spec.Hash.Incremental.hash_incremental_body", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Incremental.blake2_hash_incremental", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "aadbf6d0fb1c801c8b3b56c02448f7b2" ], [ "Spec.Hash.Incremental.md_is_hash_incremental", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.UpdateMulti.split_at_last_lazy", "equation_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.uint8", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Incremental.pad", "equation_Spec.Hash.Incremental.split_blocks", "equation_Spec.Hash.Incremental.update_last", "equation_Spec.Hash.PadFinish.pad", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_c0dc9cef58c290502a74bf3c80bf85bc", "refinement_interpretation_Tm_refine_cc936e5a549dcdc2e3f9713145143490", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_ee39f9357cbd63bb5cf348fb8515eff7", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_Lib.UpdateMulti.split_at_last_lazy", "typing_Lib.UpdateMulti.split_at_last_lazy_nb_rem", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_md", "typing_Spec.Hash.Definitions.word_length" ], 0, "98d08bfa764b0913cfd6c05d2e2793a8" ], [ "Spec.Hash.Incremental.blake2_hash_incremental_no_key_eq", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Spec.Blake2.alg", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Agile.Hash.init", "equation_Spec.Blake2.compute_prev0", "equation_Spec.Blake2.max_key", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Incremental.blake2_hash_incremental", "equation_Spec.Hash.Incremental.blake2_init", "equation_Spec.Hash.Incremental.hash_incremental", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_refl", "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_b3e3751c3894f166dfde09b500dd73a6", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Blake2.compute_prev0", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.to_blake_alg", "typing_Spec.Hash.Incremental.hash_incremental", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Blake2.Blake2S@tok", "unit_typing" ], 0, "6d2b6899b3d8bb8f2317258ddb139f5d" ], [ "Spec.Hash.Incremental.hash_is_hash_incremental", 1, 0, 0, [ "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0" ], 0, "a95186f927faf8fc79fcbd6c0d84a679" ], [ "Spec.Hash.Incremental.hash_is_hash_incremental", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Blake2.Blake2B", "constructor_distinct_Spec.Blake2.Blake2S", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Blake2.Blake2B@tok", "equality_tok_Spec.Blake2.Blake2S@tok", "equation_FStar.Seq.Base.op_At_Bar", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Agile.Hash.hash", "equation_Spec.Agile.Hash.init", "equation_Spec.Blake2.blake2", "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.size_block_w", "equation_Spec.Hash.Definitions.blake_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.init_t", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.to_blake_alg", "equation_Spec.Hash.Incremental.blake2_hash_incremental", "equation_Spec.Hash.Incremental.hash", "equation_Spec.Hash.Incremental.hash_incremental", "equation_Spec.Hash.Incremental.hash_incremental_body", "equation_Spec.Hash.Incremental.pad", "equation_Spec.Hash.PadFinish.pad", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_21d1498522ebc385ccedc0382e85c06e", "refinement_interpretation_Tm_refine_3f933d53eea19c88c15bd068de7d471e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929", "refinement_interpretation_Tm_refine_b3e3751c3894f166dfde09b500dd73a6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Blake2.size_block_w", "typing_Spec.Hash.Definitions.is_md", "typing_Spec.Hash.Definitions.max_input_length", "typing_Spec.Hash.Incremental.blake2_init", "typing_Spec.Hash.Incremental.hash", "typing_Spec.Hash.Incremental.hash_incremental", "typing_Spec.Hash.Incremental.hash_incremental_body", "typing_Spec.Hash.PadFinish.finish", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "15ec234f5e897e1d544a6cc9c85493be" ] ] ]