Support New Magic Wand Syntax

Created by bitbucket user nilsbecker_ on 2017-09-06 13:43

The following is a short summary of the main changes introduced by the new syntax:

The new syntax for packaging magic wands looks like: package A --* B { /* statements as ghost operations */}
lhs-expressions have been replaced by old[lhs]-expressions
magic wand variables have been removed
applying can be used analogously to unfolding to temporarily apply a wand without side-effects
the semantics of assert in magic wand prove scripts have been defined such that it transfers permissions into the wand's footprint if necessary

More details are available in my Bachelor's thesis report. Compare also silicon pull request #42.

viperproject / carbon