[spec] Can memory.grow take n < 0 ?

[Centril]

Reading the operational semantics of memory.grow it isn't clear whether you can shrink the amount of memory with that instruction (the meaning of "grow" and "append" isn't detailed but once can guess what it means...).

Similarly, reading growmem does not bring clarity; I didn't see the syntax meminst.data (0x00)n⋅64Ki defined anywhere; I assume it means that meminst.data is concatenated with (0x00)n⋅64Ki but it would be nice to make this clearer wrt. behavior and inductively define the operation A B.

cc rust-lang/rust#56292
Some advice would be good. :)

[gnzlbg]

In particular growmem states:

3. Let len be n added to the length of meminst.𝖽𝖺𝗍𝖺 divided by the page size 64Ki.

Where "added" works for both signed and unsigned integers, but "divided" does not specify if a signed / unsigned dive operation is performed. And the check for "overflow" happens afterwards:

4. If len is larger than 2^16, then fail.

So if n is either large enough or negative, depending on whether one interprets its bits as a signed or unsigned integer, the addition of step 3 can wrap around and be smaller than 2^16, shrinking the allocation.

Also, in step 3, "is larger than", does not specify whether the greater than signed or unsigned instruction is used.

The growmem section does not specify the types of n, len, etc. so it is also a bit unclear to me whether we are talking about i32 here or not - probably yes, otherwise 2^16 does not make much sense.

[sunfishcode]

For reference, the design PR where resize_memory was renamed to grow_memory, and the delta was made explicitly unsigned, with the intent that if shrinking should ever be supported, it should be a different operation, is WebAssembly/design#389.

[binji]

Runtime integer values are always stored on the execution stack unsigned, see the definition of Values here, which references the definition of integers here:

The latter class defines uninterpreted integers, whose signedness interpretation can vary depending on context. In the abstract syntax, they are represented as unsigned values. However, some operations convert them to signed based on a two’s complement interpretation.

You can see an example of this in the definition of i32.gt_s.

Where "added" works for both signed and unsigned integers, but "divided" does not specify if a signed / unsigned dive operation is performed.

The numerics in the formal syntax always use the standard mathematical syntax. Unsigned integer division, for example, is defined like this: trunc(i1/i2)

Similarly, none of the numbers in the formal definitions use modular arithmetic (you can see an example of how that would be specified in i32.add) so it is not possible for them to wrap around.

I didn't see the syntax meminst.data (0x00)n⋅64Ki defined anywhere; I assume it means that meminst.data is concatenated with (0x00)n⋅64Ki but it would be nice to make this clearer wrt. behavior and inductively define the operation A B.

I don't see the definition of that either, though perhaps I missed it. It is indeed meant to be a concatenation.

[Centril]

@binji Thanks for the details! :)

Perhaps meminst.data ++ (0x00)n⋅64Ki would be clearer?

[binji]

For this example, maybe, but this form of concatenation is used pervasively elsewhere in the spec (see the binary section for example) where it would be visually very noisy to do this.

[Centril]

@binji ah; makes sense -- how about adding A B to the list of conventions somewhere instead?

[binji]

Sounds good to me, but I'll defer to @rossberg for that :-)

[rossberg]

Since sequences are simply represented by iterations of a certain phrase class, juxtaposition already is concatenation by construction. Hence no further convention needs to be defined. If that is non-obvious we could add a note, but it seems like everybody read it correctly?

[Centril]

@rossberg I do think someone who is not familiar with reading literature on operational semantics could be confused so it seems noteworthy with a sentence somewhere. :) I understood what A B meant only from the context since it can also be function application in other contexts.

[binji]

Perhaps the formal semantics could be clearer, but I think the meaning of "grow" and "append" in the prose would have to be awkwardly contorted to allow shrinking. As described here the purpose of the prose to provide the intuitive meaning, which seems to have been understood here.

Closing, but feel free to reopen if you feel strongly here.

[xtuc]

Now that we switched to the WebIDL specification, the {Table,Memory}.grow takes an unsigned 32 bits int.