{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE TypeApplications #-}
#if MIN_VERSION_base(4,19,0)
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns -Wno-x-partial #-}
#else
{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}
#endif
module Documentation.SBV.Examples.Crypto.AES where
import Control.Monad (void, when)
import Data.SBV
import Data.SBV.Tools.CodeGen
import Data.SBV.Tools.Polynomial
import Data.List (transpose)
import Data.Maybe (fromJust)
import Data.Proxy
import Numeric (showHex)
import Test.QuickCheck hiding (verbose)
type GF28 = SWord 8
gf28Mult :: GF28 -> GF28 -> GF28
gf28Mult :: GF28 -> GF28 -> GF28
gf28Mult GF28
x GF28
y = (GF28, GF28, [Int]) -> GF28
forall a. Polynomial a => (a, a, [Int]) -> a
pMult (GF28
x, GF28
y, [Int
8, Int
4, Int
3, Int
1, Int
0])
gf28Pow :: GF28 -> Int -> GF28
gf28Pow :: GF28 -> Int -> GF28
gf28Pow GF28
n = Int -> GF28
forall {t}. (Integral t, Bits t) => t -> GF28
pow
where sq :: GF28 -> GF28
sq GF28
x = GF28
x GF28 -> GF28 -> GF28
`gf28Mult` GF28
x
pow :: t -> GF28
pow t
0 = GF28
1
pow t
i
| t -> Bool
forall a. Integral a => a -> Bool
odd t
i = GF28
n GF28 -> GF28 -> GF28
`gf28Mult` GF28 -> GF28
sq (t -> GF28
pow (t
i t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1))
| Bool
True = GF28 -> GF28
sq (t -> GF28
pow (t
i t -> Int -> t
forall a. Bits a => a -> Int -> a
`shiftR` Int
1))
gf28Inverse :: GF28 -> GF28
gf28Inverse :: GF28 -> GF28
gf28Inverse GF28
x = GF28
x GF28 -> Int -> GF28
`gf28Pow` Int
254
type State = [SWord 32]
type Key = [SWord 32]
type KS = (Key, [Key], Key)
rotR :: [GF28] -> Int -> [GF28]
rotR :: [GF28] -> Int -> [GF28]
rotR [GF28
a, GF28
b, GF28
c, GF28
d] Int
1 = [GF28
d, GF28
a, GF28
b, GF28
c]
rotR [GF28
a, GF28
b, GF28
c, GF28
d] Int
2 = [GF28
c, GF28
d, GF28
a, GF28
b]
rotR [GF28
a, GF28
b, GF28
c, GF28
d] Int
3 = [GF28
b, GF28
c, GF28
d, GF28
a]
rotR [GF28]
xs Int
i = [Char] -> [GF28]
forall a. HasCallStack => [Char] -> a
error ([Char] -> [GF28]) -> [Char] -> [GF28]
forall a b. (a -> b) -> a -> b
$ [Char]
"rotR: Unexpected input: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([GF28], Int) -> [Char]
forall a. Show a => a -> [Char]
show ([GF28]
xs, Int
i)
roundConstants :: [GF28]
roundConstants :: [GF28]
roundConstants = GF28
0 GF28 -> [GF28] -> [GF28]
forall a. a -> [a] -> [a]
: [ GF28 -> Int -> GF28
gf28Pow GF28
2 (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) | Int
k <- [Int
1 .. ] ]
invMixColumns :: State -> State
invMixColumns :: [SWord 32] -> [SWord 32]
invMixColumns [SWord 32]
state = ([GF28] -> SWord 32) -> [[GF28]] -> [SWord 32]
forall a b. (a -> b) -> [a] -> [b]
map [GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes ([[GF28]] -> [SWord 32]) -> [[GF28]] -> [SWord 32]
forall a b. (a -> b) -> a -> b
$ [[GF28]] -> [[GF28]]
forall a. [[a]] -> [[a]]
transpose ([[GF28]] -> [[GF28]]) -> [[GF28]] -> [[GF28]]
forall a b. (a -> b) -> a -> b
$ [[GF28]] -> [[GF28]]
mmult ((SWord 32 -> [GF28]) -> [SWord 32] -> [[GF28]]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes [SWord 32]
state)
where dot :: [b -> c] -> [b] -> c
dot [b -> c]
f = (c -> c -> c) -> [c] -> c
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 c -> c -> c
forall a. Bits a => a -> a -> a
xor ([c] -> c) -> ([b] -> [c]) -> [b] -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b -> c) -> b -> c) -> [b -> c] -> [b] -> [c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (b -> c) -> b -> c
forall a b. (a -> b) -> a -> b
($) [b -> c]
f
mmult :: [[GF28]] -> [[GF28]]
mmult [[GF28]]
n = [([GF28] -> GF28) -> [[GF28]] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map ([GF28 -> GF28] -> [GF28] -> GF28
forall {c} {b}. Bits c => [b -> c] -> [b] -> c
dot [GF28 -> GF28]
r) [[GF28]]
n | [GF28 -> GF28]
r <- [ [GF28 -> GF28
mE, GF28 -> GF28
mB, GF28 -> GF28
mD, GF28 -> GF28
m9]
, [GF28 -> GF28
m9, GF28 -> GF28
mE, GF28 -> GF28
mB, GF28 -> GF28
mD]
, [GF28 -> GF28
mD, GF28 -> GF28
m9, GF28 -> GF28
mE, GF28 -> GF28
mB]
, [GF28 -> GF28
mB, GF28 -> GF28
mD, GF28 -> GF28
m9, GF28 -> GF28
mE]
]]
mE :: GF28 -> GF28
mE = [GF28] -> GF28 -> GF28 -> GF28
forall b.
(Ord b, SymVal b, Num b) =>
[GF28] -> GF28 -> SBV b -> GF28
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [GF28]
mETable GF28
0
mB :: GF28 -> GF28
mB = [GF28] -> GF28 -> GF28 -> GF28
forall b.
(Ord b, SymVal b, Num b) =>
[GF28] -> GF28 -> SBV b -> GF28
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [GF28]
mBTable GF28
0
mD :: GF28 -> GF28
mD = [GF28] -> GF28 -> GF28 -> GF28
forall b.
(Ord b, SymVal b, Num b) =>
[GF28] -> GF28 -> SBV b -> GF28
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [GF28]
mDTable GF28
0
m9 :: GF28 -> GF28
m9 = [GF28] -> GF28 -> GF28 -> GF28
forall b.
(Ord b, SymVal b, Num b) =>
[GF28] -> GF28 -> SBV b -> GF28
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [GF28]
m9Table GF28
0
mETable :: [GF28]
mETable = (GF28 -> GF28) -> [GF28] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map (GF28 -> GF28 -> GF28
gf28Mult GF28
0xE) [GF28
0..GF28
255]
mBTable :: [GF28]
mBTable = (GF28 -> GF28) -> [GF28] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map (GF28 -> GF28 -> GF28
gf28Mult GF28
0xB) [GF28
0..GF28
255]
mDTable :: [GF28]
mDTable = (GF28 -> GF28) -> [GF28] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map (GF28 -> GF28 -> GF28
gf28Mult GF28
0xD) [GF28
0..GF28
255]
m9Table :: [GF28]
m9Table = (GF28 -> GF28) -> [GF28] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map (GF28 -> GF28 -> GF28
gf28Mult GF28
0x9) [GF28
0..GF28
255]
keyExpansion :: Int -> Key -> [Key]
keyExpansion :: Int -> [SWord 32] -> [[SWord 32]]
keyExpansion Int
nk [SWord 32]
key = [SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 [SWord 32]
keys
where keys :: [SWord 32]
keys :: [SWord 32]
keys = [SWord 32]
key [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [Int -> SWord 32 -> SWord 32 -> SWord 32
nextWord Int
i SWord 32
prev SWord 32
old | Int
i <- [Int
nk ..] | SWord 32
prev <- Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
drop (Int
nkInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SWord 32]
keys | SWord 32
old <- [SWord 32]
keys]
nextWord :: Int -> SWord 32 -> SWord 32 -> SWord 32
nextWord :: Int -> SWord 32 -> SWord 32 -> SWord 32
nextWord Int
i SWord 32
prev SWord 32
old
| Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
nk Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = SWord 32
old SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32 -> GF28 -> SWord 32
subWordRcon (SWord 32
prev SWord 32 -> Int -> SWord 32
forall a. Bits a => a -> Int -> a
`rotateL` Int
8) ([GF28]
roundConstants [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
nk))
| Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
nk Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 Bool -> Bool -> Bool
&& Int
nk Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6 = SWord 32
old SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32 -> GF28 -> SWord 32
subWordRcon SWord 32
prev GF28
0
| Bool
True = SWord 32
old SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
prev
subWordRcon :: SWord 32 -> GF28 -> SWord 32
subWordRcon :: SWord 32 -> GF28 -> SWord 32
subWordRcon SWord 32
w GF28
rc = [GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes [GF28
a GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
`xor` GF28
rc, GF28
b, GF28
c, GF28
d]
where [GF28
a, GF28
b, GF28
c, GF28
d] = (GF28 -> GF28) -> [GF28] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map GF28 -> GF28
sbox ([GF28] -> [GF28]) -> [GF28] -> [GF28]
forall a b. (a -> b) -> a -> b
$ SWord 32 -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes SWord 32
w
sboxTable :: [GF28]
sboxTable :: [GF28]
sboxTable = [GF28 -> GF28
xformByte (GF28 -> GF28
gf28Inverse GF28
b) | GF28
b <- [GF28
0 .. GF28
255]]
where xformByte :: GF28 -> GF28
xformByte :: GF28 -> GF28
xformByte GF28
b = (GF28 -> GF28 -> GF28) -> GF28 -> [GF28] -> GF28
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
xor GF28
0x63 [GF28
b GF28 -> Int -> GF28
forall a. Bits a => a -> Int -> a
`rotateR` Int
i | Int
i <- [Int
0, Int
4, Int
5, Int
6, Int
7]]
sbox :: GF28 -> GF28
sbox :: GF28 -> GF28
sbox = [GF28] -> GF28 -> GF28 -> GF28
forall b.
(Ord b, SymVal b, Num b) =>
[GF28] -> GF28 -> SBV b -> GF28
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [GF28]
sboxTable GF28
0
unSBoxTable :: [GF28]
unSBoxTable :: [GF28]
unSBoxTable = [GF28 -> GF28
gf28Inverse (GF28 -> GF28
xformByte GF28
b) | GF28
b <- [GF28
0 .. GF28
255]]
where xformByte :: GF28 -> GF28
xformByte :: GF28 -> GF28
xformByte GF28
b = (GF28 -> GF28 -> GF28) -> GF28 -> [GF28] -> GF28
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
xor GF28
0x05 [GF28
b GF28 -> Int -> GF28
forall a. Bits a => a -> Int -> a
`rotateR` Int
i | Int
i <- [Int
2, Int
5, Int
7]]
unSBox :: GF28 -> GF28
unSBox :: GF28 -> GF28
unSBox = [GF28] -> GF28 -> GF28 -> GF28
forall b.
(Ord b, SymVal b, Num b) =>
[GF28] -> GF28 -> SBV b -> GF28
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [GF28]
unSBoxTable GF28
0
sboxInverseCorrect :: GF28 -> SBool
sboxInverseCorrect :: GF28 -> SBool
sboxInverseCorrect GF28
x = GF28 -> GF28
unSBox (GF28 -> GF28
sbox GF28
x) GF28 -> GF28 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== GF28
x SBool -> SBool -> SBool
.&& GF28 -> GF28
sbox (GF28 -> GF28
unSBox GF28
x) GF28 -> GF28 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== GF28
x
addRoundKey :: Key -> State -> State
addRoundKey :: [SWord 32] -> [SWord 32] -> [SWord 32]
addRoundKey = (SWord 32 -> SWord 32 -> SWord 32)
-> [SWord 32] -> [SWord 32] -> [SWord 32]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
xor
t0Func :: GF28 -> [GF28]
t0Func :: GF28 -> [GF28]
t0Func GF28
a = [GF28
s GF28 -> GF28 -> GF28
`gf28Mult` GF28
2, GF28
s, GF28
s, GF28
s GF28 -> GF28 -> GF28
`gf28Mult` GF28
3] where s :: GF28
s = GF28 -> GF28
sbox GF28
a
t0 :: GF28 -> SWord 32
t0 :: GF28 -> SWord 32
t0 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t0Table SWord 32
0 where t0Table :: [SWord 32]
t0Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
t0Func GF28
a) | GF28
a <- [GF28
0..GF28
255]]
t1 :: GF28 -> SWord 32
t1 :: GF28 -> SWord 32
t1 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t1Table SWord 32
0 where t1Table :: [SWord 32]
t1Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
t0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
1) | GF28
a <- [GF28
0..GF28
255]]
t2 :: GF28 -> SWord 32
t2 :: GF28 -> SWord 32
t2 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t2Table SWord 32
0 where t2Table :: [SWord 32]
t2Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
t0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
2) | GF28
a <- [GF28
0..GF28
255]]
t3 :: GF28 -> SWord 32
t3 :: GF28 -> SWord 32
t3 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t3Table SWord 32
0 where t3Table :: [SWord 32]
t3Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
t0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
3) | GF28
a <- [GF28
0..GF28
255]]
u0Func :: GF28 -> [GF28]
u0Func :: GF28 -> [GF28]
u0Func GF28
a = [GF28
s GF28 -> GF28 -> GF28
`gf28Mult` GF28
0xE, GF28
s GF28 -> GF28 -> GF28
`gf28Mult` GF28
0x9, GF28
s GF28 -> GF28 -> GF28
`gf28Mult` GF28
0xD, GF28
s GF28 -> GF28 -> GF28
`gf28Mult` GF28
0xB] where s :: GF28
s = GF28 -> GF28
unSBox GF28
a
u0 :: GF28 -> SWord 32
u0 :: GF28 -> SWord 32
u0 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t0Table SWord 32
0 where t0Table :: [SWord 32]
t0Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
u0Func GF28
a) | GF28
a <- [GF28
0..GF28
255]]
u1 :: GF28 -> SWord 32
u1 :: GF28 -> SWord 32
u1 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t1Table SWord 32
0 where t1Table :: [SWord 32]
t1Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
u0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
1) | GF28
a <- [GF28
0..GF28
255]]
u2 :: GF28 -> SWord 32
u2 :: GF28 -> SWord 32
u2 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t2Table SWord 32
0 where t2Table :: [SWord 32]
t2Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
u0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
2) | GF28
a <- [GF28
0..GF28
255]]
u3 :: GF28 -> SWord 32
u3 :: GF28 -> SWord 32
u3 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t3Table SWord 32
0 where t3Table :: [SWord 32]
t3Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
u0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
3) | GF28
a <- [GF28
0..GF28
255]]
doRounds :: (Bool -> State -> Key -> State) -> KS -> State -> State
doRounds :: (Bool -> [SWord 32] -> [SWord 32] -> [SWord 32])
-> KS -> [SWord 32] -> [SWord 32]
doRounds Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
rnd ([SWord 32]
ikey, [[SWord 32]]
rkeys, [SWord 32]
fkey) [SWord 32]
sIn = Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
rnd Bool
True ([[SWord 32]] -> [SWord 32]
forall a. HasCallStack => [a] -> a
last [[SWord 32]]
rs) [SWord 32]
fkey
where s0 :: [SWord 32]
s0 = [SWord 32]
ikey [SWord 32] -> [SWord 32] -> [SWord 32]
`addRoundKey` [SWord 32]
sIn
rs :: [[SWord 32]]
rs = [SWord 32]
s0 [SWord 32] -> [[SWord 32]] -> [[SWord 32]]
forall a. a -> [a] -> [a]
: [Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
rnd Bool
False [SWord 32]
s [SWord 32]
k | [SWord 32]
s <- [[SWord 32]]
rs | [SWord 32]
k <- [[SWord 32]]
rkeys ]
aesRound :: Bool -> State -> Key -> State
aesRound :: Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
aesRound Bool
isFinal [SWord 32]
s [SWord 32]
key = [SWord 32]
d [SWord 32] -> [SWord 32] -> [SWord 32]
`addRoundKey` [SWord 32]
key
where d :: [SWord 32]
d = (Int -> SWord 32) -> [Int] -> [SWord 32]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Int -> SWord 32
f Bool
isFinal) [Int
0..Int
3]
a :: [[GF28]]
a = (SWord 32 -> [GF28]) -> [SWord 32] -> [[GF28]]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes [SWord 32]
s
f :: Bool -> Int -> SWord 32
f Bool
True Int
j = [GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes [ GF28 -> GF28
sbox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
0) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
, GF28 -> GF28
sbox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
, GF28 -> GF28
sbox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
, GF28 -> GF28
sbox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
]
f Bool
False Int
j = SWord 32
e0 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e1 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e2 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e3
where e0 :: SWord 32
e0 = GF28 -> SWord 32
t0 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
0) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
e1 :: SWord 32
e1 = GF28 -> SWord 32
t1 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
e2 :: SWord 32
e2 = GF28 -> SWord 32
t2 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
e3 :: SWord 32
e3 = GF28 -> SWord 32
t3 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
aesInvRound :: Bool -> State -> Key -> State
aesInvRound :: Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
aesInvRound Bool
isFinal [SWord 32]
s [SWord 32]
key = [SWord 32]
d [SWord 32] -> [SWord 32] -> [SWord 32]
`addRoundKey` [SWord 32]
key
where d :: [SWord 32]
d = (Int -> SWord 32) -> [Int] -> [SWord 32]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Int -> SWord 32
f Bool
isFinal) [Int
0..Int
3]
a :: [[GF28]]
a = (SWord 32 -> [GF28]) -> [SWord 32] -> [[GF28]]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes [SWord 32]
s
f :: Bool -> Int -> SWord 32
f Bool
True Int
j = [GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes [ GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
0) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
, GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
, GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
, GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
]
f Bool
False Int
j = SWord 32
e0 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e1 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e2 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e3
where e0 :: SWord 32
e0 = GF28 -> SWord 32
u0 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
0) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
e1 :: SWord 32
e1 = GF28 -> SWord 32
u1 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
e2 :: SWord 32
e2 = GF28 -> SWord 32
u2 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
e3 :: SWord 32
e3 = GF28 -> SWord 32
u3 ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
aesKeySchedule :: Key -> (KS, KS)
aesKeySchedule :: [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key
| Int
nk Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
4, Int
6, Int
8]
= (KS
encKS, KS
decKS)
| Bool
True
= [Char] -> (KS, KS)
forall a. HasCallStack => [Char] -> a
error [Char]
"aesKeySchedule: Invalid key size"
where nk :: Int
nk = [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
key
nr :: Int
nr = Int
nk Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
6
encKS :: KS
encKS@([SWord 32]
f, [[SWord 32]]
m, [SWord 32]
l) = ([[SWord 32]] -> [SWord 32]
forall a. HasCallStack => [a] -> a
head [[SWord 32]]
rKeys, Int -> [[SWord 32]] -> [[SWord 32]]
forall a. Int -> [a] -> [a]
take (Int
nrInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ([[SWord 32]] -> [[SWord 32]]
forall a. HasCallStack => [a] -> [a]
tail [[SWord 32]]
rKeys), [[SWord 32]]
rKeys [[SWord 32]] -> Int -> [SWord 32]
forall a. HasCallStack => [a] -> Int -> a
!! Int
nr)
decKS :: KS
decKS = ([SWord 32]
l, ([SWord 32] -> [SWord 32]) -> [[SWord 32]] -> [[SWord 32]]
forall a b. (a -> b) -> [a] -> [b]
map [SWord 32] -> [SWord 32]
invMixColumns ([[SWord 32]] -> [[SWord 32]]
forall a. [a] -> [a]
reverse [[SWord 32]]
m), [SWord 32]
f)
rKeys :: [[SWord 32]]
rKeys = Int -> [SWord 32] -> [[SWord 32]]
keyExpansion Int
nk [SWord 32]
key
aesEncrypt :: [SWord 32] -> KS -> [SWord 32]
aesEncrypt :: [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
pt KS
encKS
| [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
pt Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4
= (Bool -> [SWord 32] -> [SWord 32] -> [SWord 32])
-> KS -> [SWord 32] -> [SWord 32]
doRounds Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
aesRound KS
encKS [SWord 32]
pt
| Bool
True
= [Char] -> [SWord 32]
forall a. HasCallStack => [Char] -> a
error [Char]
"aesEncrypt: Invalid plain-text size"
aesDecrypt :: [SWord 32] -> KS -> [SWord 32]
aesDecrypt :: [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
ct KS
decKS
| [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
ct Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4
= (Bool -> [SWord 32] -> [SWord 32] -> [SWord 32])
-> KS -> [SWord 32] -> [SWord 32]
doRounds Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
aesInvRound KS
decKS [SWord 32]
ct
| Bool
True
= [Char] -> [SWord 32]
forall a. HasCallStack => [Char] -> a
error [Char]
"aesDecrypt: Invalid cipher-text size"
invKeyExpansion :: Int -> Key -> [Key]
invKeyExpansion :: Int -> [SWord 32] -> [[SWord 32]]
invKeyExpansion Int
nk [SWord 32]
rkey = ([SWord 32] -> [SWord 32]) -> [[SWord 32]] -> [[SWord 32]]
forall a b. (a -> b) -> [a] -> [b]
map [SWord 32] -> [SWord 32]
forall a. [a] -> [a]
reverse ([SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 [SWord 32]
keys)
where keys :: [SWord 32]
keys :: [SWord 32]
keys = [SWord 32]
rkey [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [Int -> SWord 32 -> SWord 32 -> SWord 32
invNextWord Int
i SWord 32
prev SWord 32
old | Int
i <- [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int
0 .. Int
remaining Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] | SWord 32
prev <- Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
drop Int
1 [SWord 32]
keys | SWord 32
old <- [SWord 32]
keys]
totalWords :: Int
totalWords = Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int
nk Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
6 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
remaining :: Int
remaining = Int
totalWords Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nk
invNextWord :: Int -> SWord 32 -> SWord 32 -> SWord 32
invNextWord :: Int -> SWord 32 -> SWord 32 -> SWord 32
invNextWord Int
i SWord 32
prev SWord 32
old
| Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
nk Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = SWord 32
old SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32 -> GF28 -> SWord 32
subWordRcon (SWord 32
prev SWord 32 -> Int -> SWord 32
forall a. Bits a => a -> Int -> a
`rotateL` Int
8) ([GF28]
roundConstants [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
nk))
| Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
nk Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 Bool -> Bool -> Bool
&& Int
nk Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6 = SWord 32
old SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32 -> GF28 -> SWord 32
subWordRcon SWord 32
prev GF28
0
| Bool
True = SWord 32
old SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
prev
subWordRcon :: SWord 32 -> GF28 -> SWord 32
subWordRcon :: SWord 32 -> GF28 -> SWord 32
subWordRcon SWord 32
w GF28
rc = [GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes [GF28
a GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
`xor` GF28
rc, GF28
b, GF28
c, GF28
d]
where [GF28
a, GF28
b, GF28
c, GF28
d] = (GF28 -> GF28) -> [GF28] -> [GF28]
forall a b. (a -> b) -> [a] -> [b]
map GF28 -> GF28
sbox ([GF28] -> [GF28]) -> [GF28] -> [GF28]
forall a b. (a -> b) -> a -> b
$ SWord 32 -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes SWord 32
w
aesInvKeySchedule :: Key -> KS
aesInvKeySchedule :: [SWord 32] -> KS
aesInvKeySchedule [SWord 32]
key
| Int
nk Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
4, Int
6, Int
8]
= KS
decKS
| Bool
True
= [Char] -> KS
forall a. HasCallStack => [Char] -> a
error [Char]
"aesInvKeySchedule: Invalid key size"
where nk :: Int
nk = [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
key
nr :: Int
nr = Int
nk Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
6
decKS :: KS
decKS = ([[SWord 32]] -> [SWord 32]
forall a. HasCallStack => [a] -> a
head [[SWord 32]]
rKeys, Int -> [[SWord 32]] -> [[SWord 32]]
forall a. Int -> [a] -> [a]
take (Int
nrInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) ([[SWord 32]] -> [[SWord 32]]
forall a. HasCallStack => [a] -> [a]
tail [[SWord 32]]
rKeys), [[SWord 32]]
rKeys [[SWord 32]] -> Int -> [SWord 32]
forall a. HasCallStack => [a] -> Int -> a
!! Int
nr)
rKeys :: [[SWord 32]]
rKeys = Int -> [SWord 32] -> [[SWord 32]]
invKeyExpansion Int
nk [SWord 32]
key
aesDecryptUnwoundKey :: [SWord 32] -> KS -> [SWord 32]
aesDecryptUnwoundKey :: [SWord 32] -> KS -> [SWord 32]
aesDecryptUnwoundKey [SWord 32]
ct KS
decKS
| [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
ct Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4
= (Bool -> [SWord 32] -> [SWord 32] -> [SWord 32])
-> KS -> [SWord 32] -> [SWord 32]
doRounds Bool -> [SWord 32] -> [SWord 32] -> [SWord 32]
forall {a}.
ByteConverter a =>
Bool -> [a] -> [SWord 32] -> [SWord 32]
aesInvRoundRegular KS
decKS [SWord 32]
ct
| Bool
True
= [Char] -> [SWord 32]
forall a. HasCallStack => [Char] -> a
error [Char]
"aesDecrypt: Invalid cipher-text size"
where aesInvRoundRegular :: Bool -> [a] -> [SWord 32] -> [SWord 32]
aesInvRoundRegular Bool
isFinal [a]
s [SWord 32]
key = [SWord 32]
u
where u :: State
u :: [SWord 32]
u = (Int -> SWord 32) -> [Int] -> [SWord 32]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Int -> SWord 32
f Bool
isFinal) [Int
0 .. Int
3]
where a :: [[GF28]]
a = (a -> [GF28]) -> [a] -> [[GF28]]
forall a b. (a -> b) -> [a] -> [b]
map a -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes [a]
s
kbs :: [[GF28]]
kbs = (SWord 32 -> [GF28]) -> [SWord 32] -> [[GF28]]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> [GF28]
forall a. ByteConverter a => a -> [GF28]
toBytes [SWord 32]
key
f :: Bool -> Int -> SWord 32
f Bool
True Int
j = [GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes [ GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
0) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
, GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
, GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
, GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
] SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` ([SWord 32]
key [SWord 32] -> Int -> SWord 32
forall a. HasCallStack => [a] -> Int -> a
!! Int
j)
f Bool
False Int
j = SWord 32
e0 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e1 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e2 SWord 32 -> SWord 32 -> SWord 32
forall a. Bits a => a -> a -> a
`xor` SWord 32
e3
where e0 :: SWord 32
e0 = GF28 -> SWord 32
otfU0 (GF28 -> SWord 32) -> GF28 -> SWord 32
forall a b. (a -> b) -> a -> b
$ GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
0) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0) GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
`xor` ([[GF28]]
kbs [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! Int
j [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
0)
e1 :: SWord 32
e1 = GF28 -> SWord 32
otfU1 (GF28 -> SWord 32) -> GF28 -> SWord 32
forall a b. (a -> b) -> a -> b
$ GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
3) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1) GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
`xor` ([[GF28]]
kbs [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! Int
j [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
1)
e2 :: SWord 32
e2 = GF28 -> SWord 32
otfU2 (GF28 -> SWord 32) -> GF28 -> SWord 32
forall a b. (a -> b) -> a -> b
$ GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
2) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2) GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
`xor` ([[GF28]]
kbs [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! Int
j [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
2)
e3 :: SWord 32
e3 = GF28 -> SWord 32
otfU3 (GF28 -> SWord 32) -> GF28 -> SWord 32
forall a b. (a -> b) -> a -> b
$ GF28 -> GF28
unSBox ([[GF28]]
a [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! ((Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4) [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3) GF28 -> GF28 -> GF28
forall a. Bits a => a -> a -> a
`xor` ([[GF28]]
kbs [[GF28]] -> Int -> [GF28]
forall a. HasCallStack => [a] -> Int -> a
!! Int
j [GF28] -> Int -> GF28
forall a. HasCallStack => [a] -> Int -> a
!! Int
3)
otfU0Func :: GF28 -> [GF28]
otfU0Func GF28
b = [GF28
b GF28 -> GF28 -> GF28
`gf28Mult` GF28
0xE, GF28
b GF28 -> GF28 -> GF28
`gf28Mult` GF28
0x9, GF28
b GF28 -> GF28 -> GF28
`gf28Mult` GF28
0xD, GF28
b GF28 -> GF28 -> GF28
`gf28Mult` GF28
0xB]
otfU0 :: GF28 -> SWord 32
otfU0 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t0Table SWord 32
0 where t0Table :: [SWord 32]
t0Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
otfU0Func GF28
a) | GF28
a <- [GF28
0..GF28
255]]
otfU1 :: GF28 -> SWord 32
otfU1 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t1Table SWord 32
0 where t1Table :: [SWord 32]
t1Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
otfU0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
1) | GF28
a <- [GF28
0..GF28
255]]
otfU2 :: GF28 -> SWord 32
otfU2 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t2Table SWord 32
0 where t2Table :: [SWord 32]
t2Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
otfU0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
2) | GF28
a <- [GF28
0..GF28
255]]
otfU3 :: GF28 -> SWord 32
otfU3 = [SWord 32] -> SWord 32 -> GF28 -> SWord 32
forall b.
(Ord b, SymVal b, Num b) =>
[SWord 32] -> SWord 32 -> SBV b -> SWord 32
forall a b.
(Mergeable a, Ord b, SymVal b, Num b) =>
[a] -> a -> SBV b -> a
select [SWord 32]
t3Table SWord 32
0 where t3Table :: [SWord 32]
t3Table = [[GF28] -> SWord 32
forall a. ByteConverter a => [GF28] -> a
fromBytes (GF28 -> [GF28]
otfU0Func GF28
a [GF28] -> Int -> [GF28]
`rotR` Int
3) | GF28
a <- [GF28
0..GF28
255]]
commonPT :: [SWord 32]
commonPT :: [SWord 32]
commonPT = [SWord 32
0x00112233, SWord 32
0x44556677, SWord 32
0x8899aabb, SWord 32
0xccddeeff]
aes128Key :: Key
aes128Key :: [SWord 32]
aes128Key = [SWord 32
0x00010203, SWord 32
0x04050607, SWord 32
0x08090a0b, SWord 32
0x0c0d0e0f]
aes192Key :: Key
aes192Key :: [SWord 32]
aes192Key = [SWord 32]
aes128Key [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [SWord 32
0x10111213, SWord 32
0x14151617]
aes256Key :: Key
aes256Key :: [SWord 32]
aes256Key = [SWord 32]
aes192Key [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [SWord 32
0x18191a1b, SWord 32
0x1c1d1e1f]
aes128CT :: [SWord 32]
aes128CT :: [SWord 32]
aes128CT = [SWord 32
0x69c4e0d8, SWord 32
0x6a7b0430, SWord 32
0xd8cdb780, SWord 32
0x70b4c55a]
aes192CT :: [SWord 32]
aes192CT :: [SWord 32]
aes192CT = [SWord 32
0xdda97ca4, SWord 32
0x864cdfe0, SWord 32
0x6eaf70a0, SWord 32
0xec0d7191]
aes256CT :: [SWord 32]
aes256CT :: [SWord 32]
aes256CT = [SWord 32
0x8ea2b7ca, SWord 32
0x516745bf, SWord 32
0xeafc4990, SWord 32
0x4b496089]
aes128InvKey :: Key
aes128InvKey :: [SWord 32]
aes128InvKey = [SWord 32] -> [SWord 32]
extractFinalKey [SWord 32]
aes128Key
aes192InvKey :: Key
aes192InvKey :: [SWord 32]
aes192InvKey = [SWord 32] -> [SWord 32]
extractFinalKey [SWord 32]
aes192Key
aes192InvKeyExtended :: Key
aes192InvKeyExtended :: [SWord 32]
aes192InvKeyExtended = [SWord 32] -> [SWord 32]
extractFinalKeyExtended [SWord 32]
aes192Key
aes256InvKey :: Key
aes256InvKey :: [SWord 32]
aes256InvKey = [SWord 32] -> [SWord 32]
extractFinalKey [SWord 32]
aes256Key
extractFinalKey :: [SWord 32] -> [SWord 32]
[SWord 32]
initKey = Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take Int
nk ([SWord 32] -> [SWord 32]
extractFinalKeyExtended [SWord 32]
initKey)
where nk :: Int
nk = [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
initKey
extractFinalKeyExtended :: [SWord 32] -> [SWord 32]
[SWord 32]
initKey = Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take Int
feed (([SWord 32] -> [SWord 32]) -> [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SWord 32] -> [SWord 32]
forall a. [a] -> [a]
reverse ([SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 (Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take Int
feed [SWord 32]
roundKeys)))
where nk :: Int
nk = [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
initKey
feed :: Int
feed | Int
nk Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 = Int
4
| Bool
True = Int
8
(([SWord 32]
f, [[SWord 32]]
m, [SWord 32]
l), KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
initKey
roundKeys :: [SWord 32]
roundKeys = [SWord 32]
l [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SWord 32]] -> [[SWord 32]]
forall a. [a] -> [a]
reverse [[SWord 32]]
m) [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [SWord 32]
f
t128Enc :: [SWord 32]
t128Enc :: [SWord 32]
t128Enc = [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
commonPT KS
ks
where (KS
ks, KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
aes128Key
t128Dec :: [SWord 32]
t128Dec :: [SWord 32]
t128Dec = [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
aes128CT KS
ks
where (KS
_, KS
ks) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
aes128Key
t192Enc :: [SWord 32]
t192Enc :: [SWord 32]
t192Enc = [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
commonPT KS
ks
where (KS
ks, KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
aes192Key
t192Dec :: [SWord 32]
t192Dec :: [SWord 32]
t192Dec = [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
aes192CT KS
ks
where (KS
_, KS
ks) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
aes192Key
t256Enc :: [SWord 32]
t256Enc :: [SWord 32]
t256Enc = [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
commonPT KS
ks
where (KS
ks, KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
aes256Key
t256Dec :: [SWord 32]
t256Dec :: [SWord 32]
t256Dec = [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
aes256CT KS
ks
where (KS
_, KS
ks) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
aes256Key
runAESTests :: Bool -> IO ()
runAESTests :: Bool -> IO ()
runAESTests Bool
runQC = do
IO ()
testInvKeyExpansion
[Char] -> [SWord 32] -> [SWord 32] -> [SWord 32] -> IO ()
check [Char]
"AES128" [SWord 32]
aes128Key [SWord 32]
aes128InvKey [SWord 32]
aes128CT
[Char] -> [SWord 32] -> [SWord 32] -> [SWord 32] -> IO ()
check [Char]
"AES192" [SWord 32]
aes192Key [SWord 32]
aes192InvKey [SWord 32]
aes192CT
[Char] -> [SWord 32] -> [SWord 32] -> [SWord 32] -> IO ()
check [Char]
"AES256" [SWord 32]
aes256Key [SWord 32]
aes256InvKey [SWord 32]
aes256CT
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
runQC (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[Char] -> IO ()
putStrLn [Char]
"Quick-check AES128 roundtrip" IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32) -> SBool)
-> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32) -> SBool
roundTrip128
[Char] -> IO ()
putStrLn [Char]
"Quick-check AES192 roundtrip" IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32, SWord32, SWord32) -> SBool)
-> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32, SWord32, SWord32) -> SBool
roundTrip192
[Char] -> IO ()
putStrLn [Char]
"Quick-check AES256 roundtrip" IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ((SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32, SWord32, SWord32, SWord32,
SWord32)
-> SBool)
-> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32, SWord32, SWord32, SWord32,
SWord32)
-> SBool
roundTrip256
where check :: String -> Key -> Key -> [SWord 32] -> IO ()
check :: [Char] -> [SWord 32] -> [SWord 32] -> [SWord 32] -> IO ()
check [Char]
what [SWord 32]
key [SWord 32]
invKey [SWord 32]
ctExpected = do [Char] -> [SWord 32] -> [SWord 32] -> IO ()
eq ([Char]
"Encryption " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what) [SWord 32]
ctExpected [SWord 32]
ctGot
[Char] -> [SWord 32] -> [SWord 32] -> IO ()
eq ([Char]
"Decryption " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what) [SWord 32]
commonPT [SWord 32]
ptGot
[Char] -> [SWord 32] -> [SWord 32] -> IO ()
eq ([Char]
"Decryption-OTF " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what) [SWord 32]
commonPT [SWord 32]
ptGotInv
where (KS
encKS, KS
decKS) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key
ctGot :: [SWord 32]
ctGot = [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
commonPT KS
encKS
ptGot :: [SWord 32]
ptGot = [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
ctExpected KS
decKS
ptGotInv :: [SWord 32]
ptGotInv = [SWord 32] -> KS -> [SWord 32]
aesDecryptUnwoundKey [SWord 32]
ctExpected ([SWord 32] -> KS
aesInvKeySchedule [SWord 32]
invKey)
eq :: [Char] -> [SWord 32] -> [SWord 32] -> IO ()
eq [Char]
tag [SWord 32]
expected [SWord 32]
got
| [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
expected Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
got
= [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"BAD!: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
tag
, [Char]
"Comparing different sized lists:"
, [Char]
"Expected: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SWord 32] -> [Char]
forall a. Show a => a -> [Char]
show [SWord 32]
expected
, [Char]
"Got : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SWord 32] -> [Char]
forall a. Show a => a -> [Char]
show [SWord 32]
got
]
| (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> Integer
extract [SWord 32]
expected [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> Integer
extract [SWord 32]
got
= [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"GOOD: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
tag
| Bool
True
= [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"BAD!: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
tag
, [Char]
"Expected: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ((SWord 32 -> [Char]) -> [SWord 32] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> [Char]
forall a. (SymVal a, Show a, Integral a) => SBV a -> [Char]
hex8 [SWord 32]
expected)
, [Char]
"Got : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ((SWord 32 -> [Char]) -> [SWord 32] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> [Char]
forall a. (SymVal a, Show a, Integral a) => SBV a -> [Char]
hex8 [SWord 32]
got)
]
where extract :: SWord 32 -> Integer
extract :: SWord 32 -> Integer
extract = WordN 32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN 32 -> Integer)
-> (SWord 32 -> WordN 32) -> SWord 32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (WordN 32) -> WordN 32
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN 32) -> WordN 32)
-> (SWord 32 -> Maybe (WordN 32)) -> SWord 32 -> WordN 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 32 -> Maybe (WordN 32)
forall a. SymVal a => SBV a -> Maybe a
unliteral
testInvKeyExpansion :: IO ()
testInvKeyExpansion :: IO ()
testInvKeyExpansion = do [Char] -> [SWord 32] -> IO ()
goTestInvKey [Char]
"128" [SWord 32]
aes128Key
[Char] -> [SWord 32] -> IO ()
goTestInvKey [Char]
"192" [SWord 32]
aes192Key
[Char] -> [SWord 32] -> IO ()
goTestInvKey [Char]
"256" [SWord 32]
aes256Key
goTestInvKey :: [Char] -> [SWord 32] -> IO ()
goTestInvKey [Char]
what [SWord 32]
k = do
let nk :: Int
nk = [SWord 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SWord 32]
k
nr :: Int
nr = Int
nk Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
6
feed :: Int
feed = case Int
nk of
Int
4 -> Int
4
Int
_ -> Int
8
(([SWord 32]
f, [[SWord 32]]
m, [SWord 32]
l), KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
k
required :: [SWord 32]
required = [SWord 32]
l [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SWord 32]] -> [[SWord 32]]
forall a. [a] -> [a]
reverse [[SWord 32]]
m) [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [SWord 32]
f
invKeySchedule :: [[SWord 32]]
invKeySchedule = Int -> [[SWord 32]] -> [[SWord 32]]
forall a. Int -> [a] -> [a]
take (Int
nrInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([[SWord 32]] -> [[SWord 32]]) -> [[SWord 32]] -> [[SWord 32]]
forall a b. (a -> b) -> a -> b
$ Int -> [SWord 32] -> [[SWord 32]]
invKeyExpansion Int
nk (Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take Int
nk (([SWord 32] -> [SWord 32]) -> [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SWord 32] -> [SWord 32]
forall a. [a] -> [a]
reverse ([SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 (Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take Int
feed [SWord 32]
required))))
obtained :: [SWord 32]
obtained = [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SWord 32]]
invKeySchedule
expected :: [WordN 32]
expected = (SWord 32 -> WordN 32) -> [SWord 32] -> [WordN 32]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (WordN 32) -> WordN 32
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN 32) -> WordN 32)
-> (SWord 32 -> Maybe (WordN 32)) -> SWord 32 -> WordN 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 32 -> Maybe (WordN 32)
forall a. SymVal a => SBV a -> Maybe a
unliteral) [SWord 32]
required
result :: [WordN 32]
result = (SWord 32 -> WordN 32) -> [SWord 32] -> [WordN 32]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (WordN 32) -> WordN 32
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN 32) -> WordN 32)
-> (SWord 32 -> Maybe (WordN 32)) -> SWord 32 -> WordN 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 32 -> Maybe (WordN 32)
forall a. SymVal a => SBV a -> Maybe a
unliteral) [SWord 32]
obtained
sh :: a -> [WordN 32] -> [WordN 32] -> [Char]
sh a
i [WordN 32]
a [WordN 32]
b
| [WordN 32]
a [WordN 32] -> [WordN 32] -> Bool
forall a. Eq a => a -> a -> Bool
== [WordN 32]
b = [Char]
pad [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [WordN 32] -> [Char]
disp [WordN 32]
a
| Bool
True = [Char]
pad [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [WordN 32] -> [Char]
disp [WordN 32]
a [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" |vs| " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [WordN 32] -> [Char]
disp [WordN 32]
b
where pad :: [Char]
pad = if a
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
10 then [Char]
" " else [Char]
""
disp :: [WordN 32] -> [Char]
disp = [[Char]] -> [Char]
unwords ([[Char]] -> [Char])
-> ([WordN 32] -> [[Char]]) -> [WordN 32] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WordN 32 -> [Char]) -> [WordN 32] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (SWord 32 -> [Char]
forall a. (SymVal a, Show a, Integral a) => SBV a -> [Char]
hex8 (SWord 32 -> [Char])
-> (WordN 32 -> SWord 32) -> WordN 32 -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN 32 -> SWord 32
forall a. SymVal a => a -> SBV a
literal)
lexpected :: Int
lexpected = [WordN 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [WordN 32]
expected
lresult :: Int
lresult = [WordN 32] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [WordN 32]
result
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
lexpected Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
lresult) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
[Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": BAD! Mismatching lengths: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int
lexpected, Int
lresult)
let debugging :: Bool
debugging = Bool
False
if [WordN 32]
expected [WordN 32] -> [WordN 32] -> Bool
forall a. Eq a => a -> a -> Bool
== [WordN 32]
result
then if Bool
debugging
then [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ([Char]
"Size " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": Good") [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Int -> [WordN 32] -> [WordN 32] -> [Char])
-> [Int] -> [[WordN 32]] -> [[WordN 32]] -> [[Char]]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Int -> [WordN 32] -> [WordN 32] -> [Char]
forall {a}.
(Show a, Ord a, Num a) =>
a -> [WordN 32] -> [WordN 32] -> [Char]
sh [(Int
0::Int)..] ([WordN 32] -> [[WordN 32]]
forall a. [a] -> [[a]]
chop4 [WordN 32]
expected) ([WordN 32] -> [[WordN 32]]
forall a. [a] -> [[a]]
chop4 [WordN 32]
result)
else [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"GOOD: Key generation AES" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what
else [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ([Char]
"Size " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
what [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": BAD!") [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: (Int -> [WordN 32] -> [WordN 32] -> [Char])
-> [Int] -> [[WordN 32]] -> [[WordN 32]] -> [[Char]]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Int -> [WordN 32] -> [WordN 32] -> [Char]
forall {a}.
(Show a, Ord a, Num a) =>
a -> [WordN 32] -> [WordN 32] -> [Char]
sh [(Int
0::Int)..] ([WordN 32] -> [[WordN 32]]
forall a. [a] -> [[a]]
chop4 [WordN 32]
expected) ([WordN 32] -> [[WordN 32]]
forall a. [a] -> [[a]]
chop4 [WordN 32]
result)
roundTrip128 :: (SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32) -> SBool
roundTrip128 (SWord32
i0, SWord32
i1, SWord32
i2, SWord32
i3) (SWord32
k0, SWord32
k1, SWord32
k2, SWord32
k3) = [SWord32] -> [SWord32] -> SBool
roundTrip [SWord32
i0, SWord32
i1, SWord32
i2, SWord32
i3] [SWord32
k0, SWord32
k1, SWord32
k2, SWord32
k3]
roundTrip192 :: (SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32, SWord32, SWord32) -> SBool
roundTrip192 (SWord32
i0, SWord32
i1, SWord32
i2, SWord32
i3) (SWord32
k0, SWord32
k1, SWord32
k2, SWord32
k3, SWord32
k4, SWord32
k5) = [SWord32] -> [SWord32] -> SBool
roundTrip [SWord32
i0, SWord32
i1, SWord32
i2, SWord32
i3] [SWord32
k0, SWord32
k1, SWord32
k2, SWord32
k3, SWord32
k4, SWord32
k5]
roundTrip256 :: (SWord32, SWord32, SWord32, SWord32)
-> (SWord32, SWord32, SWord32, SWord32, SWord32, SWord32, SWord32,
SWord32)
-> SBool
roundTrip256 (SWord32
i0, SWord32
i1, SWord32
i2, SWord32
i3) (SWord32
k0, SWord32
k1, SWord32
k2, SWord32
k3, SWord32
k4, SWord32
k5, SWord32
k6, SWord32
k7) = [SWord32] -> [SWord32] -> SBool
roundTrip [SWord32
i0, SWord32
i1, SWord32
i2, SWord32
i3] [SWord32
k0, SWord32
k1, SWord32
k2, SWord32
k3, SWord32
k4, SWord32
k5, SWord32
k6, SWord32
k7]
roundTrip :: [SWord32] -> [SWord32] -> SBool
roundTrip :: [SWord32] -> [SWord32] -> SBool
roundTrip [SWord32]
ptIn [SWord32]
keyIn = [SWord 32]
pt [SWord 32] -> [SWord 32] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== [SWord 32]
pt' SBool -> SBool -> SBool
.&& [SWord 32]
pt [SWord 32] -> [SWord 32] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== [SWord 32]
pt''
where pt :: [SWord 32]
pt = (SWord32 -> SWord 32) -> [SWord32] -> [SWord 32]
forall a b. (a -> b) -> [a] -> [b]
map SWord32 -> SWord 32
SWord32 -> ToSized SWord32
forall a. ToSizedBV a => a -> ToSized a
toSized [SWord32]
ptIn
key :: [SWord 32]
key = (SWord32 -> SWord 32) -> [SWord32] -> [SWord 32]
forall a b. (a -> b) -> [a] -> [b]
map SWord32 -> SWord 32
SWord32 -> ToSized SWord32
forall a. ToSizedBV a => a -> ToSized a
toSized [SWord32]
keyIn
(KS
encKS, KS
decKS) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key
ct :: [SWord 32]
ct = [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
pt KS
encKS
pt' :: [SWord 32]
pt' = [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
ct KS
decKS
pt'' :: [SWord 32]
pt'' = [SWord 32] -> KS -> [SWord 32]
aesDecryptUnwoundKey [SWord 32]
ct ([SWord 32] -> KS
aesInvKeySchedule ([SWord 32] -> [SWord 32]
extractFinalKey [SWord 32]
key))
aes128IsCorrect :: (SWord 32, SWord 32, SWord 32, SWord 32)
-> (SWord 32, SWord 32, SWord 32, SWord 32)
-> SBool
aes128IsCorrect :: (SWord 32, SWord 32, SWord 32, SWord 32)
-> (SWord 32, SWord 32, SWord 32, SWord 32) -> SBool
aes128IsCorrect (SWord 32
i0, SWord 32
i1, SWord 32
i2, SWord 32
i3) (SWord 32
k0, SWord 32
k1, SWord 32
k2, SWord 32
k3) = [SWord 32]
pt [SWord 32] -> [SWord 32] -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== [SWord 32]
pt'
where pt :: [SWord 32]
pt = [SWord 32
i0, SWord 32
i1, SWord 32
i2, SWord 32
i3]
key :: [SWord 32]
key = [SWord 32
k0, SWord 32
k1, SWord 32
k2, SWord 32
k3]
(KS
encKS, KS
decKS) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key
ct :: [SWord 32]
ct = [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
pt KS
encKS
pt' :: [SWord 32]
pt' = [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
ct KS
decKS
aes128Enc :: SWord 128 -> SWord 128 -> SWord 128
aes128Enc :: SWord 128 -> SWord 128 -> SWord 128
aes128Enc SWord 128
key SWord 128
pt = [SWord 32] -> SWord 128
from32 ([SWord 32] -> SWord 128) -> [SWord 32] -> SWord 128
forall a b. (a -> b) -> a -> b
$ [SWord 32] -> KS -> [SWord 32]
aesEncrypt (SWord 128 -> [SWord 32]
to32 SWord 128
pt) KS
ks
where to32 :: SWord 128 -> [SWord 32]
to32 :: SWord 128 -> [SWord 32]
to32 SWord 128
x = [ Proxy 127 -> Proxy 96 -> SWord 128 -> SBV (WordN ((127 - 96) + 1))
forall (i :: Natural) (j :: Natural) (n :: Natural)
(bv :: Natural -> *) (proxy :: Natural -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @127) (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @96) SWord 128
x
, Proxy 95 -> Proxy 64 -> SWord 128 -> SBV (WordN ((95 - 64) + 1))
forall (i :: Natural) (j :: Natural) (n :: Natural)
(bv :: Natural -> *) (proxy :: Natural -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @95) (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @64) SWord 128
x
, Proxy 63 -> Proxy 32 -> SWord 128 -> SBV (WordN ((63 - 32) + 1))
forall (i :: Natural) (j :: Natural) (n :: Natural)
(bv :: Natural -> *) (proxy :: Natural -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @63) (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @32) SWord 128
x
, Proxy 31 -> Proxy 0 -> SWord 128 -> SBV (WordN ((31 - 0) + 1))
forall (i :: Natural) (j :: Natural) (n :: Natural)
(bv :: Natural -> *) (proxy :: Natural -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @31) (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) SWord 128
x
]
from32 :: [SWord 32] -> SWord 128
from32 :: [SWord 32] -> SWord 128
from32 [SWord 32
a, SWord 32
b, SWord 32
c, SWord 32
d] = SWord 32
a SWord 32 -> SBV (WordN 96) -> SBV (WordN (32 + 96))
forall (n :: Natural) (bv :: Natural -> *) (m :: Natural).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
b SWord 32 -> SBV (WordN 64) -> SBV (WordN (32 + 64))
forall (n :: Natural) (bv :: Natural -> *) (m :: Natural).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
c SWord 32 -> SWord 32 -> SBV (WordN (32 + 32))
forall (n :: Natural) (bv :: Natural -> *) (m :: Natural).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
d
from32 [SWord 32]
_ = [Char] -> SWord 128
forall a. HasCallStack => [Char] -> a
error [Char]
"nope"
(KS
ks, KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule (SWord 128 -> [SWord 32]
to32 SWord 128
key)
cgAES128BlockEncrypt :: IO ()
cgAES128BlockEncrypt :: IO ()
cgAES128BlockEncrypt = Maybe [Char] -> [Char] -> SBVCodeGen () -> IO ()
forall a. Maybe [Char] -> [Char] -> SBVCodeGen a -> IO a
compileToC Maybe [Char]
forall a. Maybe a
Nothing [Char]
"aes128BlockEncrypt" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
[SWord 32]
pt <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
4 [Char]
"pt"
[SWord 32]
key <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
4 [Char]
"key"
[Integer] -> SBVCodeGen ()
cgSetDriverValues ([Integer] -> SBVCodeGen ()) -> [Integer] -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (WordN 32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN 32 -> Integer)
-> (SWord 32 -> WordN 32) -> SWord 32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (WordN 32) -> WordN 32
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN 32) -> WordN 32)
-> (SWord 32 -> Maybe (WordN 32)) -> SWord 32 -> WordN 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 32 -> Maybe (WordN 32)
forall a. SymVal a => SBV a -> Maybe a
unliteral) ([SWord 32] -> [Integer]) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [SWord 32]
commonPT [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [SWord 32]
aes128Key
let (KS
encKs, KS
_) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"ct" ([SWord 32] -> SBVCodeGen ()) -> [SWord 32] -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
pt KS
encKs
aesLibComponents :: Int -> [(String, [Integer], SBVCodeGen ())]
aesLibComponents :: Int -> [([Char], [Integer], SBVCodeGen ())]
aesLibComponents Int
sz = [ ([Char]
"aes" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"KeySchedule", [Integer]
keyDriverVals, SBVCodeGen ()
keySchedule)
, ([Char]
"aes" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"BlockEncrypt", [Integer]
encDriverVals, SBVCodeGen ()
enc)
, ([Char]
"aes" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"BlockDecrypt", [Integer]
decDriverVals, SBVCodeGen ()
dec)
, ([Char]
"aes" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"InvKeySchedule", [Integer]
invKeyDriverVals, SBVCodeGen ()
invKeySchedule)
, ([Char]
"aes" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"OTFDecrypt", [Integer]
invDecDriverVals, SBVCodeGen ()
otfDec)
]
where badSize :: a
badSize = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"aesLibComponents: Size must be one of 128, 192, or 256; received: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz
nk :: Int
nk
| Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
128 = Int
4
| Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
192 = Int
6
| Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
256 = Int
8
| Bool
True = Int
forall {a}. a
badSize
nr :: Int
nr = Int
nk Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
6
xk :: Int
xk = Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* (Int
nr Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
([Integer]
keyDriverVals, [Integer]
invKeyDriverVals, [Integer]
encDriverVals, [Integer]
decDriverVals, [Integer]
invDecDriverVals)
| Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
128 = ([SWord 32] -> [Integer]
keyDriver [SWord 32]
aes128Key, [SWord 32] -> [Integer]
keyDriver [SWord 32]
aes128InvKey, [SWord 32] -> [SWord 32] -> [Integer]
encDriver [SWord 32]
commonPT [SWord 32]
aes128Key, [SWord 32] -> [SWord 32] -> [Integer]
decDriver [SWord 32]
aes128CT [SWord 32]
aes128Key, [SWord 32] -> [SWord 32] -> [Integer]
invDecDriver [SWord 32]
aes128CT [SWord 32]
aes128InvKey)
| Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
192 = ([SWord 32] -> [Integer]
keyDriver [SWord 32]
aes192Key, [SWord 32] -> [Integer]
keyDriver [SWord 32]
aes192InvKey, [SWord 32] -> [SWord 32] -> [Integer]
encDriver [SWord 32]
commonPT [SWord 32]
aes192Key, [SWord 32] -> [SWord 32] -> [Integer]
decDriver [SWord 32]
aes192CT [SWord 32]
aes192Key, [SWord 32] -> [SWord 32] -> [Integer]
invDecDriver [SWord 32]
aes192CT [SWord 32]
aes192InvKey)
| Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
256 = ([SWord 32] -> [Integer]
keyDriver [SWord 32]
aes256Key, [SWord 32] -> [Integer]
keyDriver [SWord 32]
aes256InvKey, [SWord 32] -> [SWord 32] -> [Integer]
encDriver [SWord 32]
commonPT [SWord 32]
aes256Key, [SWord 32] -> [SWord 32] -> [Integer]
decDriver [SWord 32]
aes256CT [SWord 32]
aes256Key, [SWord 32] -> [SWord 32] -> [Integer]
invDecDriver [SWord 32]
aes256CT [SWord 32]
aes256InvKey)
| Bool
True = ([Integer], [Integer], [Integer], [Integer], [Integer])
forall {a}. a
badSize
where keyDriver :: [SWord 32] -> [Integer]
keyDriver [SWord 32]
key = (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> Integer
cvt ([SWord 32] -> [Integer]) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> a -> b
$ ([SWord 32] -> [SWord 32]) -> [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SWord 32] -> [SWord 32]
forall a. [a] -> [a]
reverse ([SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 [SWord 32]
key)
encDriver :: [SWord 32] -> [SWord 32] -> [Integer]
encDriver [SWord 32]
pt [SWord 32]
key = (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> Integer
cvt ([SWord 32] -> [Integer]) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [SWord 32]
pt [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ KS -> [SWord 32]
forall {t :: * -> *} {a}. Foldable t => ([a], t [a], [a]) -> [a]
flatten ((KS, KS) -> KS
forall a b. (a, b) -> a
fst ([SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key))
decDriver :: [SWord 32] -> [SWord 32] -> [Integer]
decDriver [SWord 32]
ct [SWord 32]
key = (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> Integer
cvt ([SWord 32] -> [Integer]) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [SWord 32]
ct [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ KS -> [SWord 32]
forall {t :: * -> *} {a}. Foldable t => ([a], t [a], [a]) -> [a]
flatten ((KS, KS) -> KS
forall a b. (a, b) -> b
snd ([SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key))
invDecDriver :: [SWord 32] -> [SWord 32] -> [Integer]
invDecDriver [SWord 32]
ct [SWord 32]
key = (SWord 32 -> Integer) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map SWord 32 -> Integer
cvt ([SWord 32] -> [Integer]) -> [SWord 32] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [SWord 32]
ct [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ KS -> [SWord 32]
forall {t :: * -> *} {a}. Foldable t => ([a], t [a], [a]) -> [a]
flatten ([SWord 32] -> KS
aesInvKeySchedule [SWord 32]
key)
flatten :: ([a], t [a], [a]) -> [a]
flatten ([a]
f, t [a]
mid, [a]
l) = [a]
f [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ t [a] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat t [a]
mid [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
l
cvt :: SWord 32 -> Integer
cvt = WordN 32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (WordN 32 -> Integer)
-> (SWord 32 -> WordN 32) -> SWord 32 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (WordN 32) -> WordN 32
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WordN 32) -> WordN 32)
-> (SWord 32 -> Maybe (WordN 32)) -> SWord 32 -> WordN 32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord 32 -> Maybe (WordN 32)
forall a. SymVal a => SBV a -> Maybe a
unliteral
keySchedule :: SBVCodeGen ()
keySchedule = do [SWord 32]
key <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
nk [Char]
"key"
let (KS
encKS, KS
decKS) = [SWord 32] -> (KS, KS)
aesKeySchedule [SWord 32]
key
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"encKS" (KS -> [SWord 32]
ksToXKey KS
encKS)
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"decKS" (KS -> [SWord 32]
ksToXKey KS
decKS)
invKeySchedule :: SBVCodeGen ()
invKeySchedule = do [SWord 32]
key <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
nk [Char]
"key"
let decKS :: KS
decKS = [SWord 32] -> KS
aesInvKeySchedule (([SWord 32] -> [SWord 32]) -> [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SWord 32] -> [SWord 32]
forall a. [a] -> [a]
reverse ([SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 [SWord 32]
key))
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"decKS" (KS -> [SWord 32]
ksToXKey KS
decKS)
enc :: SBVCodeGen ()
enc = do [SWord 32]
pt <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
4 [Char]
"pt"
[SWord 32]
xkey <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
xk [Char]
"xkey"
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"ct" ([SWord 32] -> SBVCodeGen ()) -> [SWord 32] -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ [SWord 32] -> KS -> [SWord 32]
aesEncrypt [SWord 32]
pt ([SWord 32] -> KS
xkeyToKS [SWord 32]
xkey)
dec :: SBVCodeGen ()
dec = do [SWord 32]
pt <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
4 [Char]
"ct"
[SWord 32]
xkey <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
xk [Char]
"xkey"
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"pt" ([SWord 32] -> SBVCodeGen ()) -> [SWord 32] -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ [SWord 32] -> KS -> [SWord 32]
aesDecrypt [SWord 32]
pt ([SWord 32] -> KS
xkeyToKS [SWord 32]
xkey)
otfDec :: SBVCodeGen ()
otfDec = do [SWord 32]
ct <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
4 [Char]
"ct"
[SWord 32]
xkey <- Int -> [Char] -> SBVCodeGen [SWord 32]
forall a. SymVal a => Int -> [Char] -> SBVCodeGen [SBV a]
cgInputArr Int
xk [Char]
"xkey"
[Char] -> [SWord 32] -> SBVCodeGen ()
forall a. SymVal a => [Char] -> [SBV a] -> SBVCodeGen ()
cgOutputArr [Char]
"pt" ([SWord 32] -> SBVCodeGen ()) -> [SWord 32] -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ [SWord 32] -> KS -> [SWord 32]
aesDecryptUnwoundKey [SWord 32]
ct ([SWord 32] -> KS
xkeyToKS [SWord 32]
xkey)
xkeyToKS :: [SWord 32] -> KS
xkeyToKS :: [SWord 32] -> KS
xkeyToKS [SWord 32]
xs = ([SWord 32]
f, [[SWord 32]]
m, [SWord 32]
l)
where f :: [SWord 32]
f = Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take Int
4 [SWord 32]
xs
m :: [[SWord 32]]
m = [SWord 32] -> [[SWord 32]]
forall a. [a] -> [[a]]
chop4 (Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
take (Int
xk Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
8) (Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
drop Int
4 [SWord 32]
xs))
l :: [SWord 32]
l = Int -> [SWord 32] -> [SWord 32]
forall a. Int -> [a] -> [a]
drop (Int
xk Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
4) [SWord 32]
xs
ksToXKey :: KS -> [SWord 32]
ksToXKey :: KS -> [SWord 32]
ksToXKey ([SWord 32]
f, [[SWord 32]]
m, [SWord 32]
l) = [SWord 32]
f [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [[SWord 32]] -> [SWord 32]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[SWord 32]]
m [SWord 32] -> [SWord 32] -> [SWord 32]
forall a. [a] -> [a] -> [a]
++ [SWord 32]
l
cgAESLibrary :: Int -> Maybe FilePath -> IO ()
cgAESLibrary :: Int -> Maybe [Char] -> IO ()
cgAESLibrary Int
sz Maybe [Char]
mbd
| Int
sz Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
128, Int
192, Int
256] = IO [()] -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO [()] -> IO ()) -> IO [()] -> IO ()
forall a b. (a -> b) -> a -> b
$ Maybe [Char] -> [Char] -> [([Char], SBVCodeGen ())] -> IO [()]
forall a.
Maybe [Char] -> [Char] -> [([Char], SBVCodeGen a)] -> IO [a]
compileToCLib Maybe [Char]
mbd [Char]
nm [([Char]
fnm, [Integer] -> SBVCodeGen () -> SBVCodeGen ()
forall {b}. [Integer] -> SBVCodeGen b -> SBVCodeGen b
configure [Integer]
dvals SBVCodeGen ()
f) | ([Char]
fnm, [Integer]
dvals, SBVCodeGen ()
f) <- Int -> [([Char], [Integer], SBVCodeGen ())]
aesLibComponents Int
sz]
| Bool
True = [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"cgAESLibrary: Size must be one of 128, 192, or 256, received: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz
where nm :: [Char]
nm = [Char]
"aes" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
sz [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Lib"
configure :: [Integer] -> SBVCodeGen b -> SBVCodeGen b
configure [Integer]
dvals SBVCodeGen b
code = [Integer] -> SBVCodeGen ()
cgSetDriverValues [Integer]
dvals SBVCodeGen () -> SBVCodeGen b -> SBVCodeGen b
forall a b. SBVCodeGen a -> SBVCodeGen b -> SBVCodeGen b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBVCodeGen b
code
cgAES128Library :: IO ()
cgAES128Library :: IO ()
cgAES128Library = Int -> Maybe [Char] -> IO ()
cgAESLibrary Int
128 Maybe [Char]
forall a. Maybe a
Nothing
hex8 :: (SymVal a, Show a, Integral a) => SBV a -> String
hex8 :: forall a. (SymVal a, Show a, Integral a) => SBV a -> [Char]
hex8 SBV a
v = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate (Int
8 Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
s) Char
'0' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s
where s :: [Char]
s = (a -> [Char] -> [Char]) -> [Char] -> a -> [Char]
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> [Char] -> [Char]
forall a. Integral a => a -> [Char] -> [Char]
showHex [Char]
"" (a -> [Char]) -> (SBV a -> a) -> SBV a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> (SBV a -> Maybe a) -> SBV a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV a -> [Char]) -> SBV a -> [Char]
forall a b. (a -> b) -> a -> b
$ SBV a
v
chop4 :: [a] -> [[a]]
chop4 :: forall a. [a] -> [[a]]
chop4 [] = []
chop4 [a]
xs = let ([a]
f, [a]
r) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
4 [a]
xs in [a]
f [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [[a]]
forall a. [a] -> [[a]]
chop4 [a]
r