[
  "\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,
      "28e10a292bd6168fae66605020b0a175"
    ],
    [
      "Vale.AES.GCTR.partial_seq_agreement",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
      ],
      0,
      "0d89052c553baf60ea87800e5ad5087e"
    ],
    [
      "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,
      "88d991ce4e1d14a1cf7b2471f740e66b"
    ],
    [
      "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,
      "842e7b3fc5e8cc72f70e95fcffd6bf7e"
    ],
    [
      "Vale.AES.GCTR.aes_encrypt_BE",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8d0d121afee662799bebe97355b7ba34"
    ],
    [
      "Vale.AES.GCTR.gctr_registers_def",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8d4742ff1c3810b66c8ec8fcd6f17862"
    ],
    [
      "Vale.AES.GCTR.gctr_registers_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "91438f6c9f08eeaa648fb6d627479454"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
      ],
      0,
      "5bb69940785d1c642fe69ecd7b93fa63"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d4480efc11c6c1099093290a5441f786"
    ],
    [
      "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,
      "eb25a0f6fc0199c85f3f6a69dd720ceb"
    ],
    [
      "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,
      "b11690dc41e9cd8840fa77b670634d07"
    ],
    [
      "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,
      "b47354e452324e427c2f828a7c90367b"
    ],
    [
      "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,
      "dd40fd2f12292362d28d2e1cb9c8d887"
    ],
    [
      "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,
      "9751311cf6663ddc6a9c1a5d0a0f61c9"
    ],
    [
      "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,
      "648483796b0bad0f722eccafbff8ae60"
    ],
    [
      "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,
      "69ac38f295015f95b9d233006ee4398b"
    ],
    [
      "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,
      "2fbfa1e29f5a6566020c59ad7a980ecb"
    ],
    [
      "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,
      "b70829f09a78b2457223d785a62fd3b4"
    ]
  ]
]