cryptol：具有不同宽度的算术

Question

如何对不同宽度的值进行运算？在 verilog 中，将 2 位与 8 位异或没有问题，但 cryptol 抱怨：

cryptol> let test(x: [2],y: [8]) = x ^ y

[error] at <interactive>:1:31--1:32:
  Type mismatch:
    Expected type: 2
    Inferred type: 8

我原来的问题：我想旋转 64 位值中的字节，要移动的字节数取决于两位输入。我很难让它工作：

cryptol> let shift (v, s:[2]) = v >>> (s*16+8)
[error] at <interactive>:1:5--1:38:
Unsolved constraint:
2 >= 5
  arising from
  use of literal or demoted expression
  at <interactive>:1:33--1:35

在解释器中，我可以删除 s 的类型规范，然后它就可以工作了，但是我需要从一个文件中得到它，并且 s 实际上是一个 2 位值。

Answer 1

^的类型是：

Cryptol> :t (^)
(^) : {a} (Logic a) => a -> a -> a

请注意，它要求两个参数完全相同。您收到类型错误是因为 [2] 与 [8] 不同；因为它们的大小不同。与 Verilog 不同，Cryptol 不会隐式 "pad" 事情，我认为 Cryptol 在这里做的事情绝对是正确的。 Verilog 程序员可以解决他们因隐式转换而产生的无数错误。

Cryptol 中的所有此类转换都必须是显式的。

在 Cryptol 中处理这种情况的典型方法是使用多态常量 zero:

Cryptol> :t zero
zero : {a} (Zero a) => a

值 zero 包含所有类型（您现在可以忽略 Zero 约束），您可以想象在这种情况下是 "right" 填充值。因此，您将函数定义为：

Cryptol> let test(x:[2], y:[8]) = (zero#x)^y
Cryptol> :t test
test : ([2], [8]) -> [8]

并像这样使用它：

Cryptol> test (1, 5)
0x04

如果你出于某种原因想在右边填充，你会这样做：

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 的类型，因为 >>> 的类型足够多态以允许不同的大小 shifts/rotates:

Cryptol> :t (>>>)
(>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a

在这些情况下，Cryptol 将通过查看表达式选择尽可能小的默认大小。不幸的是，它在这里做了错误的事情。通过为 zero 选择大小 3，你将有一个 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 和其他类似语言的许多缺陷。

cryptol：具有不同宽度的算术

cryptol: arithmetic with different width

cryptol