Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Vale.Arch.Types.fsti.hints
[
"�?�}w\"��0>��u>3�",
[
[
"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,
"d9e4e3527a0f51767a74e9fb2cdc791d"
],
[
"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,
"8bbfc32a1406bf3db7f28f1e92f85ed8"
],
[
"Vale.Arch.Types.le_bytes_to_nat64_to_bytes",
1,
1,
0,
[ "@query" ],
0,
"f2ab14b8a932920c71a7ff51b0c6a116"
],
[
"Vale.Arch.Types.le_nat64_to_bytes_to_nat64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_8333610bdce3cc23e40345e003cba619"
],
0,
"5c359e79438c3c35e4d2fcda065c4da4"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_empty",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"f5df9b9ba1091458866e1dac328fe5ad"
],
[
"Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes_one_quad",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"72ad93d30431e876efd8cdef3d93f9b1"
],
[
"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,
"63bcbbbf629aea60a71902ba9ec87469"
],
[
"Vale.Arch.Types.le_seq_quad32_to_bytes_to_seq_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d5e9774270c731544d7c87dd4dd7c2a0"
],
0,
"ff4a52b9f6b031c4c16517dc96aeb674"
],
[
"Vale.Arch.Types.le_quad32_to_bytes_to_quad32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc"
],
0,
"2d26d44c3db21edac024f95c3e353452"
],
[
"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,
"391ff37e219f4f07b407a18c90238e56"
],
[
"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,
"92e0968ee2f2c81d3ba3d0f58e3ef8c3"
],
[
"Vale.Arch.Types.le_bytes_to_quad32_to_bytes",
1,
1,
0,
[ "@query" ],
0,
"980297263e28ab9ae63097c59e819f64"
],
[
"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,
"2fb65f86786f60d642fbde22960d0100"
],
[
"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,
"076a885fdded61dacd5011615f88846c"
],
[
"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,
"9139d2de91a5dd8aff05e2a99b6becfd"
],
[
"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,
"ce8ad45237af5b12f55ae380ece3c143"
],
[
"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,
"a1de01791105bc00dcae0694f2a90050"
],
[
"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,
"4d498c026e0b6cc7f44c83cb020efffd"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...