Revision - 9328136 - Tweak configure script

Revision 93281362ad4fa0df971a98b303733ad47f7ee0b5 authored by Jonathan Protzenko on 15 April 2020, 18:25:02 UTC, committed by Jonathan Protzenko on 15 April 2020, 18:25:02 UTC

Tweak configure script

1 parent 321f8c4

Files
Changes

Permalinks

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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "2c0ee68d1a3ec1fb40469931fb9a0f7d"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key0_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key0"
      ],
      0,
      "eafdcd82a38c86803eb2e7b608b5a155"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "d491633e8bbb8b9f5cf9c1e06447d670"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce0_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce0"
      ],
      0,
      "e74ac672aa551966950ea4aec629db0b"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "0ae73e1eb0b5c38aebcb8b74155031fb"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad0_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.aad0"
      ],
      0,
      "0b51d0759ab51363e07c83fcbe5083c5"
    ],
    [
      "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_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_3c29cc777f854a72fc412ed90fb78dd3",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_e117f8451ead9813171cbe564e63d67e",
        "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_FStar.UInt8.t",
        "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,
      "30da13ddf69dd388121fa90c47a1118a"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input0_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_0aa5f24116ae34d7ed7665d0478f3b4d",
        "typing_Test.Vectors.Chacha20Poly1305.input0"
      ],
      0,
      "3d88aad0975eef85ab37cacb05522127"
    ],
    [
      "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_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_9ad630f63fb29672c5030882cababaa2",
        "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,
      "bfc63a6f9cab59ebead2bea31f48867f"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output0_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_dedbd06bc7ae0079e9959f8cbc8d3b38",
        "typing_Test.Vectors.Chacha20Poly1305.output0"
      ],
      0,
      "08007f7ded64ffa90b06fadeada43d01"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "4a12618ab4c49c72ee12d256a105cc80"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key1_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key1"
      ],
      0,
      "fe75b4fa270219a6ff080c053aa50654"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "105c06ab90a7e306a8d87dcb07d85362"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce1_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce1"
      ],
      0,
      "d23412f016661d4c10b1c1a4a47f6965"
    ],
    [
      "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,
      "f9d705befd96f97b7253fa715649851d"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad1_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "typing_Test.Vectors.Chacha20Poly1305.aad1"
      ],
      0,
      "b39f3afff20c08f45b249ecd3fe1683b"
    ],
    [
      "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_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_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "refinement_interpretation_Tm_refine_a4ec12512fabef911c6c75ffd253a87b",
        "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_FStar.UInt8.t",
        "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,
      "11c4acdf4fac31aefbc5ca03eb9d41df"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input1_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_72a313438505af1568dcc65012fd9cfc",
        "typing_Test.Vectors.Chacha20Poly1305.input1"
      ],
      0,
      "14c559420ecfd2b4669d24ba241cf53c"
    ],
    [
      "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_5361ddac5a39d39800941d80f898fc83",
        "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,
      "2dde9512987f177cdcbab18bb4b9cf58"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output1_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_16cc6a6b0029ec3a75e511ab54cc0631",
        "typing_Test.Vectors.Chacha20Poly1305.output1"
      ],
      0,
      "0a1fc26d0dff4e8e018b3ea389a71144"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "7de13413689c42bdb6780f77e502a3e7"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key2_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key2"
      ],
      0,
      "a90bfba0b6597f89707845b7992357c3"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "5a9d84a3875421b7ea5ae5bfdee79dcf"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce2_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce2"
      ],
      0,
      "6af852835cfb7157f63abd58ce2b77b6"
    ],
    [
      "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_31db687240398c6877bc341a1850cf99",
        "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,
      "4cf12cce1066e951a77f7d3839353be6"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad2_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_be39cf5f5def3d988cb238fa7560426b",
        "typing_Test.Vectors.Chacha20Poly1305.aad2"
      ],
      0,
      "703a8f4c34de157d28d40ba83c994052"
    ],
    [
      "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_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_a4ec12512fabef911c6c75ffd253a87b",
        "refinement_interpretation_Tm_refine_be39cf5f5def3d988cb238fa7560426b",
        "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_FStar.UInt8.t",
        "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,
      "a4ac8a2209ffc8ac434354294cd6d5cb"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input2_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_969352463670e36af4268c2723497e70",
        "typing_Test.Vectors.Chacha20Poly1305.input2"
      ],
      0,
      "5d0f098ba82013c3465e4cc918ef286e"
    ],
    [
      "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_5361ddac5a39d39800941d80f898fc83",
        "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,
      "ee15ae6842363462aab782ccd7e57ef6"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output2_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_16cc6a6b0029ec3a75e511ab54cc0631",
        "typing_Test.Vectors.Chacha20Poly1305.output2"
      ],
      0,
      "74e11fb43e7e53839dfa32213954b7ec"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "f8f8b154b111e6c97a330b4184a6392e"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key3_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key3"
      ],
      0,
      "eb5c57e834972af4951b4950d69ac977"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "70a196c554b4fc0604d4149715cda36b"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce3_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce3"
      ],
      0,
      "d843d2c08f0c1fccd038643dfcd1f88b"
    ],
    [
      "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_31db687240398c6877bc341a1850cf99",
        "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,
      "57b1340a5f7794c129acd761b60bde7c"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad3_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_be39cf5f5def3d988cb238fa7560426b",
        "typing_Test.Vectors.Chacha20Poly1305.aad3"
      ],
      0,
      "cc8950d90f8ac700cefa6baa5508440d"
    ],
    [
      "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_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_be39cf5f5def3d988cb238fa7560426b",
        "refinement_interpretation_Tm_refine_f0e8fa931fb52c422a0a77548342f6c3",
        "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_FStar.UInt8.t",
        "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,
      "7c157b2b327f98c1efb07bcd31becd86"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input3_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_0a81b0195ed43d2ad9d8198fba8302c1",
        "typing_Test.Vectors.Chacha20Poly1305.input3"
      ],
      0,
      "8c309f3ac03377f9359390d7d2a54ac8"
    ],
    [
      "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_6b8c2769f234007fcf437ec383d17078",
        "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,
      "23ca1d30bd4a02aee819707d54c56360"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output3_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_627abf2f3e02525671fcf51506099c0d",
        "typing_Test.Vectors.Chacha20Poly1305.output3"
      ],
      0,
      "6f0b3c66d280b508deedbb5c081cd3c6"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "df4f06bc164db9d5eef0c2b0900f3823"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key4_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key4"
      ],
      0,
      "adaf4791641b634b8ccba6b00bd48530"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "dba44cf0e718900c78729f39b00d5de2"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce4_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce4"
      ],
      0,
      "2fec4fa7068ddb837ea186c56021d71c"
    ],
    [
      "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,
      "5c1101a577dae940ca9a1ab90e2e57d3"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad4_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "typing_Test.Vectors.Chacha20Poly1305.aad4"
      ],
      0,
      "6a938ed091567dfdf2111b11c047c025"
    ],
    [
      "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_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_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "refinement_interpretation_Tm_refine_f0e8fa931fb52c422a0a77548342f6c3",
        "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_FStar.UInt8.t",
        "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,
      "a2884eedfcc72bb32ee9fa9f292bf1a4"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input4_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_add14fc8176b43c9f1c7df28e5a6f026",
        "typing_Test.Vectors.Chacha20Poly1305.input4"
      ],
      0,
      "f478556cf23837b74fbf0902f68831cc"
    ],
    [
      "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_6b8c2769f234007fcf437ec383d17078",
        "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,
      "b1b49053d6b611d20ea0bb1d7ddd480f"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output4_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_627abf2f3e02525671fcf51506099c0d",
        "typing_Test.Vectors.Chacha20Poly1305.output4"
      ],
      0,
      "9c69b0b9ea86197b45475cb0bc5dad3d"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "5d89a5dea03d2a3af601c927e6b33ee0"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key5_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key5"
      ],
      0,
      "0aadc5317d8b2a7c088868f982e972fe"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "f08c88777f9acfefdb848feb012bfadd"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce5_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce5"
      ],
      0,
      "77403734c37ead80d4417d97ea909886"
    ],
    [
      "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_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_7a7741e83439139fa9b6a426f5227530",
        "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,
      "64fb37894ea090d4e1241ea9882b5b8b"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad5_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_c167f790398a0ce720220e01f8ee0b52",
        "typing_Test.Vectors.Chacha20Poly1305.aad5"
      ],
      0,
      "88e44a37790012b52cf5a9588f41bef0"
    ],
    [
      "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_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_862da3d7f946597930014ec6a5a9e51b",
        "refinement_interpretation_Tm_refine_c167f790398a0ce720220e01f8ee0b52",
        "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_FStar.UInt8.t",
        "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,
      "c7d866bd63154f38fd06017ef498a189"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input5_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_05f54e590eda62f540a94ea23d8afdb8",
        "typing_Test.Vectors.Chacha20Poly1305.input5"
      ],
      0,
      "6ffbdd269678fc09f35dee54eb04dcb6"
    ],
    [
      "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_4fce3b318cf668835d2363de80eeca15",
        "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,
      "f1556385d404290be3c3255ea4d59d2f"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output5_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_6889f3820c679707a73ee2338ee52631",
        "typing_Test.Vectors.Chacha20Poly1305.output5"
      ],
      0,
      "d0822927cedf93033a62561daa641140"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "6077924e98c549f71177ec020e671207"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key6_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key6"
      ],
      0,
      "5143defed1d6982a5e1c9349d66b2506"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "c22b3876f5c7e26969159c7374bd1e9a"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce6_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce6"
      ],
      0,
      "a2724d9e0eb4f7e3a97e347cbb67a938"
    ],
    [
      "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,
      "afc20fa1855a5fbcff0133b9f172e0f7"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad6_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "typing_Test.Vectors.Chacha20Poly1305.aad6"
      ],
      0,
      "d76060fd65fe112829be003afd583356"
    ],
    [
      "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_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_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "refinement_interpretation_Tm_refine_c7fd79e00ad2429fcf25fc3557f957da",
        "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_FStar.UInt8.t",
        "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,
      "fd58d8ff446249a48bb2f96d81f8dbf7"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input6_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_1b683305a526d9662cc877d30fb1d582",
        "typing_Test.Vectors.Chacha20Poly1305.input6"
      ],
      0,
      "49e893b8b96263ba74d4100832f61949"
    ],
    [
      "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_66da3b78d177de36e9e207b39e04bfd2",
        "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,
      "14b620d1bf6af7c0e527b135e6d3117c"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output6_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_245e0ed29a390d5b0844225eb04979a5",
        "typing_Test.Vectors.Chacha20Poly1305.output6"
      ],
      0,
      "1d6e5cca60799cfa4d188d0c084ee11f"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "77829a7eb337c2d4642becf556dd3852"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key7_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key7"
      ],
      0,
      "3a2889dbc5fa6ea533505c0d3eb456fc"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "d30a0104b27b834edc16d32f04e354f7"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce7_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce7"
      ],
      0,
      "944fcec1a3abd06f5a40a290ead4a24c"
    ],
    [
      "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,
      "52d7f5bffa25e32571f86ddb5603aff9"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad7_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "typing_Test.Vectors.Chacha20Poly1305.aad7"
      ],
      0,
      "b7eee82a91b6de78589e5f1f177cc2a8"
    ],
    [
      "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_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_698eec50cf6dd8112bcd2605bf1a44ee",
        "refinement_interpretation_Tm_refine_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "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_FStar.UInt8.t",
        "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,
      "7a470fb104eea24d633e2ac5e64d6598"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input7_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_185f596162bdd92339fc6a898c52a0b0",
        "typing_Test.Vectors.Chacha20Poly1305.input7"
      ],
      0,
      "67e433fa847ed2ef27584ecd7f87c43d"
    ],
    [
      "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_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_84afd87e5389c9921d85c05cc54a7fc9",
        "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,
      "ab1ce35b2134f225d03b92eb3ae1dee1"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output7_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_501be3fb1515c79f868f5e8df9b4b955",
        "typing_Test.Vectors.Chacha20Poly1305.output7"
      ],
      0,
      "1d5ab485e30a9e74e1587ea8140da54d"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "bc7b322d01f6f1aa351cf794423f99b3"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key8_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key8"
      ],
      0,
      "6c32f87ba72aed469bc3e3745e673c8d"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "15cfb1d155974f8daa3f24e73f30224d"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce8_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce8"
      ],
      0,
      "354cd74f9422d072bf338c15235d8e90"
    ],
    [
      "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_22db6979369390f568757bdf342e5880",
        "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,
      "626912b9383ab5a772e1d15d581f2733"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad8_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_251193c7866f28bbf1eec9552c418786",
        "typing_Test.Vectors.Chacha20Poly1305.aad8"
      ],
      0,
      "caa4b8a50061eea5882934fa13de3612"
    ],
    [
      "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_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_251193c7866f28bbf1eec9552c418786",
        "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_ce16d5215552a64f0a7eeb0850749321",
        "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_FStar.UInt8.t",
        "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,
      "b034813018c0ecab8b8393ddf8a6dd47"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input8_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_b2634d5e2ba1f9c37ba0645538e2bb91",
        "typing_Test.Vectors.Chacha20Poly1305.input8"
      ],
      0,
      "15e61642d61722ae97c780a9640bcc26"
    ],
    [
      "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_c75b79dca7e93ff91bc1ec8a35749391",
        "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,
      "09f9d2eaf39bde8934ab0d3f4bf3fe1f"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output8_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3696fdb1f7e74674e961b0afcf0fedc5",
        "typing_Test.Vectors.Chacha20Poly1305.output8"
      ],
      0,
      "4017e9e0958e5b1c31460edc7fea9809"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "20cbc6573d08e9fcc9f6f72dfd9f16c3"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key9_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key9"
      ],
      0,
      "6abf1f2ab36dd186f32dd70f9f99ec0f"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "abbcda6f2d0f8fc122fbad23d50cddaf"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce9_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce9"
      ],
      0,
      "cadb7d51bb9ab7669da1c9b14e4fd164"
    ],
    [
      "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_5361ddac5a39d39800941d80f898fc83",
        "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,
      "80de9a037c3cd12b3deee478de8eb0f9"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad9_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_16cc6a6b0029ec3a75e511ab54cc0631",
        "typing_Test.Vectors.Chacha20Poly1305.aad9"
      ],
      0,
      "d3f3838ca40b00bbe3a56feee8d3dd4a"
    ],
    [
      "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_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_16cc6a6b0029ec3a75e511ab54cc0631",
        "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_83b6ab93d11a0796adc3b8f429909515",
        "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_FStar.UInt8.t",
        "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,
      "71f5ba21d1c8fe7d4c1ed98e4f478661"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input9_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_b022350e0916328d5da8a67c7834c5ba",
        "typing_Test.Vectors.Chacha20Poly1305.input9"
      ],
      0,
      "a609c7802e32486137eafe21c648e318"
    ],
    [
      "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_3f3900c653f4b98b320ad55e7270b5f7",
        "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,
      "e14f56e1163bf0018b12d7c21b8603cd"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output9_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_4390b28b6bdee73cbef1e05c78a66203",
        "typing_Test.Vectors.Chacha20Poly1305.output9"
      ],
      0,
      "af6efaa2e1d46c8207137ada2d243f44"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "06dcf6b9ce42f83e331cf52739640613"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key10_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key10"
      ],
      0,
      "a2a3b0557043faa8302da002272e9c3a"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "ffae445520bb100866cc06bd3044ef5b"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce10_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce10"
      ],
      0,
      "8c0a44d8a0256a41060bf40683d504a0"
    ],
    [
      "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_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_7a7741e83439139fa9b6a426f5227530",
        "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,
      "a661d2f45c147c4be5ccb9082516c99d"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad10_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_c167f790398a0ce720220e01f8ee0b52",
        "typing_Test.Vectors.Chacha20Poly1305.aad10"
      ],
      0,
      "af5457862cc8c2af40c86bc039b052a1"
    ],
    [
      "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_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_c167f790398a0ce720220e01f8ee0b52",
        "refinement_interpretation_Tm_refine_ff01aaff42ec55c65796a951c4ce4844",
        "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_FStar.UInt8.t",
        "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,
      "8cd5184ed85a91b5123e7a434f731659"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input10_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_4fabbb2e3bfe9bdbae07a0e4f4533a18",
        "typing_Test.Vectors.Chacha20Poly1305.input10"
      ],
      0,
      "a143642b5abe8628d143602ed046cec2"
    ],
    [
      "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_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_a05fd5f1f67954b8789d5372f41ebb0d",
        "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,
      "a3a7d1e02780338eda3781fe73f01324"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output10_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_2444ab613e230bba35f118b83c9ce25d",
        "typing_Test.Vectors.Chacha20Poly1305.output10"
      ],
      0,
      "5e1666be93a6fd783f8abbbba4e9fffc"
    ],
    [
      "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_fcb5b58d5cac0cfc8b29731cac15492e",
        "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,
      "59943250fa22ab8bf6ae6232cccd81c5"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.key11_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_5cc198752d76ccc0d60d576ac8a3a904",
        "typing_Test.Vectors.Chacha20Poly1305.key11"
      ],
      0,
      "b9face8ebe56b15848316510486edab5"
    ],
    [
      "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_42d6f44ab808208ddb9fd3f80dc034e7",
        "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,
      "f7a9019c35bb9a8c324892d1b2845a96"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.nonce11_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "typing_Test.Vectors.Chacha20Poly1305.nonce11"
      ],
      0,
      "b080e5b0917fd137efc6d84594ef69fe"
    ],
    [
      "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_b96bd415266da63ce502520b4b29c842",
        "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,
      "ceafd43c2e78021d32354f05512f8d0b"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.aad11_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_1e1ae3aabc94f4eaea04513c59ee4676",
        "typing_Test.Vectors.Chacha20Poly1305.aad11"
      ],
      0,
      "9c6dcb3fdc413b3b9a4195cfcb16d58a"
    ],
    [
      "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_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_1e1ae3aabc94f4eaea04513c59ee4676",
        "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_3f179519ac2af765670e427603bbf438",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "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_FStar.UInt8.t",
        "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,
      "27a8baf49c1c084d8538340c3a104a15"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.input11_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_81e58bc3b307bf5555ecf69d63b49d7b",
        "typing_Test.Vectors.Chacha20Poly1305.input11"
      ],
      0,
      "5d74a282a03bf1afb49b01f95f227175"
    ],
    [
      "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_afb7da85521b6c1b0e2d485db2c81c87",
        "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,
      "6ed1a9290c08d858556e1d0f810e58aa"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.output11_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_c514d0b45ad1da484d8b9f3ab1e5b880",
        "typing_Test.Vectors.Chacha20Poly1305.output11"
      ],
      0,
      "eb9dcc3f49ed35d1391a124ec67416e7"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.vector",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "72e26705c440ec22f148e08094fec89a"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.__proj__Vector__item__output_len",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "2fdb813ea0816919414bd5cfd557554c"
    ],
    [
      "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,
      "b7a0e5672f2d79ea135fcd3b53c6375d"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.__proj__Vector__item__input_len",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "af029fa1fee0ed1442589af9023c0d00"
    ],
    [
      "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,
      "cd7c3b91339bf619dec33ab8087bbe44"
    ],
    [
      "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,
      "55dd481092371d54a37f8e73903bacd5"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.__proj__Vector__item__aad_len",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "dafcbee1e7484c4d4a0ecf270366c9f1"
    ],
    [
      "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,
      "c3425e80131060159decf3bde6e16c58"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.__proj__Vector__item__nonce_len",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "8fe1c78d93de2a703911fc53a4eed1f5"
    ],
    [
      "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,
      "7238ef7bf7b8064e1bafcfecfb67fd27"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.__proj__Vector__item__key_len",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "744f3988508253e4c73ef9bb1c45986d"
    ],
    [
      "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,
      "dc4cb7c930b487c4c4ecc35cbdb85bb4"
    ],
    [
      "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_05f54e590eda62f540a94ea23d8afdb8",
        "refinement_interpretation_Tm_refine_0a81b0195ed43d2ad9d8198fba8302c1",
        "refinement_interpretation_Tm_refine_0aa5f24116ae34d7ed7665d0478f3b4d",
        "refinement_interpretation_Tm_refine_16cc6a6b0029ec3a75e511ab54cc0631",
        "refinement_interpretation_Tm_refine_185f596162bdd92339fc6a898c52a0b0",
        "refinement_interpretation_Tm_refine_1b683305a526d9662cc877d30fb1d582",
        "refinement_interpretation_Tm_refine_1e1ae3aabc94f4eaea04513c59ee4676",
        "refinement_interpretation_Tm_refine_251193c7866f28bbf1eec9552c418786",
        "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
        "refinement_interpretation_Tm_refine_3c29cc777f854a72fc412ed90fb78dd3",
        "refinement_interpretation_Tm_refine_42c3cc663ffc986561be9d8b5551c79d",
        "refinement_interpretation_Tm_refine_4fabbb2e3bfe9bdbae07a0e4f4533a18",
        "refinement_interpretation_Tm_refine_72a313438505af1568dcc65012fd9cfc",
        "refinement_interpretation_Tm_refine_7bb6499ceeaa0d5f3be47f1c9ee130f0",
        "refinement_interpretation_Tm_refine_81e58bc3b307bf5555ecf69d63b49d7b",
        "refinement_interpretation_Tm_refine_969352463670e36af4268c2723497e70",
        "refinement_interpretation_Tm_refine_add14fc8176b43c9f1c7df28e5a6f026",
        "refinement_interpretation_Tm_refine_b022350e0916328d5da8a67c7834c5ba",
        "refinement_interpretation_Tm_refine_b2634d5e2ba1f9c37ba0645538e2bb91",
        "refinement_interpretation_Tm_refine_be39cf5f5def3d988cb238fa7560426b",
        "refinement_interpretation_Tm_refine_c167f790398a0ce720220e01f8ee0b52",
        "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,
      "c9f7a82f102bd70f459bab634208ac80"
    ],
    [
      "Test.Vectors.Chacha20Poly1305.vectors_len",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_ccdbcf332f874f37b45eb9fabd5200eb",
        "typing_Test.Vectors.Chacha20Poly1305.vectors"
      ],
      0,
      "2d7a53af62b83a5a9ccc13734456116b"
    ]
  ]
]

Showing with 0 additions and 0 deletions (0 / 0 diffs computed)

Computing file changes ...