Collection of BitVec

Stream: Is there code for X?

[Ashley Blacquiere]

Is there any notion anywhere of a collection of BitVec that I could sample from for some basic cryptographic formalizations? I _want_ something like the following, with an appropriate replacement forBitVec ℕ:

structure otp (K M C : Type) where
  key : K
  enc : K × M → C
  dec : K × C → M

def otp.keygen (n : ℕ) : otp (BitVec ℕ) (BitVec ℕ) (BitVec ℕ) :=
  { key := BitVec n, enc := key ^^^ BitVec n, dec := key ^^^ BitVec n }

[Kim Morrison]

What is BitVec ℕ supposed to mean here? It takes a natural number, not a type.

Perhaps you could explain informally what you want?

[Ashley Blacquiere]

Ya, sorry, that wasn't clear. I want a type of BitVecs that contains all BitVecs of the specified width. More accurately, I need a way to sample a single uniformly distributed BitVec of a specified width from the collection of all possible BitVecs of that width.