[
  "t‹\u001a#)“Hõ\u0004\u0014£,š$\u0007À",
  [
    [
      "Vale.Interop.Cast.ghost_copy_down",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0b23dea46cbec9e3bac7e598e71eae52",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_a8fd90bb3cc2d8f4dcf6e1f70601e62e",
        "refinement_interpretation_Tm_refine_b71eaff53791c4f466c11269feda7320",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_fc6653f1f62a57baa1517a114aaa5d91",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "493006c53b6c7e8fc58bc35d42bafe31"
    ],
    [
      "Vale.Interop.Cast.ghost_copy_down",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_26d9f0cb0b75dc5ac75711633ea9a444_1",
        "binder_x_82be67653007af58de42a56b92d4cc1d_0",
        "binder_x_8d9c81642641581c3cae6c71123c7c65_3",
        "binder_x_8ed5baaa15397c011ac356144c8b6ec8_5",
        "binder_x_acc05a51470ba753956d595e2ae2b961_2",
        "binder_x_b7c72343aa082616726a069a8c7477f5_6",
        "binder_x_bd166185ef88d29d72cbe476bb27c527_4", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "equation_Vale.AsLowStar.MemoryHelpers.low_buffer_read",
        "equation_Views.view128", "equation_Views.view16",
        "equation_Views.view32", "equation_Views.view64",
        "equation_Views.view8", "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "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_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.BufferView.View_n",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.View_n",
        "refinement_interpretation_Tm_refine_0e0ed46577bcb651d36a69c7f10505de",
        "refinement_interpretation_Tm_refine_1f555912ae3584768448647dda876079",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_477a7d568d0ed1dcbd210e9d08fc26e7",
        "refinement_interpretation_Tm_refine_7d9816d4cf109719434f3a807b2954d6",
        "refinement_interpretation_Tm_refine_84e89539aeda328df7dd824b6f8acdf1",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2db5588d185160314a35f78396cdce8",
        "refinement_interpretation_Tm_refine_ce17983e6b32a8f7b43a342e2d1f5095",
        "refinement_interpretation_Tm_refine_e35516723c07b696637886292c8283ee",
        "refinement_interpretation_Tm_refine_f86266de5ffe3d2f8706a2556504fe9c",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "well-founded-ordering-on-nat"
      ],
      0,
      "4e53fcf820b92ab8086c3be45229c076"
    ],
    [
      "Vale.Interop.Cast.copy_down",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
        "equation_Prims.nat", "int_inversion",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_ff88a6ffa07bd660e3b3df07b89c350f",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "fdfef578e5b6d75b1f61e7e93ac97ed7"
    ],
    [
      "Vale.Interop.Cast.copy_down",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Interop.Types.TUInt8",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Pervasives.Native.snd",
        "equation_Interop.Base.base_typ_as_type",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_refl",
        "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0b23dea46cbec9e3bac7e598e71eae52",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4e431b3d67466e2200dbba3d77c38714",
        "refinement_interpretation_Tm_refine_528aaaa219abc36ef466fd246ab839e4",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
        "refinement_interpretation_Tm_refine_8c45889911a77c31036bdf806bd8a126",
        "refinement_interpretation_Tm_refine_980b5b6f0a8b098ae1eb0cc059d7fdb3",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a8fd90bb3cc2d8f4dcf6e1f70601e62e",
        "refinement_interpretation_Tm_refine_b71eaff53791c4f466c11269feda7320",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ff88a6ffa07bd660e3b3df07b89c350f",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_Interop.Base.base_typ_as_type",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_Vale.Interop.Cast.ghost_copy_down", "unit_typing"
      ],
      0,
      "cb747ed2a7dd2c1a8729c1e3997e620d"
    ],
    [
      "Vale.Interop.Cast.ghost_imm_copy_down",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1b1ada1777ab511f3755d9940127528a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5abce8595a375e0b00fb4dfe2ec94cab",
        "refinement_interpretation_Tm_refine_711f69b7c8e3757703e7d0ddf84643f7",
        "refinement_interpretation_Tm_refine_82d3e457c340cfa6e8d6bb27a542661f",
        "refinement_interpretation_Tm_refine_8a619b620352864cf53a7f3ec20f15a8",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.ImmutableBuffer.immutable_preorder"
      ],
      0,
      "b3fc8d398b26cb914e8da13dfe28998f"
    ],
    [
      "Vale.Interop.Cast.ghost_imm_copy_down",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_01560c8a260166f0b28f1957068733af_2",
        "binder_x_82be67653007af58de42a56b92d4cc1d_0",
        "binder_x_83faaca20e6ca768ae177daf27fa45a5_6",
        "binder_x_8c999a51e01f5a2f2ab06a0375916999_4",
        "binder_x_a58a78178c3ce3edd79570b63629bb8c_5",
        "binder_x_a7e50be629974a847614aefa9df8aec9_1",
        "binder_x_e893a2c710c5ed2679592e0d4a22e516_3", "bool_inversion",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "equation_Vale.AsLowStar.MemoryHelpers.imm_low_buffer_read",
        "equation_Views.view128", "equation_Views.view16",
        "equation_Views.view32", "equation_Views.view64",
        "equation_Views.view8",
        "fuel_guarded_inversion_LowStar.BufferView.view",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.BufferView.View_n",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.View_n",
        "refinement_interpretation_Tm_refine_21591f0ccc437c5c6ac52111e87025da",
        "refinement_interpretation_Tm_refine_3f4679acb3b652f09b42dc8e47003b21",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4fdc4ef12351ece62b0a8f72a35617d7",
        "refinement_interpretation_Tm_refine_5ab1dd9cc437fdca6f85a53624c1fce6",
        "refinement_interpretation_Tm_refine_87b5bd9c58a97d6862ffaa025038c5d1",
        "refinement_interpretation_Tm_refine_8acbbef3bb022661f3aedd9a4c8de5a3",
        "refinement_interpretation_Tm_refine_8d9d44fd4b60a404cda68e393cfbfabd",
        "refinement_interpretation_Tm_refine_ac58e1655b00d7c4371aa0f88751d8c9",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c0e28b9f02c7dd4edb5b97d673895c6d",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.ImmutableBuffer.immutable_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "well-founded-ordering-on-nat"
      ],
      0,
      "21144542813d4311d560280c2a5dcb2f"
    ],
    [
      "Vale.Interop.Cast.copy_imm_down",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer",
        "equation_LowStar.ImmutableBuffer.immutable_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f72b0c686d406abb3afa72e6a54839f6",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.ImmutableBuffer.immutable_preorder"
      ],
      0,
      "14226fa3f24e8a79a5e8cdc2962063b5"
    ],
    [
      "Vale.Interop.Cast.copy_imm_down",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Interop.Types.TUInt8",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Pervasives.Native.snd",
        "equation_Interop.Base.base_typ_as_type",
        "equation_LowStar.ImmutableBuffer.ibuffer",
        "equation_LowStar.ImmutableBuffer.immutable_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
        "lemma_FStar.Set.lemma_equal_elim",
        "lemma_FStar.Set.lemma_equal_refl",
        "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
        "lemma_LowStar.Monotonic.Buffer.modifies_refl",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_3aabb156bb2176c5ced859ee21892441",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_528aaaa219abc36ef466fd246ab839e4",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_5abce8595a375e0b00fb4dfe2ec94cab",
        "refinement_interpretation_Tm_refine_711f69b7c8e3757703e7d0ddf84643f7",
        "refinement_interpretation_Tm_refine_82d3e457c340cfa6e8d6bb27a542661f",
        "refinement_interpretation_Tm_refine_8a619b620352864cf53a7f3ec20f15a8",
        "refinement_interpretation_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
        "refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
        "refinement_interpretation_Tm_refine_980b5b6f0a8b098ae1eb0cc059d7fdb3",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_eaeecec4fba6ab00ee6a103ad9901abb",
        "refinement_interpretation_Tm_refine_f72b0c686d406abb3afa72e6a54839f6",
        "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_Interop.Base.base_typ_as_type",
        "typing_LowStar.ImmutableBuffer.immutable_preorder",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_Vale.Interop.Cast.ghost_imm_copy_down", "unit_typing"
      ],
      0,
      "5cade19ffb1d22efda7ea729a0164714"
    ],
    [
      "Vale.Interop.Cast.ghost_copy_up",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "equation_Vale.AsLowStar.MemoryHelpers.low_buffer_read",
        "equation_Views.view128", "equation_Views.view16",
        "equation_Views.view32", "equation_Views.view64",
        "equation_Views.view8", "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.BufferView.View_n",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.View_n",
        "refinement_interpretation_Tm_refine_0b23dea46cbec9e3bac7e598e71eae52",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_528aaaa219abc36ef466fd246ab839e4",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_7ee94e26591a7f356ab0d72826ff5f4e",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "ed3f34da13a4da71d264dbc7d6925108"
    ],
    [
      "Vale.Interop.Cast.imm_ghost_copy_up",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "079a7b1ee0168cf7356e19b3503335a5"
    ],
    [
      "Vale.Interop.Cast.imm_ghost_copy_up",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "equation_Vale.AsLowStar.MemoryHelpers.low_buffer_read",
        "equation_Views.view128", "equation_Views.view16",
        "equation_Views.view32", "equation_Views.view64",
        "equation_Views.view8",
        "fuel_guarded_inversion_LowStar.BufferView.view",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.BufferView.View_n",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.View_n",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_486438805b0fbd0e8a0c4ffb1de1fe55",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_7ee94e26591a7f356ab0d72826ff5f4e",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_Vale.AsLowStar.LowStarSig.view_of_base_typ"
      ],
      0,
      "4292957be14bb632d44e7b93ef43c7b8"
    ],
    [
      "Vale.Interop.Cast.imm_ghost_imm_copy_up",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer",
        "equation_LowStar.ImmutableBuffer.immutable_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8a619b620352864cf53a7f3ec20f15a8",
        "refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.ImmutableBuffer.immutable_preorder"
      ],
      0,
      "e26c9eeea7ae17bdfbdce03194324c50"
    ],
    [
      "Vale.Interop.Cast.imm_ghost_imm_copy_up",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "equation_Vale.AsLowStar.MemoryHelpers.imm_low_buffer_read",
        "equation_Views.view128", "equation_Views.view16",
        "equation_Views.view32", "equation_Views.view64",
        "equation_Views.view8",
        "fuel_guarded_inversion_LowStar.BufferView.view",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_LowStar.BufferView.View_n",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_LowStar.BufferView.View_n",
        "refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8a619b620352864cf53a7f3ec20f15a8",
        "refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_b30ef963d4202213e819607c10c7b223",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d220e72e7d800ba07c9f7e2022090513",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.BufferView.__proj__View__item__n",
        "typing_LowStar.ImmutableBuffer.immutable_preorder",
        "typing_LowStar.Monotonic.Buffer.as_seq",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_Vale.AsLowStar.LowStarSig.view_of_base_typ"
      ],
      0,
      "7563ffc502fe91e5bd325c25b59b0961"
    ],
    [
      "Vale.Interop.Cast.copy_up",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ff88a6ffa07bd660e3b3df07b89c350f",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "38db19846b510d60e1ab2986408b049a"
    ],
    [
      "Vale.Interop.Cast.copy_up",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Pervasives.Native.snd",
        "equation_Interop.Base.base_typ_as_type",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_0b23dea46cbec9e3bac7e598e71eae52",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_528aaaa219abc36ef466fd246ab839e4",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_85c00e5250272611d8e7d8bd746d8541",
        "refinement_interpretation_Tm_refine_8c45889911a77c31036bdf806bd8a126",
        "refinement_interpretation_Tm_refine_ff88a6ffa07bd660e3b3df07b89c350f",
        "typing_Interop.Base.base_typ_as_type",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Vale.Interop.Cast.ghost_copy_up", "unit_typing"
      ],
      0,
      "170de0fc526ed73a61e5ff505f7377e4"
    ],
    [
      "Vale.Interop.Cast.imm_copy_up",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.UInt.min_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat", "int_inversion",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_978d4c33025cd46e2dac7d50698e6899",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "04a86a5eb5a0c7744909a559b6f64078"
    ],
    [
      "Vale.Interop.Cast.imm_copy_up",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Pervasives.Native.snd",
        "equation_FStar.UInt.max_int",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_486438805b0fbd0e8a0c4ffb1de1fe55",
        "refinement_interpretation_Tm_refine_528aaaa219abc36ef466fd246ab839e4",
        "refinement_interpretation_Tm_refine_61faf18202b6c0d55b1dada39c6f22d6",
        "refinement_interpretation_Tm_refine_6df5af68e05bf4b7a3c40c55ea5f5c60",
        "refinement_interpretation_Tm_refine_978d4c33025cd46e2dac7d50698e6899",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_ba56f12e2b7551266be59cf86b4c2644",
        "refinement_interpretation_Tm_refine_d0b573027d6acbe835e429f32a5ec5ad",
        "refinement_interpretation_Tm_refine_dbb053629fecb39929b000133d6971ef",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Vale.Interop.Cast.imm_ghost_copy_up", "unit_typing"
      ],
      0,
      "13a4a3d84a6d945c8235d321be924d0b"
    ],
    [
      "Vale.Interop.Cast.imm_copy_imm_up",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer", "equation_Prims.eqtype",
        "equation_Prims.nat", "int_inversion",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
        "typing_Interop.Base.base_typ_as_type",
        "typing_Interop.Types.view_n",
        "typing_LowStar.ImmutableBuffer.immutable_preorder"
      ],
      0,
      "92436a17f50ca68624ffdf84e34230ad"
    ],
    [
      "Vale.Interop.Cast.imm_copy_imm_up",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "constructor_distinct_Interop.Types.TUInt8",
        "constructor_distinct_Tm_unit",
        "equality_tok_Interop.Types.TUInt8@tok",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Pervasives.Native.snd",
        "equation_Interop.Base.base_typ_as_type",
        "equation_Interop.Types.view_n",
        "equation_LowStar.ImmutableBuffer.ibuffer",
        "equation_LowStar.ImmutableBuffer.immutable_preorder",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "equation_Views.view128",
        "fuel_guarded_inversion_LowStar.BufferView.view",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "proj_equation_LowStar.BufferView.View_n",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_LowStar.BufferView.View_n",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_528aaaa219abc36ef466fd246ab839e4",
        "refinement_interpretation_Tm_refine_5b315bc01144d644a91cef8eeb129a5c",
        "refinement_interpretation_Tm_refine_8a619b620352864cf53a7f3ec20f15a8",
        "refinement_interpretation_Tm_refine_8b17e1f4975ee5a4365d503dd1cd3f04",
        "refinement_interpretation_Tm_refine_ba56f12e2b7551266be59cf86b4c2644",
        "refinement_interpretation_Tm_refine_d220e72e7d800ba07c9f7e2022090513",
        "refinement_interpretation_Tm_refine_e5510aa2cdcf6d7d1e4269aa6735ee82",
        "typing_Interop.Base.base_typ_as_type",
        "typing_LowStar.ImmutableBuffer.immutable_preorder",
        "typing_Vale.AsLowStar.LowStarSig.view_of_base_typ",
        "typing_Vale.Interop.Cast.imm_ghost_imm_copy_up", "unit_typing"
      ],
      0,
      "6c5d385f37d410bea3353509e0c3aed4"
    ]
  ]
]