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.

Sign up for GitHub

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

IVC: Add selector columns #2233

Merged
merged 9 commits into from
May 28, 2024
Merged

IVC: Add selector columns #2233

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
7d4d6db
[#2231] Add BlockSel columns into IVC
volhovm May 16, 2024
4b6821b
[#2231] Implement simple set_assert_mapper
volhovm May 16, 2024
30c9950
[#2231] Add write_sel for block functions
volhovm May 16, 2024
ca75363
[#2231] Add completeness test w/ selectors
volhovm May 16, 2024
1847b26
[#2231] Make IVC interpreter work in completeness test
volhovm May 17, 2024
d8cca45
[#2231] Generalise set_assert_mapper properly
volhovm May 17, 2024
ed19c04
[#2231] Fix IVC column indexing
volhovm May 28, 2024
2dd268f
[#2231] Rename cur into curr
volhovm May 28, 2024
58e35d5
[#2231] Cosmetics
volhovm May 28, 2024
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
83 changes: 52 additions & 31 deletions ivc/src/ivc/columns.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,9 @@ use kimchi_msm::{
serialization::interpreter::{N_LIMBS_LARGE, N_LIMBS_SMALL},
};

/// Number of blocks in the circuit.
pub const N_BLOCKS: usize = 6;

pub const IVC_POSEIDON_STATE_SIZE: usize = 3;
pub const IVC_POSEIDON_NB_FULL_ROUND: usize = 55;

Expand Down Expand Up @@ -151,6 +154,9 @@ pub type IVCPoseidonColumn = PoseidonColumn<IVC_POSEIDON_STATE_SIZE, IVC_POSEIDO
///
/// Challenges block.
///
/// relaxed
/// strict
/// (relaxed in-place)
/// r α_{L,i} α_{R}^i α_{O,i}
/// 1 |--|--------|-----------|-------------------|
/// | | | α_R = h_R | |
Expand Down Expand Up @@ -212,6 +218,9 @@ pub type IVCPoseidonColumn = PoseidonColumn<IVC_POSEIDON_STATE_SIZE, IVC_POSEIDO
// TODO: Can we pass just one coordinate and sign (x, sign) instead of (x,y) for hashing?
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
pub enum IVCColumn {
/// Selector for blocks. Inner usize is ∈ [0,#blocks).
Copy link
Member

Choose a reason for hiding this comment

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

I cannot find the up-to-date description of each different block. Is it the ones at the top of file?
My question is related to the function build_selectors, to verify the selectors are populated according to the spec.

Copy link
Member Author

Choose a reason for hiding this comment

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

Yes, the general description of each block is in the top of columns.rs. I don't know how to create const usize definitions for block sizes, because they depend on N_COL_TOTAL and N_CHALS and generic consts in rust are not supported....

Copy link
Member Author

Choose a reason for hiding this comment

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

I fixed this by adding block_height function... but I see it's merged? heh

BlockSel(usize),
volhovm marked this conversation as resolved.
Show resolved Hide resolved

/// 2*17 15-bit limbs (two base field points)
Block1Input(usize),
/// 2*4 75-bit limbs
Expand Down Expand Up @@ -284,78 +293,90 @@ impl ColumnIndexer for IVCColumn {
// This should be
// const N_COL: usize = std::cmp::max(IVCPoseidonColumn::N_COL, FECColumn::N_COL);
// which is runtime-only expression..?
const N_COL: usize = IVCPoseidonColumn::N_COL;
// 333 is not enough
const N_COL: usize = 400;
volhovm marked this conversation as resolved.
Show resolved Hide resolved

fn to_column(self) -> Column {
match self {
IVCColumn::BlockSel(i) => {
assert!(i < 2 * N_BLOCKS);
volhovm marked this conversation as resolved.
Show resolved Hide resolved
Column::FixedSelector(i)
}

IVCColumn::Block1Input(i) => {
assert!(i < 2 * N_LIMBS_SMALL);
Column::Relation(i)
Column::Relation(N_BLOCKS + i)
volhovm marked this conversation as resolved.
Show resolved Hide resolved
volhovm marked this conversation as resolved.
Show resolved Hide resolved
}
IVCColumn::Block1InputRepacked75(i) => {
assert!(i < 2 * N_LIMBS_LARGE);
Column::Relation(2 * N_LIMBS_SMALL + i)
Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + i)
}
IVCColumn::Block1InputRepacked150(i) => {
assert!(i < 2 * N_LIMBS_XLARGE);
Column::Relation(2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i)
Column::Relation(N_BLOCKS + 2 * N_LIMBS_SMALL + 2 * N_LIMBS_LARGE + i)
}

IVCColumn::Block2Hash(poseidon_col) => poseidon_col.to_column(),
IVCColumn::Block2Hash(poseidon_col) => {
poseidon_col.to_column().add_rel_offset(N_BLOCKS)
}

IVCColumn::Block3ConstPhi => Column::Relation(0),
IVCColumn::Block3ConstR => Column::Relation(1),
IVCColumn::Block3PhiPow => Column::Relation(2),
IVCColumn::Block3PhiPowR => Column::Relation(3),
IVCColumn::Block3PhiPowR2 => Column::Relation(4),
IVCColumn::Block3PhiPowR3 => Column::Relation(5),
IVCColumn::Block3ConstPhi => Column::Relation(N_BLOCKS),
volhovm marked this conversation as resolved.
Show resolved Hide resolved
IVCColumn::Block3ConstR => Column::Relation(N_BLOCKS + 1),
Copy link
Member

Choose a reason for hiding this comment

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

To me it looks like IVCColumn::Block1Input(i) and IVCColumn::Block3ConstR could collide for example when i=1, no?

Copy link
Member

@dannywillems dannywillems May 28, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

It makes sense to collide. It is like selectors q_l, q_r, q_m in vanilla plonk. The columns are shared.

Copy link
Member

Choose a reason for hiding this comment

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

I am not sure I understand why you want redundant definitions of the same column. Like, it is not as if you could access multiple rows for each constraint no? Like, at most the current row and the next, but not 4 rows ahead...

Copy link
Member

Choose a reason for hiding this comment

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

I don't understand. We can talk about it in a call, easier.

Copy link
Member Author

Choose a reason for hiding this comment

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

All the blocks share most columns. The whole point of the column indexer is to semantically separate which columns have which meaning. The opposite approach would be to just use integers for column indexing, which is inconvenient and has zero type-safety. Maybe I don't understand what you mean...?

IVCColumn::Block3PhiPow => Column::Relation(N_BLOCKS + 2),
IVCColumn::Block3PhiPowR => Column::Relation(N_BLOCKS + 3),
IVCColumn::Block3PhiPowR2 => Column::Relation(N_BLOCKS + 4),
IVCColumn::Block3PhiPowR3 => Column::Relation(N_BLOCKS + 5),
IVCColumn::Block3PhiPowLimbs(i) => {
assert!(i < N_LIMBS_SMALL);
Column::Relation(6 + i)
Column::Relation(N_BLOCKS + 6 + i)
}
IVCColumn::Block3PhiPowRLimbs(i) => {
assert!(i < N_LIMBS_SMALL);
Column::Relation(6 + N_LIMBS_SMALL + i)
Column::Relation(N_BLOCKS + 6 + N_LIMBS_SMALL + i)
}
IVCColumn::Block3PhiPowR2Limbs(i) => {
assert!(i < N_LIMBS_SMALL);
Column::Relation(6 + 2 * N_LIMBS_SMALL + i)
Column::Relation(N_BLOCKS + 6 + 2 * N_LIMBS_SMALL + i)
}
IVCColumn::Block3PhiPowR3Limbs(i) => {
assert!(i < N_LIMBS_SMALL);
Column::Relation(6 + 3 * N_LIMBS_SMALL + i)
Column::Relation(N_BLOCKS + 6 + 3 * N_LIMBS_SMALL + i)
}

IVCColumn::Block4Input1(i) => {
assert!(i < 2 * N_LIMBS_LARGE);
Column::Relation(i)
Column::Relation(N_BLOCKS + i)
}
IVCColumn::Block4Coeff => Column::Relation(8),
IVCColumn::Block4Input2AccessTime => Column::Relation(9),
IVCColumn::Block4Coeff => Column::Relation(N_BLOCKS + 8),
IVCColumn::Block4Input2AccessTime => Column::Relation(N_BLOCKS + 9),
IVCColumn::Block4Input2(i) => {
assert!(i < 2 * N_LIMBS_LARGE);
Column::Relation(10 + i)
Column::Relation(N_BLOCKS + 10 + i)
}
IVCColumn::Block4ECAddInter(fec_inter) => {
fec_inter.to_column().add_rel_offset(N_BLOCKS + 18)
}
IVCColumn::Block4ECAddInter(fec_inter) => fec_inter.to_column().add_rel_offset(18),
IVCColumn::Block4OutputRaw(fec_output) => fec_output
.to_column()
.add_rel_offset(18 + FECColumnInter::N_COL),
.add_rel_offset(N_BLOCKS + 18 + FECColumnInter::N_COL),
IVCColumn::Block4OutputAccessTime => {
Column::Relation(18 + FECColumnInter::N_COL + FECColumnOutput::N_COL)
Column::Relation(N_BLOCKS + 18 + FECColumnInter::N_COL + FECColumnOutput::N_COL)
}
IVCColumn::Block4OutputRepacked(i) => {
assert!(i < 2 * N_LIMBS_LARGE);
Column::Relation(18 + FECColumnInter::N_COL + FECColumnOutput::N_COL + 1 + i)
Column::Relation(
N_BLOCKS + 18 + FECColumnInter::N_COL + FECColumnOutput::N_COL + 1 + i,
)
}
IVCColumn::Block5ConstHr => Column::Relation(0),
IVCColumn::Block5ConstR => Column::Relation(1),
IVCColumn::Block5ChalLeft => Column::Relation(2),
IVCColumn::Block5ChalRight => Column::Relation(3),
IVCColumn::Block5ChalOutput => Column::Relation(4),
IVCColumn::Block5ConstHr => Column::Relation(N_BLOCKS),
IVCColumn::Block5ConstR => Column::Relation(N_BLOCKS + 1),
IVCColumn::Block5ChalLeft => Column::Relation(N_BLOCKS + 2),
IVCColumn::Block5ChalRight => Column::Relation(N_BLOCKS + 3),
IVCColumn::Block5ChalOutput => Column::Relation(N_BLOCKS + 4),

IVCColumn::Block6ConstR => Column::Relation(0),
IVCColumn::Block6ULeft => Column::Relation(1),
IVCColumn::Block6UOutput => Column::Relation(2),
IVCColumn::Block6ConstR => Column::Relation(N_BLOCKS),
IVCColumn::Block6ULeft => Column::Relation(N_BLOCKS + 1),
IVCColumn::Block6UOutput => Column::Relation(N_BLOCKS + 2),
}
}
}
Expand Down
141 changes: 115 additions & 26 deletions ivc/src/ivc/interpreter.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@
use crate::{
ivc::{
columns::{
IVCColumn, IVCFECLens, IVCHashLens, IVC_POSEIDON_NB_FULL_ROUND, IVC_POSEIDON_STATE_SIZE,
IVCColumn, IVCFECLens, IVCHashLens, IVC_POSEIDON_NB_FULL_ROUND,
IVC_POSEIDON_STATE_SIZE, N_BLOCKS,
},
lookups::{IVCFECLookupLens, IVCLookupTable},
},
Expand Down Expand Up @@ -184,7 +185,7 @@ where

pub fn write_inputs_row<F, Ff, Env, const N_COL_TOTAL: usize>(
env: &mut Env,
target_comms: [(Ff, Ff); N_COL_TOTAL],
target_comms: &[(Ff, Ff); N_COL_TOTAL],
row_num_local: usize,
) -> (Vec<F>, Vec<F>, Vec<F>)
where
Expand Down Expand Up @@ -245,11 +246,11 @@ where
#[allow(clippy::type_complexity)]
pub fn process_inputs<F, Ff, Env, const N_COL_TOTAL: usize>(
env: &mut Env,
comms: [[(Ff, Ff); N_COL_TOTAL]; 3],
comms: [Box<[(Ff, Ff); N_COL_TOTAL]>; 3],
) -> (
[[[F; 2 * N_LIMBS_SMALL]; N_COL_TOTAL]; 3],
[[[F; 2 * N_LIMBS_LARGE]; N_COL_TOTAL]; 3],
[[[F; 2 * N_LIMBS_XLARGE]; N_COL_TOTAL]; 3],
Box<[[[F; 2 * N_LIMBS_SMALL]; N_COL_TOTAL]; 3]>,
volhovm marked this conversation as resolved.
Show resolved Hide resolved
Box<[[[F; 2 * N_LIMBS_LARGE]; N_COL_TOTAL]; 3]>,
Box<[[[F; 2 * N_LIMBS_XLARGE]; N_COL_TOTAL]; 3]>,
)
where
F: PrimeField,
Expand All @@ -263,11 +264,11 @@ where
let row_num = env.curr_row();

let (target_comms, row_num_local, comtype) = if row_num < N_COL_TOTAL {
(comms[0], row_num, 0)
(&comms[0], row_num, 0)
} else if row_num < 2 * N_COL_TOTAL {
(comms[1], row_num - N_COL_TOTAL, 1)
(&comms[1], row_num - N_COL_TOTAL, 1)
} else {
(comms[2], row_num - 2 * N_COL_TOTAL, 2)
(&comms[2], row_num - 2 * N_COL_TOTAL, 2)
};

let (limbs_small, limbs_large, limbs_xlarge) =
Expand All @@ -286,20 +287,22 @@ where
// Left-Right-Output for a given limb size.
fn repack_output<F: PrimeField, const TWO_LIMB_SIZE: usize, const N_COL_TOTAL: usize>(
input: [Vec<Vec<F>>; 3],
) -> [[[F; TWO_LIMB_SIZE]; N_COL_TOTAL]; 3] {
input
.into_iter()
.map(|vector: Vec<Vec<_>>| {
vector
.into_iter()
.map(|subvec: Vec<_>| subvec.try_into().unwrap())
.collect::<Vec<_>>()
.try_into()
.unwrap()
})
.collect::<Vec<_>>()
.try_into()
.unwrap()
) -> Box<[[[F; TWO_LIMB_SIZE]; N_COL_TOTAL]; 3]> {
volhovm marked this conversation as resolved.
Show resolved Hide resolved
Box::new(
input
.into_iter()
.map(|vector: Vec<Vec<_>>| {
vector
.into_iter()
.map(|subvec: Vec<_>| subvec.try_into().unwrap())
.collect::<Vec<_>>()
.try_into()
.unwrap()
})
.collect::<Vec<_>>()
.try_into()
.unwrap(),
)
}

(
Expand Down Expand Up @@ -913,15 +916,101 @@ where
{
}

/// Builds selectors for the IVC circuit.
pub fn build_selectors<F, const N_COL_TOTAL: usize, const N_CHALS: usize>(
Copy link
Member

@dannywillems dannywillems May 28, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

LGTM, modulo https://github.com/o1-labs/proof-systems/pull/2233/files?diff=split&w=1#r1617095007

domain_size: usize,
) -> Vec<Vec<F>>
where
F: PrimeField,
{
// 3*N + 6*N+2 + N+1 + 35*N + 5 + 1 + N_CHALS =
Copy link
Member

Choose a reason for hiding this comment

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

Maybe change the order to N_CHALS + 1 so that it matches the order of the for-loops below.

Copy link
Member Author

Choose a reason for hiding this comment

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

Done

// 45N + 9 + N_CHALS
let mut selectors: Vec<Vec<F>> = vec![vec![F::zero(); domain_size]; N_BLOCKS];
let mut cur_row = 0;
volhovm marked this conversation as resolved.
Show resolved Hide resolved
for _i in 0..3 * N_COL_TOTAL {
selectors[0][cur_row] = F::one();
cur_row += 1;
}
for _i in 0..6 * N_COL_TOTAL + 2 {
selectors[1][cur_row] = F::one();
cur_row += 1;
}
for _i in 0..N_COL_TOTAL + 1 {
selectors[2][cur_row] = F::one();
cur_row += 1;
}
for _i in 0..(35 * N_COL_TOTAL + 5) {
selectors[3][cur_row] = F::one();
cur_row += 1;
}
for _i in 0..N_CHALS {
selectors[4][cur_row] = F::one();
cur_row += 1;
}
for _i in 0..1 {
selectors[5][cur_row] = F::one();
cur_row += 1;
}

selectors
}

/// This function generates constraitns for the whole IVC circuit.
pub fn constrain_selectors<F, Env>(env: &mut Env)
where
F: PrimeField,
Env: ColAccessCap<F, IVCColumn>,
{
for i in 0..N_BLOCKS {
Copy link
Member

@dannywillems dannywillems May 28, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

If selectors are public values, i.e. part of the setup, I think we do not need to add constraints. Constraints are only required for variables the prover performs computations with.

Copy link
Member Author

Choose a reason for hiding this comment

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

Maybe, but I'm not entirely convinced -- it seems to me that when we're folding the circuit we'll have to constrain these values. For just regular proofs -- yes, it makes sense. I suggest we keep it just in case (it's cheap), and can remove it later. I added a comment above this function. OK with you?

Copy link
Member

Choose a reason for hiding this comment

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

Ok to merge like this, but not needed. I would merge the PR, and we can move from there.

// Each selector must have value either 0 or 1.
let sel = env.read_column(IVCColumn::BlockSel(i));
env.assert_zero(sel.clone() * (sel.clone() - Env::constant(F::from(1u64))));
volhovm marked this conversation as resolved.
Show resolved Hide resolved
volhovm marked this conversation as resolved.
Show resolved Hide resolved
}
}

/// This function generates constraitns for the whole IVC circuit.
volhovm marked this conversation as resolved.
Show resolved Hide resolved
pub fn constrain_ivc<F, Ff, Env>(env: &mut Env)
where
F: PrimeField,
Ff: PrimeField,
Env: ColAccessCap<F, IVCColumn> + LookupCap<F, IVCColumn, IVCLookupTable<Ff>>,
{
constrain_selectors(env);

let s0 = env.read_column(IVCColumn::BlockSel(0));
env.set_assert_mapper(Box::new(move |x| s0.clone() * x));
volhovm marked this conversation as resolved.
Show resolved Hide resolved
constrain_inputs(env);

// TODO FIXME add constraints for hashes
volhovm marked this conversation as resolved.
Show resolved Hide resolved

let s2 = env.read_column(IVCColumn::BlockSel(2));
env.set_assert_mapper(Box::new(move |x| s2.clone() * x));
volhovm marked this conversation as resolved.
Show resolved Hide resolved
constrain_ecadds(env);

let s3 = env.read_column(IVCColumn::BlockSel(3));
env.set_assert_mapper(Box::new(move |x| s3.clone() * x));
constrain_scalars(env);

let s4 = env.read_column(IVCColumn::BlockSel(4));
env.set_assert_mapper(Box::new(move |x| s4.clone() * x));
constrain_challenges(env);

let s5 = env.read_column(IVCColumn::BlockSel(5));
env.set_assert_mapper(Box::new(move |x| s5.clone() * x));
constrain_u(env);

env.set_assert_mapper(Box::new(move |x| x));
}

/// Instantiates the IVC circuit for folding. L is relaxed (folded)
/// instance, and R is strict (new) instance that is being relaxed at
/// this step. `N_COL_TOTAL` is the total number of columnsfor IVC + APP.
#[allow(clippy::too_many_arguments)]
pub fn ivc_circuit<F, Ff, Env, PParams, const N_COL_TOTAL: usize>(
env: &mut Env,
comms_left: [(Ff, Ff); N_COL_TOTAL],
comms_right: [(Ff, Ff); N_COL_TOTAL],
comms_out: [(Ff, Ff); N_COL_TOTAL],
comms_left: Box<[(Ff, Ff); N_COL_TOTAL]>,
comms_right: Box<[(Ff, Ff); N_COL_TOTAL]>,
comms_out: Box<[(Ff, Ff); N_COL_TOTAL]>,
error_terms: [(Ff, Ff); 3], // E_L, E_R, E_O
t_terms: [(Ff, Ff); 2], // T_0, T_1
u_l: F, // part of the relaxed instance.
Expand Down
9 changes: 9 additions & 0 deletions ivc/src/ivc/lookups.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,15 @@ impl<Ff: PrimeField> LookupTableID for IVCLookupTable<Ff> {
}
}

impl<Ff: PrimeField> IVCLookupTable<Ff> {
/// Provides a full list of entries for the given table.
pub fn entries<F: PrimeField>(&self, domain_d1_size: u64) -> Vec<F> {
match self {
Self::SerLookupTable(lt) => lt.entries(domain_d1_size),
}
}
}

pub struct IVCFECLookupLens<Ff>(pub PhantomData<Ff>);

impl<Ff> MPrism for IVCFECLookupLens<Ff> {
Expand Down
Loading
Loading