Unsat config isn't getting simplified

[tothtamas28]

kprove and kore-rpc seem to disagree on whether they assume well-definedness of the LHS / initial term.

Let's discuss potential solutions. Valid answers include the following.

1. kore-rpc should not assume well-definedness of the initial term, nothing to be done.
2. kore-rpc should not assume well-definedness of the initial term, but it should indicate that a branch leads to such a term.
3. kore-rpc should assume well-definedness of the initial term.
4. kore-rpc should support both modes, e.g. by introducing a command line flag.

Resources

K version:    v5.4.7-0-g0b0189cc60
Build date:   Tue Sep 27 13:19:45 CEST 2022

kore-rpc-debug.zip

kore-rpc-debug
├── condition1.kore
├── condition1.pretty
├── condition2.kore
├── condition2.pretty
├── imp.k
├── imp-verification.k
├── init.kore
├── init.kore.json
├── init.pretty
├── next1.kore
├── next1.pretty
├── next2.kore
├── next2.pretty
├── report.tar.gz
├── request.json
├── response.json
└── spec.k

kprove behavior

Consider the following specification spec.k.

// spec.k
requires "imp-verification.k"

module SPEC
    imports IMP-VERIFICATION

    claim <T>
            <k> $n = 1 ; => . </k>
            <state> $n |-> ( 0 => 1 ) _STATE_CELL </state>
          </T>
endmodule

When running

% kprove spec.k

the prover returns #Top.

kore-rpc behavior

First, start the server.

% kore-rpc imp-verification-kompiled/definition.kore  --module IMP-VERIFICATION --server-port 3000

Then, call the execute endpoint.

% netcat -q 0 localhost 3000 < request.json > response.json

Here, request.json is derived from init.pretty, which corresponds to the LHS of the claim above.

// init.pretty
<generatedTop>
    <T>
        <k> $n = 1 ; </k>
        <state> $n |-> 0 STATE_CELL </state>
    </T>
    <generatedCounter>
        0
    </generatedCounter>
</generatedTop>

The response is branching at depth 0. The corresponding next states and predicates are as follows.

// next1.pretty
<T>
  <k>
    .
  </k>
  <state>
    $n |-> 1
    STATE_CELL
  </state>
</T>

// condition1.pretty
{
  false
#Equals
  $n in_keys ( STATE_CELL )
}

and

// next2.pretty
<T>
  <k>
    $n = 1; ~> .
  </k>
  <state>
    $n |-> 0
    STATE_CELL
  </state>
</T>

// condition2.pretty
#Not ( {
  false
#Equals
  $n in_keys ( STATE_CELL )
} )

The two branches disagree on whether cell <state> is well-defined. This however seems to be assumed by kprove, otherwise the LHS would have been a counterexample for the reachability claim.

[ehildenb]

@tothtamas28 what happens if we have an initial term like this: T #And C1 #And ... #And CN, and we first change it to this term in pyk before sending it to the backend: ((T #And C1 #And ... #And CN) #as CT) #And #Ceil(CT), so that we are just stating, from the beginning, that the term is well-defined?

This would allow the user to decide whether they want to state that it's well defined, by just saying it, and maybe the backend will already accept this term? You may have to look into how _#as_ patterns are encoded to Kore, I believe it's sugar for some other formulae.

This also seems to leave less "magic" in the backend, about it automatically adding things, allowing the tool on top to make that decision.

[ana-pantilie]

Why do you need the #as? I think if C1 ... CN are predicates then #Ceil(T #And C1 #And ... #And CN) should be equivalent to T #And C1 #And ... #And CN #And #Ceil(T).

[ana-pantilie]

By the way, this issue is actually a duplicate of https://github.com/runtimeverification/haskell-backend/issues/2428.

Unless something goes terribly wrong, I can push a quick fix which should make it behave the same as kprove does now.

After that, we've been talking about doing https://github.com/runtimeverification/haskell-backend/issues/3175.

The question is, do we want the backend to assume definedness of the configuration by default or not? For proving, the answer is most definitely yes because the branch where the configuration is not defined makes the proof trivial. For simple symbolic execution, I guess it's not that clear.

[tothtamas28]

what happens if we have an initial term like this: T #And C1 #And ... #And CN, and we first change it to this term in pyk before sending it to the backend: ((T #And C1 #And ... #And CN) #as CT) #And #Ceil(CT), so that we are just stating, from the beginning, that the term is well-defined?

It works. :rocket:

You may have to look into how #as patterns are encoded to Kore, I believe it's sugar for some other formulae.

