module Data.Crypto (generatekey, encrypt, decrypt) where import Prelude hiding (round) import Data.Word (Word8) import Data.Bits ((.&.)) generatekey :: Word -> Key generatekey :: Word -> Key generatekey Word w | Word w Word -> [Word] -> Bool forall a. Eq a => a -> [a] -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool `elem` [Word 0..Word 1023] = Word -> Key bin10 Word w | Bool otherwise = Word -> Key bin10 (Word w Word -> Word -> Word forall a. Integral a => a -> a -> a `mod` Word 1024) encrypt :: Key -> Word8 -> Word8 encrypt :: Key -> Word8 -> Word8 encrypt Key k Word8 w = let (Key sk1,Key sk2) = Key -> (Key, Key) keyschedule Key k pt :: Key pt = Word8 -> Key bin Word8 w ct :: Key ct = (IPinverse ipinverse IPinverse -> (Key -> (Key, Key)) -> Key -> Key forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> (Key, Key) -> (Key, Key) round Key sk2 ((Key, Key) -> (Key, Key)) -> (Key -> (Key, Key)) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . (Key, Key) -> (Key, Key) sw ((Key, Key) -> (Key, Key)) -> (Key -> (Key, Key)) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> (Key, Key) -> (Key, Key) round Key sk1 ((Key, Key) -> (Key, Key)) -> (Key -> (Key, Key)) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> (Key, Key) split (Key -> (Key, Key)) -> (Key -> Key) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> Key ip) Key pt in Key -> Word8 dec Key ct decrypt :: Key -> Word8 -> Word8 decrypt :: Key -> Word8 -> Word8 decrypt Key k Word8 w = let (Key sk1,Key sk2) = Key -> (Key, Key) keyschedule Key k ct :: Key ct = Word8 -> Key bin Word8 w pt :: Key pt = (IPinverse ipinverse IPinverse -> (Key -> (Key, Key)) -> Key -> Key forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> (Key, Key) -> (Key, Key) round Key sk1 ((Key, Key) -> (Key, Key)) -> (Key -> (Key, Key)) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . (Key, Key) -> (Key, Key) sw ((Key, Key) -> (Key, Key)) -> (Key -> (Key, Key)) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> (Key, Key) -> (Key, Key) round Key sk2 ((Key, Key) -> (Key, Key)) -> (Key -> (Key, Key)) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> (Key, Key) split (Key -> (Key, Key)) -> (Key -> Key) -> Key -> (Key, Key) forall b c a. (b -> c) -> (a -> b) -> a -> c . Key -> Key ip) Key ct in Key -> Word8 dec Key pt keyschedule :: Key -> (Subkey,Subkey) keyschedule :: Key -> (Key, Key) keyschedule Key k = let key' :: Subkey key' :: Key key' = Key -> Key p10 Key k s1,s2 :: Subkey (Key s1,Key s2) = Key -> (Key, Key) split Key key' s1',s2' :: Subkey s1' :: Key s1' = Key -> Key ls1 Key s1 s2' :: Key s2' = Key -> Key ls1 Key s2 sk1 :: Subkey sk1 :: Key sk1 = IPinverse p8 (Key s1',Key s2') s1'',s2'' :: Subkey s1'' :: Key s1'' = Key -> Key ls2 Key s1' s2'' :: Key s2'' = Key -> Key ls2 Key s2' sk2 :: Subkey sk2 :: Key sk2 = IPinverse p8 (Key s1'',Key s2'') in (Key sk1,Key sk2) round :: Subkey -> (Block,Block) -> (Block,Block) round :: Key -> (Key, Key) -> (Key, Key) round Key subkey (Key l,Key r) = let r' :: Block r' :: Key r' = Key -> Key expansion Key r r'' :: Block r'' :: Key r'' = Key r' Xor `xor8` Key subkey left,right :: Block (Key left,Key right) = Key -> (Key, Key) split Key r'' left',right' :: Block left' :: Key left' = Key -> Key sbox0 Key left right' :: Key right' = Key -> Key sbox1 Key right merged :: Block merged :: Key merged = IPinverse p4 (Key left',Key right') fk :: Block fk :: Key fk = Key merged Xor `xor4` Key l in (Key fk,Key r) data Bit = Zero | One deriving stock Int -> Bit -> ShowS [Bit] -> ShowS Bit -> String (Int -> Bit -> ShowS) -> (Bit -> String) -> ([Bit] -> ShowS) -> Show Bit forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: Int -> Bit -> ShowS showsPrec :: Int -> Bit -> ShowS $cshow :: Bit -> String show :: Bit -> String $cshowList :: [Bit] -> ShowS showList :: [Bit] -> ShowS Show data Block = B2 Bit Bit | B4 Bit Bit Bit Bit | B5 Bit Bit Bit Bit Bit | B8 Bit Bit Bit Bit Bit Bit Bit Bit | B10 Bit Bit Bit Bit Bit Bit Bit Bit Bit Bit deriving stock Int -> Key -> ShowS [Key] -> ShowS Key -> String (Int -> Key -> ShowS) -> (Key -> String) -> ([Key] -> ShowS) -> Show Key forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a $cshowsPrec :: Int -> Key -> ShowS showsPrec :: Int -> Key -> ShowS $cshow :: Key -> String show :: Key -> String $cshowList :: [Key] -> ShowS showList :: [Key] -> ShowS Show type Key = Block type Subkey = Block type Permutation = Block -> Block type Split = Block -> (Block,Block) type Rotation = Block -> Block type P4 = (Block,Block) -> Block type P8 = (Block,Block) -> Block type Xorbit = (Bit,Bit) -> Bit type Xor = Block -> Block -> Block type Substitution = Block -> Block type IPinverse = (Block,Block) -> Block type Mask = Word8 type Mask10 = Word type Switch = (Block,Block) -> (Block,Block) bin :: Word8 -> Block bin :: Word8 -> Key bin Word8 w = let b1,b2',b3,b4',b5',b6,b7,b8' :: Bit bits :: Mask -> Bit bits :: Word8 -> Bit bits Word8 m = if Word8 w Word8 -> Word8 -> Word8 forall a. Bits a => a -> a -> a .&. Word8 m Word8 -> Word8 -> Bool forall a. Eq a => a -> a -> Bool == Word8 m then Bit One else Bit Zero b8' :: Bit b8' = Word8 -> Bit bits Word8 0x01 b7 :: Bit b7 = Word8 -> Bit bits Word8 0x02 b6 :: Bit b6 = Word8 -> Bit bits Word8 0x04 b5' :: Bit b5' = Word8 -> Bit bits Word8 0x08 b4' :: Bit b4' = Word8 -> Bit bits Word8 0x10 b3 :: Bit b3 = Word8 -> Bit bits Word8 0x20 b2' :: Bit b2' = Word8 -> Bit bits Word8 0x40 b1 :: Bit b1 = Word8 -> Bit bits Word8 0x80 ret :: Key ret = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8' in Key ret bin10 :: Word -> Block bin10 :: Word -> Key bin10 Word w | Word w Word -> [Word] -> Bool forall a. Eq a => a -> [a] -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool `elem` [Word 0..Word 1023] = let b1,b2',b3,b4',b5',b6,b7,b8',b9,b10' :: Bit bits :: Mask10 -> Bit bits :: Word -> Bit bits Word m = if Word w Word -> Word -> Word forall a. Bits a => a -> a -> a .&. Word m Word -> Word -> Bool forall a. Eq a => a -> a -> Bool == Word m then Bit One else Bit Zero b10' :: Bit b10' = Word -> Bit bits Word 0x01 b9 :: Bit b9 = Word -> Bit bits Word 0x02 b8' :: Bit b8' = Word -> Bit bits Word 0x04 b7 :: Bit b7 = Word -> Bit bits Word 0x08 b6 :: Bit b6 = Word -> Bit bits Word 0x10 b5' :: Bit b5' = Word -> Bit bits Word 0x20 b4' :: Bit b4' = Word -> Bit bits Word 0x40 b3 :: Bit b3 = Word -> Bit bits Word 0x80 b2' :: Bit b2' = Word -> Bit bits Word 0x100 b1 :: Bit b1 = Word -> Bit bits Word 0x200 ret :: Key ret = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B10 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8' Bit b9 Bit b10' in Key ret bin10 Word _ = String -> Key forall a. HasCallStack => String -> a error String "Out of bounds" dec :: Block -> Word8 dec :: Key -> Word8 dec (B8 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8') = let bits :: Bit -> Mask -> Word8 bits :: Bit -> Word8 -> Word8 bits Bit Zero Word8 _ = Word8 0 bits Bit One Word8 m = Word8 m in Bit -> Word8 -> Word8 bits Bit b8' Word8 0x01 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b7 Word8 0x02 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b6 Word8 0x04 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b5' Word8 0x08 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b4' Word8 0x10 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b3 Word8 0x20 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b2' Word8 0x40 Word8 -> Word8 -> Word8 forall a. Num a => a -> a -> a + Bit -> Word8 -> Word8 bits Bit b1 Word8 0x80 dec Key _ = Word8 forall a. HasCallStack => a undefined dec10 :: Block -> Word dec10 :: Key -> Word dec10 (B10 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8' Bit b9 Bit b10') = let bits :: Bit -> Mask10 -> Word bits :: Bit -> Word -> Word bits Bit Zero Word _ = Word 0 bits Bit One Word m = Word m in Bit -> Word -> Word bits Bit b10' Word 0x01 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b9 Word 0x02 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b8' Word 0x04 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b7 Word 0x08 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b6 Word 0x10 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b5' Word 0x20 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b4' Word 0x40 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b3 Word 0x80 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b2' Word 0x100 Word -> Word -> Word forall a. Num a => a -> a -> a + Bit -> Word -> Word bits Bit b1 Word 0x200 dec10 Key _ = Word forall a. HasCallStack => a undefined bit :: Int -> Bit bit :: Int -> Bit bit Int 0 = Bit Zero bit Int _ = Bit One dig :: Bit -> Int dig :: Bit -> Int dig Bit Zero = Int 0 dig Bit One = Int 1 b2,b4,b5,b8,b10 :: Block b2 :: Key b2 = Bit -> Bit -> Key B2 Bit Zero Bit Zero b4 :: Key b4 = Bit -> Bit -> Bit -> Bit -> Key B4 Bit Zero Bit Zero Bit Zero Bit Zero b5 :: Key b5 = Bit -> Bit -> Bit -> Bit -> Bit -> Key B5 Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero b8 :: Key b8 = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero b10 :: Key b10 = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B10 Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero Bit Zero p10 :: Permutation p10 :: Key -> Key p10 (B10 Bit k1 Bit k2 Bit k3 Bit k4 Bit k5 Bit k6 Bit k7 Bit k8 Bit k9 Bit k10) = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B10 Bit k3 Bit k5 Bit k2 Bit k7 Bit k4 Bit k10 Bit k1 Bit k9 Bit k8 Bit k6 p10 Key _ = Key forall a. HasCallStack => a undefined split :: Split split :: Key -> (Key, Key) split (B10 Bit k1 Bit k2 Bit k3 Bit k4 Bit k5 Bit k6 Bit k7 Bit k8 Bit k9 Bit k10) = (Key block1,Key block2) where block1,block2 :: Block block1 :: Key block1 = Bit -> Bit -> Bit -> Bit -> Bit -> Key B5 Bit k1 Bit k2 Bit k3 Bit k4 Bit k5 block2 :: Key block2 = Bit -> Bit -> Bit -> Bit -> Bit -> Key B5 Bit k6 Bit k7 Bit k8 Bit k9 Bit k10 split (B8 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8') = (Key block1,Key block2) where block1,block2 :: Block block1 :: Key block1 = Bit -> Bit -> Bit -> Bit -> Key B4 Bit b1 Bit b2' Bit b3 Bit b4' block2 :: Key block2 = Bit -> Bit -> Bit -> Bit -> Key B4 Bit b5' Bit b6 Bit b7 Bit b8' split Key _ = (Key, Key) forall a. HasCallStack => a undefined sw :: Switch sw :: (Key, Key) -> (Key, Key) sw (Key b1,Key b2') = (Key b2',Key b1) ls1,ls2 :: Rotation ls1 :: Key -> Key ls1 (B5 Bit k1 Bit k2 Bit k3 Bit k4 Bit k5) = Bit -> Bit -> Bit -> Bit -> Bit -> Key B5 Bit k2 Bit k3 Bit k4 Bit k5 Bit k1 ls1 Key _ = Key forall a. HasCallStack => a undefined ls2 :: Key -> Key ls2 (B5 Bit k1 Bit k2 Bit k3 Bit k4 Bit k5) = Bit -> Bit -> Bit -> Bit -> Bit -> Key B5 Bit k3 Bit k4 Bit k5 Bit k1 Bit k2 ls2 Key _ = Key forall a. HasCallStack => a undefined p8 :: P8 p8 :: IPinverse p8 (B5 Bit _ Bit _ Bit k3 Bit k4 Bit k5,B5 Bit k6 Bit k7 Bit k8 Bit k9 Bit k10) = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit k6 Bit k3 Bit k7 Bit k4 Bit k8 Bit k5 Bit k10 Bit k9 p8 (Key, Key) _ = Key forall a. HasCallStack => a undefined ip :: Permutation ip :: Key -> Key ip (B8 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8') = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit b2' Bit b6 Bit b3 Bit b1 Bit b4' Bit b8' Bit b5' Bit b7 ip Key _ = Key forall a. HasCallStack => a undefined ipinverse :: IPinverse ipinverse :: IPinverse ipinverse (B4 Bit b1 Bit b2' Bit b3 Bit b4',B4 Bit b5' Bit b6 Bit b7 Bit b8') = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit b4' Bit b1 Bit b3 Bit b5' Bit b7 Bit b2' Bit b8' Bit b6 ipinverse (Key, Key) _ = Key forall a. HasCallStack => a undefined xor :: Xorbit xor :: Xorbit xor (Bit Zero,Bit Zero) = Bit Zero xor (Bit Zero,Bit One) = Bit One xor (Bit One,Bit Zero) = Bit One xor (Bit One,Bit One) = Bit Zero xor4 :: Xor xor4 :: Xor xor4 (B4 Bit b1 Bit b2' Bit b3 Bit b4') (B4 Bit k1 Bit k2 Bit k3 Bit k4) = Bit -> Bit -> Bit -> Bit -> Key B4 Bit o1 Bit o2 Bit o3 Bit o4 where o1,o2,o3,o4 :: Bit o1 :: Bit o1 = Xorbit xor (Bit b1,Bit k1) o2 :: Bit o2 = Xorbit xor (Bit b2',Bit k2) o3 :: Bit o3 = Xorbit xor (Bit b3,Bit k3) o4 :: Bit o4 = Xorbit xor (Bit b4',Bit k4) xor4 Key _ Key _ = Key forall a. HasCallStack => a undefined xor8 :: Xor xor8 :: Xor xor8 (B8 Bit b1 Bit b2' Bit b3 Bit b4' Bit b5' Bit b6 Bit b7 Bit b8') (B8 Bit k1 Bit k2 Bit k3 Bit k4 Bit k5 Bit k6 Bit k7 Bit k8) = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit o1 Bit o2 Bit o3 Bit o4 Bit o5 Bit o6 Bit o7 Bit o8 where o1,o2,o3,o4,o5,o6,o7,o8 :: Bit o1 :: Bit o1 = Xorbit xor (Bit b1,Bit k1) o2 :: Bit o2 = Xorbit xor (Bit b2',Bit k2) o3 :: Bit o3 = Xorbit xor (Bit b3,Bit k3) o4 :: Bit o4 = Xorbit xor (Bit b4',Bit k4) o5 :: Bit o5 = Xorbit xor (Bit b5',Bit k5) o6 :: Bit o6 = Xorbit xor (Bit b6,Bit k6) o7 :: Bit o7 = Xorbit xor (Bit b7,Bit k7) o8 :: Bit o8 = Xorbit xor (Bit b8',Bit k8) xor8 Key _ Key _ = Key forall a. HasCallStack => a undefined sbox0,sbox1 :: Substitution sbox0 :: Key -> Key sbox0 (B4 Bit b1 Bit b2' Bit b3 Bit b4') = let row :: [Int] row :: [Int] row = case (Bit -> Int dig Bit b1,Bit -> Int dig Bit b4') of (Int 0,Int 0) -> [Int 1,Int 0,Int 3,Int 2] (Int 0,Int 1) -> [Int 3,Int 2,Int 1,Int 0] (Int 1,Int 0) -> [Int 0,Int 2,Int 1,Int 3] (Int 1,Int 1) -> [Int 3,Int 1,Int 3,Int 2] (Int, Int) _ -> [Int] forall a. HasCallStack => a undefined col :: Int col :: Int col = case (Bit -> Int dig Bit b2',Bit -> Int dig Bit b3) of (Int 0,Int 0) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 0 (Int 0,Int 1) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 1 (Int 1,Int 0) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 2 (Int 1,Int 1) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 3 (Int, Int) _ -> Int forall a. HasCallStack => a undefined ret :: Block ret :: Key ret = case Int col of Int 0 -> Bit -> Bit -> Key B2 Bit Zero Bit Zero Int 1 -> Bit -> Bit -> Key B2 Bit Zero Bit One Int 2 -> Bit -> Bit -> Key B2 Bit One Bit Zero Int 3 -> Bit -> Bit -> Key B2 Bit One Bit One Int _ -> Key forall a. HasCallStack => a undefined in Key ret sbox0 Key _ = Key forall a. HasCallStack => a undefined sbox1 :: Key -> Key sbox1 (B4 Bit b1 Bit b2' Bit b3 Bit b4') = let row :: [Int] row :: [Int] row = case (Bit -> Int dig Bit b1,Bit -> Int dig Bit b4') of (Int 0,Int 0) -> [Int 0,Int 1,Int 2,Int 3] (Int 0,Int 1) -> [Int 2,Int 0,Int 1,Int 3] (Int 1,Int 0) -> [Int 3,Int 0,Int 1,Int 0] (Int 1,Int 1) -> [Int 2,Int 1,Int 0,Int 3] (Int, Int) _ -> [Int] forall a. HasCallStack => a undefined col :: Int col :: Int col = case (Bit -> Int dig Bit b2',Bit -> Int dig Bit b3) of (Int 0,Int 0) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 0 (Int 0,Int 1) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 1 (Int 1,Int 0) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 2 (Int 1,Int 1) -> [Int] row [Int] -> Int -> Int forall a. HasCallStack => [a] -> Int -> a !! Int 3 (Int, Int) _ -> Int forall a. HasCallStack => a undefined ret :: Block ret :: Key ret = case Int col of Int 0 -> Bit -> Bit -> Key B2 Bit Zero Bit Zero Int 1 -> Bit -> Bit -> Key B2 Bit Zero Bit One Int 2 -> Bit -> Bit -> Key B2 Bit One Bit Zero Int 3 -> Bit -> Bit -> Key B2 Bit One Bit One Int _ -> Key forall a. HasCallStack => a undefined in Key ret sbox1 Key _ = Key forall a. HasCallStack => a undefined expansion :: Permutation expansion :: Key -> Key expansion (B4 Bit b1 Bit b2' Bit b3 Bit b4') = Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Bit -> Key B8 Bit b4' Bit b1 Bit b2' Bit b3 Bit b2' Bit b3 Bit b4' Bit b1 expansion Key _ = Key forall a. HasCallStack => a undefined p4 :: P4 p4 :: IPinverse p4 (B2 Bit b1 Bit b2',B2 Bit b3 Bit b4') = Bit -> Bit -> Bit -> Bit -> Key B4 Bit b2' Bit b4' Bit b3 Bit b1 p4 (Key, Key) _ = Key forall a. HasCallStack => a undefined