Idris2Doc : Crypto.AES.Common

Crypto.AES.Common

(source)
Definitions
matmul : Num a => (Vect m a -> Vect m b -> c) -> Vect n (Vect m a) -> Vect m (Vect p b) -> Vect n (Vect p c)
  Visibility: export
vecxor : Bits a => Vect n a -> Vect n a -> Vect n a
  Visibility: export
matxor : Bits a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
  Visibility: export
sbox : ConstantTable 256 Bits8
  Visibility: export
inv_sbox : ConstantTable 256 Bits8
  Visibility: export
sub_byte : Bits8 -> Bits8
  Visibility: export
inv_sub_byte : Bits8 -> Bits8
  Visibility: export
sub_word : Vect m Bits8 -> Vect m Bits8
  Visibility: export
inv_sub_word : Vect m Bits8 -> Vect m Bits8
  Visibility: export
sub_bytes : Vect n (Vect m Bits8) -> Vect n (Vect m Bits8)
  Visibility: export
inv_sub_bytes : Vect n (Vect m Bits8) -> Vect n (Vect m Bits8)
  Visibility: export
rot_word : Nat -> Vect (S n) a -> Vect (S n) a
  Visibility: export
inv_rot_word : Nat -> Vect (S n) a -> Vect (S n) a
  Visibility: export
rcons : Stream Bits8
  Visibility: export
expand_key' : {auto 0 _ : NonZero n_b} -> Fin n_k -> Stream Bits8 -> Vect n_k (Vect n_b Bits8) -> Stream (Vect n_b Bits8)
  Visibility: export
expand_key : {auto 0 _ : NonZero n_b} -> {auto 0 _ : NonZero n_k} -> Vect n_k (Vect n_b Bits8) -> Stream (Vect n_b Bits8)
  Visibility: export
data Mode : Type
  Totality: total
  Visibility: public export
  Constructors:
  
AES128 : Mode
  
AES192 : Mode
  
AES256 : Mode
get_n_k : Mode -> Nat
  Visibility: public export
n_k_never_Z : (mode : Mode) -> NonZero (get_n_k mode)
  Visibility: public export
get_main_rounds : Mode -> Nat
  Visibility: public export