Skip to content

Commit

Permalink
refactor: refactor InteractionClaim to a common struct for all compon…
Browse files Browse the repository at this point in the history
…ents
  • Loading branch information
zmalatrax committed Jan 9, 2025
1 parent 36540e5 commit 52ca574
Show file tree
Hide file tree
Showing 12 changed files with 37 additions and 143 deletions.
10 changes: 5 additions & 5 deletions crates/brainfuck_prover/src/brainfuck_air/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use crate::components::{
component::{MemoryComponent, MemoryEval},
table::{MemoryElements, MemoryTable},
},
InstructionClaim, IoClaim, MemoryClaim,
InstructionClaim, InteractionClaim, IoClaim, MemoryClaim,
};
use brainfuck_vm::machine::Machine;
use stwo_prover::{
Expand Down Expand Up @@ -109,10 +109,10 @@ impl BrainfuckInteractionElements {
///
/// Mainly the claims on global relations (lookup, permutation, evaluation).
pub struct BrainfuckInteractionClaim {
input: io::component::InteractionClaim,
output: io::component::InteractionClaim,
memory: memory::component::InteractionClaim,
instruction: instruction::component::InteractionClaim,
input: InteractionClaim,
output: InteractionClaim,
memory: InteractionClaim,
instruction: InteractionClaim,
}

impl BrainfuckInteractionClaim {
Expand Down
29 changes: 1 addition & 28 deletions crates/brainfuck_prover/src/components/instruction/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,7 @@ use stwo_prover::{
preprocessed_columns::PreprocessedColumn, EvalAtRow, FrameworkComponent, FrameworkEval,
RelationEntry,
},
core::{
channel::Channel,
fields::{m31::BaseField, qm31::SecureField},
},
core::fields::m31::BaseField,
};

/// Implementation of `Component` and `ComponentProver`
Expand Down Expand Up @@ -127,30 +124,6 @@ impl FrameworkEval for InstructionEval {
}
}

// TODO: Eventually refactor all InteractionClaim into a common struct at the components mod root.
/// The claim of the interaction phase 2 (with the logUp protocol).
///
/// The total sum is the computed sum of the logUp extension column,
/// including the padded rows.
/// It allows proving two things on two disjoint subset of the Instruction main trace (whose union
/// constitutes the Instruction):
/// - One is the permutation of the Processor trace
/// - The other is a subset of the Program trace (order preserved).
/// of the Processor trace (which is the execution trace provided by the `brainfuck_vm`).
#[derive(Debug, Eq, PartialEq)]
pub struct InteractionClaim {
/// The computed sum of the logUp extension column, including padded rows.
pub claimed_sum: SecureField,
}

impl InteractionClaim {
/// Mix the sums from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
}

#[cfg(test)]
mod tests {
use brainfuck_vm::{compiler::Compiler, test_helper::create_test_machine};
Expand Down
4 changes: 1 addition & 3 deletions crates/brainfuck_prover/src/components/instruction/table.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use crate::components::{InstructionClaim, TraceColumn, TraceError, TraceEval};
use crate::components::{InstructionClaim, InteractionClaim, TraceColumn, TraceError, TraceEval};
use brainfuck_vm::{machine::ProgramMemory, registers::Registers};
use num_traits::{One, Zero};
use stwo_prover::{
Expand All @@ -17,8 +17,6 @@ use stwo_prover::{
},
};

use super::component::InteractionClaim;

/// Represents the Instruction Table, which holds the required registers
/// for the Instruction component.
///
Expand Down
26 changes: 1 addition & 25 deletions crates/brainfuck_prover/src/components/io/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,7 @@ use brainfuck_vm::instruction::InstructionType;
use num_traits::One;
use stwo_prover::{
constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval, RelationEntry},
core::{
channel::Channel,
fields::{m31::BaseField, qm31::SecureField},
},
core::fields::m31::BaseField,
};

use crate::components::IoClaim;
Expand Down Expand Up @@ -99,27 +96,6 @@ impl<const N: u32> FrameworkEval for IoEval<N> {
}
}

/// The claim of the interaction phase 2 (with the logUp protocol).
///
/// The total sum is the computed sum of the logUp extension column,
/// including the padded rows.
/// It allows proving that the I/O main trace is a sublist
/// of the Processor trace (which is the execution trace provided by the `brainfuck_vm`):
/// all input and output values are the same as the one from the execution, in the same order.
#[derive(Debug, Eq, PartialEq)]
pub struct InteractionClaim {
/// The computed sum of the logUp extension column, including padded rows.
pub claimed_sum: SecureField,
}

impl InteractionClaim {
/// Mix the sums from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
}

#[cfg(test)]
mod test {
use brainfuck_vm::{compiler::Compiler, test_helper::create_test_machine};
Expand Down
4 changes: 1 addition & 3 deletions crates/brainfuck_prover/src/components/io/table.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
use crate::components::{
io::component::InteractionClaim, IoClaim, TraceColumn, TraceError, TraceEval,
};
use crate::components::{InteractionClaim, IoClaim, TraceColumn, TraceError, TraceEval};
use brainfuck_vm::{instruction::InstructionType, registers::Registers};
use num_traits::{One, Zero};
use stwo_prover::{
Expand Down
25 changes: 1 addition & 24 deletions crates/brainfuck_prover/src/components/memory/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,7 @@ use stwo_prover::{
preprocessed_columns::PreprocessedColumn, EvalAtRow, FrameworkComponent, FrameworkEval,
RelationEntry,
},
core::{
channel::Channel,
fields::{m31::BaseField, qm31::SecureField},
},
core::fields::m31::BaseField,
};

/// Implementation of `Component` and `ComponentProver`
Expand Down Expand Up @@ -124,26 +121,6 @@ impl FrameworkEval for MemoryEval {
}
}

