[spec] Update syntax spec for memory64 #50

sbc100 · 2024-02-21T02:24:48Z

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.

document/core/syntax/types.rst

rossberg

FWIW, you can generally copy what's in the Overview pretty directly.

document/core/syntax/types.rst

document/core/syntax/instructions.rst

document/core/syntax/types.rst

sbc100 · 2024-05-29T00:09:25Z

This PR is now just missing validation and execution changes.

document/core/syntax/types.rst

document/core/text/modules.rst

document/core/text/types.rst

document/core/binary/types.rst

See #50 (comment)

sbc100 · 2024-05-30T15:16:34Z

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.

document/core/exec/instructions.rst

document/core/valid/instructions.rst

rossberg

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.

document/core/binary/types.rst

document/core/syntax/types.rst

document/core/text/modules.rst

document/core/text/types.rst

document/core/valid/instructions.rst

document/core/syntax/types.rst

document/core/exec/instructions.rst

sbc100 · 2024-05-30T21:34:24Z

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 · 2024-05-31T09:48:49Z

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 · 2024-06-03T22:24:22Z

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. WebAssembly/spec#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 · 2024-06-03T22:47:40Z

Done, merged spec/main into wasm-3.0.

sbc100 · 2024-06-06T00:39:43Z

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?

rossberg · 2024-06-12T07:29:22Z

document/core/text/types.rst

+
+Abbreviations
+.............
+


That is left a bit vague, intended to be applicable to a specific syntactic class (which currently only appears in the Latex source :) ) and otherwise "clear from context". As mentioned in my SpecTec presentation last week, I'd like to remove the handwaviness and make this more precise, but that doesn't have super-high priority.

document/core/text/types.rst

sbc100 · 2024-06-12T20:29:54Z

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 · 2024-06-13T08:27:01Z

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

I updated `instructions.rst` and make a start on `types.rst` but could use some help on how to parameterize `limits` on the index type.

sbc100 · 2024-06-18T20:53:26Z

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.

document/core/binary/instructions.rst

rossberg · 2024-06-20T08:34:45Z

document/core/exec/instructions.rst


-12. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+12. Let :math:`\X{it}_{min}` be ....?


Suggested change

12. Let :math:`\X{it}_{min}` be ....?

12. Let :math:`\X{it}_{\X{min}}` be ....?

And similarly in other places. Or perhaps name this one just plain "it"?

I would say "... be the :ref:minimum <aux-idxtype-min> of ...` and then define that as a convention in the syntax section for index types.

Done. Although I'm not sure how you would me to define aux-idxtype-min itself. Right now I've described it in prose but I imagine it warrants some kind of formal notation.

document/core/exec/instructions.rst

document/core/syntax/types.rst

document/core/text/modules.rst

document/core/valid/instructions.rst

document/core/exec/instructions.rst

sbc100 · 2024-06-24T23:29:40Z

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).

rossberg

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

Hm, I only see an update to memory.copy. Did you perhaps forget to push?

document/core/exec/instructions.rst

document/core/syntax/types.rst

document/core/valid/instructions.rst

rossberg · 2024-06-25T12:18:11Z

document/core/exec/instructions.rst


-21. Execute the instruction :math:`\MEMORYCOPY~x~y`.
+24. Execute the instruction :math:`\MEMORYCOPY~x~y`.

 .. math::


The formal rule here still needs the equivalent adjustments as the text.

sbc100 · 2024-06-26T22:16:10Z

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 · 2024-06-27T07:30:19Z

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 · 2024-06-27T15:22:23Z

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 · 2024-06-27T15:53:04Z

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

sbc100 · 2024-06-28T21:22:51Z

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

rossberg

LGTM % comments

document/core/exec/instructions.rst

document/core/valid/instructions.rst

sbc100 requested a review from rossberg February 21, 2024 06:43

sbc100 commented Feb 21, 2024

View reviewed changes

document/core/syntax/types.rst Outdated Show resolved Hide resolved

rossberg reviewed Feb 21, 2024

View reviewed changes

sbc100 mentioned this pull request May 17, 2024

Tracking issue for phase 4 advancement #43

Closed

14 tasks

sbc100 force-pushed the spec_syntax branch from 8e4bda6 to d039c0d Compare May 29, 2024 00:08

sbc100 force-pushed the spec_syntax branch 2 times, most recently from b3bba67 to e5fa979 Compare May 29, 2024 00:12

rossberg reviewed May 29, 2024

View reviewed changes

sbc100 force-pushed the spec_syntax branch from e5fa979 to 430df56 Compare May 29, 2024 16:51

rossberg reviewed May 29, 2024

View reviewed changes

document/core/binary/types.rst Outdated Show resolved Hide resolved

sbc100 added a commit that referenced this pull request May 30, 2024

Revert parameterization of limits that was added in #13.

6307764

See #50 (comment)

sbc100 mentioned this pull request May 30, 2024

Revert parameterization of limits that was added in #13. #59

Merged

sbc100 added a commit that referenced this pull request May 30, 2024

Revert parameterization of limits that was added in #13. (#59)

6f101d6

See #50 (comment)

