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
EverCrypt.fst.hints
[
"\t���\u0017�\u001d\u0014�9��H�?",
[
[
"EverCrypt.vale",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_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_intro",
"lemma_FStar.Set.lemma_equal_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"78423a19d2a1f7fc2800898d12ddc291"
],
[
"EverCrypt.vale_and_aesni",
1,
2,
1,
[
"@query", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"facae7ce8195d45d74f81af9c6b402b2"
],
[
"EverCrypt.hacl",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_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_intro",
"lemma_FStar.Set.lemma_equal_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"3bd7921335e475de379648ac077e595e"
],
[
"EverCrypt.openssl",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_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_intro",
"lemma_FStar.Set.lemma_equal_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"a4261db1f79d9393d5b1089635c99f15"
],
[
"EverCrypt.bcrypt",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.HyperStack.ST.equal_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_intro",
"lemma_FStar.Set.lemma_equal_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_LowStar.Monotonic.Buffer.loc_none"
],
0,
"56a99c346c70f2632096134aeef806d5"
],
[
"EverCrypt.random_init",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.random_init_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"5db8ef611be40511c1844135346e7e23"
],
[
"EverCrypt.random_sample",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.random_sample_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"282a9e3c2749bd2c64a582e9330ad22b"
],
[
"EverCrypt.random_cleanup",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.random_cleanup_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"b95f84d4abee1b2bf3495b52836530bb"
],
[
"EverCrypt.__proj__AES128_OPENSSL__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_OPENSSL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_de76f95304d44a7cdc55d13c0418e50e"
],
0,
"87271c3eab17389750ec2473d0621554"
],
[
"EverCrypt.__proj__AES128_BCRYPT__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_BCRYPT",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_df8fda93347719aef8c7e86c96ea66a8"
],
0,
"32a2c921212566dc74d5e8f6ec58d34d"
],
[
"EverCrypt.__proj__AES128_VALE__item__w",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_VALE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_32a2878ee0af2fa671a8c3199b7c5183"
],
0,
"e11dd6bbb05244455146999b3d5120c1"
],
[
"EverCrypt.__proj__AES128_VALE__item__sbox",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_VALE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_32a2878ee0af2fa671a8c3199b7c5183"
],
0,
"8bbbf03e498d6b25ca1166657fc2783a"
],
[
"EverCrypt.__proj__AES128_HACL__item__w",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_HACL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_f76a370fc2671365c227a2754b4a164a"
],
0,
"c4e5b2bf942f77cc40168a1760187a79"
],
[
"EverCrypt.__proj__AES128_HACL__item__sbox",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_HACL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_f76a370fc2671365c227a2754b4a164a"
],
0,
"a02b35d2023fd3396d7be6748377c8c1"
],
[
"EverCrypt.aes128_create",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_create_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"b7dac28e6b718d26d19cfe0fc0185d16"
],
[
"EverCrypt.aes128_compute",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_compute_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"bde24c7ed39ce976edcc8d6aa31fa836"
],
[
"EverCrypt.aes128_free",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_free_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"9a25d9f47a3c3d9072f84174cd5b5f0a"
],
[
"EverCrypt.__proj__AES256_OPENSSL__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES256_OPENSSL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c322fce0dc68ca7c4d0dcc00419ed3b8"
],
0,
"637fe6f9494a49ad11f48d88e2310c96"
],
[
"EverCrypt.__proj__AES256_BCRYPT__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES256_BCRYPT",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_f255943cc590437cacd9514b959b0e7f"
],
0,
"639e55cf596db56381092eb6901296ae"
],
[
"EverCrypt.__proj__AES256_HACL__item__w",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES256_HACL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d22ca4bb0c28d4ac68af518d80f17814"
],
0,
"bc91bf51fe9c37e76f709b0e0ba687f6"
],
[
"EverCrypt.__proj__AES256_HACL__item__sbox",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES256_HACL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d22ca4bb0c28d4ac68af518d80f17814"
],
0,
"bad364cf8f7652e158393eebfefb93c6"
],
[
"EverCrypt.aes256_create",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_create_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"9ad6c70a4dcdf7a5c4c416724d556f62"
],
[
"EverCrypt.aes256_compute",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_compute_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"936600764a5fa372e323e8d74586a4d4"
],
[
"EverCrypt.aes256_free",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_free_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"e1edda5e3c547fda48011de94fe00a1d"
],
[
"EverCrypt.aes128_gcm_encrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_gcm_encrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"d339d3db58726df302062ecedcd67953"
],
[
"EverCrypt.aes128_gcm_decrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_gcm_decrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"ce2417797dea2c45fbb8bbd7fc794dde"
],
[
"EverCrypt.aes256_gcm_encrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_gcm_encrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"98becf7fbffdfeac26d0fcf35fa8e583"
],
[
"EverCrypt.aes256_gcm_decrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_gcm_decrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"fd53fea82acd32123b59daafe11031e5"
],
[
"EverCrypt.block_cipher_keyLen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_CBC",
"disc_equation_EverCrypt.AES256_CBC",
"disc_equation_EverCrypt.TDES_EDE_CBC",
"fuel_guarded_inversion_EverCrypt.block_cipher_alg"
],
0,
"b20652ddc68c69c3620329e26a141bf8"
],
[
"EverCrypt.block_cipher_blockLen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_CBC",
"disc_equation_EverCrypt.AES256_CBC",
"disc_equation_EverCrypt.TDES_EDE_CBC",
"fuel_guarded_inversion_EverCrypt.block_cipher_alg"
],
0,
"acdad410817966188d7911f8d2f6ea4f"
],
[
"EverCrypt.aead_keyLen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_CCM",
"disc_equation_EverCrypt.AES128_CCM8",
"disc_equation_EverCrypt.AES128_GCM",
"disc_equation_EverCrypt.AES256_CCM",
"disc_equation_EverCrypt.AES256_CCM8",
"disc_equation_EverCrypt.AES256_GCM",
"disc_equation_EverCrypt.CHACHA20_POLY1305",
"fuel_guarded_inversion_EverCrypt.aead_alg"
],
0,
"e5741f04002581c8088bf64f3768ad1e"
],
[
"EverCrypt.aead_tagLen",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AES128_CCM",
"disc_equation_EverCrypt.AES128_CCM8",
"disc_equation_EverCrypt.AES128_GCM",
"disc_equation_EverCrypt.AES256_CCM",
"disc_equation_EverCrypt.AES256_CCM8",
"disc_equation_EverCrypt.AES256_GCM",
"disc_equation_EverCrypt.CHACHA20_POLY1305",
"fuel_guarded_inversion_EverCrypt.aead_alg"
],
0,
"ebfbb2e1abb1853f20d9a84432dbd797"
],
[
"EverCrypt.__proj__AEAD_OPENSSL__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AEAD_OPENSSL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_429db2ca56d5ca45b4b6271a1104396d"
],
0,
"86c056bbcdbb86a784ef513f5ba35850"
],
[
"EverCrypt.__proj__AEAD_BCRYPT__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AEAD_BCRYPT",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_dc2717116fd2b2a46fd5056ab3a249c7"
],
0,
"0ee422cd27e20ccfa01f660bd403131f"
],
[
"EverCrypt.__proj__AEAD_AES128_GCM_VALE__item__xkey",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AEAD_AES128_GCM_VALE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_26970fb3e99b09df8da3de2e7098c049"
],
0,
"24e39513a00c3cd48f8d52780f371a1b"
],
[
"EverCrypt.__proj__AEAD_AES256_GCM_VALE__item__xkey",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AEAD_AES256_GCM_VALE",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_fd2b80e5f412500961f27168f1c9b111"
],
0,
"9a931c24bee5edb5f7fb85f915accdbf"
],
[
"EverCrypt.__proj__AEAD_CHACHA20_POLY1305_HACL__item__k",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.AEAD_CHACHA20_POLY1305_HACL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_bc4635cff0bb12547306e2c0f2d8df0c"
],
0,
"8240abf3f82b819af5f4e775dfa54bcf"
],
[
"EverCrypt.aead_create",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_create_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"c8d902bc6dae8cf6db79474a7bf634e0"
],
[
"EverCrypt.aead_encrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_encrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"1b6d82ff78fb21101c421b76995fdb80"
],
[
"EverCrypt.aead_decrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_decrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"6b94c3f6583805b838d7779d9f7528e2"
],
[
"EverCrypt.aead_free",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_free_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"04bf34404ec05c7ee8e15ba961c0be1c"
],
[
"EverCrypt.__proj__DH_OPENSSL__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.DH_OPENSSL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_25a40ee9963803e731c1c285de47f63d"
],
0,
"8b52a0e5450ee7b68543d88ac26bce5c"
],
[
"EverCrypt.__proj__ECDH_OPENSSL__item__st",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_EverCrypt.ECDH_OPENSSL",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_c1131e08f4406d9afcdc2822ded0cfd1"
],
0,
"e84e761619896a56830b24d871b47f94"
]
]
]
Computing file changes ...
