diff --git a/README.md b/README.md index 2c8c3d4..6624219 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,9 @@ -# Picus - -
- +
+

+ + Picus +

+
Picus is a symbolic virtual machine for automated verification tasks on R1CS. ## Dependencies @@ -16,14 +18,23 @@ Picus is a symbolic virtual machine for automated verification tasks on R1CS. - Node.js: https://nodejs.org/en/ - for circom parser - Circom 2: https://docs.circom.io/ -- Boolector: https://boolector.github.io/ - - recommended for faster solving, if not, z3 will be used (may be slower) - - ## Commands +```bash +# example test for the r1cs utilities +racket ./test-read-r1cs.rkt --r1cs ./benchmarks/circomlib/EscalarMulAny@escalarmulany.r1cs + +# check uniqueness in one shot +racket ./test-z3-uniqueness.rkt --r1cs ./benchmarks/circomlib/EscalarMulAny@escalarmulany.r1cs + +# check uniqueness using naive slicing +racket ./test-z3-inc-uniqueness.rkt --r1cs ./benchmarks/circomlib/EscalarMulAny@escalarmulany.r1cs ``` + +## Other Commands + +```bash # build circom parser cd circom-parser cargo build @@ -37,20 +48,6 @@ cargo build circom -o ./examples/ ./examples/test10.circom --r1cs --sym circom -o ./benchmarks/ecne/ ./benchmarks/ecne/Num2BitsNeg@bitify.circom --r1cs --sym -# test on ecne example -racket ./run-ecne-equivalence.rkt --cname AND@gates - -# push-button example for equivalence checking -racket ./test-push-button-equivalence.rkt -# turn on error tracing (for debugging) -racket -l errortrace -t ./test-push-button-equivalence.rkt - -# example test for the r1cs utilities -racket ./test-read-r1cs.rkt - -# automatic uniqueness checking -racket ./test-uniqueness.rkt - # grab Ecne's readable constraints only julia --project=. src/gen_benchmark.jl Circom_Functions/benchmarks/bigmod_5_2.r1cs > Circom_Functions/benchmarks/bigmod_5_2.txt @@ -59,12 +56,6 @@ circom -o ./target/ ./ecne_circomlib_tests/ooo.circom --r1cs --sym --O0 julia --project=. src/Ecne.jl --r1cs target/ooo.r1cs --name oooo --sym target/ooo.sym ``` -## Notes - -- The current R1CS parser is a stricter version that only allows 3 sections of type 1, 2 and 3 only. For the parser that complies with the currently very loose spec of R1CS (https://github.com/iden3/r1csfile/blob/master/doc/r1cs_bin_format.md), please see `r1cs-ext.rkt`. To have better control of the prototype, the stricter version is used instead. -- Ecne's wire id starts from 1: https://github.com/franklynwang/EcneProject/blob/master/src/R1CSConstraintSolver.jl#L1683 -- Ecne's readable outputs are "unoptimized". To compare the outputs with Ecne, you need to comment out the "unoptimizing" snippet of Ecne. - ## Resources - Parsing a circuit into AST: https://circom.party/ diff --git a/picus/config.rkt b/picus/config.rkt index 4145743..c0f0c4a 100644 --- a/picus/config.rkt +++ b/picus/config.rkt @@ -6,5 +6,6 @@ ; the global field p as seen in: https://docs.circom.io/circom-language/basic-operators/#field-elements ; also used by ecne as seen in: reference: https://github.com/franklynwang/EcneProject/blob/master/src/R1CSConstraintSolver.jl#L10 (define p 21888242871839275222246405745257275088548364400416034343698204186575808495617) +; (define p 2) (define cap 50000) ; default mhash capacity \ No newline at end of file diff --git a/picus/r1cs-z3-interpreter.rkt b/picus/r1cs-z3-interpreter.rkt new file mode 100644 index 0000000..4383e5c --- /dev/null +++ b/picus/r1cs-z3-interpreter.rkt @@ -0,0 +1,172 @@ +#lang rosette +(require + (prefix-in tokamak: "./tokamak.rkt") + (prefix-in utils: "./utils.rkt") + (prefix-in config: "./config.rkt") + (prefix-in r1cs: "./r1cs.rkt") +) +(provide (rename-out + [interpret-r1cs interpret-r1cs] +)) + +; constants +(define str-zero "0") +(define str-one "1") +; (define p-1 (format "~a" (- config:p 1))) + +; x is factor, and y is x +(define (opt-format-mul x y) + (let ([x0 (format "~a" x)] + [y0 (format "~a" y)]) + (cond + [(|| (equal? "0" x0) (equal? "0" y0)) "0"] + [(&& (equal? "1" x0) (equal? "1" y0)) "1"] + ; [(&& (equal? "x0" x0) (equal? "x0" y0)) "1"] ; inlining x0==1 + [(equal? "1" x0) (format "~a" y0)] + [(equal? "1" y0) (format "~a" x0)] + ; [(equal? "x0" x0) (format "~a" y0)] ; inlining x0==1 + ; [(equal? "x0" y0) (format "~a" x0)] ; inlining x0==1 + [else (format "(* ~a ~a)" x0 y0)] + ) + ) +) + +(define (opt-format-add x y) + (let ([x0 (format "~a" x)] + [y0 (format "~a" y)]) + (cond + [(&& (equal? "0" x0) (equal? "0" y0)) "0"] + [(equal? "0" x0) (format "~a" y0)] + [(equal? "0" y0) (format "~a" x0)] + [else (format "(+ ~a ~a)" x0 y0)] + ) + ) +) + +(define (interpret-r1cs arg-r1cs arg-xlist) + (define raw-smt (list)) ; a list of raw smt strings + + ; first create a list of all symbolic variables according to nwires + (define nwires (r1cs:get-nwires arg-r1cs)) + ; strictly align with wid + (define xlist (if (null? arg-xlist) + ; create fresh new + ; (note) need nwires+1 to account for 1st input + (for/list ([i (+ 1 nwires)]) (format "x~a" i)) + ; use existing one + arg-xlist + )) + ; update smt + (set! raw-smt (append raw-smt + (for/list ([x xlist]) + (if (&& (! (null? arg-xlist)) (string-prefix? x "x")) + ; provided list with already defined x, skip + "" + ; otherwise you need to define this variable + (format "(declare-const ~a Int)\n(assert (<= 0 ~a))\n(assert (< ~a ~a))\n" + x x x config:p) + ) + ) + )) ; update smt + + ; then start creating constraints + (define m (r1cs:get-mconstraints arg-r1cs)) + (define rconstraints (r1cs:get-constraints arg-r1cs)) ; r1cs constraints + + ; symbolic constraints + (define sconstraints (for/list ([cnst rconstraints]) + + ; get block + (define curr-block-a (r1cs:constraint-a cnst)) + (define curr-block-b (r1cs:constraint-b cnst)) + (define curr-block-c (r1cs:constraint-c cnst)) + + ; process block a + (define nnz-a (r1cs:constraint-block-nnz curr-block-a)) + (define wids-a (r1cs:constraint-block-wids curr-block-a)) + (define factors-a (r1cs:constraint-block-factors curr-block-a)) + + ; process block b + (define nnz-b (r1cs:constraint-block-nnz curr-block-b)) + (define wids-b (r1cs:constraint-block-wids curr-block-b)) + (define factors-b (r1cs:constraint-block-factors curr-block-b)) + + ; process block c + (define nnz-c (r1cs:constraint-block-nnz curr-block-c)) + (define wids-c (r1cs:constraint-block-wids curr-block-c)) + (define factors-c (r1cs:constraint-block-factors curr-block-c)) + + ; assemble symbolic terms + ; note that terms could be empty, in which case 0 is used + ; (printf "# wids-a is: ~a\n" wids-a) + (define terms-a (cons str-zero (for/list ([w0 wids-a] [f0 factors-a]) + ; (format "(* ~a ~a)" f0 x0) + ; optimized form + (let ([x0 (list-ref xlist w0)]) + (opt-format-mul f0 x0) + ) + ))) + ; (printf "# wids-b is: ~a\n" wids-b) + (define terms-b (cons str-zero (for/list ([w0 wids-b] [f0 factors-b]) + ; (format "(* ~a ~a)" f0 x0) + ; optimized form + (let ([x0 (list-ref xlist w0)]) + (opt-format-mul f0 x0) + ) + ))) + ; (printf "# wids-c is: ~a\n" wids-c) + (define terms-c (cons str-zero (for/list ([w0 wids-c] [f0 factors-c]) + ; (format "(* ~a ~a)" f0 x0) + ; optimized form + (let ([x0 (list-ref xlist w0)]) + (opt-format-mul f0 x0) + ) + ))) + ; (printf "# done wids\n") + + (define sum-a (foldl opt-format-add "0" terms-a)) + (define sum-b (foldl opt-format-add "0" terms-b)) + (define sum-c (foldl (lambda (v l) (opt-format-add v l)) "0" terms-c)) + ; original form + ; (define ret-cnst (format "(assert (= ~a ~a))\n" + ; (format "(mod ~a ~a)" sum-c config:p) + ; (format "(mod ~a ~a)" + ; (format "(* ~a ~a)" sum-a sum-b) + ; config:p + ; ) + ; )) + ; simplified form + ; (define ret-cnst (format "(assert (= 0 ~a))\n" + ; (format "(mod ~a ~a)" + ; (format "(- (* ~a ~a) ~a)" sum-a sum-b sum-c) + ; config:p + ; ) + ; )) + ; optimized & simplified form + (define ret-cnst (format "(assert (= 0 ~a))\n" + (format "(mod ~a ~a)" + (if (equal? "0" sum-c) + (format "~a" (opt-format-mul sum-a sum-b)) + (format "(- ~a ~a)" (opt-format-mul sum-a sum-b) sum-c) + ) + config:p + ) + )) + + + ; return this assembled constraint + ret-cnst + )) + + ; update smt + (set! raw-smt (append raw-smt sconstraints)) + (set! raw-smt (append raw-smt (list (format "(assert (= 1 ~a))\n" (list-ref xlist 0))))) + + ; return symbolic variable list and symbolic constraint list + ; note that according to r1cs spec, + ; "https://github.com/iden3/r1csfile/blob/master/doc/r1cs_bin_format.md#general-considerations" + ; so we append an additional constraint here + ; see: https://github.com/iden3/r1csfile/blob/master/doc/r1cs_bin_format.md#general-considerations + ; (values xlist sconstraints) + (values xlist raw-smt) +) \ No newline at end of file diff --git a/resources/picus-transparent.png b/resources/picus-transparent.png new file mode 100644 index 0000000..0bf2195 Binary files /dev/null and b/resources/picus-transparent.png differ diff --git a/resources/picus-white.png b/resources/picus-white.png new file mode 100644 index 0000000..189b647 Binary files /dev/null and b/resources/picus-white.png differ diff --git a/test-read-r1cs.rkt b/test-read-r1cs.rkt index 42bb720..6fd1a37 100644 --- a/test-read-r1cs.rkt +++ b/test-read-r1cs.rkt @@ -24,6 +24,6 @@ (define outputs0 (r1cs:r1cs-outputs r0)) (for ([i (range t0)]) (printf "~a\n" (r1cs:r1cs->string r0 i))) (printf "# total constraints: ~a.\n" t0) -(printf "# total number of wires: ~a (+1)\n" (r1cs:get-nwires r0)) -(printf "# inputs: ~a.\n" inputs0) -(printf "# outputs: ~a.\n" outputs0) \ No newline at end of file +(printf "# total number of wires: ~a.\n" (r1cs:get-nwires r0)) +(printf "# inputs: ~a (total: ~a).\n" inputs0 (length inputs0)) +(printf "# outputs: ~a (total: ~a).\n" outputs0 (length outputs0)) \ No newline at end of file diff --git a/test-z3-inc-uniqueness.rkt b/test-z3-inc-uniqueness.rkt new file mode 100644 index 0000000..12adc36 --- /dev/null +++ b/test-z3-inc-uniqueness.rkt @@ -0,0 +1,188 @@ +#lang rosette +(require racket/engine) +(require json rosette/solver/smt/z3 + (prefix-in tokamak: "./picus/tokamak.rkt") + (prefix-in utils: "./picus/utils.rkt") + (prefix-in config: "./picus/config.rkt") + (prefix-in r1cs: "./picus/r1cs.rkt") + (prefix-in rint: "./picus/r1cs-z3-interpreter.rkt") +) + +; solving component +(define (do-solve smt-str timeout #:verbose? [verbose? #f]) + (define temp-folder (find-system-path 'temp-dir)) + (define temp-file (format "picus~a.smt" + (string-replace (format "~a" (current-inexact-milliseconds)) "." ""))) + (define temp-path (build-path temp-folder temp-file)) + (define smt-file (open-output-file temp-path)) + (display smt-str smt-file) + (close-output-port smt-file) + (when verbose? + (printf "# written to: ~a\n" temp-path) + ) + + (when verbose? + (printf "# solving...\n") + ) + (define-values (sp out in err) + ; (note) use `apply` to expand the last argument + (apply subprocess #f #f #f (find-executable-path "z3") (list temp-path)) + ) + (define engine0 (engine (lambda (_) + (define out-str (port->string out)) + (define err-str (port->string err)) + (close-input-port out) + (close-output-port in) + (close-input-port err) + (subprocess-wait sp) + (cons out-str err-str) + ))) + (define eres (engine-run timeout engine0)) + (define esol (engine-result engine0)) + (cond + [(! eres) + ; need to kill the process + (subprocess-kill sp #t) + (cons 'timeout "") + ] + [else + (define out-str (car esol)) + (define err-str (cdr esol)) + (when verbose? + (printf "# stdout:\n~a\n" out-str) + (printf "# stderr:\n~a\n" err-str) + ) + (cond + [(non-empty-string? err-str) (cons 'error err-str)] ; something wrong, not solved + [(string-prefix? out-str "unsat") (cons 'unsat out-str)] + [(string-prefix? out-str "sat") (cons 'sat out-str)] + [(string-prefix? out-str "unknown") (cons 'unknown out-str)] + [else (cons 'else out-str)] + ) + ] + ) +) + +; parse command line arguments +(define arg-r1cs null) +(command-line + #:once-each + [("--r1cs") p-r1cs "path to target r1cs" + (begin + (set! arg-r1cs p-r1cs) + (printf "# r1cs file: ~a\n" arg-r1cs) + (when (! (string-suffix? arg-r1cs ".r1cs")) + (printf "# error: file need to be *.r1cs\n") + (exit 0) + ) + ) + ] +) + +(define r0 (r1cs:read-r1cs arg-r1cs)) + +(define nwires (r1cs:get-nwires r0)) +(printf "# number of wires: ~a (+1)\n" nwires) +(printf "# number of constraints: ~a\n" (r1cs:get-mconstraints r0)) +(printf "# field size (how many bytes): ~a\n" (r1cs:get-field-size r0)) + +(printf "# interpreting original r1cs...\n") +(define-values (xlist original-raw) (rint:interpret-r1cs r0 null)) ; interpret the constraint system +(define input-list (r1cs:r1cs-inputs r0)) +(define output-list (r1cs:r1cs-outputs r0)) +(printf "# inputs: ~a.\n" input-list) +(printf "# outputs: ~a.\n" output-list) +(printf "# xlist: ~a.\n" xlist) +; (printf "# original-raw ~a\n" original-raw) + +; fix inputs, create alternative outputs +; (note) need nwires+1 to account for 1st input +; ======================================= +; output verification (weak verification) +; clara fixed version +; |- create alternative variables for all non-input variables +; |- but restrict output variables as weak verification states +(define xlist0 (for/list ([i (range (+ 1 nwires))]) + (if (not (utils:contains? input-list i)) + (format "y~a" i) + (list-ref xlist i) + ) +)) +(printf "# xlist0: ~a.\n" xlist0) +; then interpret again +(printf "# interpreting alternative r1cs...\n") +(define-values (_ alternative-raw) (rint:interpret-r1cs r0 xlist0)) + +(define partial-raw (append (list "(set-logic QF_NIA)\n") original-raw (list "") alternative-raw (list ""))) +; (define final-str (string-join final-raw "\n")) + +; keep track of index of xlist (not xlist0 since that's incomplete) +(define known-list (filter + (lambda (x) (! (null? x))) + (for/list ([i (range (+ 1 nwires))]) + (if (utils:contains? xlist0 (list-ref xlist i)) + i + null + ) + ) +)) +(define unknown-list (filter + (lambda (x) (! (null? x))) + (for/list ([i (range (+ 1 nwires))]) + (if (utils:contains? xlist0 (list-ref xlist i)) + null + i + ) + ) +)) +(printf "# initial knwon-list: ~a\n" known-list) +(printf "# initial unknown-list: ~a\n" unknown-list) + +; returns final unknown list, and if it's empty, it means all are known +; and thus verified +(define (inc-solve kl ul) + (printf "# ==== new round inc-solve ===\n") + (define tmp-kl (for/list ([i kl]) i)) + (define tmp-ul (list )) + (define changed? #f) + (for ([i ul]) + (printf " # checking: (~a ~a), " (list-ref xlist i) (list-ref xlist0 i)) + (define known-raw (for/list ([j tmp-kl]) + (format "(assert (= ~a ~a))" (list-ref xlist j) (list-ref xlist0 j)) + )) + (define final-raw (append + partial-raw known-raw (list "") + (list (format "(assert (not (= ~a ~a)))" (list-ref xlist i) (list-ref xlist0 i))) (list "") + (list "(check-sat)\n(get-model)") (list "") + )) + (define final-str (string-join final-raw "\n")) + (define res (do-solve final-str 5000)) + (cond + [(equal? 'unsat (car res)) + (printf "verified.\n") + (set! tmp-kl (cons i tmp-kl)) + (set! changed? #t) + ] + [(equal? 'sat (car res)) + (printf "sat.\n") + (set! tmp-ul (cons i tmp-ul)) + ] + [else + (printf "skip.\n") + (set! tmp-ul (cons i tmp-ul)) + ] + ) + ) + ; return + (if changed? + (inc-solve (reverse tmp-kl) (reverse tmp-ul)) + tmp-ul + ) +) + +(define res-ul (inc-solve known-list unknown-list)) +(printf "# final res-ul: ~a\n" res-ul) +(if (empty? res-ul) + (printf "# verified.\n") + (printf "# failed.\n") +) \ No newline at end of file diff --git a/test-z3-uniqueness.rkt b/test-z3-uniqueness.rkt new file mode 100644 index 0000000..073bc19 --- /dev/null +++ b/test-z3-uniqueness.rkt @@ -0,0 +1,133 @@ +#lang rosette +(require racket/engine) +(require json rosette/solver/smt/z3 + (prefix-in tokamak: "./picus/tokamak.rkt") + (prefix-in utils: "./picus/utils.rkt") + (prefix-in config: "./picus/config.rkt") + (prefix-in r1cs: "./picus/r1cs.rkt") + (prefix-in rint: "./picus/r1cs-z3-interpreter.rkt") +) + +; solving component +(define (do-solve smt-str timeout #:verbose? [verbose? #f]) + (define temp-folder (find-system-path 'temp-dir)) + (define temp-file (format "picus~a.smt" + (string-replace (format "~a" (current-inexact-milliseconds)) "." ""))) + (define temp-path (build-path temp-folder temp-file)) + (define smt-file (open-output-file temp-path)) + (display smt-str smt-file) + (close-output-port smt-file) + (when verbose? + (printf "# written to: ~a\n" temp-path) + ) + + (when verbose? + (printf "# solving...\n") + ) + (define-values (sp out in err) + ; (note) use `apply` to expand the last argument + (apply subprocess #f #f #f (find-executable-path "z3") (list temp-path)) + ) + (define engine0 (engine (lambda (_) + (define out-str (port->string out)) + (define err-str (port->string err)) + (close-input-port out) + (close-output-port in) + (close-input-port err) + (subprocess-wait sp) + (cons out-str err-str) + ))) + (define eres (engine-run timeout engine0)) + (define esol (engine-result engine0)) + (cond + [(! eres) + ; need to kill the process + (subprocess-kill sp #t) + (cons 'timeout "") + ] + [else + (define out-str (car esol)) + (define err-str (cdr esol)) + (when verbose? + (printf "# stdout:\n~a\n" out-str) + (printf "# stderr:\n~a\n" err-str) + ) + (cond + [(non-empty-string? err-str) (cons 'error err-str)] ; something wrong, not solved + [(string-prefix? out-str "unsat") (cons 'unsat out-str)] + [(string-prefix? out-str "sat") (cons 'sat out-str)] + [(string-prefix? out-str "unknown") (cons 'unknown out-str)] + [else (cons 'else out-str)] + ) + ] + ) +) + +; parse command line arguments +(define arg-r1cs null) +(command-line + #:once-each + [("--r1cs") p-r1cs "path to target r1cs" + (begin + (set! arg-r1cs p-r1cs) + (printf "# r1cs file: ~a\n" arg-r1cs) + (when (! (string-suffix? arg-r1cs ".r1cs")) + (printf "# error: file need to be *.r1cs\n") + (exit 0) + ) + ) + ] +) + +(define r0 (r1cs:read-r1cs arg-r1cs)) + +(define nwires (r1cs:get-nwires r0)) +(printf "# number of wires: ~a (+1)\n" nwires) +(printf "# number of constraints: ~a\n" (r1cs:get-mconstraints r0)) +(printf "# field size (how many bytes): ~a\n" (r1cs:get-field-size r0)) + +(printf "# interpreting original r1cs...\n") +(define-values (xlist original-raw) (rint:interpret-r1cs r0 null)) ; interpret the constraint system +(define input-list (r1cs:r1cs-inputs r0)) +(define output-list (r1cs:r1cs-outputs r0)) +(printf "# inputs: ~a.\n" input-list) +(printf "# outputs: ~a.\n" output-list) +(printf "# xlist: ~a.\n" xlist) +; (printf "# original-raw ~a\n" original-raw) + +; fix inputs, create alternative outputs +; (note) need nwires+1 to account for 1st input +; ======================================= +; output verification (weak verification) +; clara fixed version +; |- create alternative variables for all non-input variables +; |- but restrict output variables as weak verification states +(define xlist0 (for/list ([i (range (+ 1 nwires))]) + (if (not (utils:contains? input-list i)) + (format "y~a" i) + (list-ref xlist i) + ) +)) +(printf "# xlist0: ~a.\n" xlist0) +; then interpret again +(printf "# interpreting alternative r1cs...\n") +(define-values (_ alternative-raw) (rint:interpret-r1cs r0 xlist0)) +; existence of different valuation of outputs +(define tmp-diff (for/list ([i (range (+ 1 nwires))]) + (if (utils:contains? output-list i) (format "(not (= ~a ~a))" (list-ref xlist i) (list-ref xlist0 i)) null))) +(define diff-list (filter (lambda (x) (! (null? x))) tmp-diff)) +(define diff-raw (list + (string-join diff-list "\n " #:before-first "(assert (or \n " #:after-last "))\n") +)) +; (printf "# diff-raw is:\n~a\n" diff-raw) +; ======================================= + +(define final-raw (append (list "(set-logic QF_NIA)\n") original-raw (list "") alternative-raw (list "") diff-raw (list "(check-sat)\n(get-model)"))) +(define final-str (string-join final-raw "\n")) + +; solve! +(define res (do-solve final-str 10000)) +(if (equal? 'unsat (car res)) + (printf "# verified.\n") + (printf "# failed / reason: ~a\n" res) +) \ No newline at end of file diff --git a/run-test-uniqueness.sh b/tests/run-test-uniqueness.sh similarity index 100% rename from run-test-uniqueness.sh rename to tests/run-test-uniqueness.sh diff --git a/tests/test-inc-uniqueness.rkt b/tests/test-inc-uniqueness.rkt new file mode 100644 index 0000000..78f59af --- /dev/null +++ b/tests/test-inc-uniqueness.rkt @@ -0,0 +1,152 @@ +#lang rosette +(require racket/engine) +(require json rosette/solver/smt/z3 + (prefix-in tokamak: "./picus/tokamak.rkt") + (prefix-in utils: "./picus/utils.rkt") + (prefix-in config: "./picus/config.rkt") + (prefix-in r1cs: "./picus/r1cs.rkt") + (prefix-in rint: "./picus/r1cs-interpreter.rkt") +) +(current-solver (z3 #:logic 'QF_NIA)) +(printf "# using solver: ~a\n" (current-solver)) +(output-smt #t) + +; parse command line arguments +(define arg-r1cs null) +(define arg-range null) +(command-line + #:once-each + [("--r1cs") p-r1cs "path to target r1cs" + (begin + (set! arg-r1cs p-r1cs) + (printf "# r1cs file: ~a\n" arg-r1cs) + (when (! (string-suffix? arg-r1cs ".r1cs")) + (printf "# error: file need to be *.r1cs\n") + (exit 0) + ) + ) + ] + #:once-any + [("--range") "enable range analysis" + (begin + (set! arg-range (string-replace arg-r1cs ".r1cs" ".range.json")) + (printf "# range file: ~a\n" arg-range) + ) + ] +) + +(define r0 (r1cs:read-r1cs arg-r1cs)) +(define j0 (if (null? arg-range) + null + (string->jsexpr (file->string arg-range) #:null null) +)) + +(define nwires (r1cs:get-nwires r0)) +(printf "# number of wires: ~a (+1)\n" nwires) +(printf "# number of constraints: ~a\n" (r1cs:get-mconstraints r0)) +(printf "# field size (how many bytes): ~a\n" (r1cs:get-field-size r0)) + +(printf "# interpreting original r1cs...\n") +(define-values (xlist sconstraints) (rint:interpret-r1cs r0 null)) ; interpret the constraint system +(define input-list (r1cs:r1cs-inputs r0)) +(define output-list (r1cs:r1cs-outputs r0)) +(printf "# inputs: ~a.\n" input-list) +(printf "# outputs: ~a.\n" output-list) +(printf "# xlist: ~a.\n" xlist) + +; uniqueness: for all given inputs, the valuations of all outputs should be unique +; that is, inputs are shared +(define (next-symbolic-integer-alternative) + (define-symbolic* y integer?) + (assert (&& + (>= y 0) + (< y config:p) + )) + y +) + +(define known-list (for/list ([i input-list]) i)) +(define unknown-list (filter + (lambda (x) (! (utils:contains? input-list x))) + (for/list ([i (range (+ 1 nwires))]) i) +)) +(printf "# initial known-list is: ~a\n" known-list) ; known to be unique +(printf "# initial unknown-list is: ~a\n" unknown-list) + +(define xlist0 (for/list ([i (range (+ 1 nwires))]) + (if (not (utils:contains? input-list i)) (next-symbolic-integer-alternative) (list-ref xlist i)))) +(printf "# xlist0: ~a.\n" xlist0) +; then interpret again +(printf "# interpreting alternative r1cs...\n") +(define-values (_ sconstraints0) (rint:interpret-r1cs r0 xlist0)) + +(define (inc-solve kl ind) + ; existence of different valuation of outputs + ; (note) we are using || later, so we need #f for all matching cases + (define dconstraints (for/list ([i (range (+ 1 nwires))]) + (if (utils:contains? kl i) ; no need to equate inputs because they are by construction equal + (= (list-ref xlist i) (list-ref xlist0 i)) ; known to be unique, so equal + #t ; don't know, so no restrictions + ; (note) because we are applying &&, so this should be #t, not #f + ) + )) + + ; target constraints + (define iconstraints (list + (! (= (list-ref xlist ind) (list-ref xlist0 ind))) + )) + + ; query + (define uniqueness-query (&& + (apply && sconstraints) + (apply && sconstraints0) + (apply && dconstraints) + (apply && iconstraints) + )) + + ; solve + (printf "# solving uniqueness for ind=~a...\n" ind) + (printf " # dconstraints: ~a\n" dconstraints) + (printf " # iconstraints: ~a\n" iconstraints) + (define sol (solve (assert uniqueness-query))) + sol +) + +(define (loop-solve kl ul) + (define new-kl (for/list ([v kl]) v)) + (define new-ul (list )) + (printf "# start looping...\n") + (printf "------------------\n") + (for ([ind ul]) + (printf "# curr kl is: ~a\n" new-kl) + (define engine0 (engine (lambda (_) (inc-solve new-kl ind)))) + (define eres (engine-run 20000 engine0)) + (define sol (engine-result engine0)) + (cond + [(unsat? sol) + ; verified, add to kl + (printf " # verified.\n") + (set! new-kl (cons ind new-kl)) + ] + [(! eres) + (printf " # timeout.\n") + (set! new-ul (cons ind new-ul)) + ] + [else + ; not verified, move on + (printf " # failed.\n") + (set! new-ul (cons ind new-ul)) + ] + ) + ) + + (if (equal? kl new-kl) + ; no changes, end this by returning ul + new-ul + ; has changes, loop again + (loop-solve new-kl new-ul) + ) +) + +(define result (loop-solve known-list unknown-list)) +(printf "# raw result is: ~a\n" result) \ No newline at end of file diff --git a/test-uniqueness.rkt b/tests/test-uniqueness.rkt similarity index 100% rename from test-uniqueness.rkt rename to tests/test-uniqueness.rkt diff --git a/tests/test0.smt b/tests/test0.smt new file mode 100644 index 0000000..b805459 --- /dev/null +++ b/tests/test0.smt @@ -0,0 +1,200 @@ +(set-logic QF_NIA) + +(declare-const x0 Int) +(assert (<= 0 x0)) +(assert (< x0 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x1 Int) +(assert (<= 0 x1)) +(assert (< x1 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x2 Int) +(assert (<= 0 x2)) +(assert (< x2 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x3 Int) +(assert (<= 0 x3)) +(assert (< x3 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x4 Int) +(assert (<= 0 x4)) +(assert (< x4 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x5 Int) +(assert (<= 0 x5)) +(assert (< x5 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x6 Int) +(assert (<= 0 x6)) +(assert (< x6 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x7 Int) +(assert (<= 0 x7)) +(assert (< x7 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x8 Int) +(assert (<= 0 x8)) +(assert (< x8 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x9 Int) +(assert (<= 0 x9)) +(assert (< x9 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x10 Int) +(assert (<= 0 x10)) +(assert (< x10 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x11 Int) +(assert (<= 0 x11)) +(assert (< x11 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x12 Int) +(assert (<= 0 x12)) +(assert (< x12 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x13 Int) +(assert (<= 0 x13)) +(assert (< x13 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x14 Int) +(assert (<= 0 x14)) +(assert (< x14 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x15 Int) +(assert (<= 0 x15)) +(assert (< x15 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x16 Int) +(assert (<= 0 x16)) +(assert (< x16 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x17 Int) +(assert (<= 0 x17)) +(assert (< x17 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x18 Int) +(assert (<= 0 x18)) +(assert (< x18 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x19 Int) +(assert (<= 0 x19)) +(assert (< x19 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x20 Int) +(assert (<= 0 x20)) +(assert (< x20 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x21 Int) +(assert (<= 0 x21)) +(assert (< x21 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(assert (= 0 (mod (- (* (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x12) x11) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x21)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ x5 (+ x4 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x3) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x6)))) x21) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x13)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x5) x3) x12) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x15)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x4) x3) x11) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x17)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ x3 (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x19))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ x13 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x1) (+ x19 (+ x15 x17))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ x9 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x10) (+ x8 (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x7)))) x21) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x14)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x9) x7) x12) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x16)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x8) x7) x11) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x18)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x20) x7)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ x14 (+ x20 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x2) (+ x16 x18))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 1 x0)) + + + +(declare-const y1 Int) +(assert (<= 0 y1)) +(assert (< y1 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y2 Int) +(assert (<= 0 y2)) +(assert (< y2 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + + + + + + + + + + + +(declare-const y13 Int) +(assert (<= 0 y13)) +(assert (< y13 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y14 Int) +(assert (<= 0 y14)) +(assert (< y14 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y15 Int) +(assert (<= 0 y15)) +(assert (< y15 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y16 Int) +(assert (<= 0 y16)) +(assert (< y16 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y17 Int) +(assert (<= 0 y17)) +(assert (< y17 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y18 Int) +(assert (<= 0 y18)) +(assert (< y18 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y19 Int) +(assert (<= 0 y19)) +(assert (< y19 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y20 Int) +(assert (<= 0 y20)) +(assert (< y20 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y21 Int) +(assert (<= 0 y21)) +(assert (< y21 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(assert (= 0 (mod (- (* (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x12) x11) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y21)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ x5 (+ x4 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x3) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x6)))) y21) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y13)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x5) x3) x12) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y15)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x4) x3) x11) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y17)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ x3 (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y19))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ y13 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y1) (+ y19 (+ y15 y17))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ x9 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x10) (+ x8 (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x7)))) y21) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y14)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x9) x7) x12) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y16)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (* (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x8) x7) x11) (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y18)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y20) x7)) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- 0 (+ y14 (+ y20 (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y2) (+ y16 y18))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 1 x0)) + + +(assert (or + (not (= x15 y15)))) + +(check-sat) +(get-model) \ No newline at end of file diff --git a/tests/test1.smt b/tests/test1.smt new file mode 100644 index 0000000..37cafc8 --- /dev/null +++ b/tests/test1.smt @@ -0,0 +1,199 @@ +(declare-const x0 Int) +(assert (<= 0 x0)) +(assert (< x0 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x1 Int) +(assert (<= 0 x1)) +(assert (< x1 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x2 Int) +(assert (<= 0 x2)) +(assert (< x2 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x3 Int) +(assert (<= 0 x3)) +(assert (< x3 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x4 Int) +(assert (<= 0 x4)) +(assert (< x4 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x5 Int) +(assert (<= 0 x5)) +(assert (< x5 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x6 Int) +(assert (<= 0 x6)) +(assert (< x6 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x7 Int) +(assert (<= 0 x7)) +(assert (< x7 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x8 Int) +(assert (<= 0 x8)) +(assert (< x8 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x9 Int) +(assert (<= 0 x9)) +(assert (< x9 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x10 Int) +(assert (<= 0 x10)) +(assert (< x10 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x11 Int) +(assert (<= 0 x11)) +(assert (< x11 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x12 Int) +(assert (<= 0 x12)) +(assert (< x12 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x13 Int) +(assert (<= 0 x13)) +(assert (< x13 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x14 Int) +(assert (<= 0 x14)) +(assert (< x14 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x15 Int) +(assert (<= 0 x15)) +(assert (< x15 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x16 Int) +(assert (<= 0 x16)) +(assert (< x16 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x17 Int) +(assert (<= 0 x17)) +(assert (< x17 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x18 Int) +(assert (<= 0 x18)) +(assert (< x18 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x19 Int) +(assert (<= 0 x19)) +(assert (< x19 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x20 Int) +(assert (<= 0 x20)) +(assert (< x20 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const x21 Int) +(assert (<= 0 x21)) +(assert (< x21 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x12) (+ 0 0)) (+ (* 1 x11) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x21) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 1 x5) (+ (* 1 x4) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x3) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x6) (+ 0 0))))) (+ (* 1 x21) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x13) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x5) (+ (* 1 x3) (+ 0 0))) (+ (* 1 x12) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x15) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x4) (+ (* 1 x3) (+ 0 0))) (+ (* 1 x11) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x17) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 1 x3) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x19) (+ 0 0)))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 1 x13) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x1) (+ (* 1 x19) (+ (* 1 x15) (+ (* 1 x17) (+ 0 0))))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 1 x9) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x10) (+ (* 1 x8) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x7) (+ 0 0))))) (+ (* 1 x21) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x14) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x9) (+ (* 1 x7) (+ 0 0))) (+ (* 1 x12) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x16) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x8) (+ (* 1 x7) (+ 0 0))) (+ (* 1 x11) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x18) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x20) (+ (* 1 x7) (+ 0 0)))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 1 x14) (+ (* 1 x20) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x2) (+ (* 1 x16) (+ (* 1 x18) (+ 0 0))))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 1 x0)) + + + +(declare-const y1 Int) +(assert (<= 0 y1)) +(assert (< y1 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y2 Int) +(assert (<= 0 y2)) +(assert (< y2 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + + + + + + + + + + + +(declare-const y13 Int) +(assert (<= 0 y13)) +(assert (< y13 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y14 Int) +(assert (<= 0 y14)) +(assert (< y14 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y15 Int) +(assert (<= 0 y15)) +(assert (< y15 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y16 Int) +(assert (<= 0 y16)) +(assert (< y16 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y17 Int) +(assert (<= 0 y17)) +(assert (< y17 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y18 Int) +(assert (<= 0 y18)) +(assert (< y18 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y19 Int) +(assert (<= 0 y19)) +(assert (< y19 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y20 Int) +(assert (<= 0 y20)) +(assert (< y20 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(declare-const y21 Int) +(assert (<= 0 y21)) +(assert (< y21 21888242871839275222246405745257275088548364400416034343698204186575808495617)) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x12) (+ 0 0)) (+ (* 1 x11) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y21) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 1 x5) (+ (* 1 x4) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x3) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x6) (+ 0 0))))) (+ (* 1 y21) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y13) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x5) (+ (* 1 x3) (+ 0 0))) (+ (* 1 x12) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y15) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x4) (+ (* 1 x3) (+ 0 0))) (+ (* 1 x11) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y17) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 1 x3) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y19) (+ 0 0)))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 1 y13) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y1) (+ (* 1 y19) (+ (* 1 y15) (+ (* 1 y17) (+ 0 0))))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 1 x9) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x10) (+ (* 1 x8) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x7) (+ 0 0))))) (+ (* 1 y21) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y14) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x9) (+ (* 1 x7) (+ 0 0))) (+ (* 1 x12) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y16) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 x8) (+ (* 1 x7) (+ 0 0))) (+ (* 1 x11) (+ 0 0))) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y18) (+ 0 0))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y20) (+ (* 1 x7) (+ 0 0)))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 0 (mod (- (+ (+ 0 0) (+ 0 0)) (+ (* 1 y14) (+ (* 1 y20) (+ (* 21888242871839275222246405745257275088548364400416034343698204186575808495616 y2) (+ (* 1 y16) (+ (* 1 y18) (+ 0 0))))))) 21888242871839275222246405745257275088548364400416034343698204186575808495617))) + +(assert (= 1 x0)) + + +(assert (or + (not (= x1 y1)) + (not (= x2 y2)))) + +(check-sat) +(get-model) \ No newline at end of file