From ac46fa3d2fffaf03a252998ce267f28b1b8eceb3 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 18 Jun 2026 04:54:20 +0000 Subject: [PATCH 1/4] deps/haskell-backend_release: Set Version v0.1.155 --- deps/haskell-backend_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index d2140ecd43..942cf53967 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -v0.1.154 +v0.1.155 From 90eec8c668c818bedd801667f5e962fd0e39bea6 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 18 Jun 2026 04:55:18 +0000 Subject: [PATCH 2/4] flake.nix, haskell-backend/src/main/native/haskell-backend: update to version v0.1.155 --- flake.nix | 2 +- haskell-backend/src/main/native/haskell-backend | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/flake.nix b/flake.nix index 0e58f7dedb..f1a1650d98 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ llvm-backend.inputs.nixpkgs.follows = "nixpkgs"; haskell-backend = { - url = "github:runtimeverification/haskell-backend/v0.1.154"; + url = "github:runtimeverification/haskell-backend/v0.1.155"; inputs.rv-nix-tools.follows = "rv-nix-tools"; inputs.nixpkgs.follows = "nixpkgs"; }; diff --git a/haskell-backend/src/main/native/haskell-backend b/haskell-backend/src/main/native/haskell-backend index 2107c737b2..38afc81fc9 160000 --- a/haskell-backend/src/main/native/haskell-backend +++ b/haskell-backend/src/main/native/haskell-backend @@ -1 +1 @@ -Subproject commit 2107c737b2f4cc8533f5947006f75573e00f5ddf +Subproject commit 38afc81fc9414f1e11e609b01a43a436b613bd2d From 670e2602448f9865c4e5d34d24f10551a8173dfb Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 18 Jun 2026 04:57:25 +0000 Subject: [PATCH 3/4] flake.lock: update --- flake.lock | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index 6b0339bde6..9908c85c5a 100644 --- a/flake.lock +++ b/flake.lock @@ -64,16 +64,16 @@ "z3": "z3" }, "locked": { - "lastModified": 1781642796, - "narHash": "sha256-/XdSB77sCXg4YypI7Xz7ISqBW8GRqpg2oeSzKS0eaMs=", + "lastModified": 1781757330, + "narHash": "sha256-bUd4OrjJ3cMXhMkSN21tAG3ShgwCGR9j1SW1GsK0YrA=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "2107c737b2f4cc8533f5947006f75573e00f5ddf", + "rev": "38afc81fc9414f1e11e609b01a43a436b613bd2d", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.154", + "ref": "v0.1.155", "repo": "haskell-backend", "type": "github" } From 585190f34734b335ef6970d442d1684b8a90dd97 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 18 Jun 2026 05:16:41 +0000 Subject: [PATCH 4/4] 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 --- pyk/src/pyk/kore/rpc.py | 8 +++++++- pyk/src/tests/unit/kore/test_client.py | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 099c86839f..bcd1b03720 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -937,8 +937,14 @@ def from_dict(dct: Mapping[str, Any]) -> ImpliesResult: substitution = dct.get('condition', {}).get('substitution') predicate = dct.get('condition', {}).get('predicate') logs = tuple(LogEntry.from_dict(l) for l in dct['logs']) if 'logs' in dct else () + # The backend reports a tri-state `status`: valid | invalid | indeterminate. + # `indeterminate` is booster's "could not decide" signal; the kore-rpc proxy + # escalates it to a decisive kore verdict on every path except booster-only + # mode, so it only reaches us when the caller explicitly opted out of kore. + # Collapse it to `valid = False` — the conservative not-implied answer the + # binary consumers expect. return ImpliesResult( - valid=dct['valid'], + valid=dct['status'] == 'valid', implication=kore_term(dct['implication']), substitution=kore_term(substitution) if substitution is not None else None, predicate=kore_term(predicate) if predicate is not None else None, diff --git a/pyk/src/tests/unit/kore/test_client.py b/pyk/src/tests/unit/kore/test_client.py index e93e4558c2..426e322de8 100644 --- a/pyk/src/tests/unit/kore/test_client.py +++ b/pyk/src/tests/unit/kore/test_client.py @@ -178,7 +178,7 @@ def test_execute( int_bottom, int_top, {'antecedent': kore(int_bottom), 'consequent': kore(int_top), 'assume-defined': False}, - {'valid': True, 'implication': kore(int_top)}, + {'status': 'valid', 'implication': kore(int_top)}, ImpliesResult(True, int_top, None, None, ()), ), )