Skip to content

Commit 54b9fb6

Browse files
ehildenbclaude
ehildenb
and
claude
authored
Support Claude as developer, add --top-cell flag to pyk kompile (#4912)
After a Claude analysis of the tests skipped in pyk/regression-new, I have made some small progress on supporting more tests in that test-suite with pyk. In particular: - Add a `CLAUDE.md` for helping with Claude development. - Add some to `.gitignore` for ignoring generated `*-kompiled` directories. - Add some design document/context files to `pyk/docs/...` for the discovery of the remaining processes to be done for supporting the entire kompilation pipeline in Python directly. - Add the flag `--top-cell` to `pyk kompile` and thread it htrough appropriately, uncomment one test that passes now. --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 5f7c0bd commit 54b9fb6

9 files changed

Lines changed: 476 additions & 7 deletions

File tree

‎CLAUDE.md‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
2+
3+
# K Framework — Agent Guide
4+
5+
## Project Overview
6+
7+
The K Framework is a language-agnostic formal specification and verification framework developed by Runtime Verification.
8+
It lets you define programming language semantics in `.k` files and then automatically derives an interpreter, model checker, and deductive verifier from that definition.
9+
10+
The repository is a monorepo with two independent technology stacks:
11+
12+
- **Java/Scala** — the K compiler toolchain (`kompile`, `krun`, `kprove`, etc.)
13+
- **Python** (`pyk/`) — the `kframework` Python SDK for programmatically interacting with the K toolchain
14+
15+
## Repository Structure
16+
17+
```
18+
k-frontend/ K language parser and frontend (Java/Scala)
19+
k-distribution/ Main distribution bundle
20+
bin/, lib/ Symlinks into target/release/k/
21+
include/kframework/ Shared Makefile infrastructure (ktest.mak, ktest-group.mak)
22+
tests/regression-new/ Java-backend regression suite (229 test subdirs)
23+
haskell-backend/ Haskell-based symbolic backend
24+
llvm-backend/ LLVM-based concrete execution backend
25+
pyk/ Python SDK sub-project (self-contained)
26+
src/pyk/ Package source (cli, kast, kore, proof, kcfg, kdist, …)
27+
src/tests/ pytest test suite (unit/, integration/)
28+
regression-new/ Python-backend regression suite (213 test subdirs)
29+
pyproject.toml Build & tool config (hatchling, black, mypy, flake8, …)
30+
Makefile All pyk make targets
31+
k-tutorial/ Tutorial K definitions
32+
```
33+
34+
## Build
35+
36+
### Java (compile only, skip tests)
37+
38+
```
39+
mvn package -DskipTests
40+
```
41+
42+
This compiles all Maven modules (`k-frontend`, `k-distribution`, `haskell-backend`, `llvm-backend`) and produces JARs under each module's `target/` directory.
43+
Java 17 and Scala 2.13 are required.
44+
45+
### Python
46+
47+
The `pyk/` sub-project uses `hatchling` as its build backend and `uv` as its package manager.
48+
No explicit build step is needed before running lint or tests — the make targets handle installation.
49+
50+
## Lint
51+
52+
### Java
53+
54+
```
55+
mvn spotless:apply
56+
```
57+
58+
This auto-formats all Java/Scala sources (Google Java Format + Scalafmt).
59+
Run it after every Java change; commits must pass `mvn spotless:check`.
60+
61+
### Python
62+
63+
```
64+
make -C pyk check
65+
```
66+
67+
This runs, in order: `black --check`, `isort --check`, `autoflake --check`, `flake8`, `mypy`, `pydocstyle`.
68+
69+
To auto-apply all formatters:
70+
71+
```
72+
make -C pyk format
73+
```
74+
75+
Key style settings (from `pyk/pyproject.toml`):
76+
- `black`: line-length 120, skip-string-normalization
77+
- `isort`: black profile, line-length 120
78+
- `mypy`: `disallow_untyped_defs = true`
79+
- `pydocstyle`: Google convention
80+
81+
## Tests
82+
83+
There are four distinct test surfaces.
84+
85+
### 1. Java unit tests
86+
87+
```
88+
mvn verify
89+
```
90+
91+
Runs all JUnit 4 tests across `k-frontend` and `k-distribution` via Maven Surefire.
92+
Tests run with `LC_NUMERIC=en_US.UTF-8`.
93+
94+
### 2. Python unit + integration tests
95+
96+
```
97+
make -C pyk test
98+
```
99+
100+
Runs `src/tests/unit/` and `src/tests/integration/` with 4 parallel workers (pytest-xdist, worksteal).
101+
Unit tests only (faster, no K toolchain required):
102+
103+
```
104+
make -C pyk test-unit
105+
```
106+
107+
### 3. Java regression tests
108+
109+
```
110+
make -C k-distribution/tests/regression-new
111+
```
112+
113+
229 subdirectory test cases.
114+
Each test compiles a `.k` definition with `kompile` and executes it with `krun` or `kprove`, comparing output against `.out` baseline files.
115+
The shared test infrastructure lives in `k-distribution/include/kframework/ktest.mak`.
116+
117+
### 4. Python regression tests
118+
119+
```
120+
make -C pyk/regression-new
121+
```
122+
123+
213 subdirectory test cases; 113 are currently skipped (listed in `pyk/regression-new/skipped`).
124+
Same test infrastructure as the Java regression suite but exercises pyk-specific code paths.
125+
126+
## Updating Regression Baselines
127+
128+
If a change intentionally alters K program output, regenerate the `.out` files:
129+
130+
```
131+
make -C k-distribution/tests/regression-new update-results
132+
make -C pyk/regression-new update-results
133+
```
134+
135+
Commit the updated baseline files in a dedicated commit after the logic change.

‎pyk/docs/pipeline.md‎

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
# K Compilation Pipeline — Developer Reference
2+
3+
This document describes the K compilation pipeline, where pyk already participates, and the integration points for moving more of the pipeline from Java to Python.
4+
5+
## Overview
6+
7+
The pipeline has five logical stages:
8+
9+
```
10+
Outer parsing → Inner parsing → 32 compilation passes → Kore emission → Backend compilation
11+
```
12+
13+
The first four stages produce `definition.kore`.
14+
The fifth stage (LLVM/Haskell backend compilation) consumes `definition.kore` and is inherently backend-specific.
15+
16+
## Stage 1: Outer Parsing
17+
18+
**What it does**: Reads `.k` and `.md` files, resolves `require` statements, and produces a `KDefinition` (a set of `KFlatModule`s with import edges but with rule bodies still as unparsed "bubbles").
19+
20+
**Java implementation**: JavaCC grammar at `k-frontend/src/main/javacc/Outer.jj`; entry point `DefinitionParsing.parseDefinition()`.
21+
22+
**Python implementation**: `pyk/src/pyk/kast/outer_parser.py` + `outer_lexer.py`; entry point `pyk.kast.utils.parse_outer()`.
23+
24+
**Pipeline seam**: Java `kompile` accepts `--outer-parsed-json`, which reads a pre-parsed `KDefinition` JSON from a file and skips the Java outer parsing stage entirely.
25+
The JSON format is `{"format": "KAST", "version": 3, "term": <KDefinition.to_dict()>}`.
26+
27+
**`kompilex` command** (`pyk/src/pyk/__main__.py:exec_kompilex`):
28+
1. Calls `parse_outer()` (Python outer parser)
29+
2. Merges any `--pre-parsed-prelude` modules
30+
3. Serialises the result to a temp JSON file
31+
4. Calls Java `kompile --outer-parsed-json <tempfile>` for the remaining stages
32+
33+
## Stage 2: Inner Parsing (Bubble Resolution)
34+
35+
**What it does**: Parses the rule bodies ("bubbles") using the grammar generated from the user's syntax declarations.
36+
Each bubble is a rule LHS/RHS/requires/ensures that was left as a raw token stream by the outer parser.
37+
38+
**Java implementation**: `k-frontend/src/main/java/org/kframework/parser/inner/` + `RuleGrammarGenerator`.
39+
This stage runs after `--outer-parsed-json` injection, so there is currently no way to skip it from Python.
40+
41+
**Python implementation**: `pyk/src/pyk/kast/parser.py` + `lexer.py`.
42+
The Python inner parser exists but is not yet wired into the pipeline as a bypass.
43+
44+
## Stage 3: Compilation Passes (Java)
45+
46+
32 ordered passes, each a pure `Definition → Definition` transformation.
47+
They are named and can be selected individually via `--kore-backend-steps` in `KoreBackend.java`.
48+
49+
The full ordered list (from `KoreBackend.steps()`, lines 274–306):
50+
51+
| # | Pass name | What it does | External I/O? |
52+
|---|-----------|--------------|---------------|
53+
| 1 | `resolveComm` | Resolve commutative simplification rules | None |
54+
| 2 | `resolveIO` | Resolve I/O stream configuration cells | None |
55+
| 3 | `resolveFun` | Resolve `#fun` applications | None |
56+
| 4 | `resolveFunctionWithConfig` | Resolve function calls that reference the configuration | None |
57+
| 5 | `resolveStrict` | Expand `strict`/`seqstrict` attributes into heating/cooling rules | None |
58+
| 6 | `resolveAnonVars` | Replace `_` anonymous variables with fresh names | None |
59+
| 7 | `resolveContexts` | Resolve context holes and rewrites | None |
60+
| 8 | `numberSentences1` | Assign unique integer IDs to all sentences | None |
61+
| 9 | `resolveHeatCoolAttribute` | Expand `heat`/`cool` attributes into rules | None |
62+
| 10 | `resolveSemanticCasts` | Resolve `#` cast operations | None |
63+
| 11 | `subsortKItem1` | Add subsort productions: every sort is a subsort of `KItem` | None |
64+
| 12 | `constantFolding` | Fold constant expressions (via Java-reflection-based built-in hooks) | None |
65+
| 13 | `propagateMacroToRules` | Propagate `macro` label from production to its rules | None |
66+
| 14 | `guardOrs` | Transform or-patterns into guarded alternatives | None |
67+
| 15 | `resolveFreshConfigConstants` | Resolve `!Var` fresh constants in the configuration | None |
68+
| 16 | `generateSortPredicateSyntax1` | Generate `isSort(...)` predicate productions (pass 1) | None |
69+
| 17 | `generateSortProjections1` | Generate sort projection functions (pass 1) | None |
70+
| 18 | `expandMacros` | Expand macro rules | Optional coverage file write |
71+
| 19 | `addImplicitComputationCell` | Add implicit `<k>` computation cell to rules that lack it | None |
72+
| 20 | `resolveFreshConstants` | Resolve `!Var` fresh constants in rules | None |
73+
| 21 | `generateSortPredicateSyntax2` | Generate sort predicate productions (pass 2) | None |
74+
| 22 | `generateSortProjections2` | Generate sort projections (pass 2) | None |
75+
| 23 | `checkSimplificationRules` | Validate that simplification rule LHS has a function symbol | Error output |
76+
| 24 | `subsortKItem2` | Subsort to `KItem` (pass 2) | None |
77+
| 25 | `concretizeCells` | Concretize cell structure: `AddTopCellToRules` → `AddParentCells` → `CloseCells` → `SortCells` | None |
78+
| 26 | `genCoverage` | Write coverage instrumentation data | Optional file write |
79+
| 27 | `addSemanticsModule` | Add synthetic `LANGUAGE-PARSING` module | None |
80+
| 28 | `resolveConfigVar` | Add configuration variables to rule LHS | None |
81+
| 29 | `addCoolLikeAtt` | Add `cool-like` attribute to rules | None |
82+
| 30 | `removeAnywhereRules` | Filter `anywhere` rules (Haskell backend only) | Warning log |
83+
| 31 | `generateSortPredicateRules` | Generate rules implementing sort predicates | None |
84+
| 32 | `numberSentences2` | Re-number sentences (pass 2) | None |
85+
86+
26 of 32 passes are completely pure (no I/O).
87+
The remaining 6 have conditional or minor I/O that can be trivially gated.
88+
89+
**Output**: Java writes the post-pipeline KAST to `<kompiled-dir>/compiled.json` (and `compiled.txt`).
90+
This is the **second pipeline seam**: Python can read `compiled.json` and take over from here.
91+
92+
## Stage 4: Kore Emission
93+
94+
**What it does**: Converts the compiled KAST (`compiled.json`) into Kore syntax and writes `definition.kore` and `syntaxDefinition.kore`.
95+
96+
**Java implementation**: `k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java`.
97+
Uses `StringBuilder` string concatenation throughout; no intermediate structured Kore AST.
98+
99+
**Python implementation** (partially complete):
100+
101+
- `pyk/src/pyk/konvert/_module_to_kore.py` — `module_to_kore(definition)` generates:
102+
- Sort declarations
103+
- Symbol declarations
104+
- Structural axioms: subsort, assoc, idem, unit, functional, no-confusion, no-junk, overload
105+
- **Not yet**: rule axioms, macro rule separation, `Definition` wrapper, prelude imports, top-cell initializer
106+
107+
- `pyk/src/pyk/konvert/_kast_to_kore.py` — `krule_to_kore(definition, krule)` converts a single K rule to a Kore `Axiom`.
108+
This exists but is not yet called from `module_to_kore()`.
109+
110+
**Gaps to close for full Python Kore emission**:
111+
1. Call `krule_to_kore()` inside `module_to_kore()` to emit rule axioms
112+
2. Separate macro rules into their own section (matching Java's output structure)
113+
3. Add a `kdef_to_kore(definition)` wrapper that produces a `Definition` with prelude modules (BASIC-K, KSEQ, INJ, K) and the top-cell initializer attribute
114+
4. Write the result to `definition.kore` and `syntaxDefinition.kore`
115+
116+
## Stage 5: Backend Compilation
117+
118+
LLVM or Haskell compilation of `definition.kore` into a binary or compiled artifact.
119+
This is inherently backend-specific and will remain in the respective backend tools.
120+
121+
## What pyk Currently Wires Together
122+
123+
| Mechanism | What it does |
124+
|-----------|-------------|
125+
| `pyk kompile` | Thin wrapper — delegates entirely to Java `kompile` |
126+
| `pyk kompilex` | Python outer parse → JSON → Java `kompile --outer-parsed-json` |
127+
| `pyk/regression-new/include/ktest.mak` | Uses `pyk kompile` (not yet `kompilex`) |
128+
129+
## Planned Integration Points
130+
131+
1. **Outer parsing**: switch `pyk/regression-new/include/ktest.mak` from `pyk kompile` to `pyk kompilex` so all regression tests exercise Python outer parsing.
132+
133+
2. **Kore emission**: extend `_module_to_kore.py` with rule emission, add `kdef_to_kore()` wrapper, add a validation tool (`pyk emit-kore`) that reads `compiled.json` and diffs against `definition.kore`, then wire into `kompilex`.
134+
135+
3. **Compilation passes**: once outer parsing and Kore emission are in Python, individual passes can be ported one at a time, replacing Java sub-steps without changing the overall pipeline interface.
136+
137+
## Key Files
138+
139+
| Path | Role |
140+
|------|------|
141+
| `k-frontend/src/main/javacc/Outer.jj` | Java outer parser grammar |
142+
| `k-frontend/src/main/java/org/kframework/kompile/KompileOptions.java` | `--outer-parsed-json` flag |
143+
| `k-frontend/src/main/java/org/kframework/kompile/DefinitionParsing.java:305` | Outer parsing bypass entry point |
144+
| `k-frontend/src/main/java/org/kframework/backend/kore/KoreBackend.java:122` | `steps()` — ordered pass list |
145+
| `k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java` | Java Kore emission |
146+
| `pyk/src/pyk/kast/outer_parser.py` | Python outer parser |
147+
| `pyk/src/pyk/kast/utils.py` | `parse_outer()` — outer parse entry point |
148+
| `pyk/src/pyk/__main__.py:exec_kompilex` | `kompilex` pipeline driver |
149+
| `pyk/src/pyk/ktool/kompile.py` | `kompile()` — Java subprocess wrapper |
150+
| `pyk/src/pyk/konvert/_module_to_kore.py` | `module_to_kore()` — partial Kore emission |
151+
| `pyk/src/pyk/konvert/_kast_to_kore.py` | `krule_to_kore()` — rule → Kore axiom |
152+
| `pyk/src/pyk/kore/syntax.py` | Kore AST types |
153+
| `pyk/regression-new/include/ktest.mak` | Regression test kompile invocation |
154+
| `pyk/regression-new/skipped` | 113 currently skipped tests |

0 commit comments

Comments
 (0)