[
  "a×xã\t&L˜¬u³ƒ©æ©¡",
  [
    [
      "Vale.X64.BufferViewStore.bv_upd_update_heap64",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.Seq.Properties.lseq",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Interop.Types.b8_preorder",
        "equation_Vale.Interop.Types.base_typ_as_type",
        "equation_Vale.Interop.Types.down_view",
        "equation_Vale.Interop.Types.get_downview",
        "equation_Vale.Interop.Views.up_view64",
        "fuel_guarded_inversion_FStar.Pervasives.dtuple4",
        "fuel_guarded_inversion_LowStar.BufferView.Down.view",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
        "lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Mkdtuple4__1",
        "proj_equation_FStar.Pervasives.Mkdtuple4__2",
        "proj_equation_FStar.Pervasives.Mkdtuple4__3",
        "proj_equation_LowStar.BufferView.Up.View_n",
        "proj_equation_Vale.Interop.Types.Buffer_bsrc",
        "proj_equation_Vale.Interop.Types.Buffer_src",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.Up.View_n",
        "refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_59430ef12db2c39a3a93c2c604fdc458",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_cdcaa1d3db89979e51cab50994d1b6ee",
        "refinement_interpretation_Tm_refine_d9c0939c82712b7f95eb7997f76e8481",
        "typing_FStar.UInt64.t", "typing_FStar.UInt8.t",
        "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
        "typing_Vale.Interop.Types.__proj__Buffer__item__src",
        "typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
        "typing_Vale.Interop.Types.b8_preorder",
        "typing_Vale.Interop.Types.base_typ_as_type",
        "typing_Vale.Interop.Types.down_view"
      ],
      0,
      "b30eb66fcdb9dde1757b67b36e607ce6"
    ],
    [
      "Vale.X64.BufferViewStore.bv_upd_update_heap128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Interop.Types.b8_preorder",
        "equation_Vale.Interop.Types.base_typ_as_type",
        "equation_Vale.Interop.Types.down_view",
        "equation_Vale.Interop.Types.get_downview",
        "equation_Vale.Interop.Views.up_view128",
        "fuel_guarded_inversion_FStar.Pervasives.dtuple4",
        "fuel_guarded_inversion_LowStar.BufferView.Down.view",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
        "lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
        "primitive_Prims.op_Modulus",
        "proj_equation_FStar.Pervasives.Mkdtuple4__1",
        "proj_equation_FStar.Pervasives.Mkdtuple4__2",
        "proj_equation_FStar.Pervasives.Mkdtuple4__3",
        "proj_equation_LowStar.BufferView.Up.View_n",
        "proj_equation_Vale.Interop.Types.Buffer_bsrc",
        "proj_equation_Vale.Interop.Types.Buffer_src",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.Up.View_n",
        "refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_59430ef12db2c39a3a93c2c604fdc458",
        "refinement_interpretation_Tm_refine_8e5b9681a2aa20517051c843d2d9605b",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_d79f0a949c500daff89dc42b5044fdb6",
        "typing_FStar.UInt8.t",
        "typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
        "typing_Vale.Interop.Types.__proj__Buffer__item__src",
        "typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
        "typing_Vale.Interop.Types.b8_preorder",
        "typing_Vale.Interop.Types.base_typ_as_type",
        "typing_Vale.Interop.Types.down_view"
      ],
      0,
      "78bb568cbc374b8187675e0c7ac08681"
    ]
  ]
]