Isolate function application arguments

[keyboardDrummer]

Putting this PR on hold since it breaks the rule that

var x := <expr>
var y := F(x);
...

Should behave the same as:

var y := F(<expr>)
...

Because there can be facts proven in <expr> that are exposed in the first case but not in the other.

Changes

• Isolate proofs inside expressions from the surrounding proofs
• Expression proofs still affect the proof of the ensures clause of the surrounding function, unless inside a let binding.

How has this been tested?

• Added CLI test ast/expressions/statementExpressionScope.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Closing this since I currently have no intention of adding this behavior