[
  "Ì\u0016\\\"†8S™\u0011ô‚\u0013\u000f·÷‚",
  [
    [
      "WasmSupport.check_buffer_size",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
        "lemma_FStar.Set.lemma_equal_refl",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap"
      ],
      0,
      "56de1ed978b9b96635d526487e5386ab"
    ],
    [
      "WasmSupport.betole64",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "bfdb779d5538e82fe96ee8787913a66b"
    ]
  ]
]