Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ resolver = "3"

[workspace.lints]
rust.missing_debug_implementations = "warn"
rust.unreachable_pub = "warn"
rust.unused_must_use = "deny"
rust.rust_2018_idioms = { level = "deny", priority = -1 }
rust.dead_code = "allow"
Expand All @@ -35,7 +34,6 @@ rustdoc.all = "warn"
all = { level = "warn", priority = -1 }
nursery = { level = "warn", priority = -1 }
doc_markdown = "allow"
pedantic = { level = "warn", priority = -1 }
cast_possible_truncation = "allow"
cast_precision_loss = "allow"
missing_errors_doc = "allow"
Expand All @@ -45,6 +43,20 @@ should_panic_without_expect = "allow"
similar_names = "allow"
suboptimal_flops = "allow"
cast_sign_loss = "allow"
redundant_pub_crate = "allow"
too_many_lines = "allow"
to_string_trait_impl = "allow"
transmute_ptr_to_ptr = "allow"
missing_transmute_annotations = "allow"
type_complexity = "allow"
needless_range_loop = "allow"
too_many_arguments = "allow"
result_large_err = "allow"
format_push_string = "allow"
option_if_let_else = "allow"
mismatching_type_param_order = "allow"
cognitive_complexity = "allow"
large_enum_variant = "allow"

