IVC: Add selector columns #2233

volhovm · 2024-05-16T16:04:29Z

Before: ivc_circuit was building all /witness/ wires, but /constraints/, e.g. c_{b0,i}, were available for every block separately. This means c_{b0,i} for block 0 would not work on rows of block 1.

Now:

There are selectors for each block.
Every constraint is now working for the /whole circuit/, since it's now multiplied by selector: sel0 * c_{b0,i}.
Completeness test is added with lookups disabled.

Offtop:

I added the ID lens because I wanted to generalise circuit generator to work for two tables simultaneously. This proved to /not/ be useful. But the ID lens is useful I think so I keep it.

Next step:

Reduce stack usage. It overflows if stack is default 128KB, but fine with 2MB. Done in next PR IVC: Add array allocators/helpers: reduce stack usage #2247.

dannywillems · 2024-05-28T10:15:41Z

Starting having a look now.

ivc/src/ivc/columns.rs

msm/src/circuit_design/constraints.rs

ivc/src/ivc/columns.rs

querolita · 2024-05-28T10:26:17Z

ivc/src/ivc/columns.rs

-            IVCColumn::Block3PhiPowR2 => Column::Relation(4),
-            IVCColumn::Block3PhiPowR3 => Column::Relation(5),
+            IVCColumn::Block3ConstPhi => Column::Relation(N_BLOCKS),
+            IVCColumn::Block3ConstR => Column::Relation(N_BLOCKS + 1),


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

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

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...

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

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...?

ivc/src/ivc/interpreter.rs

msm/src/circuit_design/capabilities.rs

msm/src/circuit_design/composition.rs

msm/src/circuit_design/capabilities.rs

ivc/src/ivc/columns.rs

ivc/src/ivc/mod.rs

ivc/src/ivc/interpreter.rs

dannywillems · 2024-05-28T11:41:31Z

ivc/src/ivc/interpreter.rs

@@ -913,15 +920,101 @@ where
 {
 }

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


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

dannywillems · 2024-05-28T11:44:05Z

ivc/src/ivc/columns.rs

@@ -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).


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.

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....

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

dannywillems · 2024-05-28T11:45:49Z

ivc/src/ivc/interpreter.rs

+    F: PrimeField,
+    Env: ColAccessCap<F, IVCColumn>,
+{
+    for i in 0..N_BLOCKS {


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.

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?

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

ivc/src/ivc/interpreter.rs

dannywillems · 2024-05-28T11:56:28Z

msm/src/circuit_design/capabilities.rs

    type Variable: Clone
        + std::ops::Add<Self::Variable, Output = Self::Variable>
        + std::ops::Sub<Self::Variable, Output = Self::Variable>
        + std::ops::Mul<Self::Variable, Output = Self::Variable>
        + std::ops::Neg<Output = Self::Variable>
        + From<u64>
-        + std::fmt::Debug;
+        + std::fmt::Debug
+        + 'static;


🤔 not sure I like this, but let's see. What will have 'static lifetime?
A value with 'static lifetime will be embedded in the read-only data segment of the binary. Wondering what will be embedded in this segment for all programs...

I think it will be a reference to the function.

I'm also not 100% sure, but this type-level 'static is different from a variable static. The type-level static just means the datatype does not embed non-static references. We can change in the future if necessary, I couldn't find another way :(

msm/src/circuit_design/composition.rs

msm/src/circuit_design/constraints.rs

msm/src/circuit_design/witness.rs

ivc/src/ivc/interpreter.rs

msm/src/circuit_design/witness.rs

dannywillems · 2024-05-28T12:28:57Z

msm/src/circuit_design/witness.rs

@@ -352,6 +362,15 @@ impl<
            witness.cols[N_REL + N_DSEL + i] = self.fixed_selectors[i].clone();


Maybe it is modified later in https://github.com/o1-labs/proof-systems/pull/2249/files, but we should be sure that set_fixed_selectors has been called before.

Agreed. I want to rework the design later on to remove set_fixed_selectors altogether and take selectors from some trait for the column.

Opened #2255

dannywillems · 2024-05-28T12:30:00Z

msm/src/circuit_design/witness.rs

        let domain_size: usize = domain.d1.size as usize;
+
        // Boxing to avoid stack overflow
        let mut witness: Box<Witness<N_COL, Vec<F>>> = Box::new(Witness {
            cols: Box::new(std::array::from_fn(|_| Vec::with_capacity(domain_size))),


Nit: I would always add an assertion at the end of the function, checking that the size of the vector is exactly domain_size. with_capacity does not enforce that.

volhovm added 4 commits May 16, 2024 14:30

[#2231] Add BlockSel columns into IVC

7d4d6db

[#2231] Implement simple set_assert_mapper

4b6821b

[#2231] Add write_sel for block functions

30c9950

[#2231] Add completeness test w/ selectors

ca75363

volhovm marked this pull request as draft May 16, 2024 16:26

volhovm force-pushed the volhovm/2231-ivc-selector-columns branch from 3fb8773 to 6f6b200 Compare May 17, 2024 13:49

volhovm marked this pull request as ready for review May 17, 2024 13:49

volhovm force-pushed the volhovm/2231-ivc-selector-columns branch 3 times, most recently from fe4bfbb to 91e856a Compare May 17, 2024 16:52

volhovm requested review from dannywillems, querolita and fabrizio-m and removed request for querolita May 18, 2024 09:54

volhovm added 2 commits May 20, 2024 14:38

[#2231] Make IVC interpreter work in completeness test

1847b26

[#2231] Generalise set_assert_mapper properly

d8cca45

volhovm force-pushed the volhovm/2231-ivc-selector-columns branch 2 times, most recently from 317305b to d8cca45 Compare May 20, 2024 13:39

volhovm mentioned this pull request May 20, 2024

IVC: Add array allocators/helpers: reduce stack usage #2247

Merged