zksecurity / noname

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

when to fold a constant variable #188

Open katat opened 1 month ago

katat commented 1 month ago

Constant folding is needed to resolve the concrete sizes for the arrays. The MAST phase uses the propagated constants to resolved the generic parameters, such as

fn last(arr: [[Field; NN]; 3]) -> Field {
    let mut newarr = [0; NN * 3]; // <-- NN * 3 has to be folded with the resolved value of NN
    ...

Most of the time it is trivial to just fold the constant variables with the resolved values. But here is a case to take care with different rule:

fn accumulate_mut(const LEN: Field) -> Field {
    // shouldn't fold mutable variables as constants
    let mut zz = LEN; // assign a constant value
    for ii in 0..3 {
        // if zz is treated as a constant, mutable variable zz will be mistakenly folded as a constant.
        // for example, at the first iteration the zz + zz will replaced with LEN + LEN, 
        // where LEN can a concrete value such as 2.
        // then zz = 4 after 1st iteraction, and its AST will be changed to integer 4 from the expression zz + zz.
        zz = zz + zz; 
    }
    return zz;
}

Because the AST for zz = zz + zz is changed to zz = 4 after the constant folding, it won't represent the correct AST anymore. The value of zz should be changed after each iteration in the for loop. But after constant folding is done over it, the value of zz is always the same.

There is a PR to do a temporary fix by treat the mutable variable as non constant. But this is not ideal, because there can be cases like:

let mut len = 2;
len = len + 1;
accumulate_mut(len) 

So if len is treated as a non constant variable, the case above won't work also.

I think the root problem is due to the case of recursive mutation in a for loop. Therefore, one idea is to skip constant folding for mutable variable if it is within a for loop scope.

katat commented 1 month ago

This change in another PR should prevent the folding on zz + zz above, since the folding would only occur on the generic variables.

If it is not generic variable, the constant value still can be propagated even it is not folded at AST level.

So after that change, it seems this issue became non-issue.

Therefore, these two lines are not necessary anymore.