let vec_v_t (t:v_inttype{unsigned t}) (w:width) = lseq (uint_t t SEC) w
let vec_v_t (t: v_inttype{unsigned t}) (w: width) =
lseq (uint_t t SEC) w
Lib.IntVector.fsti.checked
Spec.AES.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Lib.IntVector.fsti
Lib.IntVector.v_inttype Prims.b2t Lib.IntTypes.unsigned Lib.IntVector.width Lib.Sequence.lseq Lib.IntTypes.uint_t Lib.IntTypes.SEC
module Lib.IntVector

open FStar.Mul
open Lib.Sequence
open Lib.IntTypes

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"

let v_inttype = t:inttype{unsigned t /\ ~(U1? t)}

let width = n:size_nat{n == 1 \/ n == 2 \/ n == 4 \/ n == 8 \/ n == 16 \/ n == 32}
val vec_v_t : t: Lib.IntVector.v_inttype{Lib.IntTypes.unsigned t} -> w: Lib.IntVector.width -> Type0
t: Lib.IntVector.v_inttype{Lib.IntTypes.unsigned t} -> w: Lib.IntVector.width -> Type0