1

我尝试使用 Cryptol 实现 MAA 算法。这是我到目前为止所做的，但我并不幸运。有任何想法吗？

main: ([32], [32]) -> [32]
main  (x , y)  =  add (x , y)x
           where x =  (take`{16} xy, drop`{16} xy)
          where xy = mul1 (x , y)      

mul1: ([32] ,[32])  -> [32]
mul1  (x , y) = xy
          where xy = x * y


add: ([16] ,[16])  -> [16]
add  (x , y) = xy
          where xy = x + y
4

1 回答 1

0

你的主要有一些错误。

  • add (x , y)x 说什么？争论太多
  • main (x , y) = ...那么where x = ... 现在 x 等于多少呢？如果您能提供帮助，请不要隐藏变量名。
  • where x = ...并where xy = ... 使用单个 `where 而不是嵌套只是为了保持清洁，嗯？

最后是类型错误。Add 给你一个 16 位数字（查看类型签名），所以它的结果也不能是main谁的类型的结果表明它返回一个 32 位数字。32 不等于 16。我已经解决了这个问题和上述问题，只需更改类型，main但这可能不是您想要的，因此您需要在此处添加您想要的任何逻辑（例如：零扩展或符号扩展？）。

代码：

main: ([32], [32]) -> [16]
main  (x , y)  =  add xy16
           where xy16 =  (take`{16} xy, drop`{16} xy)
                 xy = mul1 (x , y)

mul1: ([32] ,[32])  -> [32]
mul1  (x , y) = xy
          where xy = x * y


add: ([16] ,[16])  -> [16]
add  (x , y) = xy
          where xy = x + y

现在大概这是您原始问题的简化版本，但如果没有注意到您真的不需要定义一个函数add来使用+，同样适用于mul. 此外，您不需要显式类型注释take，drop因为可以推断出这些类型。例如：

main2 : [32] -> [32] -> [16]
main2 x y = take xy + drop xy where xy = x * y

然后我们可以做显而易见的事情：

Main> :prove \x y -> main (x,y) == main2 x y
Q.E.D.
于 2018-07-13T13:26:30.707 回答