Skip to content

Commit

Permalink
feat: add memory constraints for new MemoryTable
Browse files Browse the repository at this point in the history
  • Loading branch information
zmalatrax committed Dec 2, 2024
1 parent 7c07c4c commit 33ce682
Show file tree
Hide file tree
Showing 2 changed files with 53 additions and 21 deletions.
28 changes: 25 additions & 3 deletions crates/brainfuck_prover/src/brainfuck_air/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -255,9 +255,10 @@ pub fn verify_brainfuck(

let interaction_elements = BrainfuckInteractionElements::draw(channel);
// Check that the lookup sum is valid, otherwise throw
if !lookup_sum_valid(&claim, &interaction_elements, &interaction_claim) {
return Err(VerificationError::InvalidLookup("Invalid LogUp sum".to_string()));
};
// TODO: Implement lookup_sum_valid once the processor component has been implemented.
// if !lookup_sum_valid(&claim, &interaction_elements, &interaction_claim) {
// return Err(VerificationError::InvalidLookup("Invalid LogUp sum".to_string()));
// };
interaction_claim.mix_into(channel);
commitment_scheme_verifier.commit(
proof.commitments[INTERACTION_TRACE_IDX],
Expand All @@ -275,3 +276,24 @@ pub fn verify_brainfuck(

verify(&components, channel, commitment_scheme_verifier, proof)
}

#[cfg(test)]
mod tests {
use brainfuck_vm::{compiler::Compiler, test_helper::create_test_machine};

use super::{prove_brainfuck, verify_brainfuck};

#[test]
fn test_proof() {
// Get an execution trace from a valid Brainfuck program
let code = "+++>,<[>+.<-]";
let mut compiler = Compiler::new(code);
let instructions = compiler.compile();
let (mut machine, _) = create_test_machine(&instructions, &[1]);
let () = machine.execute().expect("Failed to execute machine");

let brainfuck_proof = prove_brainfuck(&machine).unwrap();

verify_brainfuck(brainfuck_proof).unwrap();
}
}
46 changes: 28 additions & 18 deletions crates/brainfuck_prover/src/components/memory/component.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use num_traits::One;
use stwo_prover::{
constraint_framework::{
preprocessed_columns::PreprocessedColumn, EvalAtRow, FrameworkComponent, FrameworkEval,
RelationEntry, ORIGINAL_TRACE_IDX,
RelationEntry,
},
core::{
channel::Channel,
Expand Down Expand Up @@ -65,10 +65,14 @@ impl FrameworkEval for MemoryEval {
let is_first = eval.get_preprocessed_column(PreprocessedColumn::IsFirst(self.log_size()));

// Get all the required registers' values
let [clk, next_clk] = eval.next_interaction_mask(ORIGINAL_TRACE_IDX, [0, 1]);
let [mp, next_mp] = eval.next_interaction_mask(ORIGINAL_TRACE_IDX, [0, 1]);
let [mv, next_mv] = eval.next_interaction_mask(ORIGINAL_TRACE_IDX, [0, 1]);
let [d, next_d] = eval.next_interaction_mask(ORIGINAL_TRACE_IDX, [0, 1]);
let clk = eval.next_trace_mask();
let mp = eval.next_trace_mask();
let mv = eval.next_trace_mask();
let d = eval.next_trace_mask();
let next_clk = eval.next_trace_mask();
let next_mp = eval.next_trace_mask();
let next_mv = eval.next_trace_mask();
let next_d = eval.next_trace_mask();

// Boundary constraints
eval.add_constraint(is_first.clone() * clk.clone());
Expand All @@ -84,28 +88,34 @@ impl FrameworkEval for MemoryEval {

// If `mp` remains the same, `clk` increases by 1
eval.add_constraint(
(next_mp.clone() - mp.clone()) * (next_clk - clk.clone() - BaseField::one().into()),
(next_mp.clone() - mp.clone() - BaseField::one().into()) *
(next_clk.clone() - clk.clone() - BaseField::one().into()),
);

// If `mp` increases by 1, then `next_mv` must be 0
eval.add_constraint((next_mp.clone() - mp.clone()) * next_mv.clone());

// The next dummy is either 0 or 1
eval.add_constraint(next_d.clone() * (next_d - BaseField::one().into()));
eval.add_constraint(next_d.clone() * (next_d.clone() - BaseField::one().into()));

// If `d` is set, then `mp` remains the same
eval.add_constraint(d.clone() * (next_mp - mp.clone()));
eval.add_constraint(d.clone() * (next_mp.clone() - mp.clone()));

// If `d` is set, then `mv` remains the same
eval.add_constraint(d.clone() * (next_mv - mv.clone()));
eval.add_constraint(d.clone() * (next_mv.clone() - mv.clone()));

// LogUp of `clk`, `mp` and `mv`
let multiplicity = E::EF::from(d) - E::EF::one();
eval.add_to_relation(&[RelationEntry::new(
&self.memory_lookup_elements,
multiplicity,
&[clk, mp, mv],
)]);
let multiplicity_row = E::EF::from(d) - E::EF::one();
// LogUp of `next_clk`, `next_mp` and `next_mv`
let multiplicity_next_row = E::EF::from(next_d) - E::EF::one();
eval.add_to_relation(&[
RelationEntry::new(&self.memory_lookup_elements, multiplicity_row, &[clk, mp, mv]),
RelationEntry::new(
&self.memory_lookup_elements,
multiplicity_next_row,
&[next_clk, next_mp, next_mv],
),
]);

eval.finalize_logup();

Expand All @@ -127,7 +137,7 @@ pub struct InteractionClaim {

impl InteractionClaim {
/// Mix the sums from the logUp protocol into the Fiat-Shamir [`Channel`],
/// to bind the proof to the trace.
/// to bound the proof to the trace.
pub fn mix_into(&self, channel: &mut impl Channel) {
channel.mix_felts(&[self.claimed_sum]);
}
Expand Down Expand Up @@ -165,8 +175,8 @@ mod tests {

// Construct the IsFirst preprocessed column
let is_first_col = gen_is_first(LOG_SIZE);
let is_first_col2 = gen_is_first(LOG_SIZE);
let preprocessed_trace = vec![is_first_col, is_first_col2];
let is_first_col_2 = gen_is_first(LOG_SIZE);
let preprocessed_trace = vec![is_first_col, is_first_col_2];

// Construct the main trace from the execution trace
let table = MemoryTable::from(trace_vm);
Expand Down

0 comments on commit 33ce682

Please sign in to comment.