		Search-engine friendly clone of the ACL2 documentation.

R1cs-bridge

R1cs-vec-elem-to-pfcs

Translate an R1CS vector element to a PFCS expression.

Signature
(r1cs-vec-elem-to-pfcs elem) → expr
Returns: expr — Type (expressionp expr).

An element of an R1CS (sparse) vector is a list of two elements: an integer coefficient and a pseudo-variable. If the pseudo-variable is 1, we generate a constant with the coefficient. Otherwise, if the coefficient is 1 and the pseudo-variable is a symbol, we generate a variable with the name of the symbol. Otherwise, we generate a multiplication of the coefficient by the variable.

This mapping works if the R1CS variables have distinct symbol names. Otherwise, different R1CS variables could become the same PFCS variable. We plan to make this mapping more robust at some point.

Definitions and Theorems

Function: r1cs-vec-elem-to-pfcs

(defun r1cs-vec-elem-to-pfcs (elem)
  (declare (xargs :guard (and (true-listp elem)
                              (equal (len elem) 2)
                              (integerp (first elem))
                              (r1cs::pseudo-varp (second elem)))))
  (let ((__function__ 'r1cs-vec-elem-to-pfcs))
    (declare (ignorable __function__))
    (b* ((coeff (first elem))
         (pvar (second elem)))
      (cond ((equal pvar 1)
             (expression-const coeff))
            ((equal coeff 1)
             (expression-var (symbol-name pvar)))
            (t (make-expression-mul
                    :arg1 (expression-const (first elem))
                    :arg2 (expression-var (symbol-name pvar))))))))

Theorem: expressionp-of-r1cs-vec-elem-to-pfcs

(defthm expressionp-of-r1cs-vec-elem-to-pfcs
  (b* ((expr (r1cs-vec-elem-to-pfcs elem)))
    (expressionp expr))
  :rule-classes :rewrite)

Theorem: r1cs-monomialp-of-r1cs-vec-elem-to-pfcs

(defthm r1cs-monomialp-of-r1cs-vec-elem-to-pfcs
  (b* ((expr (r1cs-vec-elem-to-pfcs elem)))
    (r1cs-monomialp expr))
  :rule-classes :rewrite)