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

Sketch serialization subcircuit subdirectory #1846

Merged
merged 3 commits into from
Feb 27, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions msm/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ pub mod mvlookup;
pub mod precomputed_srs;
pub mod proof;
pub mod prover;
pub mod serialization;
pub mod verifier;

/// Domain size for the MSM project, equal to the BN254 SRS size.
Expand Down
34 changes: 34 additions & 0 deletions msm/src/serialization/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
## Kimchi Foreign Field gate serialization subcircuit

The 15/16 bulletproof challenges will be given as 88 limbs, the encoding used by Kimchi.
A circuit would be required to convert into 15 bits limbs that will be used for the MSM algorithm.
We will use one row = one decomposition.

We have the following circuit shape:

| $b_{0}$ | $b_{1}$ | $b_{2}$ | $c_{0}$ | $c_{1}$ | ... | $c_{16}$ | $b_{2, 0}$ | $b_{2, 1}$ | ... | $b_{2, 19}$ |
| ------- | ------- | ------- | ------- | ------- | --- | -------- | --------- | --------- | --- | ----------- |
| ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... |
| ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... |

We can suppose that $b_{2}$ is only on 80 bits as the input is maximum
$BN254(\mathbb{F}_{scalar})$, which is 254 bits long.
We will decompose $b_{2}$ in chunks of 4 bits:

$$b_{2} = \sum_{i = 0}^{19} b_{2, i} 2^{4 i}$$

And we will add the following constraint:

1. For the first 180 bits:

$$b_{0} + b_{1} 2^88 + b_{2, 0} * 2^{88 * 2} - \sum_{j = 0}^{11} c_{j} 2^{15 j} = 0$$
dannywillems marked this conversation as resolved.
Show resolved Hide resolved

2. For the remaining 75 bits:

$$c_{12} + c_{13} * 2^{15} + c_{14} 2^{15 * 2} + c_{15} 2^{15 * 3} + c_{16} 2^{15 * 4} = \sum_{j = 1}^{19} b_{2, j} * 2^{4 (j - 1)}$$

with additional lookups.

$b_{0}$, $b_{1}$ and $b_{2}$ are the decomposition on 88 bits given by the
foreign field gate in Kimchi. The values $c_{0}$, $\cdots$, $c_{16}$ are the limbs
required for the MSM circuit. Each limbs $c_{i}$ will be on 15 bits.
30 changes: 30 additions & 0 deletions msm/src/serialization/columns.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
use crate::columns::Column;
use crate::columns::ColumnIndexer;
use crate::LIMBS_NUM;

/// Columns for the circuit splitting the bulletproof challenges in limbs used
/// by the MSM.
pub enum DecompositionColumnIndexer {
KimchiLimbs(usize),
MSMLimbs(usize),
IntermediateKimchiLimbs(usize),
}

impl ColumnIndexer for DecompositionColumnIndexer {
fn ix_to_column(self) -> Column {
match self {
DecompositionColumnIndexer::KimchiLimbs(i) => {
assert!(i < 3);
Column::X(i)
}
DecompositionColumnIndexer::MSMLimbs(i) => {
assert!(i < LIMBS_NUM);
Column::X(3 + i)
}
DecompositionColumnIndexer::IntermediateKimchiLimbs(i) => {
assert!(i < 3 + LIMBS_NUM);
Column::X(3 + LIMBS_NUM + i)
}
}
}
}
1 change: 1 addition & 0 deletions msm/src/serialization/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pub mod columns;