[
  "\u0014ªÇ\\– 8ðÁת!MÓ\fE",
  [
    [
      "Vale.AES.GCTR.inc32lite",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0"
      ],
      0,
      "03ec49f156beed38d60825e31c98b471"
    ],
    [
      "Vale.AES.GCTR.partial_seq_agreement",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
      ],
      0,
      "ff58a52c447e9d4e88c269e75ed7ad0c"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_block_offset",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "8290df67a79524b47164c88edd9681c9"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_empty",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "0c0ef7d514c9b84b19be5b61a13363f7"
    ],
    [
      "Vale.AES.GCTR.aes_encrypt_BE",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "b0e393c6702a008a9a522f803d87f719"
    ],
    [
      "Vale.AES.GCTR.gctr_registers_def",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ae5c6efecaa4b57371958b0f0a1f43eb"
    ],
    [
      "Vale.AES.GCTR.gctr_registers_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "56135dfb7abbcb4922f31378eb763585"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
      ],
      0,
      "144f0f5a2141f361b681d8cb374b15a2"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "707ec0040d65f0d6b350c6cd4728f85b"
    ],
    [
      "Vale.AES.GCTR.lemma_gctr_partial_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.GCTR.gctr_partial_opaque",
        "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCTR.gctr_partial"
      ],
      0,
      "1c6b64869d9663b75e2e0978fdbc5df8"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_ignores_postfix",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.GCTR.gctr_partial_opaque",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_05a1a488a8ea9b2e17b311a5ff0bb8b1",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "token_correspondence_Vale.AES.GCTR.gctr_partial"
      ],
      0,
      "e56fe34fd7bc978e066eb9fb5bfb2c8b"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_extend6",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "a220bedd08eb3a084f55465ec650302d"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_completed",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Vale.AES.GCTR.gctr_partial",
        "l_and-interp",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "f98689ebd3d5e7ceec3a1e83c9a772fe"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_completed",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "cabf0be6e810bdb4d0ad32172c6139ef"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_to_full_basic",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "l_and-interp",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "5a5f1535ffd2ab047f65be943675c4ad"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_to_full_advanced",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "681ecd88d08f041193842651669cec9a"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_one_block",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "dcdf692fe5e2b9a580242cac363521ee"
    ],
    [
      "Vale.AES.GCTR.gctr_bytes_helper",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.append"
      ],
      0,
      "f97af00ac123402fd7e67fb048b898b9"
    ]
  ]
]