[workspace.dependencies]
lean-isa = { path = "crates/leanIsa" }
Expand Down
64 changes: 34 additions & 30 deletions crates/air/src/prove.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,21 +76,21 @@ pub fn prove_many_air_3<
"TODO handle the case UNIVARIATE_SKIPS >= log_length"
);
}
for i in 0..tables_2.len() {
for witness in witnesses_2.iter().take(tables_2.len()) {
assert!(
univariate_skips < witnesses_2[i].log_n_rows(),
univariate_skips < witness.log_n_rows(),
"TODO handle the case UNIVARIATE_SKIPS >= log_length"
);
}
for i in 0..tables_3.len() {
for witness in witnesses_3.iter().take(tables_3.len()) {
assert!(
univariate_skips < witnesses_3[i].log_n_rows(),
univariate_skips < witness.log_n_rows(),
"TODO handle the case UNIVARIATE_SKIPS >= log_length"
);
}
let structured_air = if tables_1.len() > 0 {
let structured_air = if !tables_1.is_empty() {
tables_1[0].air.structured()
} else if tables_2.len() > 0 {
} else if !tables_2.is_empty() {
tables_2[0].air.structured()
} else {
tables_3[0].air.structured()
Expand All @@ -113,15 +113,15 @@ pub fn prove_many_air_3<

let log_lengths_1 = witnesses_1
.iter()
.map(|w| w.log_n_rows())
.map(super::witness::AirWitness::log_n_rows)
.collect::<Vec<_>>();
let log_lengths_2 = witnesses_2
.iter()
.map(|w| w.log_n_rows())
.map(super::witness::AirWitness::log_n_rows)
.collect::<Vec<_>>();
let log_lengths_3 = witnesses_3
.iter()
.map(|w| w.log_n_rows())
.map(super::witness::AirWitness::log_n_rows)
.collect::<Vec<_>>();

let max_n_constraints = Iterator::max(
Expand Down Expand Up @@ -186,10 +186,10 @@ pub fn prove_many_air_3<
sumcheck::prove_in_parallel_3::<EF, _, _, _, _>(
vec![univariate_skips; n_tables],
columns_for_zero_check_packed,
tables_1.iter().map(|t| &t.air).collect::<Vec<_>>(),
tables_2.iter().map(|t| &t.air).collect::<Vec<_>>(),
tables_3.iter().map(|t| &t.air).collect::<Vec<_>>(),
vec![&constraints_batching_scalars; n_tables],
&tables_1.iter().map(|t| &t.air).collect::<Vec<_>>(),
&tables_2.iter().map(|t| &t.air).collect::<Vec<_>>(),
&tables_3.iter().map(|t| &t.air).collect::<Vec<_>>(),
&vec![constraints_batching_scalars.as_slice(); n_tables],
all_zerocheck_challenges,
vec![true; n_tables],
prover_state,
Expand Down Expand Up @@ -237,11 +237,11 @@ pub fn prove_many_air_3<

impl<EF: ExtensionField<PF<EF>>, A: MyAir<EF>> AirTable<EF, A> {
#[instrument(name = "air: prove base", skip_all)]
pub fn prove_base<'a>(
pub fn prove_base(
&self,
prover_state: &mut FSProver<EF, impl FSChallenger<EF>>,
univariate_skips: usize,
witness: AirWitness<'a, PF<EF>>,
witness: AirWitness<'_, PF<EF>>,
) -> Vec<Evaluation<EF>> {
let mut res = prove_many_air_3::<EF, A, A, A>(
prover_state,
Expand All @@ -258,11 +258,11 @@ impl<EF: ExtensionField<PF<EF>>, A: MyAir<EF>> AirTable<EF, A> {
}

#[instrument(name = "air: prove base", skip_all)]
pub fn prove_extension<'a>(
pub fn prove_extension(
&self,
prover_state: &mut FSProver<EF, impl FSChallenger<EF>>,
univariate_skips: usize,
witness: AirWitness<'a, EF>,
witness: AirWitness<'_, EF>,
) -> Vec<Evaluation<EF>> {
let mut res = prove_many_air_3::<EF, A, A, A>(
prover_state,
Expand Down Expand Up @@ -290,8 +290,8 @@ fn eval_unstructured_column_groups<EF: ExtensionField<PF<EF>> + ExtensionField<I
for group in &witnesses.column_groups {
let batched_column = multilinears_linear_combination(
&witnesses.cols[group.clone()],
&eval_eq(&from_end(
&columns_batching_scalars,
&eval_eq(from_end(
columns_batching_scalars,
log2_ceil_usize(group.len()),
))[..group.len()],
);
Expand All @@ -300,7 +300,7 @@ fn eval_unstructured_column_groups<EF: ExtensionField<PF<EF>> + ExtensionField<I
let sub_evals = fold_multilinear(
&batched_column,
&MultilinearPoint(
outer_sumcheck_challenge[1..witnesses.log_n_rows() - univariate_skips + 1].to_vec(),
outer_sumcheck_challenge[1..=(witnesses.log_n_rows() - univariate_skips)].to_vec(),
),
);

Expand All @@ -323,8 +323,12 @@ fn open_unstructured_columns<'a, EF: ExtensionField<PF<EF>>>(
witnesses_1
.iter()
.chain(witnesses_2)
.map(|w| w.max_columns_per_group())
.chain(witnesses_3.iter().map(|w| w.max_columns_per_group())),
.map(super::witness::AirWitness::max_columns_per_group)
.chain(
witnesses_3
.iter()
.map(super::witness::AirWitness::max_columns_per_group),
),
)
.unwrap();
let columns_batching_scalars = prover_state.sample_vec(log2_ceil_usize(max_columns_per_group));
Expand Down Expand Up @@ -374,7 +378,7 @@ fn open_unstructured_columns<'a, EF: ExtensionField<PF<EF>>>(
[
from_end(&columns_batching_scalars, log2_ceil_usize(group.len())).to_vec(),
epsilons.0.clone(),
outer_sumcheck_challenge[1..log_n_rows - univariate_skips + 1].to_vec(),
outer_sumcheck_challenge[1..=(log_n_rows - univariate_skips)].to_vec(),
]
.concat(),
),
Expand All @@ -387,10 +391,10 @@ fn open_unstructured_columns<'a, EF: ExtensionField<PF<EF>>>(
}

#[instrument(skip_all)]
fn open_structured_columns<'a, EF: ExtensionField<PF<EF>> + ExtensionField<IF>, IF: Field>(
fn open_structured_columns<EF: ExtensionField<PF<EF>> + ExtensionField<IF>, IF: Field>(
prover_state: &mut FSProver<EF, impl FSChallenger<EF>>,
univariate_skips: usize,
witness: &AirWitness<'a, IF>,
witness: &AirWitness<'_, IF>,
outer_sumcheck_challenge: &[EF],
) -> Vec<Evaluation<EF>> {
let columns_batching_scalars = prover_state.sample_vec(witness.log_max_columns_per_group());
Expand All @@ -403,7 +407,7 @@ fn open_structured_columns<'a, EF: ExtensionField<PF<EF>> + ExtensionField<IF>,
for group in &witness.column_groups {
let batched_column = multilinears_linear_combination(
&witness.cols[group.clone()],
&eval_eq(&from_end(
&eval_eq(from_end(
&columns_batching_scalars,
log2_ceil_usize(group.len()),
))[..group.len()],
Expand All @@ -419,7 +423,7 @@ fn open_structured_columns<'a, EF: ExtensionField<PF<EF>> + ExtensionField<IF>,
let sub_evals = fold_multilinear(
&batched_column_mixed,
&MultilinearPoint(
outer_sumcheck_challenge[1..witness.log_n_rows() - univariate_skips + 1].to_vec(),
outer_sumcheck_challenge[1..=(witness.log_n_rows() - univariate_skips)].to_vec(),
),
);

Expand All @@ -434,7 +438,7 @@ fn open_structured_columns<'a, EF: ExtensionField<PF<EF>> + ExtensionField<IF>,
{
let point = [
epsilons.clone(),
outer_sumcheck_challenge[1..witness.log_n_rows() - univariate_skips + 1].to_vec(),
outer_sumcheck_challenge[1..=(witness.log_n_rows() - univariate_skips)].to_vec(),
]
.concat();
let mles_for_inner_sumcheck = vec![
Expand All @@ -456,8 +460,8 @@ fn open_structured_columns<'a, EF: ExtensionField<PF<EF>> + ExtensionField<IF>,
let (inner_challenges, all_inner_evals, _) = sumcheck::prove_in_parallel_1::<EF, _, _>(
vec![1; n_groups],
all_inner_mles,
vec![&ProductComputation; n_groups],
vec![&[]; n_groups],
&vec![&ProductComputation; n_groups],
&vec![[].as_slice(); n_groups],
vec![None; n_groups],
vec![false; n_groups],
prover_state,
Expand Down
14 changes: 9 additions & 5 deletions crates/air/src/table.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,12 @@ impl<EF: ExtensionField<PF<EF>>, A: MyAir<EF>> AirTable<EF, A> {
pub fn new(air: A) -> Self {
let symbolic_constraints = get_symbolic_constraints(&air, 0, 0);
let n_constraints = symbolic_constraints.len();
let constraint_degree =
Iterator::max(symbolic_constraints.iter().map(|c| c.degree_multiple())).unwrap();
let constraint_degree = Iterator::max(
symbolic_constraints
.iter()
.map(p3_uni_stark::SymbolicExpression::degree_multiple),
)
.unwrap();
assert_eq!(constraint_degree, air.degree());
Self {
air,
Expand All @@ -42,17 +46,17 @@ impl<EF: ExtensionField<PF<EF>>, A: MyAir<EF>> AirTable<EF, A> {
EF: ExtensionField<IF>,
{
if witness.n_columns() != self.n_columns() {
return Err(format!("Invalid number of columns",));
return Err("Invalid number of columns".to_string());
}
let handle_errors = |row: usize, constraint_checker: &mut ConstraintChecker<'_, IF, EF>| {
if constraint_checker.errors.len() > 0 {
if !constraint_checker.errors.is_empty() {
return Err(format!(
"Trace is not valid at row {}: contraints not respected: {}",
row,
constraint_checker
.errors
.iter()
.map(|e| e.to_string())
.map(std::string::ToString::to_string)
.collect::<Vec<_>>()
.join(", ")
));
Expand Down
23 changes: 16 additions & 7 deletions crates/air/src/test.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
use std::borrow::Borrow;

use p3_air::{Air, AirBuilder, BaseAir};
use p3_field::PrimeCharacteristicRing;
use p3_field::extension::BinomialExtensionField;
use p3_field::{PrimeCharacteristicRing, extension::BinomialExtensionField};
use p3_koala_bear::KoalaBear;
use p3_matrix::Matrix;
use rand::{Rng, SeedableRng, rngs::StdRng};
Expand Down Expand Up @@ -107,9 +106,13 @@ fn generate_structured_trace<const N_COLUMNS: usize, const N_PREPROCESSED_COLUMN
}
let mut witness_cols = vec![vec![F::ZERO]; N_COLUMNS - N_PREPROCESSED_COLUMNS];
for i in 1..n_rows {
for j in 0..N_COLUMNS - N_PREPROCESSED_COLUMNS {
let witness_cols_j_i_min_1 = witness_cols[j][i - 1];
witness_cols[j].push(
for (j, witness_col) in witness_cols
.iter_mut()
.enumerate()
.take(N_COLUMNS - N_PREPROCESSED_COLUMNS)
{
let witness_cols_j_i_min_1 = witness_col[i - 1];
witness_col.push(
witness_cols_j_i_min_1
+ F::from_usize(j + N_PREPROCESSED_COLUMNS)
+ (0..N_PREPROCESSED_COLUMNS)
Expand All @@ -133,8 +136,12 @@ fn generate_unstructured_trace<const N_COLUMNS: usize, const N_PREPROCESSED_COLU
}
let mut witness_cols = vec![vec![]; N_COLUMNS - N_PREPROCESSED_COLUMNS];
for i in 0..n_rows {
for j in 0..N_COLUMNS - N_PREPROCESSED_COLUMNS {
witness_cols[j].push(
for (j, witness_col) in witness_cols
.iter_mut()
.enumerate()
.take(N_COLUMNS - N_PREPROCESSED_COLUMNS)
{
witness_col.push(
F::from_usize(j + N_PREPROCESSED_COLUMNS)
+ (0..N_PREPROCESSED_COLUMNS)
.map(|k| trace[k][i])
Expand Down Expand Up @@ -227,6 +234,7 @@ fn test_unstructured_air() {
}

#[test]
#[allow(clippy::too_many_lines)]
fn test_many_unstructured_air() {
const N_COLUMNS_A: usize = 10;
const N_PREPROCESSED_COLUMNS_A: usize = 3;
Expand Down Expand Up @@ -347,6 +355,7 @@ fn test_many_unstructured_air() {
}

#[test]
#[allow(clippy::too_many_lines)]
fn test_many_structured_air() {
const N_COLUMNS_A: usize = 10;
const N_PREPROCESSED_COLUMNS_A: usize = 3;
Expand Down
4 changes: 2 additions & 2 deletions crates/air/src/uni_skip_utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use tracing::instrument;
use whir_p3::poly::evals::{eval_eq, scale_poly};

#[instrument(name = "matrix_up_folded", skip_all)]
pub(crate) fn matrix_up_folded<F: Field>(outer_challenges: &[F]) -> Vec<F> {
pub fn matrix_up_folded<F: Field>(outer_challenges: &[F]) -> Vec<F> {
let n = outer_challenges.len();
let mut folded = eval_eq(outer_challenges);
let outer_challenges_prod: F = outer_challenges.iter().copied().product();
Expand All @@ -13,7 +13,7 @@ pub(crate) fn matrix_up_folded<F: Field>(outer_challenges: &[F]) -> Vec<F> {
}

#[instrument(name = "matrix_down_folded", skip_all)]
pub(crate) fn matrix_down_folded<F: Field>(outer_challenges: &[F]) -> Vec<F> {
pub fn matrix_down_folded<F: Field>(outer_challenges: &[F]) -> Vec<F> {
let n = outer_challenges.len();
let mut folded = vec![F::ZERO; 1 << n];
for k in 0..n {
Expand Down
10 changes: 5 additions & 5 deletions crates/air/src/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use p3_field::Field;
use rayon::prelude::*;
use whir_p3::poly::multilinear::MultilinearPoint;

pub(crate) fn matrix_up_lde<F: Field>(point: &[F]) -> F {
pub fn matrix_up_lde<F: Field>(point: &[F]) -> F {
/*
Matrix UP:

Expand All @@ -29,7 +29,7 @@ pub(crate) fn matrix_up_lde<F: Field>(point: &[F]) -> F {
* (F::ONE - point[point.len() - 1] * F::TWO)
}

pub(crate) fn matrix_down_lde<F: Field>(point: &[F]) -> F {
pub fn matrix_down_lde<F: Field>(point: &[F]) -> F {
/*
Matrix DOWN:

Expand Down Expand Up @@ -130,21 +130,21 @@ fn next_mle<F: Field>(point: &[F]) -> F {
.sum()
}

pub(crate) fn columns_up_and_down<F: Field>(columns: &[&[F]]) -> Vec<Vec<F>> {
pub fn columns_up_and_down<F: Field>(columns: &[&[F]]) -> Vec<Vec<F>> {
columns
.par_iter()
.map(|c| column_up(c))
.chain(columns.par_iter().map(|c| column_down(c)))
.collect()
}

pub(crate) fn column_up<F: Field>(column: &[F]) -> Vec<F> {
pub fn column_up<F: Field>(column: &[F]) -> Vec<F> {
let mut up = column.to_vec();
up[column.len() - 1] = up[column.len() - 2];
up
}

pub(crate) fn column_down<F: Field>(column: &[F]) -> Vec<F> {
pub fn column_down<F: Field>(column: &[F]) -> Vec<F> {
let mut down = column[1..].to_vec();
down.push(*down.last().unwrap());
down
Expand Down
Loading
Loading