Skip to content

Commit

Permalink
doc: improve head doc and comments on interaction trace eval
Browse files Browse the repository at this point in the history
  • Loading branch information
zmalatrax committed Dec 18, 2024
1 parent 1781d0c commit 8d03db0
Showing 1 changed file with 18 additions and 10 deletions.
28 changes: 18 additions & 10 deletions crates/brainfuck_prover/src/components/instruction/table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -421,6 +421,17 @@ impl<F: Clone, EF: RelationEFTraitBound<F>> Relation<F, EF> for InstructionEleme
/// Only the 'real' rows are impacting the logUp sum.
/// Dummy rows are padded rows.
///
/// Here, the logUp has two extension columns:
/// - One to link the Instruction component with the Processor component.
/// - one to link the Instruction component with the Program component.
///
/// - They use the main Instruction trace as two disjoint subsets:
/// The subset for the Program is constituted of rows whose `ip` register value
/// remains the same with the previous `ip` register value. (It includes the first entry).
///
/// The subset for the Processor is constituted of rows whose `ip` register value
/// has changed compared to the previous `ip` value.
///
/// # Returns
/// - Interaction trace evaluation, to be committed.
/// - Interaction claim: the total sum from the logUp protocol,
Expand Down Expand Up @@ -459,24 +470,22 @@ pub fn interaction_trace_evaluation(
let ci_col = &main_trace_eval[InstructionColumn::Ci.index()].data;
let ni_col = &main_trace_eval[InstructionColumn::Ni.index()].data;

// The very first row (index 0, entry 0) is always part of the program, thus not the execution
// trace.
// We work on the second entry of the list (next_...) as the current row,
// and use the first entry of the list as the previous one.
// col_gen.write_frac(0, PackedSecureField::zero(), lookup_elements.combine([ip]));
// The very first row (index 0) is considered part of the Program subset,
// thus not part of the Processor subset.
col_gen.write_frac(
0,
PackedSecureField::zero(),
lookup_elements.combine(&[ip_col[0], ci_col[0], ni_col[0]]),
);

// Populates the first logUp column for the Processor permutation argument.
let mut prev_ip = ip_col[0];
for vec_row in 1..1 << (log_size - LOG_N_LANES) {
let ip = ip_col[vec_row];
let ci = ci_col[vec_row];
let ni = ni_col[vec_row];

// Set the fraction numerator to 0 if a padding row (ci = 0) or ip changes,
// Set the multiplicity to 0 if it's a padding row (ci = 0) or if ip has changed,
// otherwise set it to -1.
let num = ci_col.get(vec_row).map_or_else(
|| {
Expand All @@ -490,7 +499,6 @@ pub fn interaction_trace_evaluation(
}
},
);
// Only the common registers with the processor table are part of the extension column.
let denom: PackedSecureField = lookup_elements.combine(&[ip, ci, ni]);
col_gen.write_frac(vec_row, num, denom);

Expand All @@ -501,10 +509,10 @@ pub fn interaction_trace_evaluation(

// Second Column - Instruction & Program
// We want to prove that a subset of the rows of the Instruction table (which is disjoint from
// the previous subset of rows) is a set equality of the Program.
// the previous subset of rows) is an ordered set equality of the Program.
let mut col_gen = logup_gen.new_col();

// The first entry (row 0, entry 0) is always part of the program
// Populates the second logUp column for the Program evaluation argument.
col_gen.write_frac(
0,
-PackedSecureField::one(),
Expand All @@ -517,7 +525,7 @@ pub fn interaction_trace_evaluation(
let ci = ci_col[vec_row];
let ni = ni_col[vec_row];

// Set the fraction numerator to 0 if a padding row (ci = 0) or ip remains the same,
// Set the multiplicity to 0 if it's a padding row (ci = 0) or if ip remains the same,
// otherwise set it to -1.
let num = ci_col.get(vec_row).map_or_else(
|| {
Expand Down

0 comments on commit 8d03db0

Please sign in to comment.