Function in main condition not reevaluated after split

virgil-serbanuta commented 3 years ago

To reproduce (at commit ac02ece7a215aa85b32bd1cb7d4211328f3353f9):

tmp.k:

module TMP
  imports INT
  imports K-EQUAL

  syntax KItem ::= a(Int, Int) | "stuck"
  syntax Int ::= f(Int, Int)  [function, functional]

  rule f(X, X) => -1
  rule f(_, _) => 1  [owise]

  rule a(X, X) => .K
  rule a(X, Y) => stuck requires X =/=K Y

endmodule

proof-tmp.k

module PROOF-TMP
  imports TMP

  claim a(X, Y) => .K requires f(X, Y) <Int 0

endmodule

command line:

kompile tmp.k --backend haskell && kprove proof-tmp.k

Expected: proof passes

Actual:

kore-exec: [442843] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The claim cannot be rewritten further, and the claimed implication is not valid. /mnt/data/runtime-verification/elrond-multisig-2/tmp/proof-tmp.k:4:9-4:46
  #Not ( {
    X
  #Equals
    Y
  } )
#And
  <k>
    stuck ~> _DotVar1 ~> .
  </k>
#And
  {
    true
  #Equals
    f ( X , Y ) <Int 0
  }

I think that f ( X , Y ) should be evaluated using rule f(_, _) => 1 [owise], and the stuck branch should be pruned.

Information for myself: The original proof is protocol-correctness/proof/malicious-user/can-be-deleted/run-external-call-from-user/proof-recfu-unsign-void.k.

ana-pantilie commented 2 years ago

Is this still failing after ed422630f9383b2774f1ec8ea04eee86ea0afe1e?

virgil-serbanuta commented 2 years ago

I'm currently re-running the multisig proofs with the latest Haskell backend, but it will take a while. I'll post an update when done.

virgil-serbanuta commented 2 years ago

Hm, this will take even more time than I thought - after upgrading the backend, some of the tests are branching much more, which confuses my infrastructure (usually the new branches end one step because the backend detects that they are infeasible, so I guess that everything is fine; my infrastructure checks that the number of branches does not increase because that usually means that I changed a trusted claim which does not apply anymore).

virgil-serbanuta commented 2 years ago

The original proof is passing now. I did not test the example provided in the bug report.

virgil-serbanuta commented 2 years ago

Sorry, the previous comment was a bit premature, I misinterpreted the last test results, I still have to run that proof manually.

virgil-serbanuta commented 2 years ago

Sorry for all the previous noise, this is not fixed.

ana-pantilie commented 2 years ago

Thank you for checking!

ana-pantilie commented 2 years ago

@emarzion https://github.com/kframework/kore/wiki/Debugging#function-evaluation

ana-pantilie commented 2 years ago

Update:

The owise equation doesn't apply because the SideCondition never contains the required predicate, X =/=K Y. It looks like this is happening because the MultiAnd Predicate sent to simplifyPredicates (which simplifies each predicate using the others as side conditions) isn't normalized correctly. More exactly, instead of having the ... f(X, Y) ... predicate and the X =/=K Y predicates separate inside the MultiAnd, they appear together as a single element of the MultiAnd: (... f(X, Y) ...) #And (X =/=K Y).

I need to investigate further to see why this is happening.

Edit: I actually found one instance where the two predicates are split up correctly, and X =/=K Y actually appears as a side condition which should be used to simplify the ... f(X, Y) ... predicate:

Predicates:
/* Spa */
\equals{SortBool{}, _}(
    /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"),
    /* Fl Fn D Spa */
    Lbl'Unds-LT-'Int'Unds'{}(
        /* Fl Fn D Spa */
        Lblf'LParUndsCommUndsRParUnds'TEST'Unds'Int'Unds'Int'Unds'Int{}(
            /* Fl Fn D Sfa */ ConfigVarX:SortInt{},
            /* Fl Fn D Sfa */ ConfigVarY:SortInt{}
        ),
        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
    )
)
/* Spa */
\not{_}(
    /* Spa */
    \equals{SortInt{}, _}(
        /* Fl Fn D Sfa */ ConfigVarX:SortInt{},
        /* Fl Fn D Sfa */ ConfigVarY:SortInt{}
    )
)

Side conditions:
/* Spa */
\not{_}(
    /* Spa */
    \equals{SortInt{}, _}(
        /* Fl Fn D Sfa */ ConfigVarX:SortInt{},
        /* Fl Fn D Sfa */ ConfigVarY:SortInt{}
    )
)
\top{_}()

Edit 2: the f(X, Y) appears unevaluated despite the SideCondition having enough information. It looks like the problem has more to do with the equation itself, why isn't it getting attempted with this correct combination of data?

Predicate:
/* Spa */
\equals{SortBool{}, _}(
    /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"),
    /* Fl Fn D Spa */
    Lbl'Unds-LT-'Int'Unds'{}(
        /* Fl Fn D Spa */
        Lblf'LParUndsCommUndsRParUnds'TEST'Unds'Int'Unds'Int'Unds'Int{}(
            /* Fl Fn D Sfa */ ConfigVarX:SortInt{},
            /* Fl Fn D Sfa */ ConfigVarY:SortInt{}
        ),
        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
    )
)

SideCondition
Assumed true condition:
    /* Spa */
    \not{_}(
        /* Spa */
        \equals{SortInt{}, _}(
            /* Fl Fn D Sfa */ ConfigVarX:SortInt{},
            /* Fl Fn D Sfa */ ConfigVarY:SortInt{}
        )
    )
