add behavior to contact of peek
change rep of MaxValue (improves verification rate)
formatting
simplify assigns clause (achieve full verification)