Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Test.fst.hints
[
"�\u0011����2��\u0015���",
[
[
"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",
"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_block",
"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", "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_02c3cfb3befa2230fc88750f2d330141",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fe6f89dd2a38b21e35ce94bb12d76f32",
"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_block", "typing_Spec.Poly1305.size_key",
"unit_inversion", "unit_typing"
],
0,
"89549c13dd402d48da2a1facd55f7b9b"
],
[
"Test.test_aes_ecb",
1,
2,
1,
[ "@query" ],
0,
"ec64f1aee752a2bed0a9517cf727ee78"
],
[
"Test.aead_key_length32",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W128",
"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.S8",
"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.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"disc_equation_Spec.Agile.AEAD.AES128_CCM",
"disc_equation_Spec.Agile.AEAD.AES128_CCM8",
"disc_equation_Spec.Agile.AEAD.AES128_GCM",
"disc_equation_Spec.Agile.AEAD.AES256_CCM",
"disc_equation_Spec.Agile.AEAD.AES256_CCM8",
"disc_equation_Spec.Agile.AEAD.AES256_GCM",
"disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305",
"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.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.AES.AES256@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.key_length",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6ce4be029dbcb197811ab25e963c60b7"
],
[
"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.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.S8",
"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.Agile.AEAD.AES128_GCM",
"disc_equation_Spec.Agile.AEAD.AES256_GCM",
"disc_equation_Spec.Agile.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.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Prims.pow2", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred", "typing_Spec.Agile.AEAD.is_supported_alg",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"df9938e6c62067e100eaac08af69ce94"
],
[
"Test.aead_tag_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.S8",
"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.Agile.AEAD.AES128_CCM",
"constructor_distinct_Spec.Agile.AEAD.AES128_CCM8",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_CCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_CCM8",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"disc_equation_Spec.Agile.AEAD.AES128_CCM",
"disc_equation_Spec.Agile.AEAD.AES128_CCM8",
"disc_equation_Spec.Agile.AEAD.AES128_GCM",
"disc_equation_Spec.Agile.AEAD.AES256_CCM",
"disc_equation_Spec.Agile.AEAD.AES256_CCM8",
"disc_equation_Spec.Agile.AEAD.AES256_GCM",
"disc_equation_Spec.Agile.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.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"90b4679ed2d84cea07e5737cb5575ef7"
],
[
"Test.aead_iv_length32",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"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.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.Agile.AEAD.AES128_GCM",
"disc_equation_Spec.Agile.AEAD.AES256_GCM",
"disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.lt",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.AEAD.supported_alg",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.minint", "typing_Spec.AES.gf8",
"typing_Spec.Agile.AEAD.is_supported_alg",
"typing_Spec.Chacha20.size_block", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5f2b4be87d8f96e7699ad6b6483f0b0a"
],
[
"Test.test_aead_st",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"EverCrypt.Error_pretyping_8d0e43f73f7449fb1ff7df5f9916d609",
"assumption_EverCrypt.Error.error_code__uu___haseq",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"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.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"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",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"disc_equation_EverCrypt.Error.Success",
"disc_equation_EverCrypt.Error.UnsupportedAlgorithm",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@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.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES256@tok",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equality_tok_Spec.Agile.AEAD.AES256_GCM@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equation_EverCrypt.AEAD.encrypt_pre",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.freeable",
"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_t",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_heap_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.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "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.fresh_loc",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.AEAD.key_length",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.AEAD.supported_alg",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.AEAD.uint8",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Test.aead_key_length32",
"equation_Test.aead_tag_length32",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"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.Map.lemma_equal_elim",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_trans",
"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",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"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.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"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_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_r",
"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_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",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_166639a1e9653631b1db026395c18076",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"refinement_interpretation_Tm_refine_1d223276e9c55ee48bfc0e7cc503f6dc",
"refinement_interpretation_Tm_refine_200505cd22c7ccd1d9b0d8c31b374c50",
"refinement_interpretation_Tm_refine_2e242ace7be1c0e6e75d0e8e94e79c68",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_37a6e24bb5e5a95de61121e8e2f87cfb",
"refinement_interpretation_Tm_refine_3a6f7bed9d79e58891b00048eb0edb00",
"refinement_interpretation_Tm_refine_3bdcaab5919fd7be76c6f9af6980f791",
"refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4559124c960023d173109014f645d10e",
"refinement_interpretation_Tm_refine_46fe0bc703d469ce7463b60243ffa5fd",
"refinement_interpretation_Tm_refine_4a9f5a632ccb67c4adcfd65a1dab0c7c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5c809a632faab7e2334aee5cd02b19fe",
"refinement_interpretation_Tm_refine_5dd1bcde7192643e78b22b540e036e77",
"refinement_interpretation_Tm_refine_6a57518085fad7634eb7ca72281afbab",
"refinement_interpretation_Tm_refine_6b8af8bc7d435f5cf4dc190216c8db68",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"refinement_interpretation_Tm_refine_cfb9b8efff012a5d01b2c0a9c1ac3ddf",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_ebf7f6c1ea25f82a15c5ca7a27fd4468",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"true_interp", "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.rid_freeable",
"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.mk_mem",
"typing_FStar.Monotonic.HyperStack.pop",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.intersect",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.gte",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned",
"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.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"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.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg",
"typing_Spec.Agile.AEAD.tag_length",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_Test.aead_key_length32", "typing_Test.aead_tag_length32",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Lib.IntTypes.U8@tok",
"typing_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"typing_tok_Spec.Agile.AEAD.AES256_GCM@tok",
"typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "unit_inversion",
"unit_typing"
],
0,
"f738557ef51a45abe06a66618633d15c"
],
[
"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,
"2f7e43f8cd2a895db0faa4ab36f35715"
],
[
"Test.test_aead_loop",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"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.SEC",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.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.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equality_tok_Spec.Agile.AEAD.AES256_GCM@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom",
"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.int_t", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.uint8", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Test.NoHeap.vec8",
"equation_Test.aead_vector", "equation_Test.alg_of_alg",
"fuel_guarded_inversion_Test.Vectors.cipher",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Test.aead_vector", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"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",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"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",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1241abc3ce5aa42f3863ec209735efab",
"refinement_interpretation_Tm_refine_37a6e24bb5e5a95de61121e8e2f87cfb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fe6f89dd2a38b21e35ce94bb12d76f32",
"refinement_interpretation_Tm_refine_ff3f214a1d72a8cdeaa968f7e92cedb4",
"true_interp", "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.AES.gf8",
"typing_Spec.Agile.AEAD.is_supported_alg",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_Test.alg_of_alg"
],
0,
"67de0ddf4129ec047407d9c59c0da1c0"
],
[
"Test.test_aes128_gcm_loop",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.gte",
"equation_FStar.UInt32.gte", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.uint8", "equation_Spec.GaloisField.gf",
"equation_Test.Vectors.Aes128Gcm.vectors_len",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_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.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_217d1618bb4ef05db330fded6d101472",
"refinement_interpretation_Tm_refine_37a6e24bb5e5a95de61121e8e2f87cfb",
"refinement_interpretation_Tm_refine_50b61ad12f37119a11d330eabecd47e4",
"refinement_interpretation_Tm_refine_6ef4215141861f82b9cfe553cb9066e3",
"refinement_interpretation_Tm_refine_7f4123f343358ee4ea27adfd7a4bbc45",
"refinement_interpretation_Tm_refine_b0eb3fe306c2cf932a0b62d367c95146",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Test.Vectors.Aes128Gcm.vectors",
"typing_Test.Vectors.Aes128Gcm.vectors_len"
],
0,
"2b51b6ea5990010eb73a3a8612112585"
],
[
"Test.nonce_bound",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"disc_equation_Spec.Agile.Cipher.CHACHA20", "eq2-interp",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.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_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Agile.Cipher.nonce_bound",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key"
],
0,
"201c55bc8259cbe93b1551cbe19242ca"
],
[
"Test.block_len",
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.U16",
"disc_equation_Spec.Agile.Cipher.CHACHA20",
"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_FStar.UInt.uint_t",
"equation_Spec.Agile.Cipher.block_length",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg", "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_a78e81a34494fa620ef91991a1267b1f",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_Spec.Poly1305.size_key"
],
0,
"9866a9f9028acf1fcb200f4c35945e55"
],
[
"Test.key_len",
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.U16",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"disc_equation_Spec.Agile.Cipher.AES128",
"disc_equation_Spec.Agile.Cipher.AES256",
"disc_equation_Spec.Agile.Cipher.CHACHA20",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.AES.AES256@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Spec.AES.key_size",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Chacha20.size_key", "equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg", "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_a78e81a34494fa620ef91991a1267b1f",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_Spec.Poly1305.size_key"
],
0,
"4276e0182c9cab587a409b67274ea05c"
],
[
"Test.test_ctr_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"EverCrypt.Error_pretyping_8d0e43f73f7449fb1ff7df5f9916d609",
"assumption_EverCrypt.Error.error_code__uu___haseq",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_EverCrypt.Error.Success@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.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_EverCrypt.CTR.footprint",
"equation_EverCrypt.CTR.freeable",
"equation_EverCrypt.CTR.preserves_freeable",
"equation_EverCrypt.CTR.uint8",
"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.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_heap_color",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.live_region",
"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.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.fresh_loc",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.Cipher.block_length",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key",
"equation_Test.block_len", "equation_Test.key_len",
"equation_Test.nonce_bound",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"kinding_Spec.Agile.Cipher.cipher_alg@tok",
"lemma_FStar.Ghost.reveal_hide",
"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_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"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",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"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.lemma_live_equal_mem_domains",
"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_includes_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_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_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_liveness_insensitive_region_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.recallable_mgsub",
"lemma_LowStar.Monotonic.Buffer.region_liveness_insensitive_buffer",
"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",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_3daf37ab3cd19c1e74e63f8f5e0fb16a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42bcfbdc4665a5bd25629f00d56836eb",
"refinement_interpretation_Tm_refine_45363c99d308d619e68ea6909f518151",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_86a3c3bb5e4ab0a42d24322e522d24c1",
"refinement_interpretation_Tm_refine_8a16d9b932ce603163b8347227cc6527",
"refinement_interpretation_Tm_refine_8ac7ca8bf77d5dceafa302ba1e278442",
"refinement_interpretation_Tm_refine_adb7945c1c623355f3ee75d8bbb2183d",
"refinement_interpretation_Tm_refine_b43b16fcb582977fd56f68ee8088c262",
"refinement_interpretation_Tm_refine_bab55dbf24492435d66c6fe7b45c11ec",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_c2c86e2055e02266018938ee0e7acb5a",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d497f167070813c21b13e473f6e89a2a",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e4f8d5a3764d5392df9cc62524caaa7e",
"refinement_interpretation_Tm_refine_e648e65ade6f9ddaa5ecf44de47288b0",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_EverCrypt.CTR.footprint_s",
"typing_EverCrypt.CTR.state_s", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Map.restrict",
"typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.includes",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.rid_freeable",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.mk_mem",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.intersect",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.gte",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.unsigned",
"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.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.mnull", "typing_Spec.AES.gf8",
"typing_Spec.Agile.Cipher.block_length",
"typing_Spec.Agile.Cipher.key_length",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key", "typing_Test.block_len",
"typing_Test.key_len", "typing_Test.nonce_bound",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Lib.IntTypes.U8@tok", "unit_inversion", "unit_typing"
],
0,
"cb492395d5b78ce3985ebf5a25b7bdfd"
],
[
"Test.test_chacha20_ctr_loop",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"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.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.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"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.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"equation_Test.NoHeap.chacha20_vector", "equation_Test.NoHeap.vec8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Test.NoHeap.chacha20_vector", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.Ghost.reveal_hide",
"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_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_trans",
"lemma_FStar.Monotonic.HyperStack.lemma_map_invariant",
"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",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_region_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.recallable_mgsub",
"lemma_LowStar.Monotonic.Buffer.region_liveness_insensitive_buffer",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"primitive_Prims.op_disEquality",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"refinement_interpretation_Tm_refine_4953bdcf9d2d03cbdf85654b9908efb0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_75c29c4e2e4713703ff49d6d3dffcc75",
"refinement_interpretation_Tm_refine_b43b16fcb582977fd56f68ee8088c262",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cc90f5869706e45165cdcef7ec49df25",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_interpretation_Tm_refine_fe6f89dd2a38b21e35ce94bb12d76f32",
"refinement_interpretation_Tm_refine_ff3f214a1d72a8cdeaa968f7e92cedb4",
"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_tip",
"typing_FStar.Set.complement", "typing_FStar.Set.intersect",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"6d06fd142fcc138deb04da4871adf710"
],
[
"Test.test_aes128_ctr_loop",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.UInt.gte",
"equation_FStar.UInt32.gte", "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.length", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Test.Vectors.Aes128.vectors_len",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_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.Monotonic.HyperStack.lemma_tip_top_smt",
"lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_GreaterThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_6ef4215141861f82b9cfe553cb9066e3",
"refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
"refinement_interpretation_Tm_refine_7f4123f343358ee4ea27adfd7a4bbc45",
"refinement_interpretation_Tm_refine_9193be3b823a8a15b7a5724a40378599",
"refinement_interpretation_Tm_refine_a194e7d7a13747924f6808aac22662dc",
"refinement_interpretation_Tm_refine_e4f8d5a3764d5392df9cc62524caaa7e",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Test.Vectors.Aes128.vectors",
"typing_Test.Vectors.Aes128.vectors_len"
],
0,
"e95e2e90efbb85857bb08faaa6df51a0"
],
[
"Test.test_rng",
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,
"9e85b7db2481b730613e448c072fc6d3"
],
[
"Test.test_dh",
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,
"ec9d7473e5f0188d1109e826607f2c55"
],
[
"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,
"ca8db26e78e1eab96d055101f99b929f"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"90d99368ed15a81d75d70414a17c9149"
],
[
"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_05e15190c946858f68c69156f585f95a",
"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,
"60830763a5d780e58bc125fadacfba56"
],
[
"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,
"06446fb40524a2d7363686157b9a0966"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"b86d1aa113ed91e2c59f42376be3f88e"
],
[
"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,
"7b6fefb7a0bcbfa1d5cbca1996aafc7b"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"376fa63ffe110c71e11532ce09d42a88"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"4e25010b9960a5d94b7f1580f637efee"
],
[
"Test.test_aes_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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"f6da4250c1b69931fca0d36c368df908"
],
[
"Test.test_aes_ctr_body",
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,
"d283a0af6a5402ec89af6e747d0916bc"
],
[
"Test.test_chacha20_ctr_body",
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,
"414f6f13b4dc8d425d16e8dcc865eb7c"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"531bd4df7e09837d5df0cb44bbef1606"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"778efbf49fc75ff407ec4c6d28801a0b"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"b4f3cf88cf45064182239eefd28ae90e"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"0322809d90fc688c3b5c77e295eac567"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap"
],
0,
"69e95833fe26e188c70a2d656f6a0f87"
],
[
"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,
"d0d1dc7fe80dc33b3b88b836ed2ef936"
],
[
"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_05e15190c946858f68c69156f585f95a",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"33101f8667600c7b12fc6a2a77cd4ad1"
],
[
"Test.main",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equality_tok_C.EXIT_SUCCESS@tok",
"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_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", "int_inversion",
"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_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.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_Equality",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a",
"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.singleton",
"typing_tok_C.EXIT_SUCCESS@tok"
],
0,
"f812a72288e6af48527349701ad88c0f"
]
]
]
Computing file changes ...
