Assumed properties of algorithms

• The result of a good algorithm depends only on the packet it processes and the register file for the relevent channel:
  property GoodAlg alg =
  ∀ ws regf mem1 mem2
  {fst (doPacket alg ws regf mem1)}
  ===
  {fst (doPacket alg ws regf mem2)}
• We are running the state monad starting in two unrelated memories, and observing the result (the returned packet and modified register file)
  • doPacket :: Alg -> Data -> RegFile -> StateM Memory (Data,RegFile)