/// The claim of the interaction phase 2 (with the logUp protocol).
///
/// The total sum is the computed sum of the logUp extension column,
/// including the padded rows.
/// It allows proving that the Memory main trace is a permutation
/// of the Processor trace (which is the execution trace provided by the `brainfuck_vm`).
#[derive(Debug, Eq, PartialEq)]
pub struct InteractionClaim {
/// The computed sum of the logUp extension column, including padded rows.
pub claimed_sum: SecureField,
}

impl InteractionClaim {
/// Mix the sums from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
}

#[cfg(test)]
mod tests {
use crate::components::memory::{
Expand Down
3 changes: 1 addition & 2 deletions crates/brainfuck_prover/src/components/memory/table.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
use super::component::InteractionClaim;
use crate::components::{MemoryClaim, TraceColumn, TraceError, TraceEval};
use crate::components::{InteractionClaim, MemoryClaim, TraceColumn, TraceError, TraceEval};
use brainfuck_vm::registers::Registers;
use num_traits::One;
use stwo_prover::{
Expand Down
23 changes: 22 additions & 1 deletion crates/brainfuck_prover/src/components/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use program::table::ProgramColumn;
use stwo_prover::core::{
backend::simd::SimdBackend,
channel::Channel,
fields::{m31::BaseField, secure_column::SECURE_EXTENSION_DEGREE},
fields::{m31::BaseField, qm31::SecureField, secure_column::SECURE_EXTENSION_DEGREE},
pcs::TreeVec,
poly::{circle::CircleEvaluation, BitReversedOrder},
ColumnVec,
Expand Down Expand Up @@ -45,6 +45,27 @@ pub enum TraceError {
EmptyTrace,
}

/// The claim of the interaction phase 2 (with the logUp protocol).
///
/// The claimed sum is the total sum, which is the computed sum of the logUp extension column,
/// including the padding rows.
/// It allows proving that the main trace of a component is either a permutation, or a sublist of
/// another.
#[derive(Debug, Eq, PartialEq)]
pub struct InteractionClaim {
/// The computed sum of the logUp extension column, including padding rows (which are actually
/// set to a multiplicity of 0).
pub claimed_sum: SecureField,
}

impl InteractionClaim {
/// Mix the sum from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
}

/// Represents a claim associated with a specific trace in the Brainfuck STARK proving system.
#[derive(Debug, Eq, PartialEq)]
pub struct Claim<T: TraceColumn> {
Expand Down
27 changes: 1 addition & 26 deletions crates/brainfuck_prover/src/components/processor/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,7 @@ use crate::components::{
instruction::table::InstructionElements, io::table::IoElements, memory::table::MemoryElements,
ProcessorClaim,
};
use stwo_prover::{
constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval},
core::{channel::Channel, fields::qm31::SecureField},
};
use stwo_prover::constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval};

/// Implementation of `Component` and `ComponentProver`
/// for the `SimdBackend` from the constraint framework provided by Stwo
Expand Down Expand Up @@ -71,25 +68,3 @@ impl FrameworkEval for ProcessorEval {
todo!()
}
}

/// The claim of the interaction phase 2 (with the logUp protocol).
///
/// The total sum is the computed sum of the logUp extension column,
/// including the padded rows.
/// It allows proving that the Processor main trace is:
/// - A permutation of the Memory trace.
/// - A permutation of a subset of the Instruction trace.
/// - That the I/O values are the ones in the I/O components, in the same order.
#[derive(Debug, Eq, PartialEq)]
pub struct InteractionClaim {
/// The computed sum of the logUp extension column, including padded rows.
pub claimed_sum: SecureField,
}

impl InteractionClaim {
/// Mix the sums from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
}
3 changes: 1 addition & 2 deletions crates/brainfuck_prover/src/components/processor/table.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
use super::component::InteractionClaim;
use crate::components::{
instruction::table::InstructionElements, io::table::IoElements, memory::table::MemoryElements,
ProcessorClaim, TraceColumn, TraceError, TraceEval,
InteractionClaim, ProcessorClaim, TraceColumn, TraceError, TraceEval,
};
use brainfuck_vm::registers::Registers;
use num_traits::{One, Zero};
Expand Down
23 changes: 1 addition & 22 deletions crates/brainfuck_prover/src/components/program/component.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
use super::table::ProgramElements;
use crate::components::ProgramClaim;
use stwo_prover::{
constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval},
core::{channel::Channel, fields::qm31::SecureField},
};
use stwo_prover::constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval};

/// Implementation of `Component` and `ComponentProver`
/// for the `SimdBackend` from the constraint framework provided by Stwo
Expand Down Expand Up @@ -54,21 +51,3 @@ impl FrameworkEval for ProgramEval {
todo!()
}
}

/// The claim of the interaction phase 2 (with the logUp protocol).
///
/// The total sum is the computed sum of the logUp extension column,
/// including the padded rows.
#[derive(Debug, Eq, PartialEq)]
pub struct InteractionClaim {
/// The computed sum of the logUp extension column, including padded rows.
pub claimed_sum: SecureField,
}

impl InteractionClaim {
/// Mix the sums from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
}
3 changes: 1 addition & 2 deletions crates/brainfuck_prover/src/components/program/table.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
use super::component::InteractionClaim;
use crate::components::{ProgramClaim, TraceColumn, TraceError, TraceEval};
use crate::components::{InteractionClaim, ProgramClaim, TraceColumn, TraceError, TraceEval};
use brainfuck_vm::{machine::ProgramMemory, registers::Registers};
use num_traits::{One, Zero};
use stwo_prover::{
Expand Down

0 comments on commit 52ca574

Please sign in to comment.