Make Nativecode.string_of_kn really injective for good.

[ppedrot]

This is critical for soundness of native compilation, as otherwise a definition may overwrite another one. This was not the first time such a problem arised, see 244d7a9.

Fixes #22364: string_of_kn is non-injective.

[SkySkimmer]

Is this actually injective? seems like both foo_.bar and foo._bar produce foo___bar no?

[JasonGross]

What about mapping _ to _u and . to _d

[ppedrot]

Is this actually injective?

You're right. I think that for this kind of property I can only trust formal proofs...

[ppedrot]

Note that there is also a potential issue with the encoding of bound module paths, we prefix them with X and just take the underlying name, this doesn't look very injective to me, but maybe it's not exploitable.

[JasonGross]

Note that there is also a potential issue with the encoding of bound module paths, we prefix them with X and just take the underlying name, this doesn't look very injective to me, but maybe it's not exploitable.

If we follow my suggestion of having all escapes be _ followed by something that is not _, we can prefix them with _X

[ppedrot]

I'll do something along those lines, it's indeed safer.

[ppedrot]

This should be ok now. (There is still something potentially fishy with the bound module names unique identifiers, but it's not clear to me how we can be in a situation where both are accessible to the native compiler. Any idea to break that?)

[JasonGross]

how we can be in a situation where both are accessible to the native compiler. Any idea to break that?

Is it not possible to trigger native compute inside a functor?

[ppedrot]

AFAIU the only way to have two reachable bound module names with different ids is via module substitution, and at this point we don't care anymore about toplevel compilation of constants in native. (Rocq prevents you to syntactically declare twice the same name for module parameters.)