diff --git a/triton-vm/src/table/cross_table_argument.rs b/triton-vm/src/table/cross_table_argument.rs index 4e004895..efa4d1aa 100644 --- a/triton-vm/src/table/cross_table_argument.rs +++ b/triton-vm/src/table/cross_table_argument.rs @@ -224,3 +224,56 @@ impl GrandCrossTableArg { ] } } + +#[cfg(test)] +mod tests { + use proptest::prelude::*; + use proptest_arbitrary_interop::arb; + use test_strategy::proptest; + + use super::*; + + #[proptest] + fn permutation_argument_is_identical_to_evaluating_zerofier_polynomial( + #[strategy(arb())] roots: Vec, + #[strategy(arb())] initial: XFieldElement, + #[strategy(arb())] challenge: BFieldElement, + ) { + let poly_evaluation = initial * Polynomial::zerofier(&roots).evaluate(challenge); + let perm_arg_terminal = PermArg::compute_terminal(&roots, initial, challenge.lift()); + prop_assert_eq!(poly_evaluation, perm_arg_terminal); + } + + #[proptest] + fn evaluation_argument_is_identical_to_evaluating_polynomial( + #[strategy(arb())] polynomial: Polynomial, + #[strategy(arb())] challenge: BFieldElement, + ) { + let poly_evaluation = polynomial.evaluate(challenge).lift(); + + let mut polynomial = polynomial; + polynomial.normalize(); // remove leading zeros + let initial = polynomial.coefficients.pop(); + let initial = initial.ok_or(TestCaseError::Reject("polynomial must be non-zero".into()))?; + polynomial.coefficients.reverse(); + let eval_arg_terminal = + EvalArg::compute_terminal(&polynomial.coefficients, initial.lift(), challenge.lift()); + + prop_assert_eq!(poly_evaluation, eval_arg_terminal); + } + + #[proptest] + fn lookup_argument_is_identical_to_inverse_of_evaluation_of_zerofier_polynomial( + #[strategy(arb())] + #[filter(#roots.iter().all(|&r| r != #challenge) )] + roots: Vec, + #[strategy(arb())] initial: XFieldElement, + #[strategy(arb())] challenge: BFieldElement, + ) { + let polynomial = Polynomial::zerofier(&roots); + let derivative = polynomial.formal_derivative(); + let poly_evaluation = derivative.evaluate(challenge) / polynomial.evaluate(challenge); + let lookup_arg_terminal = LookupArg::compute_terminal(&roots, initial, challenge.lift()); + prop_assert_eq!(initial + poly_evaluation, lookup_arg_terminal); + } +}