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.fsti.hints
[
";��\u0015��V\u000f�} ����\u000f",
[
[
"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,
"6047cea221b106e5c2867c7976231d3f"
],
[
"Vale.Arch.Types.lo64_reveal",
1,
1,
0,
[ "@query" ],
0,
"6f7102c799cb7ac452d970a9f770838f"
],
[
"Vale.Arch.Types.hi64_reveal",
1,
1,
0,
[ "@query" ],
0,
"3a5bf994e2a7994814cdd66f63583499"
],
[
"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,
"aa1be585804629813a9fd5ecab923ee6"
],
[
"Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
1,
1,
0,
[ "@query" ],
0,
"14e7c06e5df6cf05003a530c105e7fce"
],
[
"Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619"
],
0,
"ed9ccf4e2fc04b500c56c16236e8df73"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"f77c9f7e3ebcc9d672c9c0a3a5ef29ea"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"f9e7e3e95b3687e45b2fb24d2f731111"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes",
1,
1,
0,
[
"@query", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0"
],
0,
"32d43ff2597f0885fc7e9804c4635442"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"50b86162ff10bbda4c169b36ee22d652"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"2261aa1f57a90fc08ce5fdfa235af2ef"
],
[
"Vale.Arch.Types.seq_to_four_LE_is_seq_to_seq_four_LE",
1,
1,
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,
"a92851ab2eb4175fad5a93d1edb42593"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad_of_singleton",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"4cb5592fe07d545cf70554297ee37dde"
],
[
"Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
1,
1,
0,
[ "@query" ],
0,
"9d19c67678de2171c0e2655b704dba77"
],
[
"Vale.Arch.Types.be_quad32_to_bytes",
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.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,
"2558768d1cc5b1c5e925a75819425f2f"
],
[
"Vale.Arch.Types.be_bytes_to_quad32_to_bytes",
1,
1,
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,
"a6da345ad414729db1fa0c918ffbe43c"
],
[
"Vale.Arch.Types.slice_commutes_seq_four_to_seq_LE",
1,
1,
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,
"bba29f2825cdb35f2b8baccf6fa27f2f"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes",
1,
1,
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,
"195e3b85bd55048530ddc88a14b3f414"
],
[
"Vale.Arch.Types.slice_commutes_le_seq_quad32_to_bytes0",
1,
1,
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,
"453feb653df93c87a8953dcba2f77de7"
],
[
"Vale.Arch.Types.append_distributes_le_bytes_to_seq_quad32",
1,
1,
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,
"189ffd17420a12a3ed608bfa84701cff"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...