Add support for functions

[tohrnii]

It may be desirable to have support for simple functions. This could be beneficial for two reasons:

1. Provides a good way to encapsulate some commonly repeated logic.
2. Provides a good way to support external routines.

A good example for this could be MDS matrix multiplication for Rescue Prime constraints. This function needs to be called twice, and in the context of the prover, we could use a much more efficient routine to perform the multiplication (because we know we are in the base field).

To make this feature as simple as possible, we could impose the following limitations:

• Functions are always pure - i.e., there are no side effects.
• Function parameters can be only variables (scalars, vectors, matrixes) - i.e., passing columns to functions is not allowed.

A function declaration could look as follows:

fn apply_mds(state: vector[12]) -> vector[12]:
  // function body goes here

This function takes a vector of 12 elements as a parameter, and returns a vector of 12 elements. To invoke this function, we could do something like this:

trace_columns:
  main: [state[12]]

let x = apply_mds(state)

To support external subroutines, we could use something similar to Rust's attributes. For example:

#[prover("mds.rs")]
fn apply_mds(state: vector[12]) -> vector[12]:
  // function body goes here

The above would mean that when compiling the constraints in the context of the prover, instead of using the body of the function, an apply_mds function from the mds.rs file should be used. The signature of that function would have to be:

fn apply_mds(state: [Felt; 12]) -> [Felt; 12];

However, when the constraints are compiled in the context of the verifier, the body of the function would be used as is.

Originally posted by @bobbinth in 0xPolygonMiden/miden-vm#254 (comment)

[bobbinth]

I wonder if we actually need to specify vector etc. for parameters and output values. For example:

fn apply_mds(state: vector[12]) -> vector[12]

Could be expressed just as easily as:

fn apply_mds(state: [12]) -> [12]

If we do this, we could describe data types as follows:

fn foo(bar: scalar) -> [12]  # bar is a single element
fn foo(bar: [12]) -> [12]    # bar is a vector of 12 elements
fn foo(bar: [4, 3]) -> [12]  # bar is a matrix with 4 columns and 3 rows
fn foo(bar: [[3]]) -> [12]   # bar is a table with 3 columns

The only thing that looks a bit odd here is scalar - but otherwise it is pretty consistent with how we describe types in other places.

[tohrnii]

I was also wondering the same but @grjte had a preference for explicit vector and matrix probably because scalar looks odd otherwise.

[tohrnii]

One other difference from the proposed syntax is that return statements would require the use of "return" keyword in the current implementation because it's hard to write unambiguous grammar without this with our current structure.

[bobbinth]

One other difference from the proposed syntax is that return statements would require the use of "return" keyword in the current implementation because it's hard to write unambiguous grammar without this with our current structure.

Could you elaborate a bit more on this? I'd like to avoid using a return keyword if possible - but maybe there are other ways to reduce ambiguity?

[tohrnii]

I think the problem is that we currently ignore whitespaces and newlines. So imagine a function like:

fn func(a: vector[6]) -> vector[1]:
    let x = a
    [1]

Now this could mean we are returning a vector [1] or if it's part of the previous intermediate variable declaration statement, ie, let x = a[1].

Or something like:

fn func(a: vector[6]) -> (m: scalar, n: scalar):
    let x = a
    (1, 0)

This could mean we are returning a tuple (1, 0) or it could be a part of function call a(1, 0) at the parser level.

For all other statements we have terminals like "let" and "enf" that help remove this ambiguity.

One possible solution is to not ignore whitespaces and then explicitly define where whitespaces are required in the grammar rules but that will complicate things quite a bit and will most likely be an unclean solution. Another alternative is to not ignore newlines and add a terminal for a newline and define all rules that way but even that seems like it would complicate things quite a bit.

It's possible there is some other simpler way to fix this which I'm missing though so I'll look into it more.

[bobbinth]

@tohrnii - makes sense! Though I do wonder if we should handle whitespaces a bit more strictly. For example, if I understood correctly, the following statements are equivalent:

let x = a[0]

and

let x = a   [0]

and

let x = a
[0]

Ideally, we should make it so that only the first one is valid and the other ones result in an error.

[grjte]

I was also wondering the same but @grjte had a preference for explicit vector and matrix probably because scalar looks odd otherwise.

Yes, this was my reasoning. It's not a very strong preference, but I do think scalar looks odd when it's the only one.

fn foo(bar: scalar) -> [12]  # bar is a single element
fn foo(bar: [12]) -> [12]    # bar is a vector of 12 elements
fn foo(bar: [4, 3]) -> [12]  # bar is a matrix with 4 columns and 3 rows
fn foo(bar: [[3]]) -> [12]   # bar is a table with 3 columns

Regarding the table option, I have a preference for [][] rather than nesting brackets, as mentioned here:

#143 (comment)

[grjte]

@tohrnii - makes sense! Though I do wonder if we should handle whitespaces a bit more strictly.

I agree. It would be good to add an issue for this.

[tohrnii]

Though I do wonder if we should handle whitespaces a bit more strictly.

I agree with you that would be ideal. However, my understanding is that it would complicate things. For example, what to do when it's a multi line statement, or if it's a multiline matrix declaration or for any compound expression, users might have different preferences for whitespaces (For example whitespace around arithmetic operation symbols, or whitespace around parentheses, etc). I don't think even throwing an error on 2 or more consecutive whitespaces works because of indentation (which could be spaces instead of tabs). Maybe there's a way to do this I'm missing?

[tohrnii]

I can open an issue to explore this more in the future though.

[bobbinth]

Some more thoughts on syntax. I think we should introduce the felt keyword here to define the type of parameters/return values. In the future, we can extend this to binary/integer types as well (see #334). So, function signatures would look like this:

fn foo(bar: felt) -> felt[12]        # bar is a single element; returns a vector of 12 elements
fn foo(bar: felt[12]) -> felt[4, 3]  # bar is a vector of 12 elements; returns a matrix (4 cols/3 rows)
fn foo(bar: felt[4, 3]) -> felt      # bar is a matrix (4 cols/3 rows); returns a single element

[bobbinth]

Closed by #351.