Standard library API

Every module of flang/stdlib/ and every one of its functions, exactly as the source writes them: the signature, the требует preconditions, the обеспечивает guarantees and the first пример of the function. The body is not shown: to call a function you need what it accepts, what it returns and what it promises. In flang the contract is the documentation of a function, so there is no retelling here, only the lines of the source themselves. The library is written in Russian, and so are its names.

Which module fits a task and how to import it: Library reference.

How to read the page

Under the heading of a module stand its file, the number of its functions and the state of the kernel ledger. The ledger is what flang check --proof prints for the module: how the termination of every function is proved and what the kernel said about every guarantee. It is taken by bootstrap/flang run-script docs:library-status, one module at a time with a time limit per module, and is kept in docs/site/library-status.tsv together with the SHA-256 digest of the module text it was taken from.

The status table under a module is printed only while the digest agrees with the present text of the file. A module changed after the measurement gets no table, and the line under the heading says the ledger was taken from another version of the file: an old status is never shown as the present one.

Modules

«AES»

flang/stdlib/aes.flang — functions 105; the kernel ledger was taken from this version of the file

тип «Ход шифра»
  вариант «Ход шифра» содержит расширение: список числа, квадрат: список числа

тип «Ход счёта»
  вариант «Ход счёта» содержит перенос: число, байты: список числа

тип «Ход гаммы»
  вариант «Ход гаммы» содержит расширение: список числа, счётчик: список числа, гамма: список числа, позиция: число, выход: список числа

тип «Ход поля»
  вариант «Ход поля» содержит накоплено: список числа, сдвиг: список числа

тип «Ход сдвига»
  вариант «Ход сдвига» содержит прежний: число, байты: список числа

тип «Ход GHASH»
  вариант «Ход GHASH» содержит ключ: список числа, свод: список числа, буфер: список числа, набрано: число

тип «Ход гаммы GCM»
  вариант «Ход гаммы GCM» содержит ключ: список числа, счётчик: список числа, гамма: список числа, позиция: число, выход: список числа

тип «Печать GCM»
  вариант «Печать GCM» содержит шифротекст: список числа, тег: список числа

тип «Исход GCM»
  вариант «Расшифровано» содержит текст: список числа
  вариант «Тег не сошёлся» содержит посчитан: список числа, предъявлен: список числа

тип «Ход CBC»
  вариант «Ход CBC» содержит ключ: список числа, сцепка: список числа, буфер: список числа, набрано: число, выход: список числа

тип «Ход начала»
  вариант «Ход начала» содержит предел: число, место: число, выход: список числа

тотальная функция «Веса байта»
  возвращает список числа
  обеспечивает «разрядов ровно восемь» (длина результат) равен 8
  обеспечивает «младший вес — единица» («Байт по номеру» от результат и 1) равен 1
  обеспечивает «старший вес — сто двадцать восемь» («Байт по номеру» от результат и 8) равен 128
  обеспечивает «вес старшего разряда меньше двухсот пятидесяти шести» («Байт по номеру» от результат и 8) меньше 256
  пример «Восемь весов, от единицы до ста двадцати восьми»
    ожидается [1, 2, 4, 8, 16, 32, 64, 128]

тотальная функция «Исключающее или байтов»
  принимает первый: число, второй: число
  возвращает число
  обеспечивает «итог — байт снизу» результат не меньше 0
  обеспечивает «итог — байт сверху» результат меньше 256
  пример «Ноль с нулём»
    дано первый равно 0
    дано второй равно 0
    ожидается 0

тотальная функция «Байт по номеру»
  принимает байты: список числа, номер: число
  возвращает число
  обеспечивает «байт по номеру — байт сверху» результат меньше 256
  обеспечивает «байт по номеру — байт снизу» результат не меньше 0
  обеспечивает «за границами номера — ноль» если (номер меньше 1) или (номер больше (длина байты)) то (результат равен 0) иначе да
  обеспечивает «вне списка ноль, второй записью» не ((номер меньше 1) или (номер больше (длина байты))) или (результат равен 0)
  обеспечивает «до начала списка — ноль» если (номер меньше 1) то (результат равен 0) иначе да
  обеспечивает «за хвостом списка — ноль» если (номер больше (длина байты)) то (результат равен 0) иначе да
  пример «Первый»
    дано байты равно [7, 8, 9]
    дано номер равно 1
    ожидается 7

тотальная функция «Таблица подстановки»
  возвращает список числа
  обеспечивает «в таблице ровно двести пятьдесят шесть байтов» (длина результат) равен 256
  пример «Первый байт — 0x63, последний — 0x16»
    ожидается [99, 124, 119, 123, 242, 107, 111, 197, 48, 1, 103, 43, 254, 215, 171, 118, 202, 130, 201, 125, 250, 89,
      71, 240, 173, 212, 162, 175, 156, 164, 114, 192, 183, 253, 147, 38, 54, 63, 247, 204, 52, 165, 229, 241, 113, 216,
      49, 21, 4, 199, 35, 195, 24, 150, 5, 154, 7, 18, 128, 226, 235, 39, 178, 117, 9, 131, 44, 26, 27, 110, 90, 160,
      82, 59, 214, 179, 41, 227, 47, 132, 83, 209, 0, 237, 32, 252, 177, 91, 106, 203, 190, 57, 74, 76, 88, 207, 208,
      239, 170, 251, 67, 77, 51, 133, 69, 249, 2, 127, 80, 60, 159, 168, 81, 163, 64, 143, 146, 157, 56, 245, 188, 182,
      218, 33, 16, 255, 243, 210, 205, 12, 19, 236, 95, 151, 68, 23, 196, 167, 126, 61, 100, 93, 25, 115, 96, 129, 79,
      220, 34, 42, 144, 136, 70, 238, 184, 20, 222, 94, 11, 219, 224, 50, 58, 10, 73, 6, 36, 92, 194, 211, 172, 98, 145,
      149, 228, 121, 231, 200, 55, 109, 141, 213, 78, 169, 108, 86, 244, 234, 101, 122, 174, 8, 186, 120, 37, 46, 28,
      166, 180, 198, 232, 221, 116, 31, 75, 189, 139, 138, 112, 62, 181, 102, 72, 3, 246, 14, 97, 53, 87, 185, 134, 193,
      29, 158, 225, 248, 152, 17, 105, 217, 142, 148, 155, 30, 135, 233, 206, 85, 40, 223, 140, 161, 137, 13, 191, 230,
      66, 104, 65, 153, 45, 15, 176, 84, 187, 22]

тотальная функция «Подстановка»
  принимает байт: число
  возвращает число
  обеспечивает «подстановка — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «Ноль идёт в 0x63»
    дано байт равно 0
    ожидается 99

тотальная функция «Удвоить в поле»
  принимает байт: число
  возвращает число
  обеспечивает «удвоенное — байт» (результат не меньше 0) и притом (результат меньше 256)
  обеспечивает «байт без старшего разряда удваивается просто» если ((«Свести к байту» от байт) меньше 128) то (результат равен ((«Свести к байту» от байт) умножить на 2)) иначе да
  пример «Единица удваивается в двойку»
    дано байт равно 1
    ожидается 2

тотальная функция «Утроить в поле»
  принимает байт: число
  возвращает число
  обеспечивает «утроенное — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «Ноль»
    дано байт равно 0
    ожидается 0

тотальная функция «Четыре байта»
  принимает байты: список числа, смещение: число
  возвращает список числа
  обеспечивает «слово — ровно четыре байта» (длина результат) равен 4
  пример «Первое слово»
    дано байты равно [1, 2, 3, 4, 5, 6, 7, 8]
    дано смещение равно 0
    ожидается [1, 2, 3, 4]

тотальная функция «Шестнадцать байтов»
  принимает байты: список числа, смещение: число
  возвращает список числа
  обеспечивает «блок — ровно шестнадцать байтов» (длина результат) равен 16
  пример «Начало ключа FIPS-197»
    дано байты равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано смещение равно 0
    ожидается [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]

тотальная функция «Сложить слова»
  принимает первое: список числа, второе: список числа
  возвращает список числа
  обеспечивает «сумма слов — четыре байта» (длина результат) равен 4
  пример «Слово само с собой даёт нули»
    дано первое равно [1, 2, 3, 4]
    дано второе равно [1, 2, 3, 4]
    ожидается [0, 0, 0, 0]

тотальная функция «Постоянные раундов»
  возвращает список числа
  обеспечивает «постоянных ровно десять» (длина результат) равен 10
  обеспечивает «первая постоянная раунда — единица» («Байт по номеру» от результат и 1) равен 1
  обеспечивает «последняя постоянная раунда — 0x36» («Байт по номеру» от результат и 10) равен 54
  обеспечивает «постоянных раундов больше девяти» (длина результат) больше 9
  пример «01 02 04 08 10 20 40 80 1b 36»
    ожидается [1, 2, 4, 8, 16, 32, 64, 128, 27, 54]

тотальная функция «Слово поворота»
  принимает слово: список числа, постоянная: число
  возвращает список числа
  обеспечивает «итог — четыре байта» (длина результат) равен 4
  пример «Последнее слово ключа FIPS-197 с первой постоянной»
    дано слово равно [12, 13, 14, 15]
    дано постоянная равно 1
    ожидается [214, 171, 118, 254]

тотальная функция «Шаг расширения»
  принимает расширение: список числа, постоянная: число
  возвращает список числа
  обеспечивает «шаг дописывает ровно шестнадцать байтов» (длина результат) равен ((длина расширение) плюс 16)
  пример «Первый шаг над ключом FIPS-197 даёт слова w4..w7»
    дано расширение равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано постоянная равно 1
    ожидается [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214, 170, 116, 253, 210, 175, 114, 250, 218, 166,
      120, 241, 214, 171, 118, 254]

