mirror of
https://github.com/Veridise/Picus.git
synced 2026-01-10 22:18:01 -05:00
naive slicing
This commit is contained in:
chyanju
47
README.md
47
README.md
@@ -1,7 +1,9 @@
|
||||
# Picus
|
||||
|
||||
<div align="left"><img src="https://img.shields.io/badge/tokamak-0.1-blueviolet?labelColor=blueviolet&color=3d3d3d"></div>
|
||||
|
||||
<div align="left">
|
||||
<h1>
|
||||
<img src="./resources/picus-white.png" width=50>
|
||||
Picus
|
||||
</h1>
|
||||
</div>
|
||||
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/
|
||||
|
||||
@@ -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
|
||||
172
picus/r1cs-z3-interpreter.rkt
Normal file
172
picus/r1cs-z3-interpreter.rkt
Normal file
@@ -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)
|
||||
)
|
||||
BIN
resources/picus-transparent.png
Normal file
BIN
resources/picus-transparent.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 89 KiB |
BIN
resources/picus-white.png
Normal file
BIN
resources/picus-white.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 103 KiB |
@@ -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)
|
||||
(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))
|
||||
188
test-z3-inc-uniqueness.rkt
Normal file
188
test-z3-inc-uniqueness.rkt
Normal file
@@ -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")
|
||||
)
|
||||
133
test-z3-uniqueness.rkt
Normal file
133
test-z3-uniqueness.rkt
Normal file
@@ -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)
|
||||
)
|
||||
152
tests/test-inc-uniqueness.rkt
Normal file
152
tests/test-inc-uniqueness.rkt
Normal file
@@ -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)
|
||||
200
tests/test0.smt
Normal file
200
tests/test0.smt
Normal file
@@ -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)
|
||||
199
tests/test1.smt
Normal file
199
tests/test1.smt
Normal file
@@ -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)
|
||||
Reference in New Issue
Block a user