Skip to content

Commit

Permalink
feat: array and symbolic evaluation (#390)
Browse files Browse the repository at this point in the history
  • Loading branch information
@tamirhemo
tamirhemo authored Mar 15, 2024
1 parent 67d9ed4 commit a16c0f9
Show file tree
Hide file tree
Showing 21 changed files with 1,208 additions and 532 deletions.
1 change: 1 addition & 0 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

222 changes: 190 additions & 32 deletions core/src/stark/folder.rs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,12 @@
use super::{PackedChallenge, PackedVal, StarkGenericConfig};
use std::{
marker::PhantomData,
ops::{Add, Mul, MulAssign, Sub},
};

use super::{Challenge, PackedChallenge, PackedVal, StarkGenericConfig, Val};
use crate::air::{EmptyMessageBuilder, MultiTableAirBuilder};
use p3_air::{AirBuilder, ExtensionBuilder, PairBuilder, PermutationAirBuilder, TwoRowMatrixView};
use p3_field::AbstractField;
use p3_field::{AbstractField, ExtensionField, Field};

/// A folder for prover constraints.
pub struct ProverConstraintFolder<'a, SC: StarkGenericConfig> {
Expand Down Expand Up @@ -95,57 +100,110 @@ impl<'a, SC: StarkGenericConfig> PairBuilder for ProverConstraintFolder<'a, SC>

impl<'a, SC: StarkGenericConfig> EmptyMessageBuilder for ProverConstraintFolder<'a, SC> {}

pub type VerifierConstraintFolder<'a, SC> =
GenericVerifierConstraintFolder<'a, Val<SC>, Challenge<SC>, Challenge<SC>, Challenge<SC>>;

/// A folder for verifier constraints.
pub struct VerifierConstraintFolder<'a, SC: StarkGenericConfig> {
pub preprocessed: TwoRowMatrixView<'a, SC::Challenge>,
pub main: TwoRowMatrixView<'a, SC::Challenge>,
pub perm: TwoRowMatrixView<'a, SC::Challenge>,
pub perm_challenges: &'a [SC::Challenge],
pub cumulative_sum: SC::Challenge,
pub is_first_row: SC::Challenge,
pub is_last_row: SC::Challenge,
pub is_transition: SC::Challenge,
pub alpha: SC::Challenge,
pub accumulator: SC::Challenge,
pub struct GenericVerifierConstraintFolder<'a, F, EF, Var, Expr> {
pub preprocessed: TwoRowMatrixView<'a, Var>,
pub main: TwoRowMatrixView<'a, Var>,
pub perm: TwoRowMatrixView<'a, Var>,
pub perm_challenges: &'a [EF],
pub cumulative_sum: Var,
pub is_first_row: Var,
pub is_last_row: Var,
pub is_transition: Var,
pub alpha: EF,
pub accumulator: Expr,
pub _marker: PhantomData<F>,
}

impl<'a, SC: StarkGenericConfig> AirBuilder for VerifierConstraintFolder<'a, SC> {
type F = SC::Val;
type Expr = SC::Challenge;
type Var = SC::Challenge;
type M = TwoRowMatrixView<'a, SC::Challenge>;
impl<'a, F, EF, Var, Expr> AirBuilder for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
where
F: Field,
EF: ExtensionField<F>,
Expr: AbstractField
+ From<F>
+ Add<Var, Output = Expr>
+ Add<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<F, Output = Expr>
+ MulAssign<EF>,
Var: Into<Expr>
+ Copy
+ Add<F, Output = Expr>
+ Add<Var, Output = Expr>
+ Add<Expr, Output = Expr>
+ Sub<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<Expr, Output = Expr>
+ Mul<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<Expr, Output = Expr>,
{
type F = F;
type Expr = Expr;
type Var = Var;
type M = TwoRowMatrixView<'a, Var>;

fn main(&self) -> Self::M {
self.main
}

fn is_first_row(&self) -> Self::Expr {
self.is_first_row
self.is_first_row.into()
}

fn is_last_row(&self) -> Self::Expr {
self.is_last_row
self.is_last_row.into()
}

fn is_transition_window(&self, size: usize) -> Self::Expr {
if size == 2 {
self.is_transition
self.is_transition.into()
} else {
panic!("uni-stark only supports a window size of 2")
}
}

fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
let x: SC::Challenge = x.into();
let x: Expr = x.into();
self.accumulator *= self.alpha;
self.accumulator += x;
}
}

impl<'a, SC: StarkGenericConfig> ExtensionBuilder for VerifierConstraintFolder<'a, SC> {
type EF = SC::Challenge;
type ExprEF = SC::Challenge;
type VarEF = SC::Challenge;
impl<'a, F, EF, Var, Expr> ExtensionBuilder
for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
where
F: Field,
EF: ExtensionField<F>,
Expr: AbstractField<F = EF>
+ From<F>
+ Add<Var, Output = Expr>
+ Add<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<F, Output = Expr>
+ MulAssign<EF>,
Var: Into<Expr>
+ Copy
+ Add<F, Output = Expr>
+ Add<Var, Output = Expr>
+ Add<Expr, Output = Expr>
+ Sub<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<Expr, Output = Expr>
+ Mul<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<Expr, Output = Expr>,
{
type EF = EF;
type ExprEF = Expr;
type VarEF = Var;

fn assert_zero_ext<I>(&mut self, x: I)
where
Expand All @@ -155,8 +213,33 @@ impl<'a, SC: StarkGenericConfig> ExtensionBuilder for VerifierConstraintFolder<'
}
}