тотальная функция «Расширение ключа»
  принимает ключ: список числа
  возвращает список числа
  обеспечивает «расширение — сто семьдесят шесть байтов, одиннадцать ключей раунда» (длина результат) равен 176
  обеспечивает «первый ключ раунда — сам ключ» («Шестнадцать байтов» от результат и 0) равно («Шестнадцать байтов» от ключ и 0)
  пример «Ключ 000102...0f из приложения A.1 FIPS-197»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    ожидается [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214, 170, 116, 253, 210, 175, 114, 250, 218, 166,
      120, 241, 214, 171, 118, 254, 182, 146, 207, 11, 100, 61, 189, 241, 190, 155, 197, 0, 104, 48, 179, 254, 182, 255,
      116, 78, 210, 194, 201, 191, 108, 89, 12, 191, 4, 105, 191, 65, 71, 247, 247, 188, 149, 53, 62, 3, 249, 108, 50,
      188, 253, 5, 141, 253, 60, 170, 163, 232, 169, 159, 157, 235, 80, 243, 175, 87, 173, 246, 34, 170, 94, 57, 15,
      125, 247, 166, 146, 150, 167, 85, 61, 193, 10, 163, 31, 107, 20, 249, 112, 26, 227, 95, 226, 140, 68, 10, 223, 77,
      78, 169, 192, 38, 71, 67, 135, 53, 164, 28, 101, 185, 224, 22, 186, 244, 174, 191, 122, 210, 84, 153, 50, 209,
      240, 133, 87, 104, 16, 147, 237, 156, 190, 44, 151, 78, 19, 17, 29, 127, 227, 148, 74, 23, 243, 7, 167, 139, 77,
      43, 48, 197]

тотальная функция «Подстановка блока»
  принимает квадрат: список числа
  возвращает список числа
  обеспечивает «подстановка длины не меняет» (длина результат) равен (длина квадрат)
  пример «Шестнадцать нулей идут в шестнадцать 0x63»
    дано квадрат равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99]

тотальная функция «Сдвиг строк»
  принимает квадрат: список числа
  возвращает список числа
  обеспечивает «сдвиг даёт ровно шестнадцать байтов» (длина результат) равен 16
  пример «Байты, помеченные своим местом, разъезжаются по строкам»
    дано квадрат равно [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
    ожидается [1, 6, 11, 16, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12]

тотальная функция «Смешать столбец»
  принимает б0: число, б1: число, б2: число, б3: число
  возвращает список числа
  обеспечивает «смешанный столбец — четыре байта» (длина результат) равен 4
  пример «Учебный столбец db 13 53 45 идёт в 8e 4d a1 bc»
    дано б0 равно 219
    дано б1 равно 19
    дано б2 равно 83
    дано б3 равно 69
    ожидается [142, 77, 161, 188]

тотальная функция «Смешать столбцы»
  принимает квадрат: список числа
  возвращает список числа
  обеспечивает «смешение даёт ровно шестнадцать байтов» (длина результат) равен 16
  пример «Четыре одинаковых столбца db 13 53 45»
    дано квадрат равно [219, 19, 83, 69, 219, 19, 83, 69, 219, 19, 83, 69, 219, 19, 83, 69]
    ожидается [142, 77, 161, 188, 142, 77, 161, 188, 142, 77, 161, 188, 142, 77, 161, 188]

тотальная функция «Сложить с ключом»
  принимает квадрат: список числа, ключ: список числа
  возвращает список числа
  обеспечивает «сложение даёт ровно шестнадцать байтов» (длина результат) равен 16
  пример «Ключ сам с собой обнуляет квадрат»
    дано квадрат равно [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
    дано ключ равно [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Ключ раунда»
  принимает расширение: список числа, раунд: число
  возвращает список числа
  обеспечивает «ключ раунда — шестнадцать байтов» (длина результат) равен 16
  пример «Нулевой ключ раунда — сам ключ»
    дано расширение равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214, 170, 116, 253, 210, 175, 114, 250,
      218, 166, 120, 241, 214, 171, 118, 254, 182, 146, 207, 11, 100, 61, 189, 241, 190, 155, 197, 0, 104, 48, 179, 254,
      182, 255, 116, 78, 210, 194, 201, 191, 108, 89, 12, 191, 4, 105, 191, 65, 71, 247, 247, 188, 149, 53, 62, 3, 249,
      108, 50, 188, 253, 5, 141, 253, 60, 170, 163, 232, 169, 159, 157, 235, 80, 243, 175, 87, 173, 246, 34, 170, 94,
      57, 15, 125, 247, 166, 146, 150, 167, 85, 61, 193, 10, 163, 31, 107, 20, 249, 112, 26, 227, 95, 226, 140, 68, 10,
      223, 77, 78, 169, 192, 38, 71, 67, 135, 53, 164, 28, 101, 185, 224, 22, 186, 244, 174, 191, 122, 210, 84, 153, 50,
      209, 240, 133, 87, 104, 16, 147, 237, 156, 190, 44, 151, 78, 19, 17, 29, 127, 227, 148, 74, 23, 243, 7, 167, 139,
      77, 43, 48, 197]
    дано раунд равно 0
    ожидается [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]

тотальная функция «Шаг раунда шифра»
  принимает ход: «Ход шифра», раунд: число
  возвращает «Ход шифра»
  обеспечивает «раунд шифра ключа не трогает» (длина результат.расширение) равен (длина ход.расширение)
  обеспечивает «квадрат шифра остаётся блоком» (длина результат.квадрат) равен 16
  обеспечивает «раунд шифра отдаёт то же расширение» результат.расширение равно ход.расширение
  пример «Первый раунд над блоком FIPS-197»
    дано ход равно вариант «Ход шифра» с расширение равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214,
      170, 116, 253, 210, 175, 114, 250, 218, 166, 120, 241, 214, 171, 118, 254, 182, 146, 207, 11, 100, 61, 189, 241,
      190, 155, 197, 0, 104, 48, 179, 254, 182, 255, 116, 78, 210, 194, 201, 191, 108, 89, 12, 191, 4, 105, 191, 65, 71,
      247, 247, 188, 149, 53, 62, 3, 249, 108, 50, 188, 253, 5, 141, 253, 60, 170, 163, 232, 169, 159, 157, 235, 80,
      243, 175, 87, 173, 246, 34, 170, 94, 57, 15, 125, 247, 166, 146, 150, 167, 85, 61, 193, 10, 163, 31, 107, 20, 249,
      112, 26, 227, 95, 226, 140, 68, 10, 223, 77, 78, 169, 192, 38, 71, 67, 135, 53, 164, 28, 101, 185, 224, 22, 186,
      244, 174, 191, 122, 210, 84, 153, 50, 209, 240, 133, 87, 104, 16, 147, 237, 156, 190, 44, 151, 78, 19, 17, 29,
      127, 227, 148, 74, 23, 243, 7, 167, 139, 77, 43, 48, 197] и квадрат равным [0, 16, 32, 48, 64, 80, 96, 112, 128,
      144, 160, 176, 192, 208, 224, 240]
    дано раунд равно 1
    ожидается вариант «Ход шифра» с расширение равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214, 170,
      116, 253, 210, 175, 114, 250, 218, 166, 120, 241, 214, 171, 118, 254, 182, 146, 207, 11, 100, 61, 189, 241, 190,
      155, 197, 0, 104, 48, 179, 254, 182, 255, 116, 78, 210, 194, 201, 191, 108, 89, 12, 191, 4, 105, 191, 65, 71, 247,
      247, 188, 149, 53, 62, 3, 249, 108, 50, 188, 253, 5, 141, 253, 60, 170, 163, 232, 169, 159, 157, 235, 80, 243,
      175, 87, 173, 246, 34, 170, 94, 57, 15, 125, 247, 166, 146, 150, 167, 85, 61, 193, 10, 163, 31, 107, 20, 249, 112,
      26, 227, 95, 226, 140, 68, 10, 223, 77, 78, 169, 192, 38, 71, 67, 135, 53, 164, 28, 101, 185, 224, 22, 186, 244,
      174, 191, 122, 210, 84, 153, 50, 209, 240, 133, 87, 104, 16, 147, 237, 156, 190, 44, 151, 78, 19, 17, 29, 127,
      227, 148, 74, 23, 243, 7, 167, 139, 77, 43, 48, 197] и квадрат равным [137, 216, 16, 232, 133, 90, 206, 104, 45,
      24, 67, 216, 203, 18, 143, 228]

тотальная функция «Состояние хода»
  принимает ход: «Ход шифра»
  возвращает список числа
  обеспечивает «квадрат хода — то самое квадрат» результат равно ход.квадрат
  пример «Достаёт квадрат»
    дано ход равно вариант «Ход шифра» с расширение равным пустой список и квадрат равным [1, 2]
    ожидается [1, 2]

тотальная функция «Зашифровать блок»
  принимает ключ: список числа, блок: список числа
  возвращает список числа
  обеспечивает «шифроблок ровно той же длины, что и блок, — шестнадцать байтов» (длина результат) равен 16
  пример «Официальный вектор FIPS-197, приложение B и C.1»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано блок равно [0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255]
    ожидается [105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90]

тотальная функция «Шаг счёта»
  принимает ход: «Ход счёта», байт: число
  возвращает «Ход счёта»
  обеспечивает «счёт удлиняет ответ ровно на байт» (длина результат.байты) равен ((длина ход.байты) плюс 1)
  обеспечивает «перенос — ноль или единица» (результат.перенос равен 0) или (результат.перенос равен 1)
  обеспечивает «с переполнением перенос равен единице» если (((«Свести к байту» от байт) плюс ход.перенос) не меньше 256) то (результат.перенос равен 1) иначе да
  обеспечивает «без переполнения переноса нет» если (не (((«Свести к байту» от байт) плюс ход.перенос) не меньше 256)) то (результат.перенос равен 0) иначе да
  обеспечивает «с переполнением байт кладётся уменьшенным на 256» если (((«Свести к байту» от байт) плюс ход.перенос) не меньше 256) то (результат.байты равен (приписать (((«Свести к байту» от байт) плюс ход.перенос) минус 256) к ход.байты)) иначе да
  обеспечивает «без переполнения байт кладётся как есть» если (не (((«Свести к байту» от байт) плюс ход.перенос) не меньше 256)) то (результат.байты равен (приписать ((«Свести к байту» от байт) плюс ход.перенос) к ход.байты)) иначе да
  пример «Байт 255 с переносом обнуляется и переносит дальше»
    дано ход равно вариант «Ход счёта» с перенос равным 1 и байты равным пустой список
    дано байт равно 255
    ожидается вариант «Ход счёта» с перенос равным 1 и байты равным [0]

