Implementing MAA algorithm using Cryptol

Question

I tried to implement the MAA algorithm using Cryptol. Here is what I did so far, but I was not lucky. Any ideas?

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

Your main has a few mistakes.

• add (x , y)x Say what? Too many arguments
• main (x , y) = ... and where x = ... Well what does x equal now? Don't shadow variable names if you can help it.
• where x = ... and where xy = ... Use a single `where instead of a nested just to keep things clean, eh?

Finally there is a type error. Add gives you a 16 bit number (look at the type signature) so it's result can not also be the result of main who's type indicates it returns a 32 bit number. 32 does not equal 16. I've fixed this, and the above, simply by changing the type of main but that likely isn't what you want, so you'll need to add whatever logic you desire here (ex: zero extend or sign extend?).

Code:

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

Now presumably this is a cut down version of your original problem, but if not notice you really don't need to define a function add just to use + and same goes for mul. Also you don't need the explicit type annotations on take and drop since those typed can be inferred. For example:

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

And then we can do the obvious:

Main> :prove \x y -> main (x,y) == main2 x y
Q.E.D.