Procedures to return values

[jjcnn]

Procedures are currently not allowed to return values.

I don't know how much of an issue this is, but some users may well find it useful to be able to pass a value back to the caller once a procedure finishes.

[vaivaswatha]

I was having a look at one of @AmritKumar ' s contracts today and it looks like this can be a useful thing.

Checking permissions (is sender owner, does sender have permission to do this operation) etc involve common code, which ultimately return a bool (can do or cannot do operation), and their source values are from fields. So we would want procedures which look at certain fields, compute something on it, and return a value.

[jjcnn]

If it's non-map fields, then it is just as simple to read the fields and compute the bool using a library function.

The issue is if the field is a map. Then using library functions becomes expensive.

[vaivaswatha]

Map fields are involved in this particular example, yes.

[vaivaswatha]

Here's an example check:

is_mem1 = exists m1[_sender];
is_mem2 = exists m2[_sender];
is_mem3 = exists m3[_sender];
or_res = orb_3 is_mem1 is_mem2 is_mem3;
match or_res with

This sequence appears in many transitions, and should be replaceable with

is_eligible = do_checks(_sender);

[jjcnn]

In the example contracts where this pattern occurs one of the conditional branches does nothing. Therefore, one could use a do_checks procedure which throws an exception in the empty branch:

procedure do_checks(...)
  is_mem <- exists m1[_sender];
  is_mem <- exists m2[_sender];
  is_mem <- exists m3[_sender];
  or_res = ...;
  match or_res with
    | True => (* Everything works - do nothing *)
    | False => throw ChecksFailed
  end
end

If the checks fail, then execution stops when the exception is thrown, and the result of the transition is that no state is changed. If the check succeeds, then the calling transition continues as if everything is fine, which it is.

[jjcnn]

Assigning @jubnzv to this.

Suggested breakdown of the issue:

1. Introduce a return type to type component in Syntax.ml. The return type should be optional (because transitions don't return values, and procedures are allowed to not return values), and the typechecker should ensure that the return type is None for everything that is currently in Scilla.
2. Add syntax for return values and types for procedures. I'm thinking something like this would do:

procedure MyProc (x : ...) : type Uint128 end
  <procedure body>
  x = Uint128 42;
end => x

But this is a suggestion off the top of my head, so do put some thought into whether there might be a better option.

At this stage we also need to introduce a typecheck of procedure invocations that don't expect a return value:

  MyProc (my_x); (* Typecheck should either fail or issue a warning, because MyProc returns a value *)

3. Add syntax and typechecking for invoking procedures with return values:

  res = MyProc (my_x);

[jjcnn]

iterate needs to be considered as well, because iterate MyProc some_list could work either as a map (creating a list of return values from MyProc), or could just throw the returned values away.

For now I suggest we add a typecheck in step 1 that disallows iteration of procedures that have a return value. We can then enable it for procedures with return values later on, once we decide how it should behave.

[jjcnn]

procedure MyProc (x : ...) : type ... end
  <procedure body>
  x = Uint128 42;
end => x

This way of returning a value isn't great, because of this situation:

  match some_condition with
  | True =>
    e = { _eventname : "..." ; ... };
    event e;
    (* Return 42 *)
  | False =>
    e = { _eventname : "..." ; ... };
    event e;
    (* Return 0 *)
  end

We'll need some sort of return instruction, but since return isn't currently a keyword we'll need to do something clever in order to make this change backward compatible. Still, we'll figure something out - I just can't think of a way to do it right now.

Maybe we need a special variable _return or _result, so that the above code can be writte as

  match some_condition with
  | True =>
    e = { _eventname : "..." ; ... };
    event e;
    _result = Uint128 42;
  | False =>
    e = { _eventname : "..." ; ... };
    event e;
    _result = Uint128 0;
  end

?

[jubnzv]

@jjcnn I checked the dump of all deployed contracts by 2022-07 and there are no uses of the return keyword. So, we could safely use it.

I agree, that the return keyword looks better than the procedure ... end => x syntax. It looks very familiar for developers working with languages like Solidity. And I think the ... => x syntax may create some ambiguities with shadowing when creating local variables with the same name, and it may be a bit more complicated to implement the type checking for it.