Formal Verification: Front-end API for Sumchecks

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: ```rust /// 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: ```rust 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.