diff --git a/crates/brainfuck_prover/src/brainfuck_air/mod.rs b/crates/brainfuck_prover/src/brainfuck_air/mod.rs index df61c64..12160fa 100644 --- a/crates/brainfuck_prover/src/brainfuck_air/mod.rs +++ b/crates/brainfuck_prover/src/brainfuck_air/mod.rs @@ -1,4 +1,5 @@ use crate::components::{ + instruction::table::InstructionElements, io::table::IoElements, memory::{ self, @@ -66,6 +67,7 @@ pub struct BrainfuckInteractionElements { pub input_lookup_elements: IoElements, pub output_lookup_elements: IoElements, pub memory_lookup_elements: MemoryElements, + pub instruction_lookup_elements: InstructionElements, } impl BrainfuckInteractionElements { @@ -76,6 +78,7 @@ impl BrainfuckInteractionElements { input_lookup_elements: IoElements::draw(channel), output_lookup_elements: IoElements::draw(channel), memory_lookup_elements: MemoryElements::draw(channel), + instruction_lookup_elements: InstructionElements::draw(channel), } } } diff --git a/crates/brainfuck_prover/src/components/instruction/table.rs b/crates/brainfuck_prover/src/components/instruction/table.rs index 0c483fd..c1c6df2 100644 --- a/crates/brainfuck_prover/src/components/instruction/table.rs +++ b/crates/brainfuck_prover/src/components/instruction/table.rs @@ -3,13 +3,17 @@ use brainfuck_vm::{ instruction::VALID_INSTRUCTIONS_BF, machine::ProgramMemory, registers::Registers, }; use num_traits::Zero; -use stwo_prover::core::{ - backend::{ - simd::{column::BaseColumn, m31::LOG_N_LANES}, - Column, +use stwo_prover::{ + constraint_framework::{logup::LookupElements, Relation, RelationEFTraitBound}, + core::{ + backend::{ + simd::{column::BaseColumn, m31::LOG_N_LANES}, + Column, + }, + channel::Channel, + fields::m31::BaseField, + poly::circle::{CanonicCoset, CircleEvaluation}, }, - fields::m31::BaseField, - poly::circle::{CanonicCoset, CircleEvaluation}, }; /// Represents the Instruction Table, which holds the required registers @@ -349,6 +353,59 @@ impl TraceColumn for InstructionColumn { } } +/// The number of random elements necessary for the Instruction lookup argument. +const INSTRUCTION_LOOKUP_ELEMENTS: usize = 3; + +/// The interaction elements are drawn for the extension column of the Memory component. +/// +/// The logUp protocol uses these elements to combine the values of the different +/// registers of the main trace to create a random linear combination +/// of them, and use it in the denominator of the fractions in the logUp protocol. +/// +/// There are 3 lookup elements in the Memory component, as only the 'real' registers +/// are used: `clk`, `mp` and `mv`. `d` is used to eventually nullify the numerator. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct InstructionElements(LookupElements); + +impl InstructionElements { + /// Provides dummy lookup elements. + pub fn dummy() -> Self { + Self(LookupElements::dummy()) + } + + /// Draw random elements from the Fiat-Shamir [`Channel`]. + /// + /// These elements are randomly secured, and will be use + /// to generate the interaction trace with the logUp protocol. + pub fn draw(channel: &mut impl Channel) -> Self { + Self(LookupElements::draw(channel)) + } +} + +impl> Relation for InstructionElements { + /// Combine multiple values from a basefield (e.g. [`BaseField`]) + /// and combine them to a value from an extension field (e.g. [`PackedSecureField`]) + /// + /// This is used when computing the interaction values from the main trace values. + fn combine(&self, values: &[F]) -> EF { + values + .iter() + .zip(self.0.alpha_powers) + .fold(EF::zero(), |acc, (value, power)| acc + EF::from(power) * value.clone()) - + self.0.z.into() + } + + /// Returns the name of the struct. + fn get_name(&self) -> &str { + stringify!(InstructionElements) + } + + /// Returns the number interaction elements. + fn get_size(&self) -> usize { + INSTRUCTION_LOOKUP_ELEMENTS + } +} + #[cfg(test)] mod tests { use super::*;