Proof of the Channel Separation property
Proof is by induction over the input packet list
Proof is effectively by showing that one circuit simulates the other
Invariant: the states of the two circuits stay related
Relation: the register file for the observed channel is the same in both states:
property Invariant state1 state2 ch = {regfile state1 ch} === {regfile state2 ch} regifle :: ChipState -> Channel -> RegFile regfile state ch = lookup (snd state) ch