Array copy specification potential incorrect mutable assertion

[CharlieTap]

I think there may be a mistake in the array.copy execution spec:

If we assume x is the destination array and y is the src array (because the steps set on x and get from y), then x must the array that has to be mutable. However the first 5 steps involve expanding the defined type of y and asserting that its a mutable array? but we only read from y?

[rossberg]

The 𝑚𝑢𝑡 in step 5 is a syntax variable (as can be determined from the type font), standing for whatever mutability specifier that array type has. If you click on it, you can see that it can be either const or var. Admittedly, the use of "𝑚𝑢𝑡" for this is a bit confusing, and I am tempted to change it, but it has existed since globals in Wasm 1.0.

[CharlieTap]

Ah okay, out of interest whats the intention with declaring mut here but not during the expansion of defined types in other instructions execution, for example array.new_fixed is also an array but it doesn't mention mut ?

[rossberg]

That rule is using 𝑓𝑡, matching the entire field type, which syntactically includes mutability (𝑓𝑖𝑒𝑙𝑑𝑡𝑦𝑝𝑒 ::= 𝑚𝑢𝑡 𝑠𝑡𝑜𝑟𝑎𝑔𝑒𝑡𝑦𝑝𝑒). The array.copy rule o.t.o.h. needs the storage type 𝑠𝑡 later on, so decomposes the pattern match into smaller pieces.

[CharlieTap]

Thank you thats super useful and you've indirectly answered another question I had with that 😅