prelude/k, konvert/_kast_to_kore, outer: fail clearly on #SortParam sentinel; document full fix

add_sort_params fills an uninferable ML-predicate result sort with the
#SortParam sentinel sort, but _ksort_to_kore had no handling for it: it built
SortApp('Sort#SortParam'), which crashes the Kore Id constructor ('#' is not a
legal identifier char). Emitting it correctly needs a universally-quantified
sort variable bound at the axiom level (Java's sortParams scheme), which is a
larger change requiring integration-level validation.

Until that lands, reject the sentinel in _ksort_to_kore with a clear, actionable
error instead of a cryptic crash, and document the full fix.

- prelude/k: define the shared SORT_PARAM_SENTINEL sort, used by both the
  inference site (add_sort_params) and the emission site (_ksort_to_kore).
- konvert/_kast_to_kore: _ksort_to_kore raises a descriptive ValueError for any
  member of the sentinel family (name startswith match), pointing at the design doc.
- test_konvert: cover the ordinary-sort path and sentinel rejection (bare and
  uniquely-named forms).
- docs/sortparam-kore-emission.md: design for the full sentinel -> sort-variable fix.
- outer: source the sentinel from prelude/k; note the Kore emission step is not yet implemented.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: ehildenb

pyk/docs/sortparam-kore-emission.md

@@ -0,0 +1,59 @@
+# Emitting the `#SortParam` sentinel to Kore
+
+## Status
+
+Not implemented.
+`_ksort_to_kore` raises a clear error when it encounters the sentinel, rather than producing invalid Kore.
+This document describes the full fix so it can be implemented and validated against real Kore output later.
+
+## Background
+
+Some ML-predicate productions have a result sort that cannot be inferred from their arguments.
+The canonical example is `#Equals{S1, S2}(S1, S1)`: `S1` is determined by the arguments, but `S2` (the result sort) is context-dependent.
+When `KDefinition.add_sort_params` fills in a partially-applied ML-predicate label, it can determine `S1` but not `S2`, so it fills `S2` with the sentinel sort `KSort('#SortParam')` (see `add_sort_params` in `src/pyk/kast/outer.py`).
+
+The Java frontend (`org.kframework.compile.AddSortInjections`) does the same thing, but with two differences that matter for Kore emission:
+
+- It generates a *fresh, uniquely named* sentinel per unresolved position: `#SortParam{Q0}`, `#SortParam{Q1}`, ….
+- It collects those `Qn` names during the traversal and declares them as universally-quantified sort variables on the resulting axiom (surfaced in the `sortParams(...)` rule attribute, and as sort parameters on the Kore `axiom{...}`).
+
+## The problem in pyk
+
+`_ksort_to_kore` (in `src/pyk/konvert/_kast_to_kore.py`) is a context-free, term-level converter: it maps every `KSort` to `SortApp('Sort' + name)`.
+For the sentinel this yields `SortApp('Sort#SortParam')`, which is doubly wrong:
+
+- `#` is not a legal Kore identifier character, so the `SortApp`/`Id` constructor raises `ValueError: Expected identifier`.
+- Even if it were constructible, a bare sort application referencing a sort that exists in no definition is not what the sentinel means — it must be a *bound sort variable*.
+
+`krule_to_kore` builds an axiom by calling `kast_to_kore` several independent times (lhs body, rhs body, each constraint), and sets the axiom's sort variables (`Axiom.vars`) to `()` for ordinary rules or `(SortVar('R'),)` for functional rules.
+There is no mechanism to (a) emit the sentinel as a sort variable, (b) give it a unique name, or (c) collect it back up and bind it on the axiom.
+
+## Reachability
+
+In the normal pyk flow this path is rarely hit.
+ML predicates constructed through the prelude (`mlEquals`, `mlEqualsTrue`, `bool_to_ml_pred`, …) always pass explicit sort params (e.g. `KLabel('#Equals', arg_sort, sort)`), so they hit the early return in `add_sort_params` and never produce the sentinel.
+The sentinel only arises for ML predicates that reach `add_sort_params` with *missing* sort params (e.g. frontend-loaded or hand-constructed terms) and whose result sort cannot be inferred.
+
+## Proposed fix
+
+The goal is to mirror the Java behaviour: each unresolved result sort becomes a uniquely-named, universally-quantified Kore sort variable on the enclosing axiom.
+
+1. **Unique sentinels.**
+   Replace the single bare `KSort('#SortParam')` with parametric sentinels `KSort('#SortParam', (KSort('Q0'),))`, `KSort('#SortParam', (KSort('Q1'),))`, ….
+   This removes the current "at most one unbound param" restriction (the `NotImplementedError` guard in `add_sort_params`) and lets distinct unresolved positions stay distinct.
+   Generating fresh names requires a counter; since `add_sort_params` runs per `kast_to_kore` call, the counter must be threaded from `krule_to_kore` (or `add_sort_params` must accept a starting index and return the names it used) so that names are unique *across* the several `kast_to_kore` calls that make up one axiom.
+
+2. **Emit sentinels as sort variables.**
+   Teach `_ksort_to_kore` (or the `_kapply_to_pattern` sort-emission path) to map `#SortParam{Qn}` to `SortVar('Qn')` instead of a `SortApp`.
+
+3. **Bind them on the axiom.**
+   `krule_to_kore` collects every `SortVar` emitted from a sentinel across all of its `kast_to_kore` calls and adds them to `Axiom.vars` (alongside `R` for functional rules), and to the `sortParams(...)` attribute, matching the Java output.
+
+## Validation
+
+This change alters Kore axiom output and must be validated end-to-end, not just at the unit level:
+
+- The konvert integration tests (`src/tests/integration/konvert/`), which require the K toolchain.
+- The pyk regression suite (`pyk/regression-new/`), comparing emitted Kore against the Java backend for a definition that actually exercises an uninferable ML-predicate result sort.
+
+A minimal repro to build first: a rule (loaded from a compiled definition, not constructed via the prelude) containing an ML predicate whose result sort is not determined by its arguments, asserting the emitted axiom binds a sort variable rather than referencing `Sort#SortParam`.

pyk/src/pyk/kast/outer.py

@@ -31,7 +31,7 @@
     top_down,
 )
 from .kast import kast_term
