[spec] Update syntax spec for memory64

[sbc100]

This is just a start. I've made some updates to instructions.rst and types.rst but could use some pointers so uploading now to get feedback.

[sbc100]

This PR is now just missing validation and execution changes.

[sbc100]

All comments addressed.

The Execution and Validation section are still not complete. I updated these for just memory.copy to see if I'm on the right track? Once I get memory.copy right I'll update the rest.

[sbc100]

Some more suggestions for tweaks.

Before continuing to spell out execution and validation, I'd merge the multi-memory repo into this one, so that you don't have to redo everything later (with merge conflicts everywhere). (And please merge it without squashing commits, otherwise we'll have to resolve possible conflicts over each time.) I'd also suggest doing all that in a separate PR.

Sure thing. However the multi-memory repo itself looks like its fairly out of date with upstream, resulting is a fair amount of conflicts. Would you be able update the multi-memory repo first? (I tried myself and there were a fair few conflicts.. let me know if you would rather I try to take care of that too).

[rossberg]

Ah sorry. Instead of the multi-memory repo, you could merge the wasm-3.0 branch from the main repo, which already contains it, plus various other proposals (it is the staging ground for merging phase-4 proposals and is up-to-date with main).

[sbc100]

Ah sorry. Instead of the multi-memory repo, you could merge the wasm-3.0 branch from the main repo, which already contains it, plus various other proposals (it is the staging ground for merging phase-4 proposals and is up-to-date with main).

I'm having a little trouble with the wasm-3.0 branch merge for reasons that look unrelated to memoy64.

I think the reason is because i'm already caught up with the latest main changes but wasm-3.0 doesn't have all changes from main (e.g. https://github.com/WebAssembly/spec/pull/1751). Would it be possible to merge the latest changes from main into wasm-3.0, or should I rebase memory64 on top branch point of wasm-3.0 perhaps?

[rossberg]

Done, merged spec/main into wasm-3.0.

[sbc100]

I'm most of the way through the rebase onto wasm-3.0.

Would you be OK with land this change here on main and then I can cherry pick it over to my wasm-3.0 branch once that lands?

Any other feedback on the content of this PR?

[sbc100]

The merge of main with upstream/wasm-3.0 is now complete. See https://github.com/WebAssembly/memory64/tree/wasm-3.0.

This PR should now be on top of memory64/wasm3.0. Should I close this one and open another one, or first push and change the target branch to wasm-3.0?

[rossberg]

I'd avoid reopening a PR if possible. If you can rebase it, that seems highly preferable.

[sbc100]

This PR has now been updated to target the local wasm-3.0 branch.

The validation and execution sections still only contain updates for memory.copy. I will do the rest once we finish iterating on those.

[sbc100]

In addition to addressing feedback I also updated all he instruction validation rules.

AFAIK, that just leaves the completion of the execution section (in addition to any remaining feedback).

[sbc100]

I looked into updated the formal rules for memory.copy evaluation semantics. However, the end result looks like it will be quite verbose due to repeated conditions. @rossberg can you recommend a way to factor out the index type matching conditions? @tlively suggested using a locally defined helper function perhaps?

[rossberg]

The execution rules shouldn't actually need the side conditions on what the different it's are concretely. Execution does not depend on that, and we know that they match up due to validation. Leaving out the side conditions means the types exist, but we don't care what they are (here).

You can in fact do the same in the text, that is, remove the lookup of the memory types and just amend the existing type assertions on the operands to something like

"Assert: due to :ref:validation <valid-memory.copy>, a value of :ref:value type <syntax-valtype> :math:\X{it}_n is on the top of the stack, for some :ref:index type <syntax-idxtype> :math:\X{it}_n."

and so on.

[sbc100]

The execution rules shouldn't actually need the side conditions on what the different it's are concretely. Execution does not depend on that, and we know that they match up due to validation. Leaving out the side conditions means the types exist, but we don't care what they are (here).

You can in fact do the same in the text, that is, remove the lookup of the memory types and just amend the existing type assertions on the operands to something like

"Assert: due to :ref:validation <valid-memory.copy>, a value of :ref:value type <syntax-valtype> :math:\X{it}_n is on the top of the stack, for some :ref:index type <syntax-idxtype> :math:\X{it}_n."

and so on.

Do what should the stack look line in the memory.copy execution rules? Can I just refer directly to it_x it_y and it there?

[rossberg]

Yes, it would be just a variable in the pattern match.

[sbc100]

All execution rules updated. I think that everything now % feedback.