Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
EverCrypt.Hash.fsti.hints
[
"�wB\"�\u001c� \u001e�H���2�",
[
[
"EverCrypt.Hash.broken_alg",
1,
0,
0,
[ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
0,
"b7eea65bb81fd4bb17a8122445daac13"
],
[
"EverCrypt.Hash.alg13",
1,
0,
0,
[ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
0,
"f691e6bf8f0cd72ba1cff57555def793"
],
[
"EverCrypt.Hash.uint32_fits_maxLength",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Tm_unit",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.pos",
"equation_Spec.Hash.Definitions.max_input_length", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v",
"typing_Spec.Hash.Definitions.max_input_length"
],
0,
"0abb449ac2909d487b3b0115db7f40e8"
],
[
"EverCrypt.Hash.loc_includes_union_l_footprint_s",
1,
0,
0,
[ "@query" ],
0,
"76e36fb280331fdc5b005fdf27a03b82"
],
[
"EverCrypt.Hash.invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.state",
"equation_LowStar.Buffer.pointer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
],
0,
"9f8b6ad54c7a59da3358697e112b0c45"
],
[
"EverCrypt.Hash.frame_invariant_implies_footprint_preservation",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"equation_EverCrypt.Hash.footprint",
"equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.state",
"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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.state_s",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Set.singleton",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer"
],
0,
"2e60a156b4c9828d1e60f5f5ccc4e79a"
],
[
"EverCrypt.Hash.update",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8",
"equation_LowStar.Buffer.buffer",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"refinement_interpretation_Tm_refine_ee5e5ea36a8ac8879a333964d971b753",
"typing_LowStar.Buffer.trivial_preorder"
],
0,
"1ab9edba66d85ca229bb2542b402c4d3"
],
[
"EverCrypt.Hash.update_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83e1a0ed8e967940f825c40ec86a30c4",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"249ed23565260ffb8b7d0c664749c576"
],
[
"EverCrypt.Hash.update_last",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_EverCrypt.Helpers.uint64_t", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.uint8",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.bytes",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ca524e8b1a445d963e32596f1b3827cf",
"refinement_interpretation_Tm_refine_cb6956610e36c497712e91628f3f016e",
"refinement_interpretation_Tm_refine_ce8961826e5e909d22aad978d7822e9d",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.length"
],
0,
"6e10b66dafaf98a1403d6a6a12e4e429"
],
[
"EverCrypt.Hash.finish",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@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_Lib.IntTypes.unsigned",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip"
],
0,
"e8f403a6e666d89ed9d46ab3fbd172f7"
],
[
"EverCrypt.Hash.hash",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"refinement_interpretation_Tm_refine_117a03ca3213deec9a5d7dc6b56bb4c1",
"refinement_interpretation_Tm_refine_11f5c63c78caccafb41a6490396f36ec",
"refinement_interpretation_Tm_refine_70a01283c9094ee10f0f0fa4ff6403d7",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.frameOf"
],
0,
"652e044a6f9e4d1fd039b6490e22db6e"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...