chore: adjust behavior of no verbose

.github/workflows/docker-image.yml

@@ -30,7 +30,7 @@ jobs:
         shell: bash # this ensures that pipefail is set
       - name: test expected result
         run: |
-          grep "^# weak uniqueness: unsafe\.$" ./result.out
+          grep "^weak uniqueness: unsafe\.$" ./result.out
 
   test-circom-mode:
     runs-on: ubuntu-latest
@@ -52,7 +52,7 @@ jobs:
         shell: bash # this ensures that pipefail is set
       - name: test expected result
         run: |
-          grep "^# weak uniqueness: unsafe\.$" ./result.out
+          grep "^weak uniqueness: unsafe\.$" ./result.out
 
   # run the full test for cvc5
   test-solve-with-cvc5:

picus.rkt

@@ -71,7 +71,7 @@
  [("--verbose")
   verbose
   ["verbose level (default: 0)"
-   "  0: not verbose; output algorithm computation minimally"
+   "  0: not verbose; only display the final output"
    "  1: output algorithm computation, but display ... when the output is too large"
    "  2: output full algorithm computation"]
   (set-verbose! (match verbose
@@ -154,16 +154,16 @@
     [arg-r1cs (values arg-r1cs (r1cs:read-r1cs arg-r1cs))]
     [else (compile+patch-circom arg-circom arg-patch?)]))
 
-(printf "# r1cs file: ~a\n" r1cs-path)
-(printf "# timeout: ~a\n" arg-timeout)
-(printf "# solver: ~a\n" arg-solver)
-(printf "# selector: ~a\n" arg-selector)
-(printf "# precondition: ~a\n" arg-precondition)
-(printf "# propagation on: ~a\n" arg-prop)
-(printf "# solver on: ~a\n" arg-slv)
-(printf "# smt: ~a\n" arg-smt)
-(printf "# weak: ~a\n" arg-weak)
-(printf "# cex-verbose: ~a\n" arg-cex-verbose)
+(vprintf "r1cs file: ~a\n" r1cs-path)
+(vprintf "timeout: ~a\n" arg-timeout)
+(vprintf "solver: ~a\n" arg-solver)
+(vprintf "selector: ~a\n" arg-selector)
+(vprintf "precondition: ~a\n" arg-precondition)
+(vprintf "propagation on: ~a\n" arg-prop)
+(vprintf "solver on: ~a\n" arg-slv)
+(vprintf "smt: ~a\n" arg-smt)
+(vprintf "weak: ~a\n" arg-weak)
+(vprintf "cex-verbose: ~a\n" arg-cex-verbose)
 
 ; =================================================
 ; ======== resolve solver specific methods ========
@@ -181,10 +181,10 @@
 ; ==================================
 (define nwires (r1cs:get-nwires r0))
 (define mconstraints (r1cs:get-mconstraints r0))
-(printf "# number of wires: ~a\n" nwires)
-(printf "# number of constraints: ~a\n" mconstraints)
-(printf "# field size (how many bytes): ~a\n" (r1cs:get-field-size r0))
-(printf "# prime number: ~a\n" (r1cs:get-prime-number r0))
+(vprintf "number of wires: ~a\n" nwires)
+(vprintf "number of constraints: ~a\n" mconstraints)
+(vprintf "field size (how many bytes): ~a\n" (r1cs:get-field-size r0))
+(vprintf "prime number: ~a\n" (r1cs:get-prime-number r0))
 (config:set-p! (r1cs:get-prime-number r0))
 
 ; categorize signals
@@ -193,31 +193,31 @@
 (define output-list (r1cs:r1cs-outputs r0))
 (define output-set (list->set output-list))
 (define target-set (if arg-weak (list->set output-list) (list->set (range nwires))))
-(printf "# inputs: ~a.\n" input-list)
-(printf "# outputs: ~a.\n" output-list)
-(printf "# targets: ~a.\n" target-set)
+(vprintf "inputs: ~e.\n" input-list)
+(vprintf "outputs: ~e.\n" output-list)
+(vprintf "targets: ~e.\n" target-set)
 
 ; parse original r1cs
-(printf "# parsing original r1cs...\n")
+(vprintf "parsing original r1cs...\n")
 ;; invariant: (length varlist) = nwires
 (define-values (varlist opts defs cnsts) (parse-r1cs r0 '())) ; interpret the constraint system
-(vprintf "# varlist: ~e.\n" varlist)
+(vprintf "varlist: ~e.\n" 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)))
-(vprintf "# alt-varlist ~e.\n" alt-varlist)
-(printf "# parsing alternative r1cs...\n")
+(vprintf "alt-varlist ~e.\n" alt-varlist)
+(vprintf "parsing alternative r1cs...\n")
 (define-values (_ __ alt-defs alt-cnsts) (parse-r1cs r0 alt-varlist))
 
-(printf "# configuring precondition...\n")
+(vprintf "configuring precondition...\n")
 (define-values (unique-set precondition)
   (if (null? arg-precondition)
       (values (set) '())
       (pre:read-precondition arg-precondition))) ; read!
-(printf "# unique: ~a.\n" unique-set)
+(vprintf "unique: ~a.\n" unique-set)
 
 ; ============================
 ; ======== main solve ========
@@ -252,29 +252,27 @@
    arg-selector arg-prop arg-slv arg-timeout arg-smt arg-cex-verbose path-sym
    solve interpret-r1cs
    optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1))
