Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Inconsistency in w4-yices/What4 - incorrect SMTLib-2 giving rise to false counterexamples. #1210

Closed
linesthatinterlace opened this issue Jun 4, 2021 · 8 comments
Closed

Inconsistency in w4-yices/What4 - incorrect SMTLib-2 giving rise to false counterexamples. #1210

linesthatinterlace opened this issue Jun 4, 2021 · 8 comments
Assignees
@robdockins
Labels
bug Something not working correctly upstream Tracking bugs in external tools/libraries we depend on

Comments

@linesthatinterlace
Copy link

linesthatinterlace commented Jun 4, 2021 •
edited
Loading

I have the following property:

bitget : [12] -> [436][8] -> Bit
property bitget i r = i < 3488 ==> bit_gf == if bit_bit then 0x0001 else 0x0000
  where bit_gf = (zext (((r@(i/8)) >> (i%8)) && 1))
        bit_bit = (join (map reverse r))@i

When I set prover = yices, and ask Cryptol to :prove bitgit, I get a QED in a handful of seconds. Similarly, z3 and mathsat also work. However, when I set prover = w4-yices (or indeed w4-z3), I get a "Counterexample", and then a counterexample is provided. This counterexample is not actually a counterexample, however - as in, when I run bitget on the data it says bitget evaluates as False, it reads True.

Obviously this is a pretty serious issue - I assume the What4 backend is producing wrong SMTLIB-2 somehow. I wasn't sure if I should raise this here or in https://github.com/GaloisInc/what4 but I've put it here for now. I have to assume - having found this - that I cannot trust the output of w4- proofs until it is fixed - unless anyone can satiate my fears?

I've included the output so you can see exactly what I mean.

synd> :set prover = yices
synd> :prove bitget
Q.E.D.
(Total Elapsed Time: 2.776s, using "Yices")
synd> :set prover = w4-yices
synd> :prove bitget
Counterexample
bitget
  0x885
  [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
   0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00] = False
(Total Elapsed Time: 0.871s, using "yices")
synd> bitget 0x885 [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00]
True
@linesthatinterlace
Copy link
Author

An update: on some experimentation, I've managed to find this (possible minimal) example:

mwe : [2] -> [2][1] -> Bit
property mwe i r = (r@0) >> 0 == (r@0) >> 0*i

With demonstration:

synd> :set prover = yices
synd> :prove mwe
Q.E.D.
(Total Elapsed Time: 0.003s, using "Yices")
synd> :set prover = w4-yices
synd> :prove mwe
Counterexample
mwe 0b00 [0b1, 0b0] = False
(Total Elapsed Time: 0.002s, using "yices")
synd> mwe 0b00 [0b1, 0b0]
True

The generated SMT-Lib files are as follows, using SBV and What4 in order:

; Automatically created by SBV on 2021-06-04 14:41:08.725129 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 ---
(declare-fun s0 () (_ BitVec 2))
(declare-fun s1 () (_ BitVec 1))
(declare-fun s2 () (_ BitVec 1))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert false)
(check-sat)

(set-option :produce-models true)
; :1:0
(declare-fun x!0 () (_ BitVec 1))
(define-fun x!1 () Bool (= (_ bv0 1) x!0))
(define-fun x!2 () Bool (not x!1))
(assert x!2)
(check-sat)
(exit)

Obviously this example is absurd (you would never do this) but I think it is the same core issue as the one above (with all of my context removed - and this did naturally come up in the context of verifying some crypto code).

@linesthatinterlace
Copy link
Author 

mwe : [2] -> [2][1] -> Bit
property mwe i r = (r@0) >> 0 == (r@0) >> 0*i

and

mwe : [2] -> [2][1] -> Bit
property mwe i r = (r@0) >> 0 == (r@0) >> (0*i + 1)

produce different SMT-Lib code using SBV, but identical SMT-Lib code using What4. Of course, the first is always true and the second is not. Note that if you remove the dependence on i from the second term, or replace r@0 with simply a 1-bit array, there's no issue - something appears to be breaking in that interaction.

@weaversa
Copy link
Collaborator

weaversa commented Jun 4, 2021

Is it possible this is related to this: #1191
?

@robdockins
Copy link
Contributor

This appears to be different than #1191, unfortunately.

@robdockins
Copy link
Contributor

The following also demonstrates the problem, and doesn't require any symbolic variables.

property mwe'' = r == (r << i)
 where r = 1:[1]
       i = 0:[2]

The issue seems to arise only when i has a longer bit-width than r. There is some range reduction code inside What4 that I now suspect.

@robdockins
Copy link
Contributor

Yup, looks like this line:

https://github.com/GaloisInc/what4/blob/200428c28ec776aa8739388a70964e9aff3b42a3/what4/src/What4/SWord.hs#L684

Pretty sure that max should be a min instead.

@robdockins
Copy link
Contributor

And, indeed, if I change (i%8) to ((drop (i%8)):[8]) in the original example above, it works as expected.

@robdockins
Copy link
Contributor

The underlying bug is fixed via GaloisInc/what4#127

I'll leave this ticket open until we get a new What4 release and update Cryptol to use it.

@robdockins robdockins added bug Something not working correctly upstream Tracking bugs in external tools/libraries we depend on labels Jun 4, 2021
@robdockins robdockins self-assigned this Jun 17, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robdockins robdockins

Labels
bug Something not working correctly upstream Tracking bugs in external tools/libraries we depend on
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@robdockins @weaversa @linesthatinterlace