Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Test.Vectors.Chacha20Poly1305.fst.hints
[
"&��;\u001e���Í'���ٚ",
[
[
"Test.Vectors.Chacha20Poly1305.key0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"7d3b9d847c212ba130776e07ce28e8ff"
],
[
"Test.Vectors.Chacha20Poly1305.key0_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key0"
],
0,
"173549a421338b5d6b48e10160437900"
],
[
"Test.Vectors.Chacha20Poly1305.nonce0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"ac453cb97c6520a6a0a0f9609e2ef8ac"
],
[
"Test.Vectors.Chacha20Poly1305.nonce0_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce0"
],
0,
"f338ef544a0e6d264d113a58ce7241a6"
],
[
"Test.Vectors.Chacha20Poly1305.aad0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"745a581b03aec4175570a4ef5226b9b9"
],
[
"Test.Vectors.Chacha20Poly1305.aad0_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.aad0"
],
0,
"f358bdaa3d0ac49839ce626014b4cfb6"
],
[
"Test.Vectors.Chacha20Poly1305.input0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2797cd56f154d6a19fec80698b47b6b5",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad0"
],
0,
"6e187e97c7faeaaf8fbc62823d6bb8b4"
],
[
"Test.Vectors.Chacha20Poly1305.input0_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_1851140a5a9d6bf151cff94e730d2ede",
"typing_Test.Vectors.Chacha20Poly1305.input0"
],
0,
"26006ab6287e566c2ddcfb42815fadcd"
],
[
"Test.Vectors.Chacha20Poly1305.output0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1680ab71baf816a11a1cd1dcfe6d64c0",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"228938af0ec4a054f8c65683bad075e0"
],
[
"Test.Vectors.Chacha20Poly1305.output0_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d52561b7d3766f37a92500f68cfb8cc8",
"typing_Test.Vectors.Chacha20Poly1305.output0"
],
0,
"659eb6c0f45ee52accc782b420f4d4de"
],
[
"Test.Vectors.Chacha20Poly1305.key1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"0bf971bfc68461bafb2c7efa3ead6476"
],
[
"Test.Vectors.Chacha20Poly1305.key1_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key1"
],
0,
"78d1c73b0cc27b42bccf1fcecb65da80"
],
[
"Test.Vectors.Chacha20Poly1305.nonce1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"4d3b512fd528e4fad9769a3ade0332a4"
],
[
"Test.Vectors.Chacha20Poly1305.nonce1_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce1"
],
0,
"a5d02a7f34395102a6ca2ee35302f134"
],
[
"Test.Vectors.Chacha20Poly1305.aad1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"e0ff8e43a8f642426a8ae163b76caf3e"
],
[
"Test.Vectors.Chacha20Poly1305.aad1_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"typing_Test.Vectors.Chacha20Poly1305.aad1"
],
0,
"27c95e065c14cc1e5157249f071e8f43"
],
[
"Test.Vectors.Chacha20Poly1305.input1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_FStar.UInt.min_int", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a72e4f0f5620bd118d5609c286d5f4b8",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad1"
],
0,
"11d7b04286f5a8f7323dae0b09755f35"
],
[
"Test.Vectors.Chacha20Poly1305.input1_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_5dccf04464b669d881c826e935365436",
"typing_Test.Vectors.Chacha20Poly1305.input1"
],
0,
"8189e4ca92dda75246931821033028de"
],
[
"Test.Vectors.Chacha20Poly1305.output1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_da79c9363cdb5abcffa152eada6a861f",
"typing_FStar.Map.contains", "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_tip"
],
0,
"3e2d58e5be52759f947fca5cb614ca75"
],
[
"Test.Vectors.Chacha20Poly1305.output1_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_7e594ad2af0f3614996ce396263cb36e",
"typing_Test.Vectors.Chacha20Poly1305.output1"
],
0,
"22839497da07e229d280097eb6f82030"
],
[
"Test.Vectors.Chacha20Poly1305.key2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"4481202a81a598fdd28f4dd0df3929ae"
],
[
"Test.Vectors.Chacha20Poly1305.key2_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key2"
],
0,
"d091e754764b1a592b1d7750670d7dc7"
],
[
"Test.Vectors.Chacha20Poly1305.nonce2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"e3d4588fed76aa03e14fd7120070b9bd"
],
[
"Test.Vectors.Chacha20Poly1305.nonce2_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce2"
],
0,
"d2d7fdecee0895405e69eb065063119b"
],
[
"Test.Vectors.Chacha20Poly1305.aad2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_f6bacda43435b7375ee04d185a218f51",
"typing_FStar.Map.contains", "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_tip"
],
0,
"4b712d6b6460d59f4065b66f332a40ab"
],
[
"Test.Vectors.Chacha20Poly1305.aad2_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_2f657d06ee5fc775edea771370ee385a",
"typing_Test.Vectors.Chacha20Poly1305.aad2"
],
0,
"c6fbf3589b4b49c2a1c5fd4f9f327766"
],
[
"Test.Vectors.Chacha20Poly1305.input2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2f657d06ee5fc775edea771370ee385a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_a72e4f0f5620bd118d5609c286d5f4b8",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad2"
],
0,
"42f0b53dad528a9b725df1fbc70ec2b5"
],
[
"Test.Vectors.Chacha20Poly1305.input2_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_af30b58a8dea5dcae248698ebc4240ec",
"typing_Test.Vectors.Chacha20Poly1305.input2"
],
0,
"03ae29e98017d8ba77be77bc18cfda30"
],
[
"Test.Vectors.Chacha20Poly1305.output2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_da79c9363cdb5abcffa152eada6a861f",
"typing_FStar.Map.contains", "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_tip"
],
0,
"1af76af684dce5616b5ca76609096505"
],
[
"Test.Vectors.Chacha20Poly1305.output2_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_7e594ad2af0f3614996ce396263cb36e",
"typing_Test.Vectors.Chacha20Poly1305.output2"
],
0,
"ae945a09e490324cb459bd159b613c45"
],
[
"Test.Vectors.Chacha20Poly1305.key3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"0e4afdd9de5fdaf9dad3845ad7afb89a"
],
[
"Test.Vectors.Chacha20Poly1305.key3_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key3"
],
0,
"20e4475a53224634bed777fbb00a8e2a"
],
[
"Test.Vectors.Chacha20Poly1305.nonce3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"ecc77d765acda994aab92671f6306e55"
],
[
"Test.Vectors.Chacha20Poly1305.nonce3_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce3"
],
0,
"ba09e73f19c8fe76c501b9b83aa4bbfd"
],
[
"Test.Vectors.Chacha20Poly1305.aad3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_f6bacda43435b7375ee04d185a218f51",
"typing_FStar.Map.contains", "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_tip"
],
0,
"4a09f6c1e88a893a51e89e22a56dca54"
],
[
"Test.Vectors.Chacha20Poly1305.aad3_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_2f657d06ee5fc775edea771370ee385a",
"typing_Test.Vectors.Chacha20Poly1305.aad3"
],
0,
"32f194c7d0fcccf9f2a79e05bb100236"
],
[
"Test.Vectors.Chacha20Poly1305.input3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_2f657d06ee5fc775edea771370ee385a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7af298bc946646906a101fd94bc26c59",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad3"
],
0,
"68076f1aac661eec2064adde6202b845"
],
[
"Test.Vectors.Chacha20Poly1305.input3_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_44c02d445d3883cafead5466f5657550",
"typing_Test.Vectors.Chacha20Poly1305.input3"
],
0,
"1b121b0da962fe192dcac67ee5e7f0db"
],
[
"Test.Vectors.Chacha20Poly1305.output3",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_39f16ed6a1b2254a498382dffa2b7638",
"typing_FStar.Map.contains", "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_tip"
],
0,
"6bf80a9561c6b5991ea9ebaa3c8378ff"
],
[
"Test.Vectors.Chacha20Poly1305.output3_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_c03fa248d8de3e4e83181bd5b7187e39",
"typing_Test.Vectors.Chacha20Poly1305.output3"
],
0,
"040099480580773930882770a4c2e5d6"
],
[
"Test.Vectors.Chacha20Poly1305.key4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"afa61410a0a80781b6bc2ba7c79e78c9"
],
[
"Test.Vectors.Chacha20Poly1305.key4_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key4"
],
0,
"7df8a54c7af61378d23dff6500e7dd3a"
],
[
"Test.Vectors.Chacha20Poly1305.nonce4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"19f2bd8d28958932170cb47717222ccc"
],
[
"Test.Vectors.Chacha20Poly1305.nonce4_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce4"
],
0,
"2e15a370d761a51d1bfc3d7f2e6fbb54"
],
[
"Test.Vectors.Chacha20Poly1305.aad4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"67170bc0f2ab84488a5200477ae6f1d9"
],
[
"Test.Vectors.Chacha20Poly1305.aad4_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"typing_Test.Vectors.Chacha20Poly1305.aad4"
],
0,
"5524833096c85629f5a5f8a847f22e17"
],
[
"Test.Vectors.Chacha20Poly1305.input4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_FStar.UInt.min_int", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7af298bc946646906a101fd94bc26c59",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad4"
],
0,
"8b445f4f810b8037034bfa4244e0b3eb"
],
[
"Test.Vectors.Chacha20Poly1305.input4_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b7a3a0c14dc43f8108ca42dbc9a481a4",
"typing_Test.Vectors.Chacha20Poly1305.input4"
],
0,
"03171198cbbd5f97c3b90731235ad2f5"
],
[
"Test.Vectors.Chacha20Poly1305.output4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_39f16ed6a1b2254a498382dffa2b7638",
"typing_FStar.Map.contains", "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_tip"
],
0,
"102c98d9a60419f47784b0962c4d2fcb"
],
[
"Test.Vectors.Chacha20Poly1305.output4_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_c03fa248d8de3e4e83181bd5b7187e39",
"typing_Test.Vectors.Chacha20Poly1305.output4"
],
0,
"1ce6607a7f018bda4f00c834c3b0fb00"
],
[
"Test.Vectors.Chacha20Poly1305.key5",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"5bad23b926c7bf0ceafcc3d3ed739db6"
],
[
"Test.Vectors.Chacha20Poly1305.key5_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key5"
],
0,
"5ab8e228475bcfeb78bbc4a2cd671e36"
],
[
"Test.Vectors.Chacha20Poly1305.nonce5",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"7c2ca4db0a72108388928859fb18a56b"
],
[
"Test.Vectors.Chacha20Poly1305.nonce5_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce5"
],
0,
"7936af1760b23fa45685102b4ba470c7"
],
[
"Test.Vectors.Chacha20Poly1305.aad5",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0fbe1e2f7d75a442307207311c7c13ec",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"d00e398b8d44d6e9b3d7fd37fe1bd724"
],
[
"Test.Vectors.Chacha20Poly1305.aad5_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_c265d867a414db82abf15b736ac25f34",
"typing_Test.Vectors.Chacha20Poly1305.aad5"
],
0,
"92fb6ea4ad08874161af10103b164427"
],
[
"Test.Vectors.Chacha20Poly1305.input5",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ba55194577e04001c6fd95f84b5c2606",
"refinement_interpretation_Tm_refine_c265d867a414db82abf15b736ac25f34",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad5"
],
0,
"901825ab9b491f225d7bc30735b5b5b3"
],
[
"Test.Vectors.Chacha20Poly1305.input5_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_feb03304597ba2bb79e5227207b8b187",
"typing_Test.Vectors.Chacha20Poly1305.input5"
],
0,
"e44a1232586441ec5e85ba632324811f"
],
[
"Test.Vectors.Chacha20Poly1305.output5",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_dbdb4efccd7be7a97f367ece379076a5",
"typing_FStar.Map.contains", "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_tip"
],
0,
"4b66f13ae38bba3ebd9e2cba772bfc04"
],
[
"Test.Vectors.Chacha20Poly1305.output5_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_7e3c2f16e8961f92ddefbd0917f8349e",
"typing_Test.Vectors.Chacha20Poly1305.output5"
],
0,
"9211d4adc013e2d951149397ffcae1b4"
],
[
"Test.Vectors.Chacha20Poly1305.key6",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"7d2a3547b4c4af202fa26aaf23dc95fd"
],
[
"Test.Vectors.Chacha20Poly1305.key6_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key6"
],
0,
"428be05dddfbe3e05742641a98a6a092"
],
[
"Test.Vectors.Chacha20Poly1305.nonce6",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"9f0901eb0367c423cb81dfc52c959aaa"
],
[
"Test.Vectors.Chacha20Poly1305.nonce6_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce6"
],
0,
"ff3fd0f98339b62bea68aa73519a53a5"
],
[
"Test.Vectors.Chacha20Poly1305.aad6",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"1f4246fe324aa9817c23693a05309a5b"
],
[
"Test.Vectors.Chacha20Poly1305.aad6_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"typing_Test.Vectors.Chacha20Poly1305.aad6"
],
0,
"def8ee1cb4df40511ec6c752fc490fce"
],
[
"Test.Vectors.Chacha20Poly1305.input6",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_FStar.UInt.min_int", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"refinement_interpretation_Tm_refine_b71af98d521376d5fe725a9fb2c3fd68",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad6"
],
0,
"1a0835b3af4477dd8344c53fdb8f53b4"
],
[
"Test.Vectors.Chacha20Poly1305.input6_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_86d461ecef07c655b0fe966af5ee79dc",
"typing_Test.Vectors.Chacha20Poly1305.input6"
],
0,
"5f00e7bbcad669062d296975b0e95bf6"
],
[
"Test.Vectors.Chacha20Poly1305.output6",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_eb116fafefeb9d7fdeae492adea7b5e0",
"typing_FStar.Map.contains", "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_tip"
],
0,
"ae19f02922bde23e01a97a419adf1e76"
],
[
"Test.Vectors.Chacha20Poly1305.output6_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a111bdcf4ef8c17732bcf9912566f700",
"typing_Test.Vectors.Chacha20Poly1305.output6"
],
0,
"8dd3cf0ed023600a2e8ac5df33113b1d"
],
[
"Test.Vectors.Chacha20Poly1305.key7",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"58a77514ab0be6ec4f91f6ede859568b"
],
[
"Test.Vectors.Chacha20Poly1305.key7_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key7"
],
0,
"8ee76d90b532d47e18a854d7f4c132f9"
],
[
"Test.Vectors.Chacha20Poly1305.nonce7",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"5c248106156f582b5d2570f6a3748696"
],
[
"Test.Vectors.Chacha20Poly1305.nonce7_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce7"
],
0,
"a5899c89f68fdbff1e7733f9834fe662"
],
[
"Test.Vectors.Chacha20Poly1305.aad7",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"26fe46d02c3bdaa13cd1eb1fd0698693"
],
[
"Test.Vectors.Chacha20Poly1305.aad7_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"typing_Test.Vectors.Chacha20Poly1305.aad7"
],
0,
"23a1648f9f4eaf350d060a941e9514db"
],
[
"Test.Vectors.Chacha20Poly1305.input7",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_FStar.UInt.min_int", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_3ccef3d291cbd910ed6114da27fe0463",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad7"
],
0,
"7250e68b66d04f49c3e078b70c67952d"
],
[
"Test.Vectors.Chacha20Poly1305.input7_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_73a80f1fa34f49e8785893bce6bde8b6",
"typing_Test.Vectors.Chacha20Poly1305.input7"
],
0,
"efb643b3774d83911e7adf34dfc47159"
],
[
"Test.Vectors.Chacha20Poly1305.output7",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1470fcd31ff7e6344757fdd905d35edb",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"fca9035a506ec9a65dc0787abc5ec77f"
],
[
"Test.Vectors.Chacha20Poly1305.output7_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_cd2768b248316ace6d340a652ad860de",
"typing_Test.Vectors.Chacha20Poly1305.output7"
],
0,
"d12f532ade1eaa5bc61798ecb7365f34"
],
[
"Test.Vectors.Chacha20Poly1305.key8",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"bd270a3b6658caf9bb512d3814b28ad5"
],
[
"Test.Vectors.Chacha20Poly1305.key8_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key8"
],
0,
"9cda8691aeb69674d6c24ad5487d5f3a"
],
[
"Test.Vectors.Chacha20Poly1305.nonce8",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"42f730fac584bc7309c6753f0aa852f4"
],
[
"Test.Vectors.Chacha20Poly1305.nonce8_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce8"
],
0,
"f877562293fc47f5659b40cbcdc5c120"
],
[
"Test.Vectors.Chacha20Poly1305.aad8",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_bcf8725320ef34be9f0baa2ecd9a9f5f",
"typing_FStar.Map.contains", "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_tip"
],
0,
"508f9d1e7990b1d9cd42c0fb80670e86"
],
[
"Test.Vectors.Chacha20Poly1305.aad8_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_5693c27947d2ad280810e4f45e4e8ee2",
"typing_Test.Vectors.Chacha20Poly1305.aad8"
],
0,
"5f8f2be081a0f8eba961e2fdf5060417"
],
[
"Test.Vectors.Chacha20Poly1305.input8",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5693c27947d2ad280810e4f45e4e8ee2",
"refinement_interpretation_Tm_refine_6c73eb781f420b9c204375d28532c74c",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad8"
],
0,
"a625b92a0fe7be9fa03ca89971531047"
],
[
"Test.Vectors.Chacha20Poly1305.input8_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_809622c2ba95f10b7b3e4c31d897b1ce",
"typing_Test.Vectors.Chacha20Poly1305.input8"
],
0,
"c78d8ecb417ea451192d4d63278f0be8"
],
[
"Test.Vectors.Chacha20Poly1305.output8",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_bf56715d370f214ad5d71a2ad53c06a7",
"typing_FStar.Map.contains", "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_tip"
],
0,
"963764b48a9702657601cce0958e3d9b"
],
[
"Test.Vectors.Chacha20Poly1305.output8_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_876a096a79dd53b5b1b64d245cc9cb02",
"typing_Test.Vectors.Chacha20Poly1305.output8"
],
0,
"172b0bfb629b31f73deb3acce453daf1"
],
[
"Test.Vectors.Chacha20Poly1305.key9",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"6ae14236e3cb9adef4c4fdf1052185d8"
],
[
"Test.Vectors.Chacha20Poly1305.key9_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key9"
],
0,
"4536d8eac3bbac0864ac80cc1423cd80"
],
[
"Test.Vectors.Chacha20Poly1305.nonce9",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"b90eff79a25fb55fcc98987781383457"
],
[
"Test.Vectors.Chacha20Poly1305.nonce9_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce9"
],
0,
"71fb1db9699ea90818787061167823bd"
],
[
"Test.Vectors.Chacha20Poly1305.aad9",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_da79c9363cdb5abcffa152eada6a861f",
"typing_FStar.Map.contains", "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_tip"
],
0,
"27d9a0f7b255a7f69e932f3341b1cd62"
],
[
"Test.Vectors.Chacha20Poly1305.aad9_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_7e594ad2af0f3614996ce396263cb36e",
"typing_Test.Vectors.Chacha20Poly1305.aad9"
],
0,
"6ccefbb8b8ea757aac0a19370b3c0d5e"
],
[
"Test.Vectors.Chacha20Poly1305.input9",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_7e594ad2af0f3614996ce396263cb36e",
"refinement_interpretation_Tm_refine_988416e14d16bc09b19f669a20ea8a7c",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad9"
],
0,
"d0341b485b419e090013f1b4a95b8b5f"
],
[
"Test.Vectors.Chacha20Poly1305.input9_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0792628c176737fac9c14809ad43b441",
"typing_Test.Vectors.Chacha20Poly1305.input9"
],
0,
"83d5c79f07690ef2177eaf30d92ff27a"
],
[
"Test.Vectors.Chacha20Poly1305.output9",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9b5eebac15582c9ad660be2dd67abde4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"44d395e6963eabbac1f1477d7b91a038"
],
[
"Test.Vectors.Chacha20Poly1305.output9_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_3822cae8ab38234e73c43e0b3384925b",
"typing_Test.Vectors.Chacha20Poly1305.output9"
],
0,
"c2d30cc66883b2a5d83428f8854cf86e"
],
[
"Test.Vectors.Chacha20Poly1305.key10",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"733beefb45d23a7c153c44b5ad5e75c4"
],
[
"Test.Vectors.Chacha20Poly1305.key10_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key10"
],
0,
"9b99a2f1c1d44f845d52861debe84a7f"
],
[
"Test.Vectors.Chacha20Poly1305.nonce10",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"89dfa1e21ba3066c67f34ae165991cdc"
],
[
"Test.Vectors.Chacha20Poly1305.nonce10_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce10"
],
0,
"9819839aace3610f3cc7456b4c60c5da"
],
[
"Test.Vectors.Chacha20Poly1305.aad10",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0fbe1e2f7d75a442307207311c7c13ec",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"5f8909da8b7967f0d1af7e829e5c5d9e"
],
[
"Test.Vectors.Chacha20Poly1305.aad10_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_c265d867a414db82abf15b736ac25f34",
"typing_Test.Vectors.Chacha20Poly1305.aad10"
],
0,
"7e6115fbf0583e963ab6330b6f836534"
],
[
"Test.Vectors.Chacha20Poly1305.input10",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_8da32f2145335508fb01dda5280e11f5",
"refinement_interpretation_Tm_refine_c265d867a414db82abf15b736ac25f34",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad10"
],
0,
"4ca153559a95f2fb2b6558619cc241bf"
],
[
"Test.Vectors.Chacha20Poly1305.input10_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_f8b26f30858c263543c8c79684cbf5da",
"typing_Test.Vectors.Chacha20Poly1305.input10"
],
0,
"20dfe4fb48b76158f1dcd0900ab67551"
],
[
"Test.Vectors.Chacha20Poly1305.output10",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0193826d6e668b4636e7b68a185f38d4",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"typing_FStar.Map.contains", "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_tip"
],
0,
"fe5e300bd1903f1a2d24ee1a1b36ec32"
],
[
"Test.Vectors.Chacha20Poly1305.output10_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_9004d662a1ec2bb346e66a405ab28355",
"typing_Test.Vectors.Chacha20Poly1305.output10"
],
0,
"7e9d0d485a2f70c76d2ee2a27d80ce78"
],
[
"Test.Vectors.Chacha20Poly1305.key11",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_9e8ec64c75a490b6c2a46881aede1dd4",
"typing_FStar.Map.contains", "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_tip"
],
0,
"1052b1bcfb6aad51c8969b9a89df9e9c"
],
[
"Test.Vectors.Chacha20Poly1305.key11_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a599d79344249c234cb59f5a6c89fc31",
"typing_Test.Vectors.Chacha20Poly1305.key11"
],
0,
"4b3ebbcdf170af59fb0f2f6cf8380437"
],
[
"Test.Vectors.Chacha20Poly1305.nonce11",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_436da53bab56db28cbea6920a78dd432",
"typing_FStar.Map.contains", "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_tip"
],
0,
"318d879a04e93a06dfed58cd570813e7"
],
[
"Test.Vectors.Chacha20Poly1305.nonce11_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"typing_Test.Vectors.Chacha20Poly1305.nonce11"
],
0,
"fb481e737f8865345f470564caca8a8d"
],
[
"Test.Vectors.Chacha20Poly1305.aad11",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_4812bcc40409120184d8fd2949599f38",
"typing_FStar.Map.contains", "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_tip"
],
0,
"f302746f0fdcf2b0356bbe91b017fea0"
],
[
"Test.Vectors.Chacha20Poly1305.aad11_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_aa69b94dee22dabea75977056b8a8275",
"typing_Test.Vectors.Chacha20Poly1305.aad11"
],
0,
"0df93c7e6867f843563a301af57b097a"
],
[
"Test.Vectors.Chacha20Poly1305.input11",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_46c77ecc2445dbb5b4bad95adfc32a5d",
"refinement_interpretation_Tm_refine_aa69b94dee22dabea75977056b8a8275",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "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_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_Test.Vectors.Chacha20Poly1305.aad11"
],
0,
"8dc74b42db63b8d907ceb63070ea61cd"
],
[
"Test.Vectors.Chacha20Poly1305.input11_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_5e15b75f292f9bd8498b31d75d7d13a2",
"typing_Test.Vectors.Chacha20Poly1305.input11"
],
0,
"dadb08679f584a43f662d70907a32479"
],
[
"Test.Vectors.Chacha20Poly1305.output11",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_7d3f5df5ba5e1761febeae31a8aadb93",
"typing_FStar.Map.contains", "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_tip"
],
0,
"e766c22c692c2d769b6e252c5be70b16"
],
[
"Test.Vectors.Chacha20Poly1305.output11_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b488c3cc481b648f622f6e36cb1f23a7",
"typing_Test.Vectors.Chacha20Poly1305.output11"
],
0,
"ca122b2975818c52903628252e89f910"
],
[
"Test.Vectors.Chacha20Poly1305.vector",
1,
0,
0,
[ "@query" ],
0,
"8ed5fa98a0940d8b50a92387b985bad1"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__output_len",
1,
0,
0,
[ "@query" ],
0,
"3220b56ac1cec2cc901dfa484b7e6259"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__output_len",
2,
0,
0,
[
"@query",
"proj_equation_Test.Vectors.Chacha20Poly1305.Vector_output",
"projection_inverse_Test.Vectors.Chacha20Poly1305.Vector_output"
],
0,
"7c69e8bd9f06867c2c89e5617af5bcc9"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__input_len",
1,
0,
0,
[ "@query" ],
0,
"99afea222e294a668e311f641898ee1c"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__input_len",
2,
0,
0,
[
"@query", "proj_equation_Test.Vectors.Chacha20Poly1305.Vector_input",
"projection_inverse_Test.Vectors.Chacha20Poly1305.Vector_input"
],
0,
"b66ce608e9d797399a0ed77764e165d6"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__aad",
1,
0,
0,
[
"@query", "proj_equation_Test.Vectors.Chacha20Poly1305.Vector_input",
"projection_inverse_Test.Vectors.Chacha20Poly1305.Vector_input"
],
0,
"81ade372127ba38c53633782a8795057"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__aad_len",
1,
0,
0,
[ "@query" ],
0,
"75ecbad41cc09d96decc396028fcc5e5"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__aad_len",
2,
0,
0,
[
"@query", "proj_equation_Test.Vectors.Chacha20Poly1305.Vector_aad",
"projection_inverse_Test.Vectors.Chacha20Poly1305.Vector_aad"
],
0,
"4957d74d82a6d4719e6ff95ee1ef4644"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__nonce_len",
1,
0,
0,
[ "@query" ],
0,
"b31c79705b1180913386d72a92b2c324"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__nonce_len",
2,
0,
0,
[
"@query", "proj_equation_Test.Vectors.Chacha20Poly1305.Vector_nonce",
"projection_inverse_Test.Vectors.Chacha20Poly1305.Vector_nonce"
],
0,
"e43749edd583a36fd14d6f4be65b4f93"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__key_len",
1,
0,
0,
[ "@query" ],
0,
"6dc5848357c4ba9d08150ad85a7a4744"
],
[
"Test.Vectors.Chacha20Poly1305.__proj__Vector__item__key_len",
2,
0,
0,
[
"@query", "proj_equation_Test.Vectors.Chacha20Poly1305.Vector_key",
"projection_inverse_Test.Vectors.Chacha20Poly1305.Vector_key"
],
0,
"fb9feabfe28aed545cb803ac65b0031b"
],
[
"Test.Vectors.Chacha20Poly1305.vectors",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.mem",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0792628c176737fac9c14809ad43b441",
"refinement_interpretation_Tm_refine_1851140a5a9d6bf151cff94e730d2ede",
"refinement_interpretation_Tm_refine_2f657d06ee5fc775edea771370ee385a",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_42c3cc663ffc986561be9d8b5551c79d",
"refinement_interpretation_Tm_refine_44c02d445d3883cafead5466f5657550",
"refinement_interpretation_Tm_refine_5693c27947d2ad280810e4f45e4e8ee2",
"refinement_interpretation_Tm_refine_5dccf04464b669d881c826e935365436",
"refinement_interpretation_Tm_refine_5e15b75f292f9bd8498b31d75d7d13a2",
"refinement_interpretation_Tm_refine_73a80f1fa34f49e8785893bce6bde8b6",
"refinement_interpretation_Tm_refine_7e594ad2af0f3614996ce396263cb36e",
"refinement_interpretation_Tm_refine_809622c2ba95f10b7b3e4c31d897b1ce",
"refinement_interpretation_Tm_refine_86d461ecef07c655b0fe966af5ee79dc",
"refinement_interpretation_Tm_refine_a669efdb48b7d781925cd184e7d8c119",
"refinement_interpretation_Tm_refine_aa69b94dee22dabea75977056b8a8275",
"refinement_interpretation_Tm_refine_af30b58a8dea5dcae248698ebc4240ec",
"refinement_interpretation_Tm_refine_b428c15c12720ecc1546a63b0448d3ef",
"refinement_interpretation_Tm_refine_b7a3a0c14dc43f8108ca42dbc9a481a4",
"refinement_interpretation_Tm_refine_c265d867a414db82abf15b736ac25f34",
"refinement_interpretation_Tm_refine_f8b26f30858c263543c8c79684cbf5da",
"refinement_interpretation_Tm_refine_feb03304597ba2bb79e5227207b8b187",
"typing_FStar.Map.contains", "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_tip",
"typing_Test.Vectors.Chacha20Poly1305.aad0",
"typing_Test.Vectors.Chacha20Poly1305.aad1",
"typing_Test.Vectors.Chacha20Poly1305.aad10",
"typing_Test.Vectors.Chacha20Poly1305.aad11",
"typing_Test.Vectors.Chacha20Poly1305.aad2",
"typing_Test.Vectors.Chacha20Poly1305.aad3",
"typing_Test.Vectors.Chacha20Poly1305.aad4",
"typing_Test.Vectors.Chacha20Poly1305.aad5",
"typing_Test.Vectors.Chacha20Poly1305.aad6",
"typing_Test.Vectors.Chacha20Poly1305.aad7",
"typing_Test.Vectors.Chacha20Poly1305.aad8",
"typing_Test.Vectors.Chacha20Poly1305.aad9"
],
0,
"7a4ff24be724c43c14caff3e2d533d95"
],
[
"Test.Vectors.Chacha20Poly1305.vectors_len",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_ccdbcf332f874f37b45eb9fabd5200eb",
"typing_Test.Vectors.Chacha20Poly1305.vectors"
],
0,
"f67f41d5dee9f26289db49697f180bbe"
]
]
]
Computing file changes ...
