https://github.com/project-everest/hacl-star
Tip revision: 2ca2d4dce9eb1dc7ac015a04cd6af6ac0e926e59 authored by Santiago Zanella-Beguelin on 17 July 2018, 13:56:19 UTC
WIP replicating LowStar library in Lib
WIP replicating LowStar library in Lib
Tip revision: 2ca2d4d
Hacl.Impl.Xor.Lemmas.fst.hints
[
"`²ü'[ZxÖ*ś\u0013Ø\u0013\u0006yN",
[
[
"Hacl.Impl.Xor.Lemmas.little_bytes_def_0",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
"equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
"int_typing", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"9209b6d2b2f65c7a7b1f60aed518c66a"
],
[
"Hacl.Impl.Xor.Lemmas.little_bytes_def_1",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.n", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Endianness_Tm_refine_1e62df159c33fd3091667f8254d1ab80",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2a1f1ed4a1fc43b405a8694230052ec4",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt32.v"
],
0,
"6a10de8ec619bd321db50fe000b9c0f0"
],
[
"Hacl.Impl.Xor.Lemmas.little_bytes_def_0",
2,
1,
1,
[
"@MaxFuel_assumption",
"@fuel_correspondence_FStar.Endianness.little_bytes.fuel_instrumented",
"@query",
"equation_with_fuel_FStar.Endianness.little_bytes.fuel_instrumented",
"primitive_Prims.op_Equality"
],
0,
"ebdfa74b6aa8a0068632389229f328bb"
],
[
"Hacl.Impl.Xor.Lemmas.little_bytes_def_1",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.Endianness.little_bytes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_FStar.Endianness.little_bytes.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "b2t_def",
"equation_FStar.Endianness.bytes",
"equation_FStar.Endianness.lbytes", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
"equation_Prims.nat",
"equation_with_fuel_FStar.Endianness.little_bytes.fuel_instrumented",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_FStar.UInt8.t", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Endianness_Tm_refine_1e62df159c33fd3091667f8254d1ab80",
"refinement_interpretation_FStar.Endianness_Tm_refine_93ce8845fd1f231820c6e8c088a3187e",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2a1f1ed4a1fc43b405a8694230052ec4",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Endianness.little_bytes",
"typing_FStar.Seq.Base.createEmpty", "typing_FStar.UInt32.v"
],
0,
"8d6ab15e5102917e04596bc14e6b3d60"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_uint32_to_le_def",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
"bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"function_token_typing_FStar.UInt32.n", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.UInt32.v"
],
0,
"cf5252162f53ce51df75edcd95af343f"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_uint32_to_le_def",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.Endianness.little_bytes.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.BitVector.shift_right_vec",
"equation_FStar.BitVector.zero_vec",
"equation_FStar.Endianness.bytes",
"equation_FStar.Endianness.lbytes", "equation_FStar.Int16.n",
"equation_FStar.Seq.Properties.cons", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.Int16.n",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"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_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt.shift_right_value_lemma",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Endianness_Tm_refine_1e62df159c33fd3091667f8254d1ab80",
"refinement_interpretation_FStar.Endianness_Tm_refine_93ce8845fd1f231820c6e8c088a3187e",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt32_Tm_refine_bffb82e1cd67a5f9ca62c2b0a955a3a7",
"refinement_interpretation_FStar.UInt32_Tm_refine_f5c241a114fe55ee9c3ce622243adf05",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2a1f1ed4a1fc43b405a8694230052ec4",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2c5877279a4f7b26508ada5ec9814d35",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2fd18de7bf4e6f7ab61dbb9c75218573",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_b8b3ffeef206e01f21f7c6f6f660425f",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_b99b1288b0a8cbc50f85740740b2b9c6",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Seq.Create_Tm_refine_37e9e2c96c7fceb94a3908c53e2ae85b",
"typing_FStar.BitVector.shift_right_vec",
"typing_FStar.BitVector.zero_vec",
"typing_FStar.Endianness.little_bytes",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.logand",
"typing_FStar.UInt.to_vec", "typing_FStar.UInt32.logand",
"typing_FStar.UInt32.shift_right", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Prims.pow2",
"typing_Seq.Create.create_4"
],
0,
"45d0ebb1e414175eb4725eb22726ba20"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec1",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logxor_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_1b1aa502f8001995fe80a1b40f1161c1",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_57594f310edc655e8da2d1769b99333d",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.logxor_vec", "typing_FStar.UInt.to_vec",
"typing_FStar.UInt32.v"
],
0,
"3f32b945017c27d908133d90d41580ad"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec1",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logxor_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.BitVector.logxor_vec_definition",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_1b1aa502f8001995fe80a1b40f1161c1",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_5d3256f9fafdfaf1fcafcdbdcb2cca7d",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_ea21cf9155d202d45a739fed7f941d47",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.logxor_vec", "typing_FStar.UInt.to_vec",
"typing_FStar.UInt32.v"
],
0,
"89f66e1ad67ec02cd1a52fb379f9c17a"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec2",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.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.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_FStar.UInt32.v"
],
0,
"80e864da8d1eacb81bfe86aa30f1dea1"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec2",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.BitVector.shift_right_vec",
"equation_FStar.BitVector.zero_vec", "equation_FStar.Int16.n",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.shift_right", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_FStar.Int16.n",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.BitVector.shift_right_vec_lemma_2",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_vec_lemma", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.BitVector_Tm_refine_ddf0757b7b57c93f9731d2df235a714c",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_279f1fe025d23cb48ed90106e0ca3c1b",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2bbff8ea9be82ccac62b5a1f19ace0d1",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_5f0044d4dc78e254d3a145d409df4ead",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.shift_right_vec",
"typing_FStar.BitVector.zero_vec", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt.min_int", "typing_FStar.UInt.to_vec",
"typing_FStar.UInt32.v"
],
0,
"5ed49811718ef47d6cc4701e89b7bc34"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec3",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Seq.Base.seq__uu___haseq",
"assumption_Prims.HasEq_bool", "b2t_def", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.n",
"equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool", "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_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"82ba97faeea6f0ece1669312c9f96344"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec3",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Seq.Base.seq__uu___haseq",
"assumption_Prims.HasEq_bool", "b2t_def", "bool_inversion",
"bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.BitVector.ones_vec",
"equation_FStar.BitVector.zero_vec", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.ones", "equation_FStar.UInt.size",
"equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Prims.bool",
"haseqFStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"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_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_FStar.UInt.index_to_vec_ones",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_8ae4abcfc6bc8d4903b7e1f40e070ec2",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_31e52f4bed34f8c031bec7e8fc7d226f",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.ones_vec", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
],
0,
"deb2ea33bf09a7436499b5d73c121ef4"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec4",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n",
"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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt.to_vec", "typing_FStar.UInt32.v"
],
0,
"71dcc894fa9f846e3661a0dd897532e8"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec4",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_Prims.HasEq_bool", "b2t_def", "bool_inversion",
"bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.BitVector.ones_vec",
"equation_FStar.BitVector.zero_vec", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.BitVector.logand_vec_definition",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"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_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_ea02e13ec8936a32234ab0190f4821d6",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.logand_vec", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt.to_vec", "typing_FStar.UInt32.v"
],
0,
"6e2a38a5d56531689dec2654d755e837"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec5",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Seq.Base.seq__uu___haseq",
"assumption_Prims.HasEq_bool", "b2t_def", "bool_inversion",
"bool_typing", "equation_FStar.BitVector.bv_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_FStar.UInt32.v"
],
0,
"5c43761b3bf437f68520290e3adc9f1f"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_vec5",
2,
0,
1,
[
"@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", "@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.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"equation_Prims.pos", "function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.UInt.inverse_vec_lemma", "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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.logand_vec", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_FStar.UInt32.v"
],
0,
"d91e751493759ac28652da5d87b77376"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_uint32_to_uint8_vec",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
"equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool",
"haseqHacl.Impl.Xor.Lemmas_Tm_refine_194d57fab4ae23438b3b32f440a433b9",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v"
],
0,
"b740040ba184bc39cdbcacbf44eb24f6"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_uint32_to_uint8_vec",
2,
0,
1,
[
"@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", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_Prims.HasEq_int", "b2t_def",
"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.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.UInt.inverse_num_lemma",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt32.vu_inv",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt32_Tm_refine_f5c241a114fe55ee9c3ce622243adf05",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.BitVector.logand_vec", "typing_FStar.UInt.logand",
"typing_FStar.UInt.to_vec", "typing_FStar.UInt32.logand",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v"
],
0,
"f70a5297261eb8bac96684655f65ae89"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_uint32_to_le_def2",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
"equation_FStar.BitVector.bv_t", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v"
],
0,
"8a8b18d4ae1273d577ff916196ab5d21"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_uint32_to_le_def2",
2,
0,
1,
[ "@query" ],
0,
"0b7ccc70e7c0e4ab4f8cbf6c1412b8ea"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_uint32_to_bytes",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Spec.Lib.lbytes", "equation_Spec.Lib.uint32_to_le",
"function_token_typing_FStar.UInt32.n",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_Spec.Lib.uint32_to_le"
],
0,
"e17eb8153646294066d5618f4224f389"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_uint32_to_bytes",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logxor_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"binder_x_c83ce316d405fb48b0bd99c26a4c5fd3_0",
"binder_x_c83ce316d405fb48b0bd99c26a4c5fd3_1", "bool_typing",
"equation_FStar.BitVector.bv_t", "equation_FStar.Endianness.bytes",
"equation_FStar.Endianness.lbytes", "equation_FStar.Int16.n",
"equation_FStar.UInt.fits", "equation_FStar.UInt.logxor",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Lib.uint32_to_le",
"function_token_typing_FStar.Int16.n",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.inverse_vec_lemma", "lemma_FStar.UInt8.uv_inv",
"lemma_FStar.UInt8.vu_inv", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt8_Tm_refine_22871ed0ff70fd094ad3e8d742624d47",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_3ce2589b82e1f5009cba5ebd39656287",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_47ca42c1e30622250c42386a0bbda096",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_59d5c761af173148075c6a2b8c9c4875",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_c0cd23a0177fa387ff2efd2ea9ad97b8",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_fe09877173ed71aa723e07c8a9967041",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Seq.Create_Tm_refine_37e9e2c96c7fceb94a3908c53e2ae85b",
"typing_FStar.BitVector.logxor_vec", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt.from_vec", "typing_FStar.UInt.to_vec",
"typing_FStar.UInt32.v", "typing_FStar.UInt8.uint_to_t",
"typing_FStar.UInt8.v", "typing_Seq.Create.create_4"
],
0,
"cc86211ceb7f728e90ee53e01d4d72b0"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_uint32s_to_bytes_",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Spec.Lib.lbytes", "function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt32.t",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_4639d389381bee5cf8cf77b7a6585074",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"75c68cceeeed53a89cd76bf3fda47ccd"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_uint32s_to_bytes_",
2,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Lib.uint32s_to_le.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "b2t_def",
"binder_x_7a21a38c85f23dcc37cbbd2fb726200f_1", "bool_inversion",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.snoc", "equation_FStar.UInt.fits",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_Hacl.Impl.Xor.Lemmas.u32",
"equation_Prims.nat", "equation_Spec.Lib.lbytes",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt32.t",
"function_token_typing_FStar.UInt8.t",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"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",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt32_Tm_refine_ad29e51736af79cc18f0e95a10768f33",
"refinement_interpretation_FStar.UInt8_Tm_refine_6206cb0b0b93a50ffdc1567233aaeb47",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_04e414d21bf90443142130c3b762dfcd",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_0a5886e6d023c5996305b95954d3b3c3",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_2068e6a1f5c7be334f17d2f8a7d3a001",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_5b0119b55ccddf34f4cf05e921b97113",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_8539133a23b9553305a5691ed734b08e",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_89a31cbc53ccf459d02aaa5b57db03f0",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_a8dbea419b68877fd04c7f47e8ae2d21",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_ae144950b7a783ce6dac9ffc6080a692",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_ce729abba129ce4d37730569ca24b471",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_e4fccf9eb7eeff6764446d120509935d",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_fc445105cc88ce675540b399c6b5ad5c",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Loops_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
"refinement_interpretation_Spec.Loops_Tm_refine_4af88ef44277488ec061969a3d7abb20",
"token_correspondence_FStar.UInt32.logxor",
"token_correspondence_FStar.UInt8.logxor",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.logxor", "typing_FStar.UInt32.v",
"typing_FStar.UInt8.logxor", "typing_Spec.Lib.uint32_to_le",
"typing_Spec.Lib.uint32s_to_le", "typing_Spec.Loops.seq_map2",
"well-founded-ordering-on-nat"
],
0,
"1ae31f6e73ef42c0badc4bdcc9f88f1e"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_uint32s_to_bytes",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"equation_Spec.Lib.lbytes", "function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.t",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_c12f321297c5a39bedc838b37026fdff",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_fd7d3082a09af4f36a44220dfa6b97ac",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"08a1f229af80482ec2d93e6897acfca1"
],
[
"Hacl.Impl.Xor.Lemmas.lemma_xor_uint32s_to_bytes",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
"equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_c12f321297c5a39bedc838b37026fdff",
"refinement_interpretation_Hacl.Impl.Xor.Lemmas_Tm_refine_fd7d3082a09af4f36a44220dfa6b97ac"
],
0,
"bc3287ef6e262c02758a5b520db01f07"
]
]
]