Fixing up BufLength, the use of nubOrd, and adding one more PLT rule

[msooseth]

Description

This is a fix to Prop ordering and 2 improvements.

Prop Ordering and nubOrd

remRedundantProps p = nubOrd $ collapseFalse . filter (\x -> x /= PBool True) . nubOrd $ p

has been changed to have nubOrd at the front. More importantly, Prop was not correctly ordered(!). It missed ordering by Prop type AND it had an issue with using && instead of ||. We have now fixed this and I have added new tests to catch this kind of error.

BufLength issue

Expr.simplify $ (Max (Lit 0) (BufLength (AbstractBuf "txdata")))

became:

(Max (Lit 0) (BufLength (AbstractBuf "txdata")))

Effectively "ignoring" the rule:

    go (Max a b) = case (a, b) of
                    (Lit 0, _) -> b
                    _ -> EVM.Expr.max a b

But in fact it was NOT ignoring that rule. Instead,

    go (BufLength buf) = bufLength buf

Was in fact creating an infinite loop(!) because of:

 bufLengthEnv :: Map.Map Int (Expr Buf) -> Bool -> Expr Buf -> Expr EWord
 bufLengthEnv env useEnv buf = go (Lit 0) buf
   where
     go :: Expr EWord -> Expr Buf -> Expr EWord
     [...]
    go l (AbstractBuf b) = Max l (BufLength (AbstractBuf b))

Which added one Max every time -- which was then stripped by the Max rule. This lead to a "fixedpoint" and so things didn't get simplified. This has now been fixed.

We also added 2 more small rules:

    go (PLT (Max (Lit a) b) (Lit c)) | a < c = PLT b (Lit c)

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[zoep]

Nice catch!