Sat Dec 7 13:10:00 EST 2019


The obvious path is to take some state machine from the Ethernet MAC.

EDIT: I'm still missing an element.  Can the model-wrapping be _only_
phantom types?

EDIT: The frontend transforms the data ready + bit pair into a word
stream that can go into a fifo.  How to type those?  Doesn't make a
whole lot of sense putting it that way.  The core issue here is that
one type of event stream is transformed into another, and this is done
multiple times until anything like a "packet" emerges.

But still, it does make sense to somehow type the I/O.  This
composition is actual, so it makes sense to reflect it in the types.


rmii -> word -> packet

EDIT: I'm on the wrong track.  Just start implementing, then once the
composition is there, start typing it.

A glimpse: type it without mentioning state.  It is understood that
things are stateful at a local level.