ruleOfProp is a bit clunky

[robdockins]

The ruleOfProp operation examines the statement of a proposition and attempts to determine if it can be used as a rewrite rule. However, it is has a number of problems we should find some way to address.

1) It is unsound. For example, if it encounters a term vecEq n a f x y it will assume this proves the equality of x and y regardless of what function f is supplied. Similar for pairEq. 2) It is incomplete. Some of the primitive equality-testing functions are missing, (e.g. intEq, intModEq), so these will not be recognized as rewrites. 3) It is error-prone. Item 2 seems pretty directly related to the fact that ruleOfProp must be updated as we add new equality predicates on new types, and that hasn't been done yet.

Possible solution: I think we would be better off restricting the class of theorems that are accepted as rewrite rules to address soundness. E.g., we should only accept statements of the form Eq a x y or ecEq a peq x y. Then, add axioms for converting Eq a into the various primitive equality tests, and apply them when proving the equations to start with. E.g.

axiom boolEq_Eq : (x y : Bool) -> EqTrue (boolEq x y) -> Eq Bool x y
axiom intEq_Eq : (x y : Integer) -> EqTrue (intEq x y) -> Eq Integer x y
axiom vecEq_eq: (n : Nat) -> (a : sort 0) -> (f : a -> a Bool) ->
   ( (x y : a) -> EqTrue (f x y) -> Eq a x y) ->
   ( x y : Vec n a ) -> EqTrue (vecEq n a f x y) -> Eq (Vec n a) x y

[brianhuffman]

My comment from GaloisInc/saw-script#110 is relevant: https://github.com/GaloisInc/saw-script/issues/110#issuecomment-746482057

Another thing that bothers me about ruleOfProp is that it has the names of several equality operators like boolEq, bvEq, and vecEq hard-coded into it. It would be better if the SharedContext could refer to a set of rules/axioms for turning propositions into equations, and then ruleOfProp could work generically over this set. For example, there would be a rule like (n : Nat) -> (x y : Vec n Bool) -> EqTrue (bvEq n x y) -> Eq (Vec n Bool) x y for bvEq, and if ruleOfProp was given a theorem matching the pattern EqTrue (bvEq _ _ _) then it could be composed with this rule to produce an Eq theorem that could work directly as a rewrite rule.

If ruleOfProp was implemented this way, then we could easily extend ruleOfProp to handle new forms of theorems later, even at runtime.

This is exactly the same idea proposed above, so yes, of course I support it completely. To facilitate implementation, it would be nice to have some combinators for composing theorems with resolution/modus ponens, sort of like the OF and COMP operators in Isabelle.

Also I would not hard-code a special exception for ecEq; we can add some definitions and rules like these to Cryptol.sawcore

ValidPEq : (a : sort 0) -> PEq a -> Prop;
ValidPEq a pa = (x y : a) -> ecEq a pa x y -> Eq a x y;

ecEq_Eq : (a : sort 0) -> (pa : PEq a) -> (x y : a) -> ValidPEq a pa -> EqTrue (ecEq a pa x y) -> Eq a x y;
ecEq_Eq a pa x y valid e = ...

along with some axioms (or proved theorems) stating that the various PEq dictionary combinators preserve the ValidPEq property.

[robdockins]

I missed that discussion before. Yeah, it sounds like we are largely in agreement.

We could have the PEq class carry its correctness property, which would make it pretty easy to access.

[brianhuffman]

Putting the correctness property inside the dictionary would be pretty handy. Are there any potential drawbacks to doing that? The only thing I can think of is that putting a dependent type like that inside PEq might make it harder to export certain terms to certain backends? And I guess we'd have to define PEq as a saw-core datatype instead of a (non-dependent) record type (not a big deal).

[robdockins]

I suppose that might be a problem if we wanted to target HOL or something, although I think we're already in pretty big trouble if we want to do that.

I forgot that saw-core records are necessarily non-dependent. That might be a little inconvenient. I think there are a few places where Verifier.SAW.Cryptol assumes dictionaries are records, but we can probably work around that.

[robdockins]

I guess the other problem is that we wouldn't be able to have any law-breaking PEq instances. The problematic issues with Float equality would be an issue here. Edit: on second thought, maybe it isn't an issue for floats, as long as we phrase it as an implication instead of an equivalence.

[brianhuffman]

I think it actually is an issue for floats, isn't it? We have +0 == -0 for floats, but those values are not logically equal, so the implication doesn't hold. We should probably just make a separate predicate for law-abiding Eq instances, then.

[brianhuffman]

I had a go at implementing some validity rules for equality predicates, which you can see on the ValidEq branch (af4fe14186235a6387ae8ad73e4c703140d5c18d).

[robdockins]

I think it actually is an issue for floats, isn't it? We have +0 == -0 for floats, but those values are not logically equal, so the implication doesn't hold. We should probably just make a separate predicate for law-abiding Eq instances, then.

Yes, you're right. I was only thinking about NaN, but issue with signed 0 goes the other way.