From 4554ef5035d7132023f837248cdab41752bc048b Mon Sep 17 00:00:00 2001 From: chyanju Date: Thu, 9 Mar 2023 00:38:37 -0800 Subject: [PATCH] AE sort out and updates --- README.md | 311 ++- logs/new-logs-11-2|10.zip | Bin 11634589 -> 0 bytes logs/new-logs-2202.zip | Bin 11176891 -> 0 bytes picus-dpvl-uniqueness.rkt | 9 +- picus-raw-uniqueness.rkt | 141 -- picus/algorithms/cex.rkt | 2 +- picus/algorithms/dpvl.rkt | 11 +- resources/Dockerfile@base | 3 + .../batch-run-ecne-pre.sh | 0 .../batch-run-ecne.sh | 0 scripts/batch-run-picus-noprop.sh | 27 + scripts/batch-run-picus-nosolve.sh | 27 + .../batch-run-picus-pre.sh | 0 .../batch-run-picus.sh | 0 scripts/parse-results.ipynb | 596 +++++ scripts/parse-results.py | 485 ++++ tests/.keep | 0 tests/BabyAdd-steps/backup/bb.cvc5.smt2 | 88 - tests/BabyAdd-steps/backup/esim.cvc4.smt2 | 114 - tests/BabyAdd-steps/backup/esim.cvc5.smt2 | 133 - tests/BabyAdd-steps/backup/quick1.smt2 | 89 - tests/BabyAdd-steps/backup/quick2.smt2 | 87 - tests/BabyAdd-steps/backup/quick3.smt2 | 90 - tests/BabyAdd-steps/backup/simple.cvc4.smt2 | 114 - tests/BabyAdd-steps/backup/simple.cvc5.smt2 | 179 -- tests/BabyAdd-steps/backup/step0.cvc4.smt2 | 16 - tests/BabyAdd-steps/backup/step1.cvc4.smt2 | 16 - tests/BabyAdd-steps/backup/step2.cvc4.smt2 | 114 - tests/BabyAdd-steps/backup/step2.cvc5.smt2 | 94 - tests/BabyAdd-steps/backup/step3.cvc4.smt2 | 15 - tests/BabyAdd-steps/backup/step4.cvc4.smt2 | 16 - tests/BabyAdd-steps/backup/test0.cvc5.smt2 | 110 - tests/BabyAdd-steps/backup/test1.cvc5.smt2 | 95 - tests/BabyAdd-steps/backup/test2.cvc5.smt2 | 174 -- tests/BabyAdd-steps/backup/try0.cvc5.smt2 | 29 - .../BabyAdd-steps/v1-good-sketch/debug.0.smt2 | 96 - .../BabyAdd-steps/v1-good-sketch/debug.1.smt2 | 92 - .../BabyAdd-steps/v1-good-sketch/debug.2.smt2 | 102 - .../v1-good-sketch/step1-x1-inv0.ff.smt2 | 34 - .../v1-good-sketch/step1-x1-inv1.ff.smt2 | 37 - .../v1-good-sketch/step2-x1-try0.ff.smt2 | 51 - .../v1-good-sketch/step3-x2-inv0.ff.smt2 | 34 - .../v1-good-sketch/step3-x2-inv1.ff.smt2 | 37 - .../v1-good-sketch/step4-x2-try0.ff.smt2 | 108 - .../v2-with-rewrite/debug.0.smt2 | 96 - .../v2-with-rewrite/debug.1.smt2 | 92 - .../v2-with-rewrite/debug.2.smt2 | 102 - .../v2-with-rewrite/step1-x1-inv0.ff.smt2 | 34 - .../v2-with-rewrite/step1-x1-inv1.ff.smt2 | 37 - .../v2-with-rewrite/step2-x1-try0.ff.smt2 | 104 - .../v2-with-rewrite/step3-x2-inv0.ff.smt2 | 34 - .../v2-with-rewrite/step3-x2-inv1.ff.smt2 | 37 - .../v2-with-rewrite/step4-x2-try0.ff.smt2 | 102 - tests/BabyAdd-steps/v3-tidy/step1-x1.ff.smt2 | 80 - tests/BabyAdd-steps/v3-tidy/step2-x2.ff.smt2 | 106 - tests/BabyAdd.exp0.pre.json | 34 - tests/BabyAdd.exp1.pre.json | 54 - tests/BabyAdd.exp2.cvc5.pre.json | 28 - tests/BabyAdd.exp2.z3.pre.json | 34 - tests/BitElementMulAny/be.ff.smt2 | 236 -- tests/BitElementMulAny/be.test.ff.smt2 | 271 -- tests/BitElementMulAny/be0.ff.smt2 | 215 -- tests/BitElementMulAny/be1.ff.smt2 | 226 -- tests/BitElementMulAny/be2.ff.smt2 | 235 -- tests/Montgomery2Edwards.exp1.pre.json | 18 - tests/Montgomery2Edwards.exp1s.pre.json | 21 - tests/Montgomery2Edwards.exp2.pre.json | 10 - tests/Montgomery2Edwards.exp3.pre.json | 10 - tests/Window4-old/circuit.txt | 0 tests/Window4-old/jj.0.ff.smt2 | 596 ----- tests/Window4-old/jj.1.ff.smt2 | 598 ----- tests/Window4-old/w4.0.ff.smt2 | 556 ----- tests/Window4-old/w4.1.ff.smt2 | 571 ----- tests/Window4-old/w4.2.ff.smt2 | 585 ----- tests/Window4-old/w4.3.ff.smt2 | 601 ----- tests/Window4-old/w4.4.ff.smt2 | 616 ----- tests/Window4-old/w4.5.ff.smt2 | 631 ----- tests/Window4-old/w4.6.ff.smt2 | 0 tests/Window4-old/w4.ff.smt2 | 533 ---- tests/Window4-old/w4.n.ff.smt2 | 561 ----- tests/Window4/bb.ff.smt2 | 585 ----- tests/Window4/big.ff.smt2 | 533 ---- tests/Window4/cc.ff.smt2 | 638 ----- tests/Window4/comb0.ff.smt2 | 610 ----- tests/Window4/comb1.ff.smt2 | 638 ----- tests/Window4/comb2.ff.smt2 | 721 ------ tests/Window4/comb3.ff.smt2 | 730 ------ tests/Window4/comb4.ff.smt2 | 731 ------ tests/Window4/counter-example.txt | 198 -- tests/Window4/dd.ff.smt2 | 638 ----- tests/Window4/debug.ff.smt2 | 727 ------ tests/Window4/w4.0.dbl2.ff.smt2 | 581 ----- tests/Window4/w4.1a.adr3.ff.smt2 | 563 ----- tests/Window4/w4.1b.adr3.ff.smt2 | 572 ----- tests/Window4/w4.2a.adr4.ff.smt2 | 568 ----- tests/Window4/w4.2b.adr4.ff.smt2 | 585 ----- tests/Window4/w4.3.adr5.ff.smt2 | 598 ----- tests/Window4/w4.4.adr6.ff.smt2 | 614 ----- tests/Window4/w4.5.adr7.ff.smt2 | 622 ----- tests/Window4/w4.6.adr8.ff.smt2 | 634 ----- tests/Window4/w4.7.mux.ff.smt2 | 717 ------ tests/Window4/w4.8.main.ff.smt2 | 726 ------ tests/Window4/w4.9.verify.ff.smt2 | 727 ------ tests/Window4/w4.ff.smt2 | 533 ---- tests/babyadd0-z3.smt2 | 104 - tests/babydbl0-z3.smt2 | 134 - tests/be0.ff.smt2 | 179 -- tests/binsub0-z3.smt2 | 104 - tests/binsum0-z3.smt2 | 104 - tests/btest0.cvc4.smt2 | 33 - tests/btest0.z3.smt2 | 28 - tests/btest1.cvc4.smt2 | 30 - tests/check0-cvc5.smt2 | 52 - tests/check0-z3.smt2 | 57 - tests/check1-cvc5.smt2 | 53 - tests/check1-z3.smt2 | 58 - tests/decoder-z3.smt2 | 72 - tests/dtest.circom | 45 - tests/e2m0-z3.smt2 | 63 - .../buggy-mix/test-bigmod22.pre.json | 1 - .../circom-ecdsa-d87eb70/bigmod_22.pre.json | 1 - .../circomlib-cff5ab6/AND@gates.pre.json | 1 - .../AliasCheck@aliascheck.pre.json | 1 - .../BabyAdd@babyjub.pre.json | 1 - .../BabyCheck@babyjub.pre.json | 1 - .../BabyDbl@babyjub.pre.json | 1 - .../BabyPbk@babyjub.pre.json | 1 - .../circomlib-cff5ab6/BinSub@binsub.pre.json | 1 - .../circomlib-cff5ab6/BinSum@binsum.pre.json | 1 - .../BitElementMulAny@escalarmulany.pre.json | 1 - .../Bits2Num@bitify.pre.json | 1 - .../Bits2Num_strict@bitify.pre.json | 1 - .../Bits2Point_Strict@pointbits.pre.json | 1 - .../CompConstant@compconstant.pre.json | 1 - .../Decoder@multiplexer.pre.json | 1 - ...iMCSpongeVerifier@eddsamimcsponge.pre.json | 1 - .../EdDSAMiMCVerifier@eddsamimc.pre.json | 1 - ...DSAPoseidonVerifier@eddsaposeidon.pre.json | 1 - .../EdDSAVerifier@eddsa.pre.json | 1 - .../Edwards2Montgomery@montgomery.pre.json | 1 - .../EscalarMulAny@escalarmulany.pre.json | 1 - .../EscalarProduct@multiplexer.pre.json | 1 - .../ForceEqualIfEnabled@comparators.pre.json | 1 - .../GreaterEqThan@comparators.pre.json | 1 - .../GreaterThan@comparators.pre.json | 1 - .../IsEqual@comparators.pre.json | 1 - .../IsZero@comparators.pre.json | 1 - .../LessEqThan@comparators.pre.json | 1 - .../LessThan@comparators.pre.json | 1 - .../circomlib-cff5ab6/MiMC7@mimc.pre.json | 1 - .../MiMCFeistel@mimcsponge.pre.json | 1 - .../MiMCSponge@mimcsponge.pre.json | 1 - .../Montgomery2Edwards@montgomery.pre.json | 1 - .../MontgomeryAdd@montgomery.pre.json | 1 - .../MontgomeryDouble@montgomery.pre.json | 1 - .../circomlib-cff5ab6/MultiAND@gates.pre.json | 1 - .../MultiMiMC7@mimc.pre.json | 1 - .../circomlib-cff5ab6/MultiMux1@mux1.pre.json | 1 - .../circomlib-cff5ab6/MultiMux2@mux2.pre.json | 1 - .../circomlib-cff5ab6/MultiMux3@mux3.pre.json | 1 - .../circomlib-cff5ab6/MultiMux4@mux4.pre.json | 1 - .../Multiplexer@multiplexer.pre.json | 1 - .../Multiplexor2@escalarmulany.pre.json | 1 - .../circomlib-cff5ab6/Mux1@mux1.pre.json | 1 - .../circomlib-cff5ab6/Mux2@mux2.pre.json | 1 - .../circomlib-cff5ab6/Mux3@mux3.pre.json | 1 - .../circomlib-cff5ab6/Mux4@mux4.pre.json | 1 - .../circomlib-cff5ab6/NAND@gates.pre.json | 1 - .../circomlib-cff5ab6/NOR@gates.pre.json | 1 - .../circomlib-cff5ab6/NOT@gates.pre.json | 1 - .../Num2Bits@bitify.pre.json | 1 - .../Num2BitsNeg@bitify.pre.json | 1 - .../Num2Bits_strict@bitify.pre.json | 1 - .../circomlib-cff5ab6/OR@gates.pre.json | 1 - .../Pedersen@pedersen.pre.json | 1 - .../Pedersen@pedersen_old.pre.json | 1 - .../Point2Bits_Strict@pointbits.pre.json | 1 - .../Poseidon@poseidon.pre.json | 1 - .../Segment@pedersen.pre.json | 1 - .../SegmentMulAny@escalarmulany.pre.json | 1 - .../SegmentMulFix@escalarmulfix.pre.json | 1 - .../circomlib-cff5ab6/Sigma@poseidon.pre.json | 1 - .../circomlib-cff5ab6/Sign@sign.pre.json | 1 - .../Switcher@switcher.pre.json | 1 - .../Window4@pedersen.pre.json | 1 - .../WindowMulFix@escalarmulfix.pre.json | 1 - .../circomlib-cff5ab6/XOR@gates.pre.json | 1 - .../AND@gates@circomlib.pre.json | 1 - .../AliasCheck@aliascheck@circomlib.pre.json | 1 - .../BabyAdd@babyjub@circomlib.pre.json | 1 - .../BabyCheck@babyjub@circomlib.pre.json | 1 - .../BabyDbl@babyjub@circomlib.pre.json | 1 - .../BabyPbk@babyjub@circomlib.pre.json | 1 - .../BinSub@binsub@circomlib_16.pre.json | 1 - .../BinSum@binsum@circomlib_32_2.pre.json | 1 - .../BinSum@binsum@circomlib_32_5.pre.json | 1 - ...entMulAny@escalarmulany@circomlib.pre.json | 1 - .../Bits2Num@bitify@circomlib_1.pre.json | 1 - .../Bits2Num@bitify@circomlib_128.pre.json | 1 - .../Bits2Num@bitify@circomlib_16.pre.json | 1 - .../Bits2Num@bitify@circomlib_253.pre.json | 1 - .../Bits2Num@bitify@circomlib_254.pre.json | 1 - .../Bits2Num@bitify@circomlib_256.pre.json | 1 - .../Bits2Num@bitify@circomlib_32.pre.json | 1 - .../Bits2Num@bitify@circomlib_64.pre.json | 1 - .../Bits2Num@bitify@circomlib_8.pre.json | 1 - .../Bits2Num_strict@bitify@circomlib.pre.json | 1 - .../Bits2Point@pointbits@circomlib.pre.json | 1 - ...2Point_Strict@pointbits@circomlib.pre.json | 1 - ...erifier@eddsamimcsponge@circomlib.pre.json | 1 - ...AMiMCVerifier@eddsamimc@circomlib.pre.json | 1 - ...nVerifier@eddsaposeidon@circomlib.pre.json | 1 - ...s2Montgomery@montgomery@circomlib.pre.json | 1 - ...alIfEnabled@comparators@circomlib.pre.json | 1 - ...erEqThan@comparators@circomlib_16.pre.json | 1 - ...erEqThan@comparators@circomlib_32.pre.json | 1 - ...terEqThan@comparators@circomlib_8.pre.json | 1 - ...aterThan@comparators@circomlib_16.pre.json | 1 - ...aterThan@comparators@circomlib_32.pre.json | 1 - ...eaterThan@comparators@circomlib_8.pre.json | 1 - .../IsEqual@comparators@circomlib.pre.json | 1 - .../IsZero@comparators@circomlib.pre.json | 1 - ...ssEqThan@comparators@circomlib_16.pre.json | 1 - ...ssEqThan@comparators@circomlib_32.pre.json | 1 - ...essEqThan@comparators@circomlib_8.pre.json | 1 - .../Main@main@circomlib.pre.json | 1 - ...mery2Edwards@montgomery@circomlib.pre.json | 1 - ...ontgomeryAdd@montgomery@circomlib.pre.json | 1 - ...gomeryDouble@montgomery@circomlib.pre.json | 1 - ...tiplexor2@escalarmulany@circomlib.pre.json | 1 - .../Mux1@mux1@circomlib.pre.json | 1 - .../Mux2@mux2@circomlib.pre.json | 1 - .../Mux3@mux3@circomlib.pre.json | 1 - .../Mux4@mux4@circomlib.pre.json | 1 - .../NAND@gates@circomlib.pre.json | 1 - .../NOR@gates@circomlib.pre.json | 1 - .../NOT@gates@circomlib.pre.json | 1 - .../Num2Bits@bitify@circomlib_1.pre.json | 1 - .../Num2Bits@bitify@circomlib_128.pre.json | 1 - .../Num2Bits@bitify@circomlib_16.pre.json | 1 - .../Num2Bits@bitify@circomlib_253.pre.json | 1 - .../Num2Bits@bitify@circomlib_254.pre.json | 1 - .../Num2Bits@bitify@circomlib_256.pre.json | 1 - .../Num2Bits@bitify@circomlib_32.pre.json | 1 - .../Num2Bits@bitify@circomlib_64.pre.json | 1 - .../Num2Bits@bitify@circomlib_8.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_1.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_128.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_16.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_253.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_254.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_256.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_32.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_64.pre.json | 1 - .../Num2BitsNeg@bitify@circomlib_8.pre.json | 1 - .../Num2Bits_strict@bitify@circomlib.pre.json | 1 - .../OR@gates@circomlib.pre.json | 1 - .../Pedersen@pedersen@circomlib_1.pre.json | 1 - .../Pedersen@pedersen@circomlib_128.pre.json | 1 - .../Pedersen@pedersen@circomlib_16.pre.json | 1 - .../Pedersen@pedersen@circomlib_253.pre.json | 1 - .../Pedersen@pedersen@circomlib_254.pre.json | 1 - .../Pedersen@pedersen@circomlib_256.pre.json | 1 - .../Pedersen@pedersen@circomlib_32.pre.json | 1 - .../Pedersen@pedersen@circomlib_64.pre.json | 1 - .../Pedersen@pedersen@circomlib_8.pre.json | 1 - ...Pedersen@pedersen_old@circomlib_1.pre.json | 1 - ...dersen@pedersen_old@circomlib_128.pre.json | 1 - ...edersen@pedersen_old@circomlib_16.pre.json | 1 - ...dersen@pedersen_old@circomlib_253.pre.json | 1 - ...dersen@pedersen_old@circomlib_254.pre.json | 1 - ...dersen@pedersen_old@circomlib_256.pre.json | 1 - ...edersen@pedersen_old@circomlib_32.pre.json | 1 - ...edersen@pedersen_old@circomlib_64.pre.json | 1 - ...Pedersen@pedersen_old@circomlib_8.pre.json | 1 - .../Point2Bits@pointbits@circomlib.pre.json | 1 - ...t2Bits_Strict@pointbits@circomlib.pre.json | 1 - .../SMTHash1@smthash_mimc@circomlib.pre.json | 1 - ...THash1@smthash_poseidon@circomlib.pre.json | 1 - .../SMTHash2@smthash_mimc@circomlib.pre.json | 1 - ...THash2@smthash_poseidon@circomlib.pre.json | 1 - ...Level@smtprocessorlevel@circomlib.pre.json | 1 - ...cessorSM@smtprocessorsm@circomlib.pre.json | 1 - ...rLevel@smtverifierlevel@circomlib.pre.json | 1 - ...erifierSM@smtverifiersm@circomlib.pre.json | 1 - .../Sha256_2@sha256_2@circomlib.pre.json | 1 - ...ssion@sha256compression@circomlib.pre.json | 1 - .../Sigma@poseidon@circomlib.pre.json | 1 - .../Sigma@poseidon_old@circomlib.pre.json | 1 - .../SigmaPlus@sigmaplus@circomlib.pre.json | 1 - .../Sign@sign@circomlib.pre.json | 1 - .../Switcher@switcher@circomlib.pre.json | 1 - .../T1@t1@circomlib.pre.json | 1 - .../T2@t2@circomlib.pre.json | 1 - .../Window4@pedersen@circomlib.pre.json | 1 - ...dowMulFix@escalarmulfix@circomlib.pre.json | 1 - .../XOR@gates@circomlib.pre.json | 1 - tests/example.pre.json | 35 - tests/geq0.smt2 | 127 - tests/input.json | 1 - tests/iszero0-z3.smt2 | 65 - tests/lemma0.smt2 | 40 - tests/leq0-z3.smt2 | 127 - tests/mini.smt2 | 19 - tests/multiplexer-z3.smt2 | 213 -- tests/num2bits0-z3.smt2 | 75 - tests/old-utils.ipynb | 2169 ----------------- tests/test-e2m.circom | 20 - tests/test-graph0.rkt | 20 - tests/test-graph1.rkt | 50 - tests/test-graph2.rkt | 8 - tests/test-m2e.circom | 20 - tests/test-ma.circom | 26 - tests/test-match.rkt | 9 - tests/test-md.circom | 28 - tests/test-parser-phases.rkt | 16 - tests/test-pre.rkt | 8 - tests/test-regex.rkt | 25 - tests/test0.rkt | 38 - tests/test0.smt2 | 26 - tests/test1.rkt | 37 - tests/test2.rkt | 41 - tests/tt0.smt2 | 93 - tests/utils.ipynb | 1034 -------- 324 files changed, 1374 insertions(+), 30919 deletions(-) delete mode 100644 logs/new-logs-11-2|10.zip delete mode 100644 logs/new-logs-2202.zip delete mode 100644 picus-raw-uniqueness.rkt rename batch-run-ecne-pre.sh => scripts/batch-run-ecne-pre.sh (100%) rename batch-run-ecne.sh => scripts/batch-run-ecne.sh (100%) create mode 100755 scripts/batch-run-picus-noprop.sh create mode 100755 scripts/batch-run-picus-nosolve.sh rename batch-run-picus-pre.sh => scripts/batch-run-picus-pre.sh (100%) rename batch-run-picus.sh => scripts/batch-run-picus.sh (100%) create mode 100644 scripts/parse-results.ipynb create mode 100644 scripts/parse-results.py delete mode 100644 tests/.keep delete mode 100644 tests/BabyAdd-steps/backup/bb.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/esim.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/esim.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/quick1.smt2 delete mode 100644 tests/BabyAdd-steps/backup/quick2.smt2 delete mode 100644 tests/BabyAdd-steps/backup/quick3.smt2 delete mode 100644 tests/BabyAdd-steps/backup/simple.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/simple.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/step0.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/step1.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/step2.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/step2.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/step3.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/step4.cvc4.smt2 delete mode 100644 tests/BabyAdd-steps/backup/test0.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/test1.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/test2.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/backup/try0.cvc5.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/debug.0.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/debug.1.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/debug.2.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/step1-x1-inv0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/step1-x1-inv1.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/step2-x1-try0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/step3-x2-inv0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/step3-x2-inv1.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v1-good-sketch/step4-x2-try0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/debug.0.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/debug.1.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/debug.2.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/step1-x1-inv0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/step1-x1-inv1.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/step2-x1-try0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/step3-x2-inv0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/step3-x2-inv1.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v2-with-rewrite/step4-x2-try0.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v3-tidy/step1-x1.ff.smt2 delete mode 100644 tests/BabyAdd-steps/v3-tidy/step2-x2.ff.smt2 delete mode 100644 tests/BabyAdd.exp0.pre.json delete mode 100644 tests/BabyAdd.exp1.pre.json delete mode 100644 tests/BabyAdd.exp2.cvc5.pre.json delete mode 100644 tests/BabyAdd.exp2.z3.pre.json delete mode 100644 tests/BitElementMulAny/be.ff.smt2 delete mode 100644 tests/BitElementMulAny/be.test.ff.smt2 delete mode 100644 tests/BitElementMulAny/be0.ff.smt2 delete mode 100644 tests/BitElementMulAny/be1.ff.smt2 delete mode 100644 tests/BitElementMulAny/be2.ff.smt2 delete mode 100644 tests/Montgomery2Edwards.exp1.pre.json delete mode 100644 tests/Montgomery2Edwards.exp1s.pre.json delete mode 100644 tests/Montgomery2Edwards.exp2.pre.json delete mode 100644 tests/Montgomery2Edwards.exp3.pre.json delete mode 100644 tests/Window4-old/circuit.txt delete mode 100644 tests/Window4-old/jj.0.ff.smt2 delete mode 100644 tests/Window4-old/jj.1.ff.smt2 delete mode 100644 tests/Window4-old/w4.0.ff.smt2 delete mode 100644 tests/Window4-old/w4.1.ff.smt2 delete mode 100644 tests/Window4-old/w4.2.ff.smt2 delete mode 100644 tests/Window4-old/w4.3.ff.smt2 delete mode 100644 tests/Window4-old/w4.4.ff.smt2 delete mode 100644 tests/Window4-old/w4.5.ff.smt2 delete mode 100644 tests/Window4-old/w4.6.ff.smt2 delete mode 100644 tests/Window4-old/w4.ff.smt2 delete mode 100644 tests/Window4-old/w4.n.ff.smt2 delete mode 100644 tests/Window4/bb.ff.smt2 delete mode 100644 tests/Window4/big.ff.smt2 delete mode 100644 tests/Window4/cc.ff.smt2 delete mode 100644 tests/Window4/comb0.ff.smt2 delete mode 100644 tests/Window4/comb1.ff.smt2 delete mode 100644 tests/Window4/comb2.ff.smt2 delete mode 100644 tests/Window4/comb3.ff.smt2 delete mode 100644 tests/Window4/comb4.ff.smt2 delete mode 100644 tests/Window4/counter-example.txt delete mode 100644 tests/Window4/dd.ff.smt2 delete mode 100644 tests/Window4/debug.ff.smt2 delete mode 100644 tests/Window4/w4.0.dbl2.ff.smt2 delete mode 100644 tests/Window4/w4.1a.adr3.ff.smt2 delete mode 100644 tests/Window4/w4.1b.adr3.ff.smt2 delete mode 100644 tests/Window4/w4.2a.adr4.ff.smt2 delete mode 100644 tests/Window4/w4.2b.adr4.ff.smt2 delete mode 100644 tests/Window4/w4.3.adr5.ff.smt2 delete mode 100644 tests/Window4/w4.4.adr6.ff.smt2 delete mode 100644 tests/Window4/w4.5.adr7.ff.smt2 delete mode 100644 tests/Window4/w4.6.adr8.ff.smt2 delete mode 100644 tests/Window4/w4.7.mux.ff.smt2 delete mode 100644 tests/Window4/w4.8.main.ff.smt2 delete mode 100644 tests/Window4/w4.9.verify.ff.smt2 delete mode 100644 tests/Window4/w4.ff.smt2 delete mode 100644 tests/babyadd0-z3.smt2 delete mode 100644 tests/babydbl0-z3.smt2 delete mode 100644 tests/be0.ff.smt2 delete mode 100644 tests/binsub0-z3.smt2 delete mode 100644 tests/binsum0-z3.smt2 delete mode 100644 tests/btest0.cvc4.smt2 delete mode 100644 tests/btest0.z3.smt2 delete mode 100644 tests/btest1.cvc4.smt2 delete mode 100644 tests/check0-cvc5.smt2 delete mode 100644 tests/check0-z3.smt2 delete mode 100644 tests/check1-cvc5.smt2 delete mode 100644 tests/check1-z3.smt2 delete mode 100644 tests/decoder-z3.smt2 delete mode 100644 tests/dtest.circom delete mode 100644 tests/e2m0-z3.smt2 delete mode 100644 tests/ecne-unique-set/buggy-mix/test-bigmod22.pre.json delete mode 100644 tests/ecne-unique-set/circom-ecdsa-d87eb70/bigmod_22.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/AND@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/AliasCheck@aliascheck.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BabyAdd@babyjub.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BabyCheck@babyjub.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BabyDbl@babyjub.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BabyPbk@babyjub.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BinSub@binsub.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BinSum@binsum.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/BitElementMulAny@escalarmulany.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Bits2Num@bitify.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Bits2Num_strict@bitify.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Bits2Point_Strict@pointbits.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/CompConstant@compconstant.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Decoder@multiplexer.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/EdDSAMiMCSpongeVerifier@eddsamimcsponge.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/EdDSAMiMCVerifier@eddsamimc.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/EdDSAPoseidonVerifier@eddsaposeidon.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/EdDSAVerifier@eddsa.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Edwards2Montgomery@montgomery.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/EscalarMulAny@escalarmulany.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/EscalarProduct@multiplexer.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/ForceEqualIfEnabled@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/GreaterEqThan@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/GreaterThan@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/IsEqual@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/IsZero@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/LessEqThan@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/LessThan@comparators.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MiMC7@mimc.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MiMCFeistel@mimcsponge.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MiMCSponge@mimcsponge.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Montgomery2Edwards@montgomery.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MontgomeryAdd@montgomery.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MontgomeryDouble@montgomery.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MultiAND@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MultiMiMC7@mimc.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MultiMux1@mux1.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MultiMux2@mux2.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MultiMux3@mux3.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/MultiMux4@mux4.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Multiplexer@multiplexer.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Multiplexor2@escalarmulany.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Mux1@mux1.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Mux2@mux2.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Mux3@mux3.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Mux4@mux4.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/NAND@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/NOR@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/NOT@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Num2Bits@bitify.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Num2BitsNeg@bitify.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Num2Bits_strict@bitify.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/OR@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Pedersen@pedersen.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Pedersen@pedersen_old.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Point2Bits_Strict@pointbits.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Poseidon@poseidon.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Segment@pedersen.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/SegmentMulAny@escalarmulany.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/SegmentMulFix@escalarmulfix.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Sigma@poseidon.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Sign@sign.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Switcher@switcher.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/Window4@pedersen.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/WindowMulFix@escalarmulfix.pre.json delete mode 100644 tests/ecne-unique-set/circomlib-cff5ab6/XOR@gates.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/AND@gates@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/AliasCheck@aliascheck@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BabyAdd@babyjub@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BabyCheck@babyjub@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BabyDbl@babyjub@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BabyPbk@babyjub@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BinSub@binsub@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BinSum@binsum@circomlib_32_2.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BinSum@binsum@circomlib_32_5.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/BitElementMulAny@escalarmulany@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_1.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_128.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_253.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_254.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_256.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_64.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num@bitify@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Num_strict@bitify@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Point@pointbits@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Bits2Point_Strict@pointbits@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/EdDSAMiMCSpongeVerifier@eddsamimcsponge@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/EdDSAMiMCVerifier@eddsamimc@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/EdDSAPoseidonVerifier@eddsaposeidon@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Edwards2Montgomery@montgomery@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/ForceEqualIfEnabled@comparators@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/GreaterEqThan@comparators@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/GreaterEqThan@comparators@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/GreaterEqThan@comparators@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/GreaterThan@comparators@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/GreaterThan@comparators@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/GreaterThan@comparators@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/IsEqual@comparators@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/IsZero@comparators@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/LessEqThan@comparators@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/LessEqThan@comparators@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/LessEqThan@comparators@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Main@main@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Montgomery2Edwards@montgomery@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/MontgomeryAdd@montgomery@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/MontgomeryDouble@montgomery@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Multiplexor2@escalarmulany@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Mux1@mux1@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Mux2@mux2@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Mux3@mux3@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Mux4@mux4@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/NAND@gates@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/NOR@gates@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/NOT@gates@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_1.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_128.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_253.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_254.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_256.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_64.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits@bitify@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_1.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_128.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_253.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_254.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_256.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_64.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2BitsNeg@bitify@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Num2Bits_strict@bitify@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/OR@gates@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_1.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_128.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_253.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_254.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_256.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_64.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_1.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_128.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_16.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_253.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_254.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_256.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_32.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_64.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Pedersen@pedersen_old@circomlib_8.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Point2Bits@pointbits@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Point2Bits_Strict@pointbits@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTHash1@smthash_mimc@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTHash1@smthash_poseidon@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTHash2@smthash_mimc@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTHash2@smthash_poseidon@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTProcessorLevel@smtprocessorlevel@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTProcessorSM@smtprocessorsm@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTVerifierLevel@smtverifierlevel@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SMTVerifierSM@smtverifiersm@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Sha256_2@sha256_2@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Sha256compression@sha256compression@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Sigma@poseidon@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Sigma@poseidon_old@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/SigmaPlus@sigmaplus@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Sign@sign@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Switcher@switcher@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/T1@t1@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/T2@t2@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/Window4@pedersen@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/WindowMulFix@escalarmulfix@circomlib.pre.json delete mode 100644 tests/ecne-unique-set/circomlibex-cff5ab6/XOR@gates@circomlib.pre.json delete mode 100644 tests/example.pre.json delete mode 100644 tests/geq0.smt2 delete mode 100644 tests/input.json delete mode 100644 tests/iszero0-z3.smt2 delete mode 100644 tests/lemma0.smt2 delete mode 100644 tests/leq0-z3.smt2 delete mode 100644 tests/mini.smt2 delete mode 100644 tests/multiplexer-z3.smt2 delete mode 100644 tests/num2bits0-z3.smt2 delete mode 100644 tests/old-utils.ipynb delete mode 100644 tests/test-e2m.circom delete mode 100644 tests/test-graph0.rkt delete mode 100644 tests/test-graph1.rkt delete mode 100644 tests/test-graph2.rkt delete mode 100644 tests/test-m2e.circom delete mode 100644 tests/test-ma.circom delete mode 100644 tests/test-match.rkt delete mode 100644 tests/test-md.circom delete mode 100644 tests/test-parser-phases.rkt delete mode 100644 tests/test-pre.rkt delete mode 100644 tests/test-regex.rkt delete mode 100644 tests/test0.rkt delete mode 100644 tests/test0.smt2 delete mode 100644 tests/test1.rkt delete mode 100644 tests/test2.rkt delete mode 100644 tests/tt0.smt2 delete mode 100644 tests/utils.ipynb diff --git a/README.md b/README.md index 5474b40..b26f3c8 100644 --- a/README.md +++ b/README.md @@ -1,19 +1,25 @@ -
-