тотальная функция «Байты счёта»
  принимает ход: «Ход счёта»
  возвращает список числа
  обеспечивает «байты счёта — те самые байты» результат равно ход.байты
  пример «Достаёт байты»
    дано ход равно вариант «Ход счёта» с перенос равным 0 и байты равным [1, 2]
    ожидается [1, 2]

тотальная функция «Прибавить единицу»
  принимает счётчик: список числа
  возвращает список числа
  обеспечивает «счётчик CTR остаётся блоком в шестнадцать байтов» (длина результат) равен 16
  пример «Ноль становится единицей»
    дано счётчик равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]

тотальная функция «Шаг гаммы»
  принимает ход: «Ход гаммы», байт: число
  возвращает «Ход гаммы»
  обеспечивает «выход гаммы удлиняется ровно на байт» (длина результат.выход) равен ((длина ход.выход) плюс 1)
  обеспечивает «место в гамме CTR не выходит за блок» (результат.позиция не меньше 1) и притом (результат.позиция не больше 16)
  обеспечивает «ключ гаммы CTR не трогается» результат.расширение равно ход.расширение
  обеспечивает «до конца блока счётчик CTR не трогается» если (не (ход.позиция не меньше 16)) то (результат.счётчик равно ход.счётчик) иначе да
  обеспечивает «до конца блока гамма CTR не пересчитывается» если (не (ход.позиция не меньше 16)) то (результат.гамма равно ход.гамма) иначе да
  обеспечивает «до конца блока место CTR растёт на единицу» если (не (ход.позиция не меньше 16)) то (результат.позиция равен (ход.позиция плюс 1)) иначе да
  обеспечивает «на конце блока место CTR сбрасывается в единицу» если (ход.позиция не меньше 16) то (результат.позиция равен 1) иначе да
  обеспечивает «на конце блока счётчик CTR прирастает» если (ход.позиция не меньше 16) то (результат.счётчик равно («Прибавить единицу» от ход.счётчик)) иначе да
  пример «Второй байт блока CTR-AES128 из NIST SP 800-38A, F.5.1: гамма готова, счётчик не трогается»
    дано ход равно вариант «Ход гаммы» с расширение равным [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9,
      207, 79, 60] и счётчик равным [240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254,
      255] и гамма равным [236, 140, 223, 115, 152, 96, 124, 176, 242, 210, 22, 117, 234, 158, 161,
      228] и позиция равным 1 и выход равным [135]
    дано байт равно 193
    ожидается вариант «Ход гаммы» с расширение равным [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207,
      79, 60] и счётчик равным [240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254,
      255] и гамма равным [236, 140, 223, 115, 152, 96, 124, 176, 242, 210, 22, 117, 234, 158, 161,
      228] и позиция равным 2 и выход равным [135, 77]

тотальная функция «Выход гаммы»
  принимает ход: «Ход гаммы»
  возвращает список числа
  обеспечивает «выход хода гаммы — тот самый выход» результат равно ход.выход
  пример «Достаёт выход»
    дано ход равно вариант «Ход гаммы» с расширение равным пустой список и счётчик равным пустой список и гамма равным пустой список и позиция равным 16 и выход равным [5]
    ожидается [5]

тотальная функция «Шифр CTR»
  принимает ключ: список числа, счётчик: список числа, текст: список числа
  возвращает список числа
  обеспечивает «шифротекст CTR ровно той же длины, что и открытый текст» (длина результат) равен (длина текст)
  пример «Пустому тексту — пустой шифротекст»
    дано ключ равно [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]
    дано счётчик равно [240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255]
    дано текст равно пустой список
    ожидается пустой список

