Booster's and Kore's `"implies"` endpoints disagree on a `pyk` integration test

[geo2a]

The HB update pr to K fails two pyk integrations tests:

FAILED src/tests/integration/kore/test_kore_client.py::TestKoreClient::test_implies_error[booster-0 -> X]
FAILED src/tests/integration/proof/test_imp.py::TestImpProof::test_implies[booster-antecedent-bottom]

In the first test, Booster returns a non-empty substitution and an empty predicate, while Kore returns an empty substitution and #Bottom as predicate, which is also the expected output.

AssertionError: assert CSubst(subst=Subst(_subst=FrozenDict({'Y': KVariable(name='X', sort=KSort(name='Int'))})), constraints=()) == CSubst(subst=Subst(_subst=FrozenDict({})), constraints=(KApply(label=KLabel(name='#Bottom', params=(KSort(name='GeneratedTopCell'),)), args=()),))

In the second test, an error response (indicated by an exception in KoreClient) is expected, but no exception is raised. I've modified test to compare the output to None in order to see the responses:

FAILED src/tests/integration/kore/test_kore_client.py::TestKoreClient::test_implies_error[legacy-0 -> X] - pyk.kore.rpc.ImplicationError: Implication check error: The RHS must not have free variables not present in the LHS: Configx Context: LHS: \dv{SortInt{}}("0") ;; RHS: Configx:SortInt{} ;; existentials: []

FAILED src/tests/integration/kore/test_kore_client.py::TestKoreClient::test_implies_error[legacy-X -> Y] - pyk.kore.rpc.ImplicationError: Implication check error: The RHS must not have free variables not present in the LHS: Configy Context: LHS: Configx:SortInt{} ;; RHS: Configy:SortInt{} ;; existentials: []

FAILED src/tests/integration/kore/test_kore_client.py::TestKoreClient::test_implies_error[booster-0 -> X] - AssertionError: assert ImpliesResult(valid=True, implication=Implies(sort=SortApp(name='SortInt', sorts=()), left=DV(sort=SortApp(name='SortInt', sorts=()), value=String(value='0')), right=EVar(name='x', sort=SortApp(name='SortInt', sorts=()))), substitution=And(sort=SortApp(name='SortInt', sorts=()), ops=(Equals(op_sort=SortApp(name='SortInt', sorts=()), sort=SortApp(name='SortInt', sorts=()), left=EVar(name='x', sort=SortApp(name='SortInt', sorts=())), right=DV(sort=SortApp(name='SortInt', sorts=()), value=String(value='0'))),)), predicate=Top(sort=SortApp(name='SortInt', sorts=())), logs=()) == None

FAILED src/tests/integration/kore/test_kore_client.py::TestKoreClient::test_implies_error[booster-X -> Y] - AssertionError: assert ImpliesResult(valid=True, implication=Implies(sort=SortApp(name='SortInt', sorts=()), left=EVar(name='x', sort=SortApp(name='SortInt', sorts=())), right=EVar(name='y', sort=SortApp(name='SortInt', sorts=()))), substitution=And(sort=SortApp(name='SortInt', sorts=()), ops=(Equals(op_sort=SortApp(name='SortInt', sorts=()), sort=SortApp(name='SortInt', sorts=()), left=EVar(name='y', sort=SortApp(name='SortInt', sorts=())), right=EVar(name='x', sort=SortApp(name='SortInt', sorts=()))),)), predicate=Top(sort=SortApp(name='SortInt', sorts=())), logs=()) == None

this reveals that Kore returns an error, while Booster does not.

[goodlyrottenapple]

I suspect checking whether the antecedent/consequent is #Bottom will negate any speed gains we got from implementing the simple implication check, as this would just be a call to the kore simplifier anyway :/

[geo2a]

I agree that simplifying both antecedent and consequent would probably kill the performance.

Perhaps we need to re-think the how we use the implies endpoint a little. As I understand, we currently have two use-cases for it:

• the subsumption check, implemented by the CTermSymbolic.implies method,
• the equatlity and refutation proofs, and the ImpliesProver class to discharge them.

Perhaps we could indeed implement @ehildenb original idea and have two endpoints: a lightweight "simplify-implication" (or some other name), and a the old "implies". The lightweight one will have additional assumptions:

• neither antecedent not consequent are bottom
• perhaps something else?
  we can than use "simplify-implication" without fear in the subsumption check scenario, because:
• the pyk prover simplifies the target configuration anyway, and we know it is not bottom
• kore-rpc-booster simplifies with Kore the states after the terminal and cut-point rules, therefore pyk will know if they are bottom and can ensure the precondition of "simplify-implication". We can than shift the call to the simplifier into pyk if we want.

the old "implies" endpoint can still be used for the equality proofs.

[goodlyrottenapple]

We should use a basic ceil checker in booster to re-enable the new implication endpoint and port the pyk tests into booster to check that the new implication endpoint can handle them correctly.

[Stevengre]

Both disagreements reported here are resolved, and the two failing pyk integration tests now pass against current kore-rpc-booster.

Disagreement 1 — test_implies[booster-antecedent-bottom] (unsat antecedent).
Booster now detects an unsatisfiable antecedent up front (an SMT.isSat check on the antecedent constraints in Booster.Pattern.Implies) and returns valid with a #Bottom predicate, matching Kore.
Introduced in #4060.

Disagreement 2 — test_implies_error[booster-0 -> X] / [booster-X -> Y] (RHS free variable).
Booster now computes the RHS-minus-LHS free variables and, when non-empty, returns the same ImplicationCheckError ("The RHS must not have free variables not present in the LHS") that Kore raises.
Introduced in #4026.

Verification.
Re-ran the exact tests from this issue against a build of current master (163997f9b, = release-0.1.155):

$ pytest src/tests/integration/kore/test_kore_client.py::TestKoreClient::test_implies_error \
         src/tests/integration/proof/test_imp.py::TestImpProof::test_implies \
         --use-server booster

test_kore_client.py::TestKoreClient::test_implies_error[booster-0 -> X]   PASSED
test_kore_client.py::TestKoreClient::test_implies_error[booster-X -> Y]   PASSED
test_imp.py::TestImpProof::test_implies[booster-antecedent-bottom]        PASSED
... 14 passed, 16 skipped

(K checkout v7.1.337, whose pyk already decodes the post-#4156 tri-state status field.)

These tests run on every K PR in the Pyk: Integration Tests job (make test-integration, --use-server both) against the pinned deps/haskell-backend_release (currently v0.1.155, which contains the fixes), so the agreement is now CI-guarded.

Closing as fixed.