3.1. What we will prove, and how🔗

The claim has a standard shape, called a stuttering refinement. Think of the specification's execution as a film of the architectural state, one frame per instruction. The pipeline produces its own film, one frame per clock cycle — a longer film, because some cycles are spent filling the line or waiting, with nothing visible happening to the architectural state. The theorem says: if you delete the duplicate frames from the pipeline's film, you get exactly the specification's film. Same states, same messages to the neighbours, same halts. The pipeline is allowed to take its time; it is not allowed to invent, lose, or reorder anything observable.

One structural decision makes the proof honest and small at the same time. Our pipeline model's execute stage is the step function — the previous chapter's semantics, called as a subroutine on the architectural state. This is not circular; it is the same factoring the hardware itself uses. M0 decided each element has one shared execution unit, and whether that unit's adder adds correctly is a separate, later proof at the gate level. What the pipeline adds to the world is control: registers that hold in-flight instructions, the shift-forward each cycle, and the squash on redirect. Those are what this chapter's theorem is about, because those are what overlap puts at risk.

3.2. The pipeline state🔗

Three stages: fetch (F), decode (D), and issue/execute (I). The model keeps the committed architectural state, plus what each stage holds — for D and I, an instruction tagged with the address it came from; for F, just the address to fetch next. An empty slot is a bubble.

3.3. One clock cycle🔗

Each cycle, the pipeline does one of the following. If the issue slot holds an instruction, it executes it — by calling step — and then either shifts the line forward (normal case), squashes the younger stages (a redirect: the executed instruction changed the program counter, so everything fetched behind it is wrong), holds everything in place (the instruction is waiting on a mailbox), or stops for good (HALT). If the issue slot is a bubble, the cycle just moves the line forward: whatever is in decode advances to issue, and fetch refills decode.

Notice the execute case consults ps.arch directly: by the time an instruction sits in the issue slot, the invariant below guarantees the architectural program counter points at it, so step fetches and executes exactly the in-flight instruction.

3.4. The pipeline's promise🔗

An assembly line is only correct if what is on the line corresponds to what should be built next. We state that as an invariant — four facts the pipeline maintains between every pair of cycles:

3.5. Seeing through the pipeline🔗

To compare the two films frame by frame we need to say which architectural state a pipeline state depicts. The registers are simply the committed ones; the program counter is the address of the oldest instruction still in flight (or, if the line is empty, the next fetch address). This is the "delete the duplicate frames" lens:

3.6. The theorem🔗

Every pipeline cycle is one of two things, seen through the lens: a stutter (the depicted state does not change, and nothing is said to the neighbours) or a perfect step (the depicted state changes exactly as step dictates, with exactly the same mailbox traffic). And a pipeline halt happens only when the specification halts. The invariant survives either way.