/*
 * Copyright (c) 2013-2016 Galois, Inc.
 * Distributed under the terms of the BSD3 license (see LICENSE file)
 */

/* Cryptol specification of the Speck block cipher
 * Author: David Lazar
 */

///////////////////////////////////////////////////////////////////////
// parameters
///////////////////////////////////////////////////////////////////////

Speck32_64    = encrypt`{n = 16, m = 4, T = 22}
Speck48_72    = encrypt`{n = 24, m = 3, T = 22}
Speck48_96    = encrypt`{n = 24, m = 4, T = 23}
Speck64_96    = encrypt`{n = 32, m = 3, T = 26}
Speck64_128   = encrypt`{n = 32, m = 4, T = 27}
Speck96_96    = encrypt`{n = 48, m = 2, T = 28}
Speck96_144   = encrypt`{n = 48, m = 3, T = 29}
Speck128_128  = encrypt`{n = 64, m = 2, T = 32}
Speck128_192  = encrypt`{n = 64, m = 3, T = 33}
Speck128_256  = encrypt`{n = 64, m = 4, T = 34}

Speck32_64'   = decrypt`{n = 16, m = 4, T = 22}
Speck48_72'   = decrypt`{n = 24, m = 3, T = 22}
Speck48_96'   = decrypt`{n = 24, m = 4, T = 23}
Speck64_96'   = decrypt`{n = 32, m = 3, T = 26}
Speck64_128'  = decrypt`{n = 32, m = 4, T = 27}
Speck96_96'   = decrypt`{n = 48, m = 2, T = 28}
Speck96_144'  = decrypt`{n = 48, m = 3, T = 29}
Speck128_128' = decrypt`{n = 64, m = 2, T = 32}
Speck128_192' = decrypt`{n = 64, m = 3, T = 33}
Speck128_256' = decrypt`{n = 64, m = 4, T = 34}

// check only a few of them for now
property correctSpeck32_64 (k, b) = Speck32_64' k (Speck32_64 k b) == b
property correctSpeck64_96 (k, b) = Speck64_96' k (Speck64_96 k b) == b
property correctSpeck96_144 (k, b) = Speck96_144' k (Speck96_144 k b) == b
property correctSpeck128_128 (k, b) = Speck128_128' k (Speck128_128 k b) == b
property correctSpeck128_256 (k, b) = Speck128_256' k (Speck128_256 k b) == b


///////////////////////////////////////////////////////////////////////
// round function
///////////////////////////////////////////////////////////////////////

R : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
R k (x, y) = f2 (f1 k (x, y))

R' : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
R' k (x, y) = ((x ^ k) - z <<< (if `n == 16 then 7 else 8), z)
  where z = (x ^ y) >>> (if `n == 16 then 2 else 3)

f1 : {n} (fin n) => [n] -> ([n], [n]) -> ([n], [n])
f1 k (x, y) = (y, (x >>> (if `n == 16 then 7 else 8)) + y ^ k)

f2 : {n} (fin n) => ([n], [n]) -> ([n], [n])
f2 (x, y) = (y, x <<< (if `n == 16 then 2 else 3) ^ y)


///////////////////////////////////////////////////////////////////////
// encryption / decryption
///////////////////////////////////////////////////////////////////////

encrypt : {n, m, T}
    ( fin n, fin m, fin T
    , m >= 2, T >= 2, n >= 2
    , n >= width (T-2)
    ) => [m][n] -> ([n], [n]) -> ([n], [n])
encrypt k0 b0 = bs ! 0
  where
    bs = [b0] # [R k b | b <- bs | k <- ks]
    ks = expandKey`{n = n, m = m, T = T} (reverse k0)


decrypt : {n, m, T}
    ( fin n, fin m, fin T
    , m >= 2, T >= 2, n >= 2
    , n >= width (T-2)
    ) => [m][n] -> ([n], [n]) -> ([n], [n])
decrypt k0 b0 = bs ! 0
  where
    bs = [b0] # [R' k b | b <- bs | k <- reverse ks]
    ks = expandKey`{n = n, m = m, T = T} (reverse k0)


///////////////////////////////////////////////////////////////////////
// key expansion
///////////////////////////////////////////////////////////////////////

expandKey : {n, m, T}
    ( fin n, fin m, fin T
    , m >= 2, n >= 2, T >= 2
    , n >= width (T-2)
    ) => [m][n] -> [T][n]
expandKey K = ks
  where
    ls = drop`{1} K # [snd (f1 i (l, k)) | l <- ls | k <- ks | i <- [0 .. T - 2]]
    ks = take`{1} K # [snd (f2 (k, l)) | l <- drop`{m - 1} ls | k <- ks]
    snd (x, y) = y


///////////////////////////////////////////////////////////////////////
// tests
///////////////////////////////////////////////////////////////////////

property testsPass = tests == ~zero

tests = [t01, t02, t03, t04, t05, t06, t07, t08, t09]

t00 = Speck32_64 [0x1918, 0x1110, 0x0908, 0x0100] (0x6574, 0x694C) == (0xA868, 0x42F2)
t01 = Speck48_72 [0x121110, 0x0A0908, 0x020100] (0x20796C, 0x6C6172) == (0xC049A5, 0x385ADC)
t02 = Speck48_96 [0x1A1918, 0x121110, 0x0A0908, 0x020100] (0x6D2073, 0x696874) == (0x735E10, 0xB6445D)
t03 = Speck64_96 [0x13121110, 0x0B0A0908, 0x03020100] (0x74614620, 0x736E6165) == (0x9F7952EC, 0x4175946C)
t04 = Speck64_128 [0x1B1A1918, 0x13121110, 0x0B0A0908, 0x03020100] (0x3B726574, 0x7475432D) == (0x8C6FA548, 0x454E028B)
t05 = Speck96_96 [0x0D0C0B0A0908, 0x050403020100] (0x65776F68202C, 0x656761737520) == (0x9E4D09AB7178, 0x62BDDE8F79AA)
t06 = Speck96_144 [0x151413121110, 0x0D0C0B0A0908, 0x050403020100] (0x656D6974206E, 0x69202C726576) == (0x2BF31072228A, 0x7AE440252EE6)
t07 = Speck128_128 [0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x6C61766975716520, 0x7469206564616D20) == (0xA65D985179783265, 0x7860FEDF5C570D18)
t08 = Speck128_192 [0x1716151413121110, 0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x7261482066656968, 0x43206F7420746E65) == (0x1BE4CF3A13135566, 0xF9BC185DE03C1886)
t09 = Speck128_256 [0x1F1E1D1C1B1A1918, 0x1716151413121110, 0x0F0E0D0C0B0A0908, 0x0706050403020100] (0x65736F6874206E49, 0x202E72656E6F6F70) == (0x4109010405C0F53E, 0x4EEEB48D9C188F43)