- - Picus -

-
-Picus is a symbolic virtual machine for automated verification tasks on R1CS. +# Picus -## Building from Docker +Picus is an implementation of the $\mathsf{QED}^2$ tool. + +## Getting Started Guide + +This section provides basic instructions on how to test out the tool for the kick-the-tires phase. We provide pre-built docker image, which is recommended. + +### Building from Docker (Recommended) ```bash docker build -t picus:v0 . docker run -it --rm picus:v0 bash ``` -## Dependencies (Building from Source) +### Building from Source + +You can skip this section if you build the tool from Docker. + +Building from source is not recommended if you just want to quickly run and check the results. Some dependencies require manual building and configuration, which is system specific. One only needs to make sure the following dependencies are satisfied before the tool / basic testing instructions can be executed. + +#### Dependencies - Racket (8.0+): https://racket-lang.org/ - Rosette (4.0+): https://github.com/emina/rosette @@ -37,132 +43,253 @@ docker run -it --rm picus:v0 bash - cvc5-ff: [https://github.com/alex-ozdemir/CVC4/tree/ff](https://github.com/alex-ozdemir/CVC4/tree/ff) - see installation instructions [here](./NOTES.md#installing-cvc5-ff) -## Usage +### Basic Testing Instructions -> Note: Picus is under development, so there are several experimental versions for the purpose of comparison. The larger the version number, the most recent the version. Ideally you should try to use the most recent version. +First change the directory to the repo's root path: -> WIP: Lemmas applied in different versions may be different. We are working on a unified interface to it. +```bash +cd Picus/ +``` + +Then run the script to compile the basic benchmarks: + +```bash +./scripts/prepare-circomlib.sh +``` -### Constraint Preparations +This compiles all the "circomlib-utils" benchmarks, and won't throw any error if the environment is configured successfully. -Note: To run the uniqueness checking on benchmarks included (circom files), you'll need to prepare them (compiling to r1cs files) first, by running: +Then test some benchmarks, e.g., the `Decoder` benchmark, run: ```bash -./script/prepare-??.sh +racket ./picus-dpvl-uniqueness.rkt --solver cvc5 --timeout 5000 --weak --r1cs ./benchmarks/circomlib-cff5ab6/Decoder@multiplexer.r1cs +``` + +A successful run will output logging info ***similar*** to the following (note that actual counter-example could be different due to potential stochastic search strategy in dependant libraries): + ``` +# r1cs file: ./benchmarks/circomlib-cff5ab6/Decoder@multiplexer.r1cs +# timeout: 5000 +# solver: cvc5 +# selector: counter +# precondition: () +# propagation: #t +# smt: #f +# weak: #t +# map: #f +# number of wires: 5 +# number of constraints: 4 +# field size (how many bytes): 32 +# inputs: (0 4). +# outputs: (1 2 3). +# targets: #. +# parsing original r1cs... +# xlist: (x0 x1 x2 x3 x4). +# alt-xlist (x0 y1 y2 y3 x4). +# parsing alternative r1cs... +# configuring precondition... +# unique: #. +# initial known-set # +# initial unknown-set # +# refined known-set: # +# refined unknown-set: # + # propagation (linear lemma): none. + # propagation (binary01 lemma): none. + # propagation (basis2 lemma): none. + # propagation (aboz lemma): none. + # propagation (aboz lemma): none. + # checking: (x1 y1), sat. +# final unknown set #. +# weak uniqueness: unsafe. +# counter-example: + #hash((one . 1) (p . 0) (ps1 . 21888242871839275222246405745257275088548364400416034343698204186575808495616) (ps2 . 21888242871839275222246405745257275088548364400416034343698204186575808495615) (ps3 . 21888242871839275222246405745257275088548364400416034343698204186575808495614) (ps4 . 21888242871839275222246405745257275088548364400416034343698204186575808495613) (ps5 . 21888242871839275222246405745257275088548364400416034343698204186575808495612) (x0 . 0) (x1 . 1) (x2 . 0) (x3 . 1) (x4 . 0) (y1 . 0) (y2 . 0) (y3 . 0) (zero . 0)). +``` + +If you see this, it means the environment that you are operating on is configured successfully. -where `??` corresponds to corresponding benchmark set label. +## Step-by-Step Instructions -### V0: Naive Version +This section will explain how to reproduce all experimental results that support the conclusions in the paper. Please make sure you first of all follow the "Getting Started Guide" and are able to produce all the desired results, before continuing to the rest of this section. -This version directly issues the raw constraints to the solver (with some simple optimizations to the constraints to make it more readable by the user). +This section shows instructions to reproduce results in Table 1, Table 2 and Figure 11, which are the main results of the paper. + +### Experiment Perparation + +We first create a "log" folder to store all the results and outputs generated during the experiment: ```bash -usage: test-v0-uniqueness.rkt [