-
Notifications
You must be signed in to change notification settings - Fork 95
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
o1vm/mips: use batch_inversion for the witness generation #2813
Changes from all commits
7f2d2fe
ff73fa2
52d5cd9
f108bf2
8f37429
acc0253
da3f830
dcf661c
ac0380b
a934839
c65b14a
3071eab
f4b52a7
be87dce
a11a350
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -50,10 +50,17 @@ pub const NUM_INSTRUCTION_LOOKUP_TERMS: usize = 5; | |
pub const NUM_LOOKUP_TERMS: usize = | ||
NUM_GLOBAL_LOOKUP_TERMS + NUM_DECODING_LOOKUP_TERMS + NUM_INSTRUCTION_LOOKUP_TERMS; | ||
// TODO: Delete and use a vector instead | ||
// FIXME: since the introduction of the scratch size inverse, the value below | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is fixed in #2815. |
||
// can be decreased. It implies to change the offsets defined in [column]. At | ||
// the moment, it incurs an overhead we could avoid as some columns are zeroes. | ||
// MIPS + hash_counter + byte_counter + eof + num_bytes_read + chunk + bytes | ||
// + length + has_n_bytes + chunk_bytes + preimage | ||
pub const SCRATCH_SIZE: usize = 98; | ||
|
||
/// Number of columns used by the MIPS interpreter to keep values to be | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. To verify it was the minimal value, I did try to use 11, and it failed. |
||
/// inverted. | ||
pub const SCRATCH_SIZE_INVERSE: usize = 12; | ||
|
||
#[derive(Clone, Default)] | ||
pub struct SyscallEnv { | ||
pub last_hint: Option<Vec<u8>>, | ||
|
@@ -81,7 +88,9 @@ pub struct Env<Fp, PreImageOracle: PreImageOracleT> { | |
pub registers: Registers<u32>, | ||
pub registers_write_index: Registers<u64>, | ||
pub scratch_state_idx: usize, | ||
pub scratch_state_idx_inverse: usize, | ||
pub scratch_state: [Fp; SCRATCH_SIZE], | ||
pub scratch_state_inverse: [Fp; SCRATCH_SIZE_INVERSE], | ||
pub halt: bool, | ||
pub syscall_env: SyscallEnv, | ||
pub selector: usize, | ||
|
@@ -106,6 +115,12 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreI | |
Column::ScratchState(scratch_idx) | ||
} | ||
|
||
fn alloc_scratch_inverse(&mut self) -> Self::Position { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It seems like this function for the mips witness is the same as the one in the mips constraints. I wonder if it could be generically defined in the interpreter itself, but probably not directly given that it uses the fact that it accesses a There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I do think it is fine at the moment. Agree it is a bit "annoying"/"ugly" to have duplicated code. But lgtm for the moment. |
||
let scratch_idx = self.scratch_state_idx_inverse; | ||
self.scratch_state_idx_inverse += 1; | ||
Column::ScratchStateInverse(scratch_idx) | ||
} | ||
|
||
type Variable = u64; | ||
|
||
fn variable(&self, _column: Self::Position) -> Self::Variable { | ||
|
@@ -314,17 +329,17 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreI | |
|
||
fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable { | ||
// write the result | ||
let pos = self.alloc_scratch(); | ||
let res = if *x == 0 { 1 } else { 0 }; | ||
self.write_column(pos, res); | ||
let res = { | ||
let pos = self.alloc_scratch(); | ||
unsafe { self.test_zero(x, pos) } | ||
}; | ||
// write the non deterministic advice inv_or_zero | ||
let pos = self.alloc_scratch(); | ||
let inv_or_zero = if *x == 0 { | ||
Fp::zero() | ||
let pos = self.alloc_scratch_inverse(); | ||
if *x == 0 { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I am not sure why there's this There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No reason. Seems to be an ugly code 😅. For a follow-up. |
||
self.write_field_column(pos, Fp::zero()); | ||
} else { | ||
Fp::inverse(&Fp::from(*x)).unwrap() | ||
self.write_field_column(pos, Fp::from(*x)); | ||
}; | ||
self.write_field_column(pos, inv_or_zero); | ||
// return the result | ||
res | ||
} | ||
|
@@ -339,15 +354,11 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreI | |
self.write_column(pos, is_zero); | ||
is_zero | ||
}; | ||
let _to_zero_test_inv_or_zero = { | ||
let pos = self.alloc_scratch(); | ||
let inv_or_zero = if to_zero_test == Fp::zero() { | ||
Fp::zero() | ||
} else { | ||
Fp::inverse(&to_zero_test).unwrap() | ||
}; | ||
self.write_field_column(pos, inv_or_zero); | ||
1 // Placeholder value | ||
let pos = self.alloc_scratch_inverse(); | ||
dannywillems marked this conversation as resolved.
Show resolved
Hide resolved
|
||
if to_zero_test == Fp::zero() { | ||
self.write_field_column(pos, Fp::zero()); | ||
} else { | ||
self.write_field_column(pos, to_zero_test); | ||
}; | ||
res | ||
} | ||
|
@@ -878,7 +889,9 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> { | |
registers: initial_registers.clone(), | ||
registers_write_index: Registers::default(), | ||
scratch_state_idx: 0, | ||
scratch_state_idx_inverse: 0, | ||
scratch_state: fresh_scratch_state(), | ||
scratch_state_inverse: fresh_scratch_state(), | ||
halt: state.exited, | ||
syscall_env, | ||
selector, | ||
|
@@ -897,13 +910,19 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> { | |
self.selector = N_MIPS_SEL_COLS; | ||
} | ||
|
||
pub fn reset_scratch_state_inverse(&mut self) { | ||
self.scratch_state_idx_inverse = 0; | ||
self.scratch_state_inverse = fresh_scratch_state(); | ||
} | ||
|
||
pub fn write_column(&mut self, column: Column, value: u64) { | ||
self.write_field_column(column, value.into()) | ||
} | ||
|
||
pub fn write_field_column(&mut self, column: Column, value: Fp) { | ||
match column { | ||
Column::ScratchState(idx) => self.scratch_state[idx] = value, | ||
Column::ScratchStateInverse(idx) => self.scratch_state_inverse[idx] = value, | ||
Column::InstructionCounter => panic!("Cannot overwrite the column {:?}", column), | ||
Column::Selector(s) => self.selector = s, | ||
} | ||
|
@@ -1138,6 +1157,7 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle> { | |
start: &Start, | ||
) -> Instruction { | ||
self.reset_scratch_state(); | ||
self.reset_scratch_state_inverse(); | ||
let (opcode, _instruction) = self.decode_instruction(); | ||
|
||
self.pp_info(&config.info_at, metadata, start); | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -3,7 +3,10 @@ use ark_poly::{Evaluations, Radix2EvaluationDomain}; | |
use kimchi_msm::columns::Column; | ||
|
||
use crate::{ | ||
interpreters::mips::{column::N_MIPS_SEL_COLS, witness::SCRATCH_SIZE}, | ||
interpreters::mips::{ | ||
column::N_MIPS_SEL_COLS, | ||
witness::{SCRATCH_SIZE, SCRATCH_SIZE_INVERSE}, | ||
}, | ||
pickles::proof::WitnessColumns, | ||
}; | ||
use kimchi::circuits::{ | ||
|
@@ -36,8 +39,9 @@ pub struct ColumnEnvironment<'a, F: FftField> { | |
} | ||
|
||
pub fn get_all_columns() -> Vec<Column> { | ||
let mut cols = Vec::<Column>::with_capacity(SCRATCH_SIZE + 2 + N_MIPS_SEL_COLS); | ||
for i in 0..SCRATCH_SIZE + 2 { | ||
let mut cols = | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Perhaps use There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No, you are right about using |
||
Vec::<Column>::with_capacity(SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2 + N_MIPS_SEL_COLS); | ||
for i in 0..SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2 { | ||
cols.push(Column::Relation(i)); | ||
} | ||
for i in 0..N_MIPS_SEL_COLS { | ||
|
@@ -53,26 +57,34 @@ impl<G> WitnessColumns<G, [G; N_MIPS_SEL_COLS]> { | |
if i < SCRATCH_SIZE { | ||
let res = &self.scratch[i]; | ||
Some(res) | ||
} else if i == SCRATCH_SIZE { | ||
} else if i < SCRATCH_SIZE + SCRATCH_SIZE_INVERSE { | ||
let res = &self.scratch_inverse[i - SCRATCH_SIZE]; | ||
Some(res) | ||
} else if i == SCRATCH_SIZE + SCRATCH_SIZE_INVERSE { | ||
let res = &self.instruction_counter; | ||
Some(res) | ||
} else if i == SCRATCH_SIZE + 1 { | ||
} else if i == SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 1 { | ||
let res = &self.error; | ||
Some(res) | ||
} else { | ||
panic!("We should not have that many relation columns"); | ||
panic!("We should not have that many relation columns. We have {} columns and index {} was given", SCRATCH_SIZE + SCRATCH_SIZE_INVERSE + 2, i); | ||
} | ||
} | ||
Column::DynamicSelector(i) => { | ||
assert!( | ||
i < N_MIPS_SEL_COLS, | ||
"We do not have that many dynamic selector columns" | ||
"We do not have that many dynamic selector columns. We have {} columns and index {} was given", | ||
N_MIPS_SEL_COLS, | ||
i | ||
); | ||
let res = &self.selector[i]; | ||
Some(res) | ||
} | ||
_ => { | ||
panic!("We should not have any other type of columns") | ||
panic!( | ||
"We should not have any other type of columns. The column {:?} was given", | ||
col | ||
); | ||
} | ||
} | ||
} | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In a future PR, as suggested by @mrmr1993, we can try to use BigInt/BigUInt directly to avoid computation in Montgomery representation. I do not know if it would make it better.