Restructure counterexample output format for readability

This commit adds a flag `--verbose` for verbose level, which supplants the flag `--raw-output` (or, previously, `--map`). - When the verbose level is 0 (not verbose), the output is in the circom variable format. - When the verbose level is 1, the output is a mixed between the circom variable format and the r1cs signal format, where we prefer the circom variable format whenever possible. - When the verbose level is 2, the output is always in the r1cs signal format. For `--verbose 0`, the output now has three sections: inputs, first possible outputs, and second possible outputs. For other verbosity level, there could be four sections. The extra section is "other bindings". Entries that are different in the first possible outputs and second possible outputs are further highlighted with ANSI escape sequence. Examples: With `--verbose 0`: ``` # inputs: # m1.main.inp: 0 # first possible outputs: # m1.main.out[0]: 0 # m1.main.out[1]: 0 # m1.main.success: 0 # second possible outputs: # m2.main.out[0]: 1 # m2.main.out[1]: 0 # m2.main.success: 1 ``` With `--verbose 1`: ``` # inputs: # m1.main.inp: 0 # first possible outputs: # m1.main.out[0]: 0 # m1.main.out[1]: 0 # m1.main.success: 0 # second possible outputs: # m2.main.out[0]: 1 # m2.main.out[1]: 0 # m2.main.success: 1 # other bindings: # one: 1 # p: 21888242871839275222246405745257275088548364400416034343698204186575808495617 # ps1: 21888242871839275222246405745257275088548364400416034343698204186575808495616 # ps2: 21888242871839275222246405745257275088548364400416034343698204186575808495615 # ps3: 21888242871839275222246405745257275088548364400416034343698204186575808495614 # ps4: 21888242871839275222246405745257275088548364400416034343698204186575808495613 # ps5: 21888242871839275222246405745257275088548364400416034343698204186575808495612 # zero: 0 ``` With `--verbose 2` ``` # inputs: # x4: 0 # first possible outputs: # x1: 0 # x2: 0 # x3: 0 # second possible outputs: # y1: 1 # y2: 0 # y3: 1 # other bindings: # one: 1 # p: 21888242871839275222246405745257275088548364400416034343698204186575808495617 # ps1: 21888242871839275222246405745257275088548364400416034343698204186575808495616 # ps2: 21888242871839275222246405745257275088548364400416034343698204186575808495615 # ps3: 21888242871839275222246405745257275088548364400416034343698204186575808495614 # ps4: 21888242871839275222246405745257275088548364400416034343698204186575808495613 # ps5: 21888242871839275222246405745257275088548364400416034343698204186575808495612 # zero: 0 ```
Veridise · Aug 21, 2023 · 896f13e · 896f13e
1 parent 65f0ebe
commit 896f13e
Show file tree

Hide file tree

