[spec review] 3 - Validation

[flagxor]

Detail oriented review of draft text:
http://webassembly.github.io/spec/core/bikeshed/index.html#validation%E2%91%A1

Try to be ready to discuss issues by the next in person WG meeting.

[lukewagner]

I made a fairly-fine-grained pass through Section 3. Overall, this section feels like it's in pretty good shape.

• General:
  • It would be really nice to put some form of box or shaded rectangle around/behind the deduction rules and all other mathematical definitions. Otherwise, especially when combined with the awkward typesetting, they look out of place.
• § 3.1.1
  • "It is convenient to define"; could strengthen wording here; seems like more than a "convenience", but rather just a central definition used throughout the section.
  • Note on vectors: I'm not sure the Note helps more than it distracts, given that * is used to define mathematical lists throughout the entire spec.
  • "In addition to field access C.field the following notation is adopted": I'd expand C.field to ", written C.field,", otherwise sentence seems grammatically off.
  • Is the C,field A* notation ubiquitous or invented here? If the latter: I've actually squinted at this before; is there perhaps another notation that "looks" a little more like "prepend to this field"?
• § 3.2.2.1
  • "This restriction may be removed in future versions of WebAssembly.": Given the distance, "This" seems ambiguous; it'd be good to call out the return type.
• § 3.3.4.1
  • I'd expand "width" to "bit width" to match linked definition.
• § 3.3.5.9
  • I had a bit of confusion here because C.return is effectively a valtype??. Further confusing me was the fact that resulttype is a valtype?, not a valtype* which the note in this section assumes. Could we: (1) perhaps use a more explicit variant type for C.return to indicate "not in a function", (2) change resulttype to be a valtype* (or, if not, change the note to not use [])?
• § 3.3.7.2:
  • The formal rule for C⊢instr end const should I think be C⊢instr* end const
• § 3.4.8.5:
  • Seems like a good place for a note that the const restriction may be lifted in future versions.
• § 3.4.10:
  • In the prose description, I think externtype* and externtype'* are stale and should be changed to it* and et*.

[rossberg]

@lukewagner, thanks for the review, see #752 for changes.

• General:
  • It would be really nice to put some form of box or shaded rectangle around/behind the deduction rules and all other mathematical definitions. Otherwise, especially when combined with the awkward typesetting, they look out of place.

That's a good suggestion, but unfortunately I have a hard time figuring out how that could be done properly in either Sphinx or Bikeshed. I'll take another look, but can't promise anything.

• § 3.1.1
  • "It is convenient to define"; could strengthen wording here; seems like more than a "convenience", but rather just a central definition used throughout the section.

Reworded.

• Note on vectors: I'm not sure the Note helps more than it distracts, given that * is used to define mathematical lists throughout the entire spec.

Removed.

• "In addition to field access C.field the following notation is adopted": I'd expand C.field to ", written C.field,", otherwise sentence seems grammatically off.

Done.

• Is the C,field A* notation ubiquitous or invented here? If the latter: I've actually squinted at this before; is there perhaps another notation that "looks" a little more like "prepend to this field"?

Yeah, I'm not particularly happy with that. The "C,entry" notation for extending contexts is ubiquitous, though. But usually you don't define contexts as mere arrays, which is what makes it a bit weird here.

An alternative I have considered is having the above mean append to the end and then defining extra syntax for indexing the context, which would be reversed for labels. However, I suspect that would be even more confusing.

The only other option I can think of is writing it "entry,C" but that would really be unusual and probably confusing to many readers as well.

• § 3.2.2.1
  • "This restriction may be removed in future versions of WebAssembly.": Given the distance, "This" seems ambiguous; it'd be good to call out the return type.

Done.

• § 3.3.4.1
  • I'd expand "width" to "bit width" to match linked definition.

Done.

• § 3.3.5.9
  • I had a bit of confusion here because C.return is effectively a valtype??. Further confusing me was the fact that resulttype is a valtype?, not a valtype* which the note in this section assumes. Could we: (1) perhaps use a more explicit variant type for C.return to indicate "not in a function", (2) change resulttype to be a valtype* (or, if not, change the note to not use [])?

I have changed C.return to be resulttype | NORETURN for now. However, that is a bit irregular in that empty equates "not usable" everywhere else, plus it breaks the convention that empty components can be left out, which now needs special-casing.

I didn't understand the second part of your comment. [] is the correct spelling of the empty resulttype, what was implying valtype* in the wording? In any case, that part of the note is obsolete with the other change, so I just removed it.

