Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC
1 parent 6055e85
Test.NoHeap.fst.hints
[
"\u001df�F��:�(����E�N",
[
[
"Test.NoHeap.test_many",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ca2c77f69acff4fca0b44c61a9e317a7",
"typing_FStar.UInt32.v"
],
0,
"11075c092e3fb5cd3e419a9d1d032925"
],
[
"Test.NoHeap.test_one_hash",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Integers_pretyping_6ad08c58c10cb742e34ff2d7d8900d61",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_C.String.length",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.v",
"equation_FStar.Integers.width_of_sw",
"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.gte",
"equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte",
"equation_FStar.UInt32.lte",
"equation_Hacl.Hash.Definitions.hash_len",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"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.Monotonic.HyperStack.lemma_mk_mem__projectors",
"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.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_gsub_buffer_l",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"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_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_36c12323dbf231e2a6b4d0836a1ea634",
"refinement_interpretation_Tm_refine_3bc32ff52f2ad4aa1095263abd57fcc6",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4293a786562d45dc658220b2eb3071ba",
"refinement_interpretation_Tm_refine_4b72efbcfb2ff1568cbb1422b6ca3ebb",
"refinement_interpretation_Tm_refine_55573c13df1ad79625a0017d3021d789",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6e3f78b75dbac4079b8eec2087da6bff",
"refinement_interpretation_Tm_refine_71ad6244316202b2672a98012b30c387",
"refinement_interpretation_Tm_refine_814770d986f06f66b84225be16b5517a",
"refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
"refinement_interpretation_Tm_refine_8f712f03d069feed9d20e4f750773c2b",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a8fb943dfab92c446a2ab162c943e447",
"refinement_interpretation_Tm_refine_b246c4889d2e2a782189865824902d78",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c41f648815f5716db7255768e645a3ae",
"refinement_interpretation_Tm_refine_ca2c77f69acff4fca0b44c61a9e317a7",
"refinement_interpretation_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
"refinement_interpretation_Tm_refine_e697ed116974ad298dba48b01c58ccac",
"refinement_interpretation_Tm_refine_e94605b29d4cc479bae8fbe9a0bad584",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"true_interp", "typing_C.String.length", "typing_C.String.strlen",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.upd",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"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.mem",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.add", "typing_FStar.UInt32.div",
"typing_FStar.UInt32.gte", "typing_FStar.UInt32.mul",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Hacl.Hash.Definitions.hash_len",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Chacha20.size_block", "typing_Spec.Chacha20.size_key",
"typing_Spec.Hash.Definitions.hash_length",
"typing_Spec.Hash.Definitions.word_length", "unit_inversion",
"unit_typing"
],
0,
"8f94fc3b24d34016b8a97bdb3325cd46"
],
[
"Test.NoHeap.keysized",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.Integers.int_t",
"equation_FStar.Integers.v", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lte",
"equation_Hacl.Hash.Definitions.block_len",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Chacha20.size_key", "equation_Spec.HMAC.keysized",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_3bc32ff52f2ad4aa1095263abd57fcc6",
"refinement_interpretation_Tm_refine_40ffb9620b727a8620d61ad69490538f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Spec.Chacha20.size_key"
],
0,
"f4c22aad1132f809037fc4c73d346aca"
],
[
"Test.NoHeap.test_one_hmac",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.HMAC.is_supported_alg",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.v",
"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_FStar.UInt.fits", "equation_FStar.UInt.gte",
"equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte",
"equation_FStar.UInt32.lte",
"equation_Hacl.Hash.Definitions.block_len",
"equation_Hacl.Hash.Definitions.hash_len",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.Definitions.word_length",
"equation_Test.NoHeap.keysized",
"equation_Test.NoHeap.supported_hmac_algorithm",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"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.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_complement",
"lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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.modifies_liveness_insensitive_buffer_weak",
"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_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_36c12323dbf231e2a6b4d0836a1ea634",
"refinement_interpretation_Tm_refine_40ffb9620b727a8620d61ad69490538f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4293a786562d45dc658220b2eb3071ba",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_9e5c7dbf3b04f464443f7795127d1b06",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c41f648815f5716db7255768e645a3ae",
"refinement_interpretation_Tm_refine_d1c985f427339d7177502e400dce8e81",
"typing_EverCrypt.HMAC.is_supported_alg",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.upd",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Hacl.Hash.Definitions.hash_len",
"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_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Chacha20.size_block", "typing_Spec.Chacha20.size_key",
"typing_Spec.Hash.Definitions.hash_length",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.max_input_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_Test.NoHeap.keysized", "unit_inversion", "unit_typing"
],
0,
"435b4ceafc8d0db713183ca5cd6d6593"
],
[
"Test.NoHeap.test_one_hkdf",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.HMAC.is_supported_alg",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.v",
"equation_FStar.Integers.width_of_sw",
"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_FStar.UInt.fits", "equation_FStar.UInt.gt",
"equation_FStar.UInt.gte", "equation_FStar.UInt.lte",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt128.n", "equation_FStar.UInt32.gt",
"equation_FStar.UInt32.gte", "equation_FStar.UInt32.lte",
"equation_Hacl.Hash.Definitions.block_len",
"equation_Hacl.Hash.Definitions.hash_len",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.Definitions.word_length",
"equation_Test.NoHeap.keysized",
"equation_Test.NoHeap.supported_hmac_algorithm",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"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.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_complement",
"lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"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_GreaterThan",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_36c12323dbf231e2a6b4d0836a1ea634",
"refinement_interpretation_Tm_refine_37dd275dff73e70469873bca91f7dd14",
"refinement_interpretation_Tm_refine_40ffb9620b727a8620d61ad69490538f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4293a786562d45dc658220b2eb3071ba",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
"refinement_interpretation_Tm_refine_75db076f538e8ed8a7c83c232a30e5c1",
"refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_9e5c7dbf3b04f464443f7795127d1b06",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c41f648815f5716db7255768e645a3ae",
"refinement_interpretation_Tm_refine_d1c985f427339d7177502e400dce8e81",
"refinement_interpretation_Tm_refine_d902bcc6b919bd8fdd4d2858f8998b46",
"refinement_interpretation_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
"true_interp", "typing_EverCrypt.HMAC.is_supported_alg",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.upd",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"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.mem",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt128.n", "typing_FStar.UInt32.add",
"typing_FStar.UInt32.gte", "typing_FStar.UInt32.mul",
"typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Hacl.Hash.Definitions.block_len",
"typing_Hacl.Hash.Definitions.hash_len",
"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_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Chacha20.size_block", "typing_Spec.Chacha20.size_key",
"typing_Spec.Hash.Definitions.max_input_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_Test.NoHeap.keysized", "unit_inversion", "unit_typing"
],
0,
"31a6f926d165a57bf92ee1d58d81775e"
],
[
"Test.NoHeap.test_one_chacha20",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.v",
"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_FStar.UInt.fits", "equation_FStar.UInt.gte",
"equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte",
"equation_FStar.UInt32.lte", "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.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"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.Monotonic.HyperStack.lemma_mk_mem__projectors",
"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.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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.modifies_liveness_insensitive_buffer_weak",
"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_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_35f32262b180572f6a600c5c7951db32",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
"refinement_interpretation_Tm_refine_6e3f78b75dbac4079b8eec2087da6bff",
"refinement_interpretation_Tm_refine_75db076f538e8ed8a7c83c232a30e5c1",
"refinement_interpretation_Tm_refine_812316291234d8a310a2c87c27bfa989",
"refinement_interpretation_Tm_refine_814770d986f06f66b84225be16b5517a",
"refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_d902bcc6b919bd8fdd4d2858f8998b46",
"true_interp", "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.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt.min_int", "typing_FStar.UInt32.add",
"typing_FStar.UInt32.div", "typing_FStar.UInt32.gte",
"typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.loc",
"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.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Chacha20.size_block", "typing_Spec.Chacha20.size_key",
"typing_tok_Lib.Buffer.MUT@tok", "unit_inversion", "unit_typing"
],
0,
"9c7f1a8ded32ec77bd4a3ecb8fc2814f"
],
[
"Test.NoHeap.test_one_poly1305",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"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_FStar.UInt.fits", "equation_FStar.UInt.gte",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.gte", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Poly1305.size_key",
"equation_Spec.Poly1305.to_felem", "equation_Spec.Poly1305.zero",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"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_InDomUpd1", "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.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"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_union",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"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_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_156677950ba130498d26fd9f8eb20439",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4b807a66ccc2c78e888ecc503feb847b",
"refinement_interpretation_Tm_refine_56ab909861a887a471ba68f10063795f",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_abaa121281c3e9e1623c9cee4c9179ba",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0496eb03f3fb51b5e4ca0d53ea58c01",
"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.includes",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"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_FStar.UInt.fits",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.bits",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U32@tok",
"unit_inversion"
],
0,
"7468b1c3a8b1562f990665500f589a44"
],
[
"Test.NoHeap.test_poly1305",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"equation_Test.Vectors.Poly1305.vectors_len",
"kinding_Test.Vectors.Poly1305.vector@tok",
"lemma_FStar.UInt32.uv_inv",
"refinement_interpretation_Tm_refine_3136cc18594a8aacd167f467c60b147a",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Test.Vectors.Poly1305.vectors"
],
0,
"1c63d1e05294383e33ab22496b5fe65e"
],
[
"Test.NoHeap.test_one_curve25519",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"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_FStar.UInt.fits", "equation_FStar.UInt.gte",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.gte", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Poly1305.size_key",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"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_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"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.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"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_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"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_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_156677950ba130498d26fd9f8eb20439",
"refinement_interpretation_Tm_refine_1cb4ed3ac9e4cd01b6ea93696866e9b5",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_583b6dab5523d3a3d1dc2bb9f8527bd7",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_abaa121281c3e9e1623c9cee4c9179ba",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"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.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"fae9f5e18f2a03a9ddcd80d5c15ad425"
],
[
"Test.NoHeap.test_curve25519",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"equation_Test.Vectors.Curve25519.vectors_len",
"kinding_Test.Vectors.Curve25519.vector@tok",
"lemma_FStar.UInt32.uv_inv",
"refinement_interpretation_Tm_refine_27e65b76695997d168a7299f4ee1f89c",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Test.Vectors.Curve25519.vectors"
],
0,
"acac636e346c95d737eaab262193b59b"
],
[
"Test.NoHeap.test_one_chacha20poly1305",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.Helpers.uint8_t",
"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_FStar.UInt.fits", "equation_FStar.UInt.gte",
"equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gte",
"equation_FStar.UInt32.lte", "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.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size", "equation_Lib.IntTypes.uint",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_t",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"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_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"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_union",
"lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_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_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"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_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_156677950ba130498d26fd9f8eb20439",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_3d9d302eb77c7e0f4315c98fe6a09658",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_67a8a23bbb5aff0c4e8442547959ad02",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
"refinement_interpretation_Tm_refine_6e3f78b75dbac4079b8eec2087da6bff",
"refinement_interpretation_Tm_refine_73a2255885f724875aa1dd780e3712c6",
"refinement_interpretation_Tm_refine_814770d986f06f66b84225be16b5517a",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_abaa121281c3e9e1623c9cee4c9179ba",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_cd8943ee2044f75c797c0465a2482c5a",
"refinement_interpretation_Tm_refine_da64955a90615fa75d7a1fa1907da2d6",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Map.restrict",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
"typing_FStar.UInt32.div", "typing_FStar.UInt32.gte",
"typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.size",
"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.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.Chacha20.size_block", "typing_Spec.Poly1305.size_block",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok",
"unit_inversion", "unit_typing"
],
0,
"0c59d8f3cc3c166317ac3be4bcad3ef1"
],
[
"Test.NoHeap.test_chacha20poly1305",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"equation_Test.Vectors.Chacha20Poly1305.vectors_len",
"kinding_Test.Vectors.Chacha20Poly1305.vector@tok",
"lemma_FStar.UInt32.uv_inv",
"refinement_interpretation_Tm_refine_ccdbcf332f874f37b45eb9fabd5200eb",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Test.Vectors.Chacha20Poly1305.vectors"
],
0,
"f5a5004da07fa7596bac4191ce9d4d7a"
],
[
"Test.NoHeap.main",
1,
0,
0,
[ "@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans" ],
0,
"75592daa089fad86d230b2ecb228bb87"
]
]
]
Computing file changes ...
