diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000000..96d7ba79cb0 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,135 @@ +copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved. + +# K Framework — Agent Guide + +## Project Overview + +The K Framework is a language-agnostic formal specification and verification framework developed by Runtime Verification. +It lets you define programming language semantics in `.k` files and then automatically derives an interpreter, model checker, and deductive verifier from that definition. + +The repository is a monorepo with two independent technology stacks: + +- **Java/Scala** — the K compiler toolchain (`kompile`, `krun`, `kprove`, etc.) +- **Python** (`pyk/`) — the `kframework` Python SDK for programmatically interacting with the K toolchain + +## Repository Structure + +``` +k-frontend/ K language parser and frontend (Java/Scala) +k-distribution/ Main distribution bundle + bin/, lib/ Symlinks into target/release/k/ + include/kframework/ Shared Makefile infrastructure (ktest.mak, ktest-group.mak) + tests/regression-new/ Java-backend regression suite (229 test subdirs) +haskell-backend/ Haskell-based symbolic backend +llvm-backend/ LLVM-based concrete execution backend +pyk/ Python SDK sub-project (self-contained) + src/pyk/ Package source (cli, kast, kore, proof, kcfg, kdist, …) + src/tests/ pytest test suite (unit/, integration/) + regression-new/ Python-backend regression suite (213 test subdirs) + pyproject.toml Build & tool config (hatchling, black, mypy, flake8, …) + Makefile All pyk make targets +k-tutorial/ Tutorial K definitions +``` + +## Build + +### Java (compile only, skip tests) + +``` +mvn package -DskipTests +``` + +This compiles all Maven modules (`k-frontend`, `k-distribution`, `haskell-backend`, `llvm-backend`) and produces JARs under each module's `target/` directory. +Java 17 and Scala 2.13 are required. + +### Python + +The `pyk/` sub-project uses `hatchling` as its build backend and `uv` as its package manager. +No explicit build step is needed before running lint or tests — the make targets handle installation. + +## Lint + +### Java + +``` +mvn spotless:apply +``` + +This auto-formats all Java/Scala sources (Google Java Format + Scalafmt). +Run it after every Java change; commits must pass `mvn spotless:check`. + +### Python + +``` +make -C pyk check +``` + +This runs, in order: `black --check`, `isort --check`, `autoflake --check`, `flake8`, `mypy`, `pydocstyle`. + +To auto-apply all formatters: + +``` +make -C pyk format +``` + +Key style settings (from `pyk/pyproject.toml`): +- `black`: line-length 120, skip-string-normalization +- `isort`: black profile, line-length 120 +- `mypy`: `disallow_untyped_defs = true` +- `pydocstyle`: Google convention + +## Tests + +There are four distinct test surfaces. + +### 1. Java unit tests + +``` +mvn verify +``` + +Runs all JUnit 4 tests across `k-frontend` and `k-distribution` via Maven Surefire. +Tests run with `LC_NUMERIC=en_US.UTF-8`. + +### 2. Python unit + integration tests + +``` +make -C pyk test +``` + +Runs `src/tests/unit/` and `src/tests/integration/` with 4 parallel workers (pytest-xdist, worksteal). +Unit tests only (faster, no K toolchain required): + +``` +make -C pyk test-unit +``` + +### 3. Java regression tests + +``` +make -C k-distribution/tests/regression-new +``` + +229 subdirectory test cases. +Each test compiles a `.k` definition with `kompile` and executes it with `krun` or `kprove`, comparing output against `.out` baseline files. +The shared test infrastructure lives in `k-distribution/include/kframework/ktest.mak`. + +### 4. Python regression tests + +``` +make -C pyk/regression-new +``` + +213 subdirectory test cases; 113 are currently skipped (listed in `pyk/regression-new/skipped`). +Same test infrastructure as the Java regression suite but exercises pyk-specific code paths. + +## Updating Regression Baselines + +If a change intentionally alters K program output, regenerate the `.out` files: + +``` +make -C k-distribution/tests/regression-new update-results +make -C pyk/regression-new update-results +``` + +Commit the updated baseline files in a dedicated commit after the logic change. diff --git a/pyk/docs/pipeline.md b/pyk/docs/pipeline.md new file mode 100644 index 00000000000..825b177f371 --- /dev/null +++ b/pyk/docs/pipeline.md @@ -0,0 +1,154 @@ +# K Compilation Pipeline — Developer Reference + +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. + +## Overview + +The pipeline has five logical stages: + +``` +Outer parsing → Inner parsing → 32 compilation passes → Kore emission → Backend compilation +``` + +The first four stages produce `definition.kore`. +The fifth stage (LLVM/Haskell backend compilation) consumes `definition.kore` and is inherently backend-specific. + +## Stage 1: Outer Parsing + +**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"). + +**Java implementation**: JavaCC grammar at `k-frontend/src/main/javacc/Outer.jj`; entry point `DefinitionParsing.parseDefinition()`. + +**Python implementation**: `pyk/src/pyk/kast/outer_parser.py` + `outer_lexer.py`; entry point `pyk.kast.utils.parse_outer()`. + +**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. +The JSON format is `{"format": "KAST", "version": 3, "term": }`. + +**`kompilex` command** (`pyk/src/pyk/__main__.py:exec_kompilex`): +1. Calls `parse_outer()` (Python outer parser) +2. Merges any `--pre-parsed-prelude` modules +3. Serialises the result to a temp JSON file +4. Calls Java `kompile --outer-parsed-json ` for the remaining stages + +## Stage 2: Inner Parsing (Bubble Resolution) + +**What it does**: Parses the rule bodies ("bubbles") using the grammar generated from the user's syntax declarations. +Each bubble is a rule LHS/RHS/requires/ensures that was left as a raw token stream by the outer parser. + +**Java implementation**: `k-frontend/src/main/java/org/kframework/parser/inner/` + `RuleGrammarGenerator`. +This stage runs after `--outer-parsed-json` injection, so there is currently no way to skip it from Python. + +**Python implementation**: `pyk/src/pyk/kast/parser.py` + `lexer.py`. +The Python inner parser exists but is not yet wired into the pipeline as a bypass. + +## Stage 3: Compilation Passes (Java) + +32 ordered passes, each a pure `Definition → Definition` transformation. +They are named and can be selected individually via `--kore-backend-steps` in `KoreBackend.java`. + +The full ordered list (from `KoreBackend.steps()`, lines 274–306): + +| # | Pass name | What it does | External I/O? | +|---|-----------|--------------|---------------| +| 1 | `resolveComm` | Resolve commutative simplification rules | None | +| 2 | `resolveIO` | Resolve I/O stream configuration cells | None | +| 3 | `resolveFun` | Resolve `#fun` applications | None | +| 4 | `resolveFunctionWithConfig` | Resolve function calls that reference the configuration | None | +| 5 | `resolveStrict` | Expand `strict`/`seqstrict` attributes into heating/cooling rules | None | +| 6 | `resolveAnonVars` | Replace `_` anonymous variables with fresh names | None | +| 7 | `resolveContexts` | Resolve context holes and rewrites | None | +| 8 | `numberSentences1` | Assign unique integer IDs to all sentences | None | +| 9 | `resolveHeatCoolAttribute` | Expand `heat`/`cool` attributes into rules | None | +| 10 | `resolveSemanticCasts` | Resolve `#` cast operations | None | +| 11 | `subsortKItem1` | Add subsort productions: every sort is a subsort of `KItem` | None | +| 12 | `constantFolding` | Fold constant expressions (via Java-reflection-based built-in hooks) | None | +| 13 | `propagateMacroToRules` | Propagate `macro` label from production to its rules | None | +| 14 | `guardOrs` | Transform or-patterns into guarded alternatives | None | +| 15 | `resolveFreshConfigConstants` | Resolve `!Var` fresh constants in the configuration | None | +| 16 | `generateSortPredicateSyntax1` | Generate `isSort(...)` predicate productions (pass 1) | None | +| 17 | `generateSortProjections1` | Generate sort projection functions (pass 1) | None | +| 18 | `expandMacros` | Expand macro rules | Optional coverage file write | +| 19 | `addImplicitComputationCell` | Add implicit `` computation cell to rules that lack it | None | +| 20 | `resolveFreshConstants` | Resolve `!Var` fresh constants in rules | None | +| 21 | `generateSortPredicateSyntax2` | Generate sort predicate productions (pass 2) | None | +| 22 | `generateSortProjections2` | Generate sort projections (pass 2) | None | +| 23 | `checkSimplificationRules` | Validate that simplification rule LHS has a function symbol | Error output | +| 24 | `subsortKItem2` | Subsort to `KItem` (pass 2) | None | +| 25 | `concretizeCells` | Concretize cell structure: `AddTopCellToRules` → `AddParentCells` → `CloseCells` → `SortCells` | None | +| 26 | `genCoverage` | Write coverage instrumentation data | Optional file write | +| 27 | `addSemanticsModule` | Add synthetic `LANGUAGE-PARSING` module | None | +| 28 | `resolveConfigVar` | Add configuration variables to rule LHS | None | +| 29 | `addCoolLikeAtt` | Add `cool-like` attribute to rules | None | +| 30 | `removeAnywhereRules` | Filter `anywhere` rules (Haskell backend only) | Warning log | +| 31 | `generateSortPredicateRules` | Generate rules implementing sort predicates | None | +| 32 | `numberSentences2` | Re-number sentences (pass 2) | None | + +26 of 32 passes are completely pure (no I/O). +The remaining 6 have conditional or minor I/O that can be trivially gated. + +**Output**: Java writes the post-pipeline KAST to `/compiled.json` (and `compiled.txt`). +This is the **second pipeline seam**: Python can read `compiled.json` and take over from here. + +## Stage 4: Kore Emission + +**What it does**: Converts the compiled KAST (`compiled.json`) into Kore syntax and writes `definition.kore` and `syntaxDefinition.kore`. + +**Java implementation**: `k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java`. +Uses `StringBuilder` string concatenation throughout; no intermediate structured Kore AST. + +**Python implementation** (partially complete): + +- `pyk/src/pyk/konvert/_module_to_kore.py` — `module_to_kore(definition)` generates: + - Sort declarations + - Symbol declarations + - Structural axioms: subsort, assoc, idem, unit, functional, no-confusion, no-junk, overload + - **Not yet**: rule axioms, macro rule separation, `Definition` wrapper, prelude imports, top-cell initializer + +- `pyk/src/pyk/konvert/_kast_to_kore.py` — `krule_to_kore(definition, krule)` converts a single K rule to a Kore `Axiom`. + This exists but is not yet called from `module_to_kore()`. + +**Gaps to close for full Python Kore emission**: +1. Call `krule_to_kore()` inside `module_to_kore()` to emit rule axioms +2. Separate macro rules into their own section (matching Java's output structure) +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 +4. Write the result to `definition.kore` and `syntaxDefinition.kore` + +## Stage 5: Backend Compilation + +LLVM or Haskell compilation of `definition.kore` into a binary or compiled artifact. +This is inherently backend-specific and will remain in the respective backend tools. + +## What pyk Currently Wires Together + +| Mechanism | What it does | +|-----------|-------------| +| `pyk kompile` | Thin wrapper — delegates entirely to Java `kompile` | +| `pyk kompilex` | Python outer parse → JSON → Java `kompile --outer-parsed-json` | +| `pyk/regression-new/include/ktest.mak` | Uses `pyk kompile` (not yet `kompilex`) | + +## Planned Integration Points + +1. **Outer parsing**: switch `pyk/regression-new/include/ktest.mak` from `pyk kompile` to `pyk kompilex` so all regression tests exercise Python outer parsing. + +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`. + +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. + +## Key Files + +| Path | Role | +|------|------| +| `k-frontend/src/main/javacc/Outer.jj` | Java outer parser grammar | +| `k-frontend/src/main/java/org/kframework/kompile/KompileOptions.java` | `--outer-parsed-json` flag | +| `k-frontend/src/main/java/org/kframework/kompile/DefinitionParsing.java:305` | Outer parsing bypass entry point | +| `k-frontend/src/main/java/org/kframework/backend/kore/KoreBackend.java:122` | `steps()` — ordered pass list | +| `k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java` | Java Kore emission | +| `pyk/src/pyk/kast/outer_parser.py` | Python outer parser | +| `pyk/src/pyk/kast/utils.py` | `parse_outer()` — outer parse entry point | +| `pyk/src/pyk/__main__.py:exec_kompilex` | `kompilex` pipeline driver | +| `pyk/src/pyk/ktool/kompile.py` | `kompile()` — Java subprocess wrapper | +| `pyk/src/pyk/konvert/_module_to_kore.py` | `module_to_kore()` — partial Kore emission | +| `pyk/src/pyk/konvert/_kast_to_kore.py` | `krule_to_kore()` — rule → Kore axiom | +| `pyk/src/pyk/kore/syntax.py` | Kore AST types | +| `pyk/regression-new/include/ktest.mak` | Regression test kompile invocation | +| `pyk/regression-new/skipped` | 113 currently skipped tests | diff --git a/pyk/docs/regression-triage.md b/pyk/docs/regression-triage.md new file mode 100644 index 00000000000..bb5e5d4cc87 --- /dev/null +++ b/pyk/docs/regression-triage.md @@ -0,0 +1,166 @@ +# pyk/regression-new — Skipped Test Triage + +This document categorises the 113 skipped tests in `pyk/regression-new/skipped` by root cause, +lists the tests in each category, and identifies quick-win opportunities. + +## Category A — Haskell backend (≈39 tests) + +These tests set `KOMPILE_BACKEND=haskell`. +They require the Haskell symbolic execution backend which is not the primary focus of the pyk test suite. + +``` +cell-sort-haskell, checkClaimError, concrete-function, concrete-function-cache, +concrete-haskell, context-alias-2, context-labels, domains-lemmas-no-smt, +imp-haskell, issue-1175, issue-1436, issue-1489-claimLoc, issue-1676-koreBytes, +issue-1682-korePrettyPrint, issue-1683-cfgVarsWarns, issue-2142-markConcrete, +issue-2174-kprovexParseError, issue-2287-simpl-rules-in-kprovex, +issue-2321-kprovexCrash, issue-2356-koreDecode, ite-bug, kast-kore-input, +kprove-append, kprove-branchingAllowed, kprove-error-status, kprove-java, +kprove-markdown, kprove-var-equals, map-symbolic-tests-haskell, markdownSelectors, +or-haskell, poly-sort, poly-unparsing, profile, quadratic-poly-unparsing, +set-symbolic-tests, set_unification, spec-rule-application, unification-lemmas +``` + +Not addressable without Haskell backend support. + +## Category B — GLR / Bison parser generation (≈16 tests) + +These tests pass `--gen-glr-bison-parser` or `--gen-bison-parser` to `kompile`. +They require C compilation and bison integration that is not available in pyk. + +``` +bison-parser-library, glr, glr2, glr3, glr4, imp++-llvm, issue-1602, +kast-bison, kast-bison-bytes, llvm-krun, locations, locations2, locations3, +parse-c, parseNonPgm, proof-instrumentation +``` + +Not addressable without bison integration. + +## Category C — kore backend (4 tests) + +These tests use `KOMPILE_BACKEND=kore` (the bytecode interpreter backend). + +``` +fresh1, fresh2, imp-kore, kore-brackets +``` + +Not addressable without kore backend support. + +## Category D — `pyk parse` subcommand missing (≈10 tests) + +The `ktest.mak` infrastructure sets `KAST=$(UV_RUN) pyk parse`, but `pyk parse` is not a +valid subcommand in the current pyk CLI (valid commands: print, rpc-print, rpc-kast, +prove-legacy, kompile, kompilex, run, prove, show, graph-imports, coverage, +kore-to-json, json-to-kore, parse-outer). + +These tests exercise the KAST parsing / pretty-printing pipeline. + +``` +equals-formatting, issue-2273, issue-3647-debugTokens, issue-3672-debugParse, +json-input, kast-default-output, kast-input, kast-rule +``` + +Also: `issue-1088` (uses `KAST_FLAGS=--output kast --output-file`). + +**Fix**: Add a `pyk parse` (or `pyk kast`) CLI subcommand that wraps the Java `kast` binary +(similar to how `pyk kompile` wraps `kompile`), or wire pyk's inner-parsing infrastructure +into a CLI command. + +## Category E — Missing `pyk run` flags + +`pyk run` (`exec_run` in `__main__.py`) is a thin wrapper that only accepts `pgm_file` and +`--definition`. +Several tests require flags that pass-through to the underlying Java `krun`: + +- `-cVAR=VALUE` (cell configuration override): `doubleinj` +- `--output program`: `issue-1145` +- `--parser