impl<'a, SC: StarkGenericConfig> PermutationAirBuilder for VerifierConstraintFolder<'a, SC> {
type MP = TwoRowMatrixView<'a, SC::Challenge>;
impl<'a, F, EF, Var, Expr> PermutationAirBuilder
for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
where
F: Field,
EF: ExtensionField<F>,
Expr: AbstractField<F = EF>
+ From<F>
+ Add<Var, Output = Expr>
+ Add<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<F, Output = Expr>
+ MulAssign<EF>,
Var: Into<Expr>
+ Copy
+ Add<F, Output = Expr>
+ Add<Var, Output = Expr>
+ Add<Expr, Output = Expr>
+ Sub<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<Expr, Output = Expr>
+ Mul<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<Expr, Output = Expr>,
{
type MP = TwoRowMatrixView<'a, Var>;

fn permutation(&self) -> Self::MP {
self.perm
Expand All @@ -167,18 +250,93 @@ impl<'a, SC: StarkGenericConfig> PermutationAirBuilder for VerifierConstraintFol
}
}

impl<'a, SC: StarkGenericConfig> MultiTableAirBuilder for VerifierConstraintFolder<'a, SC> {
type Sum = SC::Challenge;
impl<'a, F, EF, Var, Expr> MultiTableAirBuilder
for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
where
F: Field,
EF: ExtensionField<F>,
Expr: AbstractField<F = EF>
+ From<F>
+ Add<Var, Output = Expr>
+ Add<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<F, Output = Expr>
+ MulAssign<EF>,
Var: Into<Expr>
+ Copy
+ Add<F, Output = Expr>
+ Add<Var, Output = Expr>
+ Add<Expr, Output = Expr>
+ Sub<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<Expr, Output = Expr>
+ Mul<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<Expr, Output = Expr>,
{
type Sum = Var;

fn cumulative_sum(&self) -> Self::Sum {
self.cumulative_sum
}
}

impl<'a, SC: StarkGenericConfig> PairBuilder for VerifierConstraintFolder<'a, SC> {
impl<'a, F, EF, Var, Expr> PairBuilder for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
where
F: Field,
EF: ExtensionField<F>,
Expr: AbstractField<F = EF>
+ From<F>
+ Add<Var, Output = Expr>
+ Add<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<F, Output = Expr>
+ MulAssign<EF>,
Var: Into<Expr>
+ Copy
+ Add<F, Output = Expr>
+ Add<Var, Output = Expr>
+ Add<Expr, Output = Expr>
+ Sub<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<Expr, Output = Expr>
+ Mul<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<Expr, Output = Expr>,
{
fn preprocessed(&self) -> Self::M {
self.preprocessed
}
}

impl<'a, SC: StarkGenericConfig> EmptyMessageBuilder for VerifierConstraintFolder<'a, SC> {}
impl<'a, F, EF, Var, Expr> EmptyMessageBuilder
for GenericVerifierConstraintFolder<'a, F, EF, Var, Expr>
where
F: Field,
EF: ExtensionField<F>,
Expr: AbstractField<F = EF>
+ From<F>
+ Add<Var, Output = Expr>
+ Add<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<F, Output = Expr>
+ MulAssign<EF>,
Var: Into<Expr>
+ Copy
+ Add<F, Output = Expr>
+ Add<Var, Output = Expr>
+ Add<Expr, Output = Expr>
+ Sub<F, Output = Expr>
+ Sub<Var, Output = Expr>
+ Sub<Expr, Output = Expr>
+ Mul<F, Output = Expr>
+ Mul<Var, Output = Expr>
+ Mul<Expr, Output = Expr>,
{
}
1 change: 1 addition & 0 deletions core/src/stark/verifier.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -216,6 +216,7 @@ impl<SC: StarkGenericConfig, A: MachineAir<SC::Val>> Verifier<SC, A> {
is_transition,
alpha,
accumulator: SC::Challenge::zero(),
_marker: PhantomData,
};
chip.eval(&mut folder);

Expand Down
1 change: 1 addition & 0 deletions recursion/compiler/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,5 +11,6 @@ sp1-recursion-core = { path = "../core" }

[dev-dependencies]
p3-baby-bear = { workspace = true }
p3-air = { workspace = true }
sp1-core = { path = "../../core" }
rand = "0.8.4"
33 changes: 33 additions & 0 deletions recursion/compiler/examples/verifier.rs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
use p3_air::Air;

use sp1_core::air::MachineAir;
use sp1_core::stark::{GenericVerifierConstraintFolder, MachineChip, StarkGenericConfig};
use sp1_recursion_compiler::ir::{Ext, SymbolicExt};

#[allow(clippy::type_complexity)]
#[allow(dead_code)]
fn verify_constraints<SC: StarkGenericConfig, A: MachineAir<SC::Val>>(
chip: MachineChip<SC, A>,
folder: &mut GenericVerifierConstraintFolder<
SC::Val,
SC::Challenge,
Ext<SC::Val, SC::Challenge>,
SymbolicExt<SC::Val, SC::Challenge>,
>,
) where
A: for<'a> Air<
GenericVerifierConstraintFolder<
'a,
SC::Val,
SC::Challenge,
Ext<SC::Val, SC::Challenge>,
SymbolicExt<SC::Val, SC::Challenge>,
>,
>,
{
chip.eval(folder);
}

fn main() {
println!("Hello, world!");
}
Loading

0 comments on commit a16c0f9

Please sign in to comment.