Showing 4 changed files with 131 additions and 48 deletions.
diff --git a/README.md b/README.md
@@ -82,10 +82,11 @@ A successful run will output logging info ***similar*** to the following (note t
 # solver: cvc5
 # selector: counter
 # precondition: ()
-# propagation: #t
+# propagation on: #t
+# solver on: #t
 # smt: #f
 # weak: #t
-# map: #f
+# verbose: 0
 # number of wires: 5
 # number of constraints: 4
 # field size (how many bytes): 32
@@ -110,8 +111,17 @@ A successful run will output logging info ***similar*** to the following (note t
   # checking: (x1 y1), sat.
 # final unknown set #<set: 1 2 3>.
 # weak uniqueness: unsafe.
-# counter-example:
-  #hash((m1.main.inp . 0) (m1.main.out[0] . 0) (m1.main.out[1] . 0) (m1.main.success . 0) (m2.main.out[0] . 1) (m2.main.out[1] . 0) (m2.main.success . 1)).
+# ./benchmarks/circomlib-cff5ab6/[email protected] is underconstrained. Below is a counterexample:
+  # inputs:
+    # m1.main.inp: 0
+  # first possible outputs:
+    # m1.main.out[0]: 0
+    # m1.main.out[1]: 0
+    # m1.main.success: 0
+  # second possible outputs:
+    # m2.main.out[0]: 1
+    # m2.main.out[1]: 0
+    # m2.main.success: 1
 ```
 
 If you see this, it means the environment that you are operating on is configured successfully.

diff --git a/ansi.rkt b/ansi.rkt
@@ -0,0 +1,9 @@
+#lang racket
+
+(provide highlight)
+
+(define (ansi-code code)
+  (format "~a~a" (integer->char #x1b) code))
+
+(define (highlight s)
+  (~a (ansi-code "[33m") s (ansi-code "[0m")))
diff --git a/picus-dpvl-uniqueness.rkt b/picus-dpvl-uniqueness.rkt
@@ -8,6 +8,7 @@
     (prefix-in r1cs: "./picus/r1cs/r1cs-grammar.rkt")
     (prefix-in dpvl: "./picus/algorithms/dpvl.rkt")
     (prefix-in pre: "./picus/precondition.rkt")
+    "ansi.rkt"
 )
 
 ; =====================================
@@ -23,7 +24,7 @@
 (define arg-slv #t)
 (define arg-smt #f)
 (define arg-weak #f)
-(define arg-map #t)
+(define arg-verbose 0)
 (command-line
     #:once-each
     [("--r1cs") p-r1cs "path to target r1cs"
@@ -61,8 +62,15 @@
     [("--weak") "only check weak safety, not strong safety  (default: false)"
         (set! arg-weak #t)
     ]
-    [("--raw-output") "show the raw r1cs signals (default: false / map r1cs signals to circom variables)"
-        (set! arg-map #f)
+    [("--verbose") verbose
+     ["counterexample verbose level (default: 0)"
+      "  0: not verbose; only output with circom variable format"
+      "  1: output with circom variable format when applicable, and r1cs signal format otherwise"
+      "  2: output with r1cs signal format"]
+        (set! arg-verbose
+              (match verbose
+                [(or "0" "1" "2") (string->number verbose)]
+                [_ (tokamak:exit "unrecognized verbose level: ~a" verbose)]))
     ]
 )
 (printf "# r1cs file: ~a\n" arg-r1cs)
@@ -74,7 +82,7 @@
 (printf "# solver on: ~a\n" arg-slv)
 (printf "# smt: ~a\n" arg-smt)
 (printf "# weak: ~a\n" arg-weak)
-(printf "# map: ~a\n" arg-map)
+(printf "# verbose: ~a\n" arg-verbose)
 
 ; =================================================
 ; ======== resolve solver specific methods ========
@@ -160,7 +168,7 @@
     xlist opts defs cnsts
     alt-xlist alt-defs alt-cnsts
     unique-set precondition ; prior knowledge row
-    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-map path-sym
+    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-verbose path-sym
     solve state-smt-path interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
 ))
@@ -169,5 +177,31 @@
     (printf "# weak uniqueness: ~a.\n" res)
     (printf "# strong uniqueness: ~a.\n" res)
 )
+
+;; format-cex :: string?, (listof (pairof string? any/c)), #:diff (listof (pairof string? any/c)) -> void?
+(define (format-cex heading info #:diff [diff info])
+  (printf "  # ~a:\n" heading)
+  (for ([entry (in-list info)] [diff-entry (in-list diff)])
+    (printf (cond
+              [(equal? (cdr entry) (cdr diff-entry))
+               "    # ~a: ~a\n"]
+              [else (highlight "    # ~a: ~a\n")])
+            (car entry) (cdr entry)))
+  (when (empty? info)
+    (printf "    # no ~a\n" heading)))
+
+;; order :: hash? -> (listof (pairof string? any/c))
+(define (order info)
+  (sort (hash->list info) string<? #:key car))
+
 (when (equal? 'unsafe res)
-    (printf "# counter-example:\n  ~a.\n" res-info))
+  (printf "# ~a is underconstrained. Below is a counterexample:\n" arg-r1cs)
+  (match-define (list input-info output1-info output2-info other-info) res-info)
+  (define output1-ordered (order output1-info))
+  (define output2-ordered (order output2-info))
+
+  (format-cex "inputs" (order input-info))
+  (format-cex "first possible outputs" output1-ordered #:diff output2-ordered)
+  (format-cex "second possible outputs" output2-ordered #:diff output1-ordered)
+  (when (> arg-verbose 0)
+    (format-cex "other bindings" (order other-info))))
diff --git a/picus/algorithms/dpvl.rkt b/picus/algorithms/dpvl.rkt
@@ -64,7 +64,6 @@
 (define :arg-slv null)
 (define :arg-timeout null)
 (define :arg-smt null)
-(define :arg-map null)
 
 (define :unique-set null)
 (define :precondition null)
@@ -303,39 +302,61 @@
 )
 
 ; this creates a new hash with r1cs variables replaced by corresponding circom variables
-; (note) this will remove helping variables like "one", "ps?", etc.
-(define (map-to-vars info path-sym)
-    (define rd (csv->list (open-input-file path-sym)))
-    ; create r1cs-id to circom-var mapping
-    (define r2c-map (make-hash (for/list ([p rd])
-        (cons (list-ref p 0) (list-ref p 3))
-    )))
-    (define pinfo (if (list? info) (make-hash) info)) ; patch for info type, fix later
+; (note) when unmappable? is #f, this will remove helping variables like "one", "ps?", etc.
+;; map-to-vars :: (listof hash?), path-string?, #:unmappable? boolean? -> (listof hash?)
+(define (map-to-vars info path-sym #:unmappable? [unmappable? #f])
+  (define rd (csv->list (open-input-file path-sym)))
+  ; create r1cs-id to circom-var mapping
+  (define r2c-map
+    (make-hash (for/list ([p rd]) (cons (list-ref p 0) (list-ref p 3)))))
+  (define (process-subinfo pinfo)
     (define new-info (make-hash))
-    (for ([k (hash-keys pinfo)])
-        (cond
-            [(equal? k "x0") (void)] ; skip since this is a constant
-            [(string-prefix? k "x")
-                (define rid (substring k 1))
-                (define cid (hash-ref r2c-map rid))
-                (define val (hash-ref pinfo k))
-
-                (define sid (format "m1.~a" cid))
-                (hash-set! new-info sid val)
-            ]
-            [(string-prefix? k "y")
-                (define rid (substring k 1))
-                (define cid (hash-ref r2c-map rid))
-                (define val (hash-ref pinfo k))
-
-                (define sid (format "m2.~a" cid))
-                (hash-set! new-info sid val)
-            ]
-            [else (void)] ; skip otherwise
-        )
-    )
-    new-info
-)
+    (for ([(k val) (in-hash pinfo)])
+      (cond
+        [(string-prefix? k "x")
+         (define rid (substring k 1))
+         (define cid (hash-ref r2c-map rid))
+
+         (define sid (format "m1.~a" cid))
+         (hash-set! new-info sid val)]
+        [(string-prefix? k "y")
+         (define rid (substring k 1))
+         (define cid (hash-ref r2c-map rid))
+
+         (define sid (format "m2.~a" cid))
+         (hash-set! new-info sid val)]
+        [else
+         (when unmappable?
+           (hash-set! new-info k val))]))
+    new-info)
+  (map process-subinfo info))
+
+;; partition-vars :: (or/c '() hash?), set?, set? -> (list/c hash? hash? hash? hash?)
+(define (partition-vars info input-set output-set)
+  (define pinfo (if (list? info) (make-hash) info)) ; patch for info type, fix later
+  (for/fold ([input-info (hash)]
+             [output1-info (hash)]
+             [output2-info (hash)]
+             [other-info (hash)]
+             #:result (list input-info output1-info output2-info other-info))
+            ([(k v) (in-hash pinfo)])
+    (match k
+      [(pregexp #px"x(\\d+)" (list _ (app string->number n)))
+       #:when (set-member? input-set n)
+       (values (hash-set input-info k v)
+               output1-info
+               output2-info
+               other-info)]
+      [(pregexp #px"(?:x|y)(\\d+)" (list _ (app string->number n)))
+       #:when (set-member? output-set n)
+       (values input-info
+               (if (string-prefix? k "x") (hash-set output1-info k v) output1-info)
+               (if (string-prefix? k "y") (hash-set output2-info k v) output2-info)
+               other-info)]
+      [_ (values input-info
+                 output1-info
+                 output2-info
+                 (hash-set other-info k v))])))
 
 ; verifies signals in target-set
 ; returns (same as dpvl-iterate):
@@ -348,7 +369,7 @@
     xlist opts defs cnsts
     alt-xlist alt-defs alt-cnsts
     unique-set precondition
-    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-map path-sym
+    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-verbose path-sym
     solve state-smt-path interpret-r1cs
     parse-r1cs optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1
     ; extra constraints, usually from cex module about partial model
@@ -380,7 +401,6 @@
     (set! :arg-slv arg-slv)
     (set! :arg-timeout arg-timeout)
     (set! :arg-smt arg-smt)
-    (set! :arg-map arg-map)
 
     (set! :unique-set unique-set)
     (set! :precondition precondition)
@@ -501,9 +521,19 @@
     ; invoke the algorithm iteration
     (define-values (ret0 rks rus info) (dpvl-iterate known-set unknown-set))
 
+    ; always skip x0, since it is 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"))
+
+    (define partitioned-info (partition-vars info input-set output-set))
+
     ; do a remapping if enabled
-    (set! info (if arg-map (map-to-vars info path-sym) info))
+    (define mapped-info
+      (match arg-verbose
+        [0 (map-to-vars partitioned-info path-sym)]
+        [1 (map-to-vars partitioned-info path-sym #:unmappable? #t)]
+        [2 partitioned-info]))
 
     ; return
-    (values ret0 rks rus info)
-)
+    (values ret0 rks rus mapped-info))