From 2d302c655ed1456335cd46cf7755920ecb26c6a8 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 01:30:31 +0000 Subject: [PATCH 01/10] test_definition: add unit tests for KDefinition sort(), resolve_sorts(), add_sort_params() MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adjacent tests (already pass): sort for KVariable, KApply with direct result sort, resolve_sorts direct substitution, add_sort_params with already-filled or direct params. New-feature tests (fail at HEAD, committed with the fixes that make them pass): sort for unfilled KApply (should return None not raise), sort for nested result sort (MInt{N} → MInt{Int}), sort for KAs, resolve_sorts nested substitution, add_sort_params with nested param (MInt{N} ~ MInt{Int} → N=Int), add_sort_params ML pred sentinel. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/tests/unit/kast/test_definition.py | 170 +++++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 pyk/src/tests/unit/kast/test_definition.py diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py new file mode 100644 index 0000000000..87c0317561 --- /dev/null +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -0,0 +1,170 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +import pytest + +from pyk.kast.inner import KApply, KAs, KLabel, KSort, KVariable +from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal + +if TYPE_CHECKING: + from typing import Final + + +# --------------------------------------------------------------------------- +# Minimal test definition +# +# bar: syntax N ::= bar(N) [function] -- result sort is the param directly +# foo: syntax MInt{N} ::= foo(MInt{N}) [function] -- result/arg sorts nest the param +# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred with context-dependent result sort +# --------------------------------------------------------------------------- + +INT: Final = KSort('Int') +N: Final = KSort('N') +S1: Final = KSort('S1') +S2: Final = KSort('S2') +MINT_N: Final = KSort('MInt', (N,)) +MINT_INT: Final = KSort('MInt', (INT,)) +SORT_PARAM: Final = KSort('#SortParam') + +_BAR_PROD: Final = KProduction( + sort=N, + items=[KTerminal('bar'), KTerminal('('), KNonTerminal(N), KTerminal(')')], + params=[N], + klabel='bar', +) + +_FOO_PROD: Final = KProduction( + sort=MINT_N, + items=[KTerminal('foo'), KTerminal('('), KNonTerminal(MINT_N), KTerminal(')')], + params=[N], + klabel='foo', +) + +_EQUALS_PROD: Final = KProduction( + sort=S2, + items=[KNonTerminal(S1), KNonTerminal(S1)], + params=[S1, S2], + klabel='#Equals', +) + +DEFN: Final = KDefinition( + 'TEST', + [KFlatModule('TEST', [_BAR_PROD, _FOO_PROD, _EQUALS_PROD])], +) + + +# --------------------------------------------------------------------------- +# KDefinition.sort — adjacent tests (pass at HEAD) +# --------------------------------------------------------------------------- + + +def test_sort_kvariable() -> None: + """sort() returns the explicit sort annotation on a KVariable.""" + assert DEFN.sort(KVariable('X', sort=INT)) == INT + + +def test_sort_kapply_direct_result() -> None: + """sort() for an application whose result sort is the param directly (bar{Int}).""" + term = KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]) + assert DEFN.sort(term) == INT + + +# --------------------------------------------------------------------------- +# KDefinition.resolve_sorts — adjacent tests (pass at HEAD) +# --------------------------------------------------------------------------- + + +def test_resolve_sorts_direct() -> None: + """resolve_sorts handles direct param substitution N → Int.""" + result_sort, arg_sorts = DEFN.resolve_sorts(KLabel('bar', [INT])) + assert result_sort == INT + assert arg_sorts == (INT,) + + +# --------------------------------------------------------------------------- +# KDefinition.add_sort_params — adjacent tests (pass at HEAD) +# --------------------------------------------------------------------------- + + +def test_add_sort_params_already_filled() -> None: + """add_sort_params leaves a label alone when its params are already filled.""" + term = KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]) + assert DEFN.add_sort_params(term) == term + + +def test_add_sort_params_direct_param() -> None: + """add_sort_params fills a direct sort param by inspecting the argument sort.""" + term = KApply(KLabel('bar'), [KVariable('X', sort=INT)]) + expected = KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]) + assert DEFN.add_sort_params(term) == expected + + +# --------------------------------------------------------------------------- +# KDefinition.sort — new-feature tests (fail at HEAD before the fix) +# --------------------------------------------------------------------------- + + +def test_sort_kapply_unfilled_params_returns_none() -> None: + """sort() returns None (not raises) when the KApply label has unfilled sort params.""" + # When label has no params but the production requires them, old code raises ValueError + # from resolve_sorts(); new code catches it and returns None instead. + term = KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]) + assert DEFN.sort(term) is None + + +def test_sort_kapply_nested_result_sort() -> None: + """sort() resolves a result sort that nests the sort param (MInt{N} → MInt{Int}).""" + # Old code: resolve_sorts returns MInt{N} because sorts.get(MInt{N}, MInt{N}) leaves + # the nested param unsubstituted. New code recurses into the param tuple. + term = KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]) + assert DEFN.sort(term) == MINT_INT + + +def test_sort_kas() -> None: + """sort() returns the sort of the alias variable in a KAs pattern.""" + # Old code has no KAs case and falls through to case _: return None. + alias = KVariable('Y', sort=MINT_INT) + term = KAs(pattern=KVariable('X', sort=MINT_INT), alias=alias) + assert DEFN.sort(term) == MINT_INT + + +# --------------------------------------------------------------------------- +# KDefinition.resolve_sorts — new-feature tests (fail at HEAD before the fix) +# --------------------------------------------------------------------------- + + +def test_resolve_sorts_nested() -> None: + """resolve_sorts recursively substitutes params nested inside compound sorts.""" + # foo has param N, result sort MInt{N}, arg sort MInt{N}. + # With N → Int, both should resolve to MInt{Int}. + # Old code: sorts.get(MInt{N}, MInt{N}) → MInt{N} unchanged (N is the key, not MInt{N}). + result_sort, arg_sorts = DEFN.resolve_sorts(KLabel('foo', [INT])) + assert result_sort == MINT_INT + assert arg_sorts == (MINT_INT,) + + +# --------------------------------------------------------------------------- +# KDefinition.add_sort_params — new-feature tests (fail at HEAD before the fix) +# --------------------------------------------------------------------------- + + +def test_add_sort_params_nested_param() -> None: + """add_sort_params fills a param that appears nested inside the argument sort.""" + # foo has param N and arg sort MInt{N}. Given arg KVariable('X', sort=MInt{Int}), + # the unifier extracts N → Int from the match MInt{N} ~ MInt{Int}. + # Old code only handled the case psort IS the param (direct); it left nested cases unfilled. + term = KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]) + expected = KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]) + assert DEFN.add_sort_params(term) == expected + + +def test_add_sort_params_ml_pred_sentinel() -> None: + """add_sort_params fills the context-dependent result sort of an ML predicate with a sentinel.""" + # #Equals has params [S1, S2] where S2 is the axiom result sort (context-dependent). + # Given args of sort Int, S1 → Int is inferable but S2 is not — so S2 gets the + # sentinel KSort('#SortParam') so that krule_to_kore can introduce sort variable Q0. + # Old code: no ML pred special case, returns the term unchanged (no params filled). + term = KApply('#Equals', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) + expected = KApply(KLabel('#Equals', [INT, SORT_PARAM]), [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) + assert DEFN.add_sort_params(term) == expected From 2c635f21c27e95eaa0900b87980a00ae88851d7d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 02:43:10 +0000 Subject: [PATCH 02/10] test_definition: convert to pytest parametrization, add extra test cases MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three parametrized test functions (test_sort, test_resolve_sorts, test_add_sort_params) replace the eleven individual test functions. Each has a *_DATA tuple at module scope so new cases can be added by appending one tuple element. New cases added: - test_sort: ktoken, ksequence, kapply_unknown_label (KeyError → None), kas_unsorted_alias (alias with no sort annotation → None) - test_add_sort_params: unsortable_arg_unchanged (arg with no sort annotation prevents param filling — returns term unchanged) Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/tests/unit/kast/test_definition.py | 185 ++++++++++----------- 1 file changed, 87 insertions(+), 98 deletions(-) diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py index 87c0317561..dcae7e46e3 100644 --- a/pyk/src/tests/unit/kast/test_definition.py +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -4,19 +4,21 @@ import pytest -from pyk.kast.inner import KApply, KAs, KLabel, KSort, KVariable +from pyk.kast.inner import KApply, KAs, KLabel, KSequence, KSort, KToken, KVariable from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal if TYPE_CHECKING: from typing import Final + from pyk.kast.inner import KInner + # --------------------------------------------------------------------------- # Minimal test definition # -# bar: syntax N ::= bar(N) [function] -- result sort is the param directly -# foo: syntax MInt{N} ::= foo(MInt{N}) [function] -- result/arg sorts nest the param -# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred with context-dependent result sort +# bar: syntax N ::= bar(N) -- result sort is the param directly +# foo: syntax MInt{N} ::= foo(MInt{N}) -- result/arg sorts nest the param +# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred, result sort context-dependent # --------------------------------------------------------------------------- INT: Final = KSort('Int') @@ -55,116 +57,103 @@ # --------------------------------------------------------------------------- -# KDefinition.sort — adjacent tests (pass at HEAD) -# --------------------------------------------------------------------------- - - -def test_sort_kvariable() -> None: - """sort() returns the explicit sort annotation on a KVariable.""" - assert DEFN.sort(KVariable('X', sort=INT)) == INT - - -def test_sort_kapply_direct_result() -> None: - """sort() for an application whose result sort is the param directly (bar{Int}).""" - term = KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]) - assert DEFN.sort(term) == INT - - -# --------------------------------------------------------------------------- -# KDefinition.resolve_sorts — adjacent tests (pass at HEAD) +# KDefinition.sort # --------------------------------------------------------------------------- - -def test_resolve_sorts_direct() -> None: - """resolve_sorts handles direct param substitution N → Int.""" - result_sort, arg_sorts = DEFN.resolve_sorts(KLabel('bar', [INT])) - assert result_sort == INT - assert arg_sorts == (INT,) - - -# --------------------------------------------------------------------------- -# KDefinition.add_sort_params — adjacent tests (pass at HEAD) -# --------------------------------------------------------------------------- - - -def test_add_sort_params_already_filled() -> None: - """add_sort_params leaves a label alone when its params are already filled.""" - term = KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]) - assert DEFN.add_sort_params(term) == term +SORT_DATA: Final = ( + # Basic leaf terms + ('ktoken', KToken('42', INT), INT), + ('kvariable_with_sort', KVariable('X', sort=INT), INT), + ('ksequence', KSequence([]), KSort('K')), + # KApply: result sort substituted directly from param + ('kapply_direct_result', KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), INT), + # KApply: result sort nests the param (MInt{N} with N→Int → MInt{Int}) + ('kapply_nested_result', KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]), MINT_INT), + # KApply with unfilled sort params: sort() returns None rather than raising + ('kapply_unfilled_params', KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]), None), + # KApply with unknown label: KeyError from symbols lookup → None + ('kapply_unknown_label', KApply(KLabel('nonexistent'), []), None), + # KAs: sort of the alias variable + ('kas_sorted_alias', KAs(KVariable('X', sort=MINT_INT), KVariable('Y', sort=MINT_INT)), MINT_INT), + # KAs whose alias has no sort annotation: returns None + ('kas_unsorted_alias', KAs(KVariable('X', sort=MINT_INT), KVariable('Y')), None), +) -def test_add_sort_params_direct_param() -> None: - """add_sort_params fills a direct sort param by inspecting the argument sort.""" - term = KApply(KLabel('bar'), [KVariable('X', sort=INT)]) - expected = KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]) - assert DEFN.add_sort_params(term) == expected +@pytest.mark.parametrize( + 'test_id,term,expected', + SORT_DATA, + ids=[test_id for test_id, *_ in SORT_DATA], +) +def test_sort(test_id: str, term: KInner, expected: KSort | None) -> None: + assert DEFN.sort(term) == expected # --------------------------------------------------------------------------- -# KDefinition.sort — new-feature tests (fail at HEAD before the fix) +# KDefinition.resolve_sorts # --------------------------------------------------------------------------- - -def test_sort_kapply_unfilled_params_returns_none() -> None: - """sort() returns None (not raises) when the KApply label has unfilled sort params.""" - # When label has no params but the production requires them, old code raises ValueError - # from resolve_sorts(); new code catches it and returns None instead. - term = KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]) - assert DEFN.sort(term) is None - - -def test_sort_kapply_nested_result_sort() -> None: - """sort() resolves a result sort that nests the sort param (MInt{N} → MInt{Int}).""" - # Old code: resolve_sorts returns MInt{N} because sorts.get(MInt{N}, MInt{N}) leaves - # the nested param unsubstituted. New code recurses into the param tuple. - term = KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]) - assert DEFN.sort(term) == MINT_INT - - -def test_sort_kas() -> None: - """sort() returns the sort of the alias variable in a KAs pattern.""" - # Old code has no KAs case and falls through to case _: return None. - alias = KVariable('Y', sort=MINT_INT) - term = KAs(pattern=KVariable('X', sort=MINT_INT), alias=alias) - assert DEFN.sort(term) == MINT_INT - - -# --------------------------------------------------------------------------- -# KDefinition.resolve_sorts — new-feature tests (fail at HEAD before the fix) -# --------------------------------------------------------------------------- +RESOLVE_SORTS_DATA: Final = ( + # Direct substitution: result sort IS the param (N → Int) + ('direct_bar', KLabel('bar', [INT]), INT, (INT,)), + # Recursive substitution: result/arg sort nests the param (MInt{N} with N → Int → MInt{Int}) + ('nested_foo', KLabel('foo', [INT]), MINT_INT, (MINT_INT,)), +) -def test_resolve_sorts_nested() -> None: - """resolve_sorts recursively substitutes params nested inside compound sorts.""" - # foo has param N, result sort MInt{N}, arg sort MInt{N}. - # With N → Int, both should resolve to MInt{Int}. - # Old code: sorts.get(MInt{N}, MInt{N}) → MInt{N} unchanged (N is the key, not MInt{N}). - result_sort, arg_sorts = DEFN.resolve_sorts(KLabel('foo', [INT])) - assert result_sort == MINT_INT - assert arg_sorts == (MINT_INT,) +@pytest.mark.parametrize( + 'test_id,label,expected_result,expected_args', + RESOLVE_SORTS_DATA, + ids=[test_id for test_id, *_ in RESOLVE_SORTS_DATA], +) +def test_resolve_sorts(test_id: str, label: KLabel, expected_result: KSort, expected_args: tuple[KSort, ...]) -> None: + result, args = DEFN.resolve_sorts(label) + assert result == expected_result + assert args == expected_args # --------------------------------------------------------------------------- -# KDefinition.add_sort_params — new-feature tests (fail at HEAD before the fix) +# KDefinition.add_sort_params # --------------------------------------------------------------------------- - -def test_add_sort_params_nested_param() -> None: - """add_sort_params fills a param that appears nested inside the argument sort.""" - # foo has param N and arg sort MInt{N}. Given arg KVariable('X', sort=MInt{Int}), - # the unifier extracts N → Int from the match MInt{N} ~ MInt{Int}. - # Old code only handled the case psort IS the param (direct); it left nested cases unfilled. - term = KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]) - expected = KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]) - assert DEFN.add_sort_params(term) == expected +ADD_SORT_PARAMS_DATA: Final = ( + # Label already has params filled: leave unchanged + ( + 'already_filled', + KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), + KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), + ), + # Direct sort param: psort IS the param (N ~ Int → N=Int) + ( + 'direct_param', + KApply(KLabel('bar'), [KVariable('X', sort=INT)]), + KApply(KLabel('bar', [INT]), [KVariable('X', sort=INT)]), + ), + # Nested sort param: psort = MInt{N}, asort = MInt{Int} → N=Int via unification + ( + 'nested_param', + KApply(KLabel('foo'), [KVariable('X', sort=MINT_INT)]), + KApply(KLabel('foo', [INT]), [KVariable('X', sort=MINT_INT)]), + ), + # ML pred: S1 inferred from args, S2 (result sort) filled with #SortParam sentinel + ( + 'ml_pred_sentinel', + KApply('#Equals', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]), + KApply(KLabel('#Equals', [INT, SORT_PARAM]), [KVariable('X', sort=INT), KVariable('Y', sort=INT)]), + ), + # Unsortable argument (no sort annotation): cannot fill params, term returned unchanged + ( + 'unsortable_arg_unchanged', + KApply(KLabel('foo'), [KVariable('X')]), + KApply(KLabel('foo'), [KVariable('X')]), + ), +) -def test_add_sort_params_ml_pred_sentinel() -> None: - """add_sort_params fills the context-dependent result sort of an ML predicate with a sentinel.""" - # #Equals has params [S1, S2] where S2 is the axiom result sort (context-dependent). - # Given args of sort Int, S1 → Int is inferable but S2 is not — so S2 gets the - # sentinel KSort('#SortParam') so that krule_to_kore can introduce sort variable Q0. - # Old code: no ML pred special case, returns the term unchanged (no params filled). - term = KApply('#Equals', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) - expected = KApply(KLabel('#Equals', [INT, SORT_PARAM]), [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) +@pytest.mark.parametrize( + 'test_id,term,expected', + ADD_SORT_PARAMS_DATA, + ids=[test_id for test_id, *_ in ADD_SORT_PARAMS_DATA], +) +def test_add_sort_params(test_id: str, term: KInner, expected: KInner) -> None: assert DEFN.add_sort_params(term) == expected From bcc2dfc4062d14881c3b12bd8a16215c9922bf2d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 03:16:46 +0000 Subject: [PATCH 03/10] test_definition: add unit tests for add_cell_map_items guard Tests both the positive path (wrap when parent production expects the cell map sort) and the negative path (no wrap when parent expects the individual cell element sort) introduced in 78bfdab101. The cell-map productions are merged into the existing single DEFN to keep the fixture count low. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/tests/unit/kast/test_definition.py | 93 +++++++++++++++++++++- 1 file changed, 92 insertions(+), 1 deletion(-) diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py index dcae7e46e3..da397e3916 100644 --- a/pyk/src/tests/unit/kast/test_definition.py +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -4,6 +4,7 @@ import pytest +from pyk.kast.att import Atts, KAtt from pyk.kast.inner import KApply, KAs, KLabel, KSequence, KSort, KToken, KVariable from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal @@ -19,6 +20,12 @@ # bar: syntax N ::= bar(N) -- result sort is the param directly # foo: syntax MInt{N} ::= foo(MInt{N}) -- result/arg sorts nest the param # #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred, result sort context-dependent +# +# Cell map fragment: +# AccountCellMap ::= AccountCellMap AccountCellMap [cellCollection, element(AccountCellMapItem), wrapElement()] +# AccountCellMap ::= AccountCellMapItem(Int, AccountCell) +# AccountCell ::= (Int, Int) +# AccountCell ::= getEntry(AccountCell) -- takes element sort, NOT map sort # --------------------------------------------------------------------------- INT: Final = KSort('Int') @@ -28,6 +35,8 @@ MINT_N: Final = KSort('MInt', (N,)) MINT_INT: Final = KSort('MInt', (INT,)) SORT_PARAM: Final = KSort('#SortParam') +ACCOUNT_CELL_MAP: Final = KSort('AccountCellMap') +ACCOUNT_CELL: Final = KSort('AccountCell') _BAR_PROD: Final = KProduction( sort=N, @@ -50,9 +59,52 @@ klabel='#Equals', ) +_ACCT_MAP_CONCAT: Final = KProduction( + sort=ACCOUNT_CELL_MAP, + items=[KNonTerminal(ACCOUNT_CELL_MAP), KNonTerminal(ACCOUNT_CELL_MAP)], + klabel='_AccountCellMap_', + att=KAtt(entries=[Atts.CELL_COLLECTION(None), Atts.ELEMENT('AccountCellMapItem'), Atts.WRAP_ELEMENT('')]), +) + +_ACCT_MAP_ITEM: Final = KProduction( + sort=ACCOUNT_CELL_MAP, + items=[ + KTerminal('AccountCellMapItem'), + KTerminal('('), + KNonTerminal(INT), + KTerminal(','), + KNonTerminal(ACCOUNT_CELL), + KTerminal(')'), + ], + klabel='AccountCellMapItem', +) + +_ACCOUNT_CELL: Final = KProduction( + sort=ACCOUNT_CELL, + items=[ + KTerminal(''), + KTerminal('('), + KNonTerminal(INT), + KTerminal(','), + KNonTerminal(INT), + KTerminal(')'), + ], + klabel='', +) + +_GET_ENTRY: Final = KProduction( + sort=ACCOUNT_CELL, + items=[KTerminal('getEntry'), KTerminal('('), KNonTerminal(ACCOUNT_CELL), KTerminal(')')], + klabel='getEntry', +) + DEFN: Final = KDefinition( 'TEST', - [KFlatModule('TEST', [_BAR_PROD, _FOO_PROD, _EQUALS_PROD])], + [ + KFlatModule( + 'TEST', [_BAR_PROD, _FOO_PROD, _EQUALS_PROD, _ACCT_MAP_CONCAT, _ACCT_MAP_ITEM, _ACCOUNT_CELL, _GET_ENTRY] + ) + ], ) @@ -157,3 +209,42 @@ def test_resolve_sorts(test_id: str, label: KLabel, expected_result: KSort, expe ) def test_add_sort_params(test_id: str, term: KInner, expected: KInner) -> None: assert DEFN.add_sort_params(term) == expected + + +# --------------------------------------------------------------------------- +# KDefinition.add_cell_map_items +# --------------------------------------------------------------------------- + +_ACCT_1: Final = KApply('', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) +_ACCT_2: Final = KApply('', [KVariable('A', sort=INT), KVariable('B', sort=INT)]) + +ADD_CELL_MAP_ITEMS_DATA: Final = ( + # Parent expects AccountCellMap (the map sort) — children are wrapped in AccountCellMapItem. + ( + 'wraps_when_parent_expects_cell_map_sort', + KApply('_AccountCellMap_', [_ACCT_1, _ACCT_2]), + KApply( + '_AccountCellMap_', + [ + KApply('AccountCellMapItem', [KVariable('X', sort=INT), _ACCT_1]), + KApply('AccountCellMapItem', [KVariable('A', sort=INT), _ACCT_2]), + ], + ), + ), + # Parent expects AccountCell (the element sort) — the child must NOT be wrapped. + # Before the guard fix, _wrap_elements would incorrectly wrap here too. + ( + 'no_wrap_when_parent_expects_cell_element_sort', + KApply('getEntry', [_ACCT_1]), + KApply('getEntry', [_ACCT_1]), + ), +) + + +@pytest.mark.parametrize( + 'test_id,term,expected', + ADD_CELL_MAP_ITEMS_DATA, + ids=[test_id for test_id, *_ in ADD_CELL_MAP_ITEMS_DATA], +) +def test_add_cell_map_items(test_id: str, term: KInner, expected: KInner) -> None: + assert DEFN.add_cell_map_items(term) == expected From e8671f148cc1854ed622d45e082a3a2edc6b02b5 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 01:33:05 +0000 Subject: [PATCH 04/10] outer: sort() handles KAs and unfilled KApply; resolve_sorts() recursive substitution MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit sort() gains a KAs case that returns the alias variable's sort, and the KApply case is now wrapped in try/except so unfilled sort params (e.g. when label.params=[] but the production requires params) return None instead of raising ValueError. resolve_sorts() now recurses into nested compound sorts, enabling N → Int to also substitute inside MInt{N} → MInt{Int}. The old code used sorts.get(sort, sort) which only handled the case where sort IS a parameter, not nested inside one. Makes test_definition tests pass: test_sort_kas, test_sort_kapply_unfilled_params_returns_none, test_sort_kapply_nested_result_sort, test_resolve_sorts_nested. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 774a004e5c..a051a580e5 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -17,6 +17,7 @@ from .att import EMPTY_ATT, Atts, Format, KAst, KAtt, WithKAtt from .inner import ( KApply, + KAs, KInner, KLabel, KRewrite, @@ -1327,6 +1328,8 @@ def sort(self, kast: KInner) -> KSort | None: match kast: case KToken(_, sort) | KVariable(_, sort): return sort + case KAs(alias=KVariable(sort=sort)): + return sort case KRewrite(lhs, rhs): lhs_sort = self.sort(lhs) rhs_sort = self.sort(rhs) @@ -1336,8 +1339,11 @@ def sort(self, kast: KInner) -> KSort | None: case KSequence(_): return KSort('K') case KApply(label, _): - sort, _ = self.resolve_sorts(label) - return sort + try: + sort, _ = self.resolve_sorts(label) + return sort + except (KeyError, ValueError): + return None case _: return None @@ -1354,7 +1360,13 @@ def resolve_sorts(self, label: KLabel) -> tuple[KSort, tuple[KSort, ...]]: sorts = dict(zip(prod.params, label.params, strict=True)) def resolve(sort: KSort) -> KSort: - return sorts.get(sort, sort) + # Direct match: sort IS one of the sort parameters. + if sort in sorts: + return sorts[sort] + # Recursive substitution: sort params may appear nested (e.g. MInt{Width} → MInt{8}). + if sort.params: + return KSort(sort.name, tuple(resolve(p) for p in sort.params)) + return sort return resolve(prod.sort), tuple(resolve(sort) for sort in prod.argument_sorts) From f6a136f5704161cff837fd2365acc58babedac36 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 01:34:04 +0000 Subject: [PATCH 05/10] outer: add_sort_params() handles nested sort params and ML pred result sort sentinel The old implementation only extracted sort-param bindings when the production argument sort was exactly a sort parameter (psort in prod.params). This missed cases like MInt{Width} ~ MInt{8} where the parameter is nested. New helper _unify_sort_params recursively matches a parametric sort against an actual sort, extracting {Width: 8} from MInt{Width} ~ MInt{8}. _merge_binding handles conflicts and LUB computation when the same parameter appears in multiple argument positions. ML predicates (#Equals, #Ceil, #Floor, #In) have a context-dependent result sort that cannot be inferred from arguments alone. When Sort1 (the operand sort) is determined but Sort2 (the axiom result sort) is not, Sort2 is filled with the sentinel KSort('#SortParam'). Downstream code (_ksort_to_kore) maps this sentinel to SortVar('Q0') to emit the correct axiom{R,Q0} universally-quantified form. Makes test_definition tests pass: test_add_sort_params_nested_param, test_add_sort_params_ml_pred_sentinel. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 72 +++++++++++++++++++++++++++++++++++---- 1 file changed, 65 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index a051a580e5..ba8fc327f1 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1495,28 +1495,86 @@ def transform( # Best-effort addition of sort parameters to klabels, context insensitive def add_sort_params(self, kast: KInner) -> KInner: """Return a given term with the sort parameters on the `KLabel` filled in (which may be missing because of how the frontend works), best effort.""" + # ML predicate labels whose result sort (Sort2) is context-dependent and not inferable + # from the arguments alone. When Sort1 can be determined but Sort2 cannot, we fill Sort2 + # with the sentinel KSort('#SortParam') so that downstream Kore emission can introduce a + # universally-quantified sort variable (Q0) in the axiom. + _ML_PRED_RESULT_SORT_PARAM = KSort('#SortParam') # noqa: N806 + _ML_PRED_LABELS = frozenset({'#Equals', '#Ceil', '#Floor', '#In'}) # noqa: N806 + + def _unify_sort_params(parametric: KSort, actual: KSort, params: frozenset[KSort]) -> dict[KSort, KSort]: + """Match parametric sort against actual, extracting bindings for sort params. + + Handles both direct (parametric IS a sort param) and nested + (parametric = MInt{Width}, actual = MInt{8}) cases. + Returns empty dict when no bindings could be extracted (no match). + """ + if parametric in params: + return {parametric: actual} + if parametric.name != actual.name or len(parametric.params) != len(actual.params): + return {} + result: dict[KSort, KSort] = {} + for p_sub, a_sub in zip(parametric.params, actual.params, strict=True): + sub_bindings = _unify_sort_params(p_sub, a_sub, params) + for k, v in sub_bindings.items(): + if k in result and result[k] != v: + return {} # Conflicting bindings + result[k] = v + return result + + def _merge_binding(sort_dict: dict[KSort, KSort], k: KSort, v: KSort) -> bool: + """Merge one binding into sort_dict in place. Returns False on irreconcilable conflict.""" + if k in sort_dict: + existing = sort_dict[k] + if existing == _ML_PRED_RESULT_SORT_PARAM: + sort_dict[k] = v # Concrete sort overrides sentinel. + elif existing != v: + lub = self.least_common_supersort(existing, v) + if lub is None: + _LOGGER.warning(f'Failed to add sort parameter, sort mismatch: {(k, existing, v)}') + return False + sort_dict[k] = lub + else: + sort_dict[k] = v + return True def _add_sort_params(_k: KInner) -> KInner: if type(_k) is KApply: prod = self.symbols[_k.label.name] if len(_k.label.params) == 0 and len(prod.params) > 0: + param_set = frozenset(prod.params) sort_dict: dict[KSort, KSort] = {} for psort, asort in zip(prod.argument_sorts, map(self.sort, _k.args), strict=True): + if asort == _ML_PRED_RESULT_SORT_PARAM: + # #SortParam is the sentinel for an ML pred result sort that cannot be + # inferred bottom-up (e.g. #Equals result sort depends on outer context). + # It propagates upward into ML connectives (#And, #Or, #Not) as a + # placeholder for the axiom sort variable Q0, but a concrete sort takes + # precedence when one is available. + bindings = _unify_sort_params(psort, asort, param_set) + for k, v in bindings.items(): + if k not in sort_dict: # sentinel fills only empty slots + sort_dict[k] = v + continue if asort is None: _LOGGER.warning( f'Failed to add sort parameter, unable to determine sort for argument in production: {(prod, psort, asort)}' ) return _k - if psort in prod.params: - if psort in sort_dict and sort_dict[psort] != asort: - _LOGGER.warning( - f'Failed to add sort parameter, sort mismatch between different occurances of sort parameter: {(prod, psort, sort_dict[psort], asort)}' - ) + # Unify psort with asort to extract bindings for sort params. + # Handles both direct (psort=Width) and nested (psort=MInt{Width}) cases. + bindings = _unify_sort_params(psort, asort, param_set) + for k, v in bindings.items(): + if not _merge_binding(sort_dict, k, v): return _k - elif psort not in sort_dict: - sort_dict[psort] = asort if all(p in sort_dict for p in prod.params): return _k.let(label=KLabel(_k.label.name, [sort_dict[p] for p in prod.params])) + # ML predicates have a context-dependent result sort (Sort2) that cannot be + # inferred from arguments. Fill it with the sentinel so that krule_to_kore can + # introduce a universally-quantified sort variable for the axiom. + if _k.label.name in _ML_PRED_LABELS: + filled = {p: sort_dict.get(p, _ML_PRED_RESULT_SORT_PARAM) for p in prod.params} + return _k.let(label=KLabel(_k.label.name, [filled[p] for p in prod.params])) return _k return bottom_up(_add_sort_params, kast) From f4a76480241648b0068eaca1397145874010c615 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 25 Apr 2026 01:35:23 +0000 Subject: [PATCH 06/10] outer: add_cell_map_items wraps only when parent expects cell map sort The old _wrap_elements unconditionally wrapped any KApply matching a cell label, even when the parent production expected the individual cell sort (not the map sort). This caused double-wrapping in productions like EntryCellMapKey((...)) where the argument sort is EntryCell, not EntryCellMap. The new implementation inspects the parent production's expected argument sorts and only wraps when the expected sort matches the cell map sort (e.g. EntryCellMap). Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 30 +++++++++++++++++++++++++----- 1 file changed, 25 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index ba8fc327f1..ee42a19512 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1585,15 +1585,35 @@ def add_cell_map_items(self, kast: KInner) -> KInner: # syntax AccountCellMap [cellCollection, hook(MAP.Map)] # syntax AccountCellMap ::= AccountCellMap AccountCellMap [assoc, avoid, cellCollection, comm, element(AccountCellMapItem), function, hook(MAP.concat), unit(.AccountCellMap), wrapElement()] - cell_wrappers = {} + # Maps cell label -> (element_constructor, cell_map_sort). + # Wrapping is correct only when the parent production expects the cell MAP sort (e.g. + # EntryCellMap), not when it expects the individual cell element sort (e.g. EntryCell). + # For example, EntryCellMapKey((...)) takes EntryCell — the must NOT be + # wrapped, whereas _EntryCellMap_((...), ...) expects EntryCellMap — wrapping is needed. + cell_wrappers: dict[str, tuple[str, KSort]] = {} for ccp in self.cell_collection_productions: if Atts.ELEMENT in ccp.att and Atts.WRAP_ELEMENT in ccp.att: - cell_wrappers[ccp.att[Atts.WRAP_ELEMENT]] = ccp.att[Atts.ELEMENT] + cell_label = ccp.att[Atts.WRAP_ELEMENT] + element_ctor = ccp.att[Atts.ELEMENT] + if element_ctor in self.symbols: + cell_wrappers[cell_label] = (element_ctor, self.symbols[element_ctor].sort) def _wrap_elements(_k: KInner) -> KInner: - if type(_k) is KApply and _k.label.name in cell_wrappers: - return KApply(cell_wrappers[_k.label.name], [_k.args[0], _k]) - return _k + if not isinstance(_k, KApply) or _k.label.name not in self.symbols: + return _k + prod = self.symbols[_k.label.name] + arg_sorts = prod.argument_sorts + if not arg_sorts or len(arg_sorts) != _k.arity: + return _k + new_args: list[KInner] = list(_k.args) + changed = False + for i, (arg_sort, arg) in enumerate(zip(arg_sorts, _k.args, strict=True)): + if isinstance(arg, KApply) and arg.label.name in cell_wrappers: + element_ctor, cell_map_sort = cell_wrappers[arg.label.name] + if arg_sort == cell_map_sort: + new_args[i] = KApply(element_ctor, [arg.args[0], arg]) + changed = True + return _k.let(args=new_args) if changed else _k # To ensure we don't get duplicate wrappers. _kast = self.remove_cell_map_items(kast) From 1182496b29209722e31d1dd3fa0fac5acd614e6c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 28 Apr 2026 23:11:15 +0000 Subject: [PATCH 07/10] outer: assert at most one unbound sort param when using ML pred sentinel The single KSort('#SortParam') sentinel is only unambiguous when exactly one sort parameter is unresolvable bottom-up. Add an assertion that documents this invariant and crashes loudly if it is ever violated, with a message pointing toward the Java-style unique fresh-param fix. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index ee42a19512..563eec0c52 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1573,6 +1573,18 @@ def _add_sort_params(_k: KInner) -> KInner: # inferred from arguments. Fill it with the sentinel so that krule_to_kore can # introduce a universally-quantified sort variable for the axiom. if _k.label.name in _ML_PRED_LABELS: + unbound = [p for p in prod.params if p not in sort_dict] + # The single sentinel KSort('#SortParam') is only unambiguous when at most + # one parameter is unresolvable bottom-up. All current ML predicates + # (#Equals, #Ceil, #Floor, #In) have exactly two sort params {Sort1, + # Sort2}: Sort1 is always determined by the arguments, Sort2 (the result + # sort) is the one remaining unbound param. If this assertion ever fires, + # the sentinel scheme needs to be replaced with unique fresh params, as + # Java does with #SortParam{Q0}, #SortParam{Q1}, .... + assert len(unbound) <= 1, ( + f'Expected at most one unbound sort parameter for {_k.label.name!r}, ' + f'got {len(unbound)}: {unbound}' + ) filled = {p: sort_dict.get(p, _ML_PRED_RESULT_SORT_PARAM) for p in prod.params} return _k.let(label=KLabel(_k.label.name, [filled[p] for p in prod.params])) return _k From a53e36280345235f6d7ee5dd27e3c8d66287e5ef Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 8 May 2026 20:43:23 +0000 Subject: [PATCH 08/10] outer, test_definition: replace assert with NotImplementedError for multi-unbound ML pred sort params The single KSort('#SortParam') sentinel can only represent one unbound sort parameter at a time. If an ML predicate ever had two or more unbound params simultaneously the old assert (disabled by -O) would silently pass or raise a bare AssertionError with no guidance. Replace the assert with NotImplementedError that names the fix: generate unique fresh sentinels analogous to Java's #SortParam{Q0}, #SortParam{Q1}, etc. Add a unit test with a hypothetical 3-sort-param #Equals production (two unbound params) that verifies the error is raised. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 20 +++++++++++++------- pyk/src/tests/unit/kast/test_definition.py | 22 ++++++++++++++++++++++ 2 files changed, 35 insertions(+), 7 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index 563eec0c52..e06bf90b59 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1578,13 +1578,19 @@ def _add_sort_params(_k: KInner) -> KInner: # one parameter is unresolvable bottom-up. All current ML predicates # (#Equals, #Ceil, #Floor, #In) have exactly two sort params {Sort1, # Sort2}: Sort1 is always determined by the arguments, Sort2 (the result - # sort) is the one remaining unbound param. If this assertion ever fires, - # the sentinel scheme needs to be replaced with unique fresh params, as - # Java does with #SortParam{Q0}, #SortParam{Q1}, .... - assert len(unbound) <= 1, ( - f'Expected at most one unbound sort parameter for {_k.label.name!r}, ' - f'got {len(unbound)}: {unbound}' - ) + # sort) is the one remaining unbound param. If more than one param is + # unbound, the sentinel scheme must be replaced with unique fresh params + # (e.g. KSort('#SortParam', (KSort('Q0'),)), KSort('#SortParam', (KSort('Q1'),)), ...) + # analogously to how Java's AddSortInjections generates #SortParam{Q0}, + # #SortParam{Q1}, etc. _ksort_to_kore would also need updating to emit + # these as sort variables rather than sort applications. + if len(unbound) > 1: + raise NotImplementedError( + f'ML predicate {_k.label.name!r} has {len(unbound)} unbound sort parameters ' + f'({unbound}); the single-sentinel scheme only handles at most one. ' + f'Implement unique fresh sentinels analogous to Java #SortParam{{Q0}}, ' + f'#SortParam{{Q1}}, ... and update _ksort_to_kore to emit them as sort variables.' + ) filled = {p: sort_dict.get(p, _ML_PRED_RESULT_SORT_PARAM) for p in prod.params} return _k.let(label=KLabel(_k.label.name, [filled[p] for p in prod.params])) return _k diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py index da397e3916..6be46f92f8 100644 --- a/pyk/src/tests/unit/kast/test_definition.py +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -32,6 +32,7 @@ N: Final = KSort('N') S1: Final = KSort('S1') S2: Final = KSort('S2') +S3: Final = KSort('S3') MINT_N: Final = KSort('MInt', (N,)) MINT_INT: Final = KSort('MInt', (INT,)) SORT_PARAM: Final = KSort('#SortParam') @@ -59,6 +60,16 @@ klabel='#Equals', ) +# Hypothetical 3-param #Equals to test the multi-unbound-param guard. +# S1 is inferred from arguments; S2 and S3 are both unbound, which the single-sentinel +# scheme cannot handle — add_sort_params must raise NotImplementedError. +_EQUALS3_PROD: Final = KProduction( + sort=S2, + items=[KNonTerminal(S1), KNonTerminal(S1)], + params=[S1, S2, S3], + klabel='#Equals', +) + _ACCT_MAP_CONCAT: Final = KProduction( sort=ACCOUNT_CELL_MAP, items=[KNonTerminal(ACCOUNT_CELL_MAP), KNonTerminal(ACCOUNT_CELL_MAP)], @@ -107,6 +118,9 @@ ], ) +# Definition used only to verify the multi-unbound-param guard in add_sort_params. +DEFN3: Final = KDefinition('TEST3', [KFlatModule('TEST3', [_EQUALS3_PROD])]) + # --------------------------------------------------------------------------- # KDefinition.sort @@ -211,6 +225,14 @@ def test_add_sort_params(test_id: str, term: KInner, expected: KInner) -> None: assert DEFN.add_sort_params(term) == expected +def test_add_sort_params_multi_unbound_raises() -> None: + # #Equals with 3 sort params: S1 is inferred from arguments, S2 and S3 are both unbound. + # The single-sentinel scheme cannot distinguish them, so NotImplementedError must be raised. + term = KApply('#Equals', [KVariable('X', sort=INT), KVariable('Y', sort=INT)]) + with pytest.raises(NotImplementedError, match='2 unbound sort parameters'): + DEFN3.add_sort_params(term) + + # --------------------------------------------------------------------------- # KDefinition.add_cell_map_items # --------------------------------------------------------------------------- From c9a42102a66cc832da8d9b6d529ad9368957875e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 8 May 2026 20:54:49 +0000 Subject: [PATCH 09/10] outer, test_definition: warn when user-defined label has unresolvable sort params After the argument loop, if some sort params remain unbound and the label is not an ML predicate, add_sort_params previously fell through silently. Add a _LOGGER.warning that names the label and the unresolved params, matching the existing warning style for the asort-is-None case. Add test_add_sort_params_user_label_unresolvable_warns using a pair(S1,S2) production where S2 does not appear in any argument sort, verifying the warning fires and the term is returned unchanged. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 4 ++++ pyk/src/tests/unit/kast/test_definition.py | 24 ++++++++++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index e06bf90b59..bd47545028 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1593,6 +1593,10 @@ def _add_sort_params(_k: KInner) -> KInner: ) filled = {p: sort_dict.get(p, _ML_PRED_RESULT_SORT_PARAM) for p in prod.params} return _k.let(label=KLabel(_k.label.name, [filled[p] for p in prod.params])) + unbound = [p for p in prod.params if p not in sort_dict] + _LOGGER.warning( + f'Failed to add sort parameter, could not infer sort params from arguments: {(prod, unbound)}' + ) return _k return bottom_up(_add_sort_params, kast) diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py index 6be46f92f8..b0ae216f79 100644 --- a/pyk/src/tests/unit/kast/test_definition.py +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -1,5 +1,6 @@ from __future__ import annotations +import logging from typing import TYPE_CHECKING import pytest @@ -70,6 +71,16 @@ klabel='#Equals', ) +# User-defined label where S2 does not appear in any argument sort, so it remains +# unbound after argument processing. add_sort_params must emit a warning and +# return the term unchanged (best-effort). +_PAIR_PROD: Final = KProduction( + sort=KSort('Pair', (S1, S2)), + items=[KTerminal('pair'), KTerminal('('), KNonTerminal(S1), KTerminal(')')], + params=[S1, S2], + klabel='pair', +) + _ACCT_MAP_CONCAT: Final = KProduction( sort=ACCOUNT_CELL_MAP, items=[KNonTerminal(ACCOUNT_CELL_MAP), KNonTerminal(ACCOUNT_CELL_MAP)], @@ -121,6 +132,9 @@ # Definition used only to verify the multi-unbound-param guard in add_sort_params. DEFN3: Final = KDefinition('TEST3', [KFlatModule('TEST3', [_EQUALS3_PROD])]) +# Definition used only to verify the unresolvable-user-label warning path. +DEFN_PAIR: Final = KDefinition('TEST_PAIR', [KFlatModule('TEST_PAIR', [_PAIR_PROD])]) + # --------------------------------------------------------------------------- # KDefinition.sort @@ -233,6 +247,16 @@ def test_add_sort_params_multi_unbound_raises() -> None: DEFN3.add_sort_params(term) +def test_add_sort_params_user_label_unresolvable_warns(caplog: pytest.LogCaptureFixture) -> None: + # pair(S1, S2) has S2 absent from arguments — S2 is unbound after inference. + # add_sort_params emits a warning and returns the term unchanged (best-effort). + term = KApply(KLabel('pair'), [KVariable('X', sort=INT)]) + with caplog.at_level(logging.WARNING): + result = DEFN_PAIR.add_sort_params(term) + assert result == term + assert any('could not infer sort params' in record.message for record in caplog.records) + + # --------------------------------------------------------------------------- # KDefinition.add_cell_map_items # --------------------------------------------------------------------------- From 5ff5f458ada9865762867b4287a964e99dc262b4 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 11 May 2026 19:55:47 +0000 Subject: [PATCH 10/10] outer, test_definition: port Java AddSortInjections direct sort param inference MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extract _sort_contains and _match_sort_params as module-level pure functions, implementing the same three-strategy matching algorithm as Java's AddSortInjections.match(): direct sort param binding, structural unification, and subsort-aware matching (iterate s ≤ actual with same head as parametric). Add KDefinition.infer_sort_params() mirroring substituteProd(), including the matchExpected path for binding result-sort-only params from a known expected sort. Simplify add_sort_params() to delegate to infer_sort_params(), keeping only the ML predicate sentinel policy inline. Expand test_definition.py with: test_infer_sort_params (direct, nested, subsort-aware, matchExpected, unbound cases), test_match_sort_params (all three strategies in isolation), test_sort_contains, and a subsort_aware case in the existing test_add_sort_params table. Co-Authored-By: Claude Sonnet 4.6 --- pyk/src/pyk/kast/outer.py | 247 +++++++++++++-------- pyk/src/tests/unit/kast/test_definition.py | 161 +++++++++++++- 2 files changed, 312 insertions(+), 96 deletions(-) diff --git a/pyk/src/pyk/kast/outer.py b/pyk/src/pyk/kast/outer.py index bd47545028..6feb954b45 100644 --- a/pyk/src/pyk/kast/outer.py +++ b/pyk/src/pyk/kast/outer.py @@ -1001,6 +1001,45 @@ def let(self, *, require: str | None = None) -> KRequire: return KRequire(require=require) +def _sort_contains(sort: KSort, param: KSort) -> bool: + """Return whether ``param`` appears anywhere in the sort tree of ``sort``.""" + return sort == param or any(_sort_contains(p, param) for p in sort.params) + + +def _match_sort_params( + parametric: KSort, + actual: KSort, + params: frozenset[KSort], + subsorts_fn: Callable[[KSort], frozenset[KSort]] | None = None, +) -> dict[KSort, list[KSort]]: + """Match ``parametric`` sort against ``actual``, collecting candidate bindings per sort param. + + Three matching strategies, mirroring Java ``AddSortInjections.match()``: + + 1. Direct: ``parametric`` is itself a sort param — bind it to ``actual``. + 2. Structural: same constructor head — recurse on sub-params. + 3. Subsort-aware: iterate subsorts ``s ≤ actual`` with same head as ``parametric``, + collecting additional candidates for LUB resolution. + """ + if parametric in params: + return {parametric: [actual]} + if parametric.name == actual.name and len(parametric.params) == len(actual.params): + result: dict[KSort, list[KSort]] = {} + for p_sub, a_sub in zip(parametric.params, actual.params, strict=True): + for k, vs in _match_sort_params(p_sub, a_sub, params, subsorts_fn).items(): + result.setdefault(k, []).extend(vs) + return result + if parametric.params and subsorts_fn is not None: + result = {} + for s in subsorts_fn(actual): + if s.name == parametric.name and len(s.params) == len(parametric.params): + for p_sub, a_sub in zip(parametric.params, s.params, strict=True): + for k, vs in _match_sort_params(p_sub, a_sub, params).items(): + result.setdefault(k, []).extend(vs) + return result + return {} + + @final @dataclass(frozen=True) class KDefinition(KOuter, WithKAtt, Iterable[KFlatModule]): @@ -1492,6 +1531,61 @@ def transform( return Subst(subst)(new_term) + def infer_sort_params( + self, + prod: KProduction, + actual_sorts: tuple[KSort | None, ...], + expected_sort: KSort | None = None, + ) -> dict[KSort, KSort]: + """Infer sort parameter bindings for a parametric production application. + + Returns a (possibly partial) mapping from sort params to concrete sorts; + unbound parameters are absent from the result. + Mirrors ``AddSortInjections.substituteProd()`` in the Java frontend. + + ``actual_sorts`` must have the same length as ``prod.argument_sorts``. + ``None`` entries are skipped (unsortable arguments). + If ``expected_sort`` is given, parameters that appear only in the result sort + (not in any argument sort) are also inferred from it — this is the + ``matchExpected`` path in the Java algorithm. + """ + params = frozenset(prod.params) + candidates: dict[KSort, list[KSort]] = {} + + for psort, asort in zip(prod.argument_sorts, actual_sorts, strict=True): + if asort is None: + continue + for k, vs in _match_sort_params(psort, asort, params, self.subsorts).items(): + candidates.setdefault(k, []).extend(vs) + + if expected_sort is not None: + unbound_result_params = frozenset( + p + for p in params + if _sort_contains(prod.sort, p) + and not any(_sort_contains(asort, p) for asort in actual_sorts if asort is not None) + ) + if unbound_result_params: + for k, vs in _match_sort_params(prod.sort, expected_sort, unbound_result_params).items(): + candidates.setdefault(k, []).extend(vs) + + result: dict[KSort, KSort] = {} + for p in prod.params: + if p not in candidates: + continue + lub: KSort = candidates[p][0] + for s in candidates[p][1:]: + if lub == s: + continue + new_lub = self.least_common_supersort(lub, s) + if new_lub is None: + break + lub = new_lub + else: + result[p] = lub + + return result + # Best-effort addition of sort parameters to klabels, context insensitive def add_sort_params(self, kast: KInner) -> KInner: """Return a given term with the sort parameters on the `KLabel` filled in (which may be missing because of how the frontend works), best effort.""" @@ -1502,101 +1596,72 @@ def add_sort_params(self, kast: KInner) -> KInner: _ML_PRED_RESULT_SORT_PARAM = KSort('#SortParam') # noqa: N806 _ML_PRED_LABELS = frozenset({'#Equals', '#Ceil', '#Floor', '#In'}) # noqa: N806 - def _unify_sort_params(parametric: KSort, actual: KSort, params: frozenset[KSort]) -> dict[KSort, KSort]: - """Match parametric sort against actual, extracting bindings for sort params. - - Handles both direct (parametric IS a sort param) and nested - (parametric = MInt{Width}, actual = MInt{8}) cases. - Returns empty dict when no bindings could be extracted (no match). - """ - if parametric in params: - return {parametric: actual} - if parametric.name != actual.name or len(parametric.params) != len(actual.params): - return {} - result: dict[KSort, KSort] = {} - for p_sub, a_sub in zip(parametric.params, actual.params, strict=True): - sub_bindings = _unify_sort_params(p_sub, a_sub, params) - for k, v in sub_bindings.items(): - if k in result and result[k] != v: - return {} # Conflicting bindings - result[k] = v - return result + def _add_sort_params(_k: KInner) -> KInner: + if type(_k) is not KApply: + return _k + prod = self.symbols[_k.label.name] + if len(_k.label.params) != 0 or len(prod.params) == 0: + return _k - def _merge_binding(sort_dict: dict[KSort, KSort], k: KSort, v: KSort) -> bool: - """Merge one binding into sort_dict in place. Returns False on irreconcilable conflict.""" - if k in sort_dict: - existing = sort_dict[k] - if existing == _ML_PRED_RESULT_SORT_PARAM: - sort_dict[k] = v # Concrete sort overrides sentinel. - elif existing != v: - lub = self.least_common_supersort(existing, v) - if lub is None: - _LOGGER.warning(f'Failed to add sort parameter, sort mismatch: {(k, existing, v)}') - return False - sort_dict[k] = lub - else: - sort_dict[k] = v - return True + actual_sorts = tuple(map(self.sort, _k.args)) + param_set = frozenset(prod.params) - def _add_sort_params(_k: KInner) -> KInner: - if type(_k) is KApply: - prod = self.symbols[_k.label.name] - if len(_k.label.params) == 0 and len(prod.params) > 0: - param_set = frozenset(prod.params) - sort_dict: dict[KSort, KSort] = {} - for psort, asort in zip(prod.argument_sorts, map(self.sort, _k.args), strict=True): - if asort == _ML_PRED_RESULT_SORT_PARAM: - # #SortParam is the sentinel for an ML pred result sort that cannot be - # inferred bottom-up (e.g. #Equals result sort depends on outer context). - # It propagates upward into ML connectives (#And, #Or, #Not) as a - # placeholder for the axiom sort variable Q0, but a concrete sort takes - # precedence when one is available. - bindings = _unify_sort_params(psort, asort, param_set) - for k, v in bindings.items(): - if k not in sort_dict: # sentinel fills only empty slots - sort_dict[k] = v - continue - if asort is None: - _LOGGER.warning( - f'Failed to add sort parameter, unable to determine sort for argument in production: {(prod, psort, asort)}' - ) - return _k - # Unify psort with asort to extract bindings for sort params. - # Handles both direct (psort=Width) and nested (psort=MInt{Width}) cases. - bindings = _unify_sort_params(psort, asort, param_set) - for k, v in bindings.items(): - if not _merge_binding(sort_dict, k, v): - return _k - if all(p in sort_dict for p in prod.params): - return _k.let(label=KLabel(_k.label.name, [sort_dict[p] for p in prod.params])) - # ML predicates have a context-dependent result sort (Sort2) that cannot be - # inferred from arguments. Fill it with the sentinel so that krule_to_kore can - # introduce a universally-quantified sort variable for the axiom. - if _k.label.name in _ML_PRED_LABELS: - unbound = [p for p in prod.params if p not in sort_dict] - # The single sentinel KSort('#SortParam') is only unambiguous when at most - # one parameter is unresolvable bottom-up. All current ML predicates - # (#Equals, #Ceil, #Floor, #In) have exactly two sort params {Sort1, - # Sort2}: Sort1 is always determined by the arguments, Sort2 (the result - # sort) is the one remaining unbound param. If more than one param is - # unbound, the sentinel scheme must be replaced with unique fresh params - # (e.g. KSort('#SortParam', (KSort('Q0'),)), KSort('#SortParam', (KSort('Q1'),)), ...) - # analogously to how Java's AddSortInjections generates #SortParam{Q0}, - # #SortParam{Q1}, etc. _ksort_to_kore would also need updating to emit - # these as sort variables rather than sort applications. - if len(unbound) > 1: - raise NotImplementedError( - f'ML predicate {_k.label.name!r} has {len(unbound)} unbound sort parameters ' - f'({unbound}); the single-sentinel scheme only handles at most one. ' - f'Implement unique fresh sentinels analogous to Java #SortParam{{Q0}}, ' - f'#SortParam{{Q1}}, ... and update _ksort_to_kore to emit them as sort variables.' - ) - filled = {p: sort_dict.get(p, _ML_PRED_RESULT_SORT_PARAM) for p in prod.params} - return _k.let(label=KLabel(_k.label.name, [filled[p] for p in prod.params])) - unbound = [p for p in prod.params if p not in sort_dict] + # Separate sentinel args from real args; bail out on genuinely unsortable ones. + # Sentinels (#SortParam) propagate from nested ML preds and are handled below. + inference_sorts: list[KSort | None] = [] + for psort, asort in zip(prod.argument_sorts, actual_sorts, strict=True): + if asort == _ML_PRED_RESULT_SORT_PARAM: + inference_sorts.append(None) # skip in inference, propagate as sentinel below + elif asort is None: _LOGGER.warning( - f'Failed to add sort parameter, could not infer sort params from arguments: {(prod, unbound)}' + f'Failed to add sort parameter, unable to determine sort for argument in production: {(prod, psort, asort)}' ) + return _k + else: + inference_sorts.append(asort) + + bindings = self.infer_sort_params(prod, tuple(inference_sorts)) + + # Sentinel propagation: if an arg carried the #SortParam sentinel (from a nested ML + # pred) and inference left that arg's param slot empty, fill it with the sentinel. + # Only direct-param positions (psort IS a param) propagate the sentinel; nested cases + # (psort = MInt{S}) do not, matching the current Java behaviour. + for psort, asort in zip(prod.argument_sorts, actual_sorts, strict=True): + if asort == _ML_PRED_RESULT_SORT_PARAM and psort in param_set and psort not in bindings: + bindings[psort] = _ML_PRED_RESULT_SORT_PARAM + + if all(p in bindings for p in prod.params): + return _k.let(label=KLabel(_k.label.name, [bindings[p] for p in prod.params])) + + # ML predicates have a context-dependent result sort (Sort2) that cannot be + # inferred from arguments. Fill it with the sentinel so that krule_to_kore can + # introduce a universally-quantified sort variable for the axiom. + if _k.label.name in _ML_PRED_LABELS: + unbound = [p for p in prod.params if p not in bindings] + # The single sentinel KSort('#SortParam') is only unambiguous when at most + # one parameter is unresolvable bottom-up. All current ML predicates + # (#Equals, #Ceil, #Floor, #In) have exactly two sort params {Sort1, + # Sort2}: Sort1 is always determined by the arguments, Sort2 (the result + # sort) is the one remaining unbound param. If more than one param is + # unbound, the sentinel scheme must be replaced with unique fresh params + # (e.g. KSort('#SortParam', (KSort('Q0'),)), KSort('#SortParam', (KSort('Q1'),)), ...) + # analogously to how Java's AddSortInjections generates #SortParam{Q0}, + # #SortParam{Q1}, etc. _ksort_to_kore would also need updating to emit + # these as sort variables rather than sort applications. + if len(unbound) > 1: + raise NotImplementedError( + f'ML predicate {_k.label.name!r} has {len(unbound)} unbound sort parameters ' + f'({unbound}); the single-sentinel scheme only handles at most one. ' + f'Implement unique fresh sentinels analogous to Java #SortParam{{Q0}}, ' + f'#SortParam{{Q1}}, ... and update _ksort_to_kore to emit them as sort variables.' + ) + filled = {p: bindings.get(p, _ML_PRED_RESULT_SORT_PARAM) for p in prod.params} + return _k.let(label=KLabel(_k.label.name, [filled[p] for p in prod.params])) + + unbound = [p for p in prod.params if p not in bindings] + _LOGGER.warning( + f'Failed to add sort parameter, could not infer sort params from arguments: {(prod, unbound)}' + ) return _k return bottom_up(_add_sort_params, kast) diff --git a/pyk/src/tests/unit/kast/test_definition.py b/pyk/src/tests/unit/kast/test_definition.py index b0ae216f79..6868303c76 100644 --- a/pyk/src/tests/unit/kast/test_definition.py +++ b/pyk/src/tests/unit/kast/test_definition.py @@ -7,9 +7,18 @@ from pyk.kast.att import Atts, KAtt from pyk.kast.inner import KApply, KAs, KLabel, KSequence, KSort, KToken, KVariable -from pyk.kast.outer import KDefinition, KFlatModule, KNonTerminal, KProduction, KTerminal +from pyk.kast.outer import ( + KDefinition, + KFlatModule, + KNonTerminal, + KProduction, + KTerminal, + _match_sort_params, + _sort_contains, +) if TYPE_CHECKING: + from collections.abc import Callable from typing import Final from pyk.kast.inner import KInner @@ -18,9 +27,12 @@ # --------------------------------------------------------------------------- # Minimal test definition # -# bar: syntax N ::= bar(N) -- result sort is the param directly -# foo: syntax MInt{N} ::= foo(MInt{N}) -- result/arg sorts nest the param -# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred, result sort context-dependent +# bar: syntax N ::= bar(N) -- result sort is the param directly +# foo: syntax MInt{N} ::= foo(MInt{N}) -- result/arg sorts nest the param +# baz: syntax MInt{N} ::= baz() -- no args; param bound only from expected sort +# #Equals: syntax S2 ::= #Equals{S1,S2}(S1, S1) -- ML pred, result sort context-dependent +# +# Subsort: syntax Int ::= MInt{Int} -- MInt{Int} <: Int (enables subsort-aware matching) # # Cell map fragment: # AccountCellMap ::= AccountCellMap AccountCellMap [cellCollection, element(AccountCellMapItem), wrapElement()] @@ -81,6 +93,18 @@ klabel='pair', ) +# syntax MInt{N} ::= baz() — no argument sorts; param N only bound via expected_sort +_BAZ_PROD: Final = KProduction( + sort=MINT_N, + items=[KTerminal('baz'), KTerminal('('), KTerminal(')')], + params=[N], + klabel='baz', +) + +# syntax Int ::= MInt{Int} — subsort declaration: MInt{Int} <: Int +# Enables the subsort-aware matching path (Java AddSortInjections.match step 3). +_MINT_INT_SUBSORT: Final = KProduction(sort=INT, items=[KNonTerminal(MINT_INT)]) + _ACCT_MAP_CONCAT: Final = KProduction( sort=ACCOUNT_CELL_MAP, items=[KNonTerminal(ACCOUNT_CELL_MAP), KNonTerminal(ACCOUNT_CELL_MAP)], @@ -124,7 +148,18 @@ 'TEST', [ KFlatModule( - 'TEST', [_BAR_PROD, _FOO_PROD, _EQUALS_PROD, _ACCT_MAP_CONCAT, _ACCT_MAP_ITEM, _ACCOUNT_CELL, _GET_ENTRY] + 'TEST', + [ + _BAR_PROD, + _FOO_PROD, + _BAZ_PROD, + _EQUALS_PROD, + _MINT_INT_SUBSORT, + _ACCT_MAP_CONCAT, + _ACCT_MAP_ITEM, + _ACCOUNT_CELL, + _GET_ENTRY, + ], ) ], ) @@ -227,6 +262,13 @@ def test_resolve_sorts(test_id: str, label: KLabel, expected_result: KSort, expe KApply(KLabel('foo'), [KVariable('X')]), KApply(KLabel('foo'), [KVariable('X')]), ), + # Subsort-aware: arg sort is Int, but MInt{Int} <: Int in DEFN, so N=Int via subsort match + # (this case would fail with structural-only unification since Int ≠ MInt{N}) + ( + 'subsort_aware', + KApply(KLabel('foo'), [KVariable('X', sort=INT)]), + KApply(KLabel('foo', [INT]), [KVariable('X', sort=INT)]), + ), ) @@ -257,6 +299,115 @@ def test_add_sort_params_user_label_unresolvable_warns(caplog: pytest.LogCapture assert any('could not infer sort params' in record.message for record in caplog.records) +# --------------------------------------------------------------------------- +# KDefinition.infer_sort_params +# --------------------------------------------------------------------------- +# +# Tests the public method directly (not through add_sort_params), mirroring the +# Java AddSortInjections.substituteProd() test scenarios derived from the algorithm. + +INFER_SORT_PARAMS_DATA: Final[ + tuple[tuple[str, KProduction, tuple[KSort | None, ...], KSort | None, dict[KSort, KSort]], ...] +] = ( + # Direct param: psort IS the param (N → Int) + ('direct_param', _BAR_PROD, (INT,), None, {N: INT}), + # Nested param: psort = MInt{N}, asort = MInt{Int} → N=Int via structural match + ('nested_param', _FOO_PROD, (MINT_INT,), None, {N: INT}), + # Subsort-aware: arg sort is Int, MInt{Int} <: Int in DEFN → N=Int via subsort iteration + # (structural match fails: MInt{N} ≠ Int; subsort check finds MInt{Int} ≤ Int) + ('subsort_aware', _FOO_PROD, (INT,), None, {N: INT}), + # matchExpected: baz() has no arg sorts; N is bound from the expected_sort MInt{Int} + ('expected_sort', _BAZ_PROD, (), MINT_INT, {N: INT}), + # None arg is skipped; no bindings → empty result + ('unbound_absent', _BAR_PROD, (None,), None, {}), +) + + +@pytest.mark.parametrize( + 'test_id,prod,actual_sorts,expected_sort,expected_bindings', + INFER_SORT_PARAMS_DATA, + ids=[test_id for test_id, *_ in INFER_SORT_PARAMS_DATA], +) +def test_infer_sort_params( + test_id: str, + prod: KProduction, + actual_sorts: tuple[KSort | None, ...], + expected_sort: KSort | None, + expected_bindings: dict[KSort, KSort], +) -> None: + assert DEFN.infer_sort_params(prod, actual_sorts, expected_sort) == expected_bindings + + +# --------------------------------------------------------------------------- +# _match_sort_params (module-level helper) +# --------------------------------------------------------------------------- +# +# Directly tests the three matching strategies described in the docstring. + + +def _subsorts_fn(s: KSort) -> frozenset[KSort]: + return frozenset({MINT_INT}) if s == INT else frozenset() + + +MATCH_SORT_PARAMS_DATA: Final[ + tuple[ + tuple[ + str, KSort, KSort, frozenset[KSort], Callable[[KSort], frozenset[KSort]] | None, dict[KSort, list[KSort]] + ], + ..., + ] +] = ( + # Case 1 – direct: parametric IS a sort param + ('direct', N, INT, frozenset({N}), None, {N: [INT]}), + # Case 2 – structural: same head, recurse on sub-params + ('structural', MINT_N, MINT_INT, frozenset({N}), None, {N: [INT]}), + # Case 2 fails (different heads), no subsorts_fn → empty + ('structural_no_match_no_subsorts', MINT_N, INT, frozenset({N}), None, {}), + # Case 3 – subsort-aware: MInt{N} vs Int; subsorts_fn yields MInt{Int} → N=Int + ('subsort_aware', MINT_N, INT, frozenset({N}), _subsorts_fn, {N: [INT]}), + # No match in any case + ('no_match', INT, KSort('Bool'), frozenset({N}), None, {}), +) + + +@pytest.mark.parametrize( + 'test_id,parametric,actual,params,subsorts_fn,expected', + MATCH_SORT_PARAMS_DATA, + ids=[test_id for test_id, *_ in MATCH_SORT_PARAMS_DATA], +) +def test_match_sort_params( + test_id: str, + parametric: KSort, + actual: KSort, + params: frozenset[KSort], + subsorts_fn: Callable[[KSort], frozenset[KSort]] | None, + expected: dict[KSort, list[KSort]], +) -> None: + assert _match_sort_params(parametric, actual, params, subsorts_fn) == expected + + +# --------------------------------------------------------------------------- +# _sort_contains (module-level helper) +# --------------------------------------------------------------------------- + +SORT_CONTAINS_DATA: Final = ( + ('param_itself', N, N, True), + ('nested_one_level', MINT_N, N, True), + ('nested_two_levels', KSort('Foo', (MINT_N,)), N, True), + ('concrete_not_param', MINT_INT, N, False), + ('unrelated', INT, N, False), +) + + +@pytest.mark.parametrize( + 'test_id,sort,param,expected', + SORT_CONTAINS_DATA, + ids=[test_id for test_id, *_ in SORT_CONTAINS_DATA], +) +def test_sort_contains(test_id: str, sort: KSort, param: KSort, expected: bool) -> None: + assert _sort_contains(sort, param) == expected + + # --------------------------------------------------------------------------- # KDefinition.add_cell_map_items # ---------------------------------------------------------------------------