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

Potential test case for w4 improvements #1239

Closed
weaversa opened this issue Jul 20, 2021 · 3 comments
Closed

Potential test case for w4 improvements #1239

weaversa opened this issue Jul 20, 2021 · 3 comments
Assignees
@robdockins
Labels
prover Issues related to :sat and :prove What4/SBV Cases where there is a significant performance difference between What4 and SBV

Comments

@weaversa
Copy link
Collaborator

SBV has some simplification pass that w4 does not. The following demonstrates this weakness in w4.
SKIPJACK.txt

$ cryptol SKIPJACK.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.10.0.99 (0abde1e)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module SKIPJACK
SKIPJACK> :s prover=sbv-z3
SKIPJACK> :safe encrypt
Safe
(Total Elapsed Time: 0.056s, using "Z3")
SKIPJACK> :s prover=w4-z3
SKIPJACK> :safe encrypt
(waited 30 minutes and gave up)
@robdockins robdockins added prover Issues related to :sat and :prove What4/SBV Cases where there is a significant performance difference between What4 and SBV labels Jul 20, 2021
@robdockins
Copy link
Contributor

That's pretty dramatic; I'll definitely be interested to find out what's going on here.

@robdockins robdockins self-assigned this Jul 20, 2021
@robdockins
Copy link
Contributor

Comparing the sbv-offline prover with the w4-offline prover, we can easily see that SBV reduces the query to a concrete false, whereas the What4 backend instead produces a relatively large formula to check. I'm not sure yet what simplification rule is responsible for the difference.

@robdockins
Copy link
Contributor

:safe (G zero) already reveals the difference between the backends.

My suspicion is that this has to do with the lookup table F. SBV will render the concrete values in F into a SMT-array lookup table, whereas What4 doesn't do this (perhaps it should). This seems to affect the computation of the safety predicate resulting from the sequence lookups, but I don't know why What4 can't figure out that an 8-bit value is always going to be in bounds for a 256-element array.

robdockins added a commit that referenced this issue Jul 26, 2021
@robdockins
Update indexing primitives to remove troublesome corner cases.
c533996 
Previously, when indexing into a sequence, there were code paths
in both the SBV and What4 backends where an if/then/else tree
would be built to compute the value of a symbolic lookup, with one
branch for each valid sequence index.  They differed, however, in
what value they would comute for out-of-bound indices.  For SBV,
we would compute a `zero` value, whereas for What4 we would
raise an error.  For What4, this resulted in unfortunate and redundant
proof obligations, as we elsewhere add a test for in-bounds contditions
to the safety predicate.  Moreover, the strategy of returning a
`zero` value could panic in some situations, as not every type
has a `zero` value anymore (e.g., newtypes).

In both cases, we now do the same thing, which is not to have a case
of the if/then/else tree for out-of-bounds indices; the final element
of the sequence will simply be returned instead.  We will only raise
an out of bounds error in this code path if the sequence is actually
empty.

Fixes #1239
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robdockins robdockins

Labels
prover Issues related to :sat and :prove What4/SBV Cases where there is a significant performance difference between What4 and SBV
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@robdockins @weaversa