gistfile1.idr

KeySize : Type
KeySize = Fin 256 -- should actually be [1-256], not [0-256]

public
ARC4Key : KeySize -> Type
ARC4Key n = Vect (finToNat n) (Mod 256) -- should be Byte, but can’t convert yet

public
data AllegedRivestCipher4 : KeySize -> Type where
  ARC4 : ARC4Key n -> AllegedRivestCipher4 n

KSA : ARC4Key n -> Vect 256 (Mod 256)
KSA {n=n} key =
  fst (nextJ 0 0 (map Prelude.Classes.fromInteger (fromList [0..255]))) where
    nextJ : Mod 256 -> Mod 256 -> Vect 256 (Mod 256)
            -> (Vect 256 (Mod 256), Mod 256)
    nextJ i j S = let newJ = the (Mod 256) (j + index (cast i) S + index (cast i `mod` n) key)
                  in (swap (cast i) (cast newJ) S, newJ)

-- ./Data/Crypto/Encryption/ARC4.idr:26:11:When elaborating right hand side of Data.Crypto.Encryption.ARC4.KSA, nextJ:
-- Can't resolve type class Cast (Mod (fromInteger 256)) (Fin (finToNat n))