
  0 | module Crypto.Random
  1 | 
  2 | import Control.Monad.Error.Either
  3 | import Control.Monad.State
  4 | import Crypto.ChaCha
  5 | import Data.Bits
  6 | import Data.Fin
  7 | import Data.List
  8 | import Data.Nat
  9 | import Data.Stream
 10 | import Data.Vect
 11 | import Utils.Bytes
 12 | import Utils.Misc
 13 | 
 14 | public export
 15 | interface DRG (0 a : Type) where
 16 |   next_bytes : (n : Nat) -> a -> (a, Vect n Bits8)
 17 | 
 18 | public export
 19 | interface Monad m => MonadRandom (0 m : Type -> Type) where
 20 |   random_bytes : (n : Nat) -> m (Vect n Bits8)
 21 | 
 22 | public export
 23 | {s : _} -> DRG s => MonadRandom (State s) where
 24 |   random_bytes n = state (next_bytes n)
 25 | 
 26 | public export
 27 | next_integer : MonadRandom m => Nat -> m Integer
 28 | next_integer bytes = do
 29 |   randoms <- random_bytes bytes
 30 |   pure $ foldr (\(i,x),a => (shiftL {a=Integer} x i) .|. a) 0 $ zip ((*8) <$> [0..bytes]) (cast <$> toList randoms)
 31 | 
 32 | bytes_needed : Integer -> Nat
 33 | bytes_needed = (`div` 8) . cast . go 0
 34 |   where
 35 |     go : Nat -> Integer -> Nat
 36 |     go x n = if (n .&. ((bit x) - 1)) == n then x else go (x+8) n
 37 | 
 38 | random_num_uniform : MonadRandom m => Nat -> Integer -> m Integer
 39 | random_num_uniform bytes min = next_integer bytes >>= (\r => if r >= min then pure r else random_num_uniform bytes min)
 40 | 
 41 | public export
 42 | uniform_random : MonadRandom m => Integer -> m Integer
 43 | uniform_random {m} upper_bound =
 44 |   if upper_bound < 0 then negate <$> (uniform_random {m=m} $ abs upper_bound)
 45 |     else if upper_bound < 2 then pure 0
 46 |       else
 47 |         let bytes = bytes_needed upper_bound
 48 |         in (`mod` upper_bound) <$> random_num_uniform bytes ((bit bytes) `mod` upper_bound)
 49 | 
 50 | public export
 51 | uniform_random' : MonadRandom m => Integer -> Integer -> m Integer
 52 | uniform_random' {m} lower_bound upper_bound = do
 53 |   r <- uniform_random (upper_bound - lower_bound)
 54 |   pure (r + lower_bound)
 55 | 
 56 | public export
 57 | data ChaCha12DRG : Type where
 58 |   MkChaCha12DRG : (key : Vect 8 Bits32) -> ChaCha12DRG
 59 | 
 60 | public export
 61 | new_chacha12_drg : MonadRandom m => m ChaCha12DRG
 62 | new_chacha12_drg {m} = (\r => MkChaCha12DRG (from_le <$> group 8 4 r)) <$> (random_bytes {m=m} 32)
 63 | 
 64 | chacha12_stream : Vect 8 Bits32 -> Stream Bits8
 65 | chacha12_stream key = stream_concat $ map go nats
 66 |   where
 67 |     go : Nat -> List Bits8
 68 |     go iv = toList $ chacha_rfc8439_block 6 (cast iv) key (map (cast . finToNat) range)
 69 | 
 70 | public export
 71 | DRG ChaCha12DRG where
 72 |   next_bytes Z state = (state, [])
 73 |   next_bytes bytes (MkChaCha12DRG key) =
 74 |     let stream = chacha12_stream key
 75 |         key = map (from_le {n=4}) $ group 8 4 $ take 32 stream
 76 |         stream = drop 32 stream
 77 |     in (MkChaCha12DRG key, take bytes stream)
 78 |