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
11 changes: 11 additions & 0 deletions .github/workflows/rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,11 @@ jobs:
run: cargo clippy -p jolt-verifier --all-targets --features core-fixtures
- name: cargo clippy -p jolt-verifier --features core-fixtures,zk
run: cargo clippy -p jolt-verifier --all-targets --features core-fixtures,zk
# The field-inline feature is not enabled by host/zk/default, so the
# workspace-wide invocations above never build it. Lint the crates that
# define it explicitly so the feature keeps compiling.
- name: cargo clippy --features field-inline
run: cargo clippy -p tracer -p jolt-program -p jolt-riscv -p jolt-lookup-tables --all-targets --features field-inline

machete:
runs-on: ubuntu-latest
Expand Down Expand Up @@ -253,6 +258,12 @@ jobs:
fi
cargo nextest run -p "$pkg" "${features[@]}" --no-tests=pass
done
- name: Test crates with field-inline
shell: bash
run: |
set -euo pipefail
cargo nextest run -p jolt-program -p jolt-riscv -p jolt-lookup-tables \
--features field-inline --no-tests=pass

test-inlines:
name: Test inlines
Expand Down
3 changes: 2 additions & 1 deletion Cargo.lock

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

15 changes: 14 additions & 1 deletion crates/jolt-lookup-tables/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,14 @@ categories = ["cryptography"]
[lints]
workspace = true

[features]
core-abi-tests = []
field-inline = [
"jolt-core/field-inline",
"jolt-riscv/field-inline",
"tracer/field-inline",
]

[dependencies]
jolt-field = { workspace = true }
jolt-riscv = { workspace = true, features = ["serialization"] }
Expand All @@ -21,6 +29,11 @@ strum = { workspace = true, features = ["derive"] }
jolt-core = { workspace = true, default-features = false, features = [
"minimal",
] }
jolt-riscv = { workspace = true, features = ["serialization", "test-utils"] }
jolt-riscv = { workspace = true, features = ["serialization"] }
rand = { workspace = true }
tracer = { workspace = true, features = ["std", "test-utils"] }

[[test]]
name = "core_lookup_table_abi"
path = "tests/core_lookup_table_abi.rs"
required-features = ["core-abi-tests"]
38 changes: 32 additions & 6 deletions crates/jolt-lookup-tables/src/instructions/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,36 @@ use std::any::TypeId;
use jolt_riscv::{Flags, InstructionFlags, JoltCycle, JoltInstructionRowData};
use rand::prelude::*;
use tracer::emulator::{cpu::Cpu, terminal::DummyTerminal};
use tracer::instruction::format::{InstructionFormat, InstructionRegisterState};
use tracer::instruction::{jal::JAL, jalr::JALR, Cycle, RISCVCycle, RISCVTrace};

use crate::{InstructionLookupTable, LookupQuery, XLEN};

pub trait RandomLookupCycle: JoltCycle {
fn random(rng: &mut StdRng) -> Self;
}

impl<T> RandomLookupCycle for RISCVCycle<T>
where
T: tracer::instruction::RISCVInstruction + JoltInstructionRowData,
{
fn random(rng: &mut StdRng) -> Self {
let instruction = T::random(rng);
let concrete: tracer::instruction::Instruction = instruction.into();
let source_instruction = concrete.source_instruction();
let register_state =
<<T::Format as InstructionFormat>::RegisterState as InstructionRegisterState>::random(
rng,
&source_instruction.row().operands,
);
Self {
instruction,
register_state,
ram_access: T::RAMAccess::default(),
}
}
}

