auto-tools
auto-tools copied to clipboard
Failure of tests on fresh checkout (Mac OS X)
I've just started to get this running, and run into a roadblock:
$pip3.7 show z3-solver Name: z3-solver Version: 4.8.7.0 Summary: an efficient SMT solver library Home-page: https://github.com/Z3Prover/z3 Author: The Z3 Theorem Prover Project Author-email: None License: MIT License Location: /usr/local/lib/python3.7/site-packages Requires: Required-by:
`$python3 runAutoGroup.py --sdl schemes/cl04.sdl --config schemes/configCL.py -o TestCL -v
runAutoGroup.py:3: DeprecationWarning: the imp module is deprecated in favour of importlib; see the module's documentation for alternative uses
import imp
runAutoGroup.py:792: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead
startTime = time.clock()
sdl: 1 name := LRSW
sdl: 2 setting := symmetric
sdl: 3
sdl: 4 BEGIN :: types
sdl: 5 x := ZR
sdl: 6 y := ZR
sdl: 7 z := ZR
sdl: 8 END :: types
sdl: 9
sdl: 10
sdl: 11 BEGIN :: func:setup
sdl: 12 input := None
sdl: 13 x := random(ZR)
sdl: 14 y := random(ZR)
sdl: 15
sdl: 16 g := random(G1)
sdl: 17
sdl: 18 assumpKey := list{g, x, y}
sdl: 19
sdl: 20 output := assumpKey
sdl: 21 END :: func:setup
sdl: 22
sdl: 23
sdl: 24 BEGIN :: func:assump
sdl: 25 input := assumpKey
sdl: 26 assumpKey := expand{g, x, y}
sdl: 27 X := (g^x)
sdl: 28 Y := (g^y)
sdl: 29
sdl: 30 assumpVar := list{X, Y}
sdl: 31
sdl: 32 output := assumpVar
sdl: 33 END :: func:assump
reducing size of 'signature'
<=== Assumption Instance Graph ===>
digraph assumption {
g -> Y
g -> X
g
}
<=== Assumption Instance Graph ===> 16 : G1 :=> g := random(G1) , loop :=> False
runAutoGroup.py:794: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead endTime = time.clock() ['reductionCL'] runAutoGroup.py:820: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead startTime = time.clock() sdl: 1 name := cl04 sdl: 2 setting := symmetric sdl: 3 sdl: 4 BEGIN :: types sdl: 5 m := ZR sdl: 6 END :: types sdl: 7 sdl: 8 BEGIN :: func:setup sdl: 9 input := list{assumpKey, assumpVar} sdl: 10 sdl: 11 sdl: 12 x := random(ZR) sdl: 13 y := random(ZR) sdl: 14 g := random(G1) sdl: 15 sdl: 16 X := (g^x) sdl: 17 Y := (g^y) sdl: 18 sdl: 19 reductionKey := list{x, y} sdl: 20 reductionParams := list{p, g, X, Y} sdl: 21 output := list{reductionKey, reductionParams} sdl: 22 END :: func:setup sdl: 23 sdl: 24 sdl: 25 BEGIN :: func:queries sdl: 26 input := list{m, reductionParams, reductionKey} sdl: 27 reductionKey := expand{x, y} sdl: 28 reductionParams := expand{p, g, X, Y} sdl: 29 sdl: 30 r := random(ZR) sdl: 31 a := (g^r) sdl: 32 b := (a^y) sdl: 33 c := (a^(x + ((m * x) * y))) sdl: 34 sdl: 35 sig := list{a, b, c} sdl: 36 sdl: 37 output := sig sdl: 38 END :: func:queries sdl: 39 sdl: 40 reducing size of 'signature' <=== Reduction Setup Graph ===> digraph setup { g g -> X g -> Y }
<=== Reduction Setup Graph ===> <=== Reduction Query Graph (backward) ===> digraph queries { g -> a a -> b a -> c }
<=== Reduction Query Graph (backward) ===> <=== Reduction Graph ===> digraph reduction { g -> Y a -> c a -> b g g -> a g -> X }
<=== Reduction Graph ===> 14 : G1 :=> g := random(G1) , loop :=> False runAutoGroup.py:822: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead endTime = time.clock() runAutoGroup.py:870: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead startTime = time.clock() sdl: 1 name := cl04 sdl: 2 setting := symmetric sdl: 3 sdl: 4 BEGIN :: types sdl: 5 M := Str sdl: 6 END :: types sdl: 7 sdl: 8 BEGIN :: func:setup sdl: 9 input := list{None} sdl: 10 g := random(G1) sdl: 11 output := g sdl: 12 END :: func:setup sdl: 13 sdl: 14 sdl: 15 BEGIN :: func:keygen sdl: 16 input := list{g} sdl: 17 x := random(ZR) sdl: 18 y := random(ZR) sdl: 19 X := (g^x) sdl: 20 Y := (g^y) sdl: 21 sk := list{x, y} sdl: 22 pk := list{X, Y} sdl: 23 output := list{pk, sk} sdl: 24 END :: func:keygen sdl: 25 sdl: 26 sdl: 27 BEGIN :: func:sign sdl: 28 input := list{g, sk, M} sdl: 29 sk := expand{x, y} sdl: 30 r := random(ZR) sdl: 31 m := H(M,ZR) sdl: 32 a := (g^r) sdl: 33 b := (a^y) sdl: 34 c := (a^(x + ((m * x) * y))) sdl: 35 sig := list{a, b, c} sdl: 36 output := sig sdl: 37 END :: func:sign sdl: 38 sdl: 39 sdl: 40 BEGIN :: func:verify sdl: 41 input := list{pk, g, M, sig} sdl: 42 sig := expand{a, b, c} sdl: 43 pk := expand{X, Y} sdl: 44 m := H(M,ZR) sdl: 45 BEGIN :: if sdl: 46 if {{e(a,Y) == e(g,b)} and {(e(X,a) * (e(X,b)^m)) == e(g,c)}} sdl: 47 output := True sdl: 48 else sdl: 49 output := False sdl: 50 END :: if sdl: 51 END :: func:verify sdl: 52 name is cl04 setting is symmetric reducing size of 'signature' 10 : G1 :=> g := random(G1) , loop :=> False Each: if {{e(a,Y) == e(g,b)} and {(e(X,a) * (e(X,b)^m)) == e(g,c)}} <=== Setup Graph ===> digraph setup { }
<=== Setup Graph ===> <=== Keygen Graph ===> digraph keygen { g -> X g -> Y }
<=== Keygen Graph ===> <=== Sign Graph ===> digraph sign { g -> a a -> b a -> c }
<=== Sign Graph ===> <=== Verify Graph ===> digraph verify { a -> "P1[0]" Y -> "P1[1]" g -> "P2[0]" b -> "P2[1]" X -> "P3[0]" a -> "P3[1]" X -> "P4[0]" b -> "P4[1]" g -> "P5[0]" c -> "P5[1]" }
<=== Verify Graph ===> <=== Scheme Graph ===> digraph cl04 { g -> Y a -> c a -> b X -> "P3[0]" g -> "P5[0]" a -> "P1[0]" a -> "P3[1]" X -> "P4[0]" Y -> "P1[1]" b -> "P4[1]" g -> a b -> "P2[1]" g -> X g -> "P2[0]" c -> "P5[1]" }
<=== Scheme Graph ===>
<=== Assumption Graph ===> digraph assumption { g -> Y g -> X g }
<=== Assumption Graph ===> <=== Reduction Graph ===> digraph reduction { g -> Y a -> c a -> b g g -> a g -> X }
<=== Reduction Graph ===> <=== Merged Graph ===> digraph merged { g -> Y a -> c a -> b X -> "P3[0]" g -> "P5[0]" a -> "P1[0]" a -> "P3[1]" g X -> "P4[0]" Y -> "P1[1]" b -> "P4[1]" g -> a b -> "P2[1]" g -> X g -> "P2[0]" c -> "P5[1]" }
<=== Merged Graph ===>
pair vars LHS: ['a', 'g', 'X', 'X', 'g']
pair vars RHS: ['Y', 'b', 'a', 'b', 'c']
list of gens : ['g']
constraintList: []
pruned varList: ['a', 'b', 'c']
<===== Instantiate Z3 solver =====>
Traceback (most recent call last):
File "runAutoGroup.py", line 891, in
Sadly installing trunk z3 didn't work with python3 on my machine, but I'm a bit surprised this would have changed. Let me know what information would help in digging into this more.