in_keys() not evaluated even when it's present in term constraint

[denis-bogdanas]

#lookupMemory implementation:

    syntax Int ::= #lookupMemory  ( Map , Int ) [function, functional, smtlib(lookupMemory)]

    rule [#lookupMemory.some]:   #lookupMemory( (KEY |-> VAL:Int) _M, KEY ) => VAL modInt 256
    rule [#lookupMemory.none]:   #lookupMemory(                    M, KEY ) => 0                 requires notBool KEY in_keys(M)
    //Impossible case, for completeness
    rule [#lookupMemory.notInt]: #lookupMemory( (KEY |-> VAL    ) _M, KEY ) => 0                 requires notBool isInt(VAL)

Test:

rule <k> runLemma ( #lookupMemory((KEY |-> 33), KEY') ) => doneLemma ( 0 ) ... </k> requires notBool KEY' in_keys(KEY |-> 33)

Result:

  #Not ( {
    #lookupMemory ( KEY |-> 33 , KEY' )
  #Equals
    0
  } )
#And
  #Not ( {
    KEY
  #Equals
    KEY':Int
  } )
#And
  <kevm>
    <k>
      doneLemma ( #lookupMemory ( KEY |-> 33 , KEY' ) ) ~> DotVar2 ~> .
    </k>
...

Code: https://github.com/kframework/evm-semantics/blob/6937f1ebf3645b962cc5e7d654a8f716a873c518/tests/specs/functional/lemmas-spec.k#L39

[ttuegel]

domains.k has a rule for symbolically evaluating in_keys. Please run this example with --debug-equation to find out why it is not applied.

[denis-bogdanas]

The rules from domains.k are for Java, not Haskell:

module MAP-JAVA-SYMBOLIC [kast, symbolic]
...
  rule K1 in_keys(M K2 |-> _) => true          requires K1  ==K K2 orBool K1 in_keys(M) [simplification]
  rule K1 in_keys(M K2 |-> _) => K1 in_keys(M) requires K1 =/=K K2 [simplification]

  rule K1 in_keys(M [ K2 <- _ ]) => true          requires K1  ==K K2 orBool K1 in_keys(M) [simplification]
  rule K1 in_keys(M [ K2 <- _ ]) => K1 in_keys(M) requires K1 =/=K K2 [simplification]
endmodule

I debugged the failing test with full --log-level debug. Something rewrites in_keys expression into

        \equals{SortKItem{}, R}(
            /* Fl Fn D Sfa */ VarKEY:SortKItem{},
            /* Fl Fn D Sfc */
            /* Inj: */ inj{SortInt{}, SortKItem{}}(
                /* Fl Fn D Sfa */ VarKEY'Apos':SortInt{}
            )

but that piece of logic is not logged.

There's this piece also which looks strange:

kore-exec: [2020-07-10 21:23:48.1551454] Debug (DebugEvaluateCondition):
    (DebugAttemptEquation) while applying equation at /mnt/d/evm-semantics/evm-types.md:664:34-664:129:
    evaluating predicate:
        /* Sfc */
        \not{R}(
            /* Sfc */
            \not{R}(
                /* Spc */
                \equals{SortKItem{}, R}(
                    /* Fl Fn D Sfa */ VarKEY:SortKItem{},
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortInt{}, SortKItem{}}(
                        /* Fl Fn D Sfa */ VarKEY'Apos':SortInt{}
                    )
                )
            )
        )
    with side condition:
        \and{_PREDICATE{}}(
            /* Sfc */
            \not{_PREDICATE{}}(
                /* Spc */
                \equals{SortKItem{}, _PREDICATE{}}(
                    /* Fl Fn D Sfa */ VarKEY:SortKItem{},
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortInt{}, SortKItem{}}(
                        /* Fl Fn D Sfa */ VarKEY'Apos':SortInt{}
                    )
                )
            ),

The rule it refers to is:

rule [#lookup.none]:         #lookup( M, KEY ) => 0    requires notBool KEY in_keys(M)

Questions:

1. Should we enable in_keys lemmas for Haskell?
2. Why the predicate above has double negation (\not{R}( \not{R}(...)? It seems to be generated incorrectly.

[ttuegel]

There are rules for the backend which evaluate in_keys.

This predicate:

            \not{R}(
                /* Spc */
                \equals{SortKItem{}, R}(
                    /* Fl Fn D Sfa */ VarKEY:SortKItem{},
                    /* Fl Fn D Sfc */
                    /* Inj: */ inj{SortInt{}, SortKItem{}}(
                        /* Fl Fn D Sfa */ VarKEY'Apos':SortInt{}
                    )
                )
            )

comes from checking that a symbolic Map is defined. This would be a condition required to match some rule, probably the rule for #lookup you mentioned. The double negation appears because we are evaluating \not(\implies(sideCondition, required)); if that predicate is unsatisfiable, then the equation is applied.

[ttuegel]

Fixed by #2147.