Formal Verification: Front-end API for Sumchecks #1131
Description
For the formal verification effort, it would be good to have a high-level API for constructing sumcheck instances that also allows them to be extracted via zklean-extractor. @jprider63 and I have come up with a candidate API that looks like this:
/// An arithmetic expression over opening values to use as either the LHS or RHS of an individual claim
pub enum ClaimExpr<F> {
/// A fixed value, e.g., 0 or 1
Val(F),
/// Arithmetic operations used in claims
Add(Box<ClaimExpr<F>>, Box<ClaimExpr<F>>),
Mul(Box<ClaimExpr<F>>, Box<ClaimExpr<F>>),
Sub(Box<ClaimExpr<F>>, Box<ClaimExpr<F>>),
/// Corresponds to a [`CommittedOpening`]
CommittedVar(CommittedPolynomial),
/// Corresponds to a [`VirtualOpening`]
VirtualVar(VirtualPolynomial),
}
/// Interpreted as `input_claim = eq_eval * output_claim`.
pub struct Claim<F: JoltField> {
/// Sumcheck to take the input opening values from
pub input_sumcheck_id: SumcheckId,
pub input_claim_expr: ClaimExpr<F>,
pub expected_output_claim_expr: ClaimExpr<F>,
/// Determines whether to use [`EqPolynomial`] or [`EqPlusOnePolynomial`]
pub is_offset: bool,
}
/// Combines the component claims and performs the linear combination with powers of gamma, representing the combined claim
/// \sum_i gamma^i * input_claim_i = \sum_i gamma^i * eq_eval_i * expected_output_claim_i
pub struct InputOutputClaims<F: JoltField> {
claims: Vec<Claim<F>>,
output_sumcheck_id: SumcheckId,
gamma_pows: Vec<F>,
}
impl<F: JoltField> InputOutputClaims<F> {
pub fn new(claims: Vec<Claim<F>>, output_sumcheck_id: SumcheckId, gamma: F) -> Self { ... }
/// Computes \sum_i gamma^i * input_claim_i
pub fn input_claim(&self, acc: &impl OpeningAccumulator<F>) -> F { ... }
/// Computes \sum_i gamma^i * eq_eval_i * expected_output_claim_i
pub fn expected_output_claim(&self, r: OpeningPoint<BIG_ENDIAN, F>, acc: &impl OpeningAccumulator<F>) -> F { ... }
}
pub trait FrontendSumcheck<F: JoltField> {
fn input_output_claims(gamma: F) -> InputOutputClaims<F>;
}This doesn't seem applicable to all of the sumchecks, but it seems to apply to the ones that we're most interested in extracting for the frontend verification, e.g., RamReadWriteChecking, RegistersReadWriteChecking, InstructionVirtualization, SpartanShift, etc. The idea is that the sumcheck verifier instance could implement FrontendSumcheck if this interface is applicable. It could then call InputOutputClaims::input_claim and InputOutputClaims::expected_output_claim from its SumcheckInstanceVerifier::input_claim and SumcheckInstanceVerifier::expected_output_claim methods. Having the sumchecks in this form would allow us to extract them for use in the frontend verification.
For example, the impl for RamReadWriteSumcheck might look like this:
impl<F: JoltField> FrontendSumcheck<F> for RamReadWriteCheckingVerifier<F> {
fn input_output_claims(gamma: F) -> InputOutputClaims<F> {
let ram_read_value: ClaimExpr<F> = VirtualPolynomial::RamReadValue.into();
let ram_write_value: ClaimExpr<F> = VirtualPolynomial::RamWriteValue.into();
let ram_ra: ClaimExpr<F> = VirtualPolynomial::RamRa.into();
let ram_val: ClaimExpr<F> = VirtualPolynomial::RamVal.into();
let ram_inc: ClaimExpr<F> = CommittedPolynomial::RamInc.into();
InputOutputClaims::new(
vec![
Claim {
input_sumcheck_id: SumcheckId::SpartanOuter,
input_claim_expr: ram_read_value,
expected_output_claim_expr: ram_ra.clone() * ram_val.clone(),
is_offset: false,
},
Claim {
input_sumcheck_id: SumcheckId::SpartanOuter,
input_claim_expr: ram_write_value,
expected_output_claim_expr: ram_ra * (ram_val + ram_inc),
is_offset: false,
},
],
SumcheckId::RamReadWriteChecking,
gamma,
)
}
}I've experimented with putting several of the sumchecks in this form, and I can make a draft PR with them shortly.
There might be a small amount of overhead involved with interpreting the ClaimExpr values when the verifier wants to evaluate, but if that becomes an issue, we believe we could get rid of most or all of that overhead by making the above into a macro.