A formal proof of the Chip Model Channel Separation Property

Observations 1

Although the function chip is defined monadically, it is equivalent(*) to a simple list traversing function:

chip algs state [] = [] chip algs state (p:ps) = p':chip algs state' ps where (p',state') = runS (onePacket algs p) state

Under the assumption that onePacket has the right properties, we can prove Separation with induction over the input packet list, without reasoning about monadic code.

(*) This equivalence follows directly from the definitions.