Unsat config isn't getting simplified

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.

Reproduce the discrepancy with spec.k using kprove, then start the kore-rpc server and call its execute endpoint with request.json. Compare response.json with next1.pretty, next2.pretty, condition1.pretty, and condition2.pretty from kore-rpc-debug.zip; the work is done when the project has a decided, consistent treatment of initial-term well-definedness.