It looks like it is translated to \and (at least that's what kast does with the term).

[ehildenb]

It's not the same issue, we don't necessarily want symbolic execution and kprove to have the same behavior.

I'd rather the user be explicit about needing definedness, and the _#as_ is the quickest pattern to build without having to sift through the configuration, so that's why I suggested that.

If it works, then it seems a good solution to me. It requires that the user explicitely tell the backend that the initial configuration is defined.

[ehildenb]

And yes, _#as_ is translated to #And, which means the predicates will be deduplicated. So if we wanted to skip that step in the backend wecould just add #And(C), it just means th eterm we're passing is larger I guess.

We could also do: CONFIGURATION #And C1 #And C1 #And ... #And CN #And FRESH_CONFIG_VAR #Ceil(FRESH_CONFIG_VAR)

This is just two calls to CTerm.add_constraint, which means we should be able to expose fast-path direct Kore manipulation for this (instead of doing round trip Kore -> Kast -> Kore to do the manipulation).

[ehildenb]

@nishantjr pointed out that V #And #Ceil(V) is redundant, because variables are always defined. So it should be enough to just add ... #And FRESH_CONFIG_VAR to force the initial config to be defined.

[nishantjr]

First, note for any configuration CT, CT and CT #and Ceil(CT) are semantically equivalent. If CT is Bottom, then Ceil(CT) is also Bottom, otherwise Ceil(CT) is Top and the conjunction equals CT. This means that solutions 1 and 3 in the description are semantically the same.

Second, the next2 branch here is equals Bottom (Map union semantics) and the disjunction pretty1 \/ pretty2 is semantically equivalent to the initial configuration. I think the Haskell backend should already be able to figure this out and simplify it away. I think we just want to check that at least two branches do not simplify to #Bottom before declaring a branch point.

[tothtamas28]

@nishantjr pointed out that V #And #Ceil(V) is redundant, because variables are always defined. So it should be enough to just add ... #And FRESH_CONFIG_VAR to force the initial config to be defined.

I tried this with

  <T>
    <k>
      $n = 1; ~> .
    </k>
    <state>
      $n |-> 0
      STATE_CELL
    </state>
  </T>
#And
  CT

The result is the same branching response as for the original request (except now substitution is present in the response).

[nishantjr]

@tothtamas28 To me it looks like we need to modify kore-rpc to perform simplification and prune any branch that simplifies to #Bottom, as pretty2 should. Then, since there is only one configuration in the disjunction this point is no longer a branch point.

[ehildenb]

So you're suggestiong that the pyk exploration strategy just recognize this particular branch as "one of these is undefined", and store it separately/specially?

[ana-pantilie]

@nishantjr is right, one of the branches in the example for some reason does not get simplified away by the backend and it should.

Basically, in practice, if we don't have https://github.com/runtimeverification/haskell-backend/pull/3290 or the user supplying \\ceil(term) as a condition, the backend will branch on every partial configuration. One of these branches will be immediately pruned the next step.

If you guys are not interested in these branches at all, then https://github.com/runtimeverification/haskell-backend/pull/3290 would be the way to go. If you are, then we need to know in what way you're interested. Do you want the backend to treat this as a branch, so to stop executing, and let you handle result? Do you want the backend to continue executing but emit a warning?

[nishantjr]

@ehildenb That would be one way, though as @ana-pantilie says, we're probably never interested in these configurations that simplify to bottom or the corresponding branch points, and we can always assume the definedness conditions of the configuration. I don't think it makes sense to give users the choice of whether or not to add the definedness condition, because it is equivalent to not having those conditions (they may be inferred from the initial configuration).

[ehildenb]

I do not think we are "not interested" in them, just "not as interested". We should let the user know that there was a portion of their initial configuration that was undefined, because that is likely not their intention, and the divide-by-zero error is one example that is important, but also in KEVM we have conditions like "account exists" and such which are important (map definedness, set definedness).

But I definitely don't think the backend should just silently ignore these states. We have to let the user know somehow.

So that's why I would argue for leaving it in the pyk library, which means leaving that decision in pyk. Users of the pyk library can make their own choice about whether to add the needed definedness conditions at the start, and pyk can also automatically recognize that this is an uninteresting branch itself (if it wants to make that decision for th eroutine it's running), and navigate past it directly by selecting the defined branch.

Remeber that we are not doing kprove here, we are doing execute-to-branch, there is no "target" state, and there is no notion of "trivially true", we are just doing controlled state space exploration. If part of our state space is undefined, we want to know.

[ana-pantilie]

Alright, then I'll convert this issue into one for investigating why that unsatisfiable configuration doesn't get simplified.

[Sereja313]

@ana-pantilie I managed to reproduce this error. backend version:

Kore version 0.60.0.0
Git:
  revision: 74bc7a963a825d0f0f034b5d3412dc59448e51bb (dirty)
  branch:   master
  last commit:  Tue Feb 7 05:02:49 2023 -0700