let uint64 = UInt64.t
let uint64 =
UInt64.t
Vale.Wrapper.X64.GCTR.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Interop.Base.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.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 FStar.Ghost.fsti.checked
Vale.Wrapper.X64.GCTR.fsti
FStar.UInt64.t
module Vale.Wrapper.X64.GCTR

open Vale.X64.CPU_Features_s
open FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.AES.AES_s
open Vale.AES.GCTR
open Vale.AES.GCTR_s
open Vale.Interop.Base
open Vale.Def.Types_s

unfold
val uint64 : Prims.eqtype
Prims.eqtype