Channel Separation Property
Property of interest: channel separation
( = no information leaks between channels)
┌─────────┐ ┌─────────┐
──┤ chip ├──►┤ pick ch ├──►
└─────────┘ └─────────┘
| =
| ┌─────────┐ ┌─────────┐
──┤ pick ch ├──►┤ chip ├──►
└─────────┘ └─────────┘
|
assert Separation =
∀ ch . {pick ch . chip} === {chip . pick ch}
pick :: Channel → [Packet] → [Packet]
pick ch = filter ((==ch).fst)