From 5d902c6f47a3260eceaada5ea66a4597f56357ae Mon Sep 17 00:00:00 2001 From: sorawee Date: Tue, 22 Aug 2023 13:08:36 -0700 Subject: [PATCH] Restructure counterexample output format for readability (#5) 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 ``` --- README.md | 18 ++++-- ansi.rkt | 9 +++ picus-dpvl-uniqueness.rkt | 46 ++++++++++++++-- picus/algorithms/dpvl.rkt | 112 +++++++++++++++++++++++++------------- 4 files changed, 137 insertions(+), 48 deletions(-) create mode 100644 ansi.rkt diff --git a/README.md b/README.md index cd02e77..609a3f2 100644 --- 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 #. # 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. diff --git a/ansi.rkt b/ansi.rkt new file mode 100644 index 0000000..5512a05 --- /dev/null +++ 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 index 9c93f40..09f1768 100644 --- 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 arg-verbose 0) + (format-cex "other bindings" (order other-info)))) diff --git a/picus/algorithms/dpvl.rkt b/picus/algorithms/dpvl.rkt index a0a301d..6be60f0 100644 --- 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,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. + [(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 or y, + ;; 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): @@ -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 @@ -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) @@ -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) -) \ No newline at end of file + (values ret0 rks rus mapped-info))