Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.SHA.Simplify_Sha.fst.hints
[
"�%�k����ic�v�r4�",
[
[
"Vale.SHA.Simplify_Sha.same_seq_downview8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Vale.Interop.Views_interpretation_Tm_arrow_aba1678c8b9ac7aab440cb57b91a9c7e",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Interop.Views.down_view8",
"equation_Vale.Interop.Views.put8",
"equation_Vale.Interop.Views.put8_def",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"int_inversion", "int_typing",
"interpretation_Tm_abs_78da839197b471f0a62107e25a81f6b1",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Down.get_view_mk_buffer_view",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_get",
"proj_equation_LowStar.BufferView.Down.View_n",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Down.View_get",
"projection_inverse_LowStar.BufferView.Down.View_n",
"refinement_interpretation_Tm_refine_4dd13bedc0ec9248112ebfa660481343",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a3bfc685c48988243e45110ab3b0366a",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_LowStar.BufferView.Down.__proj__View__item__get",
"token_correspondence_Vale.Interop.Views.put8",
"token_correspondence_Vale.Interop.Views.put8_def",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.BufferView.Down.__proj__View__item__n",
"typing_LowStar.BufferView.Down.get_view",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Tm_abs_78da839197b471f0a62107e25a81f6b1",
"typing_Vale.Interop.Views.down_view8"
],
0,
"286868b5c6451ec0dae92bc8b8fb292e"
],
[
"Vale.SHA.Simplify_Sha.lemma_seq_nat8_le_seq_quad32_to_bytes_uint32",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Views.down_view8",
"equation_Vale.Interop.Views.up_view128",
"function_token_typing_FStar.UInt8.t",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Down.get_view_mk_buffer_view",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_n",
"proj_equation_LowStar.BufferView.Up.View_n",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_LowStar.BufferView.Down.View_n",
"projection_inverse_LowStar.BufferView.Up.View_n",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Vale.Interop.Types.down_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"8435eba9287b2d24a310947d6e04b564"
],
[
"Vale.SHA.Simplify_Sha.lemma_seq_nat8_le_seq_quad32_to_bytes_uint32",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Vale.SHA.Simplify_Sha_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f",
"Vale.SHA.Simplify_Sha_interpretation_Tm_arrow_c25dec9c72aa6b7bf5bd6f72fdcce3c3",
"Vale.SHA.Simplify_Sha_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
"Vale.SHA.Simplify_Sha_interpretation_Tm_arrow_f4c4992cf843ea442af1288d1d5d4d22",
"bool_inversion", "constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.BufferView.Down.as_buffer_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Def.Types_s.le_bytes_to_quad32",
"equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Four_s.four_select",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"equation_Vale.Interop.Views.down_view8",
"equation_Vale.Interop.Views.get128",
"equation_Vale.Interop.Views.get128_def",
"equation_Vale.Interop.Views.up_view128",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_FStar.UInt8.uint_to_t",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"interpretation_Tm_abs_4f03474956a6a2311e7d7bb19e902da5",
"interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"interpretation_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
"interpretation_Tm_abs_d324b025050975942eed8e4180033924",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt8.uv_inv",
"lemma_Lib.IntTypes.pow2_3",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"lemma_LowStar.BufferView.Down.get_view_mk_buffer_view",
"lemma_LowStar.BufferView.Up.as_buffer_mk_buffer",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"proj_equation_LowStar.BufferView.Down.View_n",
"proj_equation_LowStar.BufferView.Up.View_get",
"proj_equation_LowStar.BufferView.Up.View_n",
"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_LowStar.BufferView.Down.View_n",
"projection_inverse_LowStar.BufferView.Up.View_get",
"projection_inverse_LowStar.BufferView.Up.View_n",
"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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
"refinement_interpretation_Tm_refine_32a927c4be2ea7459bf10eff6091102f",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_3c856770b7b89a811b59ec4664452b5d",
"refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_553972523c0ad0511a59f7cdbdcafe94",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d4c04582d6eccfeb4e35b390a69520c",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"refinement_interpretation_Tm_refine_963efb8f77bcba49b31d59ffbced85c9",
"refinement_interpretation_Tm_refine_9e5e18b7456576682c6ab1bb3dc20cbb",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt8.uint_to_t",
"token_correspondence_FStar.UInt8.v",
"token_correspondence_LowStar.BufferView.Up.__proj__View__item__get",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Def.Opaque_s.make_opaque",
"token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
"token_correspondence_Vale.Def.Types_s.le_seq_quad32_to_bytes_def",
"token_correspondence_Vale.Def.Words.Four_s.four_to_nat",
"token_correspondence_Vale.Def.Words.Four_s.nat_to_four",
"token_correspondence_Vale.Interop.Views.get128",
"token_correspondence_Vale.Interop.Views.get128_def",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init",
"typing_FStar.Seq.Base.length",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.BufferView.Down.as_buffer",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
"typing_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
"typing_Tm_abs_b507efe3761ffdbbc33d0cf95f34a760",
"typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Interop.Types.down_view",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok"
],
0,
"d6fe53ef84dcd0bc2de36e4130f1d480"
]
]
]
Computing file changes ...
