[ "¥ïH\u0019\u001c*¬Bi®î\u0019Ö²Šù", [ [ "Spec.Hash.Lemmas.extra_state_add_nat_bound_lem1", 1, 2, 1, [ "@query", "equation_Spec.Hash.Definitions.max_extra_state" ], 0, "4142ea94f8803e0b0f90ea952bda6eea" ], [ "Spec.Hash.Lemmas.extra_state_add_nat_bound_lem1", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_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.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_add_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", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.extra_state_v", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.nat_to_extra_state", "typing_tok_Lib.IntTypes.SEC@tok", "unit_typing" ], 0, "6bef3f8ff2b37cd9ad4581e7695b117d" ], [ "Spec.Hash.Lemmas.extra_state_add_nat_bound_lem2", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Hash.Definitions.extra_state_v", "equation_Spec.Hash.Definitions.max_extra_state", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "typing_Spec.Hash.Definitions.extra_state_v" ], 0, "9b6ae2c6c05fd304cea373a98b60661f" ], [ "Spec.Hash.Lemmas.extra_state_add_nat_bound_lem2", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_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.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_add_nat", "equation_Spec.Hash.Definitions.extra_state_int_t", "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_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "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", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8a540bd64b8123f5d68c785aa9b43b6e", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.extra_state_v", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.nat_to_extra_state", "typing_tok_Lib.IntTypes.SEC@tok", "unit_typing" ], 0, "7f38f1f4202a350473d0954225170a88" ], [ "Spec.Hash.Lemmas.extra_state_add_nat_bound_associative_lem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.squash", "equation_Spec.Hash.Definitions.extra_state_int_type", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.max_extra_state", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_8a540bd64b8123f5d68c785aa9b43b6e", "typing_Spec.Hash.Definitions.is_blake" ], 0, "a2df09adc1f9e81f8d82a9e125351e42" ], [ "Spec.Hash.Lemmas.extra_state_add_nat_bound_associative_lem", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_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.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.extra_state_add_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", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "int_typing", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_028e3d676128c000131df62014b3d4df", "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe", "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8a540bd64b8123f5d68c785aa9b43b6e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.extra_state_int_type", "typing_Spec.Hash.Definitions.is_blake", "typing_Spec.Hash.Definitions.nat_to_extra_state", "typing_tok_Lib.IntTypes.SEC@tok", "unit_typing" ], 0, "3efb5256179636c8fc295cb0e8093db7" ], [ "Spec.Hash.Lemmas.extra_state_v_of_nat", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "33e1d80a0bd3c3db67d65d0abc509526" ], [ "Spec.Hash.Lemmas.extra_state_v_of_nat", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.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.max_extra_state", "equation_Spec.Hash.Definitions.nat_to_extra_state", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "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_tok_Lib.IntTypes.SEC@tok", "unit_typing" ], 0, "326b86d46a4539b6cae23464cb55b79b" ], [ "Spec.Hash.Lemmas.update_multi_zero", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Agile.Hash.update_multi.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equation_Lib.IntTypes.uint8", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.bytes_blocks", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "equation_with_fuel_Spec.Agile.Hash.update_multi.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "lemma_FStar.Seq.Base.lemma_eq_refl", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "typing_FStar.Seq.Base.empty", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Hash.Definitions.word" ], 0, "8fc658f55329622e16ad344ec06fe100" ], [ "Spec.Hash.Lemmas.update_multi_zero", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equation_Lib.UpdateMulti.uint8", "equation_Spec.Agile.Hash.update_multi", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "lemma_FStar.Seq.Base.lemma_eq_refl", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "typing_Spec.Hash.Definitions.word" ], 0, "20521b3193f886f6caa8e1f30ca2c6ad" ], [ "Spec.Hash.Lemmas.update_multi_update", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Agile.Hash.update_multi.fuel_instrumented", "@fuel_irrelevance_Spec.Agile.Hash.update_multi.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Spec.Agile.Hash_interpretation_Tm_arrow_9511bb3e8dd03332bdc255a2a2621d89", "Spec.Hash.Definitions_interpretation_Tm_arrow_3919213edab5530de5a42c49ef9baf98", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Prims.nat", "equation_Spec.Agile.Hash.split_block", "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.bytes_blocks", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.update_t", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "equation_with_fuel_Spec.Agile.Hash.update_multi.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Spec.Agile.Hash.update", "function_token_typing_Spec.Hash.Definitions.bytes", "int_inversion", "int_typing", "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", "lemma_Spec.Hash.Lemmas.update_multi_zero", "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_17631fa6304dcc08d028bd475a6dd078", "refinement_interpretation_Tm_refine_313945d6e5dd9a1523b4f94bb56574eb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_ebbe1a59e053e4d4b1f1772994d3ca80", "refinement_interpretation_Tm_refine_f6dadb4c8e10be02eb074bcec501a1ef", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "token_correspondence_Spec.Agile.Hash.update", "typing_FStar.Pervasives.Native.fst", "typing_FStar.Pervasives.Native.snd", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.split", "typing_Spec.Agile.Hash.split_block", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.bytes_blocks", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Spec.Hash.Definitions.MD5@tok", "typing_tok_Spec.Hash.Definitions.SHA1@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "036b2ed185567cc818b80d9addf0fcf1" ], [ "Spec.Hash.Lemmas.update_multi_update", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Lib.UpdateMulti.mk_update_multi.fuel_instrumented", "@query", "Lib.UpdateMulti_interpretation_Tm_arrow_23d5b1b5e5441ffc6b0ba8ce7ff0c3fc", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Spec.Agile.Hash_interpretation_Tm_arrow_9511bb3e8dd03332bdc255a2a2621d89", "Spec.Hash.Definitions_interpretation_Tm_arrow_3919213edab5530de5a42c49ef9baf98", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equation_FStar.Seq.Properties.split", "equation_Lib.IntTypes.uint8", "equation_Lib.UpdateMulti.split_block", "equation_Lib.UpdateMulti.uint8", "equation_Lib.UpdateMulti.update_t", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Agile.Hash.update_multi", "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.bytes_blocks", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.update_t", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "equation_with_fuel_Lib.UpdateMulti.mk_update_multi.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Spec.Agile.Hash.update", "function_token_typing_Spec.Hash.Definitions.bytes", "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", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "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", "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_313945d6e5dd9a1523b4f94bb56574eb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_70f8b36d78828a6fbb0eac5c69e65780", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "refinement_interpretation_Tm_refine_f7e332b8c9e9b78491d05e5af2a4a2de", "token_correspondence_Spec.Agile.Hash.update", "typing_FStar.Pervasives.Native.fst", "typing_FStar.Pervasives.Native.snd", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Lib.UpdateMulti.split_block", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.words_state" ], 0, "e2ff6a59ad692e7cdfee9867ab16da84" ], [ "Spec.Hash.Lemmas.update_multi_associative", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equation_Lib.IntTypes.uint8", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.bytes_blocks", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004" ], 0, "544758fbc9a988a94230fa94a15ff80f" ], [ "Spec.Hash.Lemmas.update_multi_associative", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equation_Lib.IntTypes.uint8", "equation_Lib.UpdateMulti.uint8", "equation_Spec.Agile.Hash.update_multi", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.bytes_blocks", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Lib.IntTypes.uint8", "lemma_FStar.Seq.Base.lemma_eq_refl", "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_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_f7a8f8340b3c54b659acfc982cbf3004", "typing_Spec.Agile.Hash.update_multi", "typing_Spec.Hash.Definitions.word" ], 0, "7e9b976f1c3a456d481fbc45cc3477cd" ], [ "Spec.Hash.Lemmas.block_length_smaller_than_max_input", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "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", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.word_length", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.block_length" ], 0, "8dcc3bf7f473b8ce7f7924ff5e3de429" ], [ "Spec.Hash.Lemmas.pad_invariant_block", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "ad4d82411547b5acd5d8c4b744967a2e" ], [ "Spec.Hash.Lemmas.pad_invariant_block", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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_Spec.Hash.Definitions.Blake2B@tok", "equality_tok_Spec.Hash.Definitions.Blake2S@tok", "equation_Prims.eqtype", "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.len_length", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_3954700d582549787d10a279872ff55c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.uu___is_Blake2S", "typing_Spec.Hash.Definitions.word_length" ], 0, "e70c644569315e2db5efd8062536d315" ], [ "Spec.Hash.Lemmas.max_input_size_len", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Spec.Hash.Definitions.len_length", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "typing_Spec.Hash.Definitions.len_length" ], 0, "edefcb3817a413c7722191c1185458f7" ], [ "Spec.Hash.Lemmas.max_input_size_len", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Spec.Hash.Definitions.MD5", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "disc_equation_Spec.Hash.Definitions.MD5", "disc_equation_Spec.Hash.Definitions.SHA1", "disc_equation_Spec.Hash.Definitions.SHA2_224", "disc_equation_Spec.Hash.Definitions.SHA2_256", "disc_equation_Spec.Hash.Definitions.SHA2_384", "disc_equation_Spec.Hash.Definitions.SHA2_512", "equality_tok_Spec.Hash.Definitions.MD5@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.max_input_length", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "8edc9efa920f3e01bbcfc82ed49b0b16" ], [ "Spec.Hash.Lemmas.pad_length", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_md", "typing_Spec.Hash.Definitions.len_length" ], 0, "15ebe196b4cb16f8d628d041dc91bf7f" ] ] ]