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.