[ "l\t°GúYê­—Ü?E\"÷°)", [ [ "Hacl.Loops.Lemmas.repeati_extensionality", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Hacl.Loops.Lemmas_interpretation_Tm_arrow_e7e6bda13570450ba98cae3dc5e7dd42", "Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_6781041e5072f14a03af8b07643f1f30_4", "binder_x_b3a9ce008df0278184098b1a723bca0c_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "binder_x_fe28d8bcde588226b4e538b35321de05_0", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_3e839a4d245a3beb00e03b7402cb44c7", "refinement_interpretation_Tm_refine_49c0ba66edcf02816cc411af6df0f144", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.LoopCombinators.repeati", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "well-founded-ordering-on-nat" ], 0, "e94a6d35af1fc99dba47d9eab9198403" ], [ "Hacl.Loops.Lemmas.repeati_right_extensionality", 1, 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_54c3ba9c6cc0203b91208dbe209fe9b7", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "e4a659a4c15dfe747e69fd745b54f3af" ], [ "Hacl.Loops.Lemmas.repeati_right_extensionality", 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_54c3ba9c6cc0203b91208dbe209fe9b7", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "a887eb8deb13d83166371e72efcaa2b7" ], [ "Hacl.Loops.Lemmas.repeati_right_extensionality", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Properties_interpretation_Tm_arrow_67c7b2626869cb316f118144000415b9", "Hacl.Loops.Lemmas_interpretation_Tm_arrow_f715d9c45d58a4f120f57b15a310761a", "Lib.LoopCombinators_interpretation_Tm_arrow_2bf7345966baadb5d8656724dcf7cee8", "Lib.LoopCombinators_interpretation_Tm_arrow_36dd113ffd3258af3d2f33c53ef8eea6", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_a35d68fb210a5c8491a1fe21a78d90fe_4", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "binder_x_bcc2f6f9f4295168fb705265fe290244_5", "binder_x_e09860b75d8922ab497a3e5bc9347578_7", "binder_x_fe28d8bcde588226b4e538b35321de05_1", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.LoopCombinators.fixed_a", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.LoopCombinators.fixed_a", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_24e0f7a4ca49aa53202cb61b2d7edc7c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913", "refinement_interpretation_Tm_refine_622464fca245921c9ddd8551e6567101", "refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e6651b74fd10aa11130b6626c647d515", "refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795", "refinement_interpretation_Tm_refine_fb92f957c6718b5dce11e5cb4a82332e", "token_correspondence_Lib.LoopCombinators.fixed_a", "typing_Lib.IntTypes.minint", "typing_Lib.LoopCombinators.repeat_right", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok", "well-founded-ordering-on-nat" ], 0, "c2a4958d27d9680962fece1564381bf4" ], [ "Hacl.Loops.Lemmas.aux_repeat_bf_s0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_bb0b8197bb42e9a1aaebe59e97685233", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.minint", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "411cd128530b06ef45eed82c110bda59" ], [ "Hacl.Loops.Lemmas.aux_repeat_bf_s0", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "2579b31c0456252fc8971f2a7ba26c6e" ], [ "Hacl.Loops.Lemmas.aux_repeat_bf_s0", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_1c325641987cce6783228428bd15a869", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_bb0b8197bb42e9a1aaebe59e97685233", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "dba3384c99d3c56bb993f33badb206ec" ], [ "Hacl.Loops.Lemmas.lemma_aux", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "415c35a2508ae9d06f68566e48a91931" ], [ "Hacl.Loops.Lemmas.lemma_aux", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "133d6716d2f43b37b1bef3de6e8e7d52" ], [ "Hacl.Loops.Lemmas.lemma_aux2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "993fa765be52d58b10f7e54b017d59ec" ], [ "Hacl.Loops.Lemmas.lemma_aux2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "fb31d049e6117a08267e9161e1990e83" ], [ "Hacl.Loops.Lemmas.lemma_aux3", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "7d975069e8b23bf80d35f6ada0010de4" ], [ "Hacl.Loops.Lemmas.lemma_aux3", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "5793e20de903a2520962c3cb16cd0ec3" ], [ "Hacl.Loops.Lemmas.aux_repeat_bf_s1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_596ec1b41cf453090618f08b7bf62083", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "4ac77c4c9fb257cff28956fdf47632ea" ], [ "Hacl.Loops.Lemmas.aux_repeat_bf_s1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0016514bc646fd8bc0bf5498dd5d811d" ], [ "Hacl.Loops.Lemmas.aux_repeat_bf_s1", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_09378811719f1db9568e56774ba6685e", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_2aa4ee2b8fa3e2c3e461553307b0a540", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_596ec1b41cf453090618f08b7bf62083", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d43fb1fb72013127e4f322fb3f69445b" ], [ "Hacl.Loops.Lemmas.repeat_blocks_split12", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "3ef1b7283defdc56d263d37cc87af93d" ], [ "Hacl.Loops.Lemmas.repeat_blocks_split12", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "2de1669a070b1f7bbd48bc23a266bbee" ], [ "Hacl.Loops.Lemmas.repeat_blocks_split12", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_596ec1b41cf453090618f08b7bf62083", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "df2bbbcef8b0282037a59bc0d01c2ff4" ], [ "Hacl.Loops.Lemmas.lemma_aux4", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "71f49d59efe0dccbd2447eca24a19183" ], [ "Hacl.Loops.Lemmas.lemma_aux4", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "3747fa0cdbcd9c2ff7c3a3da7f104c75" ], [ "Hacl.Loops.Lemmas.repeat_blocks_multi_split", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "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_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5e9c3dad358c3890f342f5eeb42bb76e", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "ab7030acdbb8e34aa29789976340a53a" ], [ "Hacl.Loops.Lemmas.repeat_blocks_multi_split", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "f7ccb0077e1a855aa04e4af729b3b94a" ], [ "Hacl.Loops.Lemmas.repeat_blocks_multi_split", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5839670106941c7a52e93e3779e15dba", "refinement_interpretation_Tm_refine_5e9c3dad358c3890f342f5eeb42bb76e", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4b1ca6733c5d0fc55470b367f807406e" ], [ "Hacl.Loops.Lemmas.repeat_blocks_split", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "c81042496478da7307b83e5ba0562776" ], [ "Hacl.Loops.Lemmas.repeat_blocks_split", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "80cb27b758d919cb2e0154615d69fb84" ], [ "Hacl.Loops.Lemmas.repeat_blocks_split", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5839670106941c7a52e93e3779e15dba", "refinement_interpretation_Tm_refine_6040141db1ba33361776c6b54feae71f", "refinement_interpretation_Tm_refine_725406258cbec7cb7a61bee1d844d771", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4a53e6d3fbe980d070ae484007c53a32" ], [ "Hacl.Loops.Lemmas.repeat_w", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntVector.width", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "3ca7925d79100cb6f1808284fd86a781" ], [ "Hacl.Loops.Lemmas.unfold_repeatw", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181" ], 0, "01a5decdbe3efe897c7cdaa6796ecc88" ], [ "Hacl.Loops.Lemmas.unfold_repeatw", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Hacl.Loops.Lemmas.repeat_w", "equation_Lib.IntTypes.bits", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_2", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "0530032ecf48dd316796704cbf5863ea" ], [ "Hacl.Loops.Lemmas.lemma_repeati_vec", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntVector.width", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181" ], 0, "9960cccce23155528b4bd07af309ecd8" ], [ "Hacl.Loops.Lemmas.lemma_repeati_vec", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Loops.Lemmas.lanes", "equation_Prims.nat", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181" ], 0, "e217d0c30804e15b0a37ef42ce6b39ff" ], [ "Hacl.Loops.Lemmas.lemma_repeati_vec", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "binder_x_8781c9ff8ea7af3c1db5b0305f1ef6aa_2", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Hacl.Loops.Lemmas.repeat_w", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_214521be6835548f2f282adfe2372d8b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_aacd5c5013e5b4b181bda5c667bdb087", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "well-founded-ordering-on-nat" ], 0, "d5e77e119228b80b1f29cd0d8d8f4dd2" ], [ "Hacl.Loops.Lemmas.lemma_repeat_blocks_multi_load_acc", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_3015949e152d57179f3877cf7b8274b6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "2caca563c4a9301fe450007629b42f58" ], [ "Hacl.Loops.Lemmas.lemma_repeat_blocks_multi_load_acc", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "bae173c2a42329d31fb58bd7ada38ab5" ], [ "Hacl.Loops.Lemmas.lemma_repeat_blocks_multi_load_acc", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_3015949e152d57179f3877cf7b8274b6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "abec10ba4c918fd94ca1ae565be5588b" ], [ "Hacl.Loops.Lemmas.swap_mul", 1, 0, 0, [ "@query" ], 0, "3de70c190c2ee4891c3099c0aa1efa51" ], [ "Hacl.Loops.Lemmas.lemma_aux1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "e4ae604f01400dcf578947f2cc71cb2f" ], [ "Hacl.Loops.Lemmas.lemma_aux1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "4ea99f33a50a162a02aa6dc10bc0713a" ], [ "Hacl.Loops.Lemmas.lemma_repeat_blocks_multi_vec", 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", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_3015949e152d57179f3877cf7b8274b6", "refinement_interpretation_Tm_refine_4822116822fd2cd76140beff9d06b6d5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "baea02c1ebb98fd852931f4083d8f7dd" ], [ "Hacl.Loops.Lemmas.lemma_repeat_blocks_multi_vec", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "49de9caeb3e2bc67083bb1e8b3084df2" ], [ "Hacl.Loops.Lemmas.lemma_repeat_blocks_multi_vec", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Loops.Lemmas.lanes", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_Minus", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_3015949e152d57179f3877cf7b8274b6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "10633074c4b3e77d1b1060448bf19a13" ] ] ]