
  0 | module Crypto.Random.C
  1 | 
  2 | import Crypto.Random
  3 | import System.FFI
  4 | import Data.Vect
  5 | import Utils.Misc
  6 | import Data.Buffer
  7 | import Data.List
  8 | import System.Info
  9 | 
 10 | %foreign "C:random_buf,libidristls"
 11 | prim_io__random_buf : Buffer -> Int -> PrimIO Int
 12 | 
 13 | public export
 14 | HasIO io => MonadRandom io where
 15 |   random_bytes Z = pure []
 16 |   random_bytes n = do
 17 |     let n' = cast n
 18 |     Just buf <- newBuffer n'
 19 |     | Nothing => assert_total $ idris_crash "somehow newBuffer failed"
 20 |     0 <- primIO $ prim_io__random_buf buf n'
 21 |     | _ => assert_total $ idris_crash "random_buf failed"
 22 |     traverse (getBits8 buf) (map (cast . finToNat) Fin.range)
 23 |