motoko-san: arguments and return values

[int-index]

Basic support for Int and Bool arguments and return values, incl. support for early return from a function.

The following example seems to work as expected:

example.mo

// @verify

actor Counter {
  var count = 0 : Int;

  public func increment() : async () {
    count += 1;
  };

  public func getZero() : async Int {
    if (true) {
      return 0;
    };
    return 1;
  };

  public func getMax(n : Int) : async Int {
    if (n > count) {
      return n;
    };
    return count;
  };

  public func getCount() : async Int {
    return count;
  };

  public func setCount(n : Int) : async () {
    count := n;
  };
};

It translates to the following Viper specification
example.vpr

define $Perm($Self) ((true && acc(($Self).count,write)))
define $Inv($Self) (true)
method __init__($Self: Ref)
    
    requires $Perm($Self)
    ensures $Perm($Self)
    ensures $Inv($Self)
    { 
      ($Self).count := 0 
    }
field count: Int
method increment($Self: Ref)
    
    requires $Perm($Self)
    requires $Inv($Self)
    ensures $Perm($Self)
    ensures $Inv($Self)
    { 
      ($Self).count := (($Self).count + 1)
      label $Ret 
    }
method getZero($Self: Ref)
     returns ($Res: Int)
    requires $Perm($Self)
    requires $Inv($Self)
    ensures $Perm($Self)
    ensures $Inv($Self)
    { 
      if (true)
         { 
           $Res := 0
           goto $Ret 
         }
      $Res := 1
      goto $Ret
      label $Ret 
    }
method getMax($Self: Ref, n: Int)
     returns ($Res: Int)
    requires $Perm($Self)
    requires $Inv($Self)
    ensures $Perm($Self)
    ensures $Inv($Self)
    { 
      if ((n > ($Self).count))
         { 
           $Res := n
           goto $Ret 
         }
      $Res := ($Self).count
      goto $Ret
      label $Ret 
    }
method getCount($Self: Ref)
     returns ($Res: Int)
    requires $Perm($Self)
    requires $Inv($Self)
    ensures $Perm($Self)
    ensures $Inv($Self)
    { 
      $Res := ($Self).count
      goto $Ret
      label $Ret 
    }
method setCount($Self: Ref, n: Int)
    
    requires $Perm($Self)
    requires $Inv($Self)
    ensures $Perm($Self)
    ensures $Inv($Self)
    { 
      ($Self).count := n
      label $Ret 
    }

[GoPavel]

LGTM except one thing: This changes is not supported several arguments
I would suggest to support it by:

and args p = match p.it with
  | M.TupP ps ->
    List.concat (List.map args ps)
  | M.ParP p -> args p