Skip to content

Commit 585190f

Browse files
ehildenbclaude
andcommitted
pyk/kore/rpc, tests/unit/kore/test_client: parse implies status tri-state
haskell-backend v0.1.155 replaces the implies `valid :: Bool` field with a `status` tri-state (valid | invalid | indeterminate). Parse `status` in `ImpliesResult.from_dict`, collapsing to `valid = (status == 'valid')`. The kore-rpc proxy escalates `indeterminate` to a decisive kore verdict except in booster-only mode, so the conservative collapse is sound for the binary consumers. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 670e260 commit 585190f

2 files changed

Lines changed: 8 additions & 2 deletions

File tree

pyk/src/pyk/kore/rpc.py

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -937,8 +937,14 @@ def from_dict(dct: Mapping[str, Any]) -> ImpliesResult:
937937
substitution = dct.get('condition', {}).get('substitution')
938938
predicate = dct.get('condition', {}).get('predicate')
939939
logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else ()
940+
# The backend reports a tri-state `status`: valid | invalid | indeterminate.
941+
# `indeterminate` is booster's "could not decide" signal; the kore-rpc proxy
942+
# escalates it to a decisive kore verdict on every path except booster-only
943+
# mode, so it only reaches us when the caller explicitly opted out of kore.
944+
# Collapse it to `valid = False` — the conservative not-implied answer the
945+
# binary consumers expect.
940946
return ImpliesResult(
941-
valid=dct['valid'],
947+
valid=dct['status'] == 'valid',
942948
implication=kore_term(dct['implication']),
943949
substitution=kore_term(substitution) if substitution is not None else None,
944950
predicate=kore_term(predicate) if predicate is not None else None,

pyk/src/tests/unit/kore/test_client.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ def test_execute(
178178
int_bottom,
179179
int_top,
180180
{'antecedent': kore(int_bottom), 'consequent': kore(int_top), 'assume-defined': False},
181-
{'valid': True, 'implication': kore(int_top)},
181+
{'status': 'valid', 'implication': kore(int_top)},
182182
ImpliesResult(True, int_top, None, None, ()),
183183
),
184184
)

0 commit comments

Comments
 (0)