investigate representing #[channel] in AsyncAPI format

Currently the #[channel] annotation used for declaring WebSocket endpoints simply places a "x-dropshot-websocket" extension in the generated OpenAPI spec endpoint.
We might consider instead representing these in AsyncAPI schema, an OpenAPI-derived format for describing APIs using protocols unsupported by OpenAPI, including WebSockets.

This would enable us to add support for defining message formats in the macro, and generating a tagged-enum wrapper with progenitor, for example.
Our current use cases for websocket channels in our APIs are for shunting packets of existing binary protocols -- serial console and websocket -- to a web client.
As a result, it's unclear if it's worth taking on all this message complexity of explicitly defining higher-level contents of "messages" for what we're shipping in the near-term, but it would be nicer for the purpose of continuing to support existing web service community standards such that tooling for other languages can generate clients for our APIs.

(relatedly: do we want a general process for graduating any one-off extensions we develop into appropriate community standards where/when they exist?)

Start by tracing the #[channel] annotation and the generated OpenAPI endpoint extension. Read the referenced AsyncAPI message-object specification and consider how progenitor would consume a generated tagged-enum wrapper. Done would require a clearly scoped decision or implementation plan for representing WebSocket channels and message formats; the issue names no files or tests.