Vincent Laporte

The compiler does that for you. ~~~ /* --------------------------------------------------- */ inline fn f (reg ptr u64[1] a, reg ptr u64[1] scratchpad) -> reg ptr u64[1], reg ptr u64[1] { reg...

Do you think your program can be compiled? What assembly code do you expect to be generated?

Yes. If you want 8-bit registers, you should declare `reg u8` variables. `bool` are one bit.

Could this kind of error be caught earlier? Say by some type-checking pass? Otherwise, you have the name of the function and the name of the argument. This can be...

Also, it seems hard to blame a particular instruction: there might be a long sequence of assignments and array slicing (or even a DAG) inducing the aliasing constraint between a...

Here is an example. Which line would you like to blame? ~~~ fn f(reg ptr u64[1] arg) -> reg u64 { stack u64[1] s; reg ptr u64[1] x y; reg...

I’m not convinced that the location reported by the Coq checker is “the right one”. IMHO, pointing to a particular instruction might be misleading.

Yes, the type checker should enforce that the given signature is correct.

I’m going to rebase…

CI is happy. Let’s wait for feedback from Jasmin users.