[
  "��R�\"\u000f��h��e��%�",
  [
    [
      "Vale.Arch.MachineHeap_s.get_heap_val32_def",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5e62f20a8041da0bf064e3b6e87f5f89"
    ],
    [
      "Vale.Arch.MachineHeap_s.get_heap_val32_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ba29c8647da282deb7e9b28bd3bf2710"
    ],
    [
      "Vale.Arch.MachineHeap_s.get_heap_val64_def",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "9a55d1b588c59070925e2b7b609a66bd"
    ],
    [
      "Vale.Arch.MachineHeap_s.get_heap_val64_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "366fb536c8f49e9466ce8593d17244f2"
    ],
    [
      "Vale.Arch.MachineHeap_s.get_heap_val128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "75a80fc1ec5b1915573a736c5d50bca2"
    ],
    [
      "Vale.Arch.MachineHeap_s.update_heap32_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.natN",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "5ebd66159677f3c483c4cbaa9b202568"
    ],
    [
      "Vale.Arch.MachineHeap_s.update_heap32_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "56caeb8724ffa207486340bbee9060b8"
    ],
    [
      "Vale.Arch.MachineHeap_s.update_heap64_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Vale.Def.Words.Two_s.nat_to_two",
        "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "21ed0120e23879b68d75c0a3d3e0768d"
    ],
    [
      "Vale.Arch.MachineHeap_s.update_heap64_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4678f4fb1a2e29a566a3053ae262cddb"
    ],
    [
      "Vale.Arch.MachineHeap_s.update_heap128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "987d6683ff4fe28dbb0fc390f5bf23ff"
    ]
  ]
]