Module units 

Equivalence over units proven apart: two circuits built of units (adders, multipliers, any module already proven equal to its counterpart), each unit cut out of its circuit — its results free inputs, its operands outputs — and the two decided over the units as functions they know nothing of, a unit’s own proof standing for what it computes.

Each side is unrolled to its latency (Side): its own outputs (those not named under a unit’s instance) read at the last clock, each unit’s operands at every clock, each unit’s results a free input at every clock, named apart by side (left: and right:) so no two units are one unless proven so. An input with no name (an undefined bit) is a fresh one of its own side at every clock, and a latch with no name starts from a fresh value of its own. A unit applied at clock t has its results at clock t + latency: a pipelined unit’s proof says its outputs that many clocks late are the function of its operands.

A unit’s function is its name: a side’s units of one function compute one function, and a left function is the right one functions pairs it with (each pair a proof made apart), so the functions fall into classes, a side’s own names and the declared pairs joined.

The decision runs in rounds. Each builds one miter of both sides with every identification so far and simulates it; the applications of one class whose operands simulate alike are a group, on either side or both. Each application of a group is put to crate::fraig against the group’s first one it has not been refuted against: a pair whose operands it proves equal, bit for bit, is identified for the next round, the later application’s results made the earlier’s (functional consistency: one function of equal operands is equal), and a refuted one tries the group’s next. A round that identifies nothing more is the last, and decides the circuits’ own outputs. An output pair that differs over units the decision knows nothing of may still agree over the real ones, so it is Verdict::Unknown, never a difference.

Report::check builds every round’s miter again, replays its derivation from the miter’s formula, finds in it the operand equalities of every identification the next round makes, and in the last the outputs’ equalities; an application made one twice, or made one with itself through others, does not check.

Structs

Application

A unit of a side applied at a clock: the side (0 left, 1 right), the unit’s index, the clock of its operands.

Claim

An output bit a side claims at a clock, under the name its counterpart on the other side is claimed by.

Report

A decision over units: a verdict per output name, the rounds that made it, and the last round’s cost.

Round

A round: the identifications its derivation justifies (an application kept, and one whose results become the kept one’s), and the derivation, from the round’s miter, of their operands’ equalities — in the last round, of the outputs’ equalities.

Side

One side: its cut circuit, the clock its own outputs are read at, and its units.

Unit

A unit of a cut circuit: its instance name, the function it computes (its module), the clocks its results follow its operands by, and the names of its operand bits (outputs of the cut circuit) and result bits (inputs of it).

Unrolled

A side unrolled frames clocks: what each named input is at each clock (bind), the output bits it claims, and its units. An input with no name is a fresh one of the side’s own at every clock, whatever bind says.

Enums

Binding

What a side’s named input is at a clock: one input both sides share by its name, a constant the environment holds it at, or a fresh input of the side’s own.

Functions

decide

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

decide_unrolled

decide over sides unrolled as each says: the claims of one name, one on each side, are an output pair.