Cryptol comparisons don't translate nicely into saw-core

[brianhuffman]

When you translate a Cryptol term using the <$ operator into SAW, you currently get an unnecessarily complicated term:

sawscript> rewrite (cryptol_ss ()) {{ \(x : [8]) y -> x <$ y }}
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x : x@1) ->
      \(y : x@1) ->
        Prelude.or (Prelude.bvslt 8 x y)
          (Prelude.and (Prelude.bvEq 8 x y) Prelude.False)

The or _ (and (bvEq x y) False) part is completely redundant. We should translate this simply as bvslt.

[brianhuffman]

Turns out this is not specific to signed comparisons. Ordinary < and <= do the same thing:

sawscript> rewrite (cryptol_ss()) {{ \(x:[8]) (y:[8]) -> x < y }}
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x : x@1) ->
      \(y : x@1) ->
        Prelude.or (Prelude.bvult 8 x y)
          (Prelude.and (Prelude.bvEq 8 x y) Prelude.False)
sawscript> rewrite (cryptol_ss()) {{ \(x:[8]) (y:[8]) -> x <= y }}
let { x@1 = Prelude.Vec 8 Prelude.Bool
    }
 in \(x : x@1) ->
      \(y : x@1) ->
        Prelude.not
          (Prelude.or (Prelude.bvult 8 y x)
             (Prelude.and (Prelude.bvEq 8 y x) Prelude.False))

[brianhuffman]

The problem comes from the way the Cmp and SignedCmp class dictionaries are defined in Cryptol.sawcore.

saw-script/cryptol-saw-core/saw/Cryptol.sawcore

Lines 537 to 541 in db538d3

	PCmp : sort 0 -> sort 1;
	PCmp a =
	#{ cmpEq : PEq a
	, cmp : a -> a -> Bool -> Bool
	};

saw-script/cryptol-saw-core/saw/Cryptol.sawcore

Lines 583 to 587 in db538d3

	PSignedCmp : sort 0 -> sort 1;
	PSignedCmp a =
	#{ signedCmpEq : PEq a
	, scmp : a -> a -> Bool -> Bool
	};

Instead of only a single continuation-style all-purpose comparison operator, the class dictionary also needs ordinary comparison operators that can be defined without extra ands and ors.

[robdockins]

Does the standard simpset not include boolean identities that would collapse this?

[brianhuffman]

There are some rewrite rules in Prelude.sawcore that can collapse that pattern, but they're not in any "standard" simpset like cryptol_ss. When doing a proof, it's easy enough to use those rewrite rules. But the real problem is when you're trying to state new rewrite rules of your own that have comparison operators on the left-hand side: In cryptol syntax you would write (x < y) == ... and the generated rewrite rule ends up as some complicated fragile pattern with and/or/False on the lhs as well. It makes it quite a hassle to do rewriting proofs.

[robdockins]

Looks like that design choice first came in here: 0e78371

Do you recall if there was a particular reason to do things that way, or was it just convenient?

[brianhuffman]

I remember implementing that dictionary passing translation. There was a specific reason for using the cmp field of type a -> a -> Bool -> Bool for comparisons: I wanted something that would correctly implement lexicographic ordering for compound types without being stupidly inefficient. Normally on type (a, b) you'd define (u, v) < (x, y) as (u < x) \/ (u == x /\ v < y). But if type a is itself a complex type, then you don't want to have to traverse u and x twice to compute the comparison result. The cmp approach works well in that regard. But what I failed to do is add special cases to simplify the comparison formulas for basic types.

[robdockins]

Maybe we could change the type of cmp to something like cmp : a -> a -> Maybe Bool -> Bool, where a Nothing indicates that there's no interesting continuation and to just emit the basic less than test.

[brianhuffman]

Yeah, I thought about using a Maybe type, but we also don't want to leave any recursors for the Maybe type lying around in the resulting term either. I think what we should do is just add an lt field to the Cmp dictionary that just implements the plain less-than comparison. The Cmp dictionary constructors for compound types like (a, b) would define lt on the pair type in terms of cmp on type a and lt on type b.