Тип ^:
Cryptol> :t (^)
(^) : {a} (Logic a) => a -> a -> a
Обратите внимание, что оба аргумента должны быть абсолютно одинаковыми.Вы получаете ошибку типа, потому что [2] отличается от [8];как они различаются по размеру.В отличие от Verilog, Cryptol не будет «накладывать» вещи неявно, и я думаю, что Cryptol определенно поступает правильно.Программисты Verilog могут присоединиться к бесчисленным ошибкам, которые у них возникли из-за неявного приведения.
Все такие приведения в Cryptol должны быть явными.
Типичным способом решения этой ситуации в Cryptol является использованиеполиморфная константа zero:
Cryptol> :t zero
zero : {a} (Zero a) => a
Значение zero населяет все типы (вы можете пока игнорировать ограничение Zero), и, как вы можете себе представить, это "правильное" значение заполнения вэтот случай.Итак, вы бы определили свою функцию следующим образом:
Cryptol> let test(x:[2], y:[8]) = (zero#x)^y
Cryptol> :t test
test : ([2], [8]) -> [8]
И использовали бы ее так:
Cryptol> test (1, 5)
0x04
И если бы вы по какой-то причине захотели заполнить справа, вы быdo:
Cryptol> let test(x:[2], y:[8]) = (x#zero)^y
Cryptol> test(1,5)
0x45
Таким образом, все явно, и вам не нужно знать все магические правила о том, как вещи дополняются, чтобы получить нужный размер.
Если вы хотитеполучить реальную фантазию, тогда вы можете сделать:
Cryptol> let test(x, y) = (zero#x)^(zero#y)
Cryptol> :t test
test : {n, m, i, j, a} (Logic a, Zero a, m + i == n + j, fin n,
fin m) =>
([i]a, [j]a) -> [m + i]a
Теперь этот тип выглядит немного страшно;но, по сути, он говорит вам, что вы можете дать ему аргументы любого размера, и он будет действителен для любого другого размера, при условии, что новый размер больше, чем максимум двух, которые вы дали.Конечно, этот предполагаемый размер гораздо более полиморфен, чем вы, возможно, заботитесь;так что вы можете дать ему что-то более читабельное:
test : {m, n} (fin m, fin n) => [m] -> [n] -> [max m n]
test x y = (zero#x) ^ (zero#y)
Я считаю, что это отлично отражает ваши намерения.Обратите внимание, как cryptol обеспечит конечность ваших входных данных, и вы получите максимум из двух указанных размеров.
Возвращаясь к вашему примеру, Cryptol говорит вам, что для умножения на 16 вам нужно как минимум 5 бит,и, таким образом, 2>=5 не является удовлетворительным.Это немного загадочно, но возникает из-за использования литералов, которые полиморфно типизированы.Вы можете использовать трюк zero для решения проблемы таким же образом, как и раньше:
Cryptol> let shift (v, s:[2]) = v >>> ((zero#s)*16+8)
[warning] at <interactive>:1:32--1:38:
Defaulting type argument 'front' of '(#)' to 3
Но обратите внимание, как cryptol предупреждает вас о типе zero, который там используется, так как тип>>> является достаточно полиморфным, чтобы допускать сдвиги / повороты разных размеров:
Cryptol> :t (>>>)
(>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
В этих случаях Cryptol выберет наименьший возможный размер по умолчанию, глядя на выражения.К сожалению, здесь это не так.Выбрав размер 3 для zero, вы получите сдвиг 5 бит, но ваше выражение может вывести максимальное значение 3*16+8=56, для представления которого требуется не менее 6 бит.Обратите внимание, что Cryptol использует только минимальный размер, необходимый для умножения, и не заботится о переполнениях!Вот почему важно обращать внимание на такие предупреждения.
Чтобы было ясно: Cryptol сделал правильную вещь в соответствии с правилами языка о том, как работает вывод типов, но в итоге он выбрал размерэто слишком мало для того, что вы хотели сделать.
Итак, вы должны написать свой shift следующим образом:
Cryptol> let shift (v, s:[2]) = v >>> (((zero:[4])#s)*16+8)
Cryptol> :t shift
shift : {n, a} (fin n) => ([n]a, [2]) -> [n]a
Здесь важно убедиться, что выражение s*16+8 будет соответствовать конечному результату, и, поскольку s имеет ширину всего 2 бита, наибольшее значение будет 56, как обсуждалось выше, для представления которого требуется по меньшей мере 6 бит.Вот почему я выбрал [4] в качестве размера zero.
Мораль этой истории заключается в том, что вы всегда должны четко указывать размеры ваших битвекторов, а Cryptol предоставит вам правильную структуручтобы выразить свои ограничения полиморфным способом, позволяя повторное использование кода без двусмысленности, избегая многих ловушек Verilog и других подобных языков.