Lemma related to set "in" not always applied

[denis-bogdanas]

Not necessary for ERC20 verifier, small workaround works.

module ISSUE
  imports COLLECTIONS
  imports STRING

  configuration <k> $PGM:KItem </k>
                <theSet> .Set </theSet>

    syntax KItem ::= #checkArg ( String )
                   | "#included"
                   | "#notIncluded"

    rule <k> #checkArg(ARG) => #included ...</k>
         <theSet> S </theSet>
      requires ARG in S

    rule <k> #checkArg(ARG) => #notIncluded ...</k>
         <theSet> S </theSet>
      requires notBool ARG in S

    rule X in ((SetItem(A) REST:Set) #as S) => X ==K A orBool X in REST                    [simplification, symbolic(S)]
endmodule

module NOTINCLUDEDSET-SPEC
  imports ISSUE

  rule <k> #checkArg("foo") => #notIncluded </k>
       <theSet> SetItem(A:KItem) </theSet>
    requires A =/=K "foo"
endmodule

Result:

  #Not ( {
    A
  #Equals
    "foo"
  } )
#And
  <generatedTop>
    <k>
      #included
    </k>
    <theSet>
      SetItem ( A )
    </theSet>
  </generatedTop>
#And
  {
    "foo" in SetItem ( A )
  #Equals
    true
  }

Positive specs works:

module INCLUDEDSET-SPEC
  imports ISSUE

  rule <k> #checkArg("foo") => #included </k>
       <theSet> SetItem("foo") SetItem(A:KItem) </theSet>
    requires A =/=K "foo"
endmodule

[andreiburdusa]

I'm not able to run the specs.
I rebuilded both the backend and the frontend using make all, but I still get the error

$ /home/andrei/kore/.build/k/bin/kprove --haskell-backend-command /home/andrei/kore/.build/kore/bin/kore-exec -d . -m INCLUDEDSET-SPEC includedset-spec.k
kore-exec: [2020-04-30 12:44:00.66598074] Error (ErrorException):
    Unexpected empty set of claims.
    Possible explanation: the frontend and the backend don't agree on the representation of claims.
    CallStack (from HasCallStack):
      error, called at src/Kore/Exec.hs:566:26 in kore-0.20.0.0-7yFXMqqWkjaHW436PDhtRm:Kore.Exec
[Error] Critical: Haskell Backend execution failed with code 1 and produced no
output.

Do you have an advice on what else I could try? @ttuegel @ana-pantilie

[ana-pantilie]

@andreiburdusa Did you make clean first? It's possible that could help.

[andreiburdusa]

@andreiburdusa Did you make clean first? It's possible that could help.

Yes, I did

[ttuegel]

The correct command to run the proof is:

/home/andrei/kore/.build/k/bin/kprove --haskell-backend-command /home/andrei/kore/.build/kore/bin/kore-exec -d . -m ISSUE includedset-spec.k

[andreiburdusa]

Now both of the specs work on my machine. @denis-bogdanas Could you also try again please?

[denis-bogdanas]

Good to know, thanks. Will reopen if there are still issues. This feature will help simplify ERC20 verifier a bit.

[denis-bogdanas]

I got a chance to check this. Now the rule is applied even when S is not symbolic
This should expose it:

module NOTINCLUDEDSET-SPEC
  imports ISSUE

  rule <k> #checkArg("foo") => #notIncluded </k>
       <theSet> SetItem("A") </theSet>
endmodule