[
  "n\u0003B/U��T�\u0019��Au�",
  [
    [
      "Vale.Interop.Views.get8_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.lseq",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "950aa85292b64410e4ba0e9349c1a24f"
    ],
    [
      "Vale.Interop.Views.get8_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e326a8f70338f3c4b2de377203c589e7"
    ],
    [
      "Vale.Interop.Views.put8_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713",
        "Vale.Interop.Views_interpretation_Tm_arrow_2dd0c4bcae97dc98989285f8c291dc4b",
        "equation_Prims.eqtype", "equation_Prims.nat", "int_typing",
        "interpretation_Tm_abs_90d717ff23a3b502df97d7dd6779d73a",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.UInt8.t",
        "typing_Tm_abs_90d717ff23a3b502df97d7dd6779d73a"
      ],
      0,
      "4e18b05eac9533f8c5e575ca6f16e7b8"
    ],
    [
      "Vale.Interop.Views.put8_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "2591cd69df13d71bab4dfbfb9bf8f59a"
    ],
    [
      "Vale.Interop.Views.up_view8",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Up.inverses",
        "function_token_typing_LowStar.BufferView.Down.inverses",
        "token_correspondence_LowStar.BufferView.Up.inverses"
      ],
      0,
      "8d5c986266280ed3e958c1c7392be098"
    ],
    [
      "Vale.Interop.Views.down_view8",
      1,
      1,
      0,
      [ "@query", "equation_LowStar.BufferView.Down.inverses" ],
      0,
      "4577944471a0a594854f2a508d51dc6d"
    ],
    [
      "Vale.Interop.Views.get16_def",
      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_FStar.UInt.uint_t", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
      ],
      0,
      "d10a26745e8b15c700ac2a0e741eb39c"
    ],
    [
      "Vale.Interop.Views.get16_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5f2df1e44d538d89abe3628e55adfe9f"
    ],
    [
      "Vale.Interop.Views.put16_def",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.UInt8_pretyping_512f0e4172b97206a8b0e16196475713", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_upd", "lemma_FStar.UInt.pow2_values",
        "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_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_FStar.UInt8.t", "typing_Prims.pow2"
      ],
      0,
      "cb06b5d630c9b48180eebc97c2477a16"
    ],
    [
      "Vale.Interop.Views.put16_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "7c4de67d450b8a4038291d6862874f9e"
    ],
    [
      "Vale.Interop.Views.up_view16",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Up.inverses",
        "function_token_typing_LowStar.BufferView.Down.inverses",
        "token_correspondence_LowStar.BufferView.Up.inverses"
      ],
      0,
      "55993f739103db1b3539722a5c5f7dec"
    ],
    [
      "Vale.Interop.Views.down_view16",
      1,
      1,
      0,
      [ "@query", "equation_LowStar.BufferView.Down.inverses" ],
      0,
      "05e3dfb8971d34118d2bf90a9ee0e31b"
    ],
    [
      "Vale.Interop.Views.get32_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "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_Prims.eqtype",
        "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "lemma_FStar.Seq.Base.lemma_init_len", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "9224ca6b2f136caaf31ca3ace871f106"
    ],
    [
      "Vale.Interop.Views.get32_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d59413d6cf892fe661853d94ff066d0a"
    ],
    [
      "Vale.Interop.Views.put32_def",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "67e958e7170a65d139bf8ab2d52d48aa"
    ],
    [
      "Vale.Interop.Views.put32_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4d1595321d922da231ca55ea8222ed26"
    ],
    [
      "Vale.Interop.Views.up_view32",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Up.inverses",
        "function_token_typing_LowStar.BufferView.Down.inverses",
        "token_correspondence_LowStar.BufferView.Up.inverses"
      ],
      0,
      "6826257ca0d497b21ead231e249bc2df"
    ],
    [
      "Vale.Interop.Views.down_view32",
      1,
      1,
      0,
      [ "@query", "equation_LowStar.BufferView.Down.inverses" ],
      0,
      "e07e019bf1e4bd1cce9d7f58fb23385a"
    ],
    [
      "Vale.Interop.Views.get64_def",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "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_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "80e439ad3884f52d42a575f28415e1e5"
    ],
    [
      "Vale.Interop.Views.get64_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "abebf7ae47509aa9b7f3c244cea68760"
    ],
    [
      "Vale.Interop.Views.put64_def",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "8476bc3c2b0b53a21afce1f80f32a656"
    ],
    [
      "Vale.Interop.Views.put64_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "35845555b45924609ec0b807a3347974"
    ],
    [
      "Vale.Interop.Views.up_view64",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Up.inverses",
        "function_token_typing_LowStar.BufferView.Down.inverses",
        "token_correspondence_LowStar.BufferView.Up.inverses"
      ],
      0,
      "98c2c5751cccd54690681708a5bc8e65"
    ],
    [
      "Vale.Interop.Views.down_view64",
      1,
      1,
      0,
      [ "@query", "equation_LowStar.BufferView.Down.inverses" ],
      0,
      "4c56fe31b6f12eb91128055f22de85e8"
    ],
    [
      "Vale.Interop.Views.get128_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "equation_FStar.Seq.Properties.lseq", "equation_Prims.eqtype",
        "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "ae255928f57af16be5f355d1cbfa7e0f"
    ],
    [
      "Vale.Interop.Views.get128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "325d211b2571c856d94e28bc018b1f74"
    ],
    [
      "Vale.Interop.Views.put128_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "equation_Prims.eqtype",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt8.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "81994e3442b34308c96e3d91cc7f6308"
    ],
    [
      "Vale.Interop.Views.put128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "f371c5fea48af6d58c5b9be1f7045fd4"
    ],
    [
      "Vale.Interop.Views.up_view128",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Up.inverses",
        "equation_Vale.Def.Types_s.quad32",
        "function_token_typing_LowStar.BufferView.Down.inverses",
        "token_correspondence_LowStar.BufferView.Up.inverses"
      ],
      0,
      "c0328a4f9d26b42f0f790de99d8cd3a1"
    ],
    [
      "Vale.Interop.Views.down_view128",
      1,
      1,
      0,
      [ "@query", "equation_LowStar.BufferView.Down.inverses" ],
      0,
      "3aa783e92f591ac10ac64c59830c4cfa"
    ],
    [
      "Vale.Interop.Views.nat32s_to_nat128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "dbea565fe6e4fa3dc06c5499d6735a92"
    ],
    [
      "Vale.Interop.Views.get32_128_def",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "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_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
      ],
      0,
      "5d35627004bc88428f6b658106293b15"
    ],
    [
      "Vale.Interop.Views.get32_128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "eea302eeb022e3ea331a89656d0f0299"
    ],
    [
      "Vale.Interop.Views.put32_128_def",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values", "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.t",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_LE"
      ],
      0,
      "d713953ed023a4c667da5f4bfddd221f"
    ],
    [
      "Vale.Interop.Views.put32_128_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4d00d1e74773c5cdd471ff3c5f9ea355"
    ],
    [
      "Vale.Interop.Views.view32_128",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Properties.lseq",
        "equation_LowStar.BufferView.Up.inverses",
        "equation_Vale.Def.Types_s.quad32",
        "function_token_typing_LowStar.BufferView.Down.inverses",
        "token_correspondence_LowStar.BufferView.Up.inverses"
      ],
      0,
      "1a8b8b32c833275bdb2455b744a07e86"
    ]
  ]
]