zksecurity / noname

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

Support default array declaration #120

Closed katat closed 2 days ago

katat commented 1 month ago

This PR is to support const generic for default array declaration.

02bad12b62b0b325394f1877b812efca58ae0868 is the test cases to showcase this new feature.

Still figuring out how to compute the value behind a constant var that is out of context in a function: https://github.com/zksecurity/noname/blob/48ec1061b6a927c72e329d97342100a3050c5d75/src/circuit_writer/writer.rs#L668-L674

katat commented 1 month ago

After supporting the const generic variable to declare a default array, we need a way for the ArrayAccess to induce the value behind size variable to do sanity checks.

Take the following code for example, we need to know the sizes of the houses array and the rooms array in order to check if the array access is within their bounds:

const houses_num = 5;
const rooms_num = 3;
const room_size = 20;

struct Room {
    size: Field,
}

struct House {
    rooms: [Room; rooms_num],
}

fn build_house(const num: Field) -> [House; num] {
    let houses = [
        House {
            rooms: [Room {size: room_size}; rooms_num]
        }; 
        num
    ];
    return houses;
}

fn main(pub resize_to: Field, total_size: Field) {
    let mut sum_size = 0;
    let mut houses = build_house(houses_num);

    for ii in 0..houses_num {
        for jj in 0..rooms_num {
            houses[ii].rooms[jj].size = resize_to;
            sum_size = sum_size + houses[ii].rooms[jj].size;
        }
    }

    assert_eq(sum_size, total_size);
}

In the circuit generation process of circuit writer, these array sizes can be induced after the array declaration expressions are computed. Because these declaration expression node ids are unique, we could save the computed size value with the expression node id as the key in a map for later references.

For example, the following is the array declaration expression node for the field rooms:

[Room {size: room_size}; rooms_num]

Now the problem is how can we trace the variables' expression nodes, such as houses[ii].rooms[jj], to their declaration expression nodes above ^. So we can look up the rooms array size by node id via the map stored earlier.

As we can compute the type for an expression node, I am wondering if it is currently possible (without major refactoring) to attach the declaration node when storing a computed type.

katat commented 1 month ago

I went with the ComputedExpr approach as described in the rfc draft 69033d3

katat commented 2 days ago

implemented by another approach: https://github.com/zksecurity/noname/pull/147