Finish `prepareSCMP`

• 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

Start at prepareSCMP and *SCION.Mem(), then trace DecodeFromBytes, SetSrcAddr, and GetAddr in the Go packet layer. Review how manually-created and decoded SCION values are specified, and confirm the ghost field, preconditions, postconditions, and simplified memory permissions are consistent when the specification is complete.