Support for Ghost Fields

[ArquintL]

This PR depends on PRs #747 & #755 and should, thus, be reviewed and merged only after merging the mentioned PRs.

This PR adds ghost fields, i.e., allows the use of ghost in front of field declarations. Note that struct embeddings can (so far) not be ghost. While ghost fields work mostly analogously to actual, non-ghost, fields, there are a few restrictions / differences to point out:

• A struct with ghost fields cannot implement an interface, however, a pointer to such a struct can (see ghost-field-interface-simple01.gobra and ghost-field-interface-fail01.gobra)
• Actual equality (==) on structs considers only actual fields, i.e., structs are equal modulo ghost fields. To include ghost fields in the comparison, ghost equality (===) can be used instead (see ghost-field-comparison-simple01.gobra)
• As a consequence, a Go map with a struct with ghost fields as a key type becomes challenging as two ghost-unequal key values can be actual-equal and, thus, map to the same entry at runtime. Although our encoding could be extended, we currently disallow such map types (see ghost-field-map-fail01.gobra)

[jcp19]

I will soon test this out in SCION to make sure that this works with the SCION idioms. I will report the results here.

[jcp19]

I just adapted the SCION code to be accepted by this new PR (https://github.com/viperproject/VerifiedSCION/pull/337). As such, I do NOT have any objections against merging this 🚀. Note that this comment is not a review, I did not look at the code.