[ "ÖN=h¿\u000f•<[ýFÁygËé", [ [ "Spec.SHA2.size_k_w", 1, 2, 1, [ "@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, "b7bc1a0c249e9a69470bb11a9beb359f" ], [ "Spec.SHA2.word_n", 1, 2, 1, [ "@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, "a59ee5fd25d5ab11d225c71b0445b59b" ], [ "Spec.SHA2.to_word", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.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_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", "equation_Spec.SHA2.word_n", "int_inversion", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_27680283e93f30a8d9ac7d3b22ec31bf", "refinement_interpretation_Tm_refine_4ba48e342440e3210d8dbddb1d5a38f9", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_59c6c389f7d2ec9ac28044f709e4c7d6", "typing_Spec.SHA2.word_n" ], 0, "b47792655cbba98a50bd8faaf091cb67" ], [ "Spec.SHA2.v'", 1, 2, 1, [ "@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, "2bd4318f35be91f04c191dba0279114c" ], [ "Spec.SHA2.k_w", 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, "07c5256415edc6e5795a3672b036730d" ], [ "Spec.SHA2.ops", 1, 2, 1, [ "@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, "bdbfc52aa0b1001efe9a8a4f7210dc95" ], [ "Spec.SHA2.op0", 1, 2, 1, [ "@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, "bdf5ae0c89d7b7279008d478c226897e" ], [ "Spec.SHA2.op_Plus_Dot", 1, 2, 1, [ "@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, "0b7550fda2425f39eaf64c323edeb90c" ], [ "Spec.SHA2.op_Hat_Dot", 1, 2, 1, [ "@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, "d147a6a6aa66b409160bdefbc3821a2f" ], [ "Spec.SHA2.op_Amp_Dot", 1, 2, 1, [ "@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, "47409b28f3b07b149ea229414f86af6b" ], [ "Spec.SHA2.op_Tilde_Dot", 1, 2, 1, [ "@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, "61934704b1480fff6be02d8a47c61424" ], [ "Spec.SHA2.op_Greater_Greater_Greater_Dot", 1, 2, 1, [ "@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, "07d99ad1828b4adfc9e5a7724fb4109f" ], [ "Spec.SHA2.op_Greater_Greater_Dot", 1, 2, 1, [ "@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, "1ad957b7e4980ea9934178d1d2b3b6c2" ], [ "Spec.SHA2._Sigma0", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "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", "equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512", "fuel_guarded_inversion_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_Spec.SHA2.Mkops_c0", "proj_equation_Spec.SHA2.Mkops_c1", "proj_equation_Spec.SHA2.Mkops_c2", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.SHA2.Mkops_c0", "projection_inverse_Spec.SHA2.Mkops_c1", "projection_inverse_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_Lib.IntTypes.bits", "typing_Lib.IntTypes.pub_int_v", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.__proj__Mkops__item__c0", "typing_Spec.SHA2.op0", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8be72ab395dec747cee59da4da83a42b" ], [ "Spec.SHA2._Sigma1", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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_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", "equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512", "fuel_guarded_inversion_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_Spec.SHA2.Mkops_c3", "proj_equation_Spec.SHA2.Mkops_c4", "proj_equation_Spec.SHA2.Mkops_c5", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.SHA2.Mkops_c3", "projection_inverse_Spec.SHA2.Mkops_c4", "projection_inverse_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_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.__proj__Mkops__item__c3", "typing_Spec.SHA2.op0", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c6f9a57169eeb220c8e709678ee0c950" ], [ "Spec.SHA2._sigma0", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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_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", "equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512", "fuel_guarded_inversion_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_Spec.SHA2.Mkops_e0", "proj_equation_Spec.SHA2.Mkops_e1", "proj_equation_Spec.SHA2.Mkops_e2", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.SHA2.Mkops_e0", "projection_inverse_Spec.SHA2.Mkops_e1", "projection_inverse_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_Lib.IntTypes.bits", "typing_Lib.IntTypes.pub_int_v", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.__proj__Mkops__item__e0", "typing_Spec.SHA2.__proj__Mkops__item__e1", "typing_Spec.SHA2.op0", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6259f1bd7db8d7d35d14479a2e8d6f0e" ], [ "Spec.SHA2._sigma1", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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_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", "equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512", "fuel_guarded_inversion_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_Spec.SHA2.Mkops_e3", "proj_equation_Spec.SHA2.Mkops_e4", "proj_equation_Spec.SHA2.Mkops_e5", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.SHA2.Mkops_e3", "projection_inverse_Spec.SHA2.Mkops_e4", "projection_inverse_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_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.__proj__Mkops__item__e3", "typing_Spec.SHA2.op0", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "37c65d01ced04626a633f0d36c3470b9" ], [ "Spec.SHA2.h0", 1, 2, 1, [ "@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, "fcb45024bb7e0dda32407bf3ffa8c8c5" ], [ "Spec.SHA2.k0", 1, 2, 1, [ "@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_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", "equation_Spec.SHA2.size_k_w", "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, "76bd1aba8b749bc22b1b2044237d6dad" ], [ "Spec.SHA2.k0", 2, 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, "b643c73e99722214d0131516e65d1516" ], [ "Spec.SHA2.shuffle_core_pre_", 1, 2, 1, [ "@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_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_", "equation_Spec.SHA2.k0", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "typing_Spec.Hash.Definitions.state_word_length", "typing_Spec.SHA2.k0" ], 0, "dde739718186f1ee4adb48bdfe0add43" ], [ "Spec.SHA2.ws0_pre_inner", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.block_w", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_upd", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_1875d6a70d645dfbc67b7e1c62462fd5", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79", "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.size_k_w" ], 0, "75aed66d6f7cbbac417261186e10e5e2" ], [ "Spec.SHA2.wsi_pre_inner", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb", "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2._sigma0", "equation_Spec.SHA2._sigma1", "equation_Spec.SHA2.k_w", "function_token_typing_Spec.SHA2.op_Plus_Dot", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_9a60330ef1cdc4eb20371b8575ea05c8", "token_correspondence_Spec.SHA2.op_Plus_Dot", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2._sigma0", "typing_Spec.SHA2._sigma1" ], 0, "68f097353c5f01b15d76f3d6261c6acb" ], [ "Spec.SHA2.ws_pre_inner", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb", "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "bool_inversion", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2._sigma0", "equation_Spec.SHA2._sigma1", "equation_Spec.SHA2.block_w", "equation_Spec.SHA2.k_w", "function_token_typing_Spec.SHA2.op_Plus_Dot", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79", "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "token_correspondence_Spec.SHA2.op_Plus_Dot", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2._sigma0", "typing_Spec.SHA2._sigma1" ], 0, "9f81627e8048e4124f35601e68e104d4" ], [ "Spec.SHA2.ws_pre_", 1, 2, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.pos", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "lemma_FStar.Seq.Base.lemma_create_len", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.size_k_w", "typing_Spec.SHA2.word_n" ], 0, "2bad0a62011f19ced1eaead548cb54ac" ], [ "Spec.SHA2.shuffle_pre", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.SHA2.k_w", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "typing_Spec.SHA2.ws_pre" ], 0, "b92b1a5bb68ec4ec1add03c221ded6f3" ], [ "Spec.SHA2.init", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "unit_typing" ], 0, "2b55e59e6536d8bbe1be5256b74ab41b" ], [ "Spec.SHA2.update_pre", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "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.extra_state", "equation_Spec.Hash.Definitions.is_md", "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", "equation_Spec.Hash.Definitions.words_state_", "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_313945d6e5dd9a1523b4f94bb56574eb", "refinement_interpretation_Tm_refine_339ea6a10a02f04502a823137e2927cb", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_tok_Lib.IntTypes.U32@tok", "unit_typing" ], 0, "2ec6e8e0381230617d522ba093e46c33" ], [ "Spec.SHA2.finish", 1, 2, 1, [ "@query" ], 0, "3f4e2ed9cf4862f5939b1091d08c75d4" ] ] ]