1

如何对不同宽度的值进行算术运算？在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 位值。

4

1 回答 1

2

的类型^是：

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

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

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 和其他类似的语言。

于 2018-10-27T17:10:39.453 回答