Incorporation of SpecTec into the phase advancement process

[conrad-watt]

If (or after?) we publish the 3.0 specification using SpecTec (#1844 (comment)), we should explicitly codify what expectations we have about completeness of SpecTec support for features in the phase advancement process. Intuitively, I think this means that our current phase 4 requirement - "the spec document has been fully updated in the forked repo" should be changed to explicitly call out that some version of SpecTec should fully support the new feature (since otherwise the spec document can't be generated in the first place). I'm assuming that, in the event that the 3.0 spec is based on SpecTec, we'll be keeping a stable version of SpecTec and associated .spectec files under https://github.com/WebAssembly/spec.

Some immediate questions:

• if an extended fork of SpecTec is necessary to support the feature, where should that fork live?
• alternatively, should we require that the main branch of SpecTec be updated with feature support by phase 4?
• do we want to include any requirements that the executable meta-interpreter or test generation from SpecTec function correctly, or will we still allow a separate interpreter and test suite to satisfy the process?

A possible set of new phase 4 and 5 requirements, in the hope of invoking Cunningham's Law:
Phase 4 entry:

• A complete set of .spectec files implementing the new feature should exist
• Some version of SpecTec (possibly a fork) should successfully consume the .spectec files to produce full prose and formal specifications for the whole language with this feature

Phase 4 during:

• The .spectec files (and any relevant fork of SpecTec) are prepared for merging with the main branch under the WebAssembly github organisation

Phase 5:

• The feature (including SpecTec extensions and .spectec files) is ready for merging

---

Practical point - threads is the feature that will stress this transition the most. We'll need to update SpecTec to...

• handle configurations with multiple threads
• handle reduction rules with relaxed memory effects
• handle the relaxed memory model

If this is just about prose and formal specification generation, I think this could be done fairly quickly. If we also require as part of the phase process that the meta-interpreter or test generator work, then there will be extra engineering needed - so it's worth hashing out these choices fairly soon.

cc @rossberg

[tlively]

The way I've been thinking about is that we would not make SpecTec a requirement in the official process docs to leave open the escape hatch of manually authoring the spec for features SpecTec might not be able to handle. Of course it would be better to update SpecTec as necessary if possible, and in that case I think it would make the most sense to get the SpecTec updates into the upstream version on the main branch as early as possible and then follow the existing process for merging main into proposal repos.

Similarly, I think we should not mention the meta-interpreter or test generator in the official requirements. Ideally it will be easier to update the test generator as necessary and use it to generate the officially required tests than to simply write the tests manually. If not, I wouldn't want to create more work for champions by requiring them to update the test generator.

[rossberg]

My take:

• if an extended fork of SpecTec is necessary to support the feature, where should that fork live?
• alternatively, should we require that the main branch of SpecTec be updated with feature support by phase 4?

Since SpecTec will live in the spec repo, and a new feature is already spec'ed in a fork of that repo, it only seems natural that necessary extensions to SpecTec are also first implemented in that fork.

• do we want to include any requirements that the executable meta-interpreter or test generation from SpecTec function correctly, or will we still allow a separate interpreter and test suite to satisfy the process?

In practice, we'll probably want the meta-interpreter to work before upstreaming a proposal. Beyond that, I think we'll need to get some practical experience before codifying process requirements on this particular point.

It's much too early to say anything about test generation.

Phase 4 entry:

• A complete set of .spectec files implementing the new feature should exist
• Some version of SpecTec (possibly a fork) should successfully consume the .spectec files to produce full prose and formal specifications for the whole language with this feature

Phase 4 during:

• The .spectec files (and any relevant fork of SpecTec) are prepared for merging with the main branch under the WebAssembly github organisation

Phase 5:

• The feature (including SpecTec extensions and .spectec files) is ready for merging

It makes sense to me that the spectec files must be completed before a proposal is thrown over the fence to the WG. I think that indeed means before entering phase 4. Everything else would practically shift all the burden from the champion to the editor, which doesn't seem feasible.

@tlively, if we need to exempt from these rules under circumstances, then that's fine. The CG or WG should be able to make that decision, and maybe the process doc can call that out. But notwithstanding the existence of escape hatches, the process should set the right expectations for "regular" proposal work moving forward.