TypedPython step 1: soundness gate

docs/INTENT.md

@@ -26,6 +26,23 @@ CPython interpreter inside a Kotlin Multiplatform application so that:
    written (`Greeter('Kotlin').greet(2)` in `sample/`).
 3. **The same code runs on every target** a Kotlin Multiplatform app ships to: desktop JVM, Android,
    iOS, Android native, and the web (wasm, experimental).
+4. **The project's own Python is statically typed by default** (TypedPython). The maintainer's goal:
+
+   > "파이썬을 컴파일 언어 및 타입 안정화, 정적 타입 검사, 컴파일 타임 타입검사를 지원할 수 있도록"
+   > — *Support Python as a compiled language with type stability, static type checking and
+   > compile-time type checking*, so that Python stays usable as AI-friendly languages such as Rust
+   > and TypeScript gain ground.
+
+   > "TypedPython을 별도 레포가 아니라 PythonMultiplatform의 기본 동작이 될거야"
+   > — *TypedPython is not a separate repository; it will be PythonMultiplatform's default behaviour.*
+
+   The maintainer chose the scope "검사만 기본, 컴파일은 opt-in" (2026-10-02): every user Python source
+   is **checked** by default; **compiling** it to native code is opt-in. The compiled code still runs on
+   the embedded CPython, as an extension module (`docs/design/typedpython.md`).
+
+   > The maintainer also asked to *explore* GPU kernels written in Python without a separate language
+   > ("GPU 관련 최적화까지도 별도 언어 없이 지원할 방안을 모색해보자"). That is an exploration, not yet
+   > a commitment; it is recorded in the design note only.
 
 The CPython version moved on from 3.13 (the build pins 3.14.x today and offers opt-in free-threaded 3.14t builds
 on desktop only); the intent — embed **CPython itself**, not a re-implementation — is unchanged.
@@ -88,7 +105,7 @@ no per-platform Python → Kotlin binding code to maintain.
 | A replacement for the `pythonx` packages | §2.3 — they are real packages in their own repository |
 | Runtime-reflection or name-lookup based binding | §2.1 — impossible under Kotlin/Native and native image |
 | A hand-written wrapper per Kotlin function or class | Generic adaptation plus generated tables; per-declaration wrappers were tried in 2024 and rotted (`docs/design/pythonx-adapter-design.md`) |
-| A Python re-implementation, transpiler, or JVM-hosted Python | It embeds CPython itself, so C extensions keep working |
+| A Python re-implementation, transpiler, or JVM-hosted Python | It embeds CPython itself, so C extensions keep working. TypedPython (§1.4) does not change this: checked code is ordinary Python, and compiled code is a CPython extension module, not a translation to another runtime |
 | A build tool, dependency resolver or packager | That is pypackpack (the work) and toolchain (the Gradle vocabulary) |
 | A sub-interpreter parallelism model | Rejected: extensions that do not declare multi-interpreter support fail to import; parallelism comes from free-threaded CPython |
 | A vendored interpreter | The build downloads and verifies CPython per platform |

docs/SPEC.md

@@ -239,6 +239,17 @@ All in `PM/commonTest`, so they run wherever the interpreter loads.
 - **N-3** Binding Kotlin/Native klib declarations at run time (B-2). `Status: planned`.
 - **N-4** Linux and Windows desktop runs in CI (P-2). `Status: planned`.
 - **N-5** Native-image upcall verification as an automated test (U-6). `Status: planned`.
