[ "±†3èùKhFªl“ã*i\t&", [ [ "Hacl.Impl.Poly1305.Fields.width", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "a717b564b8d7fff1764aaa42a49cb05b" ], [ "Hacl.Impl.Poly1305.Fields.limb", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "60ba059214e0c3a7de9cd9cb9acee443" ], [ "Hacl.Impl.Poly1305.Fields.limb_zero", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_7781f1e036957f9fd663f44508e3fe92", "refinement_interpretation_Tm_refine_f55876baa9e11eb032dbd617ba408179", "refinement_interpretation_Tm_refine_fcfed6be912dddcfb8e632609761cb07", "typing_Spec.Poly1305.size_key" ], 0, "09c4cbec4a048ac999b75bdd53bd328d" ], [ "Hacl.Impl.Poly1305.Fields.wide", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "typing_Spec.Poly1305.size_key" ], 0, "d0f80c03ce69a8cc04ec62da00dfcd79" ], [ "Hacl.Impl.Poly1305.Fields.nlimb", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec" ], 0, "8fa2ea4e19d7fd6a844395c17dafb7d4" ], [ "Hacl.Impl.Poly1305.Fields.blocklen", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@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.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "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_Hacl.Impl.Poly1305.Fields.field_spec", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "43d29a7933f1cf1255196d8af6d6943e" ], [ "Hacl.Impl.Poly1305.Fields.nelem", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec" ], 0, "2f811434c142b9e4929130bd8c6cb3b3" ], [ "Hacl.Impl.Poly1305.Fields.precomplen", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec" ], 0, "b6d11fe186c6f34402160375fe134238" ], [ "Hacl.Impl.Poly1305.Fields.felem_fits", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "b677f21ddbaca4911f65672c355c3de2" ], [ "Hacl.Impl.Poly1305.Fields.fas_nat", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "25882fe01e18b6d475f48f01ec1ef207" ], [ "Hacl.Impl.Poly1305.Fields.feval", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "90418ceeb9156a3ff77a9461f2688a83" ], [ "Hacl.Impl.Poly1305.Fields.lemma_feval_is_fas_nat", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Hacl.Impl.Poly1305.Fields.fas_nat", "typing_Hacl.Impl.Poly1305.Fields.feval", "typing_Spec.Poly1305.size_key", "typing_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "typing_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "typing_tok_Hacl.Impl.Poly1305.Fields.M32@tok" ], 0, "46a19eca63fadc1cac2e6f3678b89ef5" ], [ "Hacl.Impl.Poly1305.Fields.lemma_feval_is_fas_nat", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.fas_nat", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b" ], 0, "69caf76477ec506d4f5f08b5d77bb7bc" ], [ "Hacl.Impl.Poly1305.Fields.create_felem", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.Buffer.MUT@tok", "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.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.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x2", "equation_Lib.IntVector.width", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x2", "function_token_typing_Prims.__cache_version_number__", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "df77633e59400e6092bf643a3fed4913" ], [ "Hacl.Impl.Poly1305.Fields.create_felem", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Field32xN.felem", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "a52d6c15a842cb9dc6a7a247bbb2ae1e" ], [ "Hacl.Impl.Poly1305.Fields.load_felem_le", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@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.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Hacl.Spec.Poly1305.Vec.size_key", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x2", "equation_Lib.IntVector.uint64x4", "equation_Lib.IntVector.width", "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x2", "function_token_typing_Lib.IntVector.uint64x4", "function_token_typing_Spec.AES.elem", "int_typing", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_AmpAmp", "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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_b7e7e236a3beba992e8741bf2b5c0052", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Hacl.Spec.Poly1305.Vec.size_block", "typing_Hacl.Spec.Poly1305.Vec.size_key", "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "4c1f446450a968a9f77929fab94df059" ], [ "Hacl.Impl.Poly1305.Fields.load_felem_le", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0b2b907cafe143a33f7cdd7e43f1a546", "refinement_interpretation_Tm_refine_0d9085a92004f3e6593d9819549b5328", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_279be9bc28858d6e06732ecf7fa45362", "refinement_interpretation_Tm_refine_656c466b60cba9714887c5e369845456", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "6ba4a27fc2e4b3c3126feaa13fe845e3" ], [ "Hacl.Impl.Poly1305.Fields.load_felems_le", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@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.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x2", "equation_Lib.IntVector.uint64x4", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x2", "function_token_typing_Lib.IntVector.uint64x4", "function_token_typing_Spec.AES.elem", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4f4dbfa4626718e66c3c8f2b26fd9d5c" ], [ "Hacl.Impl.Poly1305.Fields.load_felems_le", 2, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "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.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "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.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.v_injective", "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_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0b2b907cafe143a33f7cdd7e43f1a546", "refinement_interpretation_Tm_refine_0d9085a92004f3e6593d9819549b5328", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_279be9bc28858d6e06732ecf7fa45362", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_656c466b60cba9714887c5e369845456", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6a5da8e7ab14dee1f2a4542950be2473" ], [ "Hacl.Impl.Poly1305.Fields.load_acc", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@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.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.size_block", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x2", "equation_Lib.IntVector.uint64x4", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Lib.IntVector.uint64x2", "function_token_typing_Lib.IntVector.uint64x4", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d9b80b138b8c680d922b4d07c711eda9" ], [ "Hacl.Impl.Poly1305.Fields.load_acc", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@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.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.load_acc", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_2", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_26feaf6e38ebdbada45bd37367aa4bf2", "refinement_interpretation_Tm_refine_50b5a97573571e9eabd935c025eeb75c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9901e9bd502660deebd79ec7bfef6e1f", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b22e22982abe3cb76da6196dc9c47e3f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "be54b8efa4e8e8326a3ded8698fdc07b" ], [ "Hacl.Impl.Poly1305.Fields.set_bit", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_ae160b0fc4d8939c4e8f5cbe21685856", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a7d0aadf36147d83ba6a57b485ad7062" ], [ "Hacl.Impl.Poly1305.Fields.set_bit", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1908a8751ae9574b0dbd13c4922dce7b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a1f0e3058fe95a099135997dd9f7a187", "refinement_interpretation_Tm_refine_d67c7b2035f920943d1b8d2654487e8f", "refinement_interpretation_Tm_refine_de0be697c6eb57a2112859384f733989", "typing_Spec.Poly1305.size_key" ], 0, "9fc541400e18a658f772705be039ac94" ], [ "Hacl.Impl.Poly1305.Fields.set_bit128", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.lbuffer_t", "equation_Prims.nat", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "int_typing", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8" ], 0, "3ef7abbde80843e0557f593f60104543" ], [ "Hacl.Impl.Poly1305.Fields.set_bit128", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_227fd6e3a355afc12273451ef393bd6b", "refinement_interpretation_Tm_refine_6035173ebc04dde9d6b5ed47d37f8a8d", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b90d51946cbc8b06efc92e6dba2bab08", "refinement_interpretation_Tm_refine_d984c012b1708a13bdca866d2c2256a6", "typing_Spec.Poly1305.size_key" ], 0, "e0f11a7292d843c06a20aaa78cbc666c" ], [ "Hacl.Impl.Poly1305.Fields.set_zero", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "equation_Spec.Poly1305.prime", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_Spec.Poly1305.prime" ], 0, "cf9d938f784d3c44fc66e89c3993ed3c" ], [ "Hacl.Impl.Poly1305.Fields.set_zero", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e4c0933138780179d8dc0d5538fee4", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1e9ba5c5f02af0d7253b5ea716c1b404", "refinement_interpretation_Tm_refine_690b31dfb9a09c5c77e57fc7eb526e9f", "refinement_interpretation_Tm_refine_8a5d133771c80f95afd4c22925cb3251", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "0e1ae68a4a48a3245706efd5b95015c0" ], [ "Hacl.Impl.Poly1305.Fields.reduce_felem", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_84d96e628de65675ff8992c61dbc40f7", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_FStar.Seq.Base.length", "typing_Hacl.Impl.Poly1305.Fields.fas_nat", "typing_Hacl.Impl.Poly1305.Fields.feval", "typing_Spec.Poly1305.size_key", "typing_tok_Hacl.Impl.Poly1305.Fields.M32@tok" ], 0, "59e2a80bb557aa8a335ef1945ba528f9" ], [ "Hacl.Impl.Poly1305.Fields.reduce_felem", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.fas_nat", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_12470b38d36fb95b737d591e68bbc1b9", "refinement_interpretation_Tm_refine_4268aadea005c9c25024cf8cb5081adb", "refinement_interpretation_Tm_refine_84d96e628de65675ff8992c61dbc40f7", "refinement_interpretation_Tm_refine_9d872b6af44774fe9a9a37405b4eb28c", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "97968a23848f717ea70a781236b758e6" ], [ "Hacl.Impl.Poly1305.Fields.load_precompute_r", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "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", "equality_tok_Lib.Buffer.MUT@tok", "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.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x2", "equation_Lib.IntVector.uint64x4", "equation_Lib.IntVector.width", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x2", "function_token_typing_Lib.IntVector.uint64x4", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e9c32a5fb00a4e8c339597118c871180", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Lib.Buffer.gsub", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "bc9fc97a48ba43f4b8e7895c737074fc" ], [ "Hacl.Impl.Poly1305.Fields.load_precompute_r", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e4c0933138780179d8dc0d5538fee4", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1e9ba5c5f02af0d7253b5ea716c1b404", "refinement_interpretation_Tm_refine_690b31dfb9a09c5c77e57fc7eb526e9f", "refinement_interpretation_Tm_refine_8a5d133771c80f95afd4c22925cb3251", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "e482376e69e826d3b5de8aa0e90de70e" ], [ "Hacl.Impl.Poly1305.Fields.fadd_mul_r", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.Buffer.MUT@tok", "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.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "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.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.elem", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x4", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x4", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.minint", "typing_Lib.IntVector.vec_t", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "67df0be6c688ed81d2335aa657c0693b" ], [ "Hacl.Impl.Poly1305.Fields.fadd_mul_r", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_198b4be4c1a2a0fefa267ce97b25ca8b", "refinement_interpretation_Tm_refine_71ef72aebb0053335a2a94a400348be2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cae6ef389d3918544f42e2dfc0fc495b", "refinement_interpretation_Tm_refine_f7b65ac76c8ff8ddb1d89b9e3b03d53a", "typing_Spec.Poly1305.size_key" ], 0, "bb7113b500734597d3afd3cf8fbb5715" ], [ "Hacl.Impl.Poly1305.Fields.fmul_rn", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "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.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x2", "equation_Lib.IntVector.uint64x4", "equation_Lib.IntVector.width", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x2", "function_token_typing_Lib.IntVector.uint64x4", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_58fca88c8cbe8f8a580d4eb99ee0f2ce", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "9863afc51de7c91d154a169298511cca" ], [ "Hacl.Impl.Poly1305.Fields.fmul_rn", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Vec.fmul", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_25d4d084688a57969e6c4edd6b0502af", "refinement_interpretation_Tm_refine_8cef873a89a6420278817d1323bd6daa", "refinement_interpretation_Tm_refine_96fb078e241e920e93f3f7d3ba019272", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_aab77021dcf0d03955a51483a2062657", "typing_Spec.Poly1305.size_key" ], 0, "f6a7473c08b774ea87134f8e2ad23ac1" ], [ "Hacl.Impl.Poly1305.Fields.fmul_rn_normalize", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.Buffer.MUT@tok", "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.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "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.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.lanes", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.IntVector.uint64x4", "equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "function_token_typing_Lib.IntVector.uint64x4", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf", "refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_7469e637a8c96cb70cd78854c6904f1b", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.Poly1305.Field32xN.uint64xN", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.minint", "typing_Lib.IntVector.vec_t", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "2bfd70063561b89b0981f2797c6edaad" ], [ "Hacl.Impl.Poly1305.Fields.fmul_rn_normalize", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Impl.Poly1305.Fields.precomp_r", "equation_Hacl.Spec.Poly1305.Field32xN.uint64xN", "equation_Hacl.Spec.Poly1305.Vec.normalize_n", "equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_03d3a41aa2cb6c0001c10e6b74b1b195", "refinement_interpretation_Tm_refine_0ac358512c86cddd0c410254d9d4491a", "refinement_interpretation_Tm_refine_6c954f5921079e97ea109e1d11a6a005", "refinement_interpretation_Tm_refine_8480ee3a81184dd8147599debce4b37c", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b" ], 0, "64151c726b3b3da7469f3068a7577fb5" ], [ "Hacl.Impl.Poly1305.Fields.fadd", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Hacl.Impl.Poly1305.Fields.feval", "equation_Hacl.Spec.Poly1305.Vec.fadd", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c70278d6b4b16d65c6072e991d6b1a0", "refinement_interpretation_Tm_refine_5d900e306909cf2b2db001402cc9aef6", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a4e6bb5dde32f7a16c5eadee8a98af83", "refinement_interpretation_Tm_refine_a66521eec4f7a182f6f5cd259df22129", "typing_Spec.Poly1305.size_key" ], 0, "47143e367c700044fd048d53f3552d75" ], [ "Hacl.Impl.Poly1305.Fields.uints64_from_felem_le", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "int_inversion", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "bd7f445e1695b5a82596643a5e67f568" ], [ "Hacl.Impl.Poly1305.Fields.uints64_from_felem_le", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equality_tok_Hacl.Impl.Poly1305.Fields.M128@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M256@tok", "equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Impl.Poly1305.Fields.fas_nat", "equation_Hacl.Impl.Poly1305.Fields.felem", "equation_Hacl.Impl.Poly1305.Fields.felem_fits", "equation_Lib.Buffer.lbuffer_t", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_94399ae43a5eec55136f6ab29239068d", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Spec.Poly1305.size_key" ], 0, "bdeec914596fb859259a748f36462df4" ], [ "Hacl.Impl.Poly1305.Fields.uints64_to_bytes_le", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_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", "equality_tok_Lib.Buffer.MUT@tok", "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.Vec.size_block", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.length", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Spec.AES.elem", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_127", "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_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_Hacl.Spec.Poly1305.Vec.size_block", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "e0291f6211a4f321813bb851fd09d80f" ], [ "Hacl.Impl.Poly1305.Fields.mod_add128", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Poly1305.Vec.size_key", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Poly1305.Vec.size_key" ], 0, "02feb8085e6fafc28f43d5ea05236ea7" ], [ "Hacl.Impl.Poly1305.Fields.mod_add128", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M128", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M256", "constructor_distinct_Hacl.Impl.Poly1305.Fields.M32", "disc_equation_Hacl.Impl.Poly1305.Fields.M128", "disc_equation_Hacl.Impl.Poly1305.Fields.M256", "disc_equation_Hacl.Impl.Poly1305.Fields.M32", "equation_Hacl.Impl.Poly1305.Field32xN.mod_add128", "equation_Hacl.Impl.Poly1305.Fields.limb_v", "equation_Hacl.Spec.Poly1305.Vec.size_key", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Hacl.Impl.Poly1305.Fields.field_spec", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f", "typing_Hacl.Spec.Poly1305.Vec.size_key" ], 0, "55fbe541dd660bd2ede5feb77f6c5e8c" ] ] ]