Module streams 

Stream equivalence over units proven apart: two circuits that take a stream of tokens through a valid-ready handshake and give a stream back, each at its own width and its own pace, decided equal token for token under an arrival pattern.

The environment (Environment) offers a token at the clocks it says, takes one at the clocks it says, and holds every other input as it says (a reset’s level, a value both sides share for the whole run). Under it each side’s handshakes are a schedule (schedule): the clocks it takes its input tokens at and gives its output tokens at, each proven the constant it is with the data free, so a side whose handshake depends on the data has no schedule and is refused by name. The sides are then unrolled (crate::units::Unrolled) with each side’s j-th input token read where that side takes it (Ports::token names the symbols a token’s bits are, so a side two words wide takes words 2j and 2j+1), and each side’s k-th output token claimed where that side gives it, its bits out<k>.<i>; decide decides the claims over the units as crate::units::decide_unrolled does. A token one side gives past what the other gives in the clocks unrolled is counted, not claimed.

Structs

Environment

The arrival pattern a side runs under, frames clocks: whether a token is offered at each clock, whether a given one is taken (or, for a side that never waits, watched for) at each clock, and what every other input is at each clock. Only the handshakes at those clocks are the side’s schedule, so the clocks before a reset settles are left out by offering and taking nothing there.

Ports

A side’s stream ports, by bit name: the input stream’s valid, ready and data, the output stream’s valid, ready (none for a side that never waits for it) and data; and what bit bit of the side’s j-th input token reads (token(j, bit), a symbol the other side’s token reads too).

Report

A decision of two streams: a verdict per claimed output bit (out<k>.<i>), each side’s schedule, the units’ rounds, and how many tokens each side gave in the clocks unrolled.

Schedule

A side’s schedule under its environment: the clocks it took its input tokens at and gave its output tokens at, and the derivation, from the side unrolled alone, that every handshake is the constant it was taken to be.

StreamSide

One side: its cut circuit, its units, its ports.

Enums

StreamError

Why two streams cannot be decided.

Functions

decide

Decide left against right, each under its environment, over their units, the functions of functions (each a left function, the right one proven equal to it) the only ones identified.

schedule

A side’s schedule under its environment, every handshake it rests on proven the constant it is.