тотальная функция «Сложить блоки»
  принимает первый: список числа, второй: список числа
  возвращает список числа
  обеспечивает «сумма блоков — ровно шестнадцать байтов» (длина результат) равен 16
  пример «Блок сам с собой даёт нули»
    дано первый равно [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
    дано второй равно [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Многочлен поля»
  возвращает список числа
  обеспечивает «многочлен — блок в шестнадцать байтов» (длина результат) равен 16
  обеспечивает «старший байт многочлена — 0xe1» («Байт по номеру» от результат и 1) равен 225
  обеспечивает «последний байт многочлена — ноль» («Байт по номеру» от результат и 16) равен 0
  пример «0xe1 и пятнадцать нулей»
    ожидается [225, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Шаг сдвига блока»
  принимает ход: «Ход сдвига», байт: число
  возвращает «Ход сдвига»
  обеспечивает «сдвиг удлиняет ответ ровно на байт» (длина результат.байты) равен ((длина ход.байты) плюс 1)
  обеспечивает «сдвиг помнит поданный байт» результат.прежний равен («Свести к байту» от байт)
  пример «Второй шаг сдвига 01 00…: младший разряд соседа слева становится старшим»
    дано ход равно вариант «Ход сдвига» с прежний равным 1 и байты равным [0]
    дано байт равно 0
    ожидается вариант «Ход сдвига» с прежний равным 0 и байты равным [0, 128]

тотальная функция «Байты сдвига»
  принимает ход: «Ход сдвига»
  возвращает список числа
  обеспечивает «байты сдвига — те самые байты» результат равно ход.байты
  пример «Достаёт байты»
    дано ход равно вариант «Ход сдвига» с прежний равным 0 и байты равным [1, 2]
    ожидается [1, 2]

тотальная функция «Сдвиг блока вправо»
  принимает блок: список числа
  возвращает список числа
  обеспечивает «сдвиг не меняет длины» (длина результат) равен (длина блок)
  пример «Единица в старшем разряде уезжает на разряд вправо»
    дано блок равно [128, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [64, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Привести сдвиг»
  принимает блок: список числа
  возвращает список числа
  обеспечивает «приведение не меняет длины» (длина результат) равен (длина блок)
  обеспечивает «пустому блоку приводить нечего» если ((длина блок) равен 0) то (результат равен блок) иначе да
  обеспечивает «пустому блоку приводить нечего, второй записью» не ((длина блок) равен 0) или (результат равен блок)
  обеспечивает «непустому блоку первый байт складывается с многочленом» если (не ((длина блок) равен 0)) то (результат равен (приписать («Исключающее или байтов» от (голова блок) и 225) к (хвост блок))) иначе да
  пример «Первый байт складывается с 0xe1, прочие не трогаются»
    дано блок равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    ожидается [225, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]

тотальная функция «Шаг разряда поля»
  принимает ход: «Ход поля», бит: число
  возвращает «Ход поля»
  обеспечивает «произведение разряда остаётся блоком» (длина результат.накоплено) равен 16
  обеспечивает «сдвиг остаётся блоком» (длина результат.сдвиг) равен 16
  обеспечивает «на нулевом разряде накопленное не трогается» если (не (бит равен 1)) то (результат.накоплено равно ход.накоплено) иначе да
  обеспечивает «на единичном разряде накопленное складывается со сдвигом» если (бит равен 1) то (результат.накоплено равно («Сложить блоки» от ход.накоплено и ход.сдвиг)) иначе да
  пример «Нулевой разряд: накопленное стоит, сдвиг едет вправо»
    дано ход равно вариант «Ход поля» с накоплено равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
      0] и сдвиг равным [128, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано бит равно 0
    ожидается вариант «Ход поля» с накоплено равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] и сдвиг равным [64,
      0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Шаг байта поля»
  принимает ход: «Ход поля», байт: число
  возвращает «Ход поля»
  обеспечивает «произведение байта остаётся блоком» (длина результат.накоплено) равен 16

тотальная функция «Произведение поля»
  принимает ход: «Ход поля»
  возвращает список числа
  обеспечивает «произведение хода — то самое накопленное» результат равно ход.накоплено
  пример «Достаёт произведение»
    дано ход равно вариант «Ход поля» с накоплено равным [1, 2] и сдвиг равным пустой список
    ожидается [1, 2]

тотальная функция «Умножить в поле»
  принимает первый: список числа, второй: список числа
  возвращает список числа
  обеспечивает «произведение — блок в шестнадцать байтов» (длина результат) равен 16
  пример «На нуль — нуль»
    дано первый равно [102, 233, 75, 212, 239, 138, 44, 59, 136, 76, 250, 89, 202, 52, 43, 46]
    дано второй равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Шаг GHASH»
  принимает ход: «Ход GHASH», байт: число
  возвращает «Ход GHASH»
  обеспечивает «свод остаётся блоком в шестнадцать байтов» (длина результат.свод) равен 16
  обеспечивает «ключ поля не трогается» результат.ключ равно ход.ключ
  обеспечивает «на шестнадцатом байте буфер опустошается» если (ход.набрано не меньше 15) то (результат.буфер равен пустой список) иначе да
  обеспечивает «на шестнадцатом байте счёт набранного обнуляется» если (ход.набрано не меньше 15) то (результат.набрано равен 0) иначе да
  обеспечивает «до шестнадцатого байта свод не трогается» если (не (ход.набрано не меньше 15)) то (результат.свод равен ход.свод) иначе да
  обеспечивает «до шестнадцатого байта счёт набранного растёт на единицу» если (не (ход.набрано не меньше 15)) то (результат.набрано равен (ход.набрано плюс 1)) иначе да
  обеспечивает «до шестнадцатого байта буфер прирастает байтом» если (не (ход.набрано не меньше 15)) то (результат.буфер равен (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  пример «Первый байт шифротекста GCM (SP 800-38D, Test Case 2) только копится в буфере»
    дано ход равно вариант «Ход GHASH» с ключ равным [102, 233, 75, 212, 239, 138, 44, 59, 136, 76, 250, 89, 202, 52,
      43, 46] и свод равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
      0] и буфер равным пустой список и набрано равным 0
    дано байт равно 3
    ожидается вариант «Ход GHASH» с ключ равным [102, 233, 75, 212, 239, 138, 44, 59, 136, 76, 250, 89, 202, 52, 43,
      46] и свод равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] и буфер равным [3] и набрано равным 1

тотальная функция «Свод GHASH»
  принимает ход: «Ход GHASH»
  возвращает список числа
  обеспечивает «свод хода — тот самый свод» результат равно ход.свод
  пример «Достаёт свод»
    дано ход равно вариант «Ход GHASH» с ключ равным пустой список и свод равным [1, 2] и буфер равным пустой список и набрано равным 0
    ожидается [1, 2]

тотальная функция «GHASH»
  принимает ключ: список числа, данные: список числа
  возвращает список числа
  обеспечивает «свод GHASH — блок в шестнадцать байтов» (длина результат) равен 16
  пример «Пустым данным — нулевой свод»
    дано ключ равно [102, 233, 75, 212, 239, 138, 44, 59, 136, 76, 250, 89, 202, 52, 43, 46]
    дано данные равно пустой список
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Ключ хеша»
  принимает ключ: список числа
  возвращает список числа
  обеспечивает «ключ поля — блок в шестнадцать байтов» (длина результат) равен 16
  пример «Нулевой ключ даёт H = 66e94bd4ef8a2c3b884cfa59ca342b2e (SP 800-38D, Test Case 1)»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [102, 233, 75, 212, 239, 138, 44, 59, 136, 76, 250, 89, 202, 52, 43, 46]

тотальная функция «Прибавить единицу по младшим четырём»
  принимает счётчик: список числа
  возвращает список числа
  обеспечивает «счётчик GCM остаётся блоком в шестнадцать байтов» (длина результат) равен 16
  пример «Единица прирастает в двойку, вектор не тронут»
    дано счётчик равно [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 0, 0, 0, 1]
    ожидается [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 0, 0, 0, 2]

тотальная функция «Шаг гаммы GCM»
  принимает ход: «Ход гаммы GCM», байт: число
  возвращает «Ход гаммы GCM»
  обеспечивает «выход гаммы GCM удлиняется ровно на байт» (длина результат.выход) равен ((длина ход.выход) плюс 1)
  обеспечивает «место в гамме GCM не выходит за блок» (результат.позиция не меньше 1) и притом (результат.позиция не больше 16)
  обеспечивает «ключ гаммы GCM не трогается» результат.ключ равно ход.ключ
  обеспечивает «до конца блока счётчик GCM не трогается» если (не (ход.позиция не меньше 16)) то (результат.счётчик равно ход.счётчик) иначе да
  обеспечивает «до конца блока гамма GCM не пересчитывается» если (не (ход.позиция не меньше 16)) то (результат.гамма равно ход.гамма) иначе да
  обеспечивает «до конца блока место GCM растёт на единицу» если (не (ход.позиция не меньше 16)) то (результат.позиция равен (ход.позиция плюс 1)) иначе да
  обеспечивает «на конце блока место GCM сбрасывается в единицу» если (ход.позиция не меньше 16) то (результат.позиция равен 1) иначе да
  обеспечивает «на конце блока счётчик GCM прирастает» если (ход.позиция не меньше 16) то (результат.счётчик равно («Прибавить единицу по младшим четырём» от ход.счётчик)) иначе да
  пример «Второй байт гаммы GCM (SP 800-38D, Test Case 2): счётчик по inc32 не трогается»
    дано ход равно вариант «Ход гаммы GCM» с ключ равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
      0] и счётчик равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2] и гамма равным [3, 136, 218, 206, 96, 182,
      163, 146, 243, 40, 194, 185, 113, 178, 254, 120] и позиция равным 1 и выход равным [3]
    дано байт равно 0
    ожидается вариант «Ход гаммы GCM» с ключ равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] и счётчик равным [
      0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2] и гамма равным [3, 136, 218, 206, 96, 182, 163, 146, 243, 40, 194,
      185, 113, 178, 254, 120] и позиция равным 2 и выход равным [3, 136]

тотальная функция «Выход гаммы GCM»
  принимает ход: «Ход гаммы GCM»
  возвращает список числа
  обеспечивает «выход хода гаммы GCM — тот самый выход» результат равно ход.выход
  пример «Достаёт выход»
    дано ход равно вариант «Ход гаммы GCM» с ключ равным пустой список и счётчик равным пустой список и гамма равным пустой список и позиция равным 16 и выход равным [5]
    ожидается [5]

тотальная функция «Шифр GCTR»
  принимает ключ: список числа, счётчик: список числа, текст: список числа
  возвращает список числа
  обеспечивает «шифротекст GCTR ровно той же длины, что и открытый текст» (длина результат) равен (длина текст)
  пример «Пустому тексту — пустой шифротекст»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано счётчик равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2]
    дано текст равно пустой список
    ожидается пустой список

тотальная функция «Набивка до блока»
  принимает байты: список числа
  возвращает список числа
  обеспечивает «набитое нулями делится на блоки нацело» ((длина результат) остаток от 16) равен 0
  обеспечивает «набивка короче блока» (длина результат) меньше ((длина байты) плюс 16)
  пример «Пусто остаётся пустым»
    дано байты равно пустой список
    ожидается пустой список

тотальная функция «Данные GHASH»
  принимает доп: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «данные делятся на блоки нацело» ((длина результат) остаток от 16) равен 0
  пример «Пусто и пусто — один блок из двух нулевых длин»
    дано доп равно пустой список
    дано шифротекст равно пустой список
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Начальный счётчик»
  принимает ключ: список числа, вектор: список числа
  возвращает список числа
  обеспечивает «начальный счётчик — блок в шестнадцать байтов» (длина результат) равен 16
  обеспечивает «вектору в двенадцать байтов приписана единица» если ((длина вектор) равен 12) то (результат равен («Досыпать байты» от («Досыпать байты» от вектор и («Нули» от 3)) и [1])) иначе да
  пример «Вектор в двенадцать байтов: к нему приписана единица»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]

тотальная функция «Тег GCM»
  принимает ключ: список числа, вектор: список числа, доп: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «тег GCM — ровно шестнадцать байтов» (длина результат) равен 16
  пример «Test Case 1 (SP 800-38D): нулевой ключ, пустые данные, пустой шифротекст»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано доп равно пустой список
    дано шифротекст равно пустой список
    ожидается [88, 226, 252, 206, 250, 126, 48, 97, 54, 127, 29, 87, 164, 231, 69, 90]

тотальная функция «Зашифровать GCM»
  принимает ключ: список числа, вектор: список числа, доп: список числа, текст: список числа
  возвращает «Печать GCM»
  обеспечивает «тег шифрования GCM — ровно шестнадцать байтов» (длина результат.тег) равен 16
  обеспечивает «шифротекст GCM ровно той же длины, что и открытый текст» (длина результат.шифротекст) равен (длина текст)
  пример «Test Case 1 (SP 800-38D): пустой текст, пустые данные, нулевой ключ»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано доп равно пустой список
    дано текст равно пустой список
    ожидается вариант «Печать GCM» с шифротекст равным пустой список и тег равным [88, 226, 252, 206, 250, 126, 48, 97,
      54, 127, 29, 87, 164, 231, 69, 90]

тотальная функция «Расшифровано ли»
  принимает исход: «Исход GCM»
  возвращает признак
  пример «Успех признаётся успехом»
    дано исход равно вариант «Расшифровано» с текст равным [1, 2]
    ожидается да

тотальная функция «Текст исхода»
  принимает исход: «Исход GCM»
  возвращает список числа
  обеспечивает «у отказа текста нет» («Расшифровано ли» от исход) или ((длина результат) равен 0)
  пример «У успеха берётся текст»
    дано исход равно вариант «Расшифровано» с текст равным [1, 2]
    ожидается [1, 2]

тотальная функция «Расшифровать GCM»
  принимает ключ: список числа, вектор: список числа, доп: список числа, шифротекст: список числа, тег: список числа
  возвращает «Исход GCM»
  обеспечивает «при отказе открытого текста не выдаётся» («Расшифровано ли» от результат) или ((длина («Текст исхода» от результат)) равен 0)
  обеспечивает «при успехе открытый текст той же длины, что и шифротекст» не («Расшифровано ли» от результат) или ((длина («Текст исхода» от результат)) равен (длина шифротекст))

тотальная функция «Обратная таблица подстановки»
  возвращает список числа
  обеспечивает «в обратной таблице ровно двести пятьдесят шесть байтов» (длина результат) равен 256
  пример «Двести пятьдесят шесть байтов обратной таблицы FIPS-197, рис. 14»
    ожидается [82, 9, 106, 213, 48, 54, 165, 56, 191, 64, 163, 158, 129, 243, 215, 251, 124, 227, 57, 130, 155, 47, 255,
      135, 52, 142, 67, 68, 196, 222, 233, 203, 84, 123, 148, 50, 166, 194, 35, 61, 238, 76, 149, 11, 66, 250, 195, 78,
      8, 46, 161, 102, 40, 217, 36, 178, 118, 91, 162, 73, 109, 139, 209, 37, 114, 248, 246, 100, 134, 104, 152, 22,
      212, 164, 92, 204, 93, 101, 182, 146, 108, 112, 72, 80, 253, 237, 185, 218, 94, 21, 70, 87, 167, 141, 157, 132,
      144, 216, 171, 0, 140, 188, 211, 10, 247, 228, 88, 5, 184, 179, 69, 6, 208, 44, 30, 143, 202, 63, 15, 2, 193, 175,
      189, 3, 1, 19, 138, 107, 58, 145, 17, 65, 79, 103, 220, 234, 151, 242, 207, 206, 240, 180, 230, 115, 150, 172,
      116, 34, 231, 173, 53, 133, 226, 249, 55, 232, 28, 117, 223, 110, 71, 241, 26, 113, 29, 41, 197, 137, 111, 183,
      98, 14, 170, 24, 190, 27, 252, 86, 62, 75, 198, 210, 121, 32, 154, 219, 192, 254, 120, 205, 90, 244, 31, 221, 168,
      51, 136, 7, 199, 49, 177, 18, 16, 89, 39, 128, 236, 95, 96, 81, 127, 169, 25, 181, 74, 13, 45, 229, 122, 159, 147,
      201, 156, 239, 160, 224, 59, 77, 174, 42, 245, 176, 200, 235, 187, 60, 131, 83, 153, 97, 23, 43, 4, 126, 186, 119,
      214, 38, 225, 105, 20, 99, 85, 33, 12, 125]

