feat: add accounting logging

picus.rkt

@@ -273,16 +273,24 @@
 ;    | (downstream queries)
 ;   ...
 (define path-sym (string-replace r1cs-path ".r1cs" ".sym"))
-(define-values (res res-ks res-us readable-res-info raw-res-info)
-  (dpvl:apply-algorithm
-   r0 nwires mconstraints
-   input-set output-set target-set
-   varlist opts defs cnsts
-   alt-varlist alt-defs alt-cnsts
-   unique-set precondition ; prior knowledge row
-   arg-selector arg-prop arg-slv arg-timeout path-sym
-   solve interpret-r1cs
-   optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1))
+(picus:log-accounting #:type "started_algorithm")
+(match-define-values ((list res res-ks res-us readable-res-info raw-res-info) cpu real gc)
+  (time-apply (λ ()
+                (dpvl:apply-algorithm
+                 r0 nwires mconstraints
+                 input-set output-set target-set
+                 varlist opts defs cnsts
+                 alt-varlist alt-defs alt-cnsts
+                 unique-set precondition ; prior knowledge row
+                 arg-selector arg-prop arg-slv arg-timeout path-sym
+                 solve interpret-r1cs
+                 optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1))
+              '()))
+(picus:log-accounting #:type "finished_algorithm")
+(picus:log-accounting #:type "algorithm_time"
+                      #:value (list cpu real gc)
+                      #:unit "(ms, ms, ms)"
+                      #:msg "Time spent for main algorithm (cpu, real, gc)")
 (picus:log-debug "raw map: ~a" raw-res-info)
 (picus:log-debug "final unknown set ~e" res-us)
 (picus:log-debug "~a uniqueness: ~a" (if arg-strong "strong" "weak") res)
@@ -304,6 +312,7 @@
 
 (match res
   ['unsafe
+   (picus:log-accounting #:type "finished_with_cex")
    (picus:log-main "The circuit is underconstrained")
    (picus:log-main "Counterexample:")
    (match-define (list in out1 out2 other1 other2)
@@ -320,8 +329,10 @@
        (gen-witness raw-res-info r0)))
    (picus:exit exit-code:unsafe)]
   ['safe
+   (picus:log-accounting #:type "finished_with_guarantee")
    (picus:log-main "The circuit is properly constrained")
    (picus:exit exit-code:safe)]
   ['unknown
+   (picus:log-accounting #:type "finished_wo_cex")
    (picus:log-main "Cannot determine whether the circuit is properly constrained")
    (picus:exit exit-code:unknown)])))

picus/algorithms/dpvl.rkt

@@ -146,6 +146,10 @@
                      'skip]))
   (values solved? (cdr res)))
 
+(define total-cpu 0)
+(define total-real 0)
+(define total-gc 0)
+
 ; select and solve
 ; returns:
 ;   - (values 'normal ks us info)
@@ -161,7 +165,12 @@
     ; else, set not empty, move forward
     [else
      (define sid (apply-selector uspool :weight-map))
-     (define-values (solved? info) (dpvl-solve ks us sid))
+     (match-define-values
+      ((list solved? info) cpu real gc)
+      (time-apply (λ () (dpvl-solve ks us sid)) '()))
+     (set! total-cpu (+ total-cpu cpu))
+     (set! total-real (+ total-real real))
+     (set! total-gc (+ total-gc gc))
      ; send feedback to selector
      (selector-feedback sid solved?)
      (cond
@@ -351,6 +360,10 @@
          ; this is required for the cex module to finalize a non-relevant part, which only requires a trivial model
          #:skip-query? [skip-query? #f])
 
+  (set! total-cpu 0)
+  (set! total-real 0)
+  (set! total-gc 0)
+
   ; first load in all global variables
   (set! :r0 r0)
   (set! :nwires nwires)
@@ -487,6 +500,11 @@
   ; invoke the algorithm iteration
   (define-values (ret0 rks rus info) (dpvl-iterate known-set unknown-set))
 
+  (picus:log-accounting #:type "solving_time"
+                        #:value (list total-cpu total-real total-gc)
+                        #:unit "(ms, ms, ms)"
+                        #:msg "Time spent for solving (cpu, real, gc)")
+
   ; 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)

picus/logging.rkt

@@ -45,10 +45,13 @@
          level:warning
          level:error
          level:critical
+         level:accounting
+         level:progress
 
          ;; non-standard level
          picus:log-main
          picus:log-progress
+         (rename-out [picus:log-accounting* picus:log-accounting])
 
          define/caller)
 
@@ -159,10 +162,14 @@
 (define-picus-level error 40)
 (define-picus-level critical 50)
 
-;; custom level: progress
-(define-picus-level progress 15)
+;; custom levels
+;; note that in SaaS, accounting has level 25 and progress has level 26
+;; but for standalone application, both levels are very noisy,
+;; so we set them below the info level (20).
+(define-picus-level accounting 15)
+(define-picus-level progress 16)
 
-;; from https://docs.python.org/3/library/logging.html#logging-levels
+;; Mostly from https://docs.python.org/3/library/logging.html#logging-levels
 (define-log-function debug)
 (define-log-function info)
 (define-log-function warning)
@@ -173,6 +180,20 @@
 (define-log-function main #:picus info #:rkt info)
 ;; This is for the algorithm progress.
 (define-log-function progress #:rkt debug)
+;; Accounting
+(define-log-function accounting #:rkt debug)
+
+(define/caller (picus:log-accounting* #:type entry-type
+                                      #:unit [entry-unit "unit"]
+                                      #:value [entry-value 1]
+                                      #:msg [msg ""])
+  #:caller caller
+
+  (picus:log-accounting "~a" msg
+                        #:extra (hash 'accounting (hash 'entry_type entry-type
+                                                        'entry_unit entry-unit
+                                                        'entry_value entry-value)
+                                      'caller caller)))
 
 (define/caller (picus:log-exception e) #:caller caller
-  (picus:log-error "~e" (exn->string e) #:extra (hash 'caller caller)))
+  (picus:log-error "exception: ~e" (exn->string e) #:extra (hash 'caller caller)))