let uint64 = uint_t U64 PUB
let uint64 =
uint_t U64 PUB
Vale.Wrapper.X64.Sha.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Vale.SHA.SHA_helpers.fsti.checked Vale.Arch.BufferFriend.fsti.checked Spec.SHA2.Constants.fst.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.BufferView.fsti.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Vale.Wrapper.X64.Sha.fsti
Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.PUB
module Vale.Wrapper.X64.Sha

open Vale.X64.CPU_Features_s
open FStar.HyperStack.ST
module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module BV = LowStar.BufferView
module HS = FStar.HyperStack
module BF = Vale.Arch.BufferFriend
open FStar.Mul
open Vale.SHA.SHA_helpers
open Lib.IntTypes

unfold
let uint32_p = B.buffer uint32
unfold
let uint32_i = IB.ibuffer uint32
unfold
let uint8_p = B.buffer uint8
val uint64 : Type0
Type0