Finish prepareSCMP

[jcp19]

• introduce ghost field in *SCION for when some package is manually created vs when it is obtained from decoding from bytes
  • verify fns that come from the go packet layer interfaces for both cases,
    • DecodeFromBytes should set the manuallyBuilt flag to false and should have a postcondition expressing that.
  • identify functions which are called only for one value of 'manuallyCreated' and add it as precondition/simplify the specs of these functions (e.g., SetSrcAddr, GetAddr)
  • Add public getter for this field to use in spec
• simplify *SCION.Mem() by removing duplicated expressions with lets
• remove the instance of HeaderMem from Mem(), fold it when needed and remove fractional permissions from the body, pass fractional permission to HeaderMem instead
  • this will allow us to write acc(s) instead of explicit access to all fields

[jcp19]

We would benefit from having support for multiple contracts per function; this would allow us to verify the body of prepareSCMP in a maintainable way