Skip to content

Commit

Permalink
chore: add accessors and re-org
Browse files Browse the repository at this point in the history
  • Loading branch information
Al-Kindi-0 committed Apr 5, 2024
1 parent 433e67b commit 8e2173e
Show file tree
Hide file tree
Showing 8 changed files with 94 additions and 62 deletions.
8 changes: 7 additions & 1 deletion processor/src/trace/virtual_bus/circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ pub use prover::prove;
mod verifier;
pub use verifier::verify;

use super::sum_check::Proof as SumCheckProof;
use super::sum_check::{FinalOpeningClaim, Proof as SumCheckProof};

/// A GKR proof for the correct evaluation of the sum of fractions circuit.
#[derive(Debug)]
Expand All @@ -23,6 +23,12 @@ pub struct GkrCircuitProof<E: FieldElement + 'static> {
final_layer_proof: FinalLayerProof<E>,
}

impl<E: FieldElement + 'static> GkrCircuitProof<E> {
pub fn get_final_opening_claim(&self) -> FinalOpeningClaim<E> {
self.final_layer_proof.after_merge_proof.openings_claim.clone()
}
}

/// A set of sum-check proofs for all GKR layers but for the input circuit layer.
#[derive(Debug)]
pub struct BeforeFinalLayerProof<E: FieldElement + 'static> {
Expand Down
2 changes: 2 additions & 0 deletions processor/src/trace/virtual_bus/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,8 @@ mod verifier;
pub use verifier::VirtualBusVerifier;
mod error;
mod sub_bus;

#[cfg(test)]
mod tests;

/// Generates the composition polynomials describing the virtual bus.
Expand Down
2 changes: 1 addition & 1 deletion processor/src/trace/virtual_bus/prover.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ where
}

