Support private functions and old expressions in Motoko-to-Viper translation

[aterga]

This PR adds support for translating private Motoko functions into Viper. The translation is mostly analogous to that for public async functions. However, a private function does not have to be called from a state that satisfies the canister invariant (i.e., it may be called even in intermediate states), and a private function does not have to preserve the canister invariant (i.e., it may result in an intermediate state).

Additionally, we add old expressions to enable useful specs in private actor functions, e.g.:

private func reward() : () {
  count += 1;
  assert:return count == old count + 1;
};

[crusso]

(I'm off tomorrow, @ggreif can you take a look if on duty?)

[github-actions]

Comparing from aa17d7e to c0fd8bb:
The produced WebAssembly code seems to be completely unchanged.

[ggreif]

LGTM! A few nits noted. Also test/viper/ok/private.silicon.ok is an empty file, make -C test/viper accept should get rid of it.

Maybe also update the src/viper/README.md regarding the new features?

[ggreif]

As you see I am not a fan of redundant parentheses :->
feel free to ignore those nits.

[ggreif]

Feel free to set the automerge-squash label