тотальная функция «Обратная подстановка»
  принимает байт: число
  возвращает число
  обеспечивает «обратная подстановка — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «0x63 возвращается в ноль»
    дано байт равно 99
    ожидается 0

тотальная функция «Обратная подстановка блока»
  принимает квадрат: список числа
  возвращает список числа
  обеспечивает «обратная подстановка длины не меняет» (длина результат) равен (длина квадрат)
  пример «Шестнадцать 0x63 возвращаются в шестнадцать нулей»
    дано квадрат равно [99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99, 99]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Обратный сдвиг строк»
  принимает квадрат: список числа
  возвращает список числа
  обеспечивает «обратный сдвиг даёт ровно шестнадцать байтов» (длина результат) равен 16
  пример «Разъехавшееся по строкам возвращается на свои места»
    дано квадрат равно [1, 6, 11, 16, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12]
    ожидается [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]

тотальная функция «Умножить на девять в поле»
  принимает байт: число
  возвращает число
  обеспечивает «произведение на девять — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «Ноль»
    дано байт равно 0
    ожидается 0

тотальная функция «Умножить на одиннадцать в поле»
  принимает байт: число
  возвращает число
  обеспечивает «произведение на одиннадцать — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «Единица идёт в одиннадцать»
    дано байт равно 1
    ожидается 11

тотальная функция «Умножить на тринадцать в поле»
  принимает байт: число
  возвращает число
  обеспечивает «произведение на тринадцать — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «Единица идёт в тринадцать»
    дано байт равно 1
    ожидается 13

тотальная функция «Умножить на четырнадцать в поле»
  принимает байт: число
  возвращает число
  обеспечивает «произведение на четырнадцать — байт» (результат не меньше 0) и притом (результат меньше 256)
  пример «Единица идёт в четырнадцать»
    дано байт равно 1
    ожидается 14

тотальная функция «Обратно смешать столбец»
  принимает б0: число, б1: число, б2: число, б3: число
  возвращает список числа
  обеспечивает «обратно смешанный столбец — четыре байта» (длина результат) равен 4
  пример «Учебный 8e 4d a1 bc возвращается в db 13 53 45»
    дано б0 равно 142
    дано б1 равно 77
    дано б2 равно 161
    дано б3 равно 188
    ожидается [219, 19, 83, 69]

тотальная функция «Обратно смешать столбцы»
  принимает квадрат: список числа
  возвращает список числа
  обеспечивает «обратное смешение даёт ровно шестнадцать байтов» (длина результат) равен 16
  пример «Четыре одинаковых столбца 8e 4d a1 bc»
    дано квадрат равно [142, 77, 161, 188, 142, 77, 161, 188, 142, 77, 161, 188, 142, 77, 161, 188]
    ожидается [219, 19, 83, 69, 219, 19, 83, 69, 219, 19, 83, 69, 219, 19, 83, 69]

тотальная функция «Шаг раунда расшифровки»
  принимает ход: «Ход шифра», раунд: число
  возвращает «Ход шифра»
  обеспечивает «раунд расшифровки ключа не трогает» (длина результат.расширение) равен (длина ход.расширение)
  обеспечивает «квадрат расшифровки остаётся блоком» (длина результат.квадрат) равен 16
  обеспечивает «раунд расшифровки отдаёт то же расширение» результат.расширение равно ход.расширение
  пример «Девятый обратный раунд следа FIPS-197 C.1: 7ad5fda789ef4e272bca100b3d9ff59f → 54d990a16ba09ab596bbf40ea111702f»
    дано ход равно вариант «Ход шифра» с расширение равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214,
      170, 116, 253, 210, 175, 114, 250, 218, 166, 120, 241, 214, 171, 118, 254, 182, 146, 207, 11, 100, 61, 189, 241,
      190, 155, 197, 0, 104, 48, 179, 254, 182, 255, 116, 78, 210, 194, 201, 191, 108, 89, 12, 191, 4, 105, 191, 65, 71,
      247, 247, 188, 149, 53, 62, 3, 249, 108, 50, 188, 253, 5, 141, 253, 60, 170, 163, 232, 169, 159, 157, 235, 80,
      243, 175, 87, 173, 246, 34, 170, 94, 57, 15, 125, 247, 166, 146, 150, 167, 85, 61, 193, 10, 163, 31, 107, 20, 249,
      112, 26, 227, 95, 226, 140, 68, 10, 223, 77, 78, 169, 192, 38, 71, 67, 135, 53, 164, 28, 101, 185, 224, 22, 186,
      244, 174, 191, 122, 210, 84, 153, 50, 209, 240, 133, 87, 104, 16, 147, 237, 156, 190, 44, 151, 78, 19, 17, 29,
      127, 227, 148, 74, 23, 243, 7, 167, 139, 77, 43, 48, 197] и квадрат равным [122, 213, 253, 167, 137, 239, 78, 39,
      43, 202, 16, 11, 61, 159, 245, 159]
    дано раунд равно 9
    ожидается вариант «Ход шифра» с расширение равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 214, 170,
      116, 253, 210, 175, 114, 250, 218, 166, 120, 241, 214, 171, 118, 254, 182, 146, 207, 11, 100, 61, 189, 241, 190,
      155, 197, 0, 104, 48, 179, 254, 182, 255, 116, 78, 210, 194, 201, 191, 108, 89, 12, 191, 4, 105, 191, 65, 71, 247,
      247, 188, 149, 53, 62, 3, 249, 108, 50, 188, 253, 5, 141, 253, 60, 170, 163, 232, 169, 159, 157, 235, 80, 243,
      175, 87, 173, 246, 34, 170, 94, 57, 15, 125, 247, 166, 146, 150, 167, 85, 61, 193, 10, 163, 31, 107, 20, 249, 112,
      26, 227, 95, 226, 140, 68, 10, 223, 77, 78, 169, 192, 38, 71, 67, 135, 53, 164, 28, 101, 185, 224, 22, 186, 244,
      174, 191, 122, 210, 84, 153, 50, 209, 240, 133, 87, 104, 16, 147, 237, 156, 190, 44, 151, 78, 19, 17, 29, 127,
      227, 148, 74, 23, 243, 7, 167, 139, 77, 43, 48, 197] и квадрат равным [84, 217, 144, 161, 107, 160, 154, 181, 150,
      187, 244, 14, 161, 17, 112, 47]

тотальная функция «Расшифровать блок»
  принимает ключ: список числа, блок: список числа
  возвращает список числа
  обеспечивает «расшифрованное ровно той же длины, что и шифроблок, — шестнадцать байтов» (длина результат) равен 16
  пример «Официальный вектор FIPS-197, приложение C.1, в обратную сторону»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано блок равно [105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90]
    ожидается [0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255]

тотальная функция «Состояние обратного хода»
  принимает ключ: список числа, блок: список числа, раунды: список числа
  возвращает список числа
  обеспечивает «состояние обратного хода — шестнадцать байтов» (длина результат) равен 16
  пример «Без единого раунда — блок, сложенный с десятым ключом раунда»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано блок равно [105, 196, 224, 216, 106, 123, 4, 48, 216, 205, 183, 128, 112, 180, 197, 90]
    дано раунды равно пустой список
    ожидается [122, 213, 253, 167, 137, 239, 78, 39, 43, 202, 16, 11, 61, 159, 245, 159]

тотальная функция «Шаг CBC вперёд»
  принимает ход: «Ход CBC», байт: число
  возвращает «Ход CBC»
  обеспечивает «сцепка шифрования CBC остаётся блоком в шестнадцать байтов» (длина результат.сцепка) равен 16
  обеспечивает «ключ шифрования CBC не трогается» результат.ключ равно ход.ключ
  обеспечивает «на полном блоке буфер шифрования опустошается» если (ход.набрано не меньше 15) то (результат.буфер равен пустой список) иначе да
  обеспечивает «на полном блоке счёт набранного обнуляется» если (ход.набрано не меньше 15) то (результат.набрано равен 0) иначе да
  обеспечивает «до полного блока счёт набранного шифрования растёт на единицу» если (не (ход.набрано не меньше 15)) то (результат.набрано равен (ход.набрано плюс 1)) иначе да
  обеспечивает «до полного блока буфер шифрования прирастает байтом» если (не (ход.набрано не меньше 15)) то (результат.буфер равен (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  обеспечивает «до полного блока выход шифрования не трогается» если (не (ход.набрано не меньше 15)) то (результат.выход равно ход.выход) иначе да
  обеспечивает «до полного блока сцепка шифрования не трогается» если (не (ход.набрано не меньше 15)) то (результат.сцепка равно ход.сцепка) иначе да
  пример «Первый байт CBC-AES128 (NIST SP 800-38A, F.2.1) копится в буфере, сцепка стоит вектором»
    дано ход равно вариант «Ход CBC» с ключ равным [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79,
      60] и сцепка равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
      15] и буфер равным пустой список и набрано равным 0 и выход равным пустой список
    дано байт равно 107
    ожидается вариант «Ход CBC» с ключ равным [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79,
      60] и сцепка равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
      15] и буфер равным [107] и набрано равным 1 и выход равным пустой список

