Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deps/haskell-backend_release
Original file line number Diff line number Diff line change
@@ -1 +1 @@
v0.1.154
v0.1.155
8 changes: 4 additions & 4 deletions flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
Original file line number Diff line number Diff line change
Expand Up @@ -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";
};
Expand Down
2 changes: 1 addition & 1 deletion haskell-backend/src/main/native/haskell-backend
Submodule haskell-backend updated 70 files
+1 −1 booster/hs-backend-booster.cabal
+100 −60 booster/library/Booster/Pattern/Implies.hs
+1 −1 booster/package.yaml
+22 −0 booster/test/rpc-integration/resources/implies-smt.k
+6 −0 booster/test/rpc-integration/resources/implies-smt.kompile
+1 −1 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
+20 −0 booster/test/rpc-integration/test-implies-smt/README.md
+63 −0 booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.booster-dev
+177 −0 booster/test/rpc-integration/test-implies-smt/response-001-bound-weakening.json
+37 −0 booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.booster-dev
+177 −0 booster/test/rpc-integration/test-implies-smt/response-002-does-not-imply.json
+209 −0 booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.booster-dev
+234 −0 booster/test/rpc-integration/test-implies-smt/response-003-vacuous-antecedent.json
+63 −0 booster/test/rpc-integration/test-implies-smt/response-004-address-bound.booster-dev
+234 −0 booster/test/rpc-integration/test-implies-smt/response-004-address-bound.json
+37 −0 booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.booster-dev
+177 −0 booster/test/rpc-integration/test-implies-smt/response-005-escalate-indeterminate.json
+59 −0 booster/test/rpc-integration/test-implies-smt/state-001-bound-weakening.send
+59 −0 booster/test/rpc-integration/test-implies-smt/state-002-does-not-imply.send
+75 −0 booster/test/rpc-integration/test-implies-smt/state-003-vacuous-antecedent.send
+75 −0 booster/test/rpc-integration/test-implies-smt/state-004-address-bound.send
+148 −0 booster/test/rpc-integration/test-implies-smt/state-005-escalate-indeterminate.send
+1 −1 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
+352 −4 booster/test/rpc-integration/test-implies2/response-consequent-constraint.booster-dev
+1 −1 booster/test/rpc-integration/test-implies2/response-consequent-constraint.json
+1 −1 booster/test/rpc-integration/test-implies2/response-constant-subst.json
+320 −4 booster/test/rpc-integration/test-implies2/response-refutation-1.booster-dev
+1 −1 booster/test/rpc-integration/test-implies2/response-refutation-1.json
+334 −4 booster/test/rpc-integration/test-implies2/response-refutation-3.booster-dev
+1 −1 booster/test/rpc-integration/test-implies2/response-refutation-3.json
+348 −4 booster/test/rpc-integration/test-implies2/response-refutation-4.booster-dev
+1 −1 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
+31 −23 booster/tools/booster/Proxy.hs
+1 −1 dev-tools/hs-backend-booster-dev-tools.cabal
+1 −1 dev-tools/package.yaml
+1 −1 kore-rpc-types/kore-rpc-types.cabal
+20 −1 kore-rpc-types/src/Kore/JsonRpc/Types.hs
+1 −1 kore/kore.cabal
+5 −5 kore/src/Kore/JsonRpc.hs
+1 −1 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
8 changes: 7 additions & 1 deletion pyk/src/pyk/kore/rpc.py
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion pyk/src/tests/unit/kore/test_client.py
Original file line number Diff line number Diff line change
Expand Up @@ -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, ()),
),
)
Expand Down
Loading