		Search-engine friendly clone of the ACL2 documentation.

R1cs-bridge

R1cs-to-pfcs

Translate an R1CS to a PFCS.

Signature
(r1cs-to-pfcs r1cs) → sys
Arguments: r1cs — Guard (r1cs::r1csp r1cs).
Returns: sys — Type (systemp sys).

An R!CS is formalized as consisting of a prime, a list of variables, and a list of constraints. We translate this to a PFCS with no definitions and whose constraints are the ones of the R1CS (translated). We ignore the prime in the R1CS, because PFCSes do not include primes, syntactically.

Definitions and Theorems

Function: r1cs-to-pfcs

(defun r1cs-to-pfcs (r1cs)
 (declare (xargs :guard (r1cs::r1csp r1cs)))
 (let ((__function__ 'r1cs-to-pfcs))
   (declare (ignorable __function__))
   (make-system
        :definitions nil
        :constraints
        (r1cs-constraints-to-pfcs (r1cs::r1cs->constraints r1cs)))))

Theorem: systemp-of-r1cs-to-pfcs

(defthm systemp-of-r1cs-to-pfcs
  (b* ((sys (r1cs-to-pfcs r1cs)))
    (systemp sys))
  :rule-classes :rewrite)

Theorem: r1cs-systemp-of-r1cs-to-pfcs

(defthm r1cs-systemp-of-r1cs-to-pfcs
  (b* ((sys (r1cs-to-pfcs r1cs)))
    (r1cs-systemp sys))
  :rule-classes :rewrite)