Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
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,
"8dbfe7b229c94a82782f73fe93ab50e2"
],
[
"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,
"1d492d3edc796737a842cdf47ed629a3"
],
[
"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,
"242060bea1e21cd09264166b5fc58e9e"
],
[
"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,
"b65e93992a168a682051489dda81b7a1"
],
[
"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,
"8caea1fd1a7732ba252411171f4cefcd"
],
[
"EverCrypt.random_init",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.random_init_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"04e72f89a3ed75803110634a8d3383bd"
],
[
"EverCrypt.random_sample",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.random_sample_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"603ccae833c0cc058d4c96be43b5fb2c"
],
[
"EverCrypt.random_cleanup",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.random_cleanup_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"8980b09aa94c66755e4c7c46b5fc99d5"
],
[
"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,
"c543dc7945e24152c5d222fb5fd26f19"
],
[
"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,
"8466b5c14ca55188202b7c60d7ff0b42"
],
[
"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,
"1b1d16ca65dcb2f5d4e00091ea55a924"
],
[
"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,
"d3e2ec94fcdfc447afd86282cb1a0ef4"
],
[
"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,
"46eb2431e6a01ab2af1c28f8c6fbbbe7"
],
[
"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,
"d56601878035483d6f92e3dd745e98f6"
],
[
"EverCrypt.aes128_create",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_create_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"393a13707661b241b4f1f505f9b0d6dc"
],
[
"EverCrypt.aes128_compute",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_compute_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"5d60a3fe7851a09922bbd8a91fe69429"
],
[
"EverCrypt.aes128_free",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_free_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"0366233e1c37da62b775241938020255"
],
[
"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,
"9d67d41e8cb5b604d2c049d11e966eb6"
],
[
"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,
"e30d389f6f7d84cfe621bedd9f38cdeb"
],
[
"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,
"d4aa0baaa91ac4444dbdd663bbc8480a"
],
[
"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,
"1aab7073b7e9ecd0d21752f298207043"
],
[
"EverCrypt.aes256_create",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_create_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"dee81e517a394eefe373611d18e67262"
],
[
"EverCrypt.aes256_compute",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_compute_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"69939d1232d6834def24b04c8134ed3f"
],
[
"EverCrypt.aes256_free",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_free_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"62bdffebbad800b0f45edeaf4c6957d6"
],
[
"EverCrypt.aes128_gcm_encrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_gcm_encrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"dedd9a79b017c400a399c013e9d786b5"
],
[
"EverCrypt.aes128_gcm_decrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes128_gcm_decrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"c6f9f08f2df0205e73f70226a56471bf"
],
[
"EverCrypt.aes256_gcm_encrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_gcm_encrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"28984173fa7878b48d2eec7939613b1d"
],
[
"EverCrypt.aes256_gcm_decrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aes256_gcm_decrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"e60cf105942c7a14ba5d5573aab14e94"
],
[
"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,
"8eab490be6dd65376db507918632eeb2"
],
[
"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,
"993a137b9cbe1d301c02e87f7b361e54"
],
[
"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,
"022e21a182ffe5248f0233b70fd341a8"
],
[
"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,
"a721b39b04245a551cc9cb0ba5be1879"
],
[
"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,
"1b048af698f5eed520474ddca0f8e69d"
],
[
"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,
"1c114340e74b488dc586daea887d6d3a"
],
[
"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,
"14e418b24eb39f431d711a5ecef996a8"
],
[
"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,
"c0a9308eb5eb57abc532a74b62af45d0"
],
[
"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,
"40ba0fbae0202d351440112281fe581d"
],
[
"EverCrypt.aead_create",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_create_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"385f627a1006ef9053d572d1b5f5a3b2"
],
[
"EverCrypt.aead_encrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_encrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"81cf103b293a9d8807859429b4561b02"
],
[
"EverCrypt.aead_decrypt",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_decrypt_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"890e637a01f257eef65baf9e6b615abf"
],
[
"EverCrypt.aead_free",
1,
2,
1,
[
"@query", "equation_EverCrypt.Specs.aead_free_pre",
"equation_FStar.Monotonic.HyperStack.mem"
],
0,
"41e367f3fac1e09192c2cb68af1e97d1"
],
[
"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,
"7804e13b544beb5ca745274469f9cbbd"
],
[
"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,
"d8a14cea0460c4912bd9f7b0e928bcc3"
]
]
]
Computing file changes ...
