Stabilise normalisation of `Int`comparison operators

[PetarMax]

Currently, there is a back-and-forth happening in the backend which keeps transforming notBool ==Int into =/=Int and vice versa:

[proxy][abort][detail] Kore simplification: Diff (< before - > after)
383d382
<     notBool_(_==Int_(VarCALLER_ID:SortInt{}, "6453264744265472...truncated"))
392c391,392
<     notBool_(_==Int_(VarCONTRACT_ID:SortInt{}, "6453264744265472...truncated"))
---
>     _=/=Int_(VarCALLER_ID:SortInt{}, "6453264744265472...truncated")
>     _=/=Int_(VarCONTRACT_ID:SortInt{}, "6453264744265472...truncated")
395d394
<     notBool_(_==Int_(VarORIGIN_ID:SortInt{}, "6453264744265472...truncated"))
396a396
>     _=/=Int_(VarORIGIN_ID:SortInt{}, "6453264744265472...truncated")

Specifically, notBool ==Int is transformed into =/=Int when the booster performs internalisation here, whereas =/=Int is transformed into notBool ==Int whenever this simplification from domains.md is applied. I think that this means that during analysis we are working with notBool ==Int.

I would suggest that we decide which format we prefer, together with choosing the level at which the format is established. It can be at the K-level, via simplifications, or at the backend-level, via internalisation.

I would also suggest that we normalise the other comparison operators, possibly favouring <=Int and <Int. This would mean that we do not see >=Int, >Int, or notBool [<=Int/<Int/>=Int/>Int]. We are already doing that in KEVM:

    // inequality sign normalization
    rule          A  >Int B  => B  <Int A [simplification]
    rule          A >=Int B  => B <=Int A [simplification]
    rule notBool (A  <Int B) => B <=Int A [simplification]
    rule notBool (A <=Int B) => B  <Int A [simplification]

but could bring this up to K and/or decide to move this into the backend.

[ehildenb]

I vote for K level with simplifications.

[Baltoli]

Historical context on the internalisation: KORE hands back #Not terms when given a Bool (!) so we need to normalise them back out (to stay in Bool-land).

[Baltoli]

@geo2a says we may have dealt with the underlying issue, and it might be a good time to investigate removing these special cases.

@goodlyrottenapple points out that there is still some weird magic in the old backend, so might still need to handle that.

[Baltoli]

@goodlyrottenapple to do a restricted time-box on this

[geo2a]

As I understand, Booster basically has the following rule hard-coded:

rule #Not (I1:Int ==Int I2:Int) => I1 =/=Int I2

We have anecdotal evidence that Kore will sometimes produce #Not.

Maybe we could reduce the magic by just internalising #Not as notBool, and then have a rule in domains.md that does the translation to =/=Int:

rule notBool (I1:Int ==Int I2:Int) => I1 =/=Int I2

[geo2a]

Looking further at domains.md, we have some rules that look suspiciously like they'd introduce #Not:

  rule {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification]
  rule {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification]
  rule {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification]
  rule {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification]

could that be that this is the magic that we think is introduced by Kore? One way to find out: we should add labels to these rules and see of they are actually used.

[goodlyrottenapple]

@PetarMax would you happen to have bug report exhibiting this behaviour when ran with the requisite logging?

[PetarMax]

Sorry, @goodlyrottenapple, which specific behaviour?

[goodlyrottenapple]

The back and forth of not(==Int)... no worries tho, @geo2a pointed me to a bug report which exhibits this behaviour