		Search-engine friendly clone of the ACL2 documentation.

R1cs-subset

R1cs-constraintp

Check if a PFCS constraint is an R1CS constraint.

Signature
(r1cs-constraintp constr) → yes/no
Arguments: constr — Guard (constraintp constr).
Returns: yes/no — Type (booleanp yes/no).

It must be an equality constraint, whose left side is the product of two R1CS polynomials and whose right side is an R1CS polynomial.

Definitions and Theorems

Function: r1cs-constraintp

(defun r1cs-constraintp (constr)
  (declare (xargs :guard (constraintp constr)))
  (let ((__function__ 'r1cs-constraintp))
    (declare (ignorable __function__))
    (and (constraint-case constr :equal)
         (b* ((left (constraint-equal->left constr))
              (right (constraint-equal->right constr)))
           (and (expression-case left :mul)
                (r1cs-polynomialp (expression-mul->arg1 left))
                (r1cs-polynomialp (expression-mul->arg2 left))
                (r1cs-polynomialp right))))))

Theorem: booleanp-of-r1cs-constraintp

(defthm booleanp-of-r1cs-constraintp
  (b* ((yes/no (r1cs-constraintp constr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: r1cs-constraintp-of-constraint-fix-constr

(defthm r1cs-constraintp-of-constraint-fix-constr
  (equal (r1cs-constraintp (constraint-fix constr))
         (r1cs-constraintp constr)))

Theorem: r1cs-constraintp-constraint-equiv-congruence-on-constr

(defthm r1cs-constraintp-constraint-equiv-congruence-on-constr
  (implies (constraint-equiv constr constr-equiv)
           (equal (r1cs-constraintp constr)
                  (r1cs-constraintp constr-equiv)))
  :rule-classes :congruence)