-(printf "# final unknown set ~a.\n" res-us)
-(if arg-weak
-    (printf "# weak uniqueness: ~a.\n" res)
-    (printf "# strong uniqueness: ~a.\n" res))
+(vprintf "final unknown set ~e.\n" res-us)
+(printf "~a uniqueness: ~a.\n" (if arg-weak "weak" "strong") 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)
+  (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")])
+               "    ~a: ~a\n"]
+              [else (highlight "    ~a: ~a\n")])
             (car entry) (cdr entry)))
   (when (empty? info)
-    (printf "    # no ~a\n" heading)))
+    (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 "# ~a is underconstrained. Below is a counterexample:\n" r1cs-path)
+  (printf "~a is underconstrained. Below is a counterexample:\n" r1cs-path)
   (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))

picus/algorithms/dpvl.rkt

@@ -88,7 +88,7 @@
 ;   - (values 'sat info): the given query has a counter-example (not verified)
 ;   - (values 'skip info): the given query times out (small step)
 (define (dpvl-solve ks us sid)
-  (printf "  # checking: (~a ~a), " (vector-ref :varvec sid) (vector-ref :alt-varvec sid))
+  (vprintf "  checking: (~a ~a), " (vector-ref :varvec sid) (vector-ref :alt-varvec sid))
   ; assemble commands
   (define known-cmds
     (r1cs:rcmds
@@ -121,32 +121,32 @@
   (define-values (res smt-path) (:solve final-str :arg-timeout #:output-smt? #f))
   (define solved? (cond
                     [(equal? 'unsat (car res))
-                     (printf "verified.\n")
+                     (vprintf "verified.\n")
                      ; verified, safe
                      'verified]
                     [(equal? 'sat (car res))
                      (cond
                        ; skipping query, whatever sat is good
                        [:skip-query?
-                        (printf "sat (no query).\n")
+                        (vprintf "sat (no query).\n")
                         'sat]
                        ; not skipping query, need to tell variable
                        ; (important) here if the current signal is not a target, it's ok to see a sat
                        [(set-member? :target-set sid)
                         ; the current signal is a target, now there's a counter-example, unsafe
                         ; in pp, this counter-example is valid
-                        (printf "sat.\n")
+                        (vprintf "sat.\n")
                         'sat]
                        [else
                         ; not a target, fine, just skip
-                        (printf "sat but not a target.\n")
+                        (vprintf "sat but not a target.\n")
                         'skip])]
                     [else
-                     (printf "skip.\n")
+                     (vprintf "skip.\n")
                      ; possibly timeout in small step, result is unknown
                      'skip]))
   (when :arg-smt
-    (printf "    # smt path: ~a\n" smt-path))
+    (vprintf "    smt path: ~a\n" smt-path))
   (values solved? (cdr res)))
 
 ; select and solve
@@ -400,14 +400,14 @@
       i))
 
 
-  (vprintf "# initial known-set ~e\n" known-set)
-  (vprintf "# initial unknown-set ~e\n" unknown-set)
+  (vprintf "initial known-set ~e\n" known-set)
+  (vprintf "initial unknown-set ~e\n" unknown-set)
 
   ; (precondition related) incorporate unique-set if unique-set is not an empty set
   (set! known-set (set-union known-set unique-set))
   (set! unknown-set (set-subtract unknown-set unique-set))
-  (vprintf "# refined known-set: ~e\n" known-set)
-  (vprintf "# refined unknown-set: ~e\n" unknown-set)
+  (vprintf "refined known-set: ~e\n" known-set)
+  (vprintf "refined unknown-set: ~e\n" unknown-set)
 
   ; ==== branch out: skip optimization phase 0 and apply expand & normalize ====
   ; computing rcdmap need no ab0 lemma from optimization phase 0

picus/algorithms/lemmas/aboz-lemma.rkt

@@ -19,25 +19,20 @@
 ; its p1cnsts form is different, see process below
 ; (fixme) this implements an inefficient version, could be improved
 
-(require
-    (prefix-in config: "../../config.rkt")
-    (prefix-in tokamak: "../../tokamak.rkt")
-    (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [apply-lemma apply-lemma]
-))
+(require (prefix-in config: "../../config.rkt")
+         (prefix-in tokamak: "../../tokamak.rkt")
+         (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
+         "../../verbose.rkt")
+(provide apply-lemma)
 
 ; recursively apply linear lemma
 (define (apply-lemma ks us p1cnsts range-vec)
-    (printf "  # propagation (aboz lemma): ")
+    (vprintf "  propagation (aboz lemma): ")
     (define-values (tmp-ks tmp-us) (process ks us p1cnsts range-vec))
     (let ([s0 (set-subtract tmp-ks ks)])
         (if (set-empty? s0)
-            (printf "none.\n")
-            (printf "~a added.\n" s0)
-        )
-    )
+            (vprintf "none.\n")
+            (vprintf "~e added.\n" s0)))
 
     ; apply once is enough, return
     (values tmp-ks tmp-us)

picus/algorithms/lemmas/baby-lemma.rkt

@@ -11,27 +11,22 @@
 ;   then x1 and x2 are uniquely determined, so as other intermediate signals
 
 ;  (fixme) currently this lemma implementation is not super efficient
-(require
-    (prefix-in config: "../../config.rkt")
-    (prefix-in tokamak: "../../tokamak.rkt")
-    (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [apply-lemma apply-lemma]
-))
+(require (prefix-in config: "../../config.rkt")
+         (prefix-in tokamak: "../../tokamak.rkt")
+         (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
+         "../../verbose.rkt")
+(provide apply-lemma)
 
 (define (apply-lemma ks us p1cnsts)
-    (printf "  # propagation (baby lemma): ")
+    (vprintf "  propagation (baby lemma): ")
     (define tmp-ks (list->set (set->list ks)))
     (define tmp-us (list->set (set->list us)))
 
     (set!-values (tmp-ks tmp-us) (process tmp-ks tmp-us p1cnsts))
     (let ([s0 (set-subtract tmp-ks ks)])
         (if (set-empty? s0)
-            (printf "none.\n")
-            (printf "~a added.\n" s0)
-        )
-    )
+            (vprintf "none.\n")
+            (vprintf "~e added.\n" s0)))
 
     ; apply once is enough, return
     (values tmp-ks tmp-us)
@@ -333,4 +328,4 @@
         ; otherwise, do not rewrite
         [_ #f]
     )
-)
+)

picus/algorithms/lemmas/basis2-lemma.rkt

@@ -3,25 +3,20 @@
 ;   if z = 2^0 * x0 + 2^1 * x1 + ... + 2^n * xn, and x0, x1, ..., xn are all in {0,1}
 ;   then if z is uniquely determined, so as x0, x1, ..., xn
 ; this requires p1cnsts
-(require
-    (prefix-in config: "../../config.rkt")
-    (prefix-in tokamak: "../../tokamak.rkt")
-    (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [apply-lemma apply-lemma]
-))
+(require (prefix-in config: "../../config.rkt")
+         (prefix-in tokamak: "../../tokamak.rkt")
+         (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
+         "../../verbose.rkt")
+(provide apply-lemma)
 
 ; recursively apply linear lemma
 (define (apply-lemma ks us p1cnsts range-vec)
-    (printf "  # propagation (basis2 lemma): ")
+    (vprintf "  propagation (basis2 lemma): ")
     (define-values (tmp-ks tmp-us) (process ks us p1cnsts range-vec))
     (let ([s0 (set-subtract tmp-ks ks)])
         (if (set-empty? s0)
-            (printf "none.\n")
-            (printf "~a added.\n" s0)
-        )
-    )
+            (vprintf "none.\n")
+            (vprintf "~e added.\n" s0)))
 
     ; apply once is enough, return
     (values tmp-ks tmp-us)

picus/algorithms/lemmas/bim-lemma.rkt

@@ -6,24 +6,20 @@
 ; (fixme) one-take implementation, you need a big fix on this
 ; (fixme) this impelements a special case where b = 0
 (require math
-    (prefix-in config: "../../config.rkt")
-    (prefix-in tokamak: "../../tokamak.rkt")
-    (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
-)
-(provide (rename-out
-    [apply-lemma apply-lemma]
-))
+         (prefix-in config: "../../config.rkt")
+         (prefix-in tokamak: "../../tokamak.rkt")
+         (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
+         "../../verbose.rkt")
+(provide apply-lemma)
 
 ; recursively apply linear lemma
 (define (apply-lemma ks us p1cnsts range-vec)
-    (printf "  # propagation (bim lemma): ")
+    (vprintf "  propagation (bim lemma): ")
     (define-values (tmp-ks tmp-us) (process ks us p1cnsts range-vec))
     (let ([s0 (set-subtract tmp-ks ks)])
         (if (set-empty? s0)
-            (printf "none.\n")
-            (printf "~a added.\n" s0)
-        )
-    )
+            (vprintf "none.\n")
+            (vprintf "~e added.\n" s0)))
 
     ; apply once is enough, return
     (values tmp-ks tmp-us)

picus/algorithms/lemmas/binary01-lemma.rkt

@@ -5,12 +5,13 @@
 ; (note) this lemma currently only applies to {a,b}={0,1}, add support for other values if necessary later
 ; (note) this lemma requires ab0 optimization first, applies on p1cnsts
 (require (prefix-in tokamak: "../../tokamak.rkt")
-         (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt"))
+         (prefix-in r1cs: "../../r1cs/r1cs-grammar.rkt")
+         "../../verbose.rkt")
 (provide apply-lemma)
 
 ; recursively apply linear lemma
 (define (apply-lemma ks us p1cnsts range-vec)
-    (printf "  # propagation (binary01 lemma): ")
+    (vprintf "  propagation (binary01 lemma): ")
 
     (process p1cnsts range-vec)
 
@@ -32,10 +33,8 @@
           [_ (values ks us)])))
     (let ([s0 (set-subtract new-ks ks)])
         (if (set-empty? s0)
-            (printf "none.\n")
-            (printf "~a added.\n" s0)
-        )
-    )
+            (vprintf "none.\n")
+            (vprintf "~e added.\n" s0)))
     ; apply once is enough, return
     (values new-ks new-us)
 )