[
  "9��~�\u001bW<�nHQd�\f�",
  [
    [
      "Lib.RawBuffer.blit",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint8",
        "int_inversion", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_45714303651d17b17626bf17b59ae2a7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_FStar.UInt32.v", "typing_FStar.UInt8.t",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf"
      ],
      0,
      "159981fe624d7ef489f341c64f74882d"
    ],
    [
      "Lib.RawBuffer.blit",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.mk_int", "equation_Lib.IntTypes.pub_int_t",
        "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_LowStar.Buffer.trivial_preorder",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt8.uv_inv",
        "lemma_Lib.IntTypes.v_injective",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_321725eb4d16bdb848c74e3894f7a159",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_45714303651d17b17626bf17b59ae2a7",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_f68569b7912e33ebde47e50e220f67a5",
        "true_interp", "typing_FStar.Seq.Base.index",
        "typing_FStar.UInt32.v", "typing_Lib.RawIntTypes.u8_from_UInt8",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
      ],
      0,
      "bd26efb55db8d36f15b43f3529815520"
    ],
    [
      "Lib.RawBuffer.lbytes_eq",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Lib.IntTypes.byte_t",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_none",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_22ea23156c96d1f95a36c1bf3ce83086",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_699abca7bab73696ae075e9bacac2b7d",
        "refinement_interpretation_Tm_refine_69ec46e0fdc9cd5ed2ef9c60fdc7f6e4",
        "refinement_interpretation_Tm_refine_c1fb9a388e64d6307daf25ff6fa12df2",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_FStar.UInt32.v", "typing_FStar.UInt8.t",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.loc_none"
      ],
      0,
      "d6ace28409ab74986553979fd9afdb0e"
    ]
  ]
]