使用 Cryptol 实现 MAA 算法

Question

我尝试使用 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 

Answer 1

你的主要有一些错误。

• 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.