Typechecking semantics of multidimensional types

[Jozott00]

I think we haven't discussed the typechecking semantics for accessing multidimensional types yet.

Consider the following example:

register A: Bits<5>
register X: Bits<5><32>

function t1 -> Bits<32> = X(A)
function t2 -> Bits<32> = X(A as Bits<2>)
function t3 -> Bits<32> = X(A as Bits<3>)

Register X has two dimensions, with an index dimension of size 5. This size can’t be represented by a concrete type as it is no power of 2.

Now the question is how to check access to such a register. t1-3 are functions with different index access types:

• t1 has an index type of Bits<5>, which may also contain values up to 31.
• t2 has an index type of Bits<2>, with a maximum value of 3, so it is always in range.
• t3 has an index type of Bits<3>, with a maximum value of 7. This is the next fitting type that can hold all values that can be used to access the index dimension. However, it may also hold values 5-7 which are out of range.

I think t2 must be definitely valid. t3 must also be valid; otherwise, there would be no way to access the outermost dimension 4.
IMO t1 should be valid as well, because it doesn’t differ from t3 which could also be out of range. Additionally, the user didn’t specify any concrete type for the index, so a type error would be pretty confusing.

This leaves us in a state where out-of-range access isn’t statically prevented, which causes undefined behavior. In the case of registers, the user could specify annotations that define the behavior on out-of-range accesses (read and write), e.g. raising an exception or returning some computed value.
However, it is hard to specify such behavior for generic multi-dimensional types (other than registers).

What are your thoughts on this?