From 6b8ffd90b77dc80e1cd7026c8554097e153eaa89 Mon Sep 17 00:00:00 2001
From: Jan Ferdinand Sauer <ferdinand@neptune.cash>
Date: Tue, 23 Apr 2024 15:26:05 +0200
Subject: [PATCH] test: assert table-linking arguments' properties
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Computing the terminal of any of the three table-linking arguments
“Permutation Argument”, “Evaluation Argument”, and “Lookup Argument”
corresponds to some function involving polynomials. Test that this
correspondence holds.
---
 triton-vm/src/table/cross_table_argument.rs | 53 +++++++++++++++++++++
 1 file changed, 53 insertions(+)

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<BFieldElement>,
+        #[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<BFieldElement>,
+        #[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<BFieldElement>,
+        #[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);
+    }
+}