Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
Test.fst.hints
[
"�p�\u000ft��t峘\u0000����",
[
[
"Test.test_one_aes_ecb",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq",
"assumption_Test.Vectors.block_cipher__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.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Test.Vectors.AES128",
"disc_equation_Test.Vectors.AES256",
"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_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.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.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Test.Vectors.block_cipher",
"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__",
"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_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.lemma_equal_refl", "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.lemma_live_equal_mem_domains",
"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_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_4b807a66ccc2c78e888ecc503feb847b",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Poly1305.size_key", "unit_inversion", "unit_typing"
],
0,
"de8d8be91645eecea4233f26288d8305"
],
[
"Test.test_aes_ecb",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq",
"assumption_Test.Vectors.block_cipher__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",
"disc_equation_Test.Vectors.AES128",
"disc_equation_Test.Vectors.AES256",
"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.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.IntTypes.byte_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint_t",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Test.Vectors.block_cipher",
"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__",
"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_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.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"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_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_4b807a66ccc2c78e888ecc503feb847b",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"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.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Poly1305.size_key", "unit_inversion", "unit_typing"
],
0,
"e497dbce4d8a8fe6cb939645242132a2"
],
[
"Test.aead_key_length32",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.AEAD.AES128_CCM",
"disc_equation_Spec.AEAD.AES128_CCM8",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_CCM",
"disc_equation_Spec.AEAD.AES256_CCM8",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equation_Spec.AEAD.key_length",
"fuel_guarded_inversion_Spec.AEAD.alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"061e9961e1fee0ba1919ff316461ed5a"
],
[
"Test.aead_max_length32",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Prims.nat",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.max_length", "equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Spec.AEAD.alg", "int_inversion",
"int_typing", "lemma_Lib.IntTypes.pow2_values",
"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_5a4fe33be2b93c781e552e491bb9dd31",
"typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
"typing_Spec.AEAD.is_supported_alg", "typing_Spec.Poly1305.size_key"
],
0,
"8a34843c7d8044672bbb76573b25fb9a"
],
[
"Test.aead_tag_length32",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.AES128_CCM",
"constructor_distinct_Spec.AEAD.AES128_CCM8",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_CCM",
"constructor_distinct_Spec.AEAD.AES256_CCM8",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"disc_equation_Spec.AEAD.AES128_CCM",
"disc_equation_Spec.AEAD.AES128_CCM8",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_CCM",
"disc_equation_Spec.AEAD.AES256_CCM8",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.max_length", "equation_Spec.AEAD.tag_length",
"fuel_guarded_inversion_Spec.AEAD.alg",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Lib.IntTypes.pow2_values", "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_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"6c5c269880acacdea96bcaf4f736a5ca"
],
[
"Test.aead_iv_length32",
1,
2,
1,
[ "@query", "equation_Spec.AEAD.iv_length" ],
0,
"6c40e871d1c1127f010211ab39d6d5b1"
],
[
"Test.test_aead_st",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"EverCrypt.Error_pretyping_8d0e43f73f7449fb1ff7df5f9916d609",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_EverCrypt.Error.error_code__uu___haseq",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"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.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"data_typing_intro_EverCrypt.Error.UnsupportedAlgorithm@tok",
"disc_equation_EverCrypt.Error.Success",
"disc_equation_EverCrypt.Error.UnsupportedAlgorithm",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@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",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.freeable",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.Hash.fresh_loc",
"equation_EverCrypt.Hash.loc_in",
"equation_EverCrypt.Hash.loc_unused_in",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Integers.int", "equation_FStar.Integers.int_t",
"equation_FStar.Integers.nat", "equation_FStar.Integers.uint_8",
"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_eternal_color",
"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_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AEAD.ad",
"equation_Spec.AEAD.cipher_length", "equation_Spec.AEAD.encrypted",
"equation_Spec.AEAD.is_supported_alg", "equation_Spec.AEAD.iv",
"equation_Spec.AEAD.iv_length", "equation_Spec.AEAD.key_length",
"equation_Spec.AEAD.lbytes", "equation_Spec.AEAD.max_length",
"equation_Spec.AEAD.plain", "equation_Spec.AEAD.supported_alg",
"equation_Spec.AEAD.tag_length", "equation_Spec.Poly1305.size_key",
"equation_Test.aead_iv_length32", "equation_Test.aead_key_length32",
"equation_Test.aead_max_length32", "equation_Test.aead_tag_length32",
"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_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.Ghost.reveal_hide",
"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_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_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_trans",
"lemma_FStar.Monotonic.HyperHeap.lemma_root_has_color_zero",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Set.lemma_equal_elim", "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.freeable_length",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"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_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"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_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"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_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_091a6051440d321368cc601e573f11a9",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_2fbd657fe85bcb2423f9c7e5f9b3bcb5",
"refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_485808b6c08b8fa1bad00cc3070d942a",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_64be011c479f6ccfad5574a964a1b4aa",
"refinement_interpretation_Tm_refine_67a684ae2cdcea98c0a7a1a09bcb3247",
"refinement_interpretation_Tm_refine_6f61e9633fcfc3b2d29c639586383309",
"refinement_interpretation_Tm_refine_7001d717117afb7669cd45b51ad3dc27",
"refinement_interpretation_Tm_refine_8a88f84ddb86f6a45826b1d92939a27c",
"refinement_interpretation_Tm_refine_95e42645995439c938f8e421d3734b2d",
"refinement_interpretation_Tm_refine_994c3826c4a24c6a403154c52afdad4f",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_9b063033f9f8b075fbdcde91a96a63d9",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ac3c4d67967ef17bb776f78b67f8718d",
"refinement_interpretation_Tm_refine_b132c531406fb8bcf9177da74633fea4",
"refinement_interpretation_Tm_refine_b8c10d9d868d2e33eba75ae3c3181c6f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d05a53820dba3e87ae9544e25b44e9ec",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_dffac3d1ae41d2bd5f028c010022e1ec",
"refinement_interpretation_Tm_refine_ebbcd96e7d0ec6ef1010cd27543b75ae",
"refinement_interpretation_Tm_refine_ebf7f6c1ea25f82a15c5ca7a27fd4468",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0496eb03f3fb51b5e4ca0d53ea58c01",
"refinement_kinding_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"true_interp", "typing_EverCrypt.AEAD.as_kv",
"typing_EverCrypt.AEAD.footprint_s", "typing_EverCrypt.AEAD.state_s",
"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_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.is_stack_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Seq.Base.length", "typing_FStar.Set.complement",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.gte",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.pointer_or_null",
"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.g_is_null",
"typing_LowStar.Monotonic.Buffer.get",
"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_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.mnull", "typing_Prims.pow2",
"typing_Spec.AEAD.encrypt", "typing_Spec.AEAD.is_supported_alg",
"typing_Spec.AEAD.tag_length", "typing_Spec.Poly1305.size_key",
"typing_Test.aead_iv_length32", "typing_Test.aead_key_length32",
"typing_Test.aead_tag_length32",
"typing_tok_Spec.AEAD.AES128_GCM@tok",
"typing_tok_Spec.AEAD.AES256_GCM@tok",
"typing_tok_Spec.AEAD.CHACHA20_POLY1305@tok", "unit_inversion",
"unit_typing"
],
0,
"aed142b9afdec93873b32342db2295fe"
],
[
"Test.alg_of_alg",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Test.Vectors.AES_128_GCM",
"disc_equation_Test.Vectors.AES_256_GCM",
"disc_equation_Test.Vectors.CHACHA20_POLY1305",
"fuel_guarded_inversion_Test.Vectors.cipher"
],
0,
"16f8e694e625a0ad1fbb3cf011579fdc"
],
[
"Test.test_aead_loop",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Test.Vectors_pretyping_2622f4d977f3144ef277eb2601253fe7",
"assumption_FStar.UInt32.t__uu___haseq",
"assumption_Test.Vectors.cipher__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.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"data_typing_intro_Test.Vectors.AES_256_GCM@tok",
"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_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_FStar.HyperStack.ST.equal_stack_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.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint_t",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.l_True",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.Poly1305.size_key", "equation_Test.aead_vector",
"equation_Test.alg_of_alg",
"fuel_guarded_inversion_Test.Vectors.cipher",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Test.aead_vector", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.recallable_mgsub",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "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_0adae6f2ca300a91f2e307caeacdf073",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
"refinement_interpretation_Tm_refine_994c3826c4a24c6a403154c52afdad4f",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.sub",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Spec.AEAD.is_supported_alg", "typing_Spec.Poly1305.size_key",
"typing_Test.alg_of_alg"
],
0,
"bdacb55363e85eded0fe59a3ea72ae6e"
],
[
"Test.test_aes128_gcm_loop",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"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.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.gte",
"equation_FStar.UInt32.gte", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"equation_Spec.AEAD.is_supported_alg",
"equation_Test.Vectors.Aes128Gcm.vectors_len",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_GreaterThanOrEqual",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_156677950ba130498d26fd9f8eb20439",
"refinement_interpretation_Tm_refine_217d1618bb4ef05db330fded6d101472",
"refinement_interpretation_Tm_refine_3aa88e4e00711ba8c4f1aa8f4a373336",
"refinement_interpretation_Tm_refine_67a8a23bbb5aff0c4e8442547959ad02",
"refinement_interpretation_Tm_refine_994c3826c4a24c6a403154c52afdad4f",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_abaa121281c3e9e1623c9cee4c9179ba",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Test.Vectors.Aes128Gcm.vectors",
"typing_Test.Vectors.Aes128Gcm.vectors_len"
],
0,
"aa285c2aee4776cbaeeff24af7b54fde"
],
[
"Test.test_rng",
1,
1,
0,
[
"@query", "equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro"
],
0,
"a56481ce50460ef7631534a6cafaaf3f"
],
[
"Test.test_dh",
1,
1,
0,
[
"@query", "equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro"
],
0,
"a159b549431f0938704cf5b565927563"
],
[
"Test.check_static_config",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Test.BCrypt",
"disc_equation_Test.Hacl", "disc_equation_Test.OpenSSL",
"disc_equation_Test.Vale", "fuel_guarded_inversion_Test.impl",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans"
],
0,
"378dfb379f5e7ff60d51b45b01d9a8cc"
],
[
"Test.set_config",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "assumption_Test.impl__uu___haseq",
"bool_inversion", "constructor_distinct_Test.BCrypt",
"constructor_distinct_Test.Hacl",
"constructor_distinct_Test.OpenSSL",
"constructor_distinct_Test.Vale", "data_elim_Test.Mkfeatures",
"equality_tok_Test.BCrypt@tok", "equality_tok_Test.Hacl@tok",
"equality_tok_Test.OpenSSL@tok", "equality_tok_Test.Vale@tok",
"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",
"fuel_guarded_inversion_Test.features",
"fuel_guarded_inversion_Test.impl",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "primitive_Prims.op_Negation",
"primitive_Prims.op_disEquality",
"proj_equation_Test.Mkfeatures_features_adx",
"proj_equation_Test.Mkfeatures_features_aesni",
"proj_equation_Test.Mkfeatures_features_avx",
"proj_equation_Test.Mkfeatures_features_avx2",
"proj_equation_Test.Mkfeatures_features_bmi2",
"proj_equation_Test.Mkfeatures_features_shaext",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"0dab1ade8ab9fa003eba0c7f7118ac1a"
],
[
"Test.print_config",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"data_elim_Test.Mkfeatures", "disc_equation_Test.BCrypt",
"disc_equation_Test.Hacl", "disc_equation_Test.OpenSSL",
"disc_equation_Test.Vale", "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",
"fuel_guarded_inversion_Test.features",
"fuel_guarded_inversion_Test.impl",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"proj_equation_Test.Mkfeatures_features_adx",
"proj_equation_Test.Mkfeatures_features_aesni",
"proj_equation_Test.Mkfeatures_features_avx",
"proj_equation_Test.Mkfeatures_features_avx2",
"proj_equation_Test.Mkfeatures_features_bmi2",
"proj_equation_Test.Mkfeatures_features_shaext",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "unit_inversion",
"unit_typing"
],
0,
"462f35c50e4fbf06a8f93c211f83afbc"
],
[
"Test.ts_nil",
1,
2,
1,
[
"@query", "equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro"
],
0,
"2dff73f912332ef22af3569a36a44f4b"
],
[
"Test.ts_one",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"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_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"3f2c6dc35be4137c82fd7c23c7ffeed6"
],
[
"Test.ts_append",
1,
2,
1,
[
"@query", "equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt"
],
0,
"d6e977ca013674c4a8387df8e74a49fe"
],
[
"Test.test_poly1305_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"7896fc909cfc0e69bda74de48b314d9c"
],
[
"Test.test_curve25519_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"efb18722114716aac8f8376a39f8652a"
],
[
"Test.test_aead_gcm_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"e6c0a07812929d76d1d3590e04563bcc"
],
[
"Test.test_chacha20poly1305_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"573d924f68315e452de60906805c47d1"
],
[
"Test.test_hash_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_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",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"35f2535ad253667e6b60a04d48f3af51"
],
[
"Test.test_chacha20_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"a83693bf787db5aef15d8a77c05cf63e"
],
[
"Test.test_aes128_ecb_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"3a10ca9590e7b649f84bbd3137e9b4ca"
],
[
"Test.test_aes256_ecb_body",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"7fc185309bac3151fee3af0c2883fae8"
],
[
"Test.print_sep",
1,
2,
1,
[
"@query", "equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro"
],
0,
"e2db69018850501986cf7a90b6f2bcdb"
],
[
"Test.test_all",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"253d86f9f5f2af50be14a1829ca4bfba"
],
[
"Test.main",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equality_tok_C.EXIT_SUCCESS@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"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",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion",
"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_stack_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_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_root_has_color_zero",
"lemma_FStar.Monotonic.HyperHeap.root_is_root",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"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.mem_complement",
"lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_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_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_2fbd657fe85bcb2423f9c7e5f9b3bcb5",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_f0496eb03f3fb51b5e4ca0d53ea58c01",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.sel",
"typing_FStar.Map.upd", "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.singleton",
"typing_tok_C.EXIT_SUCCESS@tok"
],
0,
"4c506b02387b177ec1b3d4b45345fb28"
]
]
]
Computing file changes ...