-from .prelude.k import K_ITEM, K
+from .prelude.k import K_ITEM, SORT_PARAM_SENTINEL, K
 from .rewrite import indexed_rewrite
 
 if TYPE_CHECKING:
@@ -1667,8 +1667,10 @@ def add_sort_params(self, kast: KInner) -> KInner:
         # 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
+        # universally-quantified sort variable (Q0) in the axiom.  NOTE: that Kore emission step
+        # is not yet implemented — _ksort_to_kore rejects the sentinel with a clear error.  See
+        # pyk/docs/sortparam-kore-emission.md for the design of the full fix.
+        _ML_PRED_RESULT_SORT_PARAM = SORT_PARAM_SENTINEL  # noqa: N806
         _ML_PRED_LABELS = frozenset({'#Equals', '#Ceil', '#Floor', '#In'})  # noqa: N806
 
         def _add_sort_params(_k: KInner) -> KInner:

pyk/src/pyk/kast/prelude/k.py

@@ -14,6 +14,12 @@
 K_ITEM: Final = KSort('KItem')
 GENERATED_TOP_CELL: Final = KSort('GeneratedTopCell')
 
+# Sentinel sort marking an ML-predicate result sort that could not be inferred from arguments
+# (introduced by KDefinition.add_sort_params).  The family also covers uniquely-named variants
+# such as `#SortParam{Q0}` once those are generated.  This sort cannot yet be emitted to Kore;
+# see pyk/docs/sortparam-kore-emission.md.
+SORT_PARAM_SENTINEL: Final = KSort('#SortParam')
+
 DOTS: Final = KToken('...', K)
 
 

pyk/src/pyk/konvert/_kast_to_kore.py

@@ -9,7 +9,7 @@
 from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, ml_pred_to_bool, var_occurrences
 from ..kast.outer import KRule
 from ..kast.prelude.bytes import BYTES, pretty_bytes_str
-from ..kast.prelude.k import K_ITEM, K, inj
+from ..kast.prelude.k import K_ITEM, SORT_PARAM_SENTINEL, K, inj
 from ..kast.prelude.kbool import BOOL, TRUE, andBool
 from ..kast.prelude.ml import mlAnd
 from ..kast.prelude.string import STRING, pretty_string
@@ -356,6 +356,18 @@ def _kimport_to_kore(kimport: KImport) -> Import:
 
 
 def _ksort_to_kore(ksort: KSort) -> SortApp:
+    # Emitting the #SortParam sentinel correctly requires a universally-quantified sort variable
+    # bound at the axiom level (a `sortParams({Q0})` attribute, as Java's AddSortInjections does);
+    # this term-level converter has no way to introduce or bind one.  Fail clearly rather than
+    # building the invalid Kore identifier `Sort#SortParam` ('#' is not a legal identifier char).
+    # `startswith` covers the whole sentinel family (e.g. a future `#SortParam{Q0}`).  The full
+    # design is in pyk/docs/sortparam-kore-emission.md.
+    if ksort.name.startswith(SORT_PARAM_SENTINEL.name):
+        raise ValueError(
+            f'Cannot emit the {SORT_PARAM_SENTINEL.name} sentinel sort to Kore: it marks an ML-predicate '
+            'result sort that add_sort_params could not infer and that must become an axiom-level '
+            'sort variable. This is not yet implemented; see pyk/docs/sortparam-kore-emission.md.'
+        )
     return SortApp('Sort' + ksort.name)
 
 

pyk/src/tests/unit/test_konvert.py

@@ -5,7 +5,11 @@
 
 import pytest
 
+from pyk.kast.inner import KSort
+from pyk.kast.prelude.k import SORT_PARAM_SENTINEL
 from pyk.konvert import munge, unmunge
+from pyk.konvert._kast_to_kore import _ksort_to_kore
+from pyk.kore.syntax import SortApp
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
@@ -49,3 +53,23 @@ def test_unmunge(symbol: str, expected: str) -> None:
 
     # Then
     assert actual == expected
+
+
+def test_ksort_to_kore_ordinary_sort() -> None:
+    assert _ksort_to_kore(KSort('Int')) == SortApp('SortInt')
+
+
+@pytest.mark.parametrize(
+    'sentinel',
+    (
+        SORT_PARAM_SENTINEL,  # bare sentinel
+        KSort(SORT_PARAM_SENTINEL.name, (KSort('Q0'),)),  # uniquely-named family member
+    ),
+    ids=['bare', 'parametric'],
+)
+def test_ksort_to_kore_rejects_sortparam_sentinel(sentinel: KSort) -> None:
+    # The #SortParam sentinel family cannot yet be emitted to Kore (it needs an axiom-level sort
+    # variable); _ksort_to_kore must fail with a clear, actionable error rather than building the
+    # invalid identifier `Sort#SortParam`.  See pyk/docs/sortparam-kore-emission.md.
+    with pytest.raises(ValueError, match=SORT_PARAM_SENTINEL.name):
+        _ksort_to_kore(sentinel)