Skip to content

Commit

Permalink
feat: add instruction lookup elements
Browse files Browse the repository at this point in the history
  • Loading branch information
zmalatrax committed Dec 11, 2024
1 parent 50ee67c commit 7e9cc5c
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 6 deletions.
3 changes: 3 additions & 0 deletions crates/brainfuck_prover/src/brainfuck_air/mod.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
use crate::components::{
instruction::table::InstructionElements,
io::table::IoElements,
memory::{
self,
Expand Down Expand Up @@ -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 {
Expand All @@ -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),
}
}
}
Expand Down
69 changes: 63 additions & 6 deletions crates/brainfuck_prover/src/components/instruction/table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<INSTRUCTION_LOOKUP_ELEMENTS>);

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<F: Clone, EF: RelationEFTraitBound<F>> Relation<F, EF> 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::*;
Expand Down

0 comments on commit 7e9cc5c

Please sign in to comment.