sbc100 force-pushed the spec_syntax branch from 430df56 to 46ad492 Compare May 30, 2024 15:15

sbc100 requested a review from tlively May 30, 2024 15:16

sbc100 commented May 30, 2024

View reviewed changes

document/core/exec/instructions.rst Outdated Show resolved Hide resolved

sbc100 commented May 30, 2024

View reviewed changes

document/core/valid/instructions.rst Outdated Show resolved Hide resolved

sbc100 commented May 30, 2024

View reviewed changes

document/core/valid/instructions.rst Outdated Show resolved Hide resolved

rossberg reviewed May 30, 2024

View reviewed changes

rossberg reviewed Jun 12, 2024

View reviewed changes

[spec] Update syntax spec for memory64

f196f3a

I updated `instructions.rst` and make a start on `types.rst` but could use some help on how to parameterize `limits` on the index type.

sbc100 force-pushed the spec_syntax branch from 329a56c to f196f3a Compare June 18, 2024 20:51

sbc100 changed the base branch from main to wasm-3.0 June 18, 2024 20:52

rossberg reviewed Jun 20, 2024

View reviewed changes

sbc100 added 2 commits June 24, 2024 15:44

feedback

d5e1a95

validation rules

b925e4a

bvisness mentioned this pull request Jun 24, 2024

Rename Index Type to something else, perhaps Offset Type #67

Closed

rossberg reviewed Jun 25, 2024

View reviewed changes

sbc100 added 2 commits June 25, 2024 16:38

feedback

2472d29

exec spec

223b6c8

sbc100 added 2 commits June 28, 2024 10:08

feedback

f124d36

exec rules

4c4bf18

rossberg reviewed Jun 29, 2024

View reviewed changes

rossberg approved these changes Jun 29, 2024

View reviewed changes

feedback

e8045b6

sbc100 merged commit c7320ac into wasm-3.0 Jul 1, 2024

sbc100 deleted the spec_syntax branch July 1, 2024 21:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[spec] Update syntax spec for memory64 #50

[spec] Update syntax spec for memory64 #50

sbc100 commented Feb 21, 2024 •

edited

Loading

rossberg left a comment

sbc100 commented May 29, 2024

sbc100 commented May 30, 2024

rossberg left a comment •

edited

Loading

sbc100 commented May 30, 2024

rossberg commented May 31, 2024 •

edited

Loading

sbc100 commented Jun 3, 2024

rossberg commented Jun 3, 2024

sbc100 commented Jun 6, 2024

rossberg Jun 12, 2024 •

edited

Loading

sbc100 commented Jun 12, 2024

rossberg commented Jun 13, 2024

sbc100 commented Jun 18, 2024

rossberg Jun 20, 2024

sbc100 Jun 24, 2024

sbc100 commented Jun 24, 2024

rossberg left a comment

rossberg Jun 25, 2024

sbc100 commented Jun 26, 2024

rossberg commented Jun 27, 2024 •

edited

Loading

sbc100 commented Jun 27, 2024

rossberg commented Jun 27, 2024

sbc100 commented Jun 28, 2024

rossberg left a comment


		12. Assert: due to :ref:`validation <valid-memory.copy>`, a value of :ref:`value type <syntax-valtype>` \|I32\| is on the top of the stack.
		12. Let :math:`\X{it}_{min}` be ....?

	12. Let :math:`\X{it}_{min}` be ....?
	12. Let :math:`\X{it}_{\X{min}}` be ....?


		Abbreviations
		.............

[spec] Update syntax spec for memory64 #50

[spec] Update syntax spec for memory64 #50

Conversation

sbc100 commented Feb 21, 2024 • edited Loading

rossberg left a comment

Choose a reason for hiding this comment

sbc100 commented May 29, 2024

sbc100 commented May 30, 2024

rossberg left a comment • edited Loading

Choose a reason for hiding this comment

sbc100 commented May 30, 2024

rossberg commented May 31, 2024 • edited Loading

sbc100 commented Jun 3, 2024

rossberg commented Jun 3, 2024

sbc100 commented Jun 6, 2024

rossberg Jun 12, 2024 • edited Loading

Choose a reason for hiding this comment

sbc100 commented Jun 12, 2024

rossberg commented Jun 13, 2024

sbc100 commented Jun 18, 2024

rossberg Jun 20, 2024

Choose a reason for hiding this comment

sbc100 Jun 24, 2024

Choose a reason for hiding this comment

sbc100 commented Jun 24, 2024

rossberg left a comment

Choose a reason for hiding this comment

rossberg Jun 25, 2024

Choose a reason for hiding this comment

sbc100 commented Jun 26, 2024

rossberg commented Jun 27, 2024 • edited Loading

sbc100 commented Jun 27, 2024

rossberg commented Jun 27, 2024

sbc100 commented Jun 28, 2024

rossberg left a comment

Choose a reason for hiding this comment

sbc100 commented Feb 21, 2024 •

edited

Loading

rossberg left a comment •

edited

Loading

rossberg commented May 31, 2024 •

edited

Loading

rossberg Jun 12, 2024 •

edited

Loading

rossberg commented Jun 27, 2024 •

edited

Loading