[spec] Prevent possible index overflow in typing rule for module instances

[rossberg]

Fixes #2191. @raoxiaojia, PTAL.

[raoxiaojia]

There are some off-by-1 errors, and the prose seems to disagree with the later spectec edits on the intention of k.

Both sources of prose edits (L738 and L800) say k is smaller than the total number of functions, which means the upper limit of k is the largest representable index. If that is the intention, then L802 needs to be k := $min(|funcaddr*|, 2^32)-1 (-1 outside the min), and L767 needs to be strict inequality k < |\funcaddr^\ast| to agree with the prose (and the spectec sources need to be similarly editted).

However, both the latex edits and prose edit seems to strongly suggest otherwise that k is intended to be the number of entries eventually in C.refs (i.e. the length). If that is the case, then the prose needs to become 'not greater than', L802 need to be k := $min(|funcaddr*|, 2^32) (without the -1), and L790 needs to gain a -1.

Either is fine! My guess is that the latter interpretation is closer to what you have in mind, but I don't want to speculate too much.

[raoxiaojia]

Thanks, it is explained very clearly! There are some nit about off-by-1 errors which I left an inline note there.

[raoxiaojia]

Oh hmm, I realised that this might be more involved than I originally thought. spectec's list syntax is defined so that the length of list is strictly below 2^32:

spec/specification/wasm-3.0/1.1-syntax.values.spectec

Line 84 in 86477a3

syntax list(syntax X) = X* -- if |X*| < $(2^32)

. That would mean that the longest a list can be is 2^32-1, which means that the largest representable index is actually 2^32-2? My understanding for the above comment was based on the (incorrect) reading that the max possible length of a list is 2^32 instead of 2^32-1.

Let me know if I've read anything else incorrectly here.

[rossberg]

Thanks, fixed the off-by-ones (I believe).

Yeah, lists can only have a length of at most 2^32-1 elements, simply because the length is encoded as a u32 in the binary format. But indices can actually address one element past that, syntactically speaking. That may feel a bit odd, but is not a problem I think?

[raoxiaojia]

I think the prose at L800 needs a similar 'smaller than' -> 'at most' change, and everything else looks correct now.
Actually it might be all fine, the 'smaller than' at L800 is talking about C.refs.

Yeah, lists can only have a length of at most 2^32-1 elements, simply because the length is encoded as a u32 in the binary format. But indices can actually address one element past that, syntactically speaking. That may feel a bit odd, but is not a problem I think?

Nothing I can immediately think of, but it's a good update for my mental model. I'll keep it in mind when I try to do a idx lookup from a list in the future.

Yeah it feels slightly odd, but I don't see a way to restrict the idx bound cleanly either. Probably fine to leave it as is unless there's a genuine soundness issue somewhere.

[rossberg]

I'd argue that L800 is right, since that's explaining what k "allows" (over not having it in the rule). It doesn't say that it has to be smaller.

Re idx: in general, you can always represent index values that are OOB, so this one extreme case isn't even all that special.

[raoxiaojia]

Indeed, agreed to both points!