R1cs-constraint-holdsp
Check whether a valuation satisfies an R1CS constraint
;; Check whether the VALUATION satisfies the CONSTRAINT.
(defund r1cs-constraint-holdsp (constraint valuation prime)
(declare (xargs :guard (and (primep prime)
(r1cs-constraintp constraint)
(r1cs-valuationp valuation prime)
(good-r1cs-constraintp constraint (strip-cars valuation)))))
;; The constraint is (a dot x) * (b dot x) - (c dot x) = 0, where x contains
;; a single constant 1 followed by the values of the variables. This is
;; equivalent to (a dot x) * (b dot x) = (c dot x).
(equal (mul (dot-product (r1cs-constraint->a constraint)
valuation
prime)
(dot-product (r1cs-constraint->b constraint)
valuation
prime)
prime)
(dot-product (r1cs-constraint->c constraint)
valuation
prime)))
