Sparse-vectorp
Recognize a sparse vector in an R1CS constraint.
;; A sparse vector, represented as a list of pairs where each pair contains a
;; coefficient and a pseudo-var. Pseudo-vars not mentioned have an implicit
;; coefficient of 0.
(defund sparse-vectorp (vec)
(declare (xargs :guard t))
(if (atom vec)
(equal vec nil)
(let ((item (first vec)))
(and (true-listp item)
(= 2 (len item))
;; could say (coefficientp (first item) prime) but then we'd have to
;; pass in the prime:
(integerp (first item))
(pseudo-varp (second item))
(sparse-vectorp (rest vec))))))
