Representation of algorithms

My definition of Alg:

• type Alg = Nat -> RegFile -> StateM Memory RegFile
• The first argument is the packet size
• Required properties are stated extensionally