[
  "��\u0003�V�\u0003\u0010�Mi%\u0013���",
  [
    [
      "Crypto.Plain.repr",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.Seq.Base.seq__uu___haseq",
        "assumption_FStar.UInt8.t__uu___haseq",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes", "equation_Prims.eqtype",
        "function_token_typing_FStar.UInt8.t",
        "haseqFStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "73800ffe16f5fb6982fd5ee6887bf225"
    ],
    [
      "Crypto.Plain.repr",
      2,
      0,
      0,
      [ "@query", "equation_Crypto.Plain.as_bytes" ],
      0,
      "58f915a4631ea59162d579d61ce6c943"
    ],
    [
      "Crypto.Plain.make",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.Seq.Base.seq__uu___haseq",
        "assumption_FStar.UInt8.t__uu___haseq",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes", "equation_Prims.eqtype",
        "function_token_typing_FStar.UInt8.t",
        "haseqFStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "0a86417d523665221640c4792a97b6c8"
    ],
    [
      "Crypto.Plain.make",
      2,
      0,
      0,
      [ "@query", "equation_Crypto.Plain.as_bytes" ],
      0,
      "8aa676a78be79789397ae5f0847ba790"
    ],
    [
      "Crypto.Plain.slice",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.Seq.Base.seq__uu___haseq",
        "assumption_FStar.UInt8.t__uu___haseq",
        "equation_Crypto.Plain.as_bytes", "equation_Crypto.Plain.plain",
        "equation_Crypto.Plain.plainLen",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes", "equation_FStar.UInt32.n",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t", "int_inversion",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Crypto.Plain_Tm_refine_8373bfe7981d84c22aeea0bf45177f5b",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "1d827ac100709a56e0411a0b9eaa98e1"
    ],
    [
      "Crypto.Plain.slice",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Crypto.Plain.as_bytes",
        "equation_Crypto.Plain.plain", "equation_Crypto.Plain.plainLen",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_FStar.UInt8.t",
        "int_inversion", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Crypto.Plain_Tm_refine_8373bfe7981d84c22aeea0bf45177f5b",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "b5b3887e5d20ae9f9fd75bdeadfb6ac6"
    ],
    [
      "Crypto.Plain.as_buffer_injective",
      1,
      0,
      0,
      [
        "@query", "equation_Crypto.Plain.as_buffer",
        "equation_Crypto.Plain.hide_buffer", "unit_typing"
      ],
      0,
      "7a8f6b2361cd297065321219bbce1e5d"
    ],
    [
      "Crypto.Plain.sel_plain",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.v",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "74f00419095199c79612a1d3554d70a5"
    ],
    [
      "Crypto.Plain.sel_plain",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "01a05722dfafb6b58dc969a89f37c702"
    ],
    [
      "Crypto.Plain.bufferRepr",
      1,
      0,
      0,
      [ "@query", "equation_Crypto.Plain.as_buffer" ],
      0,
      "983b3bc8eab84138f44c4af30e8975f5"
    ],
    [
      "Crypto.Plain.create",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_Crypto.Plain.as_buffer", "equation_Crypto.Plain.live",
        "equation_Crypto.Plain.live_", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.unused_in",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Monotonic.HyperStack.unused_in",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.n",
        "haseqCrypto.Plain_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "lemma_FStar.Buffer.lemma_size",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Crypto.Plain_Tm_refine_aa86585edfb0db002b261380c0e511c3",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "token_correspondence_Crypto.Plain.live",
        "token_correspondence_Crypto.Plain.live_", "typing_FStar.UInt32.v"
      ],
      0,
      "20d9c4ad3bd70dd4fb20944615daecdf"
    ],
    [
      "Crypto.Plain.sub",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Crypto.Plain.as_buffer",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
        "equation_FStar.UInt8.t", "fuel_guarded_inversion_FStar.UInt32.t_",
        "lemma_FStar.Buffer.lemma_size", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Crypto.Plain_Tm_refine_83c14f47d42d83320358ace5f80bd393",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "eef6ff677a641e4ad68bca00e3a01201"
    ],
    [
      "Crypto.Plain.load",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.v",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "c68f93040e09298a53aa91e3cabb5d7c"
    ],
    [
      "Crypto.Plain.load",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Crypto.Plain.as_buffer", "equation_Crypto.Plain.live",
        "equation_Crypto.Plain.plain", "equation_Crypto.Plain.plainBuffer",
        "equation_Crypto.Plain.sel_plain",
        "equation_Crypto.Symmetric.Bytes.buffer",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbuffer",
        "equation_Crypto.Symmetric.Bytes.lbytes",
        "equation_Crypto.Symmetric.Bytes.mem",
        "equation_Crypto.Symmetric.Bytes.sel_bytes",
        "equation_FStar.Buffer.buffer",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Prims.eqtype",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "refinement_interpretation_Crypto.Plain_Tm_refine_e292bbea120e8f455adf87c1ff861839",
        "refinement_interpretation_Crypto.Symmetric.Bytes_Tm_refine_0a042ab6539b2f710b0f9b6639051b4e",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Crypto.Symmetric.Bytes.sel_bytes", "typing_FStar.UInt32.v"
      ],
      0,
      "2118a45e0a459b9f1f57576f502fd000"
    ],
    [
      "Crypto.Plain.load",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Crypto.Plain.as_buffer",
        "equation_Crypto.Plain.live", "equation_Crypto.Plain.plain",
        "equation_Crypto.Plain.plainBuffer",
        "equation_Crypto.Plain.sel_plain",
        "equation_Crypto.Symmetric.Bytes.buffer",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbuffer",
        "equation_Crypto.Symmetric.Bytes.lbytes",
        "equation_Crypto.Symmetric.Bytes.sel_bytes",
        "equation_FStar.HyperStack.ST.equal_stack_domains",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.eqtype",
        "function_token_typing_FStar.UInt8.t",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "refinement_interpretation_Crypto.Plain_Tm_refine_e292bbea120e8f455adf87c1ff861839",
        "refinement_interpretation_Crypto.Symmetric.Bytes_Tm_refine_0a042ab6539b2f710b0f9b6639051b4e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "bb9cb7d79c338ec3f207f1bc6641a170"
    ],
    [
      "Crypto.Plain.store",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.v",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "typing_FStar.UInt32.v"
      ],
      0,
      "68230c1bd8cc25b4a04ba975951b093e"
    ],
    [
      "Crypto.Plain.store",
      2,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Crypto.Plain.as_buffer", "equation_Crypto.Plain.live",
        "equation_Crypto.Plain.plain", "equation_Crypto.Plain.plainBuffer",
        "equation_Crypto.Plain.sel_plain",
        "equation_Crypto.Symmetric.Bytes.buffer",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbuffer",
        "equation_Crypto.Symmetric.Bytes.lbytes",
        "equation_Crypto.Symmetric.Bytes.mem",
        "equation_Crypto.Symmetric.Bytes.sel_bytes",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.lseq", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Prims.eqtype",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Seq.Base.lemma_eq_elim", "primitive_Prims.op_AmpAmp",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Crypto.Plain_Tm_refine_e0f4be5bd72b4187a1ad66a3d3f712e3",
        "refinement_interpretation_Crypto.Plain_Tm_refine_e292bbea120e8f455adf87c1ff861839",
        "refinement_interpretation_Crypto.Symmetric.Bytes_Tm_refine_0a042ab6539b2f710b0f9b6639051b4e",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Crypto.Symmetric.Bytes.sel_bytes", "typing_FStar.UInt32.v"
      ],
      0,
      "bc6688113810433ca094d36af4ae422c"
    ],
    [
      "Crypto.Plain.store",
      3,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_Crypto.Plain.as_buffer", "equation_Crypto.Plain.live",
        "equation_Crypto.Plain.plain", "equation_Crypto.Plain.plainBuffer",
        "equation_Crypto.Plain.sel_plain",
        "equation_Crypto.Symmetric.Bytes.bytes",
        "equation_Crypto.Symmetric.Bytes.lbytes",
        "equation_Crypto.Symmetric.Bytes.mem",
        "equation_Crypto.Symmetric.Bytes.sel_bytes",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.lseq",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.eqtype",
        "function_token_typing_FStar.UInt8.t",
        "lemma_FStar.Seq.Base.lemma_eq_elim", "primitive_Prims.op_AmpAmp",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Crypto.Plain_Tm_refine_e0f4be5bd72b4187a1ad66a3d3f712e3",
        "refinement_interpretation_Crypto.Plain_Tm_refine_e292bbea120e8f455adf87c1ff861839",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Crypto.Symmetric.Bytes.sel_bytes"
      ],
      0,
      "09f6d2d670fa0f0e6e157060f0bdfb54"
    ]
  ]
]