@centril what isn't clear about https://github.com/rust-lang/rust/issues/56292#issuecomment-442561265 ?
WASM does not have signed or unsigned integers, it just has bag of bits that are integers
@Dan Gohman explained here https://github.com/rust-lang/rust/issues/56292#issuecomment-442561265 that WASM checks for overflow using
gt_u, which means that this check interprets the bits as an unsigned integer
it has signed and unsigned integer operations (for those where it makes a difference)
@gnzlbg the operational semantics of WASM does not state whether
delta < 0 is permitted or not
If wasm interprets delta as unsigned, then it does not have to state that AFAICT because it always holds ?
@gnzlbg to frame it in @RalfJ's terms, I didn't see that it states whether the concatenation is interpreted in terms of signed or unsigned integer operations or not
I would expect that it is unsigned; but there's doubt here imo
I think that's what @Dan Gohman was hinting at when they said
gt_u is used.
in particular the phrasing "grow" and "append" suggest >= but that's not a formal semantics :P
gt_u is the "greater-than unsigned" operation
@gnzlbg ye; sadly I didn't find the OCaml code well documented or readable
FWIW the spec isn't readable either, it's the only spec I actually had to send multiple PRs to because I had no idea what it was trying to say
There are multiple sources of truth that sometimes are contradictory, etc.
@gnzlbg the notation wrt. operational semantics is somewhat nonstandard
I'm so happy they even have a normative operational semantics
anyways; by keeping it
usize, we at least can rule out some bugs even if WASM permits more
Basically, the word of the implementors is worth a bit more than what's on the spec
@RalfJ this is so true; it's much more than you can usually expect
The problem is that, if the spec is ambiguous enough, people might decide to recycle these to allow for shrinking memory in the future
would be nice to formalize this in Agda
@gnzlbg we can add another function in such a case can we not?
yeah, but honestly, if this is an issue, then we should just file a github issue with the wasm spec
they tend to clarify these things pretty quickly and amend the spec as necessary
@gnzlbg this is why I suggested talking to the WASM folks on the issue
but if I can just file a GitHub issue then ill do that
Reading the semantics: they say "Either, try growing mem by n pages:"
growing seems to imply that the number of pages before has to be less or equal to the number of pages afterwards
@gnzlbg yes, however, "append" and "grow" are not defined terms
in any case, if that fails, this returns -1
@gnzlbg sure, I agree that it implies that; but implication is not certainty
still, for Rust this doesn't help much, it still doesn't really tell us whether this has to be a signed or unsigned integer type
If len is larger than 2^16, then fail.
I guess that's where Dan meant that the ML implementation uses
Let len be n added to the length of meminst.𝖽𝖺𝗍𝖺 divided by the page size 64Ki.
The question is, how is this Add works for both signed and unsigned integers the same.
len added, is it a signed or unsigned add ? I don't remember if there was a difference here.