тотальная функция «Шаг CBC назад»
  принимает ход: «Ход CBC», байт: число
  возвращает «Ход CBC»
  обеспечивает «сцепка расшифровки CBC остаётся блоком в шестнадцать байтов» (длина результат.сцепка) равен 16
  обеспечивает «ключ расшифровки CBC не трогается» результат.ключ равно ход.ключ
  обеспечивает «на полном блоке буфер расшифровки опустошается» если (ход.набрано не меньше 15) то (результат.буфер равен пустой список) иначе да
  обеспечивает «на полном блоке счёт набранного расшифровки обнуляется» если (ход.набрано не меньше 15) то (результат.набрано равен 0) иначе да
  обеспечивает «до полного блока счёт набранного расшифровки растёт на единицу» если (не (ход.набрано не меньше 15)) то (результат.набрано равен (ход.набрано плюс 1)) иначе да
  обеспечивает «до полного блока буфер расшифровки прирастает байтом» если (не (ход.набрано не меньше 15)) то (результат.буфер равен (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  обеспечивает «до полного блока выход расшифровки не трогается» если (не (ход.набрано не меньше 15)) то (результат.выход равно ход.выход) иначе да
  обеспечивает «до полного блока сцепка расшифровки не трогается» если (не (ход.набрано не меньше 15)) то (результат.сцепка равно ход.сцепка) иначе да
  обеспечивает «на полном блоке сцепкой расшифровки становится сам шифроблок» если (ход.набрано не меньше 15) то (результат.сцепка равно (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  пример «Первый байт шифротекста CBC-AES128 (F.2.2) копится в буфере, выход не трогается»
    дано ход равно вариант «Ход CBC» с ключ равным [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79,
      60] и сцепка равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
      15] и буфер равным пустой список и набрано равным 0 и выход равным пустой список
    дано байт равно 118
    ожидается вариант «Ход CBC» с ключ равным [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79,
      60] и сцепка равным [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14,
      15] и буфер равным [118] и набрано равным 1 и выход равным пустой список

тотальная функция «Выход CBC»
  принимает ход: «Ход CBC»
  возвращает список числа
  обеспечивает «выход хода CBC — тот самый выход» результат равно ход.выход
  пример «Достаёт выход»
    дано ход равно вариант «Ход CBC» с ключ равным пустой список и сцепка равным пустой список и буфер равным пустой список и набрано равным 0 и выход равным [7]
    ожидается [7]

тотальная функция «Шифр CBC»
  принимает ключ: список числа, вектор: список числа, текст: список числа
  возвращает список числа
  обеспечивает «на целом числе блоков шифротекст ровно той же длины, что и открытый текст» (не (((длина текст) остаток от 16) равен 0)) или ((длина результат) равен (длина текст))
  пример «Пустому тексту — пустой шифротекст»
    дано ключ равно [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано текст равно пустой список
    ожидается пустой список

тотальная функция «Расшифровка CBC начисто»
  принимает ключ: список числа, вектор: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «на целом числе блоков расшифрованное ровно той же длины, что и шифротекст» (не (((длина шифротекст) остаток от 16) равен 0)) или ((длина результат) равен (длина шифротекст))
  пример «Все четыре блока CBC-AES128 из NIST SP 800-38A, F.2.2»
    дано ключ равно [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано шифротекст равно [118, 73, 171, 172, 129, 25, 178, 70, 206, 233, 142, 155, 18, 233, 25, 125, 80, 134, 203, 155,
      80, 114, 25, 238, 149, 219, 17, 58, 145, 118, 120, 178, 115, 190, 214, 184, 227, 193, 116, 59, 113, 22, 230, 158,
      34, 34, 149, 22, 63, 241, 202, 161, 104, 31, 172, 9, 18, 14, 202, 48, 117, 134, 225, 167]
    ожидается [107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172,
      156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17, 229, 251, 193, 25, 26, 10, 82, 239,
      246, 159, 36, 69, 223, 79, 155, 23, 173, 43, 65, 123, 230, 108, 55, 16]

тотальная функция «Набивка PKCS7»
  принимает байты: список числа
  возвращает список числа
  обеспечивает «набитое по PKCS7 делится на блоки нацело» ((длина результат) остаток от 16) равен 0
  обеспечивает «набивка добавляет не меньше байта и не больше блока» ((длина результат) больше (длина байты)) и притом ((длина результат) не больше ((длина байты) плюс 16))
  пример «Пусто добивается целым блоком шестнадцати»
    дано байты равно пустой список
    ожидается [16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16]

тотальная функция «Длина без набивки»
  принимает байты: список числа
  возвращает число
  обеспечивает «длина без набивки не больше самой длины» результат не больше (длина байты)
  обеспечивает «длина без набивки не меньше нуля» результат не меньше 0
  обеспечивает «негодная набивка не снимается» если ((«Байт по номеру» от байты и (длина байты)) меньше 1) или ((«Байт по номеру» от байты и (длина байты)) больше 16) или ((«Байт по номеру» от байты и (длина байты)) больше (длина байты)) то (результат равен (длина байты)) иначе да
  обеспечивает «годная набивка снимается вся» если (не (((«Байт по номеру» от байты и (длина байты)) меньше 1) или ((«Байт по номеру» от байты и (длина байты)) больше 16) или ((«Байт по номеру» от байты и (длина байты)) больше (длина байты)))) то (результат равен ((длина байты) минус («Байт по номеру» от байты и (длина байты)))) иначе да
  пример «Целый блок набивки снимается весь»
    дано байты равно [16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16]
    ожидается 0

тотальная функция «Шаг начала»
  принимает ход: «Ход начала», байт: число
  возвращает «Ход начала»
  обеспечивает «место растёт ровно на единицу» результат.место равен (ход.место плюс 1)
  обеспечивает «предел не трогается» результат.предел равно ход.предел
  обеспечивает «за пределом выход начала не трогается» если ((ход.место плюс 1) больше ход.предел) то (результат.выход равно ход.выход) иначе да
  обеспечивает «до предела выход начала прирастает байтом» если (не ((ход.место плюс 1) больше ход.предел)) то (результат.выход равен (добавить («Свести к байту» от байт) к ход.выход)) иначе да
  пример «До предела байт берётся»
    дано ход равно вариант «Ход начала» с предел равным 5 и место равным 0 и выход равным пустой список
    дано байт равно 1
    ожидается вариант «Ход начала» с предел равным 5 и место равным 1 и выход равным [1]

тотальная функция «Выход начала»
  принимает ход: «Ход начала»
  возвращает список числа
  обеспечивает «выход хода начала — тот самый выход» результат равно ход.выход
  пример «Достаёт выход»
    дано ход равно вариант «Ход начала» с предел равным 0 и место равным 0 и выход равным [3]
    ожидается [3]

тотальная функция «Начало байтов»
  принимает байты: список числа, сколько: число
  возвращает список числа
  обеспечивает «начало не длиннее целого» (длина результат) не больше (длина байты)
  пример «Первые пять из шестнадцати»
    дано байты равно [1, 2, 3, 4, 5, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11, 11]
    дано сколько равно 5
    ожидается [1, 2, 3, 4, 5]

тотальная функция «Зашифровать CBC»
  принимает ключ: список числа, вектор: список числа, текст: список числа
  возвращает список числа
  обеспечивает «шифротекст ложится блоками нацело» ((длина результат) остаток от 16) равен 0
  обеспечивает «шифротекст длиннее открытого текста не меньше чем на байт и не больше чем на блок» ((длина результат) больше (длина текст)) и притом ((длина результат) не больше ((длина текст) плюс 16))
  пример «Пять байтов уходят в один блок»
    дано ключ равно [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано текст равно [1, 2, 3, 4, 5]
    ожидается [15, 110, 170, 226, 130, 197, 68, 0, 161, 146, 108, 179, 138, 104, 218, 95]

тотальная функция «Расшифровать CBC»
  принимает ключ: список числа, вектор: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «расшифрованное не длиннее шифротекста» (длина результат) не больше (длина шифротекст)
  пример «Тот же блок в обратную сторону: расшифровка зашифрованного возвращает исходное»
    дано ключ равно [43, 126, 21, 22, 40, 174, 210, 166, 171, 247, 21, 136, 9, 207, 79, 60]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано шифротекст равно [15, 110, 170, 226, 130, 197, 68, 0, 161, 146, 108, 179, 138, 104, 218, 95]
    ожидается [1, 2, 3, 4, 5]

тотальная функция «Тридцать два байта»
  принимает байты: список числа, смещение: число
  возвращает список числа
  обеспечивает «ключ — ровно тридцать два байта» (длина результат) равен 32
  пример «Ключ 000102…1f из приложения C.3 FIPS-197»
    дано байты равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26,
      27, 28, 29, 30, 31]
    дано смещение равно 0
    ожидается [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28,
      29, 30, 31]

тотальная функция «Слово подстановки»
  принимает слово: список числа
  возвращает список числа
  обеспечивает «итог — четыре байта» (длина результат) равен 4
  пример «Последнее слово ключа C.3: 1c1d1e1f идёт в 9ca472c0»
    дано слово равно [28, 29, 30, 31]
    ожидается [156, 164, 114, 192]

тотальная функция «Постоянные раундов 256»
  возвращает список числа
  обеспечивает «постоянных ровно шесть» (длина результат) равен 6
  обеспечивает «первая постоянная раунда 256 — единица» («Байт по номеру» от результат и 1) равен 1
  обеспечивает «последняя постоянная раунда 256 — 0x20» («Байт по номеру» от результат и 6) равен 32
  пример «01 02 04 08 10 20»
    ожидается [1, 2, 4, 8, 16, 32]

тотальная функция «Шаг расширения 256»
  принимает расширение: список числа, постоянная: число
  возвращает список числа
  обеспечивает «шаг дописывает ровно тридцать два байта» (длина результат) равен ((длина расширение) плюс 32)

тотальная функция «Полшага расширения 256»
  принимает расширение: список числа, постоянная: число
  возвращает список числа
  обеспечивает «полшага дописывает ровно шестнадцать байтов» (длина результат) равен ((длина расширение) плюс 16)

тотальная функция «Расширение ключа 256»
  принимает ключ: список числа
  возвращает список числа
  обеспечивает «расширение — двести сорок байтов, пятнадцать ключей раунда» (длина результат) равен 240
  обеспечивает «первый ключ раунда — первая половина ключа» («Шестнадцать байтов» от результат и 0) равно («Шестнадцать байтов» от ключ и 0)
  пример «Ключ 000102…1f из приложения C.3 FIPS-197: все шестьдесят слов»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26,
      27, 28, 29, 30, 31]
    ожидается [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28,
      29, 30, 31, 165, 115, 194, 159, 161, 118, 196, 152, 169, 127, 206, 147, 165, 114, 192, 156, 22, 81, 168, 205, 2,
      68, 190, 218, 26, 93, 164, 193, 6, 64, 186, 222, 174, 135, 223, 240, 15, 241, 27, 104, 166, 142, 213, 251, 3, 252,
      21, 103, 109, 225, 241, 72, 111, 165, 79, 146, 117, 248, 235, 83, 115, 184, 81, 141, 198, 86, 130, 127, 201, 167,
      153, 23, 111, 41, 76, 236, 108, 213, 89, 139, 61, 226, 58, 117, 82, 71, 117, 231, 39, 191, 158, 180, 84, 7, 207,
      57, 11, 220, 144, 95, 194, 123, 9, 72, 173, 82, 69, 164, 193, 135, 28, 47, 69, 245, 166, 96, 23, 178, 211, 135,
      48, 13, 77, 51, 100, 10, 130, 10, 124, 207, 247, 28, 190, 180, 254, 84, 19, 230, 187, 240, 210, 97, 167, 223, 240,
      26, 250, 254, 231, 168, 41, 121, 215, 165, 100, 74, 179, 175, 230, 64, 37, 65, 254, 113, 155, 245, 0, 37, 136, 19,
      187, 213, 90, 114, 28, 10, 78, 90, 102, 153, 169, 242, 79, 224, 126, 87, 43, 170, 205, 248, 205, 234, 36, 252,
      121, 204, 191, 9, 121, 233, 55, 26, 194, 60, 109, 104, 222, 54]

тотальная функция «Зашифровать блок 256»
  принимает ключ: список числа, блок: список числа
  возвращает список числа
  обеспечивает «шифроблок ровно той же длины, что и блок, — шестнадцать байтов» (длина результат) равен 16
  пример «Официальный вектор FIPS-197, приложение C.3 (AES-256)»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26,
      27, 28, 29, 30, 31]
    дано блок равно [0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255]
    ожидается [142, 162, 183, 202, 81, 103, 69, 191, 234, 252, 73, 144, 75, 73, 96, 137]

тотальная функция «Расшифровать блок 256»
  принимает ключ: список числа, блок: список числа
  возвращает список числа
  обеспечивает «расшифрованное ровно той же длины, что и шифроблок, — шестнадцать байтов» (длина результат) равен 16
  пример «Официальный вектор FIPS-197, приложение C.3, в обратную сторону»
    дано ключ равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26,
      27, 28, 29, 30, 31]
    дано блок равно [142, 162, 183, 202, 81, 103, 69, 191, 234, 252, 73, 144, 75, 73, 96, 137]
    ожидается [0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255]

тотальная функция «Шаг гаммы 256»
  принимает ход: «Ход гаммы», байт: число
  возвращает «Ход гаммы»
  обеспечивает «выход удлиняется ровно на байт» (длина результат.выход) равен ((длина ход.выход) плюс 1)
  обеспечивает «место в гамме не выходит за блок» (результат.позиция не меньше 1) и притом (результат.позиция не больше 16)
  обеспечивает «до конца блока место 256 растёт на единицу» если (не (ход.позиция не меньше 16)) то (результат.позиция равен (ход.позиция плюс 1)) иначе да
  обеспечивает «на конце блока место 256 сбрасывается в единицу» если (ход.позиция не меньше 16) то (результат.позиция равен 1) иначе да
  обеспечивает «ключ гаммы 256 не трогается» результат.расширение равно ход.расширение
  обеспечивает «до конца блока счётчик 256 не трогается» если (не (ход.позиция не меньше 16)) то (результат.счётчик равно ход.счётчик) иначе да
  обеспечивает «до конца блока гамма 256 не пересчитывается» если (не (ход.позиция не меньше 16)) то (результат.гамма равно ход.гамма) иначе да
  обеспечивает «на конце блока счётчик 256 прирастает» если (ход.позиция не меньше 16) то (результат.счётчик равно («Прибавить единицу» от ход.счётчик)) иначе да
  пример «Второй байт блока CTR-AES256 из NIST SP 800-38A, F.5.5»
    дано ход равно вариант «Ход гаммы» с расширение равным [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133,
      125, 119, 129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244] и счётчик равным [240, 241, 242,
      243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255] и гамма равным [11, 223, 125, 241, 89, 23, 22,
      51, 94, 154, 139, 21, 200, 96, 197, 2] и позиция равным 1 и выход равным [96]
    дано байт равно 193
    ожидается вариант «Ход гаммы» с расширение равным [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125,
      119, 129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244] и счётчик равным [240, 241, 242, 243,
      244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255] и гамма равным [11, 223, 125, 241, 89, 23, 22, 51, 94,
      154, 139, 21, 200, 96, 197, 2] и позиция равным 2 и выход равным [96, 30]

тотальная функция «Шифр CTR 256»
  принимает ключ: список числа, счётчик: список числа, текст: список числа
  возвращает список числа
  обеспечивает «шифротекст ровно той же длины, что и открытый текст» (длина результат) равен (длина текст)
  пример «Пустому тексту — пустой шифротекст»
    дано ключ равно [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97,
      8, 215, 45, 152, 16, 163, 9, 20, 223, 244]
    дано счётчик равно [240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255]
    дано текст равно пустой список
    ожидается пустой список

тотальная функция «Шаг CBC вперёд 256»
  принимает ход: «Ход CBC», байт: число
  возвращает «Ход CBC»
  обеспечивает «сцепка остаётся блоком в шестнадцать байтов» (длина результат.сцепка) равен 16
  обеспечивает «ключ не трогается» результат.ключ равно ход.ключ
  обеспечивает «до полного блока счёт набранного 256 растёт на единицу» если (не (ход.набрано не меньше 15)) то (результат.набрано равен (ход.набрано плюс 1)) иначе да
  обеспечивает «до полного блока буфер 256 прирастает байтом» если (не (ход.набрано не меньше 15)) то (результат.буфер равен (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  обеспечивает «на полном блоке буфер шифрования 256 опустошается» если (ход.набрано не меньше 15) то (результат.буфер равен пустой список) иначе да
  обеспечивает «на полном блоке счёт набранного 256 обнуляется» если (ход.набрано не меньше 15) то (результат.набрано равен 0) иначе да
  обеспечивает «до полного блока выход шифрования 256 не трогается» если (не (ход.набрано не меньше 15)) то (результат.выход равно ход.выход) иначе да
  обеспечивает «до полного блока сцепка шифрования 256 не трогается» если (не (ход.набрано не меньше 15)) то (результат.сцепка равно ход.сцепка) иначе да
  пример «Первый байт CBC-AES256 (NIST SP 800-38A, F.2.5) копится в буфере»
    дано ход равно вариант «Ход CBC» с ключ равным [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125,
      119, 129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244] и сцепка равным [0, 1, 2, 3, 4, 5, 6,
      7, 8, 9, 10, 11, 12, 13, 14, 15] и буфер равным пустой список и набрано равным 0 и выход равным пустой список
    дано байт равно 107
    ожидается вариант «Ход CBC» с ключ равным [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119,
      129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244] и сцепка равным [0, 1, 2, 3, 4, 5, 6, 7, 8,
      9, 10, 11, 12, 13, 14, 15] и буфер равным [107] и набрано равным 1 и выход равным пустой список

тотальная функция «Шаг CBC назад 256»
  принимает ход: «Ход CBC», байт: число
  возвращает «Ход CBC»
  обеспечивает «сцепка остаётся блоком в шестнадцать байтов» (длина результат.сцепка) равен 16
  обеспечивает «ключ не трогается» результат.ключ равно ход.ключ
  обеспечивает «до полного блока счёт набранного 256 растёт на единицу» если (не (ход.набрано не меньше 15)) то (результат.набрано равен (ход.набрано плюс 1)) иначе да
  обеспечивает «до полного блока буфер 256 прирастает байтом» если (не (ход.набрано не меньше 15)) то (результат.буфер равен (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  обеспечивает «на полном блоке буфер расшифровки 256 опустошается» если (ход.набрано не меньше 15) то (результат.буфер равен пустой список) иначе да
  обеспечивает «на полном блоке счёт набранного расшифровки 256 обнуляется» если (ход.набрано не меньше 15) то (результат.набрано равен 0) иначе да
  обеспечивает «до полного блока выход расшифровки 256 не трогается» если (не (ход.набрано не меньше 15)) то (результат.выход равно ход.выход) иначе да
  обеспечивает «до полного блока сцепка расшифровки 256 не трогается» если (не (ход.набрано не меньше 15)) то (результат.сцепка равно ход.сцепка) иначе да
  обеспечивает «на полном блоке сцепкой расшифровки 256 становится сам шифроблок» если (ход.набрано не меньше 15) то (результат.сцепка равно (добавить («Свести к байту» от байт) к ход.буфер)) иначе да
  пример «Первый байт шифротекста CBC-AES256 (F.2.6) копится в буфере»
    дано ход равно вариант «Ход CBC» с ключ равным [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125,
      119, 129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244] и сцепка равным [0, 1, 2, 3, 4, 5, 6,
      7, 8, 9, 10, 11, 12, 13, 14, 15] и буфер равным пустой список и набрано равным 0 и выход равным пустой список
    дано байт равно 245
    ожидается вариант «Ход CBC» с ключ равным [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119,
      129, 31, 53, 44, 7, 59, 97, 8, 215, 45, 152, 16, 163, 9, 20, 223, 244] и сцепка равным [0, 1, 2, 3, 4, 5, 6, 7, 8,
      9, 10, 11, 12, 13, 14, 15] и буфер равным [245] и набрано равным 1 и выход равным пустой список

тотальная функция «Шифр CBC 256»
  принимает ключ: список числа, вектор: список числа, текст: список числа
  возвращает список числа
  обеспечивает «на целом числе блоков шифротекст ровно той же длины, что и открытый текст» (не (((длина текст) остаток от 16) равен 0)) или ((длина результат) равен (длина текст))
  пример «Пустому тексту — пустой шифротекст»
    дано ключ равно [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97,
      8, 215, 45, 152, 16, 163, 9, 20, 223, 244]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано текст равно пустой список
    ожидается пустой список

тотальная функция «Расшифровка CBC 256 начисто»
  принимает ключ: список числа, вектор: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «на целом числе блоков расшифрованное ровно той же длины, что и шифротекст» (не (((длина шифротекст) остаток от 16) равен 0)) или ((длина результат) равен (длина шифротекст))
  пример «Все четыре блока CBC-AES256 из NIST SP 800-38A, F.2.6»
    дано ключ равно [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97,
      8, 215, 45, 152, 16, 163, 9, 20, 223, 244]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано шифротекст равно [245, 140, 76, 4, 214, 229, 241, 186, 119, 158, 171, 251, 95, 123, 251, 214, 156, 252, 78,
      150, 126, 219, 128, 141, 103, 159, 119, 123, 198, 112, 44, 125, 57, 242, 51, 105, 169, 217, 186, 207, 165, 48,
      226, 99, 4, 35, 20, 97, 178, 235, 5, 226, 195, 155, 233, 252, 218, 108, 25, 7, 140, 106, 157, 27]
    ожидается [107, 193, 190, 226, 46, 64, 159, 150, 233, 61, 126, 17, 115, 147, 23, 42, 174, 45, 138, 87, 30, 3, 172,
      156, 158, 183, 111, 172, 69, 175, 142, 81, 48, 200, 28, 70, 163, 92, 228, 17, 229, 251, 193, 25, 26, 10, 82, 239,
      246, 159, 36, 69, 223, 79, 155, 23, 173, 43, 65, 123, 230, 108, 55, 16]

тотальная функция «Зашифровать CBC 256»
  принимает ключ: список числа, вектор: список числа, текст: список числа
  возвращает список числа
  обеспечивает «шифротекст ложится блоками нацело» ((длина результат) остаток от 16) равен 0
  пример «Пять байтов уходят в один блок»
    дано ключ равно [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97,
      8, 215, 45, 152, 16, 163, 9, 20, 223, 244]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано текст равно [1, 2, 3, 4, 5]
    ожидается [36, 100, 216, 41, 27, 59, 0, 233, 62, 81, 217, 6, 102, 54, 124, 224]

тотальная функция «Расшифровать CBC 256»
  принимает ключ: список числа, вектор: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «расшифрованное не длиннее шифротекста» (длина результат) не больше (длина шифротекст)
  пример «Тот же блок в обратную сторону: расшифровка зашифрованного возвращает исходное»
    дано ключ равно [96, 61, 235, 16, 21, 202, 113, 190, 43, 115, 174, 240, 133, 125, 119, 129, 31, 53, 44, 7, 59, 97,
      8, 215, 45, 152, 16, 163, 9, 20, 223, 244]
    дано вектор равно [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
    дано шифротекст равно [36, 100, 216, 41, 27, 59, 0, 233, 62, 81, 217, 6, 102, 54, 124, 224]
    ожидается [1, 2, 3, 4, 5]

тотальная функция «Ключ хеша 256»
  принимает ключ: список числа
  возвращает список числа
  обеспечивает «ключ поля — блок в шестнадцать байтов» (длина результат) равен 16
  пример «Нулевой ключ в тридцать два байта даёт H = dc95c078a2408989ad48a21492842087 (SP 800-38D, Test Case 13)»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [220, 149, 192, 120, 162, 64, 137, 137, 173, 72, 162, 20, 146, 132, 32, 135]

тотальная функция «Шаг гаммы GCM 256»
  принимает ход: «Ход гаммы GCM», байт: число
  возвращает «Ход гаммы GCM»
  обеспечивает «выход удлиняется ровно на байт» (длина результат.выход) равен ((длина ход.выход) плюс 1)
  обеспечивает «место в гамме не выходит за блок» (результат.позиция не меньше 1) и притом (результат.позиция не больше 16)
  обеспечивает «до конца блока место 256 растёт на единицу» если (не (ход.позиция не меньше 16)) то (результат.позиция равен (ход.позиция плюс 1)) иначе да
  обеспечивает «на конце блока место 256 сбрасывается в единицу» если (ход.позиция не меньше 16) то (результат.позиция равен 1) иначе да
  обеспечивает «ключ гаммы GCM 256 не трогается» результат.ключ равно ход.ключ
  обеспечивает «до конца блока счётчик GCM 256 не трогается» если (не (ход.позиция не меньше 16)) то (результат.счётчик равно ход.счётчик) иначе да
  обеспечивает «до конца блока гамма GCM 256 не пересчитывается» если (не (ход.позиция не меньше 16)) то (результат.гамма равно ход.гамма) иначе да
  обеспечивает «на конце блока счётчик GCM 256 прирастает» если (ход.позиция не меньше 16) то (результат.счётчик равно («Прибавить единицу по младшим четырём» от ход.счётчик)) иначе да
  пример «Второй байт гаммы GCM-AES256 (SP 800-38D, Test Case 14)»
    дано ход равно вариант «Ход гаммы GCM» с ключ равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
      0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] и счётчик равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
      2] и гамма равным [206, 167, 64, 61, 77, 96, 107, 110, 7, 78, 197, 211, 186, 243, 157,
      24] и позиция равным 1 и выход равным [206]
    дано байт равно 0
    ожидается вариант «Ход гаммы GCM» с ключ равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
      0, 0, 0, 0, 0, 0, 0, 0, 0, 0] и счётчик равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2] и гамма равным [
      206, 167, 64, 61, 77, 96, 107, 110, 7, 78, 197, 211, 186, 243, 157,
      24] и позиция равным 2 и выход равным [206, 167]

тотальная функция «Шифр GCTR 256»
  принимает ключ: список числа, счётчик: список числа, текст: список числа
  возвращает список числа
  обеспечивает «шифротекст ровно той же длины, что и открытый текст» (длина результат) равен (длина текст)

тотальная функция «Начальный счётчик 256»
  принимает ключ: список числа, вектор: список числа
  возвращает список числа
  обеспечивает «начальный счётчик — блок в шестнадцать байтов» (длина результат) равен 16
  обеспечивает «вектору в двенадцать байтов приписана единица» если ((длина вектор) равен 12) то (результат равен («Досыпать байты» от («Досыпать байты» от вектор и («Нули» от 3)) и [1])) иначе да
  пример «Вектор в двенадцать байтов: к нему приписана единица»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    ожидается [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]

тотальная функция «Тег GCM 256»
  принимает ключ: список числа, вектор: список числа, доп: список числа, шифротекст: список числа
  возвращает список числа
  обеспечивает «тег — ровно шестнадцать байтов» (длина результат) равен 16
  пример «Test Case 13 (SP 800-38D): нулевой ключ в тридцать два байта, пустые данные, пустой шифротекст»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано доп равно пустой список
    дано шифротекст равно пустой список
    ожидается [83, 15, 138, 251, 199, 69, 54, 185, 169, 99, 180, 241, 196, 203, 115, 139]

тотальная функция «Зашифровать GCM 256»
  принимает ключ: список числа, вектор: список числа, доп: список числа, текст: список числа
  возвращает «Печать GCM»
  обеспечивает «тег — ровно шестнадцать байтов» (длина результат.тег) равен 16
  обеспечивает «шифротекст ровно той же длины, что и открытый текст» (длина результат.шифротекст) равен (длина текст)
  пример «Test Case 13 (SP 800-38D): пустой текст, пустые данные, нулевой ключ в тридцать два байта»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано доп равно пустой список
    дано текст равно пустой список
    ожидается вариант «Печать GCM» с шифротекст равным пустой список и тег равным [83, 15, 138, 251, 199, 69, 54, 185,
      169, 99, 180, 241, 196, 203, 115, 139]

тотальная функция «Расшифровать GCM 256»
  принимает ключ: список числа, вектор: список числа, доп: список числа, шифротекст: список числа, тег: список числа
  возвращает «Исход GCM»
  обеспечивает «при отказе открытого текста не выдаётся» («Расшифровано ли» от результат) или ((длина («Текст исхода» от результат)) равен 0)
  обеспечивает «при успехе открытый текст той же длины, что и шифротекст» не («Расшифровано ли» от результат) или ((длина («Текст исхода» от результат)) равен (длина шифротекст))
  пример «Test Case 14 в обратную сторону: тег сошёлся, текст выдан»
    дано ключ равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано вектор равно [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
    дано доп равно пустой список
    дано шифротекст равно [206, 167, 64, 61, 77, 96, 107, 110, 7, 78, 197, 211, 186, 243, 157, 24]
    дано тег равно [208, 209, 200, 167, 153, 153, 107, 240, 38, 91, 152, 181, 212, 138, 185, 25]
    ожидается вариант «Расшифровано» с текст равным [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

тотальная функция «Байт двумя знаками»
  принимает байт: число
  возвращает строка
  обеспечивает «байт печатается ровно двумя знаками» (длина результат) равен 2
  пример «Ноль»
    дано байт равно 0
    ожидается "00"

тотальная функция «Байты шестнадцатеричной строкой»
  принимает байты: список числа
  возвращает строка
  обеспечивает «на каждый байт — по два знака» (длина результат) равен ((длина байты) умножить на 2)
  пример «Пусто»
    дано байты равно пустой список
    ожидается ""