TermLike replacements:
Predicate replacements:
Assumed to be defined:

Result:
/* Sfa */
\equals{SortBool{}, _}(
    /* Fl Fn D Sfa Cl */ \dv{SortBool{}}("true"),
    /* Fl Fn D Sfa */
    Lbl'Unds-LT-'Int'Unds'{}(
        /* Fl Fn D Sfa */
        Lblf'LParUndsCommUndsRParUnds'TEST'Unds'Int'Unds'Int'Unds'Int{}(
            /* Fl Fn D Sfa */ ConfigVarX:SortInt{},
            /* Fl Fn D Sfa */ ConfigVarY:SortInt{}
        ),
        /* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
    )
)

Edit 3: I traced Kore.Equation.Application.attemptEquation. The owise equation is only attempted with a SideCondition which doesn't contain enough information, so the checkRequires step fails. The information is lost somewhere.

The chain of calls looks something like: simplifyPredicates constructs the right collection of data (Predicate: true #Equals f(X, Y) <Int 0 with SideCondition: #Not (X #Equals Y). This is sent to the Predicate simplifier, which should try to simplify the Predicate bottom-up: so this will call the Application simplifier on f(X, Y), which should be able to apply the equation because the SideCondition contains the necessary information, but I couldn't find that information in the traces. Is it erasing info from the SideCondition somewhere before calling Kore.Equation.Application.attemptEquation?

virgil-serbanuta commented 2 years ago

FWIW, I'm not sure if it's the same thing, but I think that one of my proof also contains (true #And #Top) as a single term of the main #And (or something like that it could have been (true andBool #Top), I didn't try yet to figure out the details).

ana-pantilie commented 2 years ago

Unless you're observing that through adding traces to Kore.Simplify.Condition.simplifyPredicates I don't think it's the same thing. The splitting up of conjunctions into, basically, collections of predicates is something internal to the simplifier.

Anyway, I'm still confused about the seemingly unnormalized MultiAnd Predicate, but it looks like the issue is something else.

BTW, I'm adding this info in the comments in order to keep track of progress and to show the Haskell backend team how I'm debugging the issue.

ana-pantilie commented 2 years ago

Aha! I found the culprit 😄. It's the check here: https://github.com/kframework/kore/blob/f5bed2d571628241f68c37e22d0bacb15094b6ee/kore/src/Kore/Simplify/Application.hs#L129

For some reason, the simplifier has marked the function as simplified for the SideCondition which contains the necessary information, so we don't actually attempt to evaluate with it. The question now is, why did it do that?

Edit: I've figured it out. We should delete the cache of simplified functions whenever the SideCondition changes, since we're adding information which could possibly help evaluate some of the functions we've encountered before.

ana-pantilie commented 2 years ago

@virgil-serbanuta Is this issue blocking you?

virgil-serbanuta commented 2 years ago

TL/DR:

It's not blocking in the sense that I can still work on my Multisig project. However, I won't be able to finish them without this issue being fixed or without a workaround.

Longer answer:

I have 8 proofs that seem to be affected by this issue (I'm not 100% sure that #2829 applies to all of them; it certainly seems so, but it's hard to be sure). I have a workaround for 6 of them: I forced one of the subterms to be evaluated to something more concrete (e.g. a list being forced to be either the empty list, or cons(element, list)), which causes the entire term to be re-evaluated. However, this is harder to do for the remaining 2 proofs.

If this is hard to fix, I can try again to find a workaround for the remaining proofs. I hope that I can find something more sane, but, in the extreme, for each function f(x) I could add an argument that does not influence its evaluation (e.g. f(X:Int) => g(X) +Int 1 could be transformed into f(X:Int, Dummy:Concretizer) => g(X, Dummy) +Int 1), but which I could make more concrete on-demand. To be specific, I would have a variable Dummy that I would keep it in the configuration and which would be used by all functions. Its sort could be defined as syntax Concretizer ::= s(Concretizer), and I could force Dummy to be s(?Dummy) whenever I need reevaluation. I don't know yet if either Z3 or the Haskell backend would have any problems with a sort that does not have elements that can be constructed, though (probably not).

I can probably also try to rewrite the proofs so that any function has all the conditions it needs for evaluation at the moment it shows up in the predicate, but, based on past experience, it will result in more complicated proofs, with a lot more early branching, with many branches not actually being needed. Even if that's possible, doing it in the obvious way for the two remaining proofs is likely to result in an infeasible execution time, so I'll have to think more about this.

Also, one of the following options may help (I can't say for sure that they do):

Fully re-evaluating patterns after splits - The linked PR seems to do that, but I'm not fully sure why that's not good enough - does it cause performance issues?
Some kind of hook or something else that allows me to ask the Haskell backend to fully re-evaluate the current pattern (i.e. both the term and the predicate).
Fully re-evaluating a pattern that gets stuck (this might solve some, but, most likely, not all of the 8 proofs mentioned above).

ana-pantilie commented 2 years ago

https://github.com/kframework/kore/pull/2925 this branch contains the fix for this. Unfortunately it comes with a big performance regression on some tests. If the regression doesn't affect you, then I'd suggest working on this branch for the time being. If the slowdown affects you, let me know and we'll re-prioritize it.

runtimeverification / haskell-backend

Function in main condition not reevaluated after split #2829