|
|
|---|
|
|
|
|---|
Check whether a valuation satisfies a list of R1CS constraints
;; Check whether the valuation satisfies all of the constraints. (defun r1cs-constraints-holdp (constraints valuation prime) (declare (xargs :guard (and (primep prime) (r1cs-constraint-listp constraints) (r1cs-valuationp valuation prime) (good-r1cs-constraint-listp constraints (strip-cars valuation))))) (if (endp constraints) t (and (r1cs-constraint-holdsp (first constraints) valuation prime) (r1cs-constraints-holdp (rest constraints) valuation prime))))