SBV.SMT.SMTLib2.cvtExp.sh: impossible happened

[msaaltink]

After I load this code

bar: [1] -> [1] -> Bit
bar xs ys = (xs@0) < ys@0

if I try :sat \x y -> bar x y it crashes cryptol:

cryptol: SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: s3 < s4

This is in a fairly recent version from git (14b9399) - the latest, I think.

[TomMD]

I can reproduce with just comparing bits.

f : Bit -> Bit -> Bit
f x y = x < y

And:

Main> :sat f
cryptol: SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: s0 < s1

[weaversa]

>, <, <=, >= are broken in this way. The other comparators (== and !=) don't exhibit the bug.

[iblumenfeld]

Is this really a bug? Why should False be less than True? I imagine that inequalities should only apply to numbers. Not if [False] < [True] didn’t work, that would be a bug.

Best,
Ian

Ian Blumenfeld
Galois, Inc.
(c) 410.948.8460
[email protected]

On Nov 3, 2014, at 8:07 AM, weaversa [email protected] wrote:

, <, <=',>=' are broken in this way. The other comparators (== and !=) don't exhibit the bug.

—
Reply to this email directly or view it on GitHub.

[weaversa]

Cryptol gives concrete answers:

Cryptol> True < False
False
Cryptol> True > False
True

And, the Cmp type class allows comparisons on Bit (see #129). The only restriction in Cryptol is that comparisons be between finite objects (although the type class is called Cmp instead of fin). Also, arithmetic operators are not defined on Bit, even though comparisons are. I know it seems kind of strange --- if True > False == True then why not True + False == True? And, I think the answer is that a kind of asymmetry exists as the rank (number of nestings of []) grows.

That is, if we allowed arithmetic to be defined on Bit, we could have:

True + False == True

But, when happens when we move up a rank? Surely we don't want to apply the operation element-wise:

[False True] + [True True] == [True False]
1 + 3 == 2

But, here we do want to apply element-wise:

[1 3] + [1 1] == [2 0]

So, refusing to define arithmetic on Bits removes the asymmetry (different behaviour based on rank).

Maybe I wasn't very clear...I'm trying to write down my intuition about this.

[iblumenfeld]

I see.

I looked over the SMT-LIB2 document, and I’m fairly certain that the inequality operators are not defined in the Core theory for Bools, only on theories like Int, Real, Bit-vectors, etc.

I think SMT-LIB2 is making the right choice here. Saying False < True is True is not really sensible mathematics. I suppose you could just implicitly equate less-than-or-equals to to implication (giving the very silly looking typography (<=) == (=>) ) which gives the same results that you want, but as a mathematician, it leaves a bad taste in my mouth.

Ian Blumenfeld
Galois, Inc.
(c) 410.948.8460
[email protected]

On Nov 3, 2014, at 10:09 AM, weaversa [email protected] wrote:

The Cmp type class allows comparisons on Bit (see #129). And, Cryptol gives concrete answers:

Cryptol> True < False
False
Cryptol> True > False
True
—
Reply to this email directly or view it on GitHub.

[weaversa]

Lexicographic ordering and big-bit endian (MSB 0 endian) work naturally with comparisons. Comparison of integers (and greater rank structures) can be done by folding the bit-level definitions over the greater rank structure. That is, if < is defined on Bit (as it is now in Cryptol), computing < on any greater rank structure can be done by folding the Bit definition of < lexicographically over the greater rank structure.

For example, say a = [False, True, True, False, ...] and b = [False, True, True, True, ...], then a<b can be computed by testing a@0 < b@0, then a@1 < b@1, and so on, returning the first result a@i < b@i where a@i differs from b@i. In this case a@3 < b@3 == True and so a < b == True.

[brianhuffman]

This seems to be a bug in the SBV library. I just opened an issue for it: LeventErkok/sbv#97. Once we have a patch, I'll pull it into our local fork.

In the meantime I'll add a test to our regression suite for this.

[weaversa]

The words True and False are used in Cryptol have type Bit and represent the binary digits, 1 and 0. This base type is useful to disambiguate individual bits from integers. Viewing a number as a sequence of bits is natural in Cryptol and mathematics. Treating the result of a predicate as a bit, rather than a truth value, is where Cryptol (and many computer languages) diverge from mathematics.

If False < True looks bad, does the following look just as bad?

Cryptol> [1<2, 3<4]
0x3

@brianhuffman, it may not be a bug in SBV --- maybe @LeventErkok doesn't want SBV to do comparisons on individual bits?

[LeventErkok]

@weaversa This is a bug in SBV.. Since Bool is an instance of Ord in Haskell, SBV has no choice but to implement that properly.

However, I do share Ian and Sean's sentiments.. I am not sure why we ever had instance Ord Bool in Haskell.. Seems silly to include it, and any code using this instance (which is rare I'd posit) can probably be written much clearer in other ways.

Ask John Launchbury if he's around; he might remember if there was a good reason..

As far as Cryptol is concerned; I guess you could go both ways here as well. I don't think anyone is going to complain if the type-checker rejected comparisons on Bit. But maybe the ship is sailed on that one as well, just like the Haskell case.

[LeventErkok]

Patch pushed to SBV: LeventErkok/sbv@67656c6

Give it a try and let me know if it's still choking!

[TomMD]

Works for me:

Cryptol> :sat (\x y -> (y : Bit) < x)
(\x y -> (y : Bit) < x) True False = True

I ported these by hand, but someone else probably has an automated way to port SBV patches and Cryptol/sbv, so they should commit instead.

[brianhuffman]

I usually take care of the porting of SBV updates; it's a slightly-automated process involving git diff, patch, and a fair bit of manual conflict resolution. Hopefully one of these days we'll make the process unnecessary (see #35).

Anyway, thanks for the patch, @LeventErkok!

[LeventErkok]

Cool..

I noticed you also picked up several other updates, and in particular a change required for the new release of Boolector v2.0.1. Unfortunately, the change is not backwards compatible, so if anyone is using Boolector as a backend solver for Cryptol, then they'll have to make sure to upgrade their Boolector installation.

[LeventErkok]

Ah; and you also picked up sAssert which you guys can use to implement safety-checks, ala Cryptol-1. (Not exactly the same, but good enough approximation.) Let me know if you play around with that and if it works well.