Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
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,
"ea6638230403ce7107b6552c88e76672"
],
[
"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,
"912609f6cfc7256d7651f73f17961fab"
],
[
"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,
"a0fd2d64092ab40e00316ba4090e4cff"
],
[
"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,
"79b8beee35d0af89e7ea0c7014b95572"
],
[
"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,
"138a75d713aa5189cb456e53f7b28440"
],
[
"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,
"299510f2eac4bc24394927a3901067df"
],
[
"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,
"7c89cc9ca4574d749d245b8513452dd3"
],
[
"Vale.Arch.Types.xor_lemmas",
1,
1,
0,
[ "@query" ],
0,
"bbe7e3f3fa6d3b4ec81ca5777a91d98f"
],
[
"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,
"0a0fc2220683f3c9ae4c930ba18b3f70"
],
[
"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,
"090baa92ce19fe5ddd5d8d2073ac1ff3"
],
[
"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,
"17c51c06d2e915edea6c8c2a317e86bd"
],
[
"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,
"72eeaf0efdfb64bca0107470bffff4d1"
],
[
"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,
"eea5f5c0ed60649ccc4d3d4a59870dfd"
],
[
"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,
"0bf09a0be2f0d988248a46d3371e3be3"
],
[
"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,
"0e692f4058c3c014c5b2bec114a22f46"
],
[
"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,
"caace0084b8d7fae23bfa06b8e45fafa"
],
[
"Vale.Arch.Types.lo64_reveal",
1,
1,
0,
[ "@query" ],
0,
"77e6fd88d0bb20576e68aac4a8dda126"
],
[
"Vale.Arch.Types.hi64_reveal",
1,
1,
0,
[ "@query" ],
0,
"05e7a5a06e9f1be31c112159ccbf5a01"
],
[
"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,
"5887d14333244a000e3feb121309f370"
],
[
"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,
"660554a66170e1250b5010e39f544ba6"
],
[
"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,
"f9acbbbc16f8655a56360f78291bd8d3"
],
[
"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,
"dd80d85ae075654d8a7a783a2e23778d"
],
[
"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,
"19a676e8e4403d3612e38ec1ccbebed0"
],
[
"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,
"52252bf09703b20fba53f4b983dba54f"
],
[
"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,
"2b60526ca67655cd1a5c60fdc0a17e0e"
],
[
"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,
"4fbe2e3b3223656318faed39b78f964a"
],
[
"Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
1,
3,
3,
[ "@query" ],
0,
"b76573f31fb16b272862e75ef71d360a"
],
[
"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,
"c0ea444ea8f2561f1f7444b216c1a62d"
],
[
"Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
1,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619"
],
0,
"54ee6b9f963573c916bfb87213f4a175"
],
[
"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,
"7e1fd3e6c4593f4d39ba2a6ea70d17fc"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
1,
3,
3,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"f2449de7970deb0b523fce83cd8c2048"
],
[
"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,
"5d03b58797cb6f0b538a910cb0df6f62"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
1,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"c533ba6f76956d2b5b00aae7f1359430"
],
[
"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,
"f531e1e35d267c55628b746735520ea4"
],
[
"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,
"abdf5a22b193ddc0e6f2e140b48b1ab4"
],
[
"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,
"d6913357083451803510a5f4adcf0c9e"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"e987efcd5fe96c8ca51cc9f1236b6474"
],
[
"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,
"c0fdaba7380c94be2a5e001c698f4ad6"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"a598ec40519762cf8f6e54a313053154"
],
[
"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,
"9ecb41de187271923d3f071f10868d2a"
],
[
"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,
"257a61f06e2414db15f11f1c392c2a6d"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_injective",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"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.Seq.Base.hasEq_lemma", "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,
"0bc0c61c76ea665e50f2da9fa806e2ef"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_injective_specific",
1,
0,
0,
[ "@query" ],
0,
"fc9b64b3237a527486c1308fe5d84cc8"
],
[
"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,
"14d813a51e78e75c521098cd556385b6"
],
[
"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,
"d7ae29fc76c5a82dc85aa48482937be1"
],
[
"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,
"99ea138091a6bb88be5952b54d27936f"
],
[
"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,
"6589c2dc40a5e3b987ad4142ed480ca5"
],
[
"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,
"91450608ada9b0fd01e670e9120c2a8d"
],
[
"Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
1,
0,
0,
[ "@query" ],
0,
"6f152570c1037d32f6a64be4e4e30330"
],
[
"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,
"4748f49a0a5ea1da6b9e2c87b7ea6392"
],
[
"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,
"48fde59b172cba20f57e8f22f9de42dc"
],
[
"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,
"1d9ba79abd6d522a3502393aad3e6f07"
],
[
"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,
"842a2013c056cfe9b5a6125e1f630895"
],
[
"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,
"205311c4e01b056d61bf5bf254eb04cc"
],
[
"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,
"a75c5b484bcb673bfe9ee2972a5bae21"
],
[
"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,
"4ca0d56aa8a64cd217d91ae63bc53835"
],
[
"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,
"eefb03786d3cbf594cca63d28b6beb29"
],
[
"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,
"974277a0a76282e7df90a34dd6debcba"
],
[
"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,
"ae1f7c3288aa47058cd1a4796f467a5a"
],
[
"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,
"592d8d9c9de2150816e4eba4b60ae4b8"
],
[
"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,
"19db585a182cede1cc721a6cf984cd8d"
],
[
"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,
"3d1b9b2b8a5bb6583ca896d00238af26"
],
[
"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,
"74d5826818a9dd12eca824f1314aaaee"
],
[
"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,
"fcfbd4246cd99d3f0a78b1a1ddbbbceb"
],
[
"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,
"dfec607fc17d73546e96e6071681e238"
],
[
"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,
"17f6254759e6dc6e70e27ef858d5439f"
]
]
]
Computing file changes ...
