Jean-Christophe Léchenet
Jean-Christophe Léchenet
I'd say line `x[0:1] = y[0:1]` (and this is the line reported by the Coq verifier if I disable the check in the OCaml code).
But once again, the error reported by the OCaml code is probably clearer for the user than the generic "regions are distinct" error reported by the Coq code.
Actually, I see two more solutions: - the OCaml code prints a warning and the Coq code triggers the error, thus we have both pieces of information - in Coq...
PR https://github.com/jasmin-lang/jasmin/pull/60 adds the function name and location. I leave this PR open, because we may want an even clearer message.
Benjamin's remark: we should update the type checker!
It should allow to make things cleaner and nicer.
(this was first observed by Ethan in https://github.com/ethanlee515/jasmin-dilithium)
This also gives an assert false in the checker. But I think it's just because of `(256u) #ADD` that is not supported.
Similar problem with the following piece of code ``` inline fn sum (reg u64[2] a) -> reg ptr u64 { stack u64 r; r = a[0]; r += a[1]; return...