Skip to content

Latest commit

 

History

History
336 lines (276 loc) · 7.63 KB

NOTES.md

File metadata and controls

336 lines (276 loc) · 7.63 KB
Raw

Types

bool: [0, 1].

  • 0: False
  • 1: True

booly: [0, q]

  • 0: False
  • 1-q: True

range(a, b): [a, b]

u8, byte: range(0, 0xff)

u16: range(0, 0xffff)

Rules

BOOLY(e: expr) -> booly

  • if e(x) == 0 then False else True

IF (b: booly) THEN e: expr

  • if b(x) is truthy then BOOLY(e(x)) is false

e * p

IF (e: bool) THEN e1: expr ELSE e2: expr

  • if e(x) is true then e1(x) == 0, else e2(x) == 0

e * e1 (1 - e) * e2

e1: booly AND e2:booly -> booly

e1 * e2

e1: bool AND e2:bool -> bool

e1 * e2

e1: bool OR e2:bool -> bool

e1 + e2 - e1 * e2 [alt] 1 - ((1 - e1) * (1 - e2)) = 1 - (1 - e2 - e1 + e1 * e2) = e1 + e2 - e1 * e2 # DeMorgan

e1: expr == q: const -> bool

(1 - (e1 - q) * w) % (e1 - q) * (1 - (e1 - q) * w) $ w := inv(e1 - q) if (e1 - q) != 0 $ w := 0 if (e1 - q) == 0

not(e: expr in S) -> booly for S = {s1, s2, ..., sn}

(e - s1) * (e - s2) * ... * (e - sn)

CONSTRAIN(not(e: booly))

  • e(x) == false

e == 0

Polynomail constraint analysis

DSL design notes

This is a list of features that the DSL should optimize for

  • Constraint definition and witness assignment should be done together
  • Should not expose rotations, only variables (advices, constants?) and expressions.
  • Should add gadget selectors implicitly
  • Should allow modeling state machines gadgets
  • Should make it easy to add negative tests
  • A constraint checker should report the line and trace (in case of nested gadgets) of a failing constraint along with the values used in that constraint
  • Advice and Expressions can be typed, and a checker will verify that the types are correct.

This is a list of nice to have features

  • Witness assignment should be done automatically when possible

Open questions:

  • How is composition modeled?
  • How are dynamic lookups modeled? What about composition via dynamic lookups?
  • How does it work with the challenge API?

Embeddable scripting languages for Rust

Gadgets

Aux

let from_bytes_le = |bytes| bytes.zip(0..bytes.len()).map(|(b, i)| b * 2.pow(8 * i)).sum();

fn from_bytes_le(bytes: &[T]) -> T {
    let mut res = 0;
    for i in 0..bytes.len() {
        res += b * 2.pow(8 * i)
    }
    res
}

IsZero

inputs:

  • value: any

outputs:

  • is_zero: bool
gadget iz_zero(value: expr) -> bool expr {
    let value_inv: witness;
    witness {
        value_inv = if value != 0 {
            value.invert();
        } else {
            0
        };
    }
    let is_zero_expression: bool expr = 1 - value * value_inv;
    @ value * value_inv = 0;
    return is_zero_expression;
}

LowerThan

inputs:

  • lhs: range(0, 2.pow(8*N))
  • rhs: range(0, 2.pow(8*N))

outputs:

  • lt: bool
gadget lt(N: usize, lhs: T2P8 expr, rhs: T2P8 expr) -> bool witness 
    where T2P8 is range(0, 2.pow(8*N)) {
    let lt: bool witness;
    witness {
        lt = lhs < rhs;
    }
    let diff_bytes: [u8 witness; N];
    witness {
        let diff: field = (lhs - rhs) + if lt { 2.pow(8*N) } else { 0 };
        for i in 0..N {
            diff_bytes[i] = (diff >> 8*i) & 0xff;
        }
    }
    let diff: T2P8 expr = from_bytes_le(diff_bytes);
    @ lhs - rhs = diff - lt * 2.pow(8*N);
    return lt;
}

Add256

inputs:

  • a: [u8 expr; 32]
  • b: [u8 expr; 32]
alias u128 = range(0, 2.pow(128));
gadget add256(a_le: [u8 expr; 32], b_le: [u8 expr; 32]) -> ([u8 witness; 32], bool witness) {
    let res_le: [u8 witness; 32];
    let carry_lo: range(0, 1) witness;
    let carry_hi: range(0, 1) witness;
    witness {
        let mut carry = 0;
        for i in 0..32 {
            let tmp = a_le[i] + b_le[i];
            res_le[i] = tmp & 0xff + carry;
            carry = tmp >> 8;
            if i == 15 {
                carry_lo = carry;
            }
        }
        carry_hi = carry;
    }

    let a_lo: u128 expr = from_bytes_le(a_le[..16]);
    let b_lo: u128 expr = from_bytes_le(b_le[..16]);
    let a_hi: u128 expr = from_bytes_le(a_le[16..]);
    let b_hi: u128 expr = from_bytes_le(b_le[16..]);
    let res_lo: u128 expr = from_bytes_le(res_le[..16]);
    let res_hi: u128 expr = from_bytes_le(res_le[16..]);
    @ a_lo + b_lo = res_lo + carry_lo * 2.pow(128);
    @ a_hi + b_hi + carry_lo = res_hi + carry_hi * 2.pow(128);
    return res_le;
}

Bytecode circuit

An example of a state machine + lookupable table circuit

https://hackmd.io/Cv5Pmh8fRyuuuwCFcCZdzg

Types:

  • Tag: enum{ Length, Byte }
  • Word: [u128, u128]

BytecodeLookup:

  • codeHash: Word
  • tag: Tag
  • index: u16
  • value: u8

State:

  • tag: Tag
  • length: u16
  • index: u16
  • value: u8
  • is_code: bool
  • push_data_size: u16
  • push_data_left: u16
  • hash: Word
  • values_rlc: field
  • is_first: bool fixed
  • is_last: bool fixed

Witness: list of State structs with the following values defined:

  • tag
  • if tag == Length
    • length
    • hash
  • if tag == Byte
    • value
circuit bytecode(curr: State, next: State) {
    // Length state validation
    if curr.tag == Length {
        @ curr.index = 0;
        @ curr.value = curr.length;
        if curr.length == 0 {
            @ curr.hash = EMPTY_HASH;
        }
    }
    // Byte state validation
    if curr.tag == Byte {
        @ curr.push_data_size = push_data_size_table[curr.value];
        @ curr.is_code = (curr.push_data_left == 0);
        if curr.is_code {
            @ next.push_data_left = curr.push_data_size;
        } else {
            @ next.push_data_left = curr.push_data_left - 1;
        }
    }

    // Start state
    if curr.is_first {
        @ curr.tag = Tag.Length;
    } 
    // End state
    if curr.is_last {
        @ curr.tag = Tag.Length;
    }

    // State transition validation
    if !curr.is_last {
        // Length -> Byte
        if curr.tag == Length and next.tag == Byte {
            @ next.length = curr.length;
            @ next.index = 0;
            @ next.is_code = 1;
            @ next.hash = curr.hash;
            @ next.values_rlc = next.value;
            @ next.value = any;
            @ next.push_data_left = any;
        }

        // Length -> Length
        if curr.tag == Length and next.tag == Length {
            @ curr.length = 0;
            @ curr.hash = EMPTY_HASH;
            @ next.length = any;
            @ next.index = any;
            @ next.value = any;
            @ next.is_code = any;
            @ next.push_data_left = any;
            @ next.hash = any;
            @ next.values_rlc = any;
        }

        // Byte -> Byte
        if curr.tag == Byte and next.tag == Byte {
            @ next.length = curr.length;
            @ next.index = curr.index + 1;
            @ next.hash = curr.hash;
            @ next.values_rlc = curr.values_rlc * randomness + curr.value;
            @ next.value = any;
        }

        // Byte -> Length
        if curr.tag == Byte and next.tag == Length {
            @ curr.index = curr.length - 1;
            @ curr.hash = keccak256[curr.values_rlc, curr.length];
            @ next.length = any;
            @ next.index = any;
            @ next.value = any;
            @ next.hash = any;
            @ next.values_rlc = any;
        }
    }
}

Exercice: write a function that given a list of byte vectors, generates the list of Bytecode circuit states.

fn gen(inputs: &[Vec<u8>]) -> Vec<State> {
    let mut states = Vec::new();
    for input in inputs {
        states.push(State{
            tag: Lenght,
            value: input.len(),
            hash: rlc(r, hash(input)),
        });
        for byte in input {
            states.push(State{
                tag: Byte,
                value: byte,
            });
        }
    }
}