:prove performance issues - even using "offline"/"w4-offline"

[linesthatinterlace]

Hi. This is a MWE of an issue I think I'm having elsewhere, which I think is a bottleneck with how :prove converts something to an SMT-lib file.

I have the following module:

module example where

trivial : {n} (fin n) => Bit
property trivial = (zero : [n]) == (zero : [n])

I would like to :prove trivial`{n}, for large fixed n, say. For small n it's obviously very fast - I set :set prover=offline so I could just focus on the SMT-LIB conversion, and every output basically looks like this:

Writing to SMT-Lib file standard output...
To determine the validity of the expression, use an external SMT solver.
; Automatically created by SBV on 2021-05-29 12:49:36.4225209 BST
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- tuples ---
; --- sums ---
; --- literal constants ---
; --- skolem constants ---
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert false)
(check-sat)

• that is, the SMT-Lib file produced is trivial. However, for n > 2^30 (on my machine), I start seeing dramatic slowdown, and indeed on some investigation I think it is roughly O(n) (because moving to 2^31, 2^32 seemed to roughly double the time taken).

This means for large inputs (and in cryptographic contexts the inputs in terms of number of bits can get large enough that it starts to be problematic), the :prove conversion is really slow, even where it feels like it "shouldn't" be.

I get much better performance with using w4-offline (my understanding is that this uses a different backend) but in THIS case, it crashes for larger values of n, around 2^39, with "cryptol: word too wide for memory: 549755813888 bits". Which is reasonable I suppose - this IS a lot of a memory, right - but in this case it feels like it ought not to be strictly necessary if one could only apply some basic rules...

This originally came up in a context where I have functions f : a -> a and g : a -> a, some initial value init : a, and I want to show that take{n} (iterate f init) = take{n} (iterate g init), (where I certainly can prove a property of the form p a = f a == g a) - I had hoped that in some sense a "pattern match" was possible, but it seems that that isn't true, and indeed the above case shows that even in the most trivial case it's tricky - but also that the bottleneck is NOT the SMT solvers but the conversion to SMT-Lib that they perform.

[robdockins]

The sort of "proof by congruence" that you want to do on your iterated functions is much better supported via SAW, which allows you to perform rewriting steps on intermediate terms without fully unrolling them first.

The zero == zero case is an interesting one. The fundamental problem here is that GMP will crash if we attempt to allocate a number too large https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html Rather than let that happen, we guard against such cases by checking word widths. I'm not sure why the SBV backend doesn't raise the same error, it probably should.

Again, if you want to treat values more "syntactically", then SAW is probably a better platform for those kinds of proofs.

[linesthatinterlace]

Thank you - I realised today actually that SAW is really where I need to be looking, though I don't have much experience using it for this - is it a "learn by doing" sort of thing (using the manual also, of course).

Incidentally - this didn't feel big enough to do its own thing, but sometimes a thing I might want to do on a multiple-argument function is exhaust over some arguments and prove it otherwise. An example is a property where one argument is a Bit, and I can prove the property for the two possible values of the bit, but for whatever reason the proof on the whole doesn't go so fast. Is there a way to do this kind of proof, in Cryptol or SAW?

[robdockins]

It's a little ad-hoc, but you can do the following sort of thing, which is essentially manual quantifier elimination. Assume f is some function you'd like to test:

f: [8] -> Z 127 -> Integer -> Bit

property f_test (i:Integer) =
  and [ f a b i | a <- [0 ..< 2^8], b <- [0 ..< 127] ] 

It won't run separate proofs, but it might still get the advantages you want. If not, we can think about some way to do this better.

[linesthatinterlace]

Aye, I have done summat similar to this - and it does work - but, say, if what I have is two functions f and g, and I want to show that f s x N == g s x N (maybe under certain conditions) - say I would like to use this for some rewrite rule, right? I can't exhaustively prove it because the type of s and x are very big, say, but proving for arb. s and x and some fixed N is not so bad, and N is, say, 7-bits, so isn't so many values. I certainly can do a proof "across all the N values", as you have done - and this works - but it's less clear to me I can do owt useful with that fact, if that makes sense?

[robdockins]

Are you trying to do this in SAW? I don't think we currently have a "proof-by-cases" tactic, but we really should.

[linesthatinterlace]

Yes, I happened to be doing this in Cryptol, but mainly that's a function of - to be entirely honest - not really understanding how to do more complicated proofs using SAW and tactics and that. I'm working on it, I guess.

I think it would be a very useful thing, because it feels like a reasonably natural case.

I may as well say while I'm here that if N was a type variable that sort of throws a different cat among pigeons (because then I think you can't really loop over it).

[robdockins]

I think the issues raised here are all better handled in SAW. Please feel free to open issues there if you need additional help.