[ "sM\nÀœÕŒè\u0006÷Çž\"¼¯ë", [ [ "Hacl.Spec.Poly1305.Equiv.block_v", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Spec.Poly1305.size_block", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_7fb053190ac29f3918c540a6b6cbcbb0", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181" ], 0, "a2440aba7eb6e600a3563eff0e23c033" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "bf97aadf7d1d7f563e64aeee4866677c" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "b07eaf66ee417463be6f0a56e9e0ee3c" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma1", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.load_acc", "equation_Hacl.Spec.Poly1305.Vec.load_acc1", "equation_Hacl.Spec.Poly1305.Vec.load_blocks", "equation_Hacl.Spec.Poly1305.Vec.load_elem", "equation_Hacl.Spec.Poly1305.Vec.load_elem1", "equation_Hacl.Spec.Poly1305.Vec.normalize_1", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfadd", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Hacl.Spec.Poly1305.Vec.to_elem", "equation_Lib.ByteSequence.nat_from_bytes_le", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.block", "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.poly1305_update1", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.Seq.Properties.slice_length", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd", "token_correspondence_Spec.Poly1305.poly1305_update1", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Vec.load_acc1", "typing_Hacl.Spec.Poly1305.Vec.load_blocks", "typing_Hacl.Spec.Poly1305.Vec.load_elem1", "typing_Lib.ByteSequence.nat_from_bytes_le", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.create", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "7dfefe3218a964f3824945a52f334d11" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "299cfbfa7bcbe6e969da219f9b08bcd9" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "4eecd3652fe1a2e8158c2d55e3fcb16c" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma2", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "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.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.load_acc", "equation_Hacl.Spec.Poly1305.Vec.load_acc2", "equation_Hacl.Spec.Poly1305.Vec.load_blocks", "equation_Hacl.Spec.Poly1305.Vec.load_elem", "equation_Hacl.Spec.Poly1305.Vec.load_elem2", "equation_Hacl.Spec.Poly1305.Vec.normalize_2", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfadd", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "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.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.fmul", "equation_Spec.Poly1305.poly1305_update1", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.Sequence.create2_lemma", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfmul", "token_correspondence_Spec.Poly1305.poly1305_update1", "typing_Hacl.Spec.Poly1305.Vec.load_acc", "typing_Hacl.Spec.Poly1305.Vec.load_elem", "typing_Hacl.Spec.Poly1305.Vec.pfmul", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.create2", "typing_Lib.Sequence.length", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "5b81417a2a1aa2a90fcf2cf44572e505" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma4", 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_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "d97adb1107a0bba4bb317e9bdad1a66e" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma4", 2, 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.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "cca77009dcbfab50258ecd78372a3284" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma4", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "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.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.load_acc", "equation_Hacl.Spec.Poly1305.Vec.load_acc4", "equation_Hacl.Spec.Poly1305.Vec.load_blocks", "equation_Hacl.Spec.Poly1305.Vec.load_elem", "equation_Hacl.Spec.Poly1305.Vec.load_elem4", "equation_Hacl.Spec.Poly1305.Vec.normalize_4", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfadd", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "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.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.fmul", "equation_Spec.Poly1305.poly1305_update1", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.pow2_2", "lemma_Lib.Sequence.create4_lemma", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfmul", "token_correspondence_Spec.Poly1305.poly1305_update1", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Vec.load_acc", "typing_Hacl.Spec.Poly1305.Vec.load_elem", "typing_Hacl.Spec.Poly1305.Vec.pfmul", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.create4", "typing_Lib.Sequence.index", "typing_Lib.Sequence.length", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "4b0f4dad6006b0aecc393766ac00c52a" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma", 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_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "a51570ea6f75bc429e3a2b83742ce4ee" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma", 2, 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.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "64877da001b5fa54872bc395e2b0648b" ], [ "Hacl.Spec.Poly1305.Equiv.load_acc_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Lib.Sequence.lseq", "primitive_Prims.op_Multiply", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42" ], 0, "3c65db07287dc685d33d7b55a44dbc41" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "4db64703a158f78771731229aa10a14b" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "fb4c5a7c649532dab0d64fe929857dbd" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma1", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Vec.compute_r1", "equation_Hacl.Spec.Poly1305.Vec.compute_rw", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.load_blocks", "equation_Hacl.Spec.Poly1305.Vec.load_elem", "equation_Hacl.Spec.Poly1305.Vec.load_elem1", "equation_Hacl.Spec.Poly1305.Vec.normalize_1", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfadd", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Hacl.Spec.Poly1305.Vec.to_elem", "equation_Lib.ByteSequence.nat_from_bytes_le", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.block", "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.poly1305_update1", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.Seq.Properties.slice_length", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd", "token_correspondence_Spec.Poly1305.poly1305_update1", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Vec.compute_r1", "typing_Hacl.Spec.Poly1305.Vec.fmul", "typing_Hacl.Spec.Poly1305.Vec.load_blocks", "typing_Hacl.Spec.Poly1305.Vec.load_elem1", "typing_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "typing_Lib.ByteSequence.nat_from_bytes_le", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "01671fae1ea94462a8a01d4acbe57e55" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "f918dc0241bee257dea717dfb3540f50" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma2", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "8239869c27b2d9c28b1d421bceb26d7c" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma2", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Hacl.Spec.Poly1305.Lemmas_interpretation_Tm_arrow_346404407063272523bf34715c41d594", "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.pfelem", "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Hacl.Spec.Poly1305.Vec.compute_r2", "equation_Hacl.Spec.Poly1305.Vec.compute_rw", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.load_blocks", "equation_Hacl.Spec.Poly1305.Vec.load_elem", "equation_Hacl.Spec.Poly1305.Vec.load_elem2", "equation_Hacl.Spec.Poly1305.Vec.normalize_2", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfadd", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Hacl.Spec.Poly1305.Vec.to_elem", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "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.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.fmul", "equation_Spec.Poly1305.poly1305_update1", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.Sequence.create2_lemma", "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_050542d050b31782e2f5a256a21d1330", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfmul", "token_correspondence_Spec.Poly1305.poly1305_update1", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent", "typing_Hacl.Spec.Poly1305.Vec.compute_rw", "typing_Hacl.Spec.Poly1305.Vec.fmul", "typing_Hacl.Spec.Poly1305.Vec.load_blocks", "typing_Hacl.Spec.Poly1305.Vec.load_elem", "typing_Hacl.Spec.Poly1305.Vec.pfmul", "typing_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.create2", "typing_Lib.Sequence.length", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "96cfd92a6a29a7b9505c4e06cb6c4184" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma4", 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_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "2a9fe739364a973c234453c0e2a745f3" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma4", 2, 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.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "2863e7e5e581f8a5bab4b6927691b358" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma4", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Hacl.Spec.Poly1305.Vec_interpretation_Tm_arrow_fc0a7b2ced624ae8e81f22573822751a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Lemmas.op_Plus_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.op_Star_Percent", "equation_Hacl.Spec.Poly1305.Lemmas.prime", "equation_Hacl.Spec.Poly1305.Vec.compute_r4", "equation_Hacl.Spec.Poly1305.Vec.compute_rw", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.load_blocks", "equation_Hacl.Spec.Poly1305.Vec.load_elem", "equation_Hacl.Spec.Poly1305.Vec.load_elem4", "equation_Hacl.Spec.Poly1305.Vec.normalize_4", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfadd", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.pfmul", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Hacl.Spec.Poly1305.Vec.to_elem", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "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.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.fmul", "equation_Spec.Poly1305.poly1305_update1", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfadd", "function_token_typing_Hacl.Spec.Poly1305.Vec.pfmul", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.Sequence.create4_lemma", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfadd", "token_correspondence_Hacl.Spec.Poly1305.Vec.pfmul", "token_correspondence_Spec.Poly1305.poly1305_update1", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Vec.compute_rw", "typing_Hacl.Spec.Poly1305.Vec.fmul", "typing_Hacl.Spec.Poly1305.Vec.load_blocks", "typing_Hacl.Spec.Poly1305.Vec.load_elem", "typing_Hacl.Spec.Poly1305.Vec.pfmul", "typing_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.create4", "typing_Lib.Sequence.index", "typing_Lib.Sequence.length", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Lib.Sequence.sub", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "aa1ba4c509b6968f63f2adb7c96a2d03" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma", 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_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "1b6c76b81829d5bb32457ffaa71c2176" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma", 2, 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.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "560a58c223d9a9ddcd8b9f8e2f592d43" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_nblocks_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Sequence.lseq", "equation_Spec.Poly1305.felem", "primitive_Prims.op_Multiply", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42" ], 0, "8734a72e9a92bbe9e6d871ad607fc000" ], [ "Hacl.Spec.Poly1305.Equiv.repeat_blocks_multi_vec_equiv_pre_lemma", 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_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "25b85d234ea73f27ebf3b6645e68677b" ], [ "Hacl.Spec.Poly1305.Equiv.repeat_blocks_multi_vec_equiv_pre_lemma", 2, 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.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "1f2f934bbdac12bd9236755d58fc28aa" ], [ "Hacl.Spec.Poly1305.Equiv.repeat_blocks_multi_vec_equiv_pre_lemma", 3, 0, 0, [ "@query", "eq2-interp", "equation_Hacl.Spec.Poly1305.Vec.compute_rw", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Vec.Lemmas.repeat_blocks_multi_vec_equiv_pre", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_block", "function_token_typing_Hacl.Spec.Poly1305.Vec.normalize_n", "function_token_typing_Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks" ], 0, "88ae097713b0cb92af51207f120e9891" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_multi_lemma_v", 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_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "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", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "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", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key" ], 0, "88e6e1b2ee63a799f8815003c37cfd61" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_multi_lemma_v", 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.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "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", "equation_Spec.Poly1305.size_block", "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_542f9d4f129664613f2483a6c88bc7c2", "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, "cd6985e08a879d77419473312e4335f8" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_multi_lemma_v", 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", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Equiv.block_v", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d72d06730ac28d6dd9ad3860d815728e", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "ecf154f03386c323392730323fc90a96" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_multi_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "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", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "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", "typing_Spec.Poly1305.size_key" ], 0, "490ef526b50b38a0fcce112ba3082170" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_multi_lemma", 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.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.size_block", "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", "equation_Spec.Poly1305.size_block", "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_542f9d4f129664613f2483a6c88bc7c2", "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, "c96738eaf44834ebf3fcde245f4ec1d4" ], [ "Hacl.Spec.Poly1305.Equiv.poly_update_multi_lemma", 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.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update_multi", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_db6848efac7d38cc08359175c1b52547", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "7bda0199ca5e685ab36e61029353d584" ], [ "Hacl.Spec.Poly1305.Equiv.poly1305_update_vec_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Vec.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update", "equation_Hacl.Spec.Poly1305.Vec.poly1305_update_vec", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.poly1305_update", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Spec.AES.elem", "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.minint", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "fe4ad878854168c8d34bfd42ccb04fef" ], [ "Hacl.Spec.Poly1305.Equiv.poly1305_vec_lemma", 1, 0, 0, [ "@query", "equation_Hacl.Spec.Poly1305.Vec.poly1305_mac", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.poly1305_mac", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "d5ab3d8dd2425e07902940a85aabdad9" ] ] ]