Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
Vale.AES.GCTR.fst.hints
[
"\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,
"8b4ba2a0b533c342050fabcdfef1db26"
],
[
"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,
"0996f3bd71eca8140bd4a8dc86e4cada"
],
[
"Vale.AES.GCTR.partial_seq_agreement",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
],
0,
"60f3a8a2a3808a42db6803228e6a4805"
],
[
"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,
"5cb14d74169262d798fce179953413f0"
],
[
"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,
"cc73eab482d8c19efeb62c263a73484a"
],
[
"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,
"b6c1744a485effc2bb59b3c9a9e02787"
],
[
"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,
"3cf870a37e1358710095f74796002c46"
],
[
"Vale.AES.GCTR.aes_encrypt_BE",
1,
1,
0,
[ "@query" ],
0,
"d97ed16cda9636ee5e6ab13ef36c565a"
],
[
"Vale.AES.GCTR.gctr_registers_def",
1,
1,
0,
[ "@query" ],
0,
"1b4c6bcc3156ed71fd0a2c60edb01b2e"
],
[
"Vale.AES.GCTR.gctr_registers_reveal",
1,
1,
0,
[ "@query" ],
0,
"2f85b8f7e8b3a8d9d8245e7783ab37d6"
],
[
"Vale.AES.GCTR.gctr_partial_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
],
0,
"63d5d93d2b91de614883ef504818ce76"
],
[
"Vale.AES.GCTR.gctr_partial_reveal",
1,
1,
0,
[ "@query" ],
0,
"a4dc93b0090e388f5c9871dd2d239769"
],
[
"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,
"d605bca56cbac288477a1e573cfe8a58"
],
[
"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,
"b8df50fce7603dadf93b1d64bf75ac64"
],
[
"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,
"89ed3c698f91276a28a107e6c47c1f3d"
],
[
"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,
"d87bbabeeeda70e79b951ee3720bcd5b"
],
[
"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,
"2f05eed4d12870fdc686634b972956b6"
],
[
"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,
"5f4f17fd7df94f74ad66aa26ebb8f282"
],
[
"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,
"6b2f709c3a6a61a50cfdc67958106747"
],
[
"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,
"8a823c370858a81cace488b356e7ac63"
],
[
"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_37b6dad928076ebef3a59419f9d4f9c3",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3"
],
0,
"12df91a1fbc5d9d90471a7e5eec46bcc"
],
[
"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,
"2255fc0e7d699e7b556abd471eb8d122"
],
[
"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,
"5e56b04b9de849a026b88886a5309964"
],
[
"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,
"1423e1c67494f60967091450b0ba330e"
],
[
"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,
"798097da6d9bc4a290f209b94b8e1920"
],
[
"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,
"820c457123ac59bc7ee5b550b3f486d0"
],
[
"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,
"0a889af31382ee5ecca55cfd8216aa72"
],
[
"Vale.AES.GCTR.gctr_partial_completed",
2,
1,
0,
[
"@query", "equation_Prims.min",
"equation_Vale.AES.GCTR.gctr_partial_def"
],
0,
"7642a0cfbf70906098fc88c2f8a8dd78"
],
[
"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,
"ac323c253ad36980e333927eeb63af30"
],
[
"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,
"c9372dfaafac9f058d5da67b64b6b328"
],
[
"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,
"3dfb10f550809855d8083ccfe13e2a0c"
],
[
"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,
"afa99a9bfeedb33504e82f905ef9014f"
],
[
"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,
"49099f57159f14725e5e2345341bef73"
],
[
"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,
"6df5ef40a003f481f7d7748bf476f9ab"
],
[
"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,
"6c40060c55589f17fe13aae8634480ea"
],
[
"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,
"0b80792a145ba20dbf7d22219e302206"
],
[
"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,
"7fdc08863eb8367069543a5f989e9269"
],
[
"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,
"b6edfd01952c37544650d35ef610e502"
],
[
"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,
"46ff4e3383d061ed1bba6239d245111c"
],
[
"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,
"f677bd3ca2fb67d486fbf2fdfee1e099"
],
[
"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,
"b0aae82a71011373095e83754a689546"
],
[
"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,
"ed456a73ce5bebe915e6875c661ccd2e"
],
[
"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,
"f1d0e31f95a4bc279532fdb0e23d6f1a"
],
[
"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,
"d72da4915b0da8e6605ad5cae52b9352"
],
[
"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,
"cb8cd7ded4bbea701717b47533a094cb"
],
[
"Vale.AES.GCTR.nat32_xor_bytewise_1",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"09bde81047c29e50cc770fea85e1b84a"
],
[
"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,
"4808f5b31fdeebb858703963689998f7"
],
[
"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,
"08f5a3638bfa68e70c27c5cf80c157df"
],
[
"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,
"6795c98e8fcf0e85ac14a11188fd900f"
],
[
"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,
"255607e7ab37c5692fbeabfb9ec08503"
],
[
"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,
"09db6ab2f49d8a44e9463eb875a8fe25"
],
[
"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,
"3b2fa0b45f70d2865c9301f0be0103d5"
],
[
"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,
"9c687d40c117f9e00f053e76562988e8"
],
[
"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,
"22040c5ebf9127deacdfc2307c2bd91f"
],
[
"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,
"ec87a783c742205dc0ef9a38b91991ff"
],
[
"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,
"87649ea2f6fd78096eb9fbf1c2fdf2dd"
],
[
"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,
"301552abcae0a6511d5d748396136fe8"
],
[
"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,
"b7bd4aa9fc7c33a907583c5920340936"
],
[
"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,
"734488a745aa12956bf8eff44de7813f"
],
[
"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,
"bd1c756c5910eab87caadfcd2c00a615"
],
[
"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,
"e50fcf3e2929b6bb5cea8f41d8e74627"
]
]
]
Computing file changes ...
