stdlib: comparator & bigint

[katat]

new stdlib

comparator bd2e612

• less_than
• less_than_eq
• greater_than
• greater_than_eq

bigint 1e586e9

• add_limbs
• mult_limbs
• less_than
• is_equal
• modulo
• sub
• sub_mod
• mult_mod

data type bd2e612

• uint8

Issues to resolve

1. • Method bug. Will need to investigate to understand what are the causes.
2. • Unused cell vars introduced from hint builtins. Currently disabled the check 59f98d1
3. • Builtin functions doesn't propagate constants. Currently hardcode the values in certain places. This would be resolved by upcoming hint feature.
4. • The new symbolic value definitions introduced by the builtin hints are really redundant bf9efb0. This is due to the order of constant and cell var in the binary operations. I think we need to refactor the symbolic value enum.
5. • Lack of branching support. Due to this, it has to hardcode the array boundary in some cases.
6. • Not allow silent return. This leads to unnecessary assignment in some cases.
7. • IFE branch only allow variable. Maybe we should allow literal also.

Adjustments

• Allow generic function calls within forloop 4dce945. This is the exact changes from the PR allow generic calls within forloop #189
• Allow subtract binary operation in symbolic size 75dcbe3
• Added a bunch of builtin hints bf9efb0.

[katat]

the asm diffs originated from the fact that the builtin version stored constant as cell vars.

[katat]

One idea inspired from this experiment about hint function is how we can deal with the unconstrained / unsafe expressions to:

• maximize its related safety
• be educational on what are non-deterministic calculations

Example of using builtin function as hint function

// native version of `bits::to_bits`
fn to_bits(const LEN: Field, value: Field) -> [Bool; LEN] {
    let mut bits = [false; LEN];
    let mut lc1 = 0;
    let mut e2 = 1;

    let one = 1;
    let zero = 0;

    for index in 0..LEN {
        // code for `bits::nth_bit`: https://github.com/zksecurity/noname/blob/564ae004cf4c580efb0f473c69a198b88127baed/src/stdlib/bits.rs#L37-L81
        bits[index] = bits::nth_bit(value, index);

        let bit_num = if bits[index] {one} else {zero};
        assert_eq(bit_num * (bit_num - 1), 0);

        lc1 = lc1 + if bits[index] {e2} else {zero};
        e2 = e2 + e2;
    }
    assert_eq(lc1, value);
    return bits;
}

Attribute unsafe

bits::nth_bit(value, index); is a non-deterministic function, which just does a non-deterministic calculation without constraining anything.

To make the code explicit about where the non-deterministic expressions are, we can require an attribute called unsafe, such as:

bits[index] = unsafe bits::nth_bit(value, index);

We may also require the unsafe attribute to the builtin function signature, eg:

unsafe nth_bit(val: Field, const nth: Field) -> Bool

While the unsafe attribute is for the users to acknowledge that they are responsible for having additional constraints, it can also help type check if an expression can be added as constraints.

The type check workflow would be:

1. tag unsafe attribute to flag the expression bits::nth_bit(value, index) as non-deterministic
2. a unsafe metadata can be added to the var of the bits
3. when CS trying to constrain the non-deterministic var, it will raise an error if the var is not marked unsafe via the attribute unsafe.

In comparison to how circom handles hint calculations, this approach makes it explicit whether an expression is non-deterministic at the first place.

Potential design for native hint function

The unsafe attribute idea would also work for upcoming native hint function.

For constructing the hint calculations for a hint function, we may just handle it in a separate synthesizer workflow that doesn't add any constraints but only build up a set of symbolic values. Each of them can be mapped to a cell var in a backend.