Lemmas functions should become a specification construct + be removed from programs when completely statically verified

[jennalwise]

Consider making lemma functions a specific construct in the specification language.
They should not be executed at run time when completely statically verified. But, should be executed at run time when they need run-time checked. It is okay to allow ? to appear in lemma functions, but then they will need to appear at run-time like normal functions for run-time checking purposes.

We should make our lemma functions similar to those in VeriFast:

They are just like regular C functions, except that they may not perform field assignments or call regular functions, and they must always terminate

VeriFast also has other restrictions on lemma functions that we should consider.

Viper has pure functions and magic wand, so they do not need or have lemma functions; so, there is a question on whether or not we should go this route instead.