[ "Q\u0004iklb", [ [ "Hacl.Spec.SHA2.EquivScalar.ws_next_inductive", 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.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.SHA2.k_w", "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_word_length", "equation_Spec.Hash.Definitions.word", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0163fab25e441aa76fd7ec31747e1587", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_95b28de7543287865a5d7b1a18d8f285", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "43543fd6b7a37eca476a742a1bb06251" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_inductive", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Spec.SHA2.EquivScalar_interpretation_Tm_arrow_7809d76555abdf80039ac95187382069", "Hacl.Spec.SHA2_interpretation_Tm_arrow_d795079ea14bf8e3ed52cbae75fb12b8", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb", "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.SHA2._sigma0", "equation_Hacl.Spec.SHA2._sigma1", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.ws_next_inner", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_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", "function_token_typing_Hacl.Spec.SHA2.ws_next_inner", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0163fab25e441aa76fd7ec31747e1587", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_32686e835c2f30a50ba9e61179222d4c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_8440cbc64d44753251d8ba4f92177bc7", "refinement_interpretation_Tm_refine_8747729234fd12020d723f932edc56e3", "refinement_interpretation_Tm_refine_948f1414334cb680eb91b0d267e2e19c", "refinement_interpretation_Tm_refine_95b28de7543287865a5d7b1a18d8f285", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cc62286b275420c1e615dc14a3d3ef42", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ddf4ac79bc355a03bd1dcb81c2bd2c49", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "token_correspondence_Hacl.Spec.SHA2.op_Plus_Dot", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2._sigma0", "typing_Hacl.Spec.SHA2._sigma1", "typing_Hacl.Spec.SHA2.k_w", "typing_Lib.IntTypes.bits", "typing_Lib.LoopCombinators.repeati", "typing_Lib.Sequence.index", "typing_Spec.Hash.Definitions.word", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "cf29913eb183920aff4f1b8f5fe58fbe" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_lemma", 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.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.SHA2.k_w", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.word", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_95b28de7543287865a5d7b1a18d8f285", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "73c8755df867520bd4d64bafed9901d2" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.k_w", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01" ], 0, "b5dbcf26019f176478eb34bc085535f6" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_lemma_k", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Hacl.Spec.SHA2_interpretation_Tm_arrow_d795079ea14bf8e3ed52cbae75fb12b8", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "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.ws_next_inner", "int_inversion", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.k_w", "typing_Lib.LoopCombinators.repeati", "typing_Spec.Hash.Definitions.word" ], 0, "dfe3a1bc4c4536dbb84d6a86150d0655" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_lemma_k", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Spec.SHA2_interpretation_Tm_arrow_d795079ea14bf8e3ed52cbae75fb12b8", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.SHA2.k_w", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "function_token_typing_Hacl.Spec.SHA2.ws_next_inner", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cc62286b275420c1e615dc14a3d3ef42", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.k_w", "typing_Lib.IntTypes.bits", "typing_Lib.LoopCombinators.repeati", "typing_Lib.Sequence.index", "typing_Spec.Hash.Definitions.word", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6a2183eaaa549495931d8d2ca799ed01" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_inductive", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_3fd3f47329ef3febab1cd16885681be0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ccf5d02c93e056ec8ce3dc2d999b9f5d", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.size_k_w" ], 0, "801b156880eebf9579e560a37f4afb51" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_inductive", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Spec.SHA2.EquivScalar_interpretation_Tm_arrow_cc8956e247c5b271521a1c6df9134f54", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb", "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "Spec.SHA2_interpretation_Tm_arrow_fdace9edf5f9e55d5b7dd1ba248f0507", "bool_inversion", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "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", "equation_Spec.SHA2.size_k_w", "equation_Spec.SHA2.ws0_pre_inner", "equation_Spec.SHA2.ws_pre_inner", "equation_Spec.SHA2.wsi_pre_inner", "function_token_typing_Prims.int", "function_token_typing_Spec.SHA2.op_Plus_Dot", "function_token_typing_Spec.SHA2.ws_pre_inner", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "primitive_Prims.op_Addition", "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_32686e835c2f30a50ba9e61179222d4c", "refinement_interpretation_Tm_refine_3fd3f47329ef3febab1cd16885681be0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5af4edbfd61801799c2ead29f375d4c5", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d", "refinement_interpretation_Tm_refine_8747729234fd12020d723f932edc56e3", "refinement_interpretation_Tm_refine_94661465274e0e4f0e68ed0846a21af4", "refinement_interpretation_Tm_refine_948f1414334cb680eb91b0d267e2e19c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cc62286b275420c1e615dc14a3d3ef42", "refinement_interpretation_Tm_refine_ccf5d02c93e056ec8ce3dc2d999b9f5d", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "token_correspondence_Spec.SHA2.op_Plus_Dot", "typing_FStar.Seq.Base.index", "typing_Hacl.Spec.SHA2.word_n", "typing_Lib.LoopCombinators.repeati", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2._sigma0", "typing_Spec.SHA2._sigma1", "typing_Spec.SHA2.k_w", "typing_Spec.SHA2.size_k_w" ], 0, "92fec004487cab6f04a82902e3709609" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_3cf9e8e3b7bafc7071a1f0c2f4a65940", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ccf5d02c93e056ec8ce3dc2d999b9f5d", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.size_k_w" ], 0, "c5303a2d01f08476096611fcb359b95d" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "equation_Spec.SHA2.k_w", "refinement_interpretation_Tm_refine_3cf9e8e3b7bafc7071a1f0c2f4a65940", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "11f52269df4fbb3813c6da76551daf6e" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_lemma_k", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.size_k_w" ], 0, "1eff4fcf7c70f0818724ea0a30e0a8b7" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_lemma_k", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "refinement_interpretation_Tm_refine_cc62286b275420c1e615dc14a3d3ef42" ], 0, "ae1e5f07162a57f0e6685edc37cf1e4d" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_j_step", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.Sequence.lseq", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_41236447a80ff77bd69df3f1d69e2fd4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Hacl.Spec.SHA2.ws_next_inner", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "c0c864e7a98ea5fc333a6895978be708" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_j_step", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Spec.SHA2_interpretation_Tm_arrow_046d31b7ca1b5af90ba995ae3917b5cb", "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "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.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.SHA2._sigma0", "equation_Hacl.Spec.SHA2._sigma1", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.op0", "equation_Hacl.Spec.SHA2.op224_256", "equation_Hacl.Spec.SHA2.op384_512", "equation_Hacl.Spec.SHA2.op_Greater_Greater_Dot", "equation_Hacl.Spec.SHA2.op_Greater_Greater_Greater_Dot", "equation_Hacl.Spec.SHA2.op_Hat_Dot", "equation_Hacl.Spec.SHA2.op_Plus_Dot", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.ws_next_inner", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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", "equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.op_Greater_Greater_Dot", "equation_Spec.SHA2.op_Greater_Greater_Greater_Dot", "equation_Spec.SHA2.op_Hat_Dot", "equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.size_k_w", "equation_Spec.SHA2.ws_pre_inner", "equation_Spec.SHA2.wsi_pre_inner", "fuel_guarded_inversion_Hacl.Spec.SHA2.ops", "function_token_typing_Hacl.Spec.SHA2.op_Plus_Dot", "function_token_typing_Spec.SHA2.op_Plus_Dot", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "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", "proj_equation_Hacl.Spec.SHA2.Mkops_e3", "proj_equation_Hacl.Spec.SHA2.Mkops_e4", "proj_equation_Hacl.Spec.SHA2.Mkops_e5", "proj_equation_Spec.SHA2.Mkops_e0", "proj_equation_Spec.SHA2.Mkops_e1", "proj_equation_Spec.SHA2.Mkops_e2", "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_Hacl.Spec.SHA2.Mkops_e0", "projection_inverse_Hacl.Spec.SHA2.Mkops_e1", "projection_inverse_Hacl.Spec.SHA2.Mkops_e2", "projection_inverse_Hacl.Spec.SHA2.Mkops_e3", "projection_inverse_Hacl.Spec.SHA2.Mkops_e4", "projection_inverse_Hacl.Spec.SHA2.Mkops_e5", "projection_inverse_Spec.SHA2.Mkops_e0", "projection_inverse_Spec.SHA2.Mkops_e1", "projection_inverse_Spec.SHA2.Mkops_e2", "projection_inverse_Spec.SHA2.Mkops_e3", "projection_inverse_Spec.SHA2.Mkops_e4", "projection_inverse_Spec.SHA2.Mkops_e5", "refinement_interpretation_Tm_refine_0cd7f83675521de89d4e65258bd45229", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e94040f356066f968a194e5d3da356e6", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "token_correspondence_Hacl.Spec.SHA2.op_Greater_Greater_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Greater_Greater_Greater_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Hat_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Plus_Dot", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.logxor", "token_correspondence_Spec.SHA2.op_Greater_Greater_Dot", "token_correspondence_Spec.SHA2.op_Greater_Greater_Greater_Dot", "token_correspondence_Spec.SHA2.op_Hat_Dot", "token_correspondence_Spec.SHA2.op_Plus_Dot", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Hacl.Spec.SHA2.op0", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2._sigma0", "typing_Spec.SHA2._sigma1" ], 0, "98d6ea029d9485316ab8dc00e1e24ae8" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_aux", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_41236447a80ff77bd69df3f1d69e2fd4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_95b28de7543287865a5d7b1a18d8f285", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_da3dc06aa41442daee3741929cc462fb", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "a3b2b0c7338689f8b0de8d97836a1666" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_aux", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_02373d0ad758e7530f7026e5e6ae281b", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_41236447a80ff77bd69df3f1d69e2fd4", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_95b28de7543287865a5d7b1a18d8f285", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01", "refinement_interpretation_Tm_refine_aa506aefdeaf3cd9252f3163cc8f6e10", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_da3dc06aa41442daee3741929cc462fb", "refinement_interpretation_Tm_refine_dcce9750b41d651c1eeccaa99720a316", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "a05924bf51e51e34f6aa42750b3f1c32" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_init", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.word_n", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "02729ed88ec735c86d38066dd2516036" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_init", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.word_n", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_08e783220644947729829f198a559b97", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7a51da7fe5afc1830f1104f656c03726", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_9f3af2b4c130f519785ecadcb120ea01", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_da3dc06aa41442daee3741929cc462fb", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "eb579b8d915b060babd782a24e6070bd" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_j", 1, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.word_n", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0163fab25e441aa76fd7ec31747e1587", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7a51da7fe5afc1830f1104f656c03726", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "d7d98a559272cd8e8a68332d58aec86a" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_j", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.word_n", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7a51da7fe5afc1830f1104f656c03726", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_bb6fdfc4913f744a28e1a9e26e285cac", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Hacl.Spec.SHA2.word_n", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "7f517b9f7b9c214a4e95cc3dd710da0b" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma_j", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_43cbc836b30cca97f12ddcf34328194a_2", "binder_x_59b2d428076bb38589a6dedda766d453_0", "binder_x_7bc01e531ff45d409f14b50c8c434a8e_3", "binder_x_f3b82d8a229016ce22c360cbadda84ec_1", "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.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_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.min_int", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.word_n", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos", "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.block_w", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_quant_interp_a42ba772695c6cb4c706bfd0aa669de2", "l_quant_interp_c9c0c029e9c5b8416f33068b010f7fb8", "l_quant_interp_df811b7b5068a920bdaf53b30c5ba578", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "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_0163fab25e441aa76fd7ec31747e1587", "refinement_interpretation_Tm_refine_0e2b276ea20f97bff29c074cea411c82", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_259ef478d5d63cbf6a60b378c1c4fa27", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_553d6400dc47925a71c4734bc86b82d1", "refinement_interpretation_Tm_refine_581f28b47c8dc27d5d62d378c9ad8f5d", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b3b33cbb544eb242538faa823dac58f6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Hacl.Spec.SHA2.word_n", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_tok_Lib.IntTypes.U32@tok", "well-founded-ordering-on-nat" ], 0, "833b319ea41d61bd9b8b8ee4fca17a07" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_BoxInt", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.ws_next", "equation_Lib.Sequence.lseq", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5b19eb5d67186d7acedc1932ff15caee", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Hacl.Spec.SHA2.ws_next", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.ws_pre" ], 0, "922a54d871dd2bbc01fd21c74a336019" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_pre_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Spec.SHA2_interpretation_Tm_arrow_d795079ea14bf8e3ed52cbae75fb12b8", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.to_word", "equation_Hacl.Spec.SHA2.word_n", "equation_Hacl.Spec.SHA2.ws_next", "equation_Lib.Sequence.lseq", "equation_Prims.nat", "equation_Prims.pos", "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.block_w", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "equation_Spec.SHA2.to_word", "equation_Spec.SHA2.ws_pre_", "function_token_typing_Hacl.Spec.SHA2.ws_next_inner", "function_token_typing_Spec.SHA2.ws_pre", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2ad49ef16d542c30ebbb364e898f2790", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_40384ff54a4297cd01efd4362f27136f", "refinement_interpretation_Tm_refine_4444a3fcdb0b66c16dddc6b78f54c41e", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d851fffa8226ac0de9e58e5397e86fb9", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "refinement_interpretation_Tm_refine_f65d8e299e58e95f9ca8c541c0d3d552", "token_correspondence_Spec.SHA2.ws_pre_", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.k_w", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Hacl.Spec.SHA2.word_n", "typing_Lib.LoopCombinators.repeati", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "da8c13777a6bd87db63f7e3237917117" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_core_pre_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.SHA2._Ch", "equation_Hacl.Spec.SHA2._Maj", "equation_Hacl.Spec.SHA2._Sigma0", "equation_Hacl.Spec.SHA2._Sigma1", "equation_Hacl.Spec.SHA2.op0", "equation_Hacl.Spec.SHA2.op224_256", "equation_Hacl.Spec.SHA2.op384_512", "equation_Hacl.Spec.SHA2.op_Amp_Dot", "equation_Hacl.Spec.SHA2.op_Greater_Greater_Greater_Dot", "equation_Hacl.Spec.SHA2.op_Hat_Dot", "equation_Hacl.Spec.SHA2.op_Plus_Dot", "equation_Hacl.Spec.SHA2.op_Tilde_Dot", "equation_Hacl.Spec.SHA2.shuffle_core_pre", "equation_Spec.SHA2._Ch", "equation_Spec.SHA2._Maj", "equation_Spec.SHA2._Sigma0", "equation_Spec.SHA2._Sigma1", "equation_Spec.SHA2.op0", "equation_Spec.SHA2.op224_256", "equation_Spec.SHA2.op384_512", "equation_Spec.SHA2.op_Amp_Dot", "equation_Spec.SHA2.op_Greater_Greater_Greater_Dot", "equation_Spec.SHA2.op_Hat_Dot", "equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.op_Tilde_Dot", "equation_Spec.SHA2.shuffle_core_pre_", "fuel_guarded_inversion_Spec.SHA2.ops", "function_token_typing_Spec.SHA2.shuffle_core_pre", "proj_equation_Hacl.Spec.SHA2.Mkops_c0", "proj_equation_Hacl.Spec.SHA2.Mkops_c1", "proj_equation_Hacl.Spec.SHA2.Mkops_c2", "proj_equation_Hacl.Spec.SHA2.Mkops_c3", "proj_equation_Hacl.Spec.SHA2.Mkops_c4", "proj_equation_Hacl.Spec.SHA2.Mkops_c5", "proj_equation_Spec.SHA2.Mkops_c0", "proj_equation_Spec.SHA2.Mkops_c1", "proj_equation_Spec.SHA2.Mkops_c2", "proj_equation_Spec.SHA2.Mkops_c3", "proj_equation_Spec.SHA2.Mkops_c4", "proj_equation_Spec.SHA2.Mkops_c5", "projection_inverse_Hacl.Spec.SHA2.Mkops_c0", "projection_inverse_Hacl.Spec.SHA2.Mkops_c1", "projection_inverse_Hacl.Spec.SHA2.Mkops_c2", "projection_inverse_Hacl.Spec.SHA2.Mkops_c3", "projection_inverse_Hacl.Spec.SHA2.Mkops_c4", "projection_inverse_Hacl.Spec.SHA2.Mkops_c5", "projection_inverse_Spec.SHA2.Mkops_c0", "projection_inverse_Spec.SHA2.Mkops_c1", "projection_inverse_Spec.SHA2.Mkops_c2", "projection_inverse_Spec.SHA2.Mkops_c3", "projection_inverse_Spec.SHA2.Mkops_c4", "projection_inverse_Spec.SHA2.Mkops_c5", "token_correspondence_Hacl.Spec.SHA2.op_Amp_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Greater_Greater_Greater_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Hat_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Plus_Dot", "token_correspondence_Hacl.Spec.SHA2.op_Tilde_Dot", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.logxor", "token_correspondence_Spec.SHA2.op_Amp_Dot", "token_correspondence_Spec.SHA2.op_Greater_Greater_Greater_Dot", "token_correspondence_Spec.SHA2.op_Hat_Dot", "token_correspondence_Spec.SHA2.op_Plus_Dot", "token_correspondence_Spec.SHA2.op_Tilde_Dot", "token_correspondence_Spec.SHA2.shuffle_core_pre_", "typing_Spec.SHA2.op0" ], 0, "43e0b7086912b9c4df574774a3ae41a8" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_1a99731d552df6be2792122fdcfba0e9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_ea6ae5ef5319d82c13f8e384d7ff2e70" ], 0, "798144a723d853b7320574480383a3c2" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma", 1, 0, 0, [ "@query", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Spec.SHA2.size_k_w" ], 0, "734866e3f93bafb7f52594fafb9b5d54" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner", "equation_Hacl.Spec.SHA2.k0", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.SHA2.k0", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.shuffle_pre", "equation_Spec.SHA2.size_k_w", "function_token_typing_Prims.int", "function_token_typing_Spec.SHA2.shuffle", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "token_correspondence_Spec.SHA2.shuffle_pre", "typing_Spec.SHA2.ws_pre" ], 0, "ce3bbd180668324eb7d154b62ef98840" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner16", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_1a99731d552df6be2792122fdcfba0e9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.num_rounds16" ], 0, "5fe5f85d359fa9727e493316ca72b58e" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma16_step", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_BoxInt", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0163fab25e441aa76fd7ec31747e1587", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "typing_Hacl.Spec.SHA2.num_rounds16" ], 0, "adb4ddaab4b0765571ed7287b76b6aa6" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma16_step", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_BoxInt", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_b80e715dad3db0834b62fec792ed1cd5", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "typing_Hacl.Spec.SHA2.num_rounds16" ], 0, "10ca80267dba374465c38ec2028df36d" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma16_step", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_59b2d428076bb38589a6dedda766d453_0", "binder_x_674a051be9bc0087be75856c045027b6_3", "binder_x_7bc01e531ff45d409f14b50c8c434a8e_4", "binder_x_81d82b838c64d1cdf95c37a5564f7052_2", "bool_inversion", "equation_Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner", "equation_Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner16", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.LoopCombinators.fixed_a", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.SHA2.block_w", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0163fab25e441aa76fd7ec31747e1587", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9371691726d7981cba9ff6253d44db3c", "typing_Spec.Hash.Definitions.is_sha2", "well-founded-ordering-on-nat" ], 0, "ea4b21abfbb36f087cb9425ecae1de08" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma16", 1, 0, 0, [ "@query", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Spec.SHA2.size_k_w" ], 0, "2841de1fa04b0d838477f4492516313f" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_spec_lemma16", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner_num_rounds", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.LoopCombinators.fixed_a", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.SHA2.size_k_w", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "typing_Hacl.Spec.SHA2.num_rounds16" ], 0, "3e081a4afb1cb221fb482abaf77078ef" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_inner_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "261ade7dbe653baf91c27776f65bfc34" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_next_inner_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5ebb7b4e0b79add5a23fdbde32061012", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e8588f53cd4d564ec73ef0956d5a42d1", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "a7c4e9ddf8907dcbcb33f93f31dd7932" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma_i_step", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "087dd44fe475f5100149e34fa7209181" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma_i_step", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner16", "equation_Hacl.Spec.SHA2.EquivScalar.shuffle_pre_inner_num_rounds", "equation_Hacl.Spec.SHA2.k0", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.shuffle_inner", "equation_Hacl.Spec.SHA2.shuffle_inner_loop", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.Sequence.lseq", "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.Hash.Definitions.words_state", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_1a99731d552df6be2792122fdcfba0e9", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_cf52a5ae8fae81938a5fa8e10ed7c82d", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "typing_Hacl.Spec.SHA2.k0", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word" ], 0, "bc510680be282ebb20d11ea24105658a" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_init_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.SHA2.size_k_w" ], 0, "4ebb55323106a4c50640d2e9d1ee7126" ], [ "Hacl.Spec.SHA2.EquivScalar.ws_pre_init_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Hacl.Spec.SHA2.EquivScalar_interpretation_Tm_arrow_99c664de7b2e707cd81bce12116b7298", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "bool_inversion", "constructor_distinct_Tm_unit", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.to_word", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "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.k_w", "equation_Spec.SHA2.size_k_w", "equation_Spec.SHA2.to_word", "equation_Spec.SHA2.ws0_pre_inner", "equation_Spec.SHA2.ws_pre_", "equation_Spec.SHA2.ws_pre_inner", "function_token_typing_Spec.SHA2.ws_pre", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2acb4dc77c78d0653750adf5fb54664f", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_ab3a69019970fc78aca37d8553895fb7", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cc62286b275420c1e615dc14a3d3ef42", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f", "token_correspondence_Spec.SHA2.ws_pre_", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.word_n", "typing_Lib.LoopCombinators.repeati", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_Spec.SHA2.k_w", "typing_Spec.SHA2.size_k_w" ], 0, "d62127eff534fba167d5cba7f08394b3" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_bf55d6a8af772d39e7a5873d942878f3", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "df498842c507a2137b0185aaaa43df02" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma_i", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.SHA2.k_w", "equation_Spec.SHA2.size_k_w", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5902bf4059549da518a69da91ec4c3b9", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7aa74b9f65b69e8b4de33386e835b0ca", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2" ], 0, "f5ae7fa8a3da33c23e3e2376a3912372" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma_i", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_59b2d428076bb38589a6dedda766d453_0", "binder_x_e6333f24fbf8d73654638578d7a9fd45_3", "bool_inversion", "equation_Hacl.Spec.SHA2.k_w", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.shuffle_inner_loop", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Prims.nat", "equation_Prims.op_Equals_Equals_Equals", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.SHA2.size_k_w", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_8372f23900bd9353c103c4edac5ee0fa", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Spec.Hash.Definitions.is_sha2", "well-founded-ordering-on-nat" ], 0, "f620bd0b497b9fc0696d091c271fee98" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma", 1, 0, 0, [ "@query" ], 0, "96352ff52e8aa2b7bb46f41aa5bf616c" ], [ "Hacl.Spec.SHA2.EquivScalar.shuffle_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.shuffle", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "typing_Hacl.Spec.SHA2.num_rounds16" ], 0, "5c51c070f182849e7bc6a4281e96f5fe" ], [ "Hacl.Spec.SHA2.EquivScalar.update_lemma", 1, 0, 0, [ "@query" ], 0, "bed99722ed142e90c2be990019f55cbb" ], [ "Hacl.Spec.SHA2.EquivScalar.update_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "Spec.SHA2_interpretation_Tm_arrow_5114bb93a23375880e0690cfe93800b7", "bool_inversion", "constructor_distinct_BoxInt", "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", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.Pervasives.Native.fst", "equation_Hacl.Spec.SHA2.block_t", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.op_Plus_Dot", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.update", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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_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", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_of_bytes", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.Definitions.words_state_", "equation_Spec.SHA2.op_Plus_Dot", "equation_Spec.SHA2.update_pre", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Hacl.Spec.SHA2.op_Plus_Dot", "function_token_typing_Lib.ByteSequence.uints_from_bytes_be", "function_token_typing_Spec.SHA2.update_pre", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1104ef1656c24daae724b2b877eaf1e7", "refinement_interpretation_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3", "refinement_interpretation_Tm_refine_26d768cc241c6628db9e0d45d45d9136", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_516841552c075993547f605f17f21002", "refinement_interpretation_Tm_refine_51c7da0085e0591e8fc9d164195ec376", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_80f22d3fb8b5e3f33bc412610fac0496", "refinement_interpretation_Tm_refine_8335ed89c126d8fc7c7f79107e48cc1e", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e704e005f4ba5bb70e23bf9441a95af4", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Spec.Hash.Definitions.words_of_bytes", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Hacl.Spec.SHA2.op_Plus_Dot", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.int_t", "typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.unsigned", "typing_Lib.Sequence.index", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.state_word_length", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.word_t", "typing_Spec.Loops.seq_map2", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fc3f72c241e22ffe5ad85ce1a146d9c9" ], [ "Hacl.Spec.SHA2.EquivScalar.finish_lemma", 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, "0be8f2fd9c57183a543837ab2199f2ca" ], [ "Hacl.Spec.SHA2.EquivScalar.finish_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.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", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.SHA2.emit", "equation_Hacl.Spec.SHA2.finish", "equation_Hacl.Spec.SHA2.store_state", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.bytes_of_words", "equation_Spec.Hash.Definitions.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.is_blake", "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_", "equation_Spec.Hash.PadFinish.finish", "equation_Spec.Hash.PadFinish.finish_md", "function_token_typing_Lib.ByteSequence.uints_to_bytes_be", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim", "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", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "refinement_interpretation_Tm_refine_08e8ae4e9874469e13e0ccc3b3efe3d9", "refinement_interpretation_Tm_refine_0a8fff959e4db03b948fdfc445f2c5e5", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d", "refinement_interpretation_Tm_refine_33b41d60d11d9fc4d95661088bc6bd79", "refinement_interpretation_Tm_refine_34f6c60cf7598bc37a43b3fcbd1da9b2", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7", "refinement_interpretation_Tm_refine_848d46193a8b1b57b88b82ce6ff31c1a", "refinement_interpretation_Tm_refine_8eb78539847b038e152bb9bbd48a4c2d", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e78ecf464652a5ffd112c1b62bd9c25c", "token_correspondence_Spec.Hash.Definitions.bytes_of_words", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.finish", "typing_Hacl.Spec.SHA2.store_state", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index", "typing_Lib.Sequence.sub", "typing_Spec.Hash.Definitions.hash_length", "typing_Spec.Hash.Definitions.hash_word_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.word", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.PadFinish.finish", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "1568cdcc30f7000375d54db00d9b64e0" ], [ "Hacl.Spec.SHA2.EquivScalar.repeat_blocks_multi_extensionality", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "844c7181064b24b994eba43078f1f328" ], [ "Hacl.Spec.SHA2.EquivScalar.repeat_blocks_multi_extensionality", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "5a977be37a755f5dc4a6ed0208408dff" ], [ "Hacl.Spec.SHA2.EquivScalar.repeat_blocks_multi_extensionality", 3, 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_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ec36165acc8b3b8a1f151af217f53b8", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7af7abfd9fa791df66706ab563886df2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b14928a18ba707004108386997fed9d6", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.slice", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f1050b5517b197bec3581230d8ad8e5d" ], [ "Hacl.Spec.SHA2.EquivScalar.update_multi_is_repeat_blocks_multi", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_BoxInt", "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.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.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.len_length", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8a87b8a531982aadb85bf1f25e594833", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.pad_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f9b254472006117db488b1731fd2e873" ], [ "Hacl.Spec.SHA2.EquivScalar.update_multi_is_repeat_blocks_multi", 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.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.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.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "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_Modulus", "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.len_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "12fbb83a7eb80dfa37313b470659644e" ], [ "Hacl.Spec.SHA2.EquivScalar.update_multi_is_repeat_blocks_multi", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_BoxInt", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.Seq.Properties.split", "equation_Hacl.Spec.SHA2.block_t", "equation_Hacl.Spec.SHA2.num_rounds16", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.UpdateMulti.Lemmas.repeat_f", "equation_Lib.UpdateMulti.Lemmas.repeat_l", "equation_Lib.UpdateMulti.Lemmas.uint8", "equation_Lib.UpdateMulti.split_at_last", "equation_Lib.UpdateMulti.split_at_last_nb_rem", "equation_Lib.UpdateMulti.split_block", "equation_Lib.UpdateMulti.uint8", "equation_Lib.UpdateMulti.update_full", "equation_Prims.nat", "equation_Spec.Agile.Hash.update", "equation_Spec.Agile.Hash.update_multi", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "interpretation_Tm_abs_94fc6f12247c8a4eab9124e84c54677d", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_362e2dfd5fc10941f1049c892a15d4e9", "refinement_interpretation_Tm_refine_36fc4a3bd4656ab76ef7de64c5b7198c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7fc4e979700038338efb9b0ad24f2964", "refinement_interpretation_Tm_refine_8a87b8a531982aadb85bf1f25e594833", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "token_correspondence_Spec.SHA2.update", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.SHA2.num_rounds16", "typing_Lib.IntTypes.bits", "typing_Lib.UpdateMulti.split_at_last_nb_rem", "typing_Spec.Hash.Definitions.pad_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d11da88a882af9441a921087b1652d39" ], [ "Hacl.Spec.SHA2.EquivScalar.hash_is_repeat_blocks", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "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_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Tm_unit", "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_224@tok", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.nonzero", "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_int_type", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "int_inversion", "int_typing", "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_0766302b68bb44ab7aff8c4d8be0b46f", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "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_Lib.IntTypes.v", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "unit_typing" ], 0, "292a97a56abbdf74beadc026c0e54281" ], [ "Hacl.Spec.SHA2.EquivScalar.hash_is_repeat_blocks", 2, 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", "constructor_distinct_Tm_unit", "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_224@tok", "equation_Hacl.Spec.SHA2.size_k_w", "equation_Hacl.Spec.SHA2.update_block", "equation_Hacl.Spec.SHA2.update_nblocks", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "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.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "equation_Spec.Hash.Definitions.words_state", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5eda2e166d6b590f3959f59d68af0750", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "token_correspondence_Hacl.Spec.SHA2.update", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Hacl.Spec.SHA2.size_k_w", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.pub_int_v", "typing_Lib.IntTypes.unsigned", "typing_Lib.Sequence.sub", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.state_word_length", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok" ], 0, "c1a097ab89debbe4b61a78a624821106" ], [ "Hacl.Spec.SHA2.EquivScalar.append_pad_last_length_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U64", "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, "7ed98af354eb9d800b52c0306e0f486f" ], [ "Hacl.Spec.SHA2.EquivScalar.append_pad_last_length_lemma", 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_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "db9b89125c47a4cc9f147af6cac96ca8" ], [ "Hacl.Spec.SHA2.EquivScalar.load_last_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.SHA2.padded_blocks", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "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_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13184cdcb19c1210e66a39cd8fedab1d", "refinement_interpretation_Tm_refine_13dd9e386d95428bd2cd8f17083d5aef", "refinement_interpretation_Tm_refine_184554cfcf9d901f6b211090b7c6684c", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8bea2569a76f982f82f6df876009dbe0", "refinement_interpretation_Tm_refine_9cf08ea3924cce0407272bab7df2f620", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_eb32171c74bb02949aa6c90cfbac2b67", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "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, "2043a9a13e9b2db57ee64de4d1baf972" ], [ "Hacl.Spec.SHA2.EquivScalar.load_last_lemma", 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_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.len_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.len_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e57cf459307f3dd4df6d7502eb4b4d17" ], [ "Hacl.Spec.SHA2.EquivScalar.load_last_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.SHA2.padded_blocks", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_upd", "lemma_FStar.UInt.pow2_values", "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_0170f7a8a27a460a89ef296bf90acfb6", "refinement_interpretation_Tm_refine_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_13184cdcb19c1210e66a39cd8fedab1d", "refinement_interpretation_Tm_refine_13dd9e386d95428bd2cd8f17083d5aef", "refinement_interpretation_Tm_refine_184554cfcf9d901f6b211090b7c6684c", "refinement_interpretation_Tm_refine_1f6ebfac78c0ee6cd3cef4eabad0ae2a", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_25cc7eba771a815019173df66237bc49", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_415d9f15a679296ef4a273ce6085f29d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5a31b93ba3c7fad34bf5f4c94dc9e54e", "refinement_interpretation_Tm_refine_5ac6f98bcd0ced758b5cf7f315de84a0", "refinement_interpretation_Tm_refine_5c2773dc3463e059e4307cf88406a082", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_64007e4a8c187c3787ce4f8705e9db35", "refinement_interpretation_Tm_refine_669be302d36ca44361d06a8cf43c4c72", "refinement_interpretation_Tm_refine_6fe9ca868d1e366d0866c63f98ca5acf", "refinement_interpretation_Tm_refine_79c32e115485d4f587171105658bf0b5", "refinement_interpretation_Tm_refine_7cda7d570b8a3e5bfba11fe7fb17b7f9", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8578def5d198588272dc248df6e36e4f", "refinement_interpretation_Tm_refine_88eb6f21ed51186ae42a33e69169c215", "refinement_interpretation_Tm_refine_8bea2569a76f982f82f6df876009dbe0", "refinement_interpretation_Tm_refine_8da3af77db7388ea342e0779283cf0f6", "refinement_interpretation_Tm_refine_9cf08ea3924cce0407272bab7df2f620", "refinement_interpretation_Tm_refine_aaa4fb3d69432662b855529daee8cd7d", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_bb77e9f02ef87282d7b8f0e4ef1ab607", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c549aea81551ded2366b680fce3d08ef", "refinement_interpretation_Tm_refine_c8ae1054ef63db5ed455be90c31a6de4", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d6e75f1c361b0c36b809768447e3e80c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "refinement_interpretation_Tm_refine_e948f782b8bef1ae08c958d4a09e4049", "refinement_interpretation_Tm_refine_eb32171c74bb02949aa6c90cfbac2b67", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.upd", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.index", "typing_Lib.Sequence.length", "typing_Lib.Sequence.sub", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_length", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "1f1db59d46f5594b96708bc7b2422b9f" ], [ "Hacl.Spec.SHA2.EquivScalar.load_last_pad_lemma", 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.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_Lib.IntTypes.U8@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.numbytes", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_AmpAmp", "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_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61f8c51489625e82187c8d6d3723b814", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a196537b9b1103a768f80802b7b0f4e", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "e554486c9d0f8c1760501b31de71a94c" ], [ "Hacl.Spec.SHA2.EquivScalar.load_last_pad_lemma", 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, "9cb400f4ff769d77975faad495f3a331" ], [ "Hacl.Spec.SHA2.EquivScalar.load_last_pad_lemma", 3, 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.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.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_FStar.Seq.Base.op_At_Bar", "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.numbytes", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.nat_to_len", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.PadFinish.pad", "equation_Spec.Hash.PadFinish.pad_md", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_3", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_472487d41973f0cb61dae82d55c2306c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_61f8c51489625e82187c8d6d3723b814", "refinement_interpretation_Tm_refine_64007e4a8c187c3787ce4f8705e9db35", "refinement_interpretation_Tm_refine_669be302d36ca44361d06a8cf43c4c72", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_8578def5d198588272dc248df6e36e4f", "refinement_interpretation_Tm_refine_97a5396f3da9f68385628f7ed86fe69d", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.to_seq", "typing_Prims.pow2", "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.pad0_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok" ], 0, "c074eb1126f22eea60b4e1f82b66dcbc" ], [ "Hacl.Spec.SHA2.EquivScalar.update_last_lemma", 1, 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_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_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_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@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.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_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_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_0a319766f7b5a8764d7b48155798fe57", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13dd9e386d95428bd2cd8f17083d5aef", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8bea2569a76f982f82f6df876009dbe0", "refinement_interpretation_Tm_refine_9cf08ea3924cce0407272bab7df2f620", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_eb32171c74bb02949aa6c90cfbac2b67", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "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.max_input_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok" ], 0, "e482b26ec9f6ed33eb5ef3abd6351581" ], [ "Hacl.Spec.SHA2.EquivScalar.update_last_lemma", 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_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_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "93063666422f04a44e0def8d49948323" ], [ "Hacl.Spec.SHA2.EquivScalar.update_last_lemma", 3, 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.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", "constructor_distinct_Tm_unit", "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", "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.minint", "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.length", "equation_Lib.Sequence.lseq", "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_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.max_input_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.max_input_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7811d27ed72d9d5f9981a6b156299513" ], [ "Hacl.Spec.SHA2.EquivScalar.update_last_is_repeat_blocks_multi", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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.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.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.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.Seq.Base.op_At_Bar", "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.numbytes", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.nat_to_len", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.PadFinish.pad", "equation_Spec.Hash.PadFinish.pad_md", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_3", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_2182032b8ffb445c856acde128dfcc30", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f68b09e768068763d6aac8d1124307c0", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Lib.ByteSequence.uint_to_bytes_be", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Prims.pow2", "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.nat_to_len", "typing_Spec.Hash.Definitions.pad0_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "00ca1359c28f7d54f8d42ebf89bd736e" ], [ "Hacl.Spec.SHA2.EquivScalar.update_last_is_repeat_blocks_multi", 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_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_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.block_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e33db4f4f8ba18dfb177b18558b0db29" ], [ "Hacl.Spec.SHA2.EquivScalar.update_last_is_repeat_blocks_multi", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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.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.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.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.Seq.Base.op_At_Bar", "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.load_last", "equation_Hacl.Spec.SHA2.padded_blocks", "equation_Hacl.Spec.SHA2.update_last", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.nat_to_len", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.words_state", "equation_Spec.Hash.PadFinish.pad", "equation_Spec.Hash.PadFinish.pad_md", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_2182032b8ffb445c856acde128dfcc30", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_415d9f15a679296ef4a273ce6085f29d", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f68b09e768068763d6aac8d1124307c0", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "token_correspondence_Hacl.Spec.SHA2.update", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.ByteSequence.uint_to_bytes_be", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.length", "typing_Lib.Sequence.sub", "typing_Lib.Sequence.upd", "typing_Lib.Sequence.update_sub", "typing_Prims.pow2", "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.nat_to_len", "typing_Spec.Hash.Definitions.pad0_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "typing_tok_Spec.Hash.Definitions.SHA2_512@tok" ], 0, "282c0d5038022f942cc8d5d2d952952e" ], [ "Hacl.Spec.SHA2.EquivScalar.hash_is_repeat_blocks_multi", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Lib.IntTypes.inttype", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Hash.Definitions.SHA2_224", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Tm_unit", "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_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.state_word_length", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.Definitions.word_t", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "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.len_int_type", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.pad0_length", "typing_Spec.Hash.Definitions.word_length", "typing_Spec.Hash.Definitions.word_t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok", "typing_tok_Spec.Hash.Definitions.SHA2_384@tok", "unit_typing" ], 0, "82510044f7060622553b724d561f6d16" ], [ "Hacl.Spec.SHA2.EquivScalar.hash_is_repeat_blocks_multi", 2, 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", "disc_equation_Lib.IntTypes.PUB", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_FStar.Seq.Base.op_At_Bar", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.nat_to_len", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.PadFinish.pad", "equation_Spec.Hash.PadFinish.pad_md", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_1bb461a94f2222e653284809986676f4", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_2182032b8ffb445c856acde128dfcc30", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_45de79b9bfd92937f3e5de19a3ca97cf", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_923b1a2679a97ac121731e58ecb697a1", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a64745e6e14df49979dedf0304497607", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b3fcac59602bf14430ac809b452796d0", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_f68b09e768068763d6aac8d1124307c0", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Lib.ByteSequence.uint_to_bytes_be", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.secret", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.length", "typing_Prims.pow2", "typing_Spec.Hash.Definitions.is_sha2", "typing_Spec.Hash.Definitions.len_int_type", "typing_Spec.Hash.Definitions.len_length", "typing_Spec.Hash.Definitions.nat_to_len", "typing_Spec.Hash.Definitions.pad0_length", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok" ], 0, "025a10891ad5d5a207e1f5472a91ff8b" ], [ "Hacl.Spec.SHA2.EquivScalar.hash_agile_lemma", 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.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_Lib.Sequence.lseq", "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.word_length", "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_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6ea238080aa329fd65e4814adcbafa87" ], [ "Hacl.Spec.SHA2.EquivScalar.hash_agile_lemma", 2, 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.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", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_224@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_FStar.Seq.Base.op_At_Bar", "equation_Hacl.Spec.SHA2.h0", "equation_Hacl.Spec.SHA2.hash", "equation_Hacl.Spec.SHA2.init", "equation_Hacl.Spec.SHA2.padded_blocks", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.Agile.Hash.hash", "equation_Spec.Agile.Hash.init", "equation_Spec.Hash.Definitions.block_length", "equation_Spec.Hash.Definitions.block_word_length", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.extra_state", "equation_Spec.Hash.Definitions.is_blake", "equation_Spec.Hash.Definitions.is_md", "equation_Spec.Hash.Definitions.is_sha2", "equation_Spec.Hash.Definitions.len_int_type", "equation_Spec.Hash.Definitions.len_length", "equation_Spec.Hash.Definitions.nat_to_len", "equation_Spec.Hash.Definitions.pad0_length", "equation_Spec.Hash.Definitions.pad_length", "equation_Spec.Hash.Definitions.sha2_alg", "equation_Spec.Hash.Definitions.word_length", "equation_Spec.Hash.PadFinish.pad", "equation_Spec.Hash.PadFinish.pad_blake", "equation_Spec.Hash.PadFinish.pad_md", "equation_Spec.SHA2.h0", "equation_Spec.SHA2.init", "function_token_typing_Lib.IntTypes.uint8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05ae0d87aad3130bbdbf3feeebb31964", "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403", "refinement_interpretation_Tm_refine_2182032b8ffb445c856acde128dfcc30", "refinement_interpretation_Tm_refine_2c1f6dc1d378fed54224fbf63fca7a8a", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_850fe300f875565a60c2c1ce43a6fda4", "refinement_interpretation_Tm_refine_8a87b8a531982aadb85bf1f25e594833", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e", "refinement_interpretation_Tm_refine_f68b09e768068763d6aac8d1124307c0", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Lib.ByteSequence.uint_to_bytes_be", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.secret", "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.nat_to_len", "typing_Spec.Hash.Definitions.pad0_length", "typing_Spec.Hash.Definitions.pad_length", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Hash.Definitions.SHA2_224@tok", "typing_tok_Spec.Hash.Definitions.SHA2_256@tok" ], 0, "47ac3ee9aa50e5ecdb674f2c2a29eb50" ] ] ]