Skip to content

Handle sort parameters correctly in JSON Kast format #4913

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ehildenb wants to merge 6 commits into
base: develop
Choose a base branch
from
Open

Handle sort parameters correctly in JSON Kast format #4913

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
c80d18c
ToJson, JsonParser, kast/{kast,inner,att}, prelude-modules.json, test…
ehildenb Apr 24, 2026
6a72390
konvert/_module_to_kore, test_module_to_kore: fix parameterized sort …
ehildenb Apr 24, 2026
df22648
JsonParser, kast/{inner,att}, profiling/test-data: remove v3 compat, …
ehildenb Apr 24, 2026
026a4a6
JsonParser: remove unused Outer import
ehildenb Apr 24, 2026
d6e3460
regression-new/: migrate KAST fixture v3→v4
ehildenb Apr 24, 2026
25807ba
pyk/regression-new: update baselines for KAST v4 variable hashes
ehildenb Apr 24, 2026
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 k-distribution/tests/regression-new/imp-outer-json/imp.json
View file
Open in desktop

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/json-input/json-in1.json.kast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"4"}]}}
{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"4"}]}}
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/json-input/json-in2.json.kast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"}]}}
{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"}]}}
2 changes: 1 addition & 1 deletion k-distribution/tests/regression-new/json-input/json-in3.json.kast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K"}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0"}]}]}}
{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K","params":[]}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"0"}]}]}}
8 changes: 6 additions & 2 deletions k-frontend/src/main/java/org/kframework/parser/json/JsonParser.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,6 @@
import org.kframework.kore.KLabel;
import org.kframework.kore.KORE;
import org.kframework.kore.Sort;
import org.kframework.parser.outer.Outer;
import org.kframework.parser.outer.ParseRegex;
import org.kframework.unparser.ToJson;
import org.kframework.utils.errorsystem.KEMException;
Expand Down Expand Up @@ -288,7 +287,12 @@ private static Sort toSort(JsonObject data) {
if (!data.getString("node").equals(KSORT))
throw KEMException.criticalError(
"Unexpected node found in KAST Json term: " + data.getString("node"));
return Outer.parseSort(data.getString("name"));
String name = data.getString("name");
List<Sort> params = new ArrayList<>();
for (JsonValue p : data.getJsonArray("params")) {
params.add(toSort((JsonObject) p));
}
return Sort(name, params);
}

private static ProductionItem toProductionItem(JsonObject data) {
Expand Down
10 changes: 5 additions & 5 deletions k-frontend/src/main/java/org/kframework/unparser/ToJson.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@
/** Writes a KAST term to the KAST Json format. */
public class ToJson {

public static final int version = 3;
public static final int version = 4;

///////////////////////////////
// ToJson Definition Objects //
Expand Down Expand Up @@ -381,11 +381,11 @@ public static JsonObject toJson(ProductionItem prod) {

public static JsonStructure toJson(Sort sort) {
JsonObjectBuilder jsort = factory.createObjectBuilder();

jsort.add("node", JsonParser.KSORT);
// store sort and its parameters as a flat string
jsort.add("name", sort.toString());

jsort.add("name", sort.name());
JsonArrayBuilder jparams = factory.createArrayBuilder();
JavaConverters.seqAsJavaList(sort.params()).forEach(p -> jparams.add(toJson(p)));
jsort.add("params", jparams.build());
return jsort.build();
}

Expand Down
1 change: 1 addition & 0 deletions pyk/regression-new/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
*-kompiled/
2 changes: 1 addition & 1 deletion pyk/regression-new/json-input/json-in1.json.kast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"4"}]}}
{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"4"}]}}
2 changes: 1 addition & 1 deletion pyk/regression-new/json-input/json-in2.json.kast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K"},{"node":"KSort","name":"K"}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"3"}]}}
{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#Equals","params":[{"node":"KSort","name":"K","params":[]},{"node":"KSort","name":"K","params":[]}]},"arity":2,"args":[{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"3"}]}}
2 changes: 1 addition & 1 deletion pyk/regression-new/json-input/json-in3.json.kast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"format":"KAST","version":3,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K"}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int"},"token":"0"}]}]}}
{"format":"KAST","version":4,"term":{"node":"KApply","label":{"node":"KLabel","name":"#And","params":[{"node":"KSort","name":"K","params":[]}]},"variable":false,"arity":2,"args":[{"node":"KApply","label":{"node":"KLabel","name":"<k>","params":[]},"variable":false,"arity":1,"args":[{"node":"KVariable","name":"N"}]},{"node":"KApply","label":{"node":"KLabel","name":"_>=Int_","params":[]},"variable":false,"arity":2,"args":[{"node":"KVariable","name":"N"},{"node":"KToken","sort":{"node":"KSort","name":"Int","params":[]},"token":"0"}]}]}}
48 changes: 24 additions & 24 deletions pyk/regression-new/kprove-haskell/sum-spec.k.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Subproofs: 0
│ <generatedTop>
│ <k>
│ addCounter ( N:Int )
│ ~> K_CELL_fc656f08:K
│ ~> K_CELL_f6d31965:K
│ </k>
│ <counter>
│ C:Int
Expand All @@ -25,7 +25,7 @@ Subproofs: 0
│ S:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_949ec677:Int
│ GENERATEDCOUNTER_CELL_e7e8d4ca:Int
│ </generatedCounter>
│ </generatedTop>
│ #And { true #Equals N:Int >=Int 0 }
Expand All @@ -39,7 +39,7 @@ Subproofs: 0
┃ │ <generatedTop>
┃ │ <k>
┃ │ addCounter ( N:Int )
┃ │ ~> K_CELL_fc656f08:K
┃ │ ~> K_CELL_f6d31965:K
┃ │ </k>
┃ │ <counter>
┃ │ C:Int
Expand All @@ -48,7 +48,7 @@ Subproofs: 0
┃ │ S:Int
┃ │ </sum>
┃ │ <generatedCounter>
┃ │ GENERATEDCOUNTER_CELL_949ec677:Int
┃ │ GENERATEDCOUNTER_CELL_e7e8d4ca:Int
┃ │ </generatedCounter>
┃ │ </generatedTop>
┃ │ #And { true #Equals N:Int >Int 0 }
Expand All @@ -59,7 +59,7 @@ Subproofs: 0
┃ │ <generatedTop>
┃ │ <k>
┃ │ addCounter ( N:Int +Int -1 )
┃ │ ~> K_CELL_fc656f08:K
┃ │ ~> K_CELL_f6d31965:K
┃ │ </k>
┃ │ <counter>
┃ │ C:Int +Int 1
Expand All @@ -68,7 +68,7 @@ Subproofs: 0
┃ │ S:Int +Int C:Int
┃ │ </sum>
┃ │ <generatedCounter>
┃ │ GENERATEDCOUNTER_CELL_949ec677:Int
┃ │ GENERATEDCOUNTER_CELL_e7e8d4ca:Int
┃ │ </generatedCounter>
┃ │ </generatedTop>
┃ │ #And { true #Equals N:Int >Int 0 }
Expand All @@ -78,16 +78,16 @@ Subproofs: 0
┃ ├─ 7
┃ │ <generatedTop>
┃ │ <k>
┃ │ K_CELL_fc656f08:K
┃ │ K_CELL_f6d31965:K
┃ │ </k>
┃ │ <counter>
┃ │ ?_COUNTER_CELL_af8c44a5:Int
┃ │ ?_COUNTER_CELL_c8750430:Int
┃ │ </counter>
┃ │ <sum>
┃ │ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2
┃ │ </sum>
┃ │ <generatedCounter>
┃ │ ?_GENERATEDCOUNTER_CELL_5e3e01ba:Int
┃ │ ?_GENERATEDCOUNTER_CELL_3227d86a:Int
┃ │ </generatedCounter>
┃ │ </generatedTop>
┃ │ #And { true #Equals N:Int >Int 0 }
Expand All @@ -97,21 +97,21 @@ Subproofs: 0
┃ ┊ constraint:
┃ ┊ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 ==K S:Int +Int N:Int *Int C:Int +Int N:Int +Int -1 *Int N:Int /Int 2
┃ ┊ subst:
┃ ┊ ?_COUNTER_CELL_af8c44a5 <- COUNTER_CELL_af8c44a5:Int
┃ ┊ ?_GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_5e3e01ba:Int
┃ ┊ ?_COUNTER_CELL_c8750430 <- COUNTER_CELL_c8750430:Int
┃ ┊ ?_GENERATEDCOUNTER_CELL_3227d86a <- GENERATEDCOUNTER_CELL_3227d86a:Int
┃ └─ 2 (leaf, target)
┃ <generatedTop>
┃ <k>
┃ K_CELL_fc656f08:K ~> .K
┃ K_CELL_f6d31965:K ~> .K
┃ </k>
┃ <counter>
┃ COUNTER_CELL_af8c44a5:Int
┃ COUNTER_CELL_c8750430:Int
┃ </counter>
┃ <sum>
┃ ?S:Int
┃ </sum>
┃ <generatedCounter>
┃ GENERATEDCOUNTER_CELL_5e3e01ba:Int
┃ GENERATEDCOUNTER_CELL_3227d86a:Int
┃ </generatedCounter>
┃ </generatedTop>
┃ #And { true #Equals N:Int >=Int 0 }
Expand All @@ -125,7 +125,7 @@ Subproofs: 0
│ <generatedTop>
│ <k>
│ addCounter ( N:Int )
│ ~> K_CELL_fc656f08:K
│ ~> K_CELL_f6d31965:K
│ </k>
│ <counter>
│ C:Int
Expand All @@ -134,7 +134,7 @@ Subproofs: 0
│ S:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_949ec677:Int
│ GENERATEDCOUNTER_CELL_e7e8d4ca:Int
│ </generatedCounter>
│ </generatedTop>
│ #And { N:Int #Equals 0 }
Expand All @@ -144,7 +144,7 @@ Subproofs: 0
├─ 6
│ <generatedTop>
│ <k>
│ K_CELL_fc656f08:K
│ K_CELL_f6d31965:K
│ </k>
│ <counter>
│ C:Int
Expand All @@ -153,29 +153,29 @@ Subproofs: 0
│ S:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_949ec677:Int
│ GENERATEDCOUNTER_CELL_e7e8d4ca:Int
│ </generatedCounter>
│ </generatedTop>
│ #And { N:Int #Equals 0 }
│
┊ constraint:
┊ S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_af8c44a5:Int +Int N:Int +Int -1 *Int N:Int /Int 2
┊ S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_c8750430:Int +Int N:Int +Int -1 *Int N:Int /Int 2
┊ subst:
┊ C <- COUNTER_CELL_af8c44a5:Int
┊ GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_949ec677:Int
┊ C <- COUNTER_CELL_c8750430:Int
┊ GENERATEDCOUNTER_CELL_3227d86a <- GENERATEDCOUNTER_CELL_e7e8d4ca:Int
└─ 2 (leaf, target)
<generatedTop>
<k>
K_CELL_fc656f08:K ~> .K
K_CELL_f6d31965:K ~> .K
</k>
<counter>
COUNTER_CELL_af8c44a5:Int
COUNTER_CELL_c8750430:Int
</counter>
<sum>
?S:Int
</sum>
<generatedCounter>
GENERATEDCOUNTER_CELL_5e3e01ba:Int
GENERATEDCOUNTER_CELL_3227d86a:Int
</generatedCounter>
</generatedTop>
#And { true #Equals N:Int >=Int 0 }
Expand Down
10 changes: 5 additions & 5 deletions pyk/regression-new/kprove-haskell/test-fail-spec.k.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ Failing nodes:
Matching failed.
The following cells failed matching individually (antecedent #Implies consequent):
K_CELL: doIt ( -3 #Implies 0 )
~> K_CELL_fc656f08:K
~> K_CELL_f6d31965:K
Path condition:
#Top
Failed to generate a model.
Expand All @@ -31,7 +31,7 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur
│ <generatedTop>
│ <k>
│ doIt ( -3 )
│ ~> K_CELL_fc656f08:K
│ ~> K_CELL_f6d31965:K
│ </k>
│ <counter>
│ COUNTER_CELL
Expand All @@ -40,15 +40,15 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur
│ SUM_CELL
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_c84b0b5f:Int
│ GENERATEDCOUNTER_CELL_ae2db996:Int
│ </generatedCounter>
│ </generatedTop>

┌─ 2 (root, leaf, target)
│ <generatedTop>
│ <k>
│ doIt ( 0 )
│ ~> K_CELL_fc656f08:K
│ ~> K_CELL_f6d31965:K
│ </k>
│ <counter>
│ COUNTER_CELL
Expand All @@ -57,7 +57,7 @@ Join the Runtime Verification Discord server for support: https://discord.gg/Cur
│ SUM_CELL
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_6de8d71b:Int
│ GENERATEDCOUNTER_CELL_73eeffd3:Int
│ </generatedCounter>
│ </generatedTop>

Expand Down
14 changes: 7 additions & 7 deletions pyk/regression-new/kprove-haskell/test-spec.k.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Subproofs: 0
│ <generatedTop>
│ <k>
│ doIt ( 3 )
│ ~> K_CELL_fc656f08:K
│ ~> K_CELL_f6d31965:K
│ </k>
│ <counter>
│ COUNTER_CELL
Expand All @@ -25,7 +25,7 @@ Subproofs: 0
│ SUM_CELL
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_c84b0b5f:Int
│ GENERATEDCOUNTER_CELL_ae2db996:Int
│ </generatedCounter>
│ </generatedTop>
│
Expand All @@ -34,7 +34,7 @@ Subproofs: 0
│ <generatedTop>
│ <k>
│ doIt ( 0 )
│ ~> K_CELL_fc656f08:K
│ ~> K_CELL_f6d31965:K
│ </k>
│ <counter>
│ COUNTER_CELL:Int
Expand All @@ -43,18 +43,18 @@ Subproofs: 0
│ SUM_CELL:Int
│ </sum>
│ <generatedCounter>
│ GENERATEDCOUNTER_CELL_c84b0b5f:Int
│ GENERATEDCOUNTER_CELL_ae2db996:Int
│ </generatedCounter>
│ </generatedTop>
│
┊ constraint: true
┊ subst:
┊ GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
┊ GENERATEDCOUNTER_CELL_73eeffd3 <- GENERATEDCOUNTER_CELL_ae2db996:Int
└─ 2 (leaf, target)
<generatedTop>
<k>
doIt ( 0 )
~> K_CELL_fc656f08:K
~> K_CELL_f6d31965:K
</k>
<counter>
COUNTER_CELL
Expand All @@ -63,7 +63,7 @@ Subproofs: 0
SUM_CELL
</sum>
<generatedCounter>
GENERATEDCOUNTER_CELL_6de8d71b:Int
GENERATEDCOUNTER_CELL_73eeffd3:Int
</generatedCounter>
</generatedTop>

Expand Down
20 changes: 12 additions & 8 deletions pyk/src/pyk/kast/inner.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,25 +27,29 @@
@final
@dataclass(frozen=True)
class KSort(KAst):
"""Store a simple sort name."""
"""Represent a K sort, optionally applied to sort parameters."""

name: str
params: tuple[KSort, ...]

def __init__(self, name: str):
"""Construct a new sort given the name."""
def __init__(self, name: str, params: Iterable[KSort] = ()):
object.__setattr__(self, 'name', name)
object.__setattr__(self, 'params', tuple(params))

@staticmethod
def from_dict(d: Mapping[str, Any]) -> KSort:
return KSort(name=d['name'])
return KSort(
name=d['name'],
params=(KSort.from_dict(p) for p in d.get('params', ())),
)

def to_dict(self) -> dict[str, Any]:
return {'node': 'KSort', 'name': self.name}
return {'node': 'KSort', 'name': self.name, 'params': [p.to_dict() for p in self.params]}

def let(self, *, name: str | None = None) -> KSort:
"""Return a new `KSort` with the name potentially updated."""
def let(self, *, name: str | None = None, params: Iterable[KSort] | None = None) -> KSort:
name = name if name is not None else self.name
return KSort(name=name)
params = params if params is not None else self.params
return KSort(name=name, params=params)


@final
Expand Down
2 changes: 1 addition & 1 deletion pyk/src/pyk/kast/kast.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@
class KAst(ABC):
@staticmethod
def version() -> int:
return 3
return 4

@abstractmethod
def to_dict(self) -> dict[str, Any]: ...
Expand Down
Loading
Loading