MSF and type SCT annotations

[sarranz]

This gives an error

fn extra_msf_swap(#[msf, public] reg u64 x) {}

and it makes sense. But this doesn't

fn extra_msf_poly(#[poly=t, msf] reg u64 x) {}

Is this on purpose?

[vbgl]

No. Not on purpose. The error comes from the fact that public and msf are incompatible annotations. Do you think they should be allowed both?

[sarranz]

I don't think it makes a big difference either way. I initially expected both to be rejected. Do we get any benefit from specifying the confidentiality type of an MSF?

[vbgl]

Maybe the confusion comes from the fact that the SCT-checker ignores the poly=t part, that it does not understand.