[ "QÂo–äIZ^nôzlnŒc8", [ [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_prime", 1, 0, 0, [ "@query" ], 0, "630c3498f2e0966dc725d2bcede55239" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_prime", 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_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, "e1a1433247e224eeed383ea682cf8353" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "int_typing", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.uint_to_t", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "b475519044c531b520559659d9dd0864" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero_eq", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry26_wide", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a190d9fd2e1a8de03152e87cdbef4fbd", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.index", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "63b4213c11297d85548e72789f9ab10d" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.vec_smul_mod_five_i", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "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", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "f65af6aef49e2c664c51e996cdaff99a" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.vec_smul_mod_five_i", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Prims.pos", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Hacl.Spec.Poly1305.Field32xN.pow26" ], 0, "1cdf39ec5248c0327da8d44dea11e4de" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.vec_smul_mod_five_i", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_Lib.IntTypes.pow2_2", "lemma_Lib.IntTypes.shift_left_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_57eccc6c8bd59ba82f57846da8a801f7", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7c94516bb2f52db0f466939edf55e5d0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.v", "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.U64@tok" ], 0, "05ee97042b9b96d695095752487c60a9" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.vec_smul_mod_five", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "3e839157664cadd50bcdda362e678aa8" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.vec_smul_mod_five", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Prims.pos", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Hacl.Spec.Poly1305.Field32xN.pow26" ], 0, "2d0e66d2908a5a7b948cb2eb4e7e4394" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.vec_smul_mod_five", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_cd6e2af2c720a97ef71723e3dc123b88", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_left_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.mul_mod", "function_token_typing_Lib.IntTypes.shift_left_i", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1b43ad09734150a98a09eb8af4f2257c", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7c94516bb2f52db0f466939edf55e5d0", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d2e89358d7bc2020d2e2464f7734f373", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_e7b192ccdafff2daa28742e0e1384221", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.mul_mod", "token_correspondence_Lib.IntTypes.shift_left_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "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.U64@tok" ], 0, "336ec0268b42b405d3ab1a6170a45763" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_compact", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "f45320504a47510a3ff51890a53686dc" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_lemma_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Lib.IntVector.width", "equation_Prims.pos", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Hacl.Spec.Poly1305.Field32xN.pow26" ], 0, "d55b2b5029744261b7118438a74309a9" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_lemma_i", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Prims.pos", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Hacl.Spec.Poly1305.Field32xN.pow26" ], 0, "59a66fa3b23c43330a8a6d8782917de2" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_lemma_i", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_right_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.shift_right_i", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.vec_and", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mod_mask_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13236e0c52dbe4f6e0704a273d0ea060", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_36a04e927def1e73ac998ceb9d1e059e", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_57eccc6c8bd59ba82f57846da8a801f7", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7c94516bb2f52db0f466939edf55e5d0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_8fff9b5af34beb307f1433ff6c3eaf37", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d46a7a194748aba4367abac00faa061", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.logand", "token_correspondence_Lib.IntTypes.shift_right_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "37d9c3f9f1b0ddea3c68f2315c4e89e8" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_fits_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.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "db5a92a45f35d98762467ed5c2bfffb2" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_fits_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Prims.pos", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Hacl.Spec.Poly1305.Field32xN.pow26" ], 0, "b8cba5d0b2ad2db037fbe883d100fc72" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_fits_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "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", "function_token_typing_Lib.IntVector.vec_and", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_14fc39f7b1b344cf900ab79e0d214e0c", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7c94516bb2f52db0f466939edf55e5d0", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d46a7a194748aba4367abac00faa061", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Lib.IntTypes.minint", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "c249a6f2a9cfbbd0df5325e1d2d53ac1" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_eval_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.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "int_inversion", "lemma_FStar.UInt.pow2_values", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "3159fce15efe47f80969d62f6e5ecb3e" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_eval_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Prims.pos", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Hacl.Spec.Poly1305.Field32xN.pow26" ], 0, "25fb9a95b13642b752f5cd1d0c2b27c3" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_eval_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntVector.width", "equation_Prims.nat", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181" ], 0, "e0d2323df9daf1e35fcd14c764b99d25" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_lemma_i", 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.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "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_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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "20f134c3393dfd7730ead64cae1610ec" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_lemma_i", 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.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "876571f95d06adc65346244db1f12c33" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_lemma_i", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale32", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_right_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.shift_right_i", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mod_mask_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13236e0c52dbe4f6e0704a273d0ea060", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_36a04e927def1e73ac998ceb9d1e059e", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_57eccc6c8bd59ba82f57846da8a801f7", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_6e9be704ead8ad76f9833bf58145f462", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8634b8cea33f1f5cba1ac603ce991931", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_8fff9b5af34beb307f1433ff6c3eaf37", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_abeafaec270226fd0b37bcfd80c71ee1", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d14c34939b0787063146b4d3f1d83d07", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.logand", "token_correspondence_Lib.IntTypes.shift_right_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_load", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "2cc98ea6c882409dd500e619c0d1ae4d" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_fits_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.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale32", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8634b8cea33f1f5cba1ac603ce991931", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "6c4467c2128b22009aa87855423bb1c6" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_fits_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.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "885d818ad6b847698852583a9a0b2137" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_fits_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Lib.IntVector_interpretation_Tm_arrow_2ee99524035b4fc0efae0dbafd0f30fd", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale32", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.shift_right_i", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntVector.vec_add_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_14fc39f7b1b344cf900ab79e0d214e0c", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8634b8cea33f1f5cba1ac603ce991931", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_abeafaec270226fd0b37bcfd80c71ee1", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_d14c34939b0787063146b4d3f1d83d07", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.minint", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "67c8797752d684564fdf477341432a12" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_eval_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.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale32", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "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_key", "int_inversion", "lemma_FStar.UInt.pow2_values", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8634b8cea33f1f5cba1ac603ce991931", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "c919f84a075895143ab78cd335f7786d" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_eval_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.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "c4736cecf28c4a1c649396dec8c41e7f" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry26_eval_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Lib.IntVector_interpretation_Tm_arrow_2ee99524035b4fc0efae0dbafd0f30fd", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale32", "equation_Hacl.Spec.Poly1305.Field32xN.scale64", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.shift_right_i", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntVector.vec_add_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02b2ebf135b3092fb5fd0ef9178a9ca3", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_14fc39f7b1b344cf900ab79e0d214e0c", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8634b8cea33f1f5cba1ac603ce991931", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_abeafaec270226fd0b37bcfd80c71ee1", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d14c34939b0787063146b4d3f1d83d07", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.minint", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_and", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "0dae3888fe7410099eb4d2c6f87d3e85" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_fits_lemma0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "9e452b6f9f9288bb96bcabd6f6134e6d" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_fits_lemma0", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.IntVector_interpretation_Tm_arrow_2ee99524035b4fc0efae0dbafd0f30fd", "Lib.IntVector_interpretation_Tm_arrow_3c3a9219e4df813f1b2ae9adc23ed76a", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry26_wide", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.shift_right_i", "function_token_typing_Lib.IntVector.vec_shift_right", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_14fc39f7b1b344cf900ab79e0d214e0c", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d11bd122d8489a9a2546b9192a15416d", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "token_correspondence_Lib.IntTypes.add_mod", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.sec_int_v", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_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.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "aab9ce877eca0682cc5deb0f5c53feed" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_fits_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_cd6e2af2c720a97ef71723e3dc123b88", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.IntVector_interpretation_Tm_arrow_faead18bad5c13a0f7beeb36c910236f", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry26_wide", "equation_Hacl.Spec.Poly1305.Field32xN.carry_wide_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_right_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.mul_mod", "function_token_typing_Lib.IntTypes.shift_right_i", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.vec_shift_right", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13236e0c52dbe4f6e0704a273d0ea060", "refinement_interpretation_Tm_refine_1d9d3fa86e53fad766cc041660ba4ad0", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d2e89358d7bc2020d2e2464f7734f373", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.mul_mod", "token_correspondence_Lib.IntTypes.shift_right_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.sec_int_v", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_left", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "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.U64@tok" ], 0, "78e66924e3c19659f9bda8bb791fdca5" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma_i0", 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_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_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "ab8104e85023c3001e892a813470a5d3" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma_i0", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.pow104", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.pow52", "equation_Hacl.Spec.Poly1305.Field32xN.pow78", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "236611b087d2a489e4e7462bce5fdc83" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma_i1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry26_wide", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "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_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "437bc8df6cf34de997cc8e152e390cab" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma_i1", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_5644a8a9a66bca6b63aba1f3f0bf5682", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero", "equation_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry26_wide", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.feval5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_right_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.shift_right_i", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13236e0c52dbe4f6e0704a273d0ea060", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d11bd122d8489a9a2546b9192a15416d", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.shift_right_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.transpose", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "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_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "f4d5b274e7c720911c2086e541cf65d2" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "int_inversion", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d11bd122d8489a9a2546b9192a15416d", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Spec.Poly1305.Field32xN.carry_wide_felem5", "typing_Hacl.Spec.Poly1305.Field32xN.feval5" ], 0, "1e49b2e58cc48648c340b3593d707d1c" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma_i", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_5644a8a9a66bca6b63aba1f3f0bf5682", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_cd6e2af2c720a97ef71723e3dc123b88", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.IntVector_interpretation_Tm_arrow_faead18bad5c13a0f7beeb36c910236f", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "data_typing_intro_FStar.Pervasives.Native.Mktuple5@tok", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Poly1305.Field32xN.Lemmas1.carry26_wide_zero", "equation_Hacl.Spec.Poly1305.Field32xN.as_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry26_wide", "equation_Hacl.Spec.Poly1305.Field32xN.carry_wide_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.feval5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_right_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.mul_mod", "function_token_typing_Lib.IntTypes.shift_right_i", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.vec_shift_right", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13236e0c52dbe4f6e0704a273d0ea060", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_49520c4a78c26da590d892803fee487f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d11bd122d8489a9a2546b9192a15416d", "refinement_interpretation_Tm_refine_d2e89358d7bc2020d2e2464f7734f373", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_dbb6e2304996c2066357799607e51556", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.mul_mod", "token_correspondence_Lib.IntTypes.shift_right_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.feval5", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.transpose", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.sec_int_v", "typing_Lib.IntTypes.shift_right_i", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "899fa24bee8c303cf4fe457b0887306e" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_wide_felem5_eval_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "int_inversion", "lemma_Lib.Sequence.eq_elim", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_Hacl.Spec.Poly1305.Field32xN.carry_wide_felem5", "typing_Hacl.Spec.Poly1305.Field32xN.feval5" ], 0, "2fca641d19297d4be3e4b5c3f0c4f62b" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_subtract_p5_0", 1, 0, 0, [ "@query" ], 0, "1beaa8941f76a84be724361f4048c619" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_subtract_p5_0", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.pow104", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.pow52", "equation_Hacl.Spec.Poly1305.Field32xN.pow78", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.prime", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2f45c9e16b35ebca4e315d4cbca606f7", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "66797003f01b5aa26809df0af9a4f9b7" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_subtract_p5_1", 1, 0, 0, [ "@query" ], 0, "5aebe603968180b0208abbaad1ed9471" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_subtract_p5_1", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow104", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.pow52", "equation_Hacl.Spec.Poly1305.Field32xN.pow78", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_key", "int_inversion", "int_typing", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2f45c9e16b35ebca4e315d4cbca606f7", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Spec.Poly1305.prime", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "6e0e98da1f7759af6c49a4d4c34579a6" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_subtract_p5", 1, 0, 0, [ "@query" ], 0, "5faad9738c2f5ff569163e132784ac68" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.lemma_subtract_p5", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.__cache_version_number__", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "c8eb324b16203fc1be563e76ad3eb0f3" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_s", 1, 0, 0, [ "@query" ], 0, "fedae76acd8f6504456ec2e0bf35f88c" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_s", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.S128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.eq_mask_lemma", "lemma_Lib.IntTypes.eq_mask_logand_lemma", "lemma_Lib.IntTypes.gte_mask_logand_lemma", "lemma_Lib.IntTypes.sub_mod_lemma", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_32fa55545657d174d24f9d18b564fe78", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_79cccf554dcdd144234157e1c40e9988", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_8fff9b5af34beb307f1433ff6c3eaf37", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d13c5132af51f62dfb7018a438f66ab7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.createi", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "e9cf408240852652cb246baa04f057b9" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_felem5_lemma_i", 1, 0, 1, [ "@query" ], 0, "7776c6b25921b87126a2cc557d4b63ae" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_felem5_lemma_i", 2, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_ddf90b607a103b2a2807495669efe916", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.IntTypes_interpretation_Tm_arrow_f4afff6b394bf99658a087b1e50597af", "Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "data_elim_FStar.Pervasives.Native.Mktuple5", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_s", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.subtract_p5", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.eq_mask", "function_token_typing_Lib.IntTypes.gte_mask", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.sub_mod", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.vec_and", "int_inversion", "int_typing", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02f19e993527e03e7a59aa8004f650d1", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_32fa55545657d174d24f9d18b564fe78", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6e9be704ead8ad76f9833bf58145f462", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_bbd3d2fea005af06678c3d220f823f6e", "refinement_interpretation_Tm_refine_bcbf37505db68bf5374bb6fe39b43a3d", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d13c5132af51f62dfb7018a438f66ab7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "token_correspondence_Lib.IntTypes.logand", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_and", "typing_Lib.IntVector.vec_eq_mask", "typing_Lib.IntVector.vec_gte_mask", "typing_Lib.IntVector.vec_load", "typing_Lib.IntVector.vec_sub_mod", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "dc48f93a190121b250ad2961c18e466c" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_felem5_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.subtract_p5", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_32fa55545657d174d24f9d18b564fe78", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Spec.Poly1305.Field32xN.fas_nat5", "typing_Hacl.Spec.Poly1305.Field32xN.feval5", "typing_Hacl.Spec.Poly1305.Field32xN.subtract_p5", "typing_Spec.Poly1305.size_key" ], 0, "1f0939e3fc6889d076f2684d2c1583dc" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.subtract_p5_felem5_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_10283246b3c03adf663505527582a37c", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_5644a8a9a66bca6b63aba1f3f0bf5682", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.fas_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.feval5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.subtract_p5", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.as_nat5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "int_inversion", "int_typing", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_32fa55545657d174d24f9d18b564fe78", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.subtract_p5", "typing_Hacl.Spec.Poly1305.Field32xN.transpose", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.map", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "c8a60a6625635db9f2476a0424cc6ee7" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_t", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "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, "7f6db4fa74c7d268a97ee7e12a0dfa61" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_lemma_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "472ce0b5c1045afe72947ad91f025738" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_lemma_i", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_32fa55545657d174d24f9d18b564fe78", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_57eccc6c8bd59ba82f57846da8a801f7", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e0294068a636be83f4d3a151cd3b95b7", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "865415a3d69435885a017aff4a1012aa" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "36edd8ea3012ce047b264d3b21e9cf4c" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_t", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "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", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "l_quant_interp_b62ffa816c17a75b8d8572868ea487dd", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_32fa55545657d174d24f9d18b564fe78", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.createi", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "f9893ec6e321c6a2460e6ecb38171696" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_fits_lemma0", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "lemma_FStar.UInt.pow2_values", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2cff1949ae54a0c8aa277799c4a16dc5", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.index", "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.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "811ea048ccb632feddfeec6d693b3371" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_fits_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "Lib.IntTypes_interpretation_Tm_arrow_cd6e2af2c720a97ef71723e3dc123b88", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.mul_mod", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.mul_mod_lemma", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "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_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d2e89358d7bc2020d2e2464f7734f373", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "token_correspondence_Lib.IntTypes.mul_mod", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.sec_int_v", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "0c9cc1028d3208e19c3a55dc875f0726" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma_i0", 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_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_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "98be581908669bf7c39738870b486e6e" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma_i0", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.pow104", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.pow52", "equation_Hacl.Spec.Poly1305.Field32xN.pow78", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "5385fc78eb1e245172c6dedcb7a45bb8" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma_i1", 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.Field32xN.lanes", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "proj_equation_Spec.GaloisField.GF_t", "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_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "425fcbd2dd74c9f031cbf366b8f6a095" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma_i1", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_5644a8a9a66bca6b63aba1f3f0bf5682", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.feval5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.prime", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_Lib.IntTypes.pow2_127", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5710dd694b7534e75f33436725eb7d40", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.transpose", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "a252a4ce92b7e54fa177baecd928031d" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "int_inversion", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5710dd694b7534e75f33436725eb7d40", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "typing_Hacl.Spec.Poly1305.Field32xN.feval5" ], 0, "4341202854e6e894103856b8fee387e1" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma_i", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_5644a8a9a66bca6b63aba1f3f0bf5682", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_cd6e2af2c720a97ef71723e3dc123b88", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "data_typing_intro_FStar.Pervasives.Native.Mktuple5@tok", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_nat5", "equation_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.feval5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_fits", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.mul_mod", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "primitive_Prims.op_Addition", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_49520c4a78c26da590d892803fee487f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56d08faeb4b1f0343acfaa06fb459d6d", "refinement_interpretation_Tm_refine_5710dd694b7534e75f33436725eb7d40", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d2e89358d7bc2020d2e2464f7734f373", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "token_correspondence_Hacl.Spec.Poly1305.Field32xN.as_pfelem5", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.mul_mod", "typing_Hacl.Spec.Poly1305.Field32xN.feval5", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.transpose", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "e7c73aaaf9fc7d81f82f44cb73c13000" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_eval_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_wide5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "int_inversion", "lemma_Lib.Sequence.eq_elim", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "typing_Hacl.Spec.Poly1305.Field32xN.feval5" ], 0, "2a4198e62413a2a81d891b0676abc5e9" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_full_felem5_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "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.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_t", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "int_inversion", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "l_quant_interp_b62ffa816c17a75b8d8572868ea487dd", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2cff1949ae54a0c8aa277799c4a16dc5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.Sequence.createi", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a" ], 0, "737213b94e04949bc6273cab124132d7" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_lemma_i", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntVector.width", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "5a7c850b98a5d42a0881468a5ed04290" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_lemma_i", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Lib.IntTypes_interpretation_Tm_arrow_80450669f43858ae3009d97d5eb015a7", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "b2t_def", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.mod_mask", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shift_right_i", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.logand", "function_token_typing_Lib.IntTypes.shift_right_i", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mod_mask_lemma", "lemma_Lib.IntTypes.shift_left_lemma", "lemma_Lib.IntTypes.shift_right_lemma", "lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_13236e0c52dbe4f6e0704a273d0ea060", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b", "refinement_interpretation_Tm_refine_3667fd6eabf06c7cb385f1857e7237ec", "refinement_interpretation_Tm_refine_36a04e927def1e73ac998ceb9d1e059e", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_57eccc6c8bd59ba82f57846da8a801f7", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_8fff9b5af34beb307f1433ff6c3eaf37", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d96d126280e4d44b4c6d27838df6e25f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_interpretation_Tm_refine_fffc918f3ac13711d39fee794fcdce53", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Lib.IntTypes.shift_right_i", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "63f31e7c3242eecbfed84ae208ddc45e" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_fits_lemma_i0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntVector.width", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "d3499c6598a0109915b6797a1e151851" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_fits_lemma_i0", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntVector_interpretation_Tm_arrow_2ee99524035b4fc0efae0dbafd0f30fd", "Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U128@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_t", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.scale32", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Lib.IntVector.shift_right_i", "function_token_typing_Lib.IntVector.vec_and", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "l_quant_interp_b62ffa816c17a75b8d8572868ea487dd", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0778771350877a4f173130f493961171", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_14fc39f7b1b344cf900ab79e0d214e0c", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_49520c4a78c26da590d892803fee487f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8634b8cea33f1f5cba1ac603ce991931", "refinement_interpretation_Tm_refine_8b148b95a729cf5fe3aa2da01c92567d", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.UInt32.uint_to_t", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_shift_right", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "2717c294f2f793ea67633f61f262e98f" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_fits_lemma_i1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Lib.IntVector.width", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181" ], 0, "7f0b88c3912684f823e978875a18140a" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_fits_lemma_i1", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "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.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_t", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "l_quant_interp_b62ffa816c17a75b8d8572868ea487dd", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0778771350877a4f173130f493961171", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.Sequence.create", "typing_Lib.Sequence.createi", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "4bcc35e26ef504c8912da1efcd0f660a" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_fits_lemma_i", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_183de1cb59f51c46c962d4e8a1ebd3e9", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9", "Lib.IntTypes_interpretation_Tm_arrow_cd6e2af2c720a97ef71723e3dc123b88", "Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.mask26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "equation_Hacl.Spec.Poly1305.Field32xN.zero", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.op_At_Percent_Dot", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "function_token_typing_Lib.IntTypes.add_mod", "function_token_typing_Lib.IntTypes.mul_mod", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "interpretation_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_mod_lemma", "lemma_Lib.IntVector.vec_add_mod_lemma", "lemma_Lib.IntVector.vec_and_lemma", "primitive_Prims.op_Addition", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5", "refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134", "refinement_interpretation_Tm_refine_49520c4a78c26da590d892803fee487f", "refinement_interpretation_Tm_refine_4e3bbd8eec0c3ef82902d2336c68c242", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c7434c6c05b6023e64eda6cbe46f4ac9", "refinement_interpretation_Tm_refine_d280f3c089c48c764f6d0e8776c26166", "refinement_interpretation_Tm_refine_d2e89358d7bc2020d2e2464f7734f373", "refinement_interpretation_Tm_refine_d98ca274c8e1fa507a92f56e0bc852d3", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Lib.IntTypes.add_mod", "token_correspondence_Lib.IntTypes.mul_mod", "typing_Hacl.Spec.Poly1305.Field32xN.mask26", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN_v", "typing_Hacl.Spec.Poly1305.Field32xN.zero", "typing_Lib.IntVector.vec_add_mod", "typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi", "typing_Lib.Sequence.index", "typing_Lib.Sequence.map", "typing_Lib.Sequence.map2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_5af39d96c1dfe248ec83931fe73dcc8b", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "50e0782457d516669f93c502c191c0a8" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_fits_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "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.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.carry26", "equation_Hacl.Spec.Poly1305.Field32xN.carry_full_felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "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", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "int_inversion", "int_typing", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0778771350877a4f173130f493961171", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.createi", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "7fe1e68c2b9daa8f78af7c2243bb178b" ], [ "Hacl.Poly1305.Field32xN.Lemmas1.carry_reduce_felem5_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Hacl.Spec.Poly1305.Field32xN_interpretation_Tm_arrow_a7361ff514189f826f088552abd677d3", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Poly1305.Field32xN.Lemmas1.acc_inv_t", "equation_Hacl.Spec.Poly1305.Field32xN.as_tup64_i", "equation_Hacl.Spec.Poly1305.Field32xN.felem5", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.felem_fits5", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.max26", "equation_Hacl.Spec.Poly1305.Field32xN.pow26", "equation_Hacl.Spec.Poly1305.Field32xN.transpose", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_5", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits1", "equation_Hacl.Spec.Poly1305.Field32xN.tup64_fits5", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.width", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple5", "function_token_typing_Hacl.Spec.Poly1305.Field32xN.tup64_5", "int_inversion", "int_typing", "interpretation_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "l_quant_interp_b62ffa816c17a75b8d8572868ea487dd", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "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_FStar.Pervasives.Native.Mktuple5__1", "projection_inverse_FStar.Pervasives.Native.Mktuple5__2", "projection_inverse_FStar.Pervasives.Native.Mktuple5__3", "projection_inverse_FStar.Pervasives.Native.Mktuple5__4", "projection_inverse_FStar.Pervasives.Native.Mktuple5__5", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0778771350877a4f173130f493961171", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26b730cb944f71bac9def42c920eb7ed", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Spec.Poly1305.Field32xN.max26", "typing_Hacl.Spec.Poly1305.Field32xN.pow26", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.createi", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_baadd0755aa20f9b2a01722e1436594a", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "a68dd33d074dc93f2c7e2bd2b3592573" ] ] ]