Revision 1ebe439a4891c708c1f66dd945556fb531d77578 authored by Guido Martínez on 18 March 2020, 01:11:06 UTC, committed by Guido Martínez on 18 March 2020, 01:32:40 UTC
There was previously a bug in `lemma_mult_lt_right` in F*, but now it works as intended.
1 parent 17177ef
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,
"f9baf2a436eab534977a815909138e80"
],
[
"Test.test_aes_ecb",
1,
2,
1,
[ "@query" ],
0,
"d815c5a8238ce3aac30c60f3b23f5411"
],
[
"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,
"e51b177e0b12500b1111b77e09148d0d"
],
[
"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,
"75a158242b95d38b59a464f01bc463eb"
],
[
"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,
"a9c0a5e5813cade256a68d5ecb76e6a5"
],
[
"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,
"9d60b3ff49506641f20176aa28b10993"
],
[
"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,
"bb77009b8ce8b60baf0e72571ceb4bd1"
],
[
"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,
"fa75cbdb9445fba03da8abcc0db72858"
],
[
"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,
"b0c3cd614bba6c0e00e2536c861c9593"
],
[
"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,
"8437c3f1b6ea2fd98d5d2197759e2b84"
],
[
"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,
"b00cf9efa03cff2cf3598288fa1b30f5"
],
[
"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,
"12e78879b0dcead137772a2eecda799e"
],
[
"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,
"417cfd6c760b78025c35987d421aa83c"
],
[
"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,
"c4ec48892f26596a60341d6ed01d4e0a"
],
[
"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,
"496df2ee2fcd1f12be2a129a6fc459ca"
],
[
"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,
"4ffd913016c32036900de99a666b1ab4"
],
[
"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,
"7336709efd6e65af28164e2e0918aebb"
],
[
"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,
"649125a75c40c4019eb33fbe4cffe353"
],
[
"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,
"0c237f1e492113bf766f4b0ff3698253"
],
[
"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,
"dd5eb41f2b29a3dc9040d58e75fc62e8"
],
[
"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,
"0a251f3633fd870a06b0e025325af6d4"
],
[
"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,
"09b65a7b2ac6600d2ac3cc6d70aac5cc"
],
[
"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,
"47c9357d50297697b3a117fa6893588f"
],
[
"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,
"924fd9003a010cc67340ede9fa5f8dde"
],
[
"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,
"c2cb73dea8dd1b29133dc64b39a3e44c"
],
[
"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,
"3564d5b67cd3634060ffba310dfb07f6"
],
[
"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,
"9e6c41882268fa57ae2e3f88700401ce"
],
[
"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,
"7d32e5804e9fe88911edaddec840ec8c"
],
[
"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,
"5e63971026a1ab062d085107a573f8c4"
],
[
"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,
"8db9500e75985baa740bb6ba0c8fa1d1"
],
[
"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,
"19715395eaee67512553f85db4e79213"
],
[
"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,
"28d95599ac622c677f9e24da683dc1d8"
],
[
"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,
"fbc4e186e8b5d4c55c321fe6869825d3"
],
[
"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,
"e7da7cdcb9f70111fea285ad3770e82a"
],
[
"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,
"69b70e09f2945a1cd4bd886177280205"
],
[
"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,
"2d686bcc6a81ef4659fbe9beb833eeb8"
]
]
]
Computing file changes ...
