:prove correctSimon32_64 doesn't seem to terminate

[davidlazar]

I killed the command after 10 minutes. The proof takes a few seconds in Cryptol 1.

[acfoltzer]

Which provers have you tried with? CVC4 does indeed seem to not finish, but maybe yices or Z3 would fare better?

[davidlazar]

Z3 version 4.3.1 also didn't finish.

[dylanmc]

I confirm that Yices doesn't halt within 5 hours. I'll talk with Brian about what he thinks the cause is, and what we could do to address it.

[weaversa]

If I may provide a suggestion (that you've already heard - but just to go on public record).

AIG + ABC?

If you are super tied to SMT, someone could explore Beaver: http://uclid.eecs.berkeley.edu/jha/beaver-dist/beaver.html

[LeventErkok]

Cryptol-1 was able to do this, via internal blasting to AIG's and the custom ABC connection. Unfortunately, the results were mixed. I actually asked Mishchenko about this explicitly, and after talking to him why the results were not as good as expected, we came to the following conclusion, which I'll capture here in case you guys want to go down that path:

The issue is that AIG-based equivalence checking and in particular how ABC approaches the problem very much relies on having two distinct entry points: You create an AIG for the "spec", and another for the "implementation" and then ABC quickly does sat-sweeping to knock-out a whole bunch of in-equivalences to speed-up its search.

Unfortunately, this does not really work for the "theorem" based approach that Cryptol takes. (I think you guys changed it to "property" in Cryptol-2; which is the right keyword really.) The reason is that the theorem simply gives you a bit-valued function; i.e., in a sense it computes the "miter" that corresponds to the equivalence before the AIG's are constructed. That is, we take the theorem, and blast it to an AIG. Then we take the trivial theorem \x ->True of the same type as the original, and blast it. And then ask ABC to prove these two things are equal.

Now the problem becomes clear. The first AIG is the combination of the f and g with all the DAG nodes tangled up in not-necessarily the structurally corresponding ways. While the second AIG is the trivial one that ignores all its inputs and just returns True or everything.

In theory, this is just fine, because this is precisely what needs to be proven. But the constructed AIG no longer reflects the two entry points, they get mixed up. Thus ABC has a harder time proving equivalence.

To be more concrete, if you want to prove f equals g; then it's best for ABC to have these separately converted to AIG's and fed to ABC; as opposed to computing the AIG for the bit-valued function \x -> f x == g x and the trivial function \x -> True, and ask ABC to prove these equivalent. You have to let ABC compute the miter itself for it to be really effective.

So the issue is not a philosophical or a theoretical one, but one of practicality. This approach of proving equivalence is not what ABC has been "tuned" and "optimized" for.

Cryptol-1 had an :eq command which sort of facilitated this, but looks like you guys have done away with that. And also the fact remains that not all properties of interest can be easily cast in terms of f == g for some functions f and g.

In any case, I think a solid ABC connection would be really worthwhile; but if you do explore such a bridge, keep in mind this miter-construction problem and figure out if there's a nice way to let ABC do that instead of Cryptol. Otherwise, ABC kind of bogs down to any other SAT solver, and you loose all the tricks and heuristics Mischenko and co. implemented over the years.

This is also the same reason why I never got around to putting ABC as a backend for SBV; First, blasting is not an easy thing to do (think of multiplication/division, which algorithms do you pick? Wallace tree, school-book, booth encoding?) and miter construction on the Haskell side is pretty much baked in with the SBV approach. And modern SMT solvers do a really good job anyhow at least for academic examples of interest.

But if you are interested in co-verification (i.e., between Cryptol and Verilog/VHDL etc.), then ABC is a must have, and it's best to have ABC compute the miter. With software/hardware co-verification, you can't really afford just the theorems anyways, unless you have some fancy extern facilities like Cryptol-1 had, which Cryptol-2 seem to completely ignore, at least as far as I can see from the current release. And also keep in mind, in the "real" world, it's the structural complexity that comes down to bite you and how much your tool can deal with that, as opposed to "smarts." A good blasting bit-solver can handle many-a-problem where SMT chokes when it comes to hardware verification, as exemplified by the current industrial practice.

[kiniry]

@brianhuffman and @dylanmc, do we park this in 2.2 then, given ongoing discussions about ABC integration?

[brianhuffman]

With cvc4 version 1.3, :prove correctSimon32_64 takes forever, but with version 1.4 it completes in under a tenth of a second (significantly less time than it takes to typecheck the file). The only issue here is that some solvers are faster at some problems than others.

If anyone thinks we need to add support for prover=abc to Cryptol, then we should add that as a separate ticket.

[weaversa]

This is working great now that abc support is back!