/// Internal helper for [`materialize_entry_test!`]. The macro picks up the
/// verbose `Foo<RISCVCycle<TracerType>>` / `RISCVCycle<TracerType>` type pair
/// from a Jolt struct ident and a tracer instruction path, and passes the
Expand All @@ -20,12 +46,12 @@ pub fn materialize_entry_test_fn<T, C, I>(
instr_wrapper: impl Fn(C::Instruction) -> I,
) where
T: LookupQuery<XLEN> + core::fmt::Debug,
C: JoltCycle,
C: RandomLookupCycle,
I: InstructionLookupTable<XLEN>,
{
let mut rng = StdRng::seed_from_u64(12345);
for _ in 0..10_000 {
let raw = C::random(&mut rng);
let raw: C = RandomLookupCycle::random(&mut rng);
let table = instr_wrapper(raw.instruction()).lookup_table().unwrap();
let cycle: T = cycle_wrapper(raw);
assert_eq!(
Expand Down Expand Up @@ -56,13 +82,13 @@ pub fn instruction_inputs_match_constraint_fn<C, T, I>(
cycle_wrapper: impl Fn(C) -> T,
instr_wrapper: impl Fn(C::Instruction) -> I,
) where
C: JoltCycle,
C: RandomLookupCycle,
T: LookupQuery<XLEN> + core::fmt::Debug,
I: JoltInstructionRowData + Flags,
{
let mut rng = StdRng::seed_from_u64(12345);
for _ in 0..10_000 {
let raw: C = C::random(&mut rng);
let raw: C = RandomLookupCycle::random(&mut rng);
let instr = raw.instruction();
let normalized = instr.jolt_instruction_row();
let unexpanded_pc = normalized.address as u64;
Expand Down Expand Up @@ -116,14 +142,14 @@ pub fn instruction_inputs_match_constraint_fn<C, T, I>(
)]
pub fn lookup_output_matches_trace_test_fn<C, T>(cycle_wrapper: impl Fn(C) -> T)
where
C: JoltCycle + Copy + core::fmt::Debug,
C: RandomLookupCycle + Copy + core::fmt::Debug,
C::Instruction: RISCVTrace + 'static,
RISCVCycle<C::Instruction>: Into<Cycle>,
T: LookupQuery<XLEN>,
{
let mut rng = StdRng::seed_from_u64(12345);
for _ in 0..10_000 {
let raw: C = C::random(&mut rng);
let raw: C = RandomLookupCycle::random(&mut rng);
let instr = raw.instruction();
let normalized = instr.jolt_instruction_row();
let rs1_idx = normalized.operands.rs1;
Expand Down
2 changes: 1 addition & 1 deletion crates/jolt-lookup-tables/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,4 +12,4 @@ pub use interleave::{interleave_bits, uninterleave_bits};
pub use lookup_bits::LookupBits;
pub use tables::prefixes::ALL_PREFIXES;
pub use tables::{LookupTableKind, PrefixSuffixDecomposition};
pub use traits::{InstructionLookupTable, LookupQuery, LookupTable};
pub use traits::{InstructionLookupTable, JoltLookupQuery, LookupQuery, LookupTable};
17 changes: 6 additions & 11 deletions crates/jolt-lookup-tables/src/tables/prefixes/change_divisor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,15 +15,11 @@ impl<F: Field> SparseDensePrefix<F> for ChangeDivisorPrefix {
fn evaluate(checkpoints: &[PrefixEval<F>], b: LookupBits, suffix_len: usize) -> F {
let j_start = 2 * XLEN - suffix_len - b.len();

// change_divisor computes: checkpoint * x_msb * prod((1-x_i) * y_i) for remaining pairs
// where x_msb is the first x bit (at j=0).
//
// At j=0: x_msb must be 1, all remaining x bits must be 0, all y bits must be 1.
// At j=1: checkpoint * r_x (from j=1) * c (y bit) — special case for first y bit.
// At j>1: checkpoint * (1-x_i) * y_i for each pair.
//
// At binary points, non-zero only when x_msb=1, all subsequent x bits=0, all y bits=1.
// Exception: j=1 uses x*y instead of (1-x)*y.
// change_divisor restricted to binary points is checkpoint * x_0 * y_0
// * prod_{i>0}((1-x_i) * y_i): non-zero only when the operand MSB x_0 is 1,
// every later x bit is 0, and every y bit is 1. When the phase does not
// contain the MSB pair (j_start > 0), the x_0 * y_0 factor is already
// folded into the checkpoint.

if j_start == 0 {
// Phase includes the MSB x bit. Extract it.
Expand All @@ -43,8 +39,7 @@ impl<F: Field> SparseDensePrefix<F> for ChangeDivisorPrefix {
return F::zero();
}

// j=1 contributes x*y = x_msb * y_0, j>1 contributes (1-x_i)*y_i.
// Since x_rest=0 and all y=1, each (1-0)*1 = 1, and x_msb*y_0 = 1.
// With x_msb=1, x_rest=0, and all y bits 1, every product factor is 1.
checkpoints[Prefixes::ChangeDivisor]
} else {
// All x bits must be 0, all y bits must be 1 for non-zero result
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,15 +12,9 @@ impl<F: Field> SparseDensePrefix<F> for LeftShiftHelperPrefix {
}

fn evaluate(checkpoints: &[PrefixEval<F>], b: LookupBits, _suffix_len: usize) -> F {
// Tracks product of (1 + y_i) across rounds.
// At binary points, (1 + y_i) = 1 when y_i=0, 2 when y_i=1.
// So product = 2^(popcount(y_phase_bits)).
// But the leading run of y=1 bits is the only part that matters for the
// prefix_mle structure: checkpoint * prod(1+y_i) for phase bits, which at
// binary points = checkpoint * 2^(leading_ones of y) for the multiplicative chain,
// then remaining y=0 bits contribute factor 1.
// Actually the full product is needed: each y_i independently multiplies.
// At binary points: prod over all y_i in phase of (1+y_i) = 2^(count of y_i=1).
// Tracks the product of (1 + y_i) across rounds. At binary points each
// factor is 1 when y_i=0 and 2 when y_i=1, so the phase contribution is
// 2^(popcount of the phase's y bits).
let (_x, y) = b.uninterleave();
checkpoints[Prefixes::LeftShiftHelper] * F::from_u64(1u64 << u64::from(y).count_ones())
}
Expand Down
23 changes: 15 additions & 8 deletions crates/jolt-lookup-tables/src/tables/prefixes/mod.rs
Original file line number Diff line number Diff line change
@@ -1,14 +1,11 @@
//! Prefix polynomial evaluations for the sparse-dense decomposition.
//!
//! Each prefix captures the "contribution" of high-order bound variables
//! to a lookup table's MLE during sumcheck. Prefixes are evaluated at
//! binary points to materialize a dense polynomial, which is then bound
//! using standard polynomial operations during sumcheck rounds.
//!
//! Checkpoints accumulate prefix values across phases. They are initialized
//! via [`SparseDensePrefix::default_checkpoint`] and updated by the consumer
//! at phase boundaries (the bound polynomial's final scalar becomes the new
//! checkpoint).
//! to a lookup table's MLE during sumcheck. At the start of each phase,
//! prefixes are evaluated at binary points to materialize a dense polynomial,
//! which is then bound during the phase's sumcheck rounds. The fully bound
//! value becomes the prefix's checkpoint for the next phase. Checkpoints are
//! initialized via [`SparseDensePrefix::default_checkpoint`].

pub mod and;
pub mod andn;
Expand Down Expand Up @@ -76,6 +73,9 @@ pub trait SparseDensePrefix<F: Field>: 'static + Sync {
#[derive(Clone, Copy)]
pub struct PrefixEval<F>(pub(crate) F);

/// Full RV64 instruction lookup address width.
pub const LOG_K: usize = 2 * crate::XLEN;

impl<F: Display> Display for PrefixEval<F> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(f, "{}", self.0)
Expand All @@ -88,6 +88,13 @@ impl<F> From<F> for PrefixEval<F> {
}
}

impl<F: Copy> PrefixEval<F> {
/// Returns the underlying field evaluation.
pub fn value(self) -> F {
self.0
}
}

impl<F> Index<Prefixes> for &[PrefixEval<F>] {
type Output = F;

Expand Down
4 changes: 2 additions & 2 deletions crates/jolt-lookup-tables/src/tables/suffixes/rev8w.rs
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@
use super::SparseDenseSuffix;
use crate::lookup_bits::LookupBits;
use crate::tables::virtual_rev8w::rev8w;

pub enum Rev8WSuffix {}

impl SparseDenseSuffix for Rev8WSuffix {
fn suffix_mle(b: LookupBits) -> u64 {
let val = u128::from(b) as u32;
val.swap_bytes() as u64
rev8w(u128::from(b) as u64)
}
}
Loading