Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Vale.Arch.Types.fst.hints
[
"t�9ߵ LW�j���o�",
[
[
"Vale.Arch.Types.lemma_nat_to_two32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "int_typing",
"lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"252eeb89c634247fbc6589efa3e95f23"
],
[
"Vale.Arch.Types.lemma_nat_to_two32",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "int_typing",
"lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d657313e832f90b9da2597122651ce83"
],
0,
"3b129669aa928cdb83bc169d6e2dab95"
],
[
"Vale.Arch.Types.lemma_BitwiseXorCommutative",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "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.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"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", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
"typing_Vale.Def.Types_s.ixor"
],
0,
"8ac47ce7f2c2da526ca9f5cf7b2ab34a"
],
[
"Vale.Arch.Types.lemma_BitwiseXorWithZero",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@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.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Vale.Def.Types_s.ixor"
],
0,
"4d9c8faf5744088ee95ce1ef644ba644"
],
[
"Vale.Arch.Types.lemma_BitwiseXorCancel",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "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_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2"
],
0,
"f4007879e743d18a5749259de25d4fea"
],
[
"Vale.Arch.Types.lemma_BitwiseXorCancel64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "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_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2897f455bd1a2e7bd7f8f1aa6ce63472",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c6633917f79a67f4eaac4ed70320fc6",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Prims.pow2"
],
0,
"05ccc330201aa5fdb58ebab20eaa451d"
],
[
"Vale.Arch.Types.lemma_BitwiseXorAssociative",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "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_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ca87202d8e02d1c00a86cd121980a4f",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt.fits",
"typing_FStar.UInt.to_vec", "typing_Vale.Def.Types_s.ixor"
],
0,
"1cf3f3fbf99ad220ffb72b7a1b3a75cb"
],
[
"Vale.Arch.Types.xor_lemmas",
1,
1,
0,
[ "@query" ],
0,
"e7b40ece0f4eeb8ca4afa31372e75aa8"
],
[
"Vale.Arch.Types.lemma_quad32_xor",
1,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"data_elim_Vale.Def.Words_s.Mkfour",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Types_s.quad32_xor",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def"
],
0,
"40e4f76148c9774528cae8a5e2b053eb"
],
[
"Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2",
"equation_Prims.nat", "equation_Vale.Def.Types_s.nat32_to_be_bytes",
"equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
"equation_Vale.Def.Words.Seq_s.seq4",
"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.reverse_seq",
"function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_Vale.Lib.Seqs.reverse_reverse_seq",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"typing_Vale.Def.Types_s.nat32_to_be_bytes"
],
0,
"bf0fc2a0c066ae7901dfd63d5dc5d4ff"
],
[
"Vale.Arch.Types.lemma_reverse_bytes_quad32",
1,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"data_elim_Vale.Def.Words_s.Mkfour", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_reverse",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
"lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"03cc4e591e59139eed3c90bedb5337d0"
],
[
"Vale.Arch.Types.lemma_reverse_bytes_nat32",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.be_bytes_to_nat32",
"equation_Vale.Def.Types_s.nat32_to_be_bytes",
"equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
"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.reverse_seq",
"function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"interpretation_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"lemma_FStar.Seq.Base.init_index_",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"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_a",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2",
"typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
"typing_Vale.Def.Types_s.nat32_to_be_bytes",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.Def.Words.Seq_s.seq_to_four_BE",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3"
],
0,
"f9a1e6222dcbe66e7117bb9f05b16ed8"
],
[
"Vale.Arch.Types.lemma_reverse_bytes_quad32_zero",
1,
1,
0,
[
"@query", "equation_Vale.Def.Words.Four_s.four_reverse",
"equation_Vale.Def.Words_s.nat32",
"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,
"82e11c1c8f8abfaed1e4d931efd32b83"
],
[
"Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_seq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_afc033f4783947c3d425ff758d5e540a",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Types_s.reverse_bytes_nat32_seq"
],
0,
"91be6b5c3d2600f5b70f3b6bc10925d0"
],
[
"Vale.Arch.Types.lemma_insert_nat64_properties",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Types_s.insert_nat64_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_to_two_two",
"equation_Vale.Def.Words.Four_s.two_two_to_four",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words.Two_s.two_insert",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Types_s.insert_nat64",
"int_inversion", "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",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"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",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Def.Types_s.insert_nat64_def"
],
0,
"eb45e8c2f9a65194ebeb3e73c321e615"
],
[
"Vale.Arch.Types.lemma_insert_nat64_nat32s",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Vale.Def.Types_s.insert_nat64_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_to_two_two",
"equation_Vale.Def.Words.Four_s.two_two_to_four",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words.Two_s.two_insert",
"equation_Vale.Def.Words.Two_s.two_to_nat",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Types_s.insert_nat64",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Two.nat_to_two_to_nat",
"primitive_Prims.op_Multiply", "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",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Def.Types_s.insert_nat64_def"
],
0,
"40732af265fa788116f9d779493646e2"
],
[
"Vale.Arch.Types.lo64_reveal",
1,
1,
0,
[ "@query" ],
0,
"2fbf252a0e3cc2408ccc821536b44678"
],
[
"Vale.Arch.Types.hi64_reveal",
1,
1,
0,
[ "@query" ],
0,
"f62adb789a48b25c37f7f1fb8a4076d3"
],
[
"Vale.Arch.Types.lemma_lo64_properties",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "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_s.nat32",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Arch.Types.lo64", "int_typing",
"lemma_FStar.UInt.pow2_values", "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_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.Arch.Types.lo64_def"
],
0,
"b499cddb984017d6a63f5ddff1c76530"
],
[
"Vale.Arch.Types.lemma_hi64_properties",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Vale.Arch.Types.hi64_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_s.nat32",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Arch.Types.hi64", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"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.Mktwo_hi",
"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_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.Arch.Types.hi64_def"
],
0,
"348e1dfdff320ae28d241fc04d3d50fd"
],
[
"Vale.Arch.Types.lemma_reverse_bytes_nat64_32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.reverse_bytes_nat64_def",
"equation_Vale.Def.Words.Two_s.two_to_nat",
"equation_Vale.Def.Words_s.nat32",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Vale.Def.Types_s.reverse_bytes_nat64",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Two.nat_to_two_to_nat",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat64_def",
"typing_Prims.pow2"
],
0,
"671cb623697865409419eb9d80818a09"
],
[
"Vale.Arch.Types.lemma_reverse_bytes_quad32_64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.Types.hi64_def",
"equation_Vale.Arch.Types.lo64_def",
"equation_Vale.Def.Types_s.reverse_bytes_nat64_def",
"equation_Vale.Def.Words.Four_s.four_reverse",
"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_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Vale.Arch.Types.hi64",
"function_token_typing_Vale.Arch.Types.lo64",
"function_token_typing_Vale.Def.Types_s.reverse_bytes_nat64",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Two.nat_to_two_to_nat",
"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_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"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",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Arch.Types.hi64_def",
"token_correspondence_Vale.Arch.Types.lo64_def",
"token_correspondence_Vale.Def.Types_s.reverse_bytes_nat64_def",
"typing_Prims.pow2"
],
0,
"502c63db188c5f316027a4b9f6d8b6ff"
],
[
"Vale.Arch.Types.lemma_equality_check_helper",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_elim_Vale.Def.Words_s.Mkfour",
"data_elim_Vale.Def.Words_s.Mktwo", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Arch.Types.hi64_def",
"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.nat1", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.Def.Words_s.two",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Arch.Types.hi64",
"function_token_typing_Vale.Arch.Types.lo64",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.two@tok",
"l_quant_interp_170d6477ea866701a90ae6e76923559c",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Equality",
"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",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.Types.hi64_def",
"token_correspondence_Vale.Arch.Types.lo64_def",
"typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64",
"typing_Vale.Def.Words.Four_s.four_to_two_two",
"typing_Vale.Def.Words.Two_s.two_select",
"typing_Vale.Def.Words_s.__proj__Mktwo__item__lo",
"typing_Vale.Def.Words_s.int_to_natN"
],
0,
"0b6bbfdfe918ef48a1bb8750668e1c3d"
],
[
"Vale.Arch.Types.lemma_equality_check_helper_2",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"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",
"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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"5f24b2a456efce2cf79f84e2bf90ea72"
],
[
"Vale.Arch.Types.push_pop_xmm",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_elim_Vale.Def.Words_s.Mkfour",
"data_elim_Vale.Def.Words_s.Mktwo", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Arch.Types.hi64_def",
"equation_Vale.Arch.Types.lo64_def",
"equation_Vale.Def.Types_s.insert_nat64_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_to_two_two",
"equation_Vale.Def.Words.Four_s.two_two_to_four",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words.Two_s.two_insert",
"equation_Vale.Def.Words.Two_s.two_select",
"equation_Vale.Def.Words.Two_s.two_to_nat",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.Def.Words_s.two",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Arch.Types.hi64",
"function_token_typing_Vale.Arch.Types.lo64",
"function_token_typing_Vale.Def.Types_s.insert_nat64",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.two@tok",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Two.nat_to_two_to_nat",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"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.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Arch.Types.hi64_def",
"token_correspondence_Vale.Arch.Types.lo64_def",
"token_correspondence_Vale.Def.Types_s.insert_nat64_def",
"typing_Prims.pow2", "typing_Vale.Arch.Types.hi64",
"typing_Vale.Arch.Types.lo64",
"typing_Vale.Def.Words.Four_s.four_to_two_two",
"typing_Vale.Def.Words.Two_s.nat_to_two",
"typing_Vale.Def.Words.Two_s.two_insert",
"typing_Vale.Def.Words.Two_s.two_select",
"typing_Vale.Def.Words_s.int_to_natN"
],
0,
"c35f178da78acb39d000a93c7af75f15"
],
[
"Vale.Arch.Types.lemma_insrq_extrq_relations",
1,
3,
3,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_elim_Vale.Def.Words_s.Mkfour", "equation_Prims.nat",
"equation_Vale.Arch.Types.hi64_def",
"equation_Vale.Arch.Types.lo64_def",
"equation_Vale.Def.Types_s.insert_nat64_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_to_two_two",
"equation_Vale.Def.Words.Four_s.two_two_to_four",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words.Two_s.two_insert",
"equation_Vale.Def.Words.Two_s.two_select",
"equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"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_Vale.Arch.Types.hi64",
"function_token_typing_Vale.Arch.Types.lo64",
"function_token_typing_Vale.Arch.Types.lo64_def",
"function_token_typing_Vale.Def.Types_s.insert_nat64",
"function_token_typing_Vale.Def.Types_s.insert_nat64_def",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Arch.Types.lemma_insert_nat64_properties",
"primitive_Prims.op_Multiply", "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",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"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.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.Types.hi64_def",
"token_correspondence_Vale.Def.Types_s.insert_nat64_def",
"typing_Vale.Arch.Types.hi64", "typing_Vale.Arch.Types.lo64_def",
"typing_Vale.Def.Types_s.insert_nat64"
],
0,
"c2f573fd6dfad15ee16e7ab7ea30bd0e"
],
[
"Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
1,
3,
3,
[ "@query" ],
0,
"c048cf8600e8e5586c61fadcaf45b310"
],
[
"Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
2,
3,
3,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"data_typing_intro_Vale.Def.Words_s.Mktwo@tok", "equation_Prims.nat",
"equation_Prims.pos",
"equation_Vale.Def.Types_s.le_bytes_to_nat64_def",
"equation_Vale.Def.Types_s.le_nat64_to_bytes_def",
"equation_Vale.Def.Words.Seq_s.seq2",
"equation_Vale.Def.Words.Seq_s.seq_to_two_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_nat64",
"function_token_typing_Vale.Def.Types_s.le_nat64_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
"lemma_Vale.Def.Words.Two.two_to_nat_to_two",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"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_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f9ee523a22c7eb000c4c8d4de6592dcb",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def",
"token_correspondence_Vale.Def.Types_s.le_nat64_to_bytes_def",
"typing_Prims.pow2", "typing_Vale.Def.Types_s.le_nat64_to_bytes",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Def.Words.Seq_s.two_to_seq_LE",
"typing_Vale.Def.Words_s.natN"
],
0,
"3c071f94b0b94b556d66737ed96c8385"
],
[
"Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
1,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619"
],
0,
"589190f2b41993535738bc0da0c13e6e"
],
[
"Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
2,
3,
3,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat",
"equation_Vale.Def.Types_s.le_bytes_to_nat64_def",
"equation_Vale.Def.Types_s.le_nat64_to_bytes_def",
"equation_Vale.Def.Words.Seq_s.seq2",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_to_two_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",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_nat64",
"function_token_typing_Vale.Def.Types_s.le_nat64_to_bytes",
"function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE",
"lemma_Vale.Def.Words.Seq.two_to_seq_to_two_LE",
"lemma_Vale.Def.Words.Two.nat_to_two_to_nat",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_nat64_def",
"token_correspondence_Vale.Def.Types_s.le_nat64_to_bytes_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"8feb1b45aefb595af101c0d8eaaf9a6d"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
1,
3,
3,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"b69c0cf813c1b5dbb37df07a9170e9e9"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
2,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "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",
"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",
"interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"9ca550e4b63f3c260ca4e4a6994c7401"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
1,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"da0ece2789fad2d6d84d87050f2a75a2"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_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_Vale.Def.Types_s.le_bytes_to_seq_quad32",
"function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
"interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.Def.Words.Seq.seq_to_seq_four_to_seq_LE",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6517d0c8716e159a40f752c583d756c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a65d20b338845083fa7a7ab8518b0f7b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Prims.pow2",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"15ea1509c8af42824f70880a180b0b55"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes",
1,
0,
0,
[
"@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"d9acc90bfcff1b27c5f020041a69f3c6"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat32",
"interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
],
0,
"29c4e9395f61403e05c6691d88a3f237"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"a5e8a39989c72681b24b8f44182ce9cc"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_8e8890e19356591ca1f9e83b434ba1ba",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"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",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"function_token_typing_Vale.Def.Words.Four_s.four_to_nat",
"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_init_len",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE",
"lemma_Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Lib.Seqs_s.seq_map"
],
0,
"a34a17969d1b53268baa5b6a517efa8f"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"b13f94710f1d127bde62e2495b0c2a58"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat",
"equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
"equation_Vale.Def.Words.Seq_s.seq_to_four_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",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32",
"function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"lemma_Vale.Def.Words.Seq.seq_four_to_seq_to_seq_four_LE",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"e73552c10d5dbee6b22457595b3f4ac7"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_of_singleton",
1,
0,
0,
[
"@query", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def"
],
0,
"38105e07035c74590e5b53febf69e37e"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_injective",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "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.Types_s.le_quad32_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_typing",
"interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43",
"lemma_FStar.UInt.pow2_values", "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_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE"
],
0,
"a839cbf6af4ae4f73cc85928925cd8d8"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_injective_specific",
1,
0,
0,
[ "@query" ],
0,
"b8c76d4c0c33ad88fd50a4b5ab817621"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_injective",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_typing",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"typing_FStar.Seq.Base.init", "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_four_to_seq_LE"
],
0,
"9c7ea89bb7076ece44fbb845cfa4f543"
],
[
"Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seqn",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"ada8fa98acd70a38bf4b883f6d82a2a9"
],
[
"Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Arch.Types_interpretation_Tm_arrow_f190567c0e1fa3ea695a387828243344",
"equation_Prims.nat", "equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"int_inversion",
"interpretation_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
"interpretation_Tm_abs_4d71202e4ba071eb1eb9023f14fa665d",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"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_create",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_96d5057c16747c54e40078129bdefb54",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Tm_abs_345accc9b683aa8ec5c7fabfbba2a524",
"typing_Vale.Def.Words.Seq_s.seq_to_four_LE"
],
0,
"8a818d01440fea2e66411d5ffca5e76f"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"f69e34a9d37b0c603726d057719c71ae"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_to_four_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",
"function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32",
"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",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca"
],
0,
"12000133b296241ebde1f3e56e7fc9c5"
],
[
"Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
1,
0,
0,
[ "@query" ],
0,
"4bd2406482b1770716ca5336778da665"
],
[
"Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"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_typing",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.create"
],
0,
"4dc6b514dc80cfa8135212be732110c2"
],
[
"Vale.Arch.Types.be_quad32_to_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seqn",
"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",
"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",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_029dc40463b676c106e396144db4f6f0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE"
],
0,
"96b3e729c211c339633b97b453b7a99f"
],
[
"Vale.Arch.Types.be_bytes_to_quad32_to_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.Types.be_quad32_to_bytes",
"equation_Vale.Def.Words.Seq_s.seq16",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_Vale.Arch.Types.be_quad32_to_bytes"
],
0,
"e2e8d759e89909c3ed38262baed7b477"
],
[
"Vale.Arch.Types.be_bytes_to_quad32_to_bytes",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat", "equation_Vale.Arch.Types.be_quad32_to_bytes",
"equation_Vale.Def.Types_s.be_bytes_to_quad32_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq16",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
"equation_Vale.Def.Words.Seq_s.seqn",
"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",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Vale.Def.Types_s.be_bytes_to_quad32",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
"lemma_Vale.Def.Words.Seq.seq_to_seq_four_to_seq_BE",
"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",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Vale.Def.Types_s.be_bytes_to_quad32_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Def.Words.Four_s.nat_to_four",
"typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Arch.Types.be_quad32_to_bytes",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
],
0,
"58ce9a3fc6b44da58185e2d89d5f9e66"
],
[
"Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Arch.Types.reverse_bytes_nat32_quad32",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Types_s.reverse_bytes_nat32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32",
"lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_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_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",
"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,
"1ab69b80a2b41b9b746998103bc84651"
],
[
"Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32_seq",
1,
0,
0,
[
"@query", "equation_Vale.Arch.Types.reverse_bytes_nat32_quad32_seq",
"lemma_Vale.Arch.Types.lemma_reverse_reverse_bytes_nat32_quad32"
],
0,
"bd2cc3371a089e811d7704de90052082"
],
[
"Vale.Arch.Types.lemma_reverse_reverse_bytes_quad32_seq",
1,
0,
0,
[
"@query", "equation_Vale.Arch.Types.reverse_bytes_quad32_seq",
"lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32"
],
0,
"947152317953db41f96ddd9c1be38050"
],
[
"Vale.Arch.Types.lemma_le_seq_quad32_to_bytes_length",
1,
0,
0,
[ "@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length" ],
0,
"1b2948a30f9eb75425d00c8dbcbe54d6"
],
[
"Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "kinding_Vale.Def.Words_s.four@tok",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_49d153dee59f77aa2974f04c57015388",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a9d54547d44b88f605af20f5c4cd19dc",
"typing_FStar.Seq.Base.length",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
],
0,
"f6d446555e67d0043eb81beac54f77eb"
],
[
"Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Arch.Types_interpretation_Tm_arrow_32c83d7dfb0acafa0853c18310eaef3e",
"equation_Prims.nat",
"function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"int_inversion", "int_typing",
"interpretation_Tm_abs_595fd624207608dd886b2e84a81a518b",
"interpretation_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.init_index_",
"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",
"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_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_21ef7f5ab4b8827eb094439f3acdea47",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_49d153dee59f77aa2974f04c57015388",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a8ed1c32215ef7054758d7b9026da0dd",
"refinement_interpretation_Tm_refine_a9d54547d44b88f605af20f5c4cd19dc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f0e12f26859fbf7671f3fb2fdbdad52a",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_c0ef6c6aba95253319fbfee7753c7c34",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
],
0,
"d53307a217d1a78a5ad8347f181ddfa7"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3234ac1d1198c8b724cbaa98bc293002",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee"
],
0,
"4cb72e0e71f7f809c70117c7f6c05d0a"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_Prims.nat",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_3234ac1d1198c8b724cbaa98bc293002",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
],
0,
"0e3a3d7cdf047e58a5a1d0cdb00edc51"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee"
],
0,
"2fc6b53c17f249b228691901b2e3d01c"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c064a9ee86fe2a45597a2563ec269cee",
"typing_FStar.Seq.Base.length"
],
0,
"694980b0c22448dd30518d468080c260"
],
[
"Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Def.Words_s.nat8",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"bb341a81ee6656b78f26b26f8e76a3f1"
],
[
"Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.pos",
"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",
"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",
"interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"aeeaacf48ef57cbf267e24288d4a2e7d"
],
[
"Vale.Arch.Types.append_distributes_le_seq_quad32_to_bytes",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"function_token_typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"int_typing", "lemma_FStar.UInt.pow2_values",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def"
],
0,
"720c77e04607a1f5df856ebd914b1d78"
]
]
]
Computing file changes ...
