{-# LANGUAGE DataKinds #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Documentation.SBV.Examples.Crypto.SHA where
import Data.SBV
import Data.SBV.Tools.CodeGen
import Data.Char (ord, toLower)
import Data.List (genericLength)
import Numeric (showHex)
import Data.Proxy (Proxy(..))
data SHA w = SHA { SHA w -> Int
wordSize :: Int
, SHA w -> Int
blockSize :: Int
, SHA w -> (Int, Int, Int)
sum0Coefficients :: (Int, Int, Int)
, SHA w -> (Int, Int, Int)
sum1Coefficients :: (Int, Int, Int)
, SHA w -> (Int, Int, Int)
sigma0Coefficients :: (Int, Int, Int)
, SHA w -> (Int, Int, Int)
sigma1Coefficients :: (Int, Int, Int)
, SHA w -> [w]
shaConstants :: [w]
, SHA w -> [w]
h0 :: [w]
, SHA w -> Int
shaLoopCount :: Int
}
ch :: Bits a => a -> a -> a -> a
ch :: a -> a -> a -> a
ch x :: a
x y :: a
y z :: a
z = (a
x a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
y) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a -> a
forall a. Bits a => a -> a
complement a
x a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
z)
maj :: Bits a => a -> a -> a -> a
maj :: a -> a -> a -> a
maj x :: a
x y :: a
y z :: a
z = (a
x a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
y) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
z) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
y a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
z)
sum0 :: Bits a => SHA w -> a -> a
sum0 :: SHA w -> a -> a
sum0 SHA{sum0Coefficients :: forall w. SHA w -> (Int, Int, Int)
sum0Coefficients = (a :: Int
a, b :: Int
b, c :: Int
c)} x :: a
x = (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
a) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
b) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
c)
sum1 :: Bits a => SHA w -> a -> a
sum1 :: SHA w -> a -> a
sum1 SHA{sum1Coefficients :: forall w. SHA w -> (Int, Int, Int)
sum1Coefficients = (a :: Int
a, b :: Int
b, c :: Int
c)} x :: a
x = (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
a) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
b) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
c)
sigma0 :: Bits a => SHA w -> a -> a
sigma0 :: SHA w -> a -> a
sigma0 SHA{sigma0Coefficients :: forall w. SHA w -> (Int, Int, Int)
sigma0Coefficients = (a :: Int
a, b :: Int
b, c :: Int
c)} x :: a
x = (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
a) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
b) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`shiftR` Int
c)
sigma1 :: Bits a => SHA w -> a -> a
sigma1 :: SHA w -> a -> a
sigma1 SHA{sigma1Coefficients :: forall w. SHA w -> (Int, Int, Int)
sigma1Coefficients = (a :: Int
a, b :: Int
b, c :: Int
c)} x :: a
x = (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
a) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`rotateR` Int
b) a -> a -> a
forall a. Bits a => a -> a -> a
`xor` (a
x a -> Int -> a
forall a. Bits a => a -> Int -> a
`shiftR` Int
c)
sha224P :: SHA (SWord 32)
sha224P :: SHA (SWord 32)
sha224P = SHA :: forall w.
Int
-> Int
-> (Int, Int, Int)
-> (Int, Int, Int)
-> (Int, Int, Int)
-> (Int, Int, Int)
-> [w]
-> [w]
-> Int
-> SHA w
SHA { wordSize :: Int
wordSize = 32
, blockSize :: Int
blockSize = 512
, sum0Coefficients :: (Int, Int, Int)
sum0Coefficients = ( 2, 13, 22)
, sum1Coefficients :: (Int, Int, Int)
sum1Coefficients = ( 6, 11, 25)
, sigma0Coefficients :: (Int, Int, Int)
sigma0Coefficients = ( 7, 18, 3)
, sigma1Coefficients :: (Int, Int, Int)
sigma1Coefficients = (17, 19, 10)
, shaConstants :: [SWord 32]
shaConstants = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5
, 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174
, 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da
, 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967
, 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85
, 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070
, 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3
, 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
]
, h0 :: [SWord 32]
h0 = [ 0xc1059ed8, 0x367cd507, 0x3070dd17, 0xf70e5939
, 0xffc00b31, 0x68581511, 0x64f98fa7, 0xbefa4fa4
]
, shaLoopCount :: Int
shaLoopCount = 64
}
sha256P :: SHA (SWord 32)
sha256P :: SHA (SWord 32)
sha256P = SHA (SWord 32)
sha224P { h0 :: [SWord 32]
h0 = [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a
, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19
]
}
sha384P :: SHA (SWord 64)
sha384P :: SHA (SWord 64)
sha384P = SHA :: forall w.
Int
-> Int
-> (Int, Int, Int)
-> (Int, Int, Int)
-> (Int, Int, Int)
-> (Int, Int, Int)
-> [w]
-> [w]
-> Int
-> SHA w
SHA { wordSize :: Int
wordSize = 64
, blockSize :: Int
blockSize = 1024
, sum0Coefficients :: (Int, Int, Int)
sum0Coefficients = (28, 34, 39)
, sum1Coefficients :: (Int, Int, Int)
sum1Coefficients = (14, 18, 41)
, sigma0Coefficients :: (Int, Int, Int)
sigma0Coefficients = ( 1, 8, 7)
, sigma1Coefficients :: (Int, Int, Int)
sigma1Coefficients = (19, 61, 6)
, shaConstants :: [SWord 64]
shaConstants = [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc
, 0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118
, 0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2
, 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694
, 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65
, 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5
, 0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4
, 0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70
, 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df
, 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b
, 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30
, 0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8
, 0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8
, 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3
, 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec
, 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b
, 0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178
, 0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b
, 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c
, 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817
]
, h0 :: [SWord 64]
h0 = [ 0xcbbb9d5dc1059ed8, 0x629a292a367cd507, 0x9159015a3070dd17, 0x152fecd8f70e5939
, 0x67332667ffc00b31, 0x8eb44a8768581511, 0xdb0c2e0d64f98fa7, 0x47b5481dbefa4fa4
]
, shaLoopCount :: Int
shaLoopCount = 80
}
sha512P :: SHA (SWord 64)
sha512P :: SHA (SWord 64)
sha512P = SHA (SWord 64)
sha384P { h0 :: [SWord 64]
h0 = [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1
, 0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179
]
}
sha512_224P :: SHA (SWord 64)
sha512_224P :: SHA (SWord 64)
sha512_224P = SHA (SWord 64)
sha512P { h0 :: [SWord 64]
h0 = [ 0x8C3D37C819544DA2, 0x73E1996689DCD4D6, 0x1DFAB7AE32FF9C82, 0x679DD514582F9FCF
, 0x0F6D2B697BD44DA8, 0x77E36F7304C48942, 0x3F9D85A86A1D36C8, 0x1112E6AD91D692A1
]
}
sha512_256P :: SHA (SWord 64)
sha512_256P :: SHA (SWord 64)
sha512_256P = SHA (SWord 64)
sha512P { h0 :: [SWord 64]
h0 = [ 0x22312194FC2BF72C, 0x9F555FA3C84C64C2, 0x2393B86B6F53B151, 0x963877195940EABD
, 0x96283EE2A88EFFE3, 0xBE5E1E2553863992, 0x2B0199FC2C85B8AA, 0x0EB72DDC81C52CA2
]
}
newtype Block a = Block [a]
prepareMessage :: forall w. (Num w, ByteConverter w) => SHA w -> String -> [Block w]
prepareMessage :: SHA w -> String -> [Block w]
prepareMessage SHA{Int
wordSize :: Int
wordSize :: forall w. SHA w -> Int
wordSize, Int
blockSize :: Int
blockSize :: forall w. SHA w -> Int
blockSize} s :: String
s
| Integer
msgLen Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
maxLen
= String -> [Block w]
forall a. HasCallStack => String -> a
error (String -> [Block w]) -> String -> [Block w]
forall a b. (a -> b) -> a -> b
$ "Message is too big! Size: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
msgLen String -> String -> String
forall a. [a] -> [a] -> [a]
++ " Max: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
maxLen
| Bool
True
= [w] -> [Block w]
forall a. [a] -> [Block a]
parse ([w] -> [Block w]) -> [w] -> [Block w]
forall a b. (a -> b) -> a -> b
$ Int -> ([SWord 8] -> w) -> [SWord 8] -> [w]
forall a b. Int -> ([a] -> b) -> [a] -> [b]
chunkBy (Int
wordSize Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 8) [SWord 8] -> w
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
padded
where
maxLen :: Integer
maxLen :: Integer
maxLen = 2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(2Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
wordSize :: Integer)
msgLen :: Integer
msgLen :: Integer
msgLen = 8 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* String -> Integer
forall i a. Num i => [a] -> i
genericLength String
s
parse :: [a] -> [Block a]
parse = Int -> ([a] -> Block a) -> [a] -> [Block a]
forall a b. Int -> ([a] -> b) -> [a] -> [b]
chunkBy 16 [a] -> Block a
forall a. [a] -> Block a
Block
msgSizeAsBytes :: [SWord 8]
msgSizeAsBytes :: [SWord 8]
msgSizeAsBytes
| Int
wordSize Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 32 = SWord 64 -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes (Integer -> SWord 64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
msgLen :: SWord 64)
| Int
wordSize Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 64 = SWord 128 -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes (Integer -> SWord 128
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
msgLen :: SWord 128)
| Bool
True = String -> [SWord 8]
forall a. HasCallStack => String -> a
error (String -> [SWord 8]) -> String -> [SWord 8]
forall a b. (a -> b) -> a -> b
$ "prepareMessage: Unexpected word size: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
wordSize
kLen :: Int
kLen :: Int
kLen = Int
blockSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ((Integer
msgLen Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
wordSize)) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
blockSize)
padded :: [SWord 8]
padded :: [SWord 8]
padded = (Char -> SWord 8) -> String -> [SWord 8]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> SWord 8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> SWord 8) -> (Char -> Int) -> Char -> SWord 8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord) String
s [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. [a] -> [a] -> [a]
++ [0x80] [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. [a] -> [a] -> [a]
++ Int -> SWord 8 -> [SWord 8]
forall a. Int -> a -> [a]
replicate ((Int
kLen Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 8) Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) 0 [SWord 8] -> [SWord 8] -> [SWord 8]
forall a. [a] -> [a] -> [a]
++ [SWord 8]
msgSizeAsBytes
hashBlock :: (Num w, Bits w) => SHA w -> [w] -> Block w -> [w]
hashBlock :: SHA w -> [w] -> Block w -> [w]
hashBlock p :: SHA w
p@SHA{Int
shaLoopCount :: Int
shaLoopCount :: forall w. SHA w -> Int
shaLoopCount, [w]
shaConstants :: [w]
shaConstants :: forall w. SHA w -> [w]
shaConstants} hPrev :: [w]
hPrev (Block m :: [w]
m) = [w]
step4
where lim :: Int
lim = Int
shaLoopCount Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1
w :: Int -> w
w t :: Int
t
| 0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
t Bool -> Bool -> Bool
&& Int
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 15 = [w]
m [w] -> Int -> w
forall a. [a] -> Int -> a
!! Int
t
| 16 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
t Bool -> Bool -> Bool
&& Int
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lim = SHA w -> w -> w
forall a w. Bits a => SHA w -> a -> a
sigma1 SHA w
p (Int -> w
w (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
-2)) w -> w -> w
forall a. Num a => a -> a -> a
+ Int -> w
w (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
-7) w -> w -> w
forall a. Num a => a -> a -> a
+ SHA w -> w -> w
forall a w. Bits a => SHA w -> a -> a
sigma0 SHA w
p (Int -> w
w (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
-15)) w -> w -> w
forall a. Num a => a -> a -> a
+ Int -> w
w (Int
tInt -> Int -> Int
forall a. Num a => a -> a -> a
-16)
| Bool
True = String -> w
forall a. HasCallStack => String -> a
error (String -> w) -> String -> w
forall a b. (a -> b) -> a -> b
$ "hashBlock, unexpected t: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
t
step3Body :: [w] -> Int -> [w]
step3Body [a :: w
a, b :: w
b, c :: w
c, d :: w
d, e :: w
e, f :: w
f, g :: w
g, h :: w
h] t :: Int
t = [w
t1 w -> w -> w
forall a. Num a => a -> a -> a
+ w
t2, w
a, w
b, w
c, w
d w -> w -> w
forall a. Num a => a -> a -> a
+ w
t1, w
e, w
f, w
g]
where t1 :: w
t1 = w
h w -> w -> w
forall a. Num a => a -> a -> a
+ SHA w -> w -> w
forall a w. Bits a => SHA w -> a -> a
sum1 SHA w
p w
e w -> w -> w
forall a. Num a => a -> a -> a
+ w -> w -> w -> w
forall a. Bits a => a -> a -> a -> a
ch w
e w
f w
g w -> w -> w
forall a. Num a => a -> a -> a
+ [w]
shaConstants [w] -> Int -> w
forall a. [a] -> Int -> a
!! Int
t w -> w -> w
forall a. Num a => a -> a -> a
+ Int -> w
w Int
t
t2 :: w
t2 = SHA w -> w -> w
forall a w. Bits a => SHA w -> a -> a
sum0 SHA w
p w
a w -> w -> w
forall a. Num a => a -> a -> a
+ w -> w -> w -> w
forall a. Bits a => a -> a -> a -> a
maj w
a w
b w
c
step3Body xs :: [w]
xs t :: Int
t = String -> [w]
forall a. HasCallStack => String -> a
error (String -> [w]) -> String -> [w]
forall a b. (a -> b) -> a -> b
$ "Impossible! step3Body received a list of length " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([w] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [w]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", iteration: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
t
step3 :: [w]
step3 = ([w] -> Int -> [w]) -> [w] -> [Int] -> [w]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [w] -> Int -> [w]
step3Body [w]
hPrev [0 .. Int
lim]
step4 :: [w]
step4 = (w -> w -> w) -> [w] -> [w] -> [w]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith w -> w -> w
forall a. Num a => a -> a -> a
(+) [w]
step3 [w]
hPrev
shaP :: (Num w, Bits w, ByteConverter w) => SHA w -> String -> [w]
shaP :: SHA w -> String -> [w]
shaP p :: SHA w
p@SHA{[w]
h0 :: [w]
h0 :: forall w. SHA w -> [w]
h0} = ([w] -> Block w -> [w]) -> [w] -> [Block w] -> [w]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (SHA w -> [w] -> Block w -> [w]
forall w. (Num w, Bits w) => SHA w -> [w] -> Block w -> [w]
hashBlock SHA w
p) [w]
h0 ([Block w] -> [w]) -> (String -> [Block w]) -> String -> [w]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SHA w -> String -> [Block w]
forall w. (Num w, ByteConverter w) => SHA w -> String -> [Block w]
prepareMessage SHA w
p
sha224 :: String -> SWord 224
sha224 :: String -> SWord 224
sha224 s :: String
s = SWord 32
h0 SWord 32 -> SBV (WordN 192) -> SBV (WordN (32 + 192))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h1 SWord 32 -> SBV (WordN 160) -> SBV (WordN (32 + 160))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h2 SWord 32 -> SWord 128 -> SBV (WordN (32 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h3 SWord 32 -> SBV (WordN 96) -> SBV (WordN (32 + 96))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h4 SWord 32 -> SWord 64 -> SBV (WordN (32 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h5 SWord 32 -> SWord 32 -> SBV (WordN (32 + 32))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h6
where [h0 :: SWord 32
h0, h1 :: SWord 32
h1, h2 :: SWord 32
h2, h3 :: SWord 32
h3, h4 :: SWord 32
h4, h5 :: SWord 32
h5, h6 :: SWord 32
h6, _] = SHA (SWord 32) -> String -> [SWord 32]
forall w.
(Num w, Bits w, ByteConverter w) =>
SHA w -> String -> [w]
shaP SHA (SWord 32)
sha224P String
s
sha256 :: String -> SWord 256
sha256 :: String -> SWord 256
sha256 s :: String
s = SWord 32
h0 SWord 32 -> SWord 224 -> SBV (WordN (32 + 224))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h1 SWord 32 -> SBV (WordN 192) -> SBV (WordN (32 + 192))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h2 SWord 32 -> SBV (WordN 160) -> SBV (WordN (32 + 160))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h3 SWord 32 -> SWord 128 -> SBV (WordN (32 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h4 SWord 32 -> SBV (WordN 96) -> SBV (WordN (32 + 96))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h5 SWord 32 -> SWord 64 -> SBV (WordN (32 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h6 SWord 32 -> SWord 32 -> SBV (WordN (32 + 32))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h7
where [h0 :: SWord 32
h0, h1 :: SWord 32
h1, h2 :: SWord 32
h2, h3 :: SWord 32
h3, h4 :: SWord 32
h4, h5 :: SWord 32
h5, h6 :: SWord 32
h6, h7 :: SWord 32
h7] = SHA (SWord 32) -> String -> [SWord 32]
forall w.
(Num w, Bits w, ByteConverter w) =>
SHA w -> String -> [w]
shaP SHA (SWord 32)
sha256P String
s
sha384 :: String -> SWord 384
sha384 :: String -> SWord 384
sha384 s :: String
s = SWord 64
h0 SWord 64 -> SBV (WordN 320) -> SBV (WordN (64 + 320))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h1 SWord 64 -> SWord 256 -> SBV (WordN (64 + 256))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h2 SWord 64 -> SBV (WordN 192) -> SBV (WordN (64 + 192))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h3 SWord 64 -> SWord 128 -> SBV (WordN (64 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h4 SWord 64 -> SWord 64 -> SBV (WordN (64 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h5
where [h0 :: SWord 64
h0, h1 :: SWord 64
h1, h2 :: SWord 64
h2, h3 :: SWord 64
h3, h4 :: SWord 64
h4, h5 :: SWord 64
h5, _, _] = SHA (SWord 64) -> String -> [SWord 64]
forall w.
(Num w, Bits w, ByteConverter w) =>
SHA w -> String -> [w]
shaP SHA (SWord 64)
sha384P String
s
sha512 :: String -> SWord 512
sha512 :: String -> SWord 512
sha512 s :: String
s = SWord 64
h0 SWord 64 -> SBV (WordN 448) -> SBV (WordN (64 + 448))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h1 SWord 64 -> SWord 384 -> SBV (WordN (64 + 384))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h2 SWord 64 -> SBV (WordN 320) -> SBV (WordN (64 + 320))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h3 SWord 64 -> SWord 256 -> SBV (WordN (64 + 256))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h4 SWord 64 -> SBV (WordN 192) -> SBV (WordN (64 + 192))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h5 SWord 64 -> SWord 128 -> SBV (WordN (64 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h6 SWord 64 -> SWord 64 -> SBV (WordN (64 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h7
where [h0 :: SWord 64
h0, h1 :: SWord 64
h1, h2 :: SWord 64
h2, h3 :: SWord 64
h3, h4 :: SWord 64
h4, h5 :: SWord 64
h5, h6 :: SWord 64
h6, h7 :: SWord 64
h7] = SHA (SWord 64) -> String -> [SWord 64]
forall w.
(Num w, Bits w, ByteConverter w) =>
SHA w -> String -> [w]
shaP SHA (SWord 64)
sha512P String
s
sha512_224 :: String -> SWord 224
sha512_224 :: String -> SWord 224
sha512_224 s :: String
s = SWord 64
h0 SWord 64 -> SBV (WordN 160) -> SBV (WordN (64 + 160))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h1 SWord 64 -> SBV (WordN 96) -> SBV (WordN (64 + 96))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h2 SWord 64 -> SWord 32 -> SBV (WordN (64 + 32))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 32
h3Top
where [h0 :: SWord 64
h0, h1 :: SWord 64
h1, h2 :: SWord 64
h2, h3 :: SWord 64
h3, _, _, _, _] = SHA (SWord 64) -> String -> [SWord 64]
forall w.
(Num w, Bits w, ByteConverter w) =>
SHA w -> String -> [w]
shaP SHA (SWord 64)
sha512_224P String
s
h3Top :: SBV (WordN ((63 - 32) + 1))
h3Top = Proxy 63 -> Proxy 32 -> SWord 64 -> SBV (WordN ((63 - 32) + 1))
forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
(proxy :: Nat -> *).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
(i + 1) <= n, j <= i, IsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract (Proxy 63
forall k (t :: k). Proxy t
Proxy @63) (Proxy 32
forall k (t :: k). Proxy t
Proxy @32) SWord 64
h3
sha512_256 :: String -> SWord 256
sha512_256 :: String -> SWord 256
sha512_256 s :: String
s = SWord 64
h0 SWord 64 -> SBV (WordN 192) -> SBV (WordN (64 + 192))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h1 SWord 64 -> SWord 128 -> SBV (WordN (64 + 128))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h2 SWord 64 -> SWord 64 -> SBV (WordN (64 + 64))
forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, IsNonZero n, SymVal (bv n), KnownNat m, IsNonZero m,
SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SWord 64
h3
where [h0 :: SWord 64
h0, h1 :: SWord 64
h1, h2 :: SWord 64
h2, h3 :: SWord 64
h3, _, _, _, _] = SHA (SWord 64) -> String -> [SWord 64]
forall w.
(Num w, Bits w, ByteConverter w) =>
SHA w -> String -> [w]
shaP SHA (SWord 64)
sha512_256P String
s
knownAnswerTests :: Int -> Bool
knownAnswerTests :: Int -> Bool
knownAnswerTests nTest :: Int
nTest = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [Bool] -> [Bool]
forall a. Int -> [a] -> [a]
take Int
nTest ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ [SWord 224 -> String
forall a. (Show a, Integral a, SymVal a) => SBV a -> String
showHash (String -> SWord 224
sha224 String
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
r | (t :: String
t, r :: String
r) <- [(String, String)]
sha224Kats ]
[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [SWord 256 -> String
forall a. (Show a, Integral a, SymVal a) => SBV a -> String
showHash (String -> SWord 256
sha256 String
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
r | (t :: String
t, r :: String
r) <- [(String, String)]
sha256Kats ]
[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [SWord 384 -> String
forall a. (Show a, Integral a, SymVal a) => SBV a -> String
showHash (String -> SWord 384
sha384 String
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
r | (t :: String
t, r :: String
r) <- [(String, String)]
sha384Kats ]
[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [SWord 512 -> String
forall a. (Show a, Integral a, SymVal a) => SBV a -> String
showHash (String -> SWord 512
sha512 String
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
r | (t :: String
t, r :: String
r) <- [(String, String)]
sha512Kats ]
[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [SWord 224 -> String
forall a. (Show a, Integral a, SymVal a) => SBV a -> String
showHash (String -> SWord 224
sha512_224 String
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
r | (t :: String
t, r :: String
r) <- [(String, String)]
sha512_224Kats]
[Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [SWord 256 -> String
forall a. (Show a, Integral a, SymVal a) => SBV a -> String
showHash (String -> SWord 256
sha512_256 String
t) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
r | (t :: String
t, r :: String
r) <- [(String, String)]
sha512_256Kats]
where
sha224Kats :: [(String, String)]
sha224Kats :: [(String, String)]
sha224Kats = [ ("" , "d14a028c2a3a2bc9476102bb288234c415a2b01f828ea62ac5b3e42f")
, ("a" , "abd37534c7d9a2efb9465de931cd7055ffdb8879563ae98078d6d6d5")
, ("abc" , "23097d223405d8228642a477bda255b32aadbce4bda0b3f7e36c9da7")
, ("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq", "75388b16512776cc5dba5da1fd890150b0c6455cb4f58b1952522525")
]
sha256Kats :: [(String, String)]
sha256Kats :: [(String, String)]
sha256Kats = [ ("" , "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855")
, ("a" , "ca978112ca1bbdcafac231b39a23dc4da786eff8147c4e72b9807785afee48bb")
, ("abc" , "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad")
, ("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq", "248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1")
]
sha384Kats :: [(String, String)]
sha384Kats :: [(String, String)]
sha384Kats = [ ("" , "38b060a751ac96384cd9327eb1b1e36a21fdb71114be07434c0cc7bf63f6e1da274edebfe76f65fbd51ad2f14898b95b")
, ("a" , "54a59b9f22b0b80880d8427e548b7c23abd873486e1f035dce9cd697e85175033caa88e6d57bc35efae0b5afd3145f31")
, ("abc" , "cb00753f45a35e8bb5a03d699ac65007272c32ab0eded1631a8b605a43ff5bed8086072ba1e7cc2358baeca134c825a7")
, ("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu", "09330c33f71147e83d192fc782cd1b4753111b173b3b05d22fa08086e3b0f712fcc7c71a557e2db966c3e9fa91746039")
]
sha512Kats :: [(String, String)]
sha512Kats :: [(String, String)]
sha512Kats = [ ("" , "cf83e1357eefb8bdf1542850d66d8007d620e4050b5715dc83f4a921d36ce9ce47d0d13c5d85f2b0ff8318d2877eec2f63b931bd47417a81a538327af927da3e")
, ("a" , "1f40fc92da241694750979ee6cf582f2d5d7d28e18335de05abc54d0560e0f5302860c652bf08d560252aa5e74210546f369fbbbce8c12cfc7957b2652fe9a75")
, ("abc" , "ddaf35a193617abacc417349ae20413112e6fa4e89a97ea20a9eeee64b55d39a2192992a274fc1a836ba3c23a3feebbd454d4423643ce80e2a9ac94fa54ca49f")
, ("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu", "8e959b75dae313da8cf4f72814fc143f8f7779c6eb9f7fa17299aeadb6889018501d289e4900f7e4331b99dec4b5433ac7d329eeb6dd26545e96e55b874be909")
]
sha512_224Kats :: [(String, String)]
sha512_224Kats :: [(String, String)]
sha512_224Kats = [ ("" , "6ed0dd02806fa89e25de060c19d3ac86cabb87d6a0ddd05c333b84f4")
, ("a" , "d5cdb9ccc769a5121d4175f2bfdd13d6310e0d3d361ea75d82108327")
, ("abc" , "4634270F707B6A54DAAE7530460842E20E37ED265CEEE9A43E8924AA")
, ("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu", "23FEC5BB94D60B23308192640B0C453335D664734FE40E7268674AF9")
]
sha512_256Kats :: [(String, String)]
sha512_256Kats :: [(String, String)]
sha512_256Kats = [ ("" , "c672b8d1ef56ed28ab87c3622c5114069bdd3ad7b8f9737498d0c01ecef0967a")
, ("a" , "455e518824bc0601f9fb858ff5c37d417d67c2f8e0df2babe4808858aea830f8")
, ("abc" , "53048E2681941EF99B2E29B76B4C7DABE4C2D0C634FC6D46E0E2F13107E7AF23")
, ("abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu", "3928E184FB8690F840DA3988121D31BE65CB9D3EF83EE6146FEAC861E19B563A")
]
cgSHA256 :: IO ()
cgSHA256 :: IO ()
cgSHA256 = Maybe String -> String -> SBVCodeGen () -> IO ()
forall a. Maybe String -> String -> SBVCodeGen a -> IO a
compileToC Maybe String
forall a. Maybe a
Nothing "sha256" (SBVCodeGen () -> IO ()) -> SBVCodeGen () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let algorithm :: SHA (SWord 32)
algorithm = SHA (SWord 32)
sha256P
[SWord 8]
hInBytes <- Int -> String -> SBVCodeGen [SWord 8]
forall a. SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr 32 "hIn"
[SWord 8]
blockBytes <- Int -> String -> SBVCodeGen [SWord 8]
forall a. SymVal a => Int -> String -> SBVCodeGen [SBV a]
cgInputArr 64 "block"
let hIn :: [SWord 32]
hIn = Int -> ([SWord 8] -> SWord 32) -> [SWord 8] -> [SWord 32]
forall a b. Int -> ([a] -> b) -> [a] -> [b]
chunkBy 4 [SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
hInBytes
block :: [SWord 32]
block = Int -> ([SWord 8] -> SWord 32) -> [SWord 8] -> [SWord 32]
forall a b. Int -> ([a] -> b) -> [a] -> [b]
chunkBy 4 [SWord 8] -> SWord 32
forall a. ByteConverter a => [SWord 8] -> a
fromBytes [SWord 8]
blockBytes
result :: [SWord 32]
result = SHA (SWord 32) -> [SWord 32] -> Block (SWord 32) -> [SWord 32]
forall w. (Num w, Bits w) => SHA w -> [w] -> Block w -> [w]
hashBlock SHA (SWord 32)
algorithm [SWord 32]
hIn ([SWord 32] -> Block (SWord 32)
forall a. [a] -> Block a
Block [SWord 32]
block)
String -> [SWord 8] -> SBVCodeGen ()
forall a. SymVal a => String -> [SBV a] -> SBVCodeGen ()
cgOutputArr "hash" ([SWord 8] -> SBVCodeGen ()) -> [SWord 8] -> SBVCodeGen ()
forall a b. (a -> b) -> a -> b
$ (SWord 32 -> [SWord 8]) -> [SWord 32] -> [SWord 8]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SWord 32 -> [SWord 8]
forall a. ByteConverter a => a -> [SWord 8]
toBytes [SWord 32]
result
chunkBy :: Int -> ([a] -> b) -> [a] -> [b]
chunkBy :: Int -> ([a] -> b) -> [a] -> [b]
chunkBy i :: Int
i f :: [a] -> b
f = [a] -> [b]
go
where go :: [a] -> [b]
go [] = []
go xs :: [a]
xs
| [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
first Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i = String -> [b]
forall a. HasCallStack => String -> a
error (String -> [b]) -> String -> [b]
forall a b. (a -> b) -> a -> b
$ "chunkBy: Not a multiple of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
first)
| Bool
True = [a] -> b
f [a]
first b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [b]
go [a]
rest
where (first :: [a]
first, rest :: [a]
rest) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i [a]
xs
showHash :: (Show a, Integral a, SymVal a) => SBV a -> String
showHash :: SBV a -> String
showHash x :: SBV a
x = case (SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
x, SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
x) of
(KBounded False n :: Int
n, Just v :: a
v) -> Int -> String -> String
pad (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` 4) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
showHex a
v ""
_ -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "Impossible happened: Unexpected hash value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
x
where pad :: Int -> String -> String
pad l :: Int
l s :: String
s = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
l (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
reverse String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat '0'