I'm already new to Haskell with Cryptol dialect, also I'm irritated because I can't use loops... I would like to implement array like this one... Initialization Matrix but I have the only idea to get every 4th element starting by [0] index and load this new list to S0. Similarly starting by 1 index of the list and load to new S1 array every 4th element.
Cryptol's type system is designed so that these sorts of bit splits that you find in crypto algorithms is almost trivial to express. And in fact, lack of loops is a plus, not a detriment, once you get used to that style.
There could be multiple ways to code your "initialization" code. But here's how I would go about it:
load : {a} [128][a] -> [4][32][a]
load(elts) = reverse (transpose cols)
where cols : [32][4][a]
cols = split elts
Note that the type here is more general than what you need, but it allows for easier testing. Here's what I get at the cryptol prompt:
Main> :set base=10
Main> load [127, 126 .. 0]
Showing a specific instance of polymorphic result:
* Using '7' for type argument 'a' of 'Main::load'
[[124, 120, 116, 112, 108, 104, 100, 96, 92, 88, 84, 80, 76, 72,
68, 64, 60, 56, 52, 48, 44, 40, 36, 32, 28, 24, 20, 16, 12, 8, 4,
0],
[125, 121, 117, 113, 109, 105, 101, 97, 93, 89, 85, 81, 77, 73, 69,
65, 61, 57, 53, 49, 45, 41, 37, 33, 29, 25, 21, 17, 13, 9, 5, 1],
[126, 122, 118, 114, 110, 106, 102, 98, 94, 90, 86, 82, 78, 74, 70,
66, 62, 58, 54, 50, 46, 42, 38, 34, 30, 26, 22, 18, 14, 10, 6, 2],
[127, 123, 119, 115, 111, 107, 103, 99, 95, 91, 87, 83, 79, 75, 71,
67, 63, 59, 55, 51, 47, 43, 39, 35, 31, 27, 23, 19, 15, 11, 7, 3]]
This is a little hard to read, so here it is formatted:
[[124, 120, 116, 112, 108, 104, 100, 96, 92, 88, 84, 80, 76, 72, 68, 64, 60, 56, 52, 48, 44, 40, 36, 32, 28, 24, 20, 16, 12, 8, 4, 0],
[125, 121, 117, 113, 109, 105, 101, 97, 93, 89, 85, 81, 77, 73, 69, 65, 61, 57, 53, 49, 45, 41, 37, 33, 29, 25, 21, 17, 13, 9, 5, 1],
[126, 122, 118, 114, 110, 106, 102, 98, 94, 90, 86, 82, 78, 74, 70, 66, 62, 58, 54, 50, 46, 42, 38, 34, 30, 26, 22, 18, 14, 10, 6, 2],
[127, 123, 119, 115, 111, 107, 103, 99, 95, 91, 87, 83, 79, 75, 71, 67, 63, 59, 55, 51, 47, 43, 39, 35, 31, 27, 23, 19, 15, 11, 7, 3]]
which is exactly the structure you wanted. Now we can specialize:
loadBits : [128] -> [4][32]
loadBits(vector) = reverse (transpose cols)
where cols : [32][4]
cols = split vector
Note that the code is exactly the same as before, we just made it specific to the type you wanted.
Hope this gets you started!