cnst gen: always generate full xvec and yvec (#17)

Prior this commit, yvec will reuse input variables from xvec
which is sound because we assume that they are equal anyway.
However, this reusing adds complexity to Picus.
This commit removes the reusing, simplifying the codebase.
The removal should also not affect performance,
since SMT solvers are very good at dealing with equalities.
This also allows modular verification to be programmed more
straightforwardly.

changelogs/unreleased/23-11-10-full-yvec.yaml

@@ -0,0 +1,3 @@
+changed:
+  - Used full yvec in constraint generation,
+    which simplifies the code base.

picus.rkt

@@ -231,17 +231,12 @@
 ; parse original r1cs
 (picus:log-progress "parsing original r1cs...")
 ;; invariant: (length varlist) = nwires
-(define-values (varlist opts defs cnsts) (parse-r1cs r0 '())) ; interpret the constraint system
+(define-values (varlist opts defs cnsts) (parse-r1cs r0 "x")) ; interpret the constraint system
 (picus:log-debug "varlist: ~e" varlist)
 ; parse alternative r1cs
-(define alt-varlist
-  (for/list ([i (in-range nwires)] [var (in-list varlist)])
-    (if (not (utils:contains? input-list i))
-        (format "y~a" i)
-        var)))
-(picus:log-debug "alt-varlist ~e" alt-varlist)
 (picus:log-progress "parsing alternative r1cs...")
-(define-values (_ __ alt-defs alt-cnsts) (parse-r1cs r0 alt-varlist))
+(define-values (alt-varlist __ alt-defs alt-cnsts) (parse-r1cs r0 "y"))
+(picus:log-debug "alt-varlist ~e" alt-varlist)
 
 (picus:log-progress "configuring precondition...")
 (define-values (unique-set precondition)

picus/algorithms/dpvl.rkt

@@ -301,6 +301,15 @@
                output2-info
                other1-info
                other2-info)]
+      ;; skip y<number-id> when <number-id> is in the input set,
+      ;; since it's the same as x<number-id>
+      [(pregexp #px"^y(\\d+)$" (list _ (app string->number n)))
+       #:when (set-member? input-set n)
+       (values input-info
+               output1-info
+               output2-info
+               other1-info
+               other2-info)]
       ;; matching for a variable in the output set. By construction,
       ;; this variable is in the form x<number-id> or y<number-id>,
       ;; where x indicates that it is in the first set
@@ -403,19 +412,14 @@
   (set! :extcnsts extcnsts)
   (set! :skip-query? skip-query?)
 
-  (define alt-varset (list->set :alt-varlist))
-
-  ; keep track of index of varlist (not alt-varlist since that's incomplete)
   (define known-set
-    (for/set ([var (in-list :varlist)]
-              [i (in-naturals)]
-              #:when (set-member? alt-varset var))
+    (for/set ([i (in-range :nwires)]
+              #:when (set-member? :input-set i))
       i))
 
   (define unknown-set
-    (for/set ([var (in-list :varlist)]
-              [i (in-naturals)]
-              #:unless (set-member? alt-varset var))
+    (for/set ([i (in-range :nwires)]
+              #:unless (set-member? :input-set i))
       i))
 
 
@@ -513,10 +517,11 @@
                         #:unit "ms"
                         #:msg "Time spent for solving (gc)")
 
-  ; always skip x0, since it is hard-coded to 1 in the algorithm, but
+  ; always skip x0 and y0, since they are hard-coded to 1 in the algorithm, but
   ; the actual value here might be different, which could be misleading.
   (when (hash? info)
-    (hash-remove! info "x0"))
+    (hash-remove! info "x0")
+    (hash-remove! info "y0"))
 
   (define partitioned-info (sort-vars (partition-vars info input-set output-set)))
 

picus/r1cs/r1cs-cvc5-parser.rkt

@@ -8,11 +8,10 @@
 ; turns r1cs binary form into standard form
 ; arguments:
 ;   - arg-r1cs: r1cs binary form instance using the struct r1cs grammar
-;   - arg-varlist: symbols (in string) to use, usually in "x?" form
-;                  when parsing alt constraints, non-input symbols are replaced with "y?" series
+;   - prefix :: (or/c "x" "y")
 ; returns:
 ;   - (values varlist options declarations constraints)
-(define (parse-r1cs arg-r1cs arg-varlist)
+(define (parse-r1cs arg-r1cs prefix)
 
   ; a list of options
   (define raw-opts
@@ -28,25 +27,14 @@
   ; first create a list of all symbolic variables according to nwires
   (define nwires (r1cs:get-nwires arg-r1cs))
   ; strictly align with wid
-  (define xvec
-    (match arg-varlist
-      ['()
-       ; create fresh new
-       (for/vector ([i nwires]) (format "x~a" i))]
-      [_
-       ; use existing one
-       (list->vector arg-varlist)]))
+  (define varvec (for/vector ([i nwires]) (format "~a~a" prefix i)))
 
   ; add declarations for variables
   (set! raw-decls
         (append raw-decls
                 (list (r1cs:rcmt "======== declaration constraints ========"))
-                (for/list ([x xvec])
-                  (if (and (not (null? arg-varlist)) (string-prefix? x "x"))
-                      ; provided list with already defined x, skip
-                      (r1cs:rcmt (format "~a: already defined" x))
-                      ; otherwise you need to define this variable
-                      (r1cs:rdef (r1cs:rvar (format "~a" x)) (r1cs:rtype "F"))))))
+                (for/list ([x (in-vector varvec)])
+                  (r1cs:rdef (r1cs:rvar x) (r1cs:rtype "F")))))
 
   ; then start creating constraints
   (define m (r1cs:get-mconstraints arg-r1cs))
@@ -82,19 +70,19 @@
         (cons (r1cs:rint 0)
               (for/list ([w0 wids-a] [f0 factors-a])
                 ; (format "(* ~a ~a)" f0 x0)
-                (let ([x0 (vector-ref xvec w0)])
+                (let ([x0 (vector-ref varvec w0)])
                   (r1cs:rmul (list (r1cs:rint f0) (r1cs:rvar x0)))))))
       (define terms-b
         (cons (r1cs:rint 0)
               (for/list ([w0 wids-b] [f0 factors-b])
                 ; (format "(* ~a ~a)" f0 x0)
-                (let ([x0 (vector-ref xvec w0)])
+                (let ([x0 (vector-ref varvec w0)])
                   (r1cs:rmul (list (r1cs:rint f0) (r1cs:rvar x0)))))))
       (define terms-c
         (cons (r1cs:rint 0)
               (for/list ([w0 wids-c] [f0 factors-c])
                 ; (format "(* ~a ~a)" f0 x0)
-                (let ([x0 (vector-ref xvec w0)])
+                (let ([x0 (vector-ref varvec w0)])
                   (r1cs:rmul (list (r1cs:rint f0) (r1cs:rvar x0)))))))
       (define sum-a (r1cs:radd terms-a))
       (define sum-b (r1cs:radd terms-b))
@@ -116,10 +104,10 @@
          sconstraints
          (list (r1cs:rassert
                 (r1cs:req
-                 (r1cs:rint 1) (r1cs:rvar (format "~a" (vector-ref xvec 0))))))))
+                 (r1cs:rint 1) (r1cs:rvar (format "~a" (vector-ref varvec 0))))))))
 
   (values
-   (vector->list xvec)
+   (vector->list varvec)
    (r1cs:rcmds raw-opts)
    (r1cs:rcmds raw-decls)
    (r1cs:rcmds raw-cnsts)))

picus/r1cs/r1cs-z3-parser.rkt

@@ -8,11 +8,10 @@
 ; turns r1cs binary form into standard form
 ; arguments:
 ;   - arg-r1cs: r1cs binary form instance using the struct r1cs grammar
-;   - arg-varlist: symbols (in string) to use, usually in "x?" form
-;                  when parsing alt constraints, non-input symbols are replaced with "y?" series
+;   - prefix :: (or/c "x" "y")
 ; returns:
 ;   - (values varlist options declarations constraints)
-(define (parse-r1cs arg-r1cs arg-varlist)
+(define (parse-r1cs arg-r1cs prefix)
 
   ; a list of options
   (define raw-opts (list (r1cs:rlogic "QF_NIA")))
@@ -23,38 +22,23 @@
   ; first create a list of all symbolic variables according to nwires
   (define nwires (r1cs:get-nwires arg-r1cs))
   ; strictly align with wid
-  (define varvec
-    (match arg-varlist
-      ['()
-       ; create fresh new
-       (for/vector ([i (in-range nwires)]) (format "x~a" i))]
-      [_
-       ; use existing one
-       (list->vector arg-varlist)]))
+  (define varvec (for/vector ([i (in-range nwires)]) (format "~a~a" prefix i)))
 
   ; add declarations for variables
   (set! raw-decls
         (append raw-decls
                 (list (r1cs:rcmt "======== declaration constraints ========"))
                 (for/list ([x (in-vector varvec)])
-                  (if (and (not (null? arg-varlist)) (string-prefix? x "x"))
-                      ; provided list with already defined x, skip
-                      (r1cs:rcmt (format "~a: already defined" x))
-                      ; otherwise you need to define this variable
-                      (r1cs:rdef (r1cs:rvar (format "~a" x)) (r1cs:rtype "Int"))))))
+                  (r1cs:rdef (r1cs:rvar x) (r1cs:rtype "Int")))))
 
   ; add range constraints for declared variables
   (set! raw-decls
         (append raw-decls
                 (list (r1cs:rcmt "======== range constraints ========"))
                 (for/list ([x (in-vector varvec)])
-                  (if (and (not (null? arg-varlist)) (string-prefix? x "x"))
-                      ; provided list with already defined x, skip
-                      (r1cs:rcmt (format "~a: already defined" x))
-                      ; otherwise you need to define this variable
-                      (r1cs:rassert (r1cs:rand (list
-                                                (r1cs:rleq (r1cs:rint 0) (r1cs:rvar (format "~a" x)))
-                                                (r1cs:rlt (r1cs:rvar (format "~a" x)) (r1cs:rint config:p)))))))))
+                  (r1cs:rassert (r1cs:rand (list
+                                            (r1cs:rleq (r1cs:rint 0) (r1cs:rvar x))
+                                            (r1cs:rlt (r1cs:rvar x) (r1cs:rint config:p))))))))
 
   ; then start creating constraints
   (define m (r1cs:get-mconstraints arg-r1cs))