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

Logup for o1vm #2757

Open
wants to merge 32 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
0a07bba
Add flake.nix; flake.lock
Fizzixnerd Aug 28, 2024
1ec45d7
o1vm/pickles: first shot at logup
Fizzixnerd Nov 13, 2024
1348b91
o1vm/pickles: Format
Fizzixnerd Nov 15, 2024
047534f
WIP: remove lookup_env from proof inputs
marcbeunardeau88 Nov 20, 2024
91b3ba4
WIP WitnessColumns contains lookup related things
marcbeunardeau88 Nov 20, 2024
a8a411a
o1vm/pickles: compiles again
Fizzixnerd Nov 22, 2024
75c6c19
o1vm/pickles: do lookup constraints
Fizzixnerd Nov 26, 2024
1cb1e50
o1vm/pickles: remove dead code
Fizzixnerd Nov 26, 2024
09e9cbd
o1vm/pickles: cargo fmt
Fizzixnerd Nov 26, 2024
a24ef42
merge master
Fizzixnerd Nov 27, 2024
70392b7
o1vm/pickles: Cargo format
Fizzixnerd Nov 27, 2024
48ea3d3
o1vm/pickles: rename logup to lookup
Fizzixnerd Nov 27, 2024
d9b472b
o1vm/pickles: add joint_combiner to challenge
Fizzixnerd Nov 27, 2024
55a2441
o1vm/pickles: remove unneeded comment
Fizzixnerd Nov 27, 2024
67730a0
o1vm/pickles: format
Fizzixnerd Nov 27, 2024
4556330
o1vm/pickles: Fix compilation error
Fizzixnerd Dec 3, 2024
9f61816
WIP: ignore lookup in verifier for now
Fizzixnerd Dec 3, 2024
395e322
WIP: Format
Fizzixnerd Dec 3, 2024
21524a5
WIP: Fix index arithmetic in column_env.rs
Fizzixnerd Dec 3, 2024
87d4f9c
o1vm/main: move lookup cst into instruction loop
marcbeunardeau88 Dec 3, 2024
0b53415
question for misha
marcbeunardeau88 Dec 3, 2024
d0236c7
bug fix ?
marcbeunardeau88 Dec 3, 2024
68085b7
WIP: format
Fizzixnerd Dec 3, 2024
5cdbb94
o1vm/pickles: add initial multiplicities and fixed tables to witness
Fizzixnerd Dec 5, 2024
4fc47da
o1vm/pickles: implement add_lookup for mips witnesses
Fizzixnerd Dec 5, 2024
95563f7
o1vm/pickles: Format
Fizzixnerd Dec 5, 2024
d7b1fc9
Merge branch 'master' into fizzixnerd/logup-pickles
Fizzixnerd Jan 6, 2025
14dd237
Merge remote-tracking branch 'origin/master' into fizzixnerd/logup-pi…
Fizzixnerd Jan 6, 2025
b17b781
o1vm/pickles: get compiling again
Fizzixnerd Jan 6, 2025
2a4b4ac
o1vm/pickles/lookup: checkpoint for lookups
Fizzixnerd Jan 6, 2025
487da00
WIP
marcbeunardeau88 Jan 7, 2025
681455f
Merge Marc's work
Fizzixnerd Jan 13, 2025
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
9 changes: 5 additions & 4 deletions msm/src/logup.rs
Original file line number Diff line number Diff line change
Expand Up @@ -275,13 +275,13 @@ pub struct LogupWitness<F, ID: LookupTableID> {
#[derive(Debug, Clone)]
pub struct LookupProof<T, ID> {
/// The multiplicity polynomials
pub(crate) m: BTreeMap<ID, Vec<T>>,
pub m: BTreeMap<ID, Vec<T>>,
/// The polynomial keeping the sum of each row
pub(crate) h: BTreeMap<ID, Vec<T>>,
pub h: BTreeMap<ID, Vec<T>>,
/// The "running-sum" over the rows, coined `φ`
pub(crate) sum: T,
pub sum: T,
/// All fixed lookup tables values, indexed by their ID
pub(crate) fixed_tables: BTreeMap<ID, T>,
pub fixed_tables: BTreeMap<ID, T>,
Copy link
Contributor Author

Choose a reason for hiding this comment

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

This can be reverted.

}

/// Iterator implementation to abstract the content of the structure.
Expand Down Expand Up @@ -512,6 +512,7 @@ pub mod prover {
}

/// Represents the environment for the logup argument.
#[derive(Clone)]
Fizzixnerd marked this conversation as resolved.
Show resolved Hide resolved
pub struct Env<G: KimchiCurve, ID: LookupTableID> {
/// The polynomial of the multiplicities, indexed by the table ID.
pub lookup_counters_poly_d1: BTreeMap<ID, Vec<DensePolynomial<G::ScalarField>>>,
Expand Down
170 changes: 136 additions & 34 deletions o1vm/src/pickles/column_env.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,19 @@
use ark_ff::FftField;
use ark_poly::{Evaluations, Radix2EvaluationDomain};
use kimchi_msm::columns::Column;
use kimchi_msm::{columns::Column, logup::prover::QuotientPolynomialEnvironment, LookupTableID};
use poly_commitment::PolyComm;

use crate::{
interpreters::mips::{column::N_MIPS_SEL_COLS, witness::SCRATCH_SIZE},
pickles::proof::WitnessColumns,
};
use kimchi::circuits::{
berkeley_columns::{BerkeleyChallengeTerm, BerkeleyChallenges},
domains::{Domain, EvaluationDomains},
expr::{ColumnEnvironment as TColumnEnvironment, Constants},
use kimchi::{
circuits::{
berkeley_columns::{BerkeleyChallengeTerm, BerkeleyChallenges},
domains::{Domain, EvaluationDomains},
expr::{ColumnEnvironment as TColumnEnvironment, Constants},
},
curve::KimchiCurve,
};

type Evals<F> = Evaluations<F, Radix2EvaluationDomain<F>>;
Expand All @@ -18,10 +22,10 @@ type Evals<F> = Evaluations<F, Radix2EvaluationDomain<F>>;
/// required to evaluate an expression as a polynomial.
///
/// All are evaluations.
pub struct ColumnEnvironment<'a, F: FftField> {
pub struct ColumnEnvironment<'a, F: FftField, G: KimchiCurve, ID: LookupTableID> {
/// The witness column polynomials. Includes relation columns and dynamic
/// selector columns.
pub witness: &'a WitnessColumns<Evals<F>, [Evals<F>; N_MIPS_SEL_COLS]>,
pub witness: &'a WitnessColumns<Evals<F>, G, [Evals<F>; N_MIPS_SEL_COLS], ID>,
/// The value `prod_{j != 1} (1 - ω^j)`, used for efficiently
/// computing the evaluations of the unnormalized Lagrange basis
/// polynomials.
Expand All @@ -33,6 +37,9 @@ pub struct ColumnEnvironment<'a, F: FftField> {
pub challenges: BerkeleyChallenges<F>,
/// The domains used in the PLONK argument.
pub domain: EvaluationDomains<F>,

/// Lookup specific polynomials
pub lookup: Option<QuotientPolynomialEnvironment<'a, F, ID>>,
}

pub fn get_all_columns() -> Vec<Column> {
Expand All @@ -46,47 +53,142 @@ pub fn get_all_columns() -> Vec<Column> {
cols
}

impl<G> WitnessColumns<G, [G; N_MIPS_SEL_COLS]> {
pub fn get_column(&self, col: &Column) -> Option<&G> {
match *col {
Column::Relation(i) => {
if i < SCRATCH_SIZE {
let res = &self.scratch[i];
Some(res)
} else if i == SCRATCH_SIZE {
let res = &self.instruction_counter;
Some(res)
} else if i == SCRATCH_SIZE + 1 {
let res = &self.error;
Some(res)
} else {
panic!("We should not have that many relation columns");
}
pub fn get_column_comm<'a, G: KimchiCurve, ID: LookupTableID>(
Fizzixnerd marked this conversation as resolved.
Show resolved Hide resolved
env: &'a WitnessColumns<PolyComm<G>, G, [PolyComm<G>; N_MIPS_SEL_COLS], ID>,
col: &Column,
) -> Option<&'a PolyComm<G>> {
match *col {
Column::Relation(i) => {
if i < SCRATCH_SIZE {
let res = &env.scratch[i];
Some(res)
} else if i == SCRATCH_SIZE {
let res = &env.instruction_counter;
Some(res)
} else if i == SCRATCH_SIZE + 1 {
let res = &env.error;
Some(res)
} else {
panic!("We should not have that many relation columns");
}
Column::DynamicSelector(i) => {
assert!(
i < N_MIPS_SEL_COLS,
"We do not have that many dynamic selector columns"
);
let res = &self.selector[i];
}
Column::DynamicSelector(i) => {
assert!(
i < N_MIPS_SEL_COLS,
"We do not have that many dynamic selector columns"
);
let res = &env.selector[i];
Some(res)
}
Column::LookupPartialSum((table_id, i)) => {
if let Some(ref lookup) = env.lookup_env {
let table_id = ID::from_u32(table_id);
Some(&lookup.lookup_terms_comms_d1[&table_id][i])
} else {
panic!("No lookup provided")
}
}
Column::LookupAggregation => {
if let Some(ref lookup) = env.lookup_env {
Some(&lookup.lookup_aggregation_comm_d1)
} else {
panic!("No lookup provided")
}
}
Column::LookupMultiplicity((table_id, i)) => {
if let Some(ref lookup) = env.lookup_env {
Some(&lookup.lookup_counters_comm_d1[&ID::from_u32(table_id)][i])
} else {
panic!("No lookup provided")
}
}
Column::LookupFixedTable(table_id) => {
if let Some(ref lookup) = env.lookup_env {
Some(&lookup.fixed_lookup_tables_comms_d1[&ID::from_u32(table_id)])
} else {
panic!("No lookup provided")
}
}
_ => {
panic!("We should not have any other type of columns")
}
}
}

pub fn get_column_eval<'a, G: KimchiCurve, ID: LookupTableID>(
Fizzixnerd marked this conversation as resolved.
Show resolved Hide resolved
env: &'a WitnessColumns<Evals<G::ScalarField>, G, [Evals<G::ScalarField>; N_MIPS_SEL_COLS], ID>,
col: &Column,
) -> Option<&'a Evals<G::ScalarField>> {
match *col {
Column::Relation(i) => {
if i < SCRATCH_SIZE {
let res = &env.scratch[i];
Some(res)
} else if i == SCRATCH_SIZE {
let res = &env.instruction_counter;
Some(res)
} else if i == SCRATCH_SIZE + 1 {
let res = &env.error;
Some(res)
} else {
panic!("We should not have that many relation columns");
}
}
Column::DynamicSelector(i) => {
assert!(
i < N_MIPS_SEL_COLS,
"We do not have that many dynamic selector columns"
);
let res = &env.selector[i];
Some(res)
}
Column::LookupPartialSum((table_id, i)) => {
if let Some(ref lookup) = env.lookup_env {
let table_id = ID::from_u32(table_id);
Some(&lookup.lookup_terms_evals_d8[&table_id][i])
} else {
panic!("No lookup provided")
}
}
Column::LookupAggregation => {
if let Some(ref lookup) = env.lookup_env {
Some(&lookup.lookup_aggregation_evals_d8)
} else {
panic!("No lookup provided")
}
_ => {
panic!("We should not have any other type of columns")
}
Column::LookupMultiplicity((table_id, i)) => {
if let Some(ref lookup) = env.lookup_env {
Some(&lookup.lookup_counters_evals_d8[&ID::from_u32(table_id)][i])
} else {
panic!("No lookup provided")
}
}
Column::LookupFixedTable(table_id) => {
if let Some(ref lookup) = env.lookup_env {
Some(&lookup.fixed_lookup_tables_evals_d8[&ID::from_u32(table_id)])
} else {
panic!("No lookup provided")
}
}
_ => {
panic!("We should not have any other type of columns")
}
}
}

impl<'a, F: FftField> TColumnEnvironment<'a, F, BerkeleyChallengeTerm, BerkeleyChallenges<F>>
for ColumnEnvironment<'a, F>
impl<'a, F: FftField, G: KimchiCurve, ID: LookupTableID>
TColumnEnvironment<'a, F, BerkeleyChallengeTerm, BerkeleyChallenges<F>>
for ColumnEnvironment<'a, F, G, ID>
where
G: KimchiCurve<ScalarField = F>,
{
// FIXME: do we change to the MIPS column type?
// We do not want to keep kimchi_msm/generic prover
type Column = Column;

fn get_column(&self, col: &Self::Column) -> Option<&'a Evals<F>> {
self.witness.get_column(col)
get_column_eval(self.witness, col)
}

fn get_domain(&self, d: Domain) -> Radix2EvaluationDomain<F> {
Expand Down
7 changes: 6 additions & 1 deletion o1vm/src/pickles/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ use o1vm::{
witness::{self as mips_witness},
Instruction,
},
lookups::LookupTableIDs,
pickles::{proof::ProofInputs, prover, verifier},
preimage_oracle::PreImageOracle,
};
Expand All @@ -28,6 +29,8 @@ use mina_curves::pasta::{Fp, Vesta};

pub const DOMAIN_SIZE: usize = 1 << 15;

type ID = LookupTableIDs;

pub fn main() -> ExitCode {
let cli = cannon_cli::main_cli();

Expand Down Expand Up @@ -95,7 +98,7 @@ pub fn main() -> ExitCode {
constraints
};

let mut curr_proof_inputs: ProofInputs<Vesta> = ProofInputs::new(DOMAIN_SIZE);
let mut curr_proof_inputs: ProofInputs<Vesta, ID> = ProofInputs::new(DOMAIN_SIZE);
while !mips_wit_env.halt {
let _instr: Instruction = mips_wit_env.step(&configuration, &meta, &start);
for (scratch, scratch_chunk) in mips_wit_env
Expand Down Expand Up @@ -126,6 +129,7 @@ pub fn main() -> ExitCode {
DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
_,
ID,
>(domain_fp, &srs, curr_proof_inputs, &constraints, &mut rng)
.unwrap();
// FIXME: check that the proof is correct. This is for testing purposes.
Expand All @@ -140,6 +144,7 @@ pub fn main() -> ExitCode {
Vesta,
DefaultFqSponge<VestaParameters, PlonkSpongeConstantsKimchi>,
DefaultFrSponge<Fp, PlonkSpongeConstantsKimchi>,
ID,
>(domain_fp, &srs, &constraints, &proof);
debug!(
"Verification done in {elapsed} μs",
Expand Down
36 changes: 25 additions & 11 deletions o1vm/src/pickles/proof.rs
Original file line number Diff line number Diff line change
@@ -1,39 +1,53 @@
use std::collections::BTreeMap;

use kimchi::{curve::KimchiCurve, proof::PointEvaluations};
use kimchi_msm::{
logup::{prover::Env as LookupEnv, LookupProof},
LogupWitness, LookupTableID,
};
use poly_commitment::{ipa::OpeningProof, PolyComm};

use crate::interpreters::mips::{column::N_MIPS_SEL_COLS, witness::SCRATCH_SIZE};

pub struct WitnessColumns<G, S> {
pub scratch: [G; SCRATCH_SIZE],
pub instruction_counter: G,
pub error: G,
#[derive(Clone)]
Copy link
Contributor Author

Choose a reason for hiding this comment

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

Needed to do some evil clones, will likely need optimizing

Copy link
Contributor

Choose a reason for hiding this comment

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

Indeed, let's keep it for a follow-up

pub struct WitnessColumns<F, G: KimchiCurve, S, ID: LookupTableID> {
pub scratch: [F; crate::interpreters::mips::witness::SCRATCH_SIZE],
pub instruction_counter: F,
pub error: F,
pub selector: S,
pub lookup_env: Option<LookupEnv<G, ID>>,
}

pub struct ProofInputs<G: KimchiCurve> {
pub evaluations: WitnessColumns<Vec<G::ScalarField>, Vec<G::ScalarField>>,
pub struct ProofInputs<G: KimchiCurve, ID: LookupTableID> {
pub evaluations: WitnessColumns<Vec<G::ScalarField>, G, Vec<G::ScalarField>, ID>,
pub logups: BTreeMap<ID, LogupWitness<G::ScalarField, ID>>,
}

impl<G: KimchiCurve> ProofInputs<G> {
impl<G: KimchiCurve, ID: LookupTableID> ProofInputs<G, ID> {
pub fn new(domain_size: usize) -> Self {
ProofInputs {
evaluations: WitnessColumns {
scratch: std::array::from_fn(|_| Vec::with_capacity(domain_size)),
instruction_counter: Vec::with_capacity(domain_size),
error: Vec::with_capacity(domain_size),
selector: Vec::with_capacity(domain_size),
lookup_env: None,
},
logups: BTreeMap::new(),
}
}
}

// FIXME: should we blind the commitment?
pub struct Proof<G: KimchiCurve> {
pub commitments: WitnessColumns<PolyComm<G>, [PolyComm<G>; N_MIPS_SEL_COLS]>,
pub zeta_evaluations: WitnessColumns<G::ScalarField, [G::ScalarField; N_MIPS_SEL_COLS]>,
pub zeta_omega_evaluations: WitnessColumns<G::ScalarField, [G::ScalarField; N_MIPS_SEL_COLS]>,
pub struct Proof<G: KimchiCurve, ID: LookupTableID> {
pub commitments: WitnessColumns<PolyComm<G>, G, [PolyComm<G>; N_MIPS_SEL_COLS], ID>,
pub zeta_evaluations: WitnessColumns<G::ScalarField, G, [G::ScalarField; N_MIPS_SEL_COLS], ID>,
pub zeta_omega_evaluations:
WitnessColumns<G::ScalarField, G, [G::ScalarField; N_MIPS_SEL_COLS], ID>,
pub quotient_commitment: PolyComm<G>,
pub quotient_evaluations: PointEvaluations<Vec<G::ScalarField>>,
pub logup_commitments: Option<LookupProof<PolyComm<G>, ID>>,
pub logup_evaluations: Option<LookupProof<PointEvaluations<G::ScalarField>, ID>>,
/// IPA opening proof
pub opening_proof: OpeningProof<G>,
}
Loading
Loading