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 #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 #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. 🚀

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?