R1cs-holdsp
Check whether a valuation satisifies an R1CS.
;; Check whether VALUATION satisifies R1CS.
(defun r1cs-holdsp (r1cs valuation)
(declare (xargs :guard (and (r1csp r1cs)
(r1cs-valuationp valuation (r1cs->prime r1cs))
;; all of the variables in the r1cs should be bound in the valuation
(subsetp-eq (r1cs->vars r1cs) (strip-cars valuation)))
:guard-hints (("Goal" :in-theory (enable r1csp
r1cs->constraints
r1cs->prime
r1cs->vars)))))
(r1cs-constraints-holdp (r1cs->constraints r1cs)
valuation
(r1cs->prime r1cs)))
