Tying event tape commitment as part of vm proof

[codeblooded1729]

The Problem:

We assume honest provers using a provided SDK that generates correct proofs and event tapes.
We want to protect these provers from a malicious sequencer who might try to alter the event tape.
The sequencer needs to verify the proof, which ideally should include a canonical commitment to the event tape for verification.

Challenges of Existing Solutions:

Variable-Length Event Tape:

Ideally, the proof verification circuit (built with Plonky2) should take a commitment to the event tape as input.
However, the event tape can vary in length, making it difficult to have a fixed verification circuit in Plonky2.

Extracting Commitment from Starky Proofs:

An alternative is to have the prover's code (provided by the SDK) compute the canonical commitment before generating the proof.
To link this commitment to the final proof, it needs to be extracted from the Starky proof and integrated into the Plonky2 proof.
This involves making 32 entries referring to the commitment in MemoryInit table public, potentially requiring a significant increase in number of selector columns.

Proposed Solution: Dedicated Event Tape Hash Table:

Introduce a pre-initialized memory region named event_tape_commitment.
Populate the commitment values in the MemoryInit table as usual.
Create a dedicated Stark table named EventTapeHashTable.
This table will only have one populated row with entries for address (addr) and value, both marked public.
A filter (is_first) differentiates this single row from padded entries, as well as
allowes us to do cross table lookup against the MemoryInit table with the public entries in the EventTapeHashTable.
The only difference between this and the former approach is that we have to constrain only single row, as opposed to 32 rows. This greatly simplifies public input constraints, and number of extra selector columns required

[codeblooded1729]

Steps to integrate

1. include a pre initialized memory region event_tape_commitment say at addr EVENTCOMM
2. Create a new table EventTapeCommitment

pub struct EventTapeCommitment{
       pub addr: [F; 32]
       pub values: [F: 32]
       pub is_first: F
}

Apart from its populated first row, all other rows would be padding rows. We can set number of rows to any minimal table size that our proof system can support. 8 should be fine.
3. set PUBLIC_INPUTS = 32 for its Stark
4. Include the following constraints on first row

• addr[i] = EVENTCOMM + i, value[i] = public_input[i] for i in 0..32
• is_first = 1

5. include constraints to ensure all is_first is set to 0 for padded rows
6. include 32 CTLs against MemoryInit table of the form (addr[i], value[i], is_first)
7. Update our public inputs struct

pub struct PublicInputs<F> {
    pub entry_point: F,
    pub event_comm: [F; 32],
}

8. Make sure the hash is linked to public inputs for EventTapeCommitment stark, for both prover and verifier.

[sai-deng]

If I understand it correctly, you will use #1369 to connect the pre-initialized memory region 'event_tape_commitment' with the actual 'event_tape'?

[sai-deng]

An alternative method:
Same as your method to connect 'event_tape_commitment' with the actual 'event_tape' in the pre-initialized memory region.
Instead of creating a new STARK table, can we simply add PUBLIC_INPUTS = 32 in MozakStark? In the verifier, we simply run a permutation check (grand product) of these 32 inputs and the associated MemoryInit columns.

[codeblooded1729]

This is a nice idea! In fact we can make an api out of this which allows us to "open" certain row values, without actually opening the trace polynomials at these rows!
Let me put forth my understanding of how can we go about making this api

1. We would have a separate filter column to specify the rows which we want to open. The API would look like

pub fn open_event_commitment() -> Table {
       MemoryInitTable::new(
           Column::singles(col_map().addr, col_map().value),
           col_map().event_commitment  // ---> filter column for identifying event tape commitment rows
       )
}

2. We can use the generated challenge gamma to create a running grand product (or running sum, like in logup), just like in CTL. The polynomial corresponding to this would be called open_public
3. Prover opens open_public at last row as open_public_val just like how we do in CTL. This value corresponds to final grand product
4. He constrains grand_product(public_values[TableKind::MemoryInit], gamma) == open_public_val

let me know if this is all good

[sai-deng]

Looks good to me 👍