/* Source:
Alexander Semenov
Institute for System Dynamics and Control Theory
Russian Academy of Sciences
*/

Trivium_stream : [93] -> [84] -> [111] -> [inf]
Trivium_stream R1 R2 R3 = stream
	where
	(stream, ra, rb, rc) = shift_regs R1 R2 R3

type N = 300
Trivium : ([93], [84], [111]) -> [N]Bit
Trivium (reg1, reg2, reg3) = keystream
  where
    keystream =  take`{N} (Trivium_stream reg1 reg2 reg3)

shift : {d} (fin d, d >=1) => [d] -> Bit -> [d]
shift fill bit = fills
	where
		fills = [bit]#(drop`{1} (fill >> 1))


shift_regs : {d,e,f} (fin d, fin e, fin f, d >=1, e >=1, f>=1) => [d] -> [e] -> [f] -> ([inf],[inf][d],[inf][e],[inf][f])
shift_regs r1 r2 r3 = (stream, regA, regB, regC)
	where

		s1 = [(f1 @ 65) ^ (f1 @ 92)  | f1 <- regA]
		s2 = [(f2 @ 68) ^ (f2 @ 83)  | f2 <- regB]
		s3 = [(f3 @ 65) ^ (f3 @ 110) | f3 <- regC]

		stream = s1 ^ s2 ^ s3
		t1 = [(f1 @ 65) ^ ((f1 @ 90) && (f1 @ 91)) ^ (f1 @ 92) ^ (f2 @ 77) |
				f2 <- regB |
				f1 <- regA ]
		t2 = [(f2 @ 68) ^ ((f2 @ 81) && (f2 @ 82)) ^ (f2 @ 83) ^ (f3 @ 86) |
				f2 <- regB |
				f3 <- regC ]
		t3 = [(f3 @ 65) ^ ((f3 @ 108) && (f3 @ 109)) ^ (f3 @ 110) ^ (f1 @ 68)|
				f1 <- regA |
				f3 <- regC ]

		regA = [r1] # [shift f b| f <- regA | b <- t3]
		regB = [r2] # [shift f b| f <- regB | b <- t1]
		regC = [r3] # [shift f b| f <- regC | b <- t2]

Trivium_alt : ([93], [84], [111]) -> [N]Bit
Trivium_alt (r1, r2, r3) = take`{N} (s1 ^ s2 ^ s3)
  where
    a_65 = drop`{27} a_92
    a_68 = drop`{24} a_92
    a_90 = drop`{2} a_92
    a_91 = drop`{1} a_92
    a_92 = reverse r1 # t3

    b_68 = drop`{15} b_83
    b_77 = drop`{6} b_83
    b_81 = drop`{2} b_83
    b_82 = drop`{1} b_83
    b_83 = reverse r2 # t1

    c_65 = drop`{45} c_110
    c_86 = drop`{24} c_110
    c_108 = drop`{2} c_110
    c_109 = drop`{1} c_110
    c_110 = reverse r3 # t2

    s1 = a_65 ^ a_92
    s2 = b_68 ^ b_83
    s3 = c_65 ^ c_110

    t1 = s1 ^ (a_90 && a_91) ^ b_77
    t2 = s2 ^ (b_81 && b_82) ^ c_86
    t3 = s3 ^ (c_108 && c_109) ^ a_68

/*********************************************************/

iv1 = 0b111111111111111111101111111111111111111011111111111111111110111111111111111111101111111111111
iv2 = 0b000000000000000000001000000000000000000001000000000000000000001000000000000000000001
iv3 = 0b111111111111111110111111111111111111101111111111111111111011111111111111111110111111111111100000000000000000000

test_keystream = 0b011111110111101111110100001110000000000000100010000000000000000100011000101100001110001011011010101010000100101110001111100011000110000101001011001111011101110110111010011011010110001000111101101111101100101001000111010001010011111110011100100011101010011110101001001000011100001111111100000001110001

property Trivium_correct = (Trivium(iv1, iv2, iv3)) == test_keystream
property Trivium_search (x, y, z) = (Trivium(x, y, z)) == test_keystream
property Trivium_alt_correct = (Trivium_alt(iv1, iv2, iv3)) == test_keystream
property Trivium_alt_equivalent x = take`{200}(Trivium_alt x) == take (Trivium x)