module RandomTest

import Crypto.Random
import Crypto.Random.C
import Data.Vect
import Data.Fin
import Control.Monad.Error.Either

%default partial

b8_to_fin : Bits8 -> Fin 256
b8_to_fin b = case natToFin (cast b) 256 of Just x => x

incr : Vect 256 Bits32 -> Bits8 -> Vect 256 Bits32
incr vect byte = updateAt (b8_to_fin byte) (+1) vect

mean : (Cast a Double, Num a) => {n : Nat} -> Vect n a -> Double
mean vect = (sum $ map cast vect) / (cast n)

export
test_random : EitherT String IO ()
test_random = do
  let random_bytes_size = 262144.0
  data' <- random_bytes (cast random_bytes_size)
  let distribution = foldl incr (replicate _ 0) data'
  let delta_mean = abs (mean data' - 128)
  let True = delta_mean < 2
  | False => throwE "random generated bytes mean deviates too far from 128: \{show delta_mean}"

  let expected_mean = random_bytes_size / 256.0
  let delta_distri_mean = abs (mean distribution - expected_mean)
  let True = delta_distri_mean < 1.5
  | False => throwE "random generated bytes distribution mean deviates too far from \{show expected_mean}: \{show delta_mean}"

  pure ()
