		Search-engine friendly clone of the ACL2 documentation.

R1cs-subset

Sr1cs-constraintp

Check if a PFCS constraint is a structured R1CS constraint.

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

If the constraint is an equality, it must be in R1CS form. If the constraint is a relation application, the arguments must be constants or variables: this way, the constraints resulting from the body of the relation, instantiated from the arguments, are in R1CS form if the ones in the body of the relation are.

Definitions and Theorems

Function: sr1cs-constraintp

(defun sr1cs-constraintp (constr)
  (declare (xargs :guard (constraintp constr)))
  (let ((__function__ 'sr1cs-constraintp))
    (declare (ignorable __function__))
    (constraint-case
         constr
         :equal (r1cs-constraintp constr)
         :relation (expression-const/var-listp constr.args))))

Theorem: booleanp-of-sr1cs-constraintp

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

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

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

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

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