Skip to content

Commit

Permalink
Restructure counterexample output format for readability (#5)
Browse files Browse the repository at this point in the history 
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
```
  • Loading branch information
@sorawee
sorawee authored Aug 22, 2023
1 parent 5934bf3 commit 5d902c6
Show file tree
Hide file tree
Showing 4 changed files with 137 additions and 48 deletions.
18 changes: 14 additions & 4 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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/Decoder@multiplexer.r1cs 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.
Expand Down
9 changes: 9 additions & 0 deletions ansi.rkt
View file
Original file line number Diff line number Diff line change
@@ -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")))
46 changes: 40 additions & 6 deletions picus-dpvl-uniqueness.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
)

; =====================================
Expand All @@ -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"
Expand Down Expand Up @@ -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)
Expand All @@ -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 ========
Expand Down Expand Up @@ -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
))
Expand All @@ -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))))
112 changes: 74 additions & 38 deletions picus/algorithms/dpvl.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -303,39 +302,67 @@
)

; 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
;; matching for a variable in the input set. By construction,
;; this variable is in the form x<number-id>.
[(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)]
;; 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
;; and y indicates that it is in the second set.
[(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):
Expand All @@ -348,7 +375,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
Expand Down Expand Up @@ -380,7 +407,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)
Expand Down Expand Up @@ -501,9 +527,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))

0 comments on commit 5d902c6

Please sign in to comment.