• § 3.3.7.2:
  • The formal rule for C⊢instr end const should I think be C⊢instr* end const

Fixed.

• § 3.4.8.5:
  • Seems like a good place for a note that the const restriction may be lifted in future versions.

Added here and likewise for imports.

• § 3.4.10:
  • In the prose description, I think externtype* and externtype'* are stale and should be changed to it* and et*.

Cleaned up naming of these and others, plus a few other tweaks.

[lukewagner]

An alternative I have considered is having the above mean append to the end and then defining extra syntax for indexing the context, which would be reversed for labels. However, I suspect that would be even more confusing.

Yeah, I also thought about suggesting this. Given how pretty much everything else works in a stacky manner by appending, it seems like all you need to make this look nice is find a stylized bracket that means "index from the end" and use that. That actually seems more natural all around.

I have changed C.return to be resulttype | NORETURN for now. However, that is a bit irregular in that empty equates "not usable" everywhere else, plus it breaks the convention that empty components can be left out, which now needs special-casing.

Thinking about this a bit more: is NORETURN even necessary? IIUC, it's only set for initializer expressions and those have a separate validation predicate that rules out return anyway. Moreover, if we interpret return as "jump to the outermost label of this frame", then it seems like initializer expressions could one day allow return so the the "non-returning expression" category may not even be fundamentally necessary.

[lukewagner]

Additionally:

• § 3.3.7.2:
  • It's not immediately obvious that init exprs additionally require get_global to refer to an import; you have to connect the dots with how the validation context C' is constructed in module validation. It'd be nice to add a note.
  • If we do decide to drop the immutability requirement, and since all imports are immutable globals and thus it's not an observable change, it might also be good to eagerly drop the const requirement in v.1?

[rossberg]

An alternative I have considered is having the above mean append to the end and then defining extra syntax for indexing the context, which would be reversed for labels. However, I suspect that would be even more confusing.

Yeah, I also thought about suggesting this.

To avoid introducing one-off notation, I tried the other suggestion and reversed the context extension notation to entry,C with some respective note. On second look it doesn't seem too bad, and there aren't many occurrences of it anyway.

While applying the change I noticed another problem with NORETURN breaking conventions for empty context fields. Due to that and because it generally seems like a bad fit, I backed out of that earlier change. Instead I added more explicit notes and tried to tweak wording and notation to make it as clear as possible. I think it is okay now, given that it only occurs in a single place, but PTAL.

Thinking about this a bit more: is NORETURN even necessary? IIUC, it's only set for initializer expressions and those have a separate validation predicate that rules out return anyway. Moreover, if we interpret return as "jump to the outermost label of this frame", then it seems like initializer expressions could one day allow return so the the "non-returning expression" category may not even be fundamentally necessary.

The latter is pretty much what I had initially -- until @conradwatt discovered during his mechanisation effort that it breaks Preservation. :( The reason is rather technical: roughly, the rules have no way of detecting what "outermost" is, because there is no syntactic marker, and it all has to be compositional to work properly. All well-typed instruction sequences can form larger ones, so it would effectively allow typing any return to a random inner scope.

Hail to mechanisation, because this was a somewhat subtle issue.

A separate predicate also wouldn't play well with a preservation proof, for related reasons. The only clean solution is to track any such constraint as contextual information.

§ 3.3.7.2:

• It's not immediately obvious that init exprs additionally require get_global to refer to an import; you have to connect the dots with how the validation context C' is constructed in module validation. It'd be nice to add a note.

Good idea, done.

• If we do decide to drop the immutability requirement, and since all imports are immutable globals and thus it's not an observable change, it might also be good to eagerly drop the const requirement in v.1?

Done. And because it would be weird otherwise I also changed the term from "constant expression" to "static expression".

[rossberg]

• If we do decide to drop the immutability requirement, and since all imports are immutable globals and thus it's not an observable change, it might also be good to eagerly drop the const requirement in v.1?

Done. And because it would be weird otherwise I also changed the term from "constant expression" to "static expression".

@titzer's latest comment raises a valid objection. Hence I reverted this last bit -- it needs more discussion than is appropriate for a mere editorial change.

[binji]

It sounds like all issues have been addressed here. The one exception is the discussion about lifting the constraint that globals be immutable in a constant expression. Since we haven't discussed this since then, I assume we're OK lifting this restriction later (if at all). Closing.