Types specifying the simplify-implication RPC endpoint
#3614
Conversation
geo2a
force-pushed
the
rpc-simplify-implication
branch
from
640eaf9
to
60990ab
Compare
geo2a
force-pushed
the
rpc-simplify-implication
branch
from
69847a5
to
8785dc9
Compare
geo2a
force-pushed
the
rpc-simplify-implication
branch
3 times, most recently
from
9d6acef
to
3f22ee1
Compare
|
We need a testing harness! Let's make it easy from the start to test these functionalities. |
|
@ehildenb @goodlyrottenapple I've added a stub implementation into I've also extended the RPC API docs. @ehildenb please have a look at the shape of the responses and advise on how we should format them so |
| deriving stock (Generic, Show, Eq) | ||
| deriving | ||
| (FromJSON, ToJSON) | ||
| via CustomJSON '[] ImplicationValidityResult |
There was a problem hiding this comment.
could use the same via CustomJSON '[FieldLabelModifier '[CamelToKebab]] as above. I think this is the naming convention in pyk?
There was a problem hiding this comment.
LGTM @ehildenb @tothtamas28 please let us know if there are any tweaks to the responses you would like
| #### Implication **invalid**: terms do not match | ||
|
|
||
| Matching between antecedent and consequent configurations failed (different constructors, shared variables, sort error, etc.), constraints has not been subsumption been attempted. No matching substitution is returned. | ||
|
|
||
| ``` | ||
| { | ||
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "validity": {"tag": "implication-valid", | ||
| "contents": {"tag": "matching-failed", | ||
| "contents": "Shared variables: X:SortWordStack{}" | ||
| }}, | ||
| } | ||
| } | ||
| ``` |
There was a problem hiding this comment.
The result here should be "unification-failed", and that's what we should be checking. Eventually, if unification succeeds and matching fails, we want ot return an core problem which may or may not be unsat, that the user can then forward to the more powerful implies endpoint.
Just want to make sure that when we get this response back, what it actually means is there is absolutely no overlap between the terms, we know because we found differing constructors.
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "validity": {"tag": "implication-valid", |
There was a problem hiding this comment.
| "validity": {"tag": "implication-valid", | |
| "validity": {"tag": "implication-invalid", |
I think this should likely actually just be unknown result actually, but we return the unsat core (the constarints we arent' sure about).
| #### Implication **unknown**: constraint subsumption indeterminate | ||
|
|
||
| If matching is successful, but the constraint solver procedure (internal, or the SMT solver if enabled) returned "unknown". Response contains the matching substitution and the unknown core of constraints. | ||
|
|
||
| ``` | ||
| { | ||
| "jsonrpc": "2.0", | ||
| "id": 1, | ||
| "result": { | ||
| "validity": {"tag": "implication-unknown", | ||
| "contents": {"tag": "constraint-subsumption-unknown", | ||
| "contents": {"tag": "constraint-subsumption-failed", | ||
| "contents": {"format": "KORE", "version": 1, "term": {}} | ||
| }}, | ||
| "substitution": {"format": "KORE", "version": 1, "term": {}}, | ||
| } | ||
| } | ||
| ``` |
There was a problem hiding this comment.
How is this different than "Implication invalid: terms match, but constraints subsumption failed"
There was a problem hiding this comment.
I thought, we'd want to have a tri-state constraint subsumption check, just like we have a tri-stat matching routine. But perhaps we can indeed expose the "failed" and "unknown" constraint subsumption as just "failed" and have less user-facing cases.
There was a problem hiding this comment.
Part of the confusion for me is that for the failure cases, you're using "terms don't match" as the criteria, but that's not how the tri-state matching algorithm works. It either reports back:
- Terms match with substitution alpha.
- Terms definitely don't unify.
- Unknown.
The key here is that unification and matching are different algorithms, different complexities, and different properties. Saying a term matches another means it's completely subsumed, and saying that they don't unify means they have no overlap.
So I guess the language here needs to be cleared up, because here for example
we're saying "terms don't match" because of differing constructor, where I think it should be saying "terms don't unify".
Unification and matching are not interchangeable. See https://github.com/runtimeverification/hs-backend-booster/issues/193 again for the desired interface.
This PR modifies
kore-rpc-typesto include types that specify the newsimplify-implicationRPC endpoint. Based on the specification in #3787.Note that the CI fails due to Z3 starvation, which is unrelated to these changes.