+- **N-6** TypedPython soundness gate (INTENT §1.4; `docs/design/typedpython.md` §4.2): checking a set of
+  user Python files reports every Pyrefly type error, the Any-leak kinds (`implicit-any-parameter`,
+  `unannotated-return`, `unknown-variable-type`, `no-any-return-implicit`, `no-any-return-explicit`,
+  `explicit-any`) and any user-code expression of type `Any` outside `cast()` (`any-flow`) as errors;
+  the forbidden list (`eval`/`exec`, computed-name `getattr`/`setattr`/`delattr`, patching an imported
+  module or a module-level class) as warnings in `checked` mode and errors in `compiled` mode. Nothing
+  inside dependencies is reported. `python -m typedpython check` exits 0 / 1 / 2 for clean / errors /
+  tool failure. `Status: partial` — the gate is asserted by
+  `python-multiplatform-ksp/src/test/python/` (run with that module's `.venv`); it is **not yet run by the
+  build** (design §6 step 1b), and rebinding a variable to a different type and mixed-element containers
+  are not detected (Pyrefly 1.3.2 reports neither).
 
 ---
 

docs/design/typedpython.md

@@ -207,6 +207,23 @@ TypedPython 은 그래서 자체 텐서 런타임을 만들지 않고 **torch op
 각 단계는 AGENTS.md §5·§14 의 TDD 와 측정 테스트 규정을 따른다. 특히 3 은 경계 비용 감소를, 4 는
 upstream 대비 수치 오차를 기준선으로 박아 둔다.
 
+### 6.1 단계 1 의 현재 상태 (2026-10-03, #16)
+
+- **위치:** `python-multiplatform-ksp/src/main/python/typedpython/`, 테스트는
+  `python-multiplatform-ksp/src/test/python/`. 사용자 지시("ksp랑 통합")에 따라 KSP 모듈 안에 둔다.
+  KSP 프로세서는 Kotlin 심볼만 보고 파이썬 파일 변경으로는 다시 돌지 않으므로, **실행**은 1b 에서
+  Gradle 태스크가 맡는다 — KSP 모듈은 소스와 배포(jar 리소스)의 자리다.
+- **구현된 규칙:** SPEC N-6. Pyrefly 의 `Any` 유출 kind 6개를 에러로 올리고, Pyrefly 의
+  per-expression 타입 리포트(`--report-pysa`)로 사용자 코드 안의 `Any` 식을 찾는다(`any-flow`).
+  `cast()` 인자, 버려지는 식 문장의 값, 함수 시그니처 자체는 제외한다.
+- **미구현:** 타입이 다른 값으로의 재할당, 원소 타입이 섞인 컨테이너. Pyrefly 1.3.2 는 둘 다
+  보고하지 않고, 타입 리포트에 대입 대상의 타입이 없다.
+- **측정:** 1800줄 합성 모듈에서 plain `pyrefly check` 160–235 ms, 게이트 1.3–1.9 s — 두 번 잰 비율이
+  모두 약 8배다. 단독 측정이 아니다(두 번째는 load average 18.6). 절대값보다 비율을 기준으로 본다. 차이의
+  대부분은 타입 리포트가 typeshed 사본까지 디스크에 쓰는 비용으로 보인다(추정, 미분해). 1b 에서
+  빌드마다 돌리기 전에 줄일 대상이다.
+- **고정:** Pyrefly `==1.3.2`. 타입 리포트는 Pyrefly 가 버전을 매기는 포맷이지 공개 API 가 아니다.
+
 ## 7. 위험
 
 - **Pyrefly 의 외부 API 안정성.** 라이브러리 임베드는 확인 전까지 미룬다 (§4.1).

python-multiplatform-ksp/.gitignore

@@ -0,0 +1,5 @@
+.venv/
+__pycache__/
+.pytest_cache/
+*.egg-info/
+.pytest_tmp/

python-multiplatform-ksp/pyproject.toml

@@ -0,0 +1,29 @@
+# TypedPython soundness gate (docs/design/typedpython.md §4.2).
+# The Kotlin processor in this module is built by Gradle; this file only describes the Python
+# package that lives next to it in src/main/python.
+[project]
+name = "typedpython"
+version = "0.1.0"
+requires-python = ">=3.13"
+# Pinned exactly: the gate reads Pyrefly's per-expression type report (--report-pysa), whose
+# format is versioned by Pyrefly, not by a public API.
+dependencies = ["pyrefly==1.3.2"]
+
+[project.scripts]
+typedpython = "typedpython.__main__:cli"
+
+[build-system]
+requires = ["hatchling"]
+build-backend = "hatchling.build"
+
+[tool.hatch.build.targets.wheel]
+packages = ["src/main/python/typedpython"]
+
+[project.optional-dependencies]
+test = ["pytest"]
+
+[tool.pytest.ini_options]
+testpaths = ["src/test/python"]
+pythonpath = ["src/main/python"]
+addopts = "--basetemp=.pytest_tmp"
+markers = ["measurement: records cost; asserts only sanity bounds"]

python-multiplatform-ksp/src/main/python/typedpython/__init__.py

@@ -0,0 +1,4 @@
+"""TypedPython — static checking for the Python code of a PythonMultiplatform project.
+
+See docs/design/typedpython.md. This package is the soundness gate (§4.2).
+"""

python-multiplatform-ksp/src/main/python/typedpython/__main__.py

@@ -0,0 +1,49 @@
+"""`python -m typedpython check [--mode checked|compiled] [--format text|json] PATHS...`
+
+Exit status: 0 no errors (warnings allowed), 1 errors, 2 the gate itself could not run.
+"""
+import argparse
+import json
+import sys
+from pathlib import Path
+
+from typedpython import gate
+from typedpython.paths import python_files
+from typedpython.pyrefly import PyreflyError
+
+EXIT_CLEAN, EXIT_ERRORS, EXIT_FAILURE = 0, 1, 2
+
+
+def main(argv: list[str]) -> int:
+    parser = argparse.ArgumentParser(prog="typedpython")
+    commands = parser.add_subparsers(dest="command", required=True)
+    check = commands.add_parser("check", help="type-check user Python code")
+    check.add_argument("paths", nargs="+", type=Path, help="files, or directories to check recursively")
+    check.add_argument("--mode", choices=["checked", "compiled"], default="checked")
+    check.add_argument("--format", choices=["text", "json"], default="text")
+    check.add_argument("--search-path", action="append", type=Path, default=[],
+                       help="directory to resolve imports from (repeatable)")
+    args = parser.parse_args(argv)
+
+    try:
+        found = gate.check(python_files(args.paths), mode=args.mode, search_paths=args.search_path)
+    except PyreflyError as e:
+        print(f"typedpython: {e}", file=sys.stderr)
+        return EXIT_FAILURE
+
+    if args.format == "json":
+        print(json.dumps([d.to_json() for d in found], indent=2))
+    else:
+        for d in found:
+            print(f"{d.severity.upper()} {d.path}:{d.line}:{d.column}: {d.message} [{d.rule}]")
+
+    return EXIT_ERRORS if any(d.severity == "error" for d in found) else EXIT_CLEAN
+
+
+def cli() -> None:
+    """Console-script entry point (`typedpython check ...`)."""
+    sys.exit(main(sys.argv[1:]))
+
+
+if __name__ == "__main__":
+    cli()

python-multiplatform-ksp/src/main/python/typedpython/diagnostic.py

@@ -0,0 +1,17 @@
+from dataclasses import dataclass, asdict
+from typing import Literal
+
+Severity = Literal["error", "warning"]
+
+
+@dataclass(frozen=True, order=True)
+class Diagnostic:
+    path: str
+    line: int
+    column: int
+    rule: str
+    severity: Severity
+    message: str
+
+    def to_json(self) -> dict[str, object]:
+        return asdict(self)

python-multiplatform-ksp/src/main/python/typedpython/forbidden.py

@@ -0,0 +1,110 @@
+"""The forbidden list (docs/design/typedpython.md §3.1), found by walking the AST.
+
+These are the dynamic features that make a static type unreliable at compile time. The gate
+reports them as warnings for `checked` code and as errors for `compiled` code; this module only
+finds them.
+
+Not covered here: rebinding a variable to a different type and containers that mix element
+types. Both need inferred types for assignment targets, which Pyrefly 1.3.2 does not report.
+"""
+import ast
+from dataclasses import dataclass
+
+DYNAMIC_ATTRIBUTE_CALLS = {"getattr", "setattr", "delattr"}
+# Index of the attribute-name argument in each of the calls above.
+NAME_ARGUMENT = 1
+
+
+@dataclass(frozen=True)
+class Finding:
+    rule: str
+    line: int
+    column: int
+    message: str
+
+
+def scan(source: str, path: str) -> list[Finding]:
+    tree = ast.parse(source, filename=path)
+    patchable = _module_level_modules_and_classes(tree)
+    findings: list[Finding] = []
+
+    for node in ast.walk(tree):
+        if isinstance(node, ast.Call) and isinstance(node.func, ast.Name):
+            findings += _check_call(node, node.func.id, patchable)
+        elif isinstance(node, (ast.Assign, ast.AugAssign, ast.AnnAssign, ast.Delete)):
+            for target in _targets(node):
+                if _is_patch_target(target, patchable):
+                    assert isinstance(target, ast.Attribute) and isinstance(target.value, ast.Name)
+                    findings.append(_finding(
+                        "forbidden/monkeypatch", target,
+                        f"`{target.value.id}.{target.attr}` changes a module or class from outside it",
+                    ))
+
+    return sorted(findings, key=lambda f: (f.line, f.column, f.rule))
+
+
+def _check_call(call: ast.Call, name: str, patchable: set[str]) -> list[Finding]:
+    if name in ("eval", "exec"):
+        return [_finding(f"forbidden/{name}", call, f"`{name}` runs code the checker cannot see")]
+    if name not in DYNAMIC_ATTRIBUTE_CALLS or len(call.args) <= NAME_ARGUMENT:
+        return []
+
+    attribute = call.args[NAME_ARGUMENT]
+    if not (isinstance(attribute, ast.Constant) and isinstance(attribute.value, str)):
+        return [_finding(
+            "forbidden/dynamic-attr", call,
+            f"`{name}` with a computed attribute name hides the attribute from the checker",
+        )]
+
+    # A literal name is static, but setattr/delattr on a module or class is still a patch.
+    receiver = call.args[0]
+    if name != "getattr" and isinstance(receiver, ast.Name) and receiver.id in patchable:
+        return [_finding(
+            "forbidden/monkeypatch", call,
+            f"`{name}` on `{receiver.id}` changes a module or class from outside it",
+        )]
+    return []
+
+
+def _module_level_modules_and_classes(tree: ast.Module) -> set[str]:
+    """Names bound at module scope to an imported module/name or to a class definition."""
+    names: set[str] = set()
+    for node in tree.body:
+        if isinstance(node, ast.Import):
+            names |= {(alias.asname or alias.name).split(".")[0] for alias in node.names}
+        elif isinstance(node, ast.ImportFrom):
+            names |= {alias.asname or alias.name for alias in node.names if alias.name != "*"}
+        elif isinstance(node, ast.ClassDef):
+            names.add(node.name)
+    return names
+
+
+def _targets(node: ast.stmt) -> list[ast.expr]:
+    if isinstance(node, ast.Assign):
+        return [t for target in node.targets for t in _flatten(target)]
+    if isinstance(node, ast.Delete):
+        return [t for target in node.targets for t in _flatten(target)]
+    if isinstance(node, (ast.AugAssign, ast.AnnAssign)):
+        return [node.target]
+    return []
+
+
+def _flatten(target: ast.expr) -> list[ast.expr]:
+    if isinstance(target, (ast.Tuple, ast.List)):
+        return [t for element in target.elts for t in _flatten(element)]
+    if isinstance(target, ast.Starred):
+        return _flatten(target.value)
+    return [target]
+
+
+def _is_patch_target(target: ast.expr, patchable: set[str]) -> bool:
+    return (
+        isinstance(target, ast.Attribute)
+        and isinstance(target.value, ast.Name)
+        and target.value.id in patchable
+    )
+
+
+def _finding(rule: str, node: ast.expr, message: str) -> Finding:
+    # ast columns are 0-based; Pyrefly's (and every editor's) are 1-based.
+    return Finding(rule, node.lineno, node.col_offset + 1, message)