[ "\u0006oõü_ô­ºt¥|×î¸MU", [ [ "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, "7eea74d5abdcc4cea7124d0703db29d4" ], [ "Vale.AES.GCTR.lemma_counter_init", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented", "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented", "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits", "equation_FStar.UInt.logand", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.mod", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Arch.Types.lo64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_to_two_two", "equation_Vale.Def.Words.Two_s.two_select", "equation_Vale.Def.Words.Two_s.two_to_nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented", "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented", "equation_with_fuel_Prims.pow2.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.bool", "function_token_typing_Vale.Arch.Types.lo64", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "proj_equation_Vale.Def.Words_s.Mktwo_lo", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Vale.Def.Words_s.Mktwo_hi", "projection_inverse_Vale.Def.Words_s.Mktwo_lo", "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_FStar.UInt.to_vec.fuel_instrumented", "token_correspondence_Vale.Arch.Types.lo64_def", "typing_FStar.BitVector.logand_vec", "typing_FStar.Seq.Base.create", "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec", "typing_Prims.pow2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "f9438f9e6a80a8e3b837e523eaebe00a" ], [ "Vale.AES.GCTR.partial_seq_agreement", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000" ], 0, "a3d679e925e04c243d57d1cca27b7e30" ], [ "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, "734574b5b154f2bdc784ddd35a0aceaa" ], [ "Vale.AES.GCTR.gctr_encrypt_block_offset", 2, 1, 0, [ "@query", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Words_s.nat32", "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" ], 0, "cecc2e8c7900d9426448eabaea8a3e5f" ], [ "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, "766554799338a08e9f65ee0d561cc37e" ], [ "Vale.AES.GCTR.gctr_encrypt_empty", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR.make_gctr_plain_LE", "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "55efa00fe456e82945f6da453147a565" ], [ "Vale.AES.GCTR.aes_encrypt_BE", 1, 1, 0, [ "@query" ], 0, "f8fbd26b5e9753eb59d587860a4ada05" ], [ "Vale.AES.GCTR.gctr_registers_def", 1, 1, 0, [ "@query" ], 0, "2f7ed559b8c6b63ad208afdddd5a31c9" ], [ "Vale.AES.GCTR.gctr_registers_reveal", 1, 1, 0, [ "@query" ], 0, "b50c651ed7bbb5df374ef22af49d1d63" ], [ "Vale.AES.GCTR.gctr_partial_def", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000" ], 0, "86ff942833e21a5d7b03aa61c8678f9f" ], [ "Vale.AES.GCTR.gctr_partial_reveal", 1, 1, 0, [ "@query" ], 0, "e9db59c3a9ec69e2924162c6f8b6795e" ], [ "Vale.AES.GCTR.gctr_partial_opaque_init", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.min", "equation_Vale.AES.GCTR.gctr_partial_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.AES.GCTR.gctr_partial", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxInt_proj_0", "token_correspondence_Vale.AES.GCTR.gctr_partial_def" ], 0, "e9f35f0c8f3ac509b4390f713c23d67d" ], [ "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, "60f854c8d17befbf4b86599d49ab726d" ], [ "Vale.AES.GCTR.lemma_gctr_partial_append", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min", "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial_def", "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.AES.GCTR.gctr_partial", "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_LessThanOrEqual", "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_def" ], 0, "757aa8869a93c0ff4c0ad2296a3b246b" ], [ "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, "1b737b17c410248610cba7540aebb322" ], [ "Vale.AES.GCTR.gctr_partial_opaque_ignores_postfix", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.min", "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial_def", "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.AES.GCTR.gctr_partial", "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_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_def", "typing_FStar.Seq.Base.length" ], 0, "e841727f0d8c244723cd5ae0ce9cb8fb" ], [ "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, "9ec22f38fbf02dc3280e23cf2b73637f" ], [ "Vale.AES.GCTR.gctr_partial_extend6", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.min", "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial_def", "equation_Vale.AES.GCTR.inc32lite", "equation_Vale.AES.GCTR_s.inc32", "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.AES.GCTR.gctr_partial", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.AES.GCTR.gctr_partial_def", "typing_FStar.Seq.Base.length", "typing_Prims.min", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0" ], 0, "ff7f6e123399f3173e7afd285da439d6" ], [ "Vale.AES.GCTR.gctr_encrypt_recursive_length", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@fuel_irrelevance_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_e4836109f73687024ac3edd113084865", "binder_x_35779122094374fadf807bdd7bfc8013_2", "binder_x_ae567c2fb75be05905677af440075565_4", "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3", "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0", "binder_x_f960072d0bfae1e534f0393998cf6653_1", "equality_tok_Prims.LexTop@tok", "equation_FStar.Seq.Properties.cons", "equation_FStar.Seq.Properties.head", "equation_FStar.Seq.Properties.tail", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "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_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head", "typing_Vale.AES.AES_s.aes_encrypt_LE", "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Types_s.quad32_xor", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat" ], 0, "04df69a3967fa9deb44da1879cc897fa" ], [ "Vale.AES.GCTR.gctr_encrypt_length", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR_s.gctr_plain_LE", "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a", "refinement_interpretation_Tm_refine_465d996cbf22d32cb08a9b2aefd1ad7b", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3" ], 0, "874774d099ba7619731553dd685c1937" ], [ "Vale.AES.GCTR.gctr_encrypt_length", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_35779122094374fadf807bdd7bfc8013_2", "binder_x_63ff6bedd9b59ccc58bc7a6af3b47a72_1", "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3", "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.Seq.Properties.split", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_plain_LE", "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE", "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "equation_Vale.AES.GCTR_s.pad_to_128_bits", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "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", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE", "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "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_06b9f0ab8ff3c0e49aa83954383f15a4", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.AES.GCTR_s.gctr_encrypt_recursive", "typing_Vale.AES.GCTR_s.pad_to_128_bits", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE" ], 0, "2eb48cf38587714b6a553ef207c4408a" ], [ "Vale.AES.GCTR.gctr_indexed_helper", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.AES.AES_s.aes_key_LE", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3" ], 0, "db28e5133025be0790495f376308dd60" ], [ "Vale.AES.GCTR.gctr_indexed_helper", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@fuel_irrelevance_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_e4836109f73687024ac3edd113084865", "binder_x_35779122094374fadf807bdd7bfc8013_2", "binder_x_ae567c2fb75be05905677af440075565_4", "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3", "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0", "binder_x_f960072d0bfae1e534f0393998cf6653_1", "equality_tok_Prims.LexTop@tok", "equation_FStar.Seq.Properties.cons", "equation_FStar.Seq.Properties.head", "equation_FStar.Seq.Properties.tail", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR.aes_encrypt_BE", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Vale.AES.GCTR.gctr_encrypt_recursive_length", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "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", "refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_86acedbab4aa063aa52cf417ac3141b1", "refinement_interpretation_Tm_refine_8dd65c71dfe8b21be0b6480212d07c90", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_be84f82d45e5967648bfd92d64cb5eca", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f8caad6ddda489be07534c22db7d3ebb", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head", "typing_Vale.AES.AES_s.aes_encrypt_LE", "typing_Vale.AES.GCTR_s.gctr_encrypt_block", "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Types_s.quad32_xor", "typing_Vale.Def.Types_s.reverse_bytes_quad32", "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat" ], 0, "c38b1f2f6106ba0dd399f56a7a7d7b1b" ], [ "Vale.AES.GCTR.gctr_indexed", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.AES.AES_s.aes_key_LE", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3" ], 0, "6a393393f5eb99ec5fe3480ac282a219" ], [ "Vale.AES.GCTR.gctr_indexed", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@query", "binder_x_35779122094374fadf807bdd7bfc8013_2", "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_4", "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3", "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0", "binder_x_f960072d0bfae1e534f0393998cf6653_1", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "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.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_16e48e2e4bd437230f03a1983752209d", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_55d9332cf0766ec1950e1203865a6be7", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_Vale.AES.GCTR_s.gctr_encrypt_recursive" ], 0, "580b2bbd961c888e74fb17f26be02e98" ], [ "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, "084ae574269cb0f33ff439c9b7f68e90" ], [ "Vale.AES.GCTR.gctr_partial_completed", 2, 1, 0, [ "@query", "equation_Prims.min", "equation_Vale.AES.GCTR.gctr_partial_def" ], 0, "0d019b89226f7f24fca4d5ef70cfc4c5" ], [ "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, "bf0f650313265258edc549694155e9eb" ], [ "Vale.AES.GCTR.gctr_partial_opaque_completed", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.l_and", "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.AES.GCTR.gctr_partial", "l_and-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "token_correspondence_Vale.AES.GCTR.gctr_partial_def" ], 0, "7bd5ce4ce55eb295e1f072f2dbf14dcf" ], [ "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, "2896ab69cc68134dba9a064c169f1564" ], [ "Vale.AES.GCTR.gctr_partial_to_full_basic", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def" ], 0, "3c680ad95ea354b0b0e353e8b3e6fc74" ], [ "Vale.AES.GCTR.step1", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Properties.split", "equation_Prims.nat", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes", "equation_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Addition", "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", "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_84a2905827f2440604f2654bb0f156ec", "refinement_interpretation_Tm_refine_86d33b0f21e34d7762468dcd4dbae48d", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "typing_FStar.Seq.Base.slice", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes" ], 0, "6bd2b18bd52fa6c1d4436e2e6199add7" ], [ "Vale.AES.GCTR.lemma_slice_orig_index", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp", "equation_Prims.nat", "equation_Prims.squash", "int_inversion", "l_and-interp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc" ], 0, "04695136081bf78e3e32f82d76613f8a" ], [ "Vale.AES.GCTR.lemma_ishl_32", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "int_inversion", "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_c1424615841f28cac7fc34e92b7ff33c" ], 0, "216be49f23e42ae8b821f8c26705d197" ], [ "Vale.AES.GCTR.lemma_ishl_ixor_32", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "int_inversion", "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_c1424615841f28cac7fc34e92b7ff33c" ], 0, "0e68411cdf548f773939193c578a7290" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_1_helper1", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "4b2f5333c18a91cdc2c650800849b8ba" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_2_helper1", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.natN", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "6a046c2108c295ef2773f568b96814ee" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_3_helper1", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.AES.GCTR.nat24", "equation_Vale.Def.Words_s.natN", "int_inversion", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "2e52debe08ea9f69a2b0ede71a7dbe66" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_1_helper2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "adc6768aaf66a860358120df3c36cd62" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_2_helper2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "a8929df3900bc9807ab0b46366f4c848" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_3_helper2", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "bf9e2444d7051ca6eb7fc09c05b27454" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_1_helper3", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "66ffcf075edf6d286ff42e5a68522dd8" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_2_helper3", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "b3ed05718e206b8af28f251610159ddd" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_3_helper3", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "3984117246913260f2c1708dff17d78e" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_1", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "8f8d80c847005288c0c02d84c2c9ee9c" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_2", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "54ccbafa38c080d85d4621c65ba4b24b" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_3", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "d8943e797e82c14773f90fe673fccb72" ], [ "Vale.AES.GCTR.nat32_xor_bytewise_4", 1, 1, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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_30c926ebf383bedbae82319bb48dcf51", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Def.Words_s.int_to_natN" ], 0, "3591164a95e492784b183a0615657f78" ], [ "Vale.AES.GCTR.nat32_xor_bytewise", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "equation_Vale.Def.Words.Seq_s.seqn", "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_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Vale.Def.Words_s.Mkfour_hi2", "proj_equation_Vale.Def.Words_s.Mkfour_lo0", "proj_equation_Vale.Def.Words_s.Mkfour_lo1", "projection_inverse_BoxBool_proj_0", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice" ], 0, "535660b131703647960b6451354669df" ], [ "Vale.AES.GCTR.lemma_slices_le_quad32_to_bytes", 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", "Vale.AES.GCTR_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f", "Vale.AES.GCTR_interpretation_Tm_arrow_d99575c656699ec1bf0db12d4bfb9bae", "Vale.Def.Words.Four_s_interpretation_Tm_arrow_3411db9d06d17e1f56929dd49c5039c7", "constructor_distinct_Tm_unit", "equation_Prims.nat", "equation_Prims.pos", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Four_s.four_select", "equation_Vale.Def.Words.Seq_s.seq4", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "equation_Vale.Def.Words.Seq_s.seqn", "equation_Vale.Def.Words_s.nat32", "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", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_FStar.Seq.Base.index", "function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes", "function_token_typing_Vale.Def.Words.Four_s.nat_to_four", "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "interpretation_Tm_abs_4f03474956a6a2311e7d7bb19e902da5", "interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43", "interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.init_index_", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "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_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc", "refinement_interpretation_Tm_refine_b75956299d71331caf39bdc95ee7a81c", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd", "token_correspondence_Vale.Def.Words.Four_s.nat_to_four", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Tm_abs_4f03474956a6a2311e7d7bb19e902da5", "typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac", "typing_Vale.Def.Types_s.le_quad32_to_bytes", "typing_Vale.Def.Words.Four_s.four_to_nat", "typing_Vale.Def.Words.Seq_s.four_to_seq_LE", "typing_Vale.Def.Words.Seq_s.seq_to_four_LE", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2", "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1" ], 0, "13aad8687274605d82d4e9fb547a4ba8" ], [ "Vale.AES.GCTR.quad32_xor_bytewise", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Types_s.quad32_xor_def", "equation_Vale.Def.Words.Seq_s.seq_to_four_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.Def.Types_s.quad32_xor", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "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_BoxBool_proj_0", "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_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_49442ef358733fc3ea5275d290f1a90a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_Vale.Def.Types_s.quad32_xor_def", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Vale.Def.Types_s.quad32_xor", "unit_inversion" ], 0, "e27fb1bcb1740819f8d3647d7df0db96" ], [ "Vale.AES.GCTR.slice_pad_to_128_bits", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat", "equation_Vale.AES.GCTR_s.pad_to_128_bits", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "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", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_ee7b6e756c39827ea7822b443c038504", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length" ], 0, "53f18a02e036ee25d904c91c0b4057c9" ], [ "Vale.AES.GCTR.step2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.pad_to_128_bits", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.hasEq_lemma", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ee7b6e756c39827ea7822b443c038504", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length" ], 0, "d4468cf8deb1998746d2be9398ed1078" ], [ "Vale.AES.GCTR.gctr_partial_to_full_advanced", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "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_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", "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, "67a19de8dd20504683acf2d0b618c6e8" ], [ "Vale.AES.GCTR.gctr_partial_to_full_advanced", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.Seq.Properties.split", "equation_Prims.nat", "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.pad_to_128_bits", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Addition", "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_1ba8fd8bb363097813064c67740b2de5", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_e1bea99dc78d1ca62997794b26d8be1c", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_Vale.AES.AES_s.aes_encrypt_LE", "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Types_s.le_quad32_to_bytes", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Def.Types_s.quad32_xor", "typing_Vale.Def.Types_s.reverse_bytes_quad32" ], 0, "0260db60d9ad8005774d595c337bdf97" ], [ "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, "f662e52f27addaecbbcd48588cc13799" ], [ "Vale.AES.GCTR.gctr_encrypt_one_block", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@fuel_irrelevance_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "equation_FStar.Seq.Properties.cons", "equation_FStar.Seq.Properties.head", "equation_FStar.Seq.Properties.tail", "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.GCTR.aes_encrypt_BE", "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE", "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE", "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Properties.slice_is_empty", "primitive_Prims.op_Equality", "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_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0" ], 0, "6f21952df74b3e619f694c830a98a042" ], [ "Vale.AES.GCTR.lemma_length_simplifier", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "bool_inversion", "bool_typing", "eq2-interp", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Properties.slice_length", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan", "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", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes" ], 0, "752eed810f315c2c2abaaf28d0f7cb57" ], [ "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, "147db2e1b9405d2df959e05e47ed346f" ], [ "Vale.AES.GCTR.gctr_bytes_helper", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min", "equation_Prims.nat", "equation_Vale.AES.GCTR.aes_encrypt_BE", "equation_Vale.AES.GCTR.gctr_partial_def", "equation_Vale.AES.GCTR_s.gctr_encrypt_block", "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "fuel_guarded_inversion_Vale.Def.Words_s.four", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AES.GCTR.gctr_partial", "function_token_typing_Vale.AES.GCTR.gctr_partial_def", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_length", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "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_BoxBool_proj_0", "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_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "token_correspondence_Vale.AES.GCTR.gctr_partial", "token_correspondence_Vale.AES.GCTR.gctr_partial_def", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes" ], 0, "794c7d128f086511387acd548d3cbfdb" ] ] ]