# ZKEVM - Precompile Table

## Layout

### Memory as byte per row

#### Single table for all precompiles

| `sequence_id` | `operation` | `io` | `length` | `index` | `byte` |
| ------------- | ------------------------------------------------------------------------------------------------------------------------ | ------------------------------------------ | -------- | ------- | ------ |
| | <ul><li>`ECRECOVER`</li><li>`SHA256`</li><li>`RIPEMD160`</li><li>`MODEXP`</li><li>`ECADD`</li><li>`ECMUL`</li><li>`ECPAIRING`</li><li>`BLAKE2F`</li><li>`PAD`</li></ul> | <ul><li>`INPUT`</li><li>`OUTPUT`</li></ul> | | | |

Each precompile sub circuits will scan through the `sequence_id` to verify that `output == operation(input)`, and check the boundary of the range are different `operation`, hence we guarantee that everything in precompile table is correct.

If single sub circuit couldn't verify all input/output pairs in precompile table, we could also adopt any IVC scheme to incrementally scan through them

#### Taking inputs from the EVM circuit and the flow of operations

We don't really hex the values in the EVM, done in state circuit. Copy circuit will read byte by byte from the state circuit and write it into the precompile table. Until this point, we have no guarantee that everything in the table is correct. THIS is where the precompile subcircuit comes into play.

#### What does the subcircuit/precompile circuit take as input?

struct Bn254AddTable_Circuit{
    sq_id: Column<Advice>,
    // operation: u8,
    // length: u8,
    io: Column<Advice>,
    index: Column<Advice>, 
    byte: Column<Advice>,
}
//here the table is for PPLONKish arithmetization/circuit

struct Bn254AddTableRow{
    sq_id: usize,
    // operation: u8,
    // length: u8,
    io: bool,
    index: usize, 
    byte: u8
} //here the table is like Vec<Bn254AddTableRow> just conceptuallh

struct Bn254AddCircuit<F: ScalarField> {
    // a.x, a.y, b.x, b.y
   // inputs: Vec<EcPoint<F, CRTInteger<F>>>; //in this case, no range check is req because F specializes to Fr anyway
    inputs: Vec<[[u8; 32]; 4]>,
    // output: Vec<[[u8;32]; 2]> // 
}

fn bn_add(input: [[u8; 32]; 4]) -> [[u8; 32]; 2] {
    let [ax, ay, bx, by] = input;
    let ax = f_from_bytes(ax);
    let ay = f_from_bytes(ay);
    let bx = f_from_bytes(bx);
    let by = f_from_bytes(by);
    
    match (ax, ay, bx, by) {
        ((Some(ax), Some(ay), Some(bx), Some(by))) => {
            // return a + b
        }
        _ => {
            [[0; 32]; 2]
        }
    }
}

//assume that it will not be in the check
i
impl Circuit<F> for Bn254AddCircuit<F> {
    
    //usually we model it based on the EVM, but can allocate it myself in main -> and this is through just copying values or 'assigning' regions according to the normal BN254 Table Row
    
    fn configure(meta, bn254_add_table: Bn254AddTable_Circuit) -> Self::Config {
        let u8_table = meta.fixed_column();
        let [sq_id, io, index, byte] = bn254_add_table;

        meta.lookup(byte -> u8_table);
    }

    fn load_table(&self, layouter) -> Result<Vec<[[AssignedCell<F>; 32]; 6]>, Error> {
        layouter.assign_region(|region| {
            let mut offset = 0;
            for (sq_id, input) in self.inputs.iter().enmuerate() {
                let output = bn_add(input); //for the prover to do
                for (index, byte) in input.iter().enumerate() {
                    // region.assign(...)
                }
                for (index, byte) in output.iter().enumerate() {
                    let index = index + 64;
                    // region.assign(...)
                }
            } 
        });
    }
    
    //output == operation(input)

    fn syntehsize(&self) -> Result<(), Error> {
        let ios = self.load_table();
        // check output == operation(input)
        for io in ios.iter() {
            let [ax, ay, bx, by, cx, cy] = io;
            let ax = main_gate.assign_field_from_bytes(ax)?;
            // 
            
            let a = main_gate.assign_point(ax, ay);
            // 

            main_gate.assert_eq(main_gate.add(a, b), c);

           
            
            // Copy bytes to Maingate region, and do curve/field operations
            //convert into CRTInteger, and check the range 
        }
//         //range check
//         for (sequence_id, input) in self.inputs.iter().enumerate() {
//             // ax = [u8; 32]
//             let [ax, ay, bx, by] = input;
//             //maybe use rangechip here to do a rangecheck for normal 8 bit inputs
//             let (ax, ax_is_valid) = self.assign_field(ax)?;
//             let (ay, ay_is_valid) = self.assign_field(ay)?;
//             let (bx, bx_is_valid) = self.assign_field(bx)?;
//             let (by, by_is_valid) = self.assign_field(by)?;
            
//             //each ax, ay, bx, by should lie on the BN254 Scalar Field 
//             //what happens in halo2-lib is load input, and do range_check(input, bits), so it checks for input belongs to 
//             // [0, 2^bits)
            
            
//             // perform addition here if all are valid field elements
        
                //todo - use EccChip/halo2-ecc to perform the operations
        
                //add test cases
            
//             let output = ...;
            
            
//         }
    }
}

a.x = [0xfffffffffffff..ff]

#### Per table for each precompile

We can also have per table for ecah precompile, just need to ignore the `operation` column.

### Memory as word per row

Considering we might want to have memory as word per row, the Copy circuit will also be adjusted to work with that, for the precompile table we just need to change the `byte` into `word`, then the sub circuits need to do the decomposition themselves when necessary.

## Connect to EVM circuit

In EVM cirucit, when we encounter call to precompile address, we will do a copy table lookup, then inside Copy circuit it will copy input/output bytes to the precompile table with specified `operation`.

## Rationale

For most precompiles they could be used with input with dynamic size (`SHA256`, `RIPEMD160`, `MODEXP`, `ECPAIRING`, `BLAKE2F`), it'd be easier to realize to have a single interface to connect EVM circuit with precompile table, and we could reuse the Copy circuit as the bridge to pass around these input/output.

{%hackmd C0hM4L6mT9-5XXfjBXmAxA %}

## High level step-by-step analysis of precompile implementation

<ol>
For testing purposes, or from the main EVM circuit, take in (input, output) in the form of [(seq id, operation_tag, 1 , length, data), (seq id, operation_tag, 0, length, data)]

This will be for one single operation/precompile call.
</ol>

Copy the contents of this (input, output) into the existing precompile table, adding an extra column, ```index``` (ranging from 0...length-1), iterating over the vectors

<ol>

</ol>