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