Cryptol hangs on `:r` with some modules

[brianhuffman]

The problem seems to occur when reloading a file that contains at least two different "tricky" definitions that need solver support to type check. Here's a minimized example:

module Test where

pproduct1 : {u, v} (fin u, fin v) => [u][1 + v] -> [1 + u * v]
pproduct1 xs = if `u == 0 then 1 else pmult x0 (pproduct1 xs')
  where
    x0 = drop`{(1 - min 1 u) * v} (xs @ 0)
    xs' = drop`{min 1 u} xs

pproduct2 : {u, v} (fin u, fin v) => [u][1 + v] -> [1 + u * v]
pproduct2 xs = if `u == 0 then 1 else pmult x0 (pproduct2 xs')
  where
    x0 = drop`{(1 - min 1 u) * v} (xs @ 0)
    xs' = drop`{min 1 u} xs

Loading it with cryptol Test.cry works just fine, taking practically no time.

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.11.0.99 (c013035, modified)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Test
Test> :r
Loading module Cryptol
Loading module Test

But then after typing :r, it prints the "Loading module" messages and then just hangs, with z3 running at 100% cpu.

The bug occurs with a recent master version (c013035701578cca997abcd2a2c5b7cfd7bcac4f) on MacOS. This seems to be a regression, as the bug does not occur with the earlier cryptol-2.11 release.

[brianhuffman]

Bisection identifies 3114110aaf8dd1e38a3150d43f22ddc22d13ac22 (#1128) as the first bad commit.

[robdockins]

I wonder if this is essentially the same issue as https://github.com/GaloisInc/cryptol/issues/1250. That was fixed in #1258 by resetting the solver. Maybe we should do the same on :r

[brianhuffman]

It does get unstuck if you interrupt it with ctrl-C (which resets the solver) and then do :r again. So yes, I think resetting the solver on every :r would do it.

[yav]

I investigated what's happening here, and to me this looks like a z3 bug. Here is a trimmed down (not fully) smt-lib file that reproduces the problem directly with z3: out.txt

[robdockins]

This appears to be version specific as well. Z3 version 4.8.9 exhibits the hang, but a wide variety of other versions (that I happen to have lying around) from 4.8.1 to 4.8.11 do not.

[robdockins]

https://github.com/GaloisInc/cryptol/issues/965 seems like it might be related too, it also seems specific to Z3 4.8.9.

[brianhuffman]

I ran into a variation of this issue just now. Unlike before, it no longer requires a reload; it actually hangs when the module is first loaded. (The bug is triggered by exactly the same source file listed in the original post above.)

I did a bisection, and found that 3fabe4a21f92191e845f571997b5bdc338c7437e (#1302) is the first bad commit. This commit only modifies the definition of sortBy in the cryptol prelude; apparently it does it in such a way that merely loading the prelude puts z3 into a buggy state.

I'm see the bug with z3-4.8.9. Switching to 4.8.10 seems to make it work. I guess we should just consider 4.8.9 to be deprecated?

[yav]

Seems reasonable, although I am using z3-4.8.10 and it can't pass all the tests either, but at least it is hanging during :proof rather than just loading a module.

[brianhuffman]

The cryptol README says, "Cryptol generally requires the most recent version of Z3, but you can see the specific version tested in CI by looking here." The link indicates z3 version 4.8.10, so I would hope that 4.8.10 actually works. Is that link actually right? Are we using 4.8.10 in CI?

[yav]

We do appear to be using 4.8.10 indeed, so perhaps I am just not being patient enough. The two tests I am having trouble with are regression/negshift.icry and regression/primes.icry

[yav]

It would appear that the problem with negshift is the 32-bit case. I run a bunch of tests with different sizes, here are the numbers, which are pretty odd:

Main> :set proverStats=yes
Main> :set prover=z3
Main> :prove negLeftShift`{8,Bit}
Q.E.D.
(Total Elapsed Time: 0.066s, using "Z3")
Main> :prove negLeftShift`{9,Bit}
Q.E.D.
(Total Elapsed Time: 0.097s, using "Z3")
Main> :prove negLeftShift`{10,Bit}
Q.E.D.
(Total Elapsed Time: 0.183s, using "Z3")
Main> :prove negLeftShift`{11,Bit}
Q.E.D.
(Total Elapsed Time: 0.342s, using "Z3")
Main> :prove negLeftShift`{12,Bit}
Q.E.D.
(Total Elapsed Time: 0.362s, using "Z3")
Main> :prove negLeftShift`{13,Bit}
Q.E.D.
(Total Elapsed Time: 1.092s, using "Z3")
Main> :prove negLeftShift`{14,Bit}
Q.E.D.
(Total Elapsed Time: 2.972s, using "Z3")
Main> :prove negLeftShift`{15,Bit}
Q.E.D.
(Total Elapsed Time: 4.085s, using "Z3")
Main> :prove negLeftShift`{16,Bit}
Q.E.D.
(Total Elapsed Time: 27.806s, using "Z3")
Main> :prove negLeftShift`{17,Bit}
Q.E.D.
(Total Elapsed Time: 0.138s, using "Z3")
Main> :prove negLeftShift`{18,Bit}
Q.E.D.
(Total Elapsed Time: 10m:5.245s, using "Z3")