5.7. Utility🔗

def

Jar.Crypto.seqFromHash (l : Nat) (h : Hash) : Array Nat
Jar.Crypto.seqFromHash (l : Nat)
  (h : Hash) : Array Nat

Numeric-sequence-from-hash. GP Appendix F eq (F.2). seqFromHash(l, h) : ℍ → ⟦ℕ_{2^32}⟧_l Generates l pseudorandom 32-bit naturals from hash h using Blake2b.

def

Jar.Crypto.shuffle.{u_1} {α : Type u_1} [Inhabited α] (s : Array α)
  (h : Hash) : Array α
Jar.Crypto.shuffle.{u_1} {α : Type u_1}
  [Inhabited α] (s : Array α) (h : Hash) :
  Array α

Fisher-Yates shuffle with hash entropy. GP Appendix F eq (F.3). F(s, h) : ⟦T⟧_l × ℍ → ⟦T⟧_l