Named results shadow parameter names
If the result of a function is named with the same name as a parameter of the function, it becomes impossible to refer to this parameter in the ensures. I think it should be forbidden to give the result the same name as a parameter.
let samename (x:uint64) : (x:uint64)
requires { x = 1 }
ensures { x = 3 }
= 3