Dot-product
Dot product of R1CS coefficients and values.
;; Compute the dot product of the vector of coefficients and the vector of
;; values, where each value is either obtained by looking up a variable in the
;; valuation or is the special constant 1. Since the representation is sparse,
;; we map over all the pairs in the vector and take the sum of the
;; corresponding products.
(defund dot-product (vec valuation prime)
(declare (xargs :guard (and (sparse-vectorp vec)
(primep prime)
(r1cs-valuationp valuation prime)
(good-sparse-vectorp vec (strip-cars valuation)))
:verify-guards nil ;done below
))
(if (endp vec)
0
(let* ((item (first vec))
(coeff (first item))
(pseudo-var (second item))
(var-value (if (equal 1 pseudo-var)
1
(lookup-eq pseudo-var valuation))))
(add (mul (mod coeff prime) ;reduce the coefficient mod the prime in case it is, e.g., -1
var-value prime)
(dot-product (rest vec) valuation prime)
prime))))
