Simplification

No failing algorithms

• The proof instead makes use of the extra assumption that algorithms are "good"
• No runProtected
• The type of onePacket is thus slightly simpler:
  • Original
    • onePacket :: Algs->Packet->StateM ChipState (Maybe Packet)
  • My model
    • onePacket :: Algs->Packet->StateM ChipState Packet
• Motivation: ...