JAR: Join-Accumulate Refine

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.fisherYatesShuffle.{u_1} {α : Type u_1} [Inhabited α]
  (s : Array α) (r : Array Nat) : Array α
Jar.Crypto.fisherYatesShuffle.{u_1}
  {α : Type u_1} [Inhabited α]
  (s : Array α) (r : Array Nat) : Array α

Fisher-Yates shuffle with numeric randomness source. GP Appendix F eq (F.1). F(s, r) : ⟦T⟧l × ⟦ℕ⟧{l:} → ⟦T⟧_l Selection variant: pick element at random index j from working copy, place it in output[i], fill gap at j with last remaining element.

🔗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