zksecurity / noname

Noname: a programming language to write zkapps
https://zksecurity.github.io/noname/
193 stars 50 forks source link

Fix function instantiation #187

Closed katat closed 1 month ago

katat commented 1 month ago

This PR is for https://github.com/zksecurity/noname/issues/185

Changes

  1. Instantiate all functions, no matter whether it is generic function not. This is to resolve the case that @gio54321 pointed out below.
  2. Avoid unnecessary GenericSizedArray type
  3. Fix scope tracking for monomorphizing a function. It helps determine whether it is within a scope being monomorphized so as to decide whether to update the AST. This is not necessary if all functions are instantiated at the moment, but will be needed if decided to use a more efficient way to monomorphize the functions instead of all.

Another potential approach

To properly avoid instantiating all functions but only the ones containing generic vars or function calls, it would need an additional function AST walker to check if it is a function needed to be instantiated, or add a flag require_instantiation during the AST walk in TAST phase.

Then it can properly determine whether to instantiate a function, instead of simply relying on checking if it contains generic variables in the function signature.

gio54321 commented 1 month ago

This fix was quick! :smile: I don't think however that this approach solves the issue in the general case. Take for example this circuit, which adds an additional call to a generic function

fn zip(a1: [Field; LEN], a2: [Field; LEN]) -> [[Field; 2]; LEN] {
    let mut result = [[0; 2]; LEN];
    for index in 0..LEN {
        result[index] = [a1[index], a2[index]];
    }
    return result;
}

fn sum_arr(arr1: [Field; 3], arr2: [Field; 3]) -> [Field; 3] {
    let mut result = [0; 3];
    let pairs = zip(arr1, arr2);
    for idx in 0..3 {
        let item = pairs[idx];
        result[idx] = item[0] + item[1];
    }
    return result;
}

fn main(pub arr: [Field; 3]) -> [Field; 3] {
    let result = sum_arr(arr, arr);
    return result;
}

The function zip requires monomrphization and it is instantiated in sum_arr with LEN=3, but the body of sum_arr is not monomorphized. In my head, the need for monomorphization cannot be derived only from the signature but rather from the call graph, i.e., it is kind of a transitive property

A possible approach would be to always monomorphize the body of the functions recursively, and then put in scope the monomorphized symbol (I mean the zip#LEN=3 symbol) only if the function signature is generic.

katat commented 1 month ago

Cool, thanks for taking a look :)

A possible approach would be to always monomorphize the body of the functions recursively, and then put in scope the monomorphized symbol (I mean the zip#LEN=3 symbol) only if the function signature is generic.

I think it already works this way. Even though the body of sum_arr is not monomorphized, the function zip should be monomorphized. It should work recursively already. But maybe I miss something :o

The current rule for monomorphization is:

Then in synthesizer phase (circuit writer), the replaced FnCall node should look up the monomorphized function AST instead of the origin one.

katat commented 1 month ago

but yeah, your example doesn't compile. I am taking a look.

katat commented 1 month ago

Indeed, this is an issue as you described above. This is a great spot! @gio54321

We used to instantiate all the functions, including the non generic ones. But we tried to only instantiate the generic functions while keeping the non generic function as it is in order to minimize the affected scopes after monomorphization phase. That is why the use of fn_info.sig().require_monomorphization() to determine it needs to instantiate the function.

The problem this code doesn't work as I described above is because it only keeps walking into the generic functions when it handles FnCall node.

Therefore, I think updating the handling of FnCall to keep it walk through all the function calls besides the generic functions should fix the issue.