[ "d\u0010\u0002.UQuFg", [ [ "Hacl.Bignum.bn_add1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "da7cb7e024f29cf5f9403645e3a90649" ], [ "Hacl.Bignum.bn_add1", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_add1", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "3dad088f9fbfc0313d0f45cdf84ff759" ], [ "Hacl.Bignum.bn_sub1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4db475f6b11a521a5809419ef67b7a8e" ], [ "Hacl.Bignum.bn_sub1", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_sub1", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "7ecf143984f0f69ad4fae2793dfbd91b" ], [ "Hacl.Bignum.bn_add_eq_len_st", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "194fd2b2169809b71c6354616cc0b2ff" ], [ "Hacl.Bignum.bn_add_eq_len", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Addition.bn_add", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.bn_add", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.sub", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e4a558bf8088cf1bfd1450f0d83deb67" ], [ "Hacl.Bignum.bn_sub_eq_len_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "13eb1035e74e3cde57f9551f1d489404" ], [ "Hacl.Bignum.bn_sub_eq_len", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Addition.bn_sub", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.bn_sub", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "function_token_typing_FStar.Monotonic.Heap.heap", "int_inversion", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.sub", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "2799993757796e7b53abf6f9cad4ee3a" ], [ "Hacl.Bignum.bn_add", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_dd894954154c0efc25ea48b66d8a9bbf", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "73ee0e3c9b7ac87b1a5c887a1aab4ae0" ], [ "Hacl.Bignum.bn_add", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.Addition.bn_add", "equation_Hacl.Spec.Bignum.Base.carry", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.bn_add", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "00238a795573c1c4b5123efc3f19833b" ], [ "Hacl.Bignum.bn_sub", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_dd894954154c0efc25ea48b66d8a9bbf", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c4fad9e054c9e5193d982f488e2861dc" ], [ "Hacl.Bignum.bn_sub", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.Addition.bn_sub", "equation_Hacl.Spec.Bignum.Base.carry", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.bn_sub", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2" ], 0, "1b086e840de8da6899c58d64b229e3d1" ], [ "Hacl.Bignum.bn_reduce_once", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "0c4da4b2b820dfa76d206add86388935" ], [ "Hacl.Bignum.bn_reduce_once", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "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", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Base.carry", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_reduce_once", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "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_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2ea832f400aac2b6ab9d69ced5ee0c11", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_738752d165bb8861f915c64da4c33cee", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8507969383ab88e2a151843b178d6b42", "refinement_interpretation_Tm_refine_9c7687f042133ab0c6f674a635e3f076", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "3810b2a05ef0b7c760954028e5128050" ], [ "Hacl.Bignum.bn_add_mod_n_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8f8f243511c31355da04938e58b8e05e" ], [ "Hacl.Bignum.bn_add_mod_n", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.Buffer.MUT", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_add_mod_n", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "refinement_interpretation_Tm_refine_2ea832f400aac2b6ab9d69ced5ee0c11", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.loc", "typing_LowStar.Buffer.trivial_preorder", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "6d1c2ba28f2c75cd19e8154c89c52225" ], [ "Hacl.Bignum.bn_sub_mod_n_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "814ad29f33d07691023c3ff1a8897442" ], [ "Hacl.Bignum.bn_sub_mod_n", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "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", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Base.carry", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_sub_mod_n", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Negation", "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_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_35dfca096d5bc45e3dc1fcd3f9c0a8c5", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8507969383ab88e2a151843b178d6b42", "refinement_interpretation_Tm_refine_9c7687f042133ab0c6f674a635e3f076", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.sel", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "1e17276fa54c485f2baad30b23111205" ], [ "Hacl.Bignum.bn_mul1", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e00c843de2ee8922c7a25f3c3ef61426" ], [ "Hacl.Bignum.bn_mul1", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_mul1", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "refinement_interpretation_Tm_refine_5327649b3d32f10c0e209c64bebe9967", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_bf8dcbc23ba62c6eaf0e4749e3f0d5e6", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "0712fdb39aa014755bb60dacdecf5c19" ], [ "Hacl.Bignum.bn_karatsuba_mul_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "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_Lib.IntTypes.maxint", "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", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "55c04de517d462823a56cd879c1b8f12" ], [ "Hacl.Bignum.bn_karatsuba_mul", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "2d70174750ce795509c96d891f30c65e" ], [ "Hacl.Bignum.bn_karatsuba_mul", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_karatsuba_mul", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a" ], 0, "5188c0f29f49a034603f4d974bbe13c5" ], [ "Hacl.Bignum.bn_mul_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2f1e932fa1e93c406800b418feeca6e3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "0c7fc9b78bccdbc68cdf7cafb4b1ba34" ], [ "Hacl.Bignum.bn_mul", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Lib.Buffer.lbuffer_t", "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_Prims.nat", "function_token_typing_Lib.IntTypes.uint64", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2f1e932fa1e93c406800b418feeca6e3", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "99162691db997b121aa08c6c7a73799d" ], [ "Hacl.Bignum.bn_mul", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_mul", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "83b431c12b2eeb4cef8b1ca09e328ac7" ], [ "Hacl.Bignum.bn_karatsuba_sqr_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "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_Lib.IntTypes.maxint", "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", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e5353f02f8d99b652f9373c9138d5d3f" ], [ "Hacl.Bignum.bn_karatsuba_sqr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "29800dba444c0b8ab1b78fe38169fcb0" ], [ "Hacl.Bignum.bn_karatsuba_sqr", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_karatsuba_sqr", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_692121769a46bb8926d59b8ca3cd043a" ], 0, "f2ca6737d469e704d62bd07f696b5a80" ], [ "Hacl.Bignum.bn_sqr_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_ad5c1623934a11c8d7877f0adfe0f6fc", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "724551dd890072d103d9db5691e6d6ff" ], [ "Hacl.Bignum.bn_sqr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_ad5c1623934a11c8d7877f0adfe0f6fc", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "daa016862e759c97f089a2993a9d4574" ], [ "Hacl.Bignum.bn_sqr", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_sqr", "equation_Lib.IntTypes.v", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_ad5c1623934a11c8d7877f0adfe0f6fc" ], 0, "cf8ae8d8bc701a34e33fd71fbd5e38e2" ], [ "Hacl.Bignum.bn_mul1_lshift_add_in_place", 1, 0, 0, [ "@MaxIFuel_assumption", "@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.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "primitive_Prims.op_Addition", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_65c10f95049b68e16da55bde39a0ae86", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8143932c42afa05dd884850c296ffba5" ], [ "Hacl.Bignum.bn_mul1_lshift_add_in_place", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_mul1_lshift_add", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "5de05bc1f421600769471ab0f7857fcc" ], [ "Hacl.Bignum.bn_rshift", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Lib.Buffer.lbuffer_t", "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_Prims.nat", "function_token_typing_Lib.IntTypes.uint64", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "201212a222183d35e648d22c806071a1" ], [ "Hacl.Bignum.bn_rshift", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a59cca81a4df745d6d279734c54987b7" ], [ "Hacl.Bignum.bn_rshift", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "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.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Lib.bn_div_pow2", "equation_Hacl.Spec.Bignum.bn_rshift", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies1", "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.Sequence.slice", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "lemma_Lib.Buffer.as_seq_gsub", "lemma_Lib.IntTypes.sub_lemma", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_", "primitive_Prims.op_Addition", "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_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8f116650038cb4d28e9a3fe457286927", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "1b908eb04c4ea3f4bbe40e9b624590b7" ], [ "Hacl.Bignum.bn_sub_mask", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.S128", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "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.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Addition.bn_sub", "equation_Hacl.Spec.Bignum.Base.carry", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_sub_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.Buffer.bget_as_seq", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_00c9bc5043eb53390cc6a38dc4943559", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2ea832f400aac2b6ab9d69ced5ee0c11", "refinement_interpretation_Tm_refine_2ef8f43a290174b3a89dd42b03d028a5", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_5327649b3d32f10c0e209c64bebe9967", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6730a98db0fc2fce0c450da579d1b7b1", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8507969383ab88e2a151843b178d6b42", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a6a6223131bb8839e400e35c336c3854", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d13c5132af51f62dfb7018a438f66ab7", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e9e7bf8f4d2fe07860f799fa2a4ea81c", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.ByteSequence.seq_eq_mask", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.sub", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "73b8052ad024c577e0bc34e67bff8017" ], [ "Hacl.Bignum.bn_sub_mask", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Lib.IntTypes.S128", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "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.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Addition.bn_sub", "equation_Hacl.Spec.Bignum.Base.carry", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_sub_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint32", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.Buffer.bget_as_seq", "lemma_Lib.IntTypes.v_injective", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_00c9bc5043eb53390cc6a38dc4943559", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2ea832f400aac2b6ab9d69ced5ee0c11", "refinement_interpretation_Tm_refine_2ef8f43a290174b3a89dd42b03d028a5", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_5327649b3d32f10c0e209c64bebe9967", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6730a98db0fc2fce0c450da579d1b7b1", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8507969383ab88e2a151843b178d6b42", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a6a6223131bb8839e400e35c336c3854", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d13c5132af51f62dfb7018a438f66ab7", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e9e7bf8f4d2fe07860f799fa2a4ea81c", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.ByteSequence.seq_eq_mask", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.create", "typing_Lib.Sequence.sub", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "17c0c1fff37d3c0a16305e81e775f5e9" ], [ "Hacl.Bignum.bn_get_ith_bit", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "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_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "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_20041da81ea68980c160f95ec3014015", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ca5b9e728b36ec473b6229b6e81cd498" ], [ "Hacl.Bignum.bn_get_ith_bit", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "a38e8b74e2be0116d91ea368009a2cbc" ], [ "Hacl.Bignum.bn_get_ith_bit", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_get_ith_bit", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "e0c04b5c836bb6730f14d5ad1baa88d3" ], [ "Hacl.Bignum.bn_get_bits", 1, 0, 0, [ "@MaxIFuel_assumption", "@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.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "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_26063e8f5832ae97bf1d9753b5b741be", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "325d922366cdfed33934cada19c951c8" ], [ "Hacl.Bignum.bn_get_bits", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "4f4a3b0d9029ecde986ef1ecb3c87bf9" ], [ "Hacl.Bignum.bn_get_bits", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_get_bits", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "becc7c2076334631c65119762c1d854c" ], [ "Hacl.Bignum.bn_set_ith_bit", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "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_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "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_20041da81ea68980c160f95ec3014015", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "7c609e671901c129b0f7a0c45f11a4ab" ], [ "Hacl.Bignum.bn_set_ith_bit", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "98f2f4bccfafbece488dd8a7926731c2" ], [ "Hacl.Bignum.bn_set_ith_bit", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_set_ith_bit", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "18f6d13bb2116223fa9bec159bce9e5f" ], [ "Hacl.Bignum.cswap2", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.v", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ddf90c0656799c8d60d94ddf1a0c8eb7" ], [ "Hacl.Bignum.cswap2", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.cswap2", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "0084ec3d18f00e2b6d812e5f456315f2" ], [ "Hacl.Bignum.bn", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Bignum.meta_len", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "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", "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_06eb4f1fa9612b97cc2b633a94839814", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "dbf98e09fdf1e940780146bc7ab92e72" ], [ "Hacl.Bignum.__proj__Mkbn__item__add", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_b704b54cd4b720c3c05be1fd667649db" ], 0, "b282a63f4c1cc2fd94923d10e761b2d6" ], [ "Hacl.Bignum.__proj__Mkbn__item__sub", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_6740e6b39a1a59b2160f9c68c24e3a76", "refinement_interpretation_Tm_refine_b704b54cd4b720c3c05be1fd667649db" ], 0, "b7e3e2b6d60f8a021e5d8521a2eead24" ], [ "Hacl.Bignum.__proj__Mkbn__item__add_mod_n", 1, 0, 0, [ "@query" ], 0, "7b0eb205e398af01b9fa89df63c254dd" ], [ "Hacl.Bignum.__proj__Mkbn__item__add_mod_n", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_e0ab8a8974e5b3a9101c38b7001ed683" ], 0, "ac33edf31944f5cba722d6870b1393f4" ], [ "Hacl.Bignum.__proj__Mkbn__item__sub_mod_n", 1, 0, 0, [ "@query" ], 0, "e5e03d2707eb8e5e22170cd5decb7629" ], [ "Hacl.Bignum.__proj__Mkbn__item__sub_mod_n", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_e0ab8a8974e5b3a9101c38b7001ed683" ], 0, "d3794ebe29b97dcab3f1840853d03de3" ], [ "Hacl.Bignum.__proj__Mkbn__item__mul", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_typing", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "f4888e3cfc0d0707d61a4a992543e0df" ], [ "Hacl.Bignum.__proj__Mkbn__item__mul", 2, 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Bignum.meta_len", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "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", "fuel_guarded_inversion_Hacl.Bignum.bn", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Bignum.Mkbn_len", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Bignum.Mkbn_len", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_06eb4f1fa9612b97cc2b633a94839814", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6065f173033e10a9ea94570e4e669b17", "refinement_interpretation_Tm_refine_81c7ef7d641d62c76efdc13fe91209b8", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.__proj__Mkbn__item__len", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "783b2e8d53218773e881ccf33dd60004" ], [ "Hacl.Bignum.__proj__Mkbn__item__sqr", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_typing", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "02e55a875dbd1bc882689523e4de10cd" ], [ "Hacl.Bignum.__proj__Mkbn__item__sqr", 2, 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Bignum.meta_len", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "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", "fuel_guarded_inversion_Hacl.Bignum.bn", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.Bignum.Mkbn_len", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Hacl.Bignum.Mkbn_len", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_06eb4f1fa9612b97cc2b633a94839814", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.__proj__Mkbn__item__len", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "22f6ecdcb0e54209570e3d0e7acd3d5e" ], [ "Hacl.Bignum.add_mod_n", 1, 0, 0, [ "@query" ], 0, "feef93e68df4fb2ecb24c0d953f9c6ff" ], [ "Hacl.Bignum.sub_mod_n", 1, 0, 0, [ "@query" ], 0, "317bf57e544cdcc6ff825f8b21528961" ], [ "Hacl.Bignum.mul", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_typing", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "fde3bb52d97ddcd49f8c9eb6785dd07a" ], [ "Hacl.Bignum.sqr", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_typing", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "9ced6517a9f5434a1297a51ad3cc893d" ], [ "Hacl.Bignum.bn_add_mod_n_", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_65f79c29d7aa53771b1f973ceba3ebbf", "refinement_interpretation_Tm_refine_77232eeb9423c787761ffdf1fa7d56d9", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "bf374fece2336c5684f9dcd8cb43de97" ], [ "Hacl.Bignum.bn_sub_mod_n_", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_65f79c29d7aa53771b1f973ceba3ebbf", "refinement_interpretation_Tm_refine_77232eeb9423c787761ffdf1fa7d56d9", "refinement_interpretation_Tm_refine_825fe1ce5d530067039356208bd82ad4", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92" ], 0, "4c024af30f47a3831d895740510bbdac" ], [ "Hacl.Bignum.mk_runtime_bn", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "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.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Bignum.meta_len", "equation_Hacl.Spec.Bignum.Addition.bn_add", "equation_Hacl.Spec.Bignum.Addition.bn_sub", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_add", "equation_Hacl.Spec.Bignum.bn_sub", "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.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt.pow2_values", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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_06eb4f1fa9612b97cc2b633a94839814", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.sub", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8c9e3748fc56306229670f61c4fd56c9" ], [ "Hacl.Bignum.mk_runtime_bn_len_lemma", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.mk_runtime_bn", "equation_Hacl.Bignum.mk_runtime_bn_u32", "equation_Hacl.Bignum.mk_runtime_bn_u64", "fuel_guarded_inversion_Hacl.Bignum.bn", "proj_equation_Hacl.Bignum.Mkbn_len", "projection_inverse_Hacl.Bignum.Mkbn_len", "typing_Hacl.Bignum.mk_runtime_bn" ], 0, "63df04293cf1b47ff7bdd7ca67b56468" ], [ "Hacl.Bignum.bn_is_odd", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947" ], 0, "c397890db5d35cde7636373c2f7c11ee" ], [ "Hacl.Bignum.bn_is_odd", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_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.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.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.eq", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.eq", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.bn_is_odd", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies0", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.gt_lemma", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_8cc8cfcb64d575010750a5c00af3e912", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "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.minint", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "719204cf9a9b17014ec5d5169039bf7f" ], [ "Hacl.Bignum.bn_eq_mask_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "39aec6e7f38f04d292d1b93c282b42fd" ], [ "Hacl.Bignum.bn_eq_mask", 1, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_eq_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "e6b9ea22e5455c93d0a0595fe9559081" ], [ "Hacl.Bignum.bn_is_zero_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947" ], 0, "0790b85de72be92a1f414bb148ae1795" ], [ "Hacl.Bignum.bn_is_zero_mask", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_is_zero_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "54ea9694d5145ff374b8315986153880" ], [ "Hacl.Bignum.bn_lt_mask_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "equation_Prims.nat", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "1d558a86906dcde6e0e3dc9fdafa461e" ], [ "Hacl.Bignum.bn_lt_mask", 1, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_lt_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "adb984171bc8bb3d37ec9bbf1b8e6229" ], [ "Hacl.Bignum.bn_lt_pow2_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "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_Lib.IntTypes.maxint", "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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_33847aeea1e1f6a30128d1c29277c83f", "refinement_interpretation_Tm_refine_4f32bc7da14f02bd3360820d3a0b92a4", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "578a3ee792291aa2126bef6ba7cf0643" ], [ "Hacl.Bignum.bn_lt_pow2_mask", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_lt_pow2_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "547042948c5dd1b7af5dc2edb22e1958" ], [ "Hacl.Bignum.bn_gt_pow2_mask", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "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_Lib.IntTypes.maxint", "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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_33847aeea1e1f6a30128d1c29277c83f", "refinement_interpretation_Tm_refine_4f32bc7da14f02bd3360820d3a0b92a4", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "a3eedd6e8dfd2b423eb772a4baca8ae7" ], [ "Hacl.Bignum.bn_gt_pow2_mask", 2, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_gt_pow2_mask", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "c68fc4c6f735833b4a983a41b20f996e" ], [ "Hacl.Bignum.bn_from_uint", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.v", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "941573093cfdf9a59d6c2e7be7333260" ], [ "Hacl.Bignum.bn_from_uint", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.bn_from_uint", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.upd_slice", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.sub_lemma", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_4fe0f7e228a856d0575495f6b377ee05", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8cc8cfcb64d575010750a5c00af3e912", "refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e9c32a5fb00a4e8c339597118c871180", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.gsub", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.sub", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.upd", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.len", "typing_Prims.pow2", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "8bac8adfffb019a06a4e179b473f067d" ], [ "Hacl.Bignum.bn_from_bytes_be", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "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_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_834039b9477f844fb4d2de05cf4e8b52", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d9e7fe75f44ca6257c29894936451ecb" ], [ "Hacl.Bignum.bn_from_bytes_be", 2, 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "1f8bebde39e107e58fa38670be67e219" ], [ "Hacl.Bignum.bn_from_bytes_be", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_from_bytes_be", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "dbb5c3c3ddfb4e285e9b2ff959b55efa" ], [ "Hacl.Bignum.bn_to_bytes_be", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "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_3b30e5cbbdc74f89ea2da23758cc9b99", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "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, "39b8392adef93ae5a0c3de194bafc504" ], [ "Hacl.Bignum.bn_to_bytes_be", 2, 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "24ab436a12d7cc287378023d552faa82" ], [ "Hacl.Bignum.bn_to_bytes_be", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_to_bytes_be", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "8732233365e4777d110494bdf9b45a82" ], [ "Hacl.Bignum.bn_from_bytes_le", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "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_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.lbignum", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_834039b9477f844fb4d2de05cf4e8b52", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.limb", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "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.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ce43dce3d3d51230fb017ce991ae7875" ], [ "Hacl.Bignum.bn_from_bytes_le", 2, 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b87599f6791a74ea0cd4073f9dbc4220" ], [ "Hacl.Bignum.bn_from_bytes_le", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_from_bytes_le", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "60b6cbc9689c469142a9e66612b84fe1" ], [ "Hacl.Bignum.bn_to_bytes_le", 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.blocks", "equation_Hacl.Bignum.Definitions.limb", "equation_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "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_3b30e5cbbdc74f89ea2da23758cc9b99", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56718590fe22c020c437a3dfde0cee6b", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Hacl.Bignum.Definitions.blocks", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.numbytes", "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, "b4b092ba8d21e971d351e6edf69ad31d" ], [ "Hacl.Bignum.bn_to_bytes_le", 2, 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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "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_Hacl.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "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", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.numbytes", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3f43b594622d1b03eb8b18c02bfeb7e1" ], [ "Hacl.Bignum.bn_to_bytes_le", 3, 0, 0, [ "@query", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.bn_to_bytes_le", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.v" ], 0, "844bb1511a32e67c90ef08f9efd8e0ad" ] ] ]