A formal proof of the Chip Model Channel Separation Property

The Chip

chip :: [Packet] → [Packet] type Packet = (Channel,Data) type Channel = Int type Data = [Word]

      ┌──────┐
ps ───┤ chip ├──►  ps'
      └──────┘

One chip processes packets on a number of independent channels
Behavior:
1. input a packet
2. do some processing (encryption/decryption),
3. output a modified packet
Packet processing is stateful: the output for a packet can depend on all previous input on the same channel.