[
  "˜œþ\u0001`µL\u0011©\u000f°` ®wÆ",
  [
    [
      "Vale.AES.GCTR_s.gctr_plain_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "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",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "bc29e25fadc895c38dc5c7cdbb621abb"
    ],
    [
      "Vale.AES.GCTR_s.gctr_plain_internal_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "e05c361f2fdde6ef578516039c02ab76"
    ],
    [
      "Vale.AES.GCTR_s.inc32",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "3fe8ada91116daa3160a655b9bcefd17"
    ],
    [
      "Vale.AES.GCTR_s.gctr_encrypt_block",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "bc31da069ec55afff0fbbeb974534141"
    ],
    [
      "Vale.AES.GCTR_s.gctr_encrypt_recursive",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
        "binder_x_f960072d0bfae1e534f0393998cf6653_1",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Equality", "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_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
      ],
      0,
      "4ae35dc56d6e34627f22054354057436"
    ],
    [
      "Vale.AES.GCTR_s.pad_to_128_bits",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "d3339c59c7530aa611d91c9ec2ab68bb"
    ],
    [
      "Vale.AES.GCTR_s.gctr_encrypt_LE_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
      ],
      0,
      "b19783e241a1f22e2098ba4cfffe578b"
    ],
    [
      "Vale.AES.GCTR_s.gctr_encrypt_LE_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4d4e6001dcbe5eaae2d2b65451ea6783"
    ]
  ]
]