Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

program-table #210

Merged
merged 14 commits into from
Sep 14, 2024
Merged

program-table #210

merged 14 commits into from
Sep 14, 2024

Conversation

naure
Copy link
Collaborator

@naure naure commented Sep 11, 2024

Issue #110.

@naure naure requested a review from kunxian-xia September 11, 2024 15:41
@naure naure marked this pull request as ready for review September 11, 2024 19:53
@naure naure changed the title program-table: initial program table program-table Sep 11, 2024
Copy link
Collaborator

@kunxian-xia kunxian-xia left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR looks good to me except some nitpicks. However, the riscv_add example fails on my local machine.

ceno_zkvm/src/instructions/riscv/addsub.rs Outdated Show resolved Hide resolved
Copy link
Collaborator

@hero78119 hero78119 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

change are very neat!

(A TODO marks in later PR): we also need to extend MockProver to support program table lookup for better debug

range_config.clone(),
&(),
);
zkvm_fixed_traces.register_table_circuit::<ProgramTableCircuit<E>>(
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍 since we register new circuit, to verify e2e test not broken, this PR probabaly go after #209

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense, I’ll just wait and make it work with that test.

Copy link
Collaborator Author

@naure naure Sep 13, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The program table is now integrated in the MockProver as well. Unittests work.

ceno_zkvm/examples/riscv_add.rs Outdated Show resolved Hide resolved
ceno_zkvm/src/tables/program.rs Show resolved Hide resolved
@naure
Copy link
Collaborator Author

naure commented Sep 13, 2024

This PR looks good to me except some nitpicks. However, the riscv_add example fails on my local machine.

I haven’t figured this out yet but I realized it happens to me on master as well.

#222

@naure naure requested a review from kunxian-xia September 13, 2024 17:33
@naure
Copy link
Collaborator Author

naure commented Sep 13, 2024

This is in a good enough shape to merge. Remaining work is in issues.

@naure naure mentioned this pull request Sep 14, 2024
kunxian-xia pushed a commit that referenced this pull request Sep 14, 2024
This is another approach to #223, fixing #222 / #210. Features:

- Prepare for parallel proving with independent transcripts per thread.
- Soundness with different transcripts in each thread.
- Type-safe API which captures the transcript by value.

There is no function to merge the threads back into one transcript, but
that can be added if ever needed.

---------

Co-authored-by: Aurélien Nicolas <[email protected]>
@naure
Copy link
Collaborator Author

naure commented Sep 14, 2024

Resolved merge conflicts and added support for SUB.

@kunxian-xia kunxian-xia merged commit a8174ae into master Sep 14, 2024
6 checks passed
@kunxian-xia kunxian-xia deleted the program-table branch September 14, 2024 13:42
hero78119 added a commit that referenced this pull request Sep 19, 2024
### Goal
To make sumcheck protocol support different num_vars, aiming for
- [x] minimal change to sumcheck protocol, make verifier remain the
same. no extra meta data passed from prover, and what prover have just
mle and it's eval size

Besides this PR also remove some parallism in verifier since it's
unnecessary for relative low cost.

### design rationale
(Also comments in codebase for reference)
To deal with different num_vars, we exploit a fact that for each product
which num_vars < max_num_vars,
for it evaluation value we need to times 2^(max_num_vars - num_vars)
E.g. Giving multivariate poly $f(X) = f_1(X1) + f_2(X), X1 \in {F}^{n'},
X \in {F}^{n}, |X1| := n', |X| = n, n' <= n$
For i round univariate poly, $f^i(x)$
$f^i[0] = \sum_b f(r, 0, b), b \in [0, 1]^{n-i-1}, r \in {F}^{n-i-1}$
chanllenge get from prev rounds
= $\sum_b f_1(r, 0, b1) + f_2(r, 0, b), |b| >= |b1|, |b| - |b1| = n -
n'$
= $2^{(|b| - |b1|)} * \sum_{b1} f_1(r, 0, b1) + \sum_b f_2(r, 0, b)$
same applied on f^i[1]
It imply that, for every evals in f_1, to compute univariate poly, we
just need to times a factor 2^(|b| - |b1|) for it evaluation value


### benchmark
benchmark with ceno_zkvm `riscv_add`, and gkr `keccak` both remain the
same and no impact.
You might see some redundancy coding style, but this is for retain the
best performance. I tried other variants and it impact benchmark results

### scope
Related to #109 #210 ....
To address #126 #127 
This enhance protocol features potiential can be used for `range
table-circuit`, `init/final-memory`, `cpu-init/cpu-final halt` to make
selector sumcheck support batching different num_instance witin.
hero78119 pushed a commit that referenced this pull request Sep 30, 2024
This is another approach to #223, fixing #222 / #210. Features:

- Prepare for parallel proving with independent transcripts per thread.
- Soundness with different transcripts in each thread.
- Type-safe API which captures the transcript by value.

There is no function to merge the threads back into one transcript, but
that can be added if ever needed.

---------

Co-authored-by: Aurélien Nicolas <[email protected]>
hero78119 pushed a commit that referenced this pull request Sep 30, 2024
_Issue #110._

---------

Co-authored-by: Aurélien Nicolas <[email protected]>
hero78119 added a commit that referenced this pull request Sep 30, 2024
### Goal
To make sumcheck protocol support different num_vars, aiming for
- [x] minimal change to sumcheck protocol, make verifier remain the
same. no extra meta data passed from prover, and what prover have just
mle and it's eval size

Besides this PR also remove some parallism in verifier since it's
unnecessary for relative low cost.

### design rationale
(Also comments in codebase for reference)
To deal with different num_vars, we exploit a fact that for each product
which num_vars < max_num_vars,
for it evaluation value we need to times 2^(max_num_vars - num_vars)
E.g. Giving multivariate poly $f(X) = f_1(X1) + f_2(X), X1 \in {F}^{n'},
X \in {F}^{n}, |X1| := n', |X| = n, n' <= n$
For i round univariate poly, $f^i(x)$
$f^i[0] = \sum_b f(r, 0, b), b \in [0, 1]^{n-i-1}, r \in {F}^{n-i-1}$
chanllenge get from prev rounds
= $\sum_b f_1(r, 0, b1) + f_2(r, 0, b), |b| >= |b1|, |b| - |b1| = n -
n'$
= $2^{(|b| - |b1|)} * \sum_{b1} f_1(r, 0, b1) + \sum_b f_2(r, 0, b)$
same applied on f^i[1]
It imply that, for every evals in f_1, to compute univariate poly, we
just need to times a factor 2^(|b| - |b1|) for it evaluation value


### benchmark
benchmark with ceno_zkvm `riscv_add`, and gkr `keccak` both remain the
same and no impact.
You might see some redundancy coding style, but this is for retain the
best performance. I tried other variants and it impact benchmark results

### scope
Related to #109 #210 ....
To address #126 #127 
This enhance protocol features potiential can be used for `range
table-circuit`, `init/final-memory`, `cpu-init/cpu-final halt` to make
selector sumcheck support batching different num_instance witin.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Status: Done
Development

Successfully merging this pull request may close these issues.

add program table circuit register machine bytecode lookup
3 participants