Slow (non-terminating?) proofs of A51, Bivium, Trivium

[atomb]

Alexander Semenov recently wrote up Cryptol implementations of the stream ciphers A51, Bivium, and Trivium in Cryptol, along with some correctness properties, which are now in the Cryptol repository.

https://github.com/GaloisInc/cryptol/tree/master/examples/contrib

Proving these in Cryptol works great:

Cryptol> :l A51.cry
Loading module Cryptol
Loading module Main
Main> :prove A51_correct
Q.E.D.
Main> :l bivium.cry
Loading module Cryptol
Loading module Main
Main> :prove Bivium_correct
Q.E.D.
Main> :l trivium.cry
Loading module Cryptol
Loading module Main
Main> :prove Trivium_correct
Q.E.D.
Main>

Proving them in SAW, not so well:

sawscript> import "A51.cry"
Loading module Main
sawscript> prove_print z3 {{ A51_correct }}
^CCtrl-C

It is easy to generate the theorems, so it seems like it's a problem in the SBV backend (and I've confirmed that the same happens with the ABC backend).

sawscript> prove_print (offline_extcore "foo") {{ A51_correct }}
Valid
Theorem (A51_correct)
sawscript> :q
$ du -ch fooprove.extcore
 20K    fooprove.extcore
 20K    total

[brianhuffman]

All of those correctness theorems have type Bit in Cryptol (i.e. they don't quantify over any variables) so we can also compare the time for concrete evaluation.

sawscript> time (print {{ Bivium_correct }})
True
Time: 3.907268s

sawscript> time (print {{ Trivium_correct }})
True
Time: 15.450085s

After 10 minutes, I'm still waiting for A51_correct to finish. I was also able to finish z3 proofs of Bivium_correct and Trivium_correct (they took about 3-4 times as long as the concrete evaluations).

Anyway, it looks like we have a performance bug in the saw-core evaluator, which is independent of the backend. Those algorithms are all implemented using some infinite stream operations, so my guess is that we're recomputing some stream elements many times.

[brianhuffman]

I looked into this further, and I found some interesting examples of slowdown behavior. Problems arise with recursively defined infinite streams that use the append operator (#). Consider these two variations on the iterate function, which we will combine with a function expensive whose runtime is proportional to its argument.

iterate : {a} (a -> a) -> a -> [inf]a
iterate f x = [x] # iterate f (f x)

iterate' : {a} (a -> a) -> a -> [inf]a
iterate' f x0 = xs where xs = [x0] # [ f x | x <- xs ]

stupid : [16] -> Bit
stupid n = (n == 0) || stupid (n - 1)

expensive : [16] -> [16]
expensive x = if stupid x then x+1 else 0

Now we can run the following commands for various values of n:

time (print {{ (iterate expensive 0) @ n}})
time (print {{ (iterate' expensive 0) @ n}})
time (print {{ take`{n}(iterate expensive 0) }})
time (print {{ take`{n}(iterate' expensive 0) }})

The first two commands have a similar runtime, which is quadratic in n, as expected. The third command is still quadratic, but takes slightly longer for the same value of n. This shows that with iterate, we are not losing sharing. The fourth, however, is cubic in n. This indicates that with iterate' we are losing sharing, and that we are duplicating a lot of computation. Very interesting!

Next, we can do the same experiments, but iterating a much cheaper function: replace expensive with ((+) 0x0001). Now the first two tests (with @) both run in linear time. The last test (take with iterate') takes quadratic time, which makes sense because we know that iterate' loses sharing. But interestingly, the third test (take with iterate), which doesn't lose sharing, also takes quadratic time. So something else is going on here.

To summarize: I think we have two separate causes of performance problems. First, we lose data sharing with some recursive definitions (in particular, definitions like iterate' that use recursion on data types rather than function types).

Second, there is an additional cost to traverse a recursively defined infinite stream. This probably has to do with the inefficiency of # on the saw-core representation of streams, which is like a memoized function from index to elements. The Cryptol interpreter uses lazy lists, which are worse for indexing, but better at concatenation.