[DMS-55] Add Prim.Ret primitive that acts like var:return

[DK318]

Problem

Sometimes we want to reference a return variable in predicates. It's not possible because Prim.forall/Prim.exists accepts a lambda that shadows the outer var:return.

Example

func foo(): T {
  ...
  assert:system Prim.forall<T>(func tt = (tt == var:return));
  ...
};

var:return in the example refers to the result of the lambda inside Prim.forall but we want it to be referenced to the result of foo.

Solution

Introduce new primitive Prim.Ret with <T>() -> T type that is translated to $Res Viper variable.

Possible Problems

Since Prim.Ret is a regular Motoko's primitive then the user may do some inappropriate actions. For example:

let arr = Prim.Ret<[var Nat]>();
arr[0] := 42;

We don't restrict such actions. We suppose that Prim.Ret would be used only inside assertions. Using it in other places could lead to undefined behavior.

[GoPavel]

LGTM,
Could you also revert changes of #11?