From 0be361708ca207f463fa8663d431e0f5a678b415 Mon Sep 17 00:00:00 2001 From: clararod9 Date: Wed, 31 Aug 2022 15:19:37 -0700 Subject: [PATCH] adding lema basis --- .../optimizers/r1cs-cvc5-simple-optimizer.rkt | 2 + .../r1cs-cvc5-template-optimizer.rkt | 2 + picus/optimizers/r1cs-z3-AB0-optimizer.rkt | 3 ++ picus/optimizers/r1cs-z3-simple-optimizer.rkt | 2 + .../optimizers/r1cs-z3-template-optimizer.rkt | 2 + picus/r1cs-cvc5-interpreter.rkt | 1 + picus/r1cs-grammar.rkt | 2 + picus/r1cs-z3-interpreter.rkt | 2 + test-pp-uniqueness.rkt | 54 ++++++++++++++++++- 9 files changed, 69 insertions(+), 1 deletion(-) diff --git a/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt b/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt index e8ab8c7..356b543 100644 --- a/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt +++ b/picus/optimizers/r1cs-cvc5-simple-optimizer.rkt @@ -151,6 +151,8 @@ (r1cs:ror (for/list ([v vs]) v)) ) ] + [(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))] + [(r1cs:rint v) (cond diff --git a/picus/optimizers/r1cs-cvc5-template-optimizer.rkt b/picus/optimizers/r1cs-cvc5-template-optimizer.rkt index 4ea212a..9f91cb5 100644 --- a/picus/optimizers/r1cs-cvc5-template-optimizer.rkt +++ b/picus/optimizers/r1cs-cvc5-template-optimizer.rkt @@ -32,6 +32,8 @@ [(r1cs:rand vs) (r1cs:rand (for/list ([v vs]) (optimize-r1cs v)))] [(r1cs:ror vs) (r1cs:ror (for/list ([v vs]) (optimize-r1cs v)))] + [(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))] + [(r1cs:rint v) (r1cs:rint v)] [(r1cs:rstr v) (r1cs:rstr v)] [(r1cs:rvar v) (r1cs:rvar v)] diff --git a/picus/optimizers/r1cs-z3-AB0-optimizer.rkt b/picus/optimizers/r1cs-z3-AB0-optimizer.rkt index 7bc3677..df92d10 100644 --- a/picus/optimizers/r1cs-z3-AB0-optimizer.rkt +++ b/picus/optimizers/r1cs-z3-AB0-optimizer.rkt @@ -79,6 +79,9 @@ [(r1cs:rand vs) (r1cs:rand (for/list ([v vs]) (optimize-r1cs v)))] [(r1cs:ror vs) (r1cs:ror (for/list ([v vs]) (optimize-r1cs v)))] + [(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))] + + [(r1cs:rint v) (r1cs:rint v)] [(r1cs:rstr v) (r1cs:rstr v)] [(r1cs:rvar v) (r1cs:rvar v)] diff --git a/picus/optimizers/r1cs-z3-simple-optimizer.rkt b/picus/optimizers/r1cs-z3-simple-optimizer.rkt index bf5274b..41df365 100644 --- a/picus/optimizers/r1cs-z3-simple-optimizer.rkt +++ b/picus/optimizers/r1cs-z3-simple-optimizer.rkt @@ -130,6 +130,8 @@ (r1cs:rand (for/list ([v new-vs]) v)) ) ] + [(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))] + [(r1cs:ror vs) (define new-vs (for/list ([v vs]) (optimize-r1cs v))) ; if there's only one element, extract content directly diff --git a/picus/optimizers/r1cs-z3-template-optimizer.rkt b/picus/optimizers/r1cs-z3-template-optimizer.rkt index 6fbb08c..b88504b 100644 --- a/picus/optimizers/r1cs-z3-template-optimizer.rkt +++ b/picus/optimizers/r1cs-z3-template-optimizer.rkt @@ -32,6 +32,8 @@ [(r1cs:rand vs) (r1cs:rand (for/list ([v vs]) (optimize-r1cs v)))] [(r1cs:ror vs) (r1cs:ror (for/list ([v vs]) (optimize-r1cs v)))] + [(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))] + [(r1cs:rint v) (r1cs:rint v)] [(r1cs:rstr v) (r1cs:rstr v)] [(r1cs:rvar v) (r1cs:rvar v)] diff --git a/picus/r1cs-cvc5-interpreter.rkt b/picus/r1cs-cvc5-interpreter.rkt index dc65d26..2e01f3d 100644 --- a/picus/r1cs-cvc5-interpreter.rkt +++ b/picus/r1cs-cvc5-interpreter.rkt @@ -47,6 +47,7 @@ [(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))] [(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))] + [(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))] [(r1cs:rint v) (format "#f~am~a" v config:p)] [(r1cs:rstr v) v] diff --git a/picus/r1cs-grammar.rkt b/picus/r1cs-grammar.rkt index 8dcdfb5..24c6576 100644 --- a/picus/r1cs-grammar.rkt +++ b/picus/r1cs-grammar.rkt @@ -35,6 +35,8 @@ ; sub-command level (struct rand (vs) #:mutable #:transparent #:reflection-name 'r1cs:rand) ; vs: a list of bools (struct ror (vs) #:mutable #:transparent #:reflection-name 'r1cs:ror) ; vs: a list of bools +(struct rimp (lhs rhs) #:mutable #:transparent #:reflection-name 'r1cs:imp) + ; no rnot here out of simplicity, use neq, or other unequalty instead ; sub-command level (struct radd (vs) #:mutable #:transparent #:reflection-name 'r1cs:radd) ; vs: list diff --git a/picus/r1cs-z3-interpreter.rkt b/picus/r1cs-z3-interpreter.rkt index ef506fe..ef5c9ba 100644 --- a/picus/r1cs-z3-interpreter.rkt +++ b/picus/r1cs-z3-interpreter.rkt @@ -47,6 +47,8 @@ [(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))] [(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))] + [(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))] + [(r1cs:rint v) (format "~a" v)] [(r1cs:rstr v) v] diff --git a/test-pp-uniqueness.rkt b/test-pp-uniqueness.rkt index 6bb7881..a1ced50 100644 --- a/test-pp-uniqueness.rkt +++ b/test-pp-uniqueness.rkt @@ -21,6 +21,7 @@ (prefix-in cvc5-rint: "./picus/r1cs-cvc5-interpreter.rkt") (prefix-in cvc5-parser: "./picus/r1cs-cvc5-parser.rkt") (prefix-in cvc5-osimp: "./picus/optimizers/r1cs-cvc5-simple-optimizer.rkt") + (prefix-in cvc5-brep: "./picus/optimizers/r1cs-cvc5-base-representation-optimizer.rkt") ; note: cvc5 doesn't have AB0 optimizer, use template instead ) @@ -108,10 +109,31 @@ [(equal? "z3" arg-solver) (lambda (x) ( z3-oab0:optimize-r1cs (z3-osimp:optimize-r1cs x) ))] - [(equal? "cvc5" arg-solver) (lambda (x) (cvc5-osimp:optimize-r1cs x))] + [(equal? "cvc5" arg-solver) (lambda (x) + (cvc5-osimp:optimize-r1cs x) + )] [else (tokamak:exit "you can't reach here")] ) ) +(define (optimizer:get-base-representation) + (cond + [(equal? "z3" arg-solver) '()] + [(equal? "cvc5" arg-solver) (lambda (x) + (cvc5-brep:get-base-representations x) + )] + [else (tokamak:exit "you can't reach here")] + ) +) +(define (optimizer:generate-base-representations-constraints) + (cond + [(equal? "z3" arg-solver) '()] + [(equal? "cvc5" arg-solver) (lambda (x y) + (cvc5-brep:generate-base-representations-constraints x y) + )] + [else (tokamak:exit "you can't reach here")] + ) +) + (define (rint:interpret-r1cs) (cond [(equal? "z3" arg-solver) z3-rint:interpret-r1cs] @@ -158,6 +180,23 @@ (printf "# parsing alternative r1cs...\n") (define-values (_ alternative-definitions alternative-cnsts) ((parser:parse-r1cs) r0 xlist0)) +(define optimized-original-cnsts ((optimizer:optimize) original-cnsts)) +(define optimized-alternative-cnsts ((optimizer:optimize) alternative-cnsts)) + +; to generate the constraints checking for base-representations +(define base-representations-original ((optimizer:get-base-representation) optimized-original-cnsts)) +(define base-representations-alternative ((optimizer:get-base-representation) optimized-alternative-cnsts)) +;(printf "# Base representations original: ~a.\n" base-representations-original) +;(printf "# Base representations alternative: ~a.\n" base-representations-alternative) +(define constraints-base-representations + ((optimizer:generate-base-representations-constraints) + base-representations-original + base-representations-alternative + ) +) +(printf "# New constraints: ~a.\n" constraints-base-representations) + + (define partial-cmds (r1cs:append-rcmds (r1cs:rcmds (list (r1cs:rcmt (r1cs:rstr "================================")) @@ -173,6 +212,13 @@ )) alternative-definitions alternative-cnsts + (r1cs:rcmds (list + (r1cs:rcmt (r1cs:rstr "================================")) + (r1cs:rcmt (r1cs:rstr "========= Added lemmas =========")) + (r1cs:rcmt (r1cs:rstr "================================")) + )) + constraints-base-representations + )) ; keep track of index of xlist (not xlist0 since that's incomplete) @@ -252,6 +298,12 @@ )) alternative-definitions (r1cs:get-subset-cmds alternative-cnsts list-c) + (r1cs:rcmds (list + (r1cs:rcmt (r1cs:rstr "================================")) + (r1cs:rcmt (r1cs:rstr "========= Added lemmas =========")) + (r1cs:rcmt (r1cs:rstr "================================")) + )) + constraints-base-representations ) )