Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Vale.SHA.Simplify_Sha.fsti.hints
[
"ο�H�];�3ō�\u000e��o",
[
[
"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",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"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,
"8be4118c476beeba138f29e69802b126"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...