[ "¾ø\rƒLÀm® T¼˜j\u0002è\u001d", [ [ "Hacl.Spec.SHA2.size_k_w", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "f43ecba4b811ed425a42378a7b2487a3" ], [ "Hacl.Spec.SHA2.word_n", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "a8b55ea5cf6ac48051b72df064e324d4" ], [ "Hacl.Spec.SHA2.to_word", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.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.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "constructor_distinct_Tm_unit", "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_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@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_Hacl.Spec.SHA2.word_n", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "int_inversion", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_08e1ab035bd0aa023855913e2a882bda", "refinement_interpretation_Tm_refine_27680283e93f30a8d9ac7d3b22ec31bf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_59c6c389f7d2ec9ac28044f709e4c7d6", "typing_Hacl.Spec.SHA2.word_n" ], 0, "c5dae9fb34b85f0fa92ecbf9ac40571a" ], [ "Hacl.Spec.SHA2.v'", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@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_Lib.IntTypes.unsigned", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "da532267b06c51f4be6621446beb1e59" ], [ "Hacl.Spec.SHA2.num_rounds16", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "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.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.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_Hacl.Spec.SHA2.size_k_w", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "254690f074f37702d88f44d9756e55e7" ], [ "Hacl.Spec.SHA2.k_w", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "19668b2bc3d359d3e47c1f7f466b47fc" ], [ "Hacl.Spec.SHA2.block_t", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fad9177ebc905955d16a68dfaaadde6a" ], [ "Hacl.Spec.SHA2.ops", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Prims.eqtype", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.UInt32.t" ], 0, "6798e5e56b9238132439725cd1267a6b" ], [ "Hacl.Spec.SHA2.op0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "43fbec2a41a04a323b62eccd04841ab7" ], [ "Hacl.Spec.SHA2.op_Plus_Dot", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@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_Lib.IntTypes.unsigned", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "34566577d4dbf2a646472b9dae42358a" ], [ "Hacl.Spec.SHA2.op_Hat_Dot", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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.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_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "c89ca4e4fd6cccef28644552b97f786b" ], [ "Hacl.Spec.SHA2.op_Amp_Dot", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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.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_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "844847108534f621848ae8d2473fc448" ], [ "Hacl.Spec.SHA2.op_Tilde_Dot", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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.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_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "063451094dee0ffb0eaba586732e2de0" ], [ "Hacl.Spec.SHA2.op_Greater_Greater_Greater_Dot", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@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_Lib.IntTypes.unsigned", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "a15238f40a2b41c10a2b34defc06c870" ], [ "Hacl.Spec.SHA2.op_Greater_Greater_Dot", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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.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_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "typing_Spec.Hash.Definitions.uu___is_SHA2_512" ], 0, "21362a4b26ad7fc246aaf86c9e5cd8c7" ], [ "Hacl.Spec.SHA2._Sigma0", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "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_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.SHA2.op0", "equation_Hacl.Spec.SHA2.op224_256", "equation_Hacl.Spec.SHA2.op384_512", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Hacl.Spec.SHA2.ops", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Spec.SHA2.Mkops_c0", "proj_equation_Hacl.Spec.SHA2.Mkops_c1", "proj_equation_Hacl.Spec.SHA2.Mkops_c2", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Spec.SHA2.Mkops_c0", "projection_inverse_Hacl.Spec.SHA2.Mkops_c1", "projection_inverse_Hacl.Spec.SHA2.Mkops_c2", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.SHA2.__proj__Mkops__item__c0", "typing_Hacl.Spec.SHA2.op0", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "297e2d0ec0878e8e086f016257a4f6b7" ], [ "Hacl.Spec.SHA2._Sigma1", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "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_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.SHA2.op0", "equation_Hacl.Spec.SHA2.op224_256", "equation_Hacl.Spec.SHA2.op384_512", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Hacl.Spec.SHA2.ops", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Spec.SHA2.Mkops_c3", "proj_equation_Hacl.Spec.SHA2.Mkops_c4", "proj_equation_Hacl.Spec.SHA2.Mkops_c5", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Spec.SHA2.Mkops_c3", "projection_inverse_Hacl.Spec.SHA2.Mkops_c4", "projection_inverse_Hacl.Spec.SHA2.Mkops_c5", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.SHA2.__proj__Mkops__item__c3", "typing_Hacl.Spec.SHA2.op0", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "29176e55e69079019a322593222a4ffc" ], [ "Hacl.Spec.SHA2._sigma0", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "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_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.SHA2.op0", "equation_Hacl.Spec.SHA2.op224_256", "equation_Hacl.Spec.SHA2.op384_512", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Hacl.Spec.SHA2.ops", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Spec.SHA2.Mkops_e0", "proj_equation_Hacl.Spec.SHA2.Mkops_e1", "proj_equation_Hacl.Spec.SHA2.Mkops_e2", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Spec.SHA2.Mkops_e0", "projection_inverse_Hacl.Spec.SHA2.Mkops_e1", "projection_inverse_Hacl.Spec.SHA2.Mkops_e2", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.SHA2.__proj__Mkops__item__e0", "typing_Hacl.Spec.SHA2.__proj__Mkops__item__e1", "typing_Hacl.Spec.SHA2.op0", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.pub_int_v", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d2168d90f74f53801b15fd1044a83966" ], [ "Hacl.Spec.SHA2._sigma1", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "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_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.SHA2.op0", "equation_Hacl.Spec.SHA2.op224_256", "equation_Hacl.Spec.SHA2.op384_512", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_t", "fuel_guarded_inversion_Hacl.Spec.SHA2.ops", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Spec.SHA2.Mkops_e3", "proj_equation_Hacl.Spec.SHA2.Mkops_e4", "proj_equation_Hacl.Spec.SHA2.Mkops_e5", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Spec.SHA2.Mkops_e3", "projection_inverse_Hacl.Spec.SHA2.Mkops_e4", "projection_inverse_Hacl.Spec.SHA2.Mkops_e5", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.SHA2.__proj__Mkops__item__e3", "typing_Hacl.Spec.SHA2.op0", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "55ea7b635d5b20c8f9859b4ebf23adf1" ], [ "Hacl.Spec.SHA2.h0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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.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.List.Tot.Properties.llist", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.Constants.h224_l", "typing_Spec.SHA2.Constants.h256_l", "typing_Spec.SHA2.Constants.h384_l", "typing_Spec.SHA2.Constants.h512_l" ], 0, "4f16a061a826f0d78f189aee5154cd74" ], [ "Hacl.Spec.SHA2.k0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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.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.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.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.List.Tot.Properties.llist", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_fbb3412f12fd58a91571022d7c9fa36d", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.Constants.k224_256_l", "typing_Spec.SHA2.Constants.k384_512_l" ], 0, "b45e822021aa3e081c5e9d694bcf20ae" ], [ "Hacl.Spec.SHA2.k0", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "eebf6bb0ea31b8e40bf37bcb14ad0286" ], [ "Hacl.Spec.SHA2.shuffle_core_pre", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "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", "equation_Hacl.Spec.SHA2.k0", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.words_state_", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_1a99731d552df6be2792122fdcfba0e9", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "typing_Hacl.Spec.SHA2.k0", "typing_Spec.Hash.Definitions.state_word_length" ], 0, "00d454688ef873e148eff1e0913058d9" ], [ "Hacl.Spec.SHA2.ws_next_inner", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Hacl.Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb", "Hacl.Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "equation_Hacl.Spec.SHA2._sigma0", "equation_Hacl.Spec.SHA2._sigma1", "equation_Hacl.Spec.SHA2.k_w", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "function_token_typing_Hacl.Spec.SHA2.op_Plus_Dot", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "token_correspondence_Hacl.Spec.SHA2.op_Plus_Dot", "typing_Hacl.Spec.SHA2._sigma0", "typing_Hacl.Spec.SHA2._sigma1", "typing_Spec.Hash.Definitions.word" ], 0, "1a5381dcc2b33933392f0a6ea0f3faa1" ], [ "Hacl.Spec.SHA2.shuffle_inner", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.k0", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_1a99731d552df6be2792122fdcfba0e9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.k0", "typing_Hacl.Spec.SHA2.num_rounds16" ], 0, "745d63c8abe3959a120b7b12b3e20b7f" ], [ "Hacl.Spec.SHA2.shuffle", 1, 0, 0, [ "@query" ], 0, "bc7f2cde2c5fc427fe145ee43490b583" ], [ "Hacl.Spec.SHA2.update", 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", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.SHA2.block_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state_", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_80f22d3fb8b5e3f33bc412610fac0496", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "098d952bc1377ba302109cbb2654ab44" ], [ "Hacl.Spec.SHA2.load_last", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.sha2_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.len_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f552856778137967bbdbd4da25fe8163" ], [ "Hacl.Spec.SHA2.load_last", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "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_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "lemma_FStar.UInt.pow2_values", "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", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61f8c51489625e82187c8d6d3723b814", "refinement_interpretation_Tm_refine_733aa099fbdfad92c94850d0be6d76dc", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_828da124833a7b9ebf848df1eb46f9e8", "refinement_interpretation_Tm_refine_90af67ab52b0bbbd6188bde83a87bc86", "refinement_interpretation_Tm_refine_9a196537b9b1103a768f80802b7b0f4e", "refinement_interpretation_Tm_refine_9cf08ea3924cce0407272bab7df2f620", "refinement_interpretation_Tm_refine_c7b4f970846df875b13290cd9378bcf0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e63cb8889ebb0528c8520efdb69a8057", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "e3fa07b6c94001236758009b7dc38a4d" ], [ "Hacl.Spec.SHA2.update_last", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5ad9291d4c3f4bed94df2f88cfb60966" ], [ "Hacl.Spec.SHA2.update_last", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "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_Tm_unit", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.SHA2.padded_blocks", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.len_t", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.unsigned", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.state_word_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f6d359306ab6fa27121263341bd2a3ea" ], [ "Hacl.Spec.SHA2.store_state", 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_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.state_word_length", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "cc9146203402cbd89343244643243230" ], [ "Hacl.Spec.SHA2.emit", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c2dd360f9344a3b7676597121bd0bc33" ], [ "Hacl.Spec.SHA2.emit", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "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.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "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", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.hash_word_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e6153fea5d21a4b380649f5b81977bc0" ], [ "Hacl.Spec.SHA2.finish", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "9cbdc27909a364e72d6485a465fbaac1" ], [ "Hacl.Spec.SHA2.update_block", 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.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.word_length" ], 0, "75e1a80becac349cba307fd1b8104880" ], [ "Hacl.Spec.SHA2.update_block", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5eda2e166d6b590f3959f59d68af0750", "refinement_interpretation_Tm_refine_90af67ab52b0bbbd6188bde83a87bc86", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ef22bd4baeed9ab59be7f00116a2a250" ], [ "Hacl.Spec.SHA2.update_nblocks", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word_length" ], 0, "682fe7281e79edf6a8b8bb00f2ab9897" ], [ "Hacl.Spec.SHA2.hash", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.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_Lib.IntTypes.PUB", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f643b9a14ebfdd130ac3fa14e021f656", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@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, "23f6bed5f4dcaf490669688ef96bc3fd" ], [ "Hacl.Spec.SHA2.sha224", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equation_Spec.Hash.Definitions.is_sha2", "projection_inverse_BoxBool_proj_0" ], 0, "35b4befe4fca9ca72879043be2c8a25d" ], [ "Hacl.Spec.SHA2.sha256", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Spec.Hash.Definitions.is_sha2", "projection_inverse_BoxBool_proj_0" ], 0, "8d57320c9d6700bbbd8d41f62192c401" ], [ "Hacl.Spec.SHA2.sha384", 1, 0, 0, [ "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.Hash.Definitions.is_sha2", "projection_inverse_BoxBool_proj_0" ], 0, "98f1d304cacc6aebe49ed0bf6439ad89" ], [ "Hacl.Spec.SHA2.sha512", 1, 0, 0, [ "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.Hash.Definitions.is_sha2", "projection_inverse_BoxBool_proj_0" ], 0, "0f8d2677ed7d1761f95d8745899de7cc" ] ] ]