/// Proves the GKR-LogUp relation.
pub fn prove(&self, trace: MainTrace, transcript: &mut C) -> GkrCircuitProof<E> {
pub fn prove(&self, trace: &MainTrace, transcript: &mut C) -> GkrCircuitProof<E> {
// TODO: Optimize this so that we can work with base field element directly and thus save
// on memory usage.
let trace_len = trace.num_rows();
Expand Down
1 change: 1 addition & 0 deletions processor/src/trace/virtual_bus/sub_bus/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use vm_core::FieldElement;
mod range_checker;
pub use range_checker::*;

/// Defines a sub-bus of the global virtual bus
pub trait BusBuilder<E: FieldElement> {
fn compute_initial_claim(&self) -> E;

Expand Down
32 changes: 32 additions & 0 deletions processor/src/trace/virtual_bus/sub_bus/range_checker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,28 @@ use miden_air::trace::{
};
use vm_core::FieldElement;

/// Defines the range checker sub-bus.
///
/// Define the following variables:
///
/// - rc_value: the range checker value
/// - rc_multiplicity: the range checker multiplicity value
/// - flag_s: boolean flag indicating a stack operation with range checks. This flag is degree 3.
/// - sv0-sv3: stack value 0-3, the 4 values range-checked from the stack
/// - flag_m: boolean flag indicating the memory chiplet is active (i.e. range checks are required).
/// This flag is degree 3.
/// - mv0-mv1: memory value 0-1, the 2 values range-checked from the memory chiplet
///
/// Let `col(x)` denote the multi-linear extension of trace column `col`. This means that
/// for x \in \{0 , 1\}^{\nu}, where \nu is the log_2 of the trace length, `col(x)` is the value
/// at row index [x] = \sum_{j=0}^{\nu - 1} x_j * 2^j of column `col`.
///
/// Given the above, the range checker is implemented using the expression
///
/// 0 = \sum_{x \in \{0 , 1\}^{\nu}} rc_multiplicity(x) / (alpha - rc_value)(x)
/// - flag_s(x) / (alpha - sv0)(x) - flag_s(x) / (alpha - sv1)(x)
/// - flag_s(x) / (alpha - sv2)(x) - flag_s(x) / (alpha - sv3)(x)
/// - flag_m(x) / (alpha - mv0)(x) - flag_m(x) / (alpha - mv1)(x)
pub struct RangeCheckerBus<E: FieldElement> {
alphas: Vec<E>,
}
Expand All @@ -29,9 +51,12 @@ impl<E: FieldElement + 'static> BusBuilder<E> for RangeCheckerBus<E> {

fn build_numerators(&self) -> Vec<Arc<dyn CompositionPolynomial<E>>> {
vec![
// rc_multiplicity(x)
Arc::new(RangeCheckMultiplicity::default()),
// flag_m(x)
Arc::new(MemoryFlagChiplet::default()),
Arc::new(MemoryFlagChiplet::default()),
// flag_s(x)
Arc::new(U32RangeCheckFlag::default()),
Arc::new(U32RangeCheckFlag::default()),
Arc::new(U32RangeCheckFlag::default()),
Expand All @@ -41,12 +66,19 @@ impl<E: FieldElement + 'static> BusBuilder<E> for RangeCheckerBus<E> {

fn build_denominators(&self) -> Vec<Arc<dyn CompositionPolynomial<E>>> {
vec![
// (alpha - rc_value)(x)
Arc::new(TableValue::new(self.alphas.clone())),
// (alpha - mv0)(x)
Arc::new(MemoryValue::new(0, self.alphas.clone())),
// (alpha - mv1)(x)
Arc::new(MemoryValue::new(1, self.alphas.clone())),
// (alpha - sv0)(x)
Arc::new(StackValue::new(0, self.alphas.clone())),
// (alpha - sv1)(x)
Arc::new(StackValue::new(1, self.alphas.clone())),
// (alpha - sv2)(x)
Arc::new(StackValue::new(2, self.alphas.clone())),
// (alpha - sv3)(x)
Arc::new(StackValue::new(3, self.alphas.clone())),
]
}
Expand Down
4 changes: 2 additions & 2 deletions processor/src/trace/virtual_bus/sum_check/prover/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ mod error;
/// protocol prover.
/// The sum-check protocol is an interactive protocol (IP) for proving the following relation:
///
/// v = \sum_{(x_0,\cdots, x_{\nu - 1}) \in \{0 , 1\}^{2^{\nu}}}
/// v = \sum_{(x_0,\cdots, x_{\nu - 1}) \in \{0 , 1\}^{\nu}}
/// g(f_0((x_0,\cdots, x_{\nu - 1})), \cdots , f_c((x_0,\cdots, x_{\nu - 1})))
///
/// where:
Expand Down Expand Up @@ -60,7 +60,7 @@ mod error;
/// of degree at most `d`. Thus, the Prover in each round sends `d + 1` values, either
/// the coefficients or the evaluations of `s_i`.
///
/// 2. The Prover has each `f_i` in its evaluation form over the hyper-cube \{0 , 1\}^{2^{\nu}}.
/// 2. The Prover has each `f_i` in its evaluation form over the hyper-cube \{0 , 1\}^{\nu}.
///
/// 3. An optimization is for the Prover to not send `s_i(0)` as it can be recoverd from the current
/// reduced claim s_{i - 1}(r_{i - 1}) using the relation s_{i}(0) = s_{i}(1) - s_{i - 1}(r_{i - 1}).
Expand Down
4 changes: 2 additions & 2 deletions processor/src/trace/virtual_bus/sum_check/verifier/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,11 +12,11 @@ mod error;
/// protocol verifier. The protocol is described in [`SumCheckProver`].
/// The sum-check Verifier is composed of two parts:
///
/// 1. Multi-round interaction where it sends challenges and receives polynomials. For each
/// 1. A multi-round interaction where it sends challenges and receives polynomials. For each
/// polynomial received it uses the sent randomness to reduce the current claim to a new one.
///
/// 2. A final round where the Verifier queries the multi-linear oracles it received at the outset
/// of the protocol (i.e., commitments) for their evaluations the random point
/// of the protocol (i.e., commitments) for their evaluations at the random point
/// `(r_0, ... , r_{\nu - 1})` where $\nu$ is the number of rounds of the sum-check protocol and
/// `r_i` is the randomness sent by the Verifier at each round.
pub struct SumCheckVerifier<B, E, P, C, H, V>
Expand Down
103 changes: 47 additions & 56 deletions processor/src/trace/virtual_bus/tests.rs
Original file line number Diff line number Diff line change
@@ -1,59 +1,50 @@
#[cfg(test)]
mod test {
use crate::{
trace::virtual_bus::{prover::VirtualBusProver, verifier::VirtualBusVerifier},
DefaultHost, ExecutionTrace, Process,
};
use alloc::vec::Vec;
use miden_air::{trace::main_trace::MainTrace, ExecutionOptions};
use vm_core::crypto::random::RpoRandomCoin;
use vm_core::{
code_blocks::CodeBlock, CodeBlockTable, Felt, FieldElement, Kernel, Operation, StackInputs,
};

#[test]
fn test_vb_prover() {
let s = 5;
let e = 5;
let stack: Vec<_> = (0..(1 << s)).into_iter().collect();
let operations: Vec<_> = (0..(1 << e))
.flat_map(|_| {
vec![Operation::U32split, Operation::U32add, Operation::U32xor, Operation::MStoreW]
})
.collect();

let trace = build_full_trace(&stack, operations, Kernel::default());

// TODO: this should be generated using the transcript up to when the prover sends the commitment
// of the main trace.
let alphas = vec![Felt::from(7898787_u32)];

let seed = [Felt::ZERO; 4]; // TODO: should be initialized with the appropriate transcript
let mut transcript = RpoRandomCoin::new(seed.into());

let vb_prover = VirtualBusProver::new(alphas.clone()).unwrap();

let proof = vb_prover.prove(trace, &mut transcript);

let seed = [Felt::ZERO; 4]; // TODO: should be initialized with the appropriate transcript
let mut transcript = RpoRandomCoin::new(seed.into());
let vb_verifier = VirtualBusVerifier::new(alphas).unwrap();
let _final_opening_claim = vb_verifier.verify(proof, &mut transcript);
}
use crate::{
trace::virtual_bus::{prover::VirtualBusProver, verifier::VirtualBusVerifier},
DefaultHost, ExecutionTrace, Process,
};
use alloc::vec::Vec;
use miden_air::{trace::main_trace::MainTrace, ExecutionOptions};
use vm_core::crypto::random::RpoRandomCoin;
use vm_core::{
code_blocks::CodeBlock, CodeBlockTable, Felt, FieldElement, Kernel, Operation, StackInputs,
};

#[test]
fn test_vb_prover_verifier() {
let s = 6;
let o = 6;
let stack: Vec<_> = (0..(1 << s)).into_iter().collect();
let operations: Vec<_> = (0..(1 << o))
.flat_map(|_| {
vec![Operation::U32split, Operation::U32add, Operation::U32xor, Operation::MStoreW]
})
.collect();

let trace = build_full_trace(&stack, operations, Kernel::default());

// this should be generated using the transcript up to when the prover sends the commitment
// to the main trace.
let alphas: Vec<Felt> = vec![test_utils::rand::rand_value()];

let seed = [Felt::ZERO; 4]; // should be initialized with the appropriate transcript
let mut transcript = RpoRandomCoin::new(seed.into());
let vb_prover = VirtualBusProver::new(alphas.clone()).unwrap();
let proof = vb_prover.prove(&trace, &mut transcript);

let seed = [Felt::ZERO; 4]; // should be initialized with the appropriate transcript
let mut transcript = RpoRandomCoin::new(seed.into());
let vb_verifier = VirtualBusVerifier::new(alphas).unwrap();
let _final_opening_claim = vb_verifier.verify(proof, &mut transcript);
}

fn build_full_trace(
stack_inputs: &[u64],
operations: Vec<Operation>,
kernel: Kernel,
) -> MainTrace {
let stack_inputs: Vec<Felt> = stack_inputs.iter().map(|a| Felt::new(*a)).collect();
let stack_inputs = StackInputs::new(stack_inputs).unwrap();
let host = DefaultHost::default();
let mut process = Process::new(kernel, stack_inputs, host, ExecutionOptions::default());
let program = CodeBlock::new_span(operations);
process.execute_code_block(&program, &CodeBlockTable::default()).unwrap();
let (trace, _, _): (MainTrace, _, _) = ExecutionTrace::test_finalize_trace(process);
fn build_full_trace(stack_inputs: &[u64], operations: Vec<Operation>, kernel: Kernel) -> MainTrace {
let stack_inputs: Vec<Felt> = stack_inputs.iter().map(|a| Felt::new(*a)).collect();
let stack_inputs = StackInputs::new(stack_inputs).unwrap();
let host = DefaultHost::default();
let mut process = Process::new(kernel, stack_inputs, host, ExecutionOptions::default());
let program = CodeBlock::new_span(operations);
process.execute_code_block(&program, &CodeBlockTable::default()).unwrap();
let (trace, _, _): (MainTrace, _, _) = ExecutionTrace::test_finalize_trace(process);

trace
}
trace
}

0 comments on commit 8e2173e

Please sign in to comment.