		Search-engine friendly clone of the ACL2 documentation.

R1cs-bridge

R1cs-constraint-to-pfcs

Translate an R1CS constraint to a PFCS constraint.

Signature
(r1cs-constraint-to-pfcs rconstr) → pconstr
Arguments: rconstr — Guard (r1cs::r1cs-constraintp rconstr).
Returns: pconstr — Type (constraintp pconstr).

We translate this to an equality constraint between (i) the product of a and b and (ii) c.

Definitions and Theorems

Function: r1cs-constraint-to-pfcs

(defun r1cs-constraint-to-pfcs (rconstr)
 (declare (xargs :guard (r1cs::r1cs-constraintp rconstr)))
 (let ((__function__ 'r1cs-constraint-to-pfcs))
   (declare (ignorable __function__))
   (b*
    ((a-expr
          (r1cs-vector-to-pfcs (r1cs::r1cs-constraint->a rconstr)))
     (b-expr
          (r1cs-vector-to-pfcs (r1cs::r1cs-constraint->b rconstr)))
     (c-expr
          (r1cs-vector-to-pfcs (r1cs::r1cs-constraint->c rconstr))))
    (make-constraint-equal :left (make-expression-mul :arg1 a-expr
                                                      :arg2 b-expr)
                           :right c-expr))))

Theorem: constraintp-of-r1cs-constraint-to-pfcs

(defthm constraintp-of-r1cs-constraint-to-pfcs
  (b* ((pconstr (r1cs-constraint-to-pfcs rconstr)))
    (constraintp pconstr))
  :rule-classes :rewrite)

Theorem: r1cs-constraintp-of-r1cs-constraint-to-pfcs

(defthm r1cs-constraintp-of-r1cs-constraint-to-pfcs
  (b* ((pconstr (r1cs-constraint-to-pfcs rconstr)))
    (r1cs-constraintp pconstr))
  :rule-classes :rewrite)