Commit b1419c1
Update dependency: deps/haskell-backend_release (#4935)
Bumps `deps/haskell-backend_release` to `v0.1.155`. This release
replaces the `implies` RPC result's `valid :: Bool` field with a
`status` tri-state (`valid` | `invalid` | `indeterminate`), so pyk's
response parsing is updated in lockstep.
`indeterminate` is booster's "could not decide" signal (an indeterminate
match or an SMT-unknown obligation). The kore-rpc proxy escalates it to
a decisive kore verdict on every path except booster-only mode, so it
only reaches a client that explicitly opted out of kore; pyk collapses
it to the conservative not-implied answer for its binary consumers.
**Changes:**
- Update `deps/haskell-backend_release`, `flake.{nix,lock}`, and the
`haskell-backend` submodule to `v0.1.155`.
- Parse the new `status` field in `ImpliesResult.from_dict`
(`pyk/src/pyk/kore/rpc.py`), deriving `valid = (status == 'valid')`.
- Migrate the `implies` mock-response unit fixture from `valid` to
`status`.
**Validation:**
- `make -C pyk check` clean; full pyk unit suite (1769 tests) passes,
including `test_implies`.
- Verified no other recorded RPC fixtures in the repo encode the old
`valid` field — integration tests drive a live backend and compare
against constructed `ImpliesResult` objects.
---------
Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>1 parent 3b9cd43 commit b1419c1
6 files changed
Lines changed: 15 additions & 9 deletions
File tree
- deps
- haskell-backend/src/main/native
- pyk/src
- pyk/kore
- tests/unit/kore
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | | - | |
| 1 | + | |
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
8 | 8 | | |
9 | 9 | | |
10 | 10 | | |
11 | | - | |
| 11 | + | |
12 | 12 | | |
13 | 13 | | |
14 | 14 | | |
| |||
Submodule haskell-backend updated 70 files
- booster/hs-backend-booster.cabal+1-1
- booster/library/Booster/Pattern/Implies.hs+100-60
- booster/package.yaml+1-1
- booster/test/rpc-integration/resources/implies-smt.k+22
- booster/test/rpc-integration/resources/implies-smt.kompile+6
- booster/test/rpc-integration/test-3934-smt/response-003.booster-dev+1-1
- booster/test/rpc-integration/test-3934-smt/response-003.json+1-1
- booster/test/rpc-integration/test-3934-smt/response-005.booster-dev+1-1
- booster/test/rpc-integration/test-3934-smt/response-005.json+1-1
- booster/test/rpc-integration/test-3934-smt/response-007.booster-dev+1-1
- booster/test/rpc-integration/test-3934-smt/response-007.json+1-1
- booster/test/rpc-integration/test-foundry-bug-report/response-006.json+1-1
- booster/test/rpc-integration/test-foundry-bug-report/response-008.json+1-1
- booster/test/rpc-integration/test-foundry-bug-report/response-010.json+1-1
- booster/test/rpc-integration/test-foundry-bug-report/response-012.json+1-1
- booster/test/rpc-integration/test-foundry-bug-report/response-014.json+1-1
- booster/test/rpc-integration/test-foundry-bug-report/response-016.json+1-1
- booster/test/rpc-integration/test-implies-issue-3941/response-001.booster-dev+1-1
- booster/test/rpc-integration/test-implies-issue-3941/response-001.json+1-1
- booster/test/rpc-integration/test-implies-smt/README.md+20
- booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.booster-dev+63
- booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.json+177
- booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.booster-dev+37
- booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.json+177
- booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.booster-dev+209
- booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.json+234
- booster/test/rpc-integration/test-implies-smt/response-004-address-bound.booster-dev+63
- booster/test/rpc-integration/test-implies-smt/response-004-address-bound.json+234
- booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.booster-dev+37
- booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.json+177
- booster/test/rpc-integration/test-implies-smt/state-001-bound-weakening.send+59
- booster/test/rpc-integration/test-implies-smt/state-002-does-not-imply.send+59
- booster/test/rpc-integration/test-implies-smt/state-003-vacuous-antecedent.send+75
- booster/test/rpc-integration/test-implies-smt/state-004-address-bound.send+75
- booster/test/rpc-integration/test-implies-smt/state-005-escalate-indeterminate.send+148
- booster/test/rpc-integration/test-implies/response-0->1.json+1-1
- booster/test/rpc-integration/test-implies/response-0->B.json+1-1
- booster/test/rpc-integration/test-implies/response-0->T.json+1-1
- booster/test/rpc-integration/test-implies/response-B->0.json+1-1
- booster/test/rpc-integration/test-implies/response-X->0.booster-dev+1-1
- booster/test/rpc-integration/test-implies/response-X->0.json+1-1
- booster/test/rpc-integration/test-implies/response-X->T.json+1-1
- booster/test/rpc-integration/test-implies/response-X->X.json+1-1
- booster/test/rpc-integration/test-implies/response-fail-0->X.json+1-1
- booster/test/rpc-integration/test-implies2/response-antecedent-bottom.json+1-1
- booster/test/rpc-integration/test-implies2/response-consequent-constraint.booster-dev+352-4
- booster/test/rpc-integration/test-implies2/response-consequent-constraint.json+1-1
- booster/test/rpc-integration/test-implies2/response-constant-subst.json+1-1
- booster/test/rpc-integration/test-implies2/response-refutation-1.booster-dev+320-4
- booster/test/rpc-integration/test-implies2/response-refutation-1.json+1-1
- booster/test/rpc-integration/test-implies2/response-refutation-3.booster-dev+334-4
- booster/test/rpc-integration/test-implies2/response-refutation-3.json+1-1
- booster/test/rpc-integration/test-implies2/response-refutation-4.booster-dev+348-4
- booster/test/rpc-integration/test-implies2/response-refutation-4.json+1-1
- booster/test/rpc-integration/test-implies2/response-trivial.json+1-1
- booster/test/rpc-integration/test-implies2/response-variable-subst.json+1-1
- booster/tools/booster/Proxy.hs+31-23
- dev-tools/hs-backend-booster-dev-tools.cabal+1-1
- dev-tools/package.yaml+1-1
- kore-rpc-types/kore-rpc-types.cabal+1-1
- kore-rpc-types/src/Kore/JsonRpc/Types.hs+20-1
- kore/kore.cabal+1-1
- kore/src/Kore/JsonRpc.hs+5-5
- package/debian/changelog+1-1
- package/version+1-1
- scripts/booster-integration-tests.sh+1-1
- test/rpc-server/implies/implied-substitution/response.golden+1-1
- test/rpc-server/implies/implied-trivial/response.golden+1-1
- test/rpc-server/implies/not-implied-stuck/response.golden+1-1
- test/rpc-server/implies/not-implied/response.golden+1-1
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
937 | 937 | | |
938 | 938 | | |
939 | 939 | | |
| 940 | + | |
| 941 | + | |
| 942 | + | |
| 943 | + | |
| 944 | + | |
| 945 | + | |
940 | 946 | | |
941 | | - | |
| 947 | + | |
942 | 948 | | |
943 | 949 | | |
944 | 950 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
178 | 178 | | |
179 | 179 | | |
180 | 180 | | |
181 | | - | |
| 181 | + | |
182 | 182 | | |
183 | 183 | | |
184 | 184 | | |
| |||
0 commit comments