[
"\u0012X��\u0018/�O^j^\u0000\u0006\u0007�",
[
[
"Test.Bytes.test_chacha20_poly1305",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_BarBar", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Test.Bytes_Tm_refine_d656a7e1bdf9ea987654e40b6ce6dd5b",
"refinement_interpretation_Test.Bytes_Tm_refine_e6e3f7c1f800390e5f198e21f3a0bf39",
"refinement_interpretation_Test.Lowstarize_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"f3cf7c42439ae0987d2e329af04115c2"
],
[
"Test.Bytes.test_aead",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_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.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"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_Test.Bytes.aead_vector",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool",
"function_token_typing_Test.Bytes.aead_vector", "int_inversion",
"interpretation_LowStar.Buffer_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_non_tip_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1",
"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.mem_complement",
"lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Test.Bytes_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Test.Bytes_Tm_refine_6e827fe2e5356b616dbd0cec1bc6fc28",
"refinement_interpretation_Test.Bytes_Tm_refine_bfc946b4b16c3b52a8c9d72b00b5b32b",
"refinement_interpretation_Test.Bytes_Tm_refine_ca2c77f69acff4fca0b44c61a9e317a7",
"refinement_interpretation_Test.Bytes_Tm_refine_fee4d47786f2acf99bc14199ca24e2b8",
"refinement_interpretation_Test.Lowstarize_Tm_refine_0adae6f2ca300a91f2e307caeacdf073",
"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.singleton",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"5b53fe10f60e271b8097e3aefbd33794"
],
[
"Test.Bytes.main",
1,
0,
0,
[ "@query" ],
0,
"fdf55ff6536ee64d9bdd3aa56103b693"
]
]
]
