TypedPython stage 2: typed IR → C back end, end to end on desktop

.github/workflows/typedpython.yml

@@ -0,0 +1,77 @@
+name: TypedPython CI
+
+# The TypedPython gate and compiler are Python (python-multiplatform-ksp/src/{main,test}/python).
+# Gradle does not run them; this workflow does.
+on:
+  push:
+    branches: [ "develop", "main" ]
+    paths: [ "python-multiplatform-ksp/**", ".github/workflows/typedpython.yml" ]
+  pull_request:
+    branches: [ "develop", "main" ]
+    paths: [ "python-multiplatform-ksp/**", ".github/workflows/typedpython.yml" ]
+
+jobs:
+  test:
+    name: TypedPython tests (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+    defaults:
+      run:
+        working-directory: python-multiplatform-ksp
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: astral-sh/setup-uv@v5
+
+      - name: Create the environment
+        # pyrefly is pinned exactly: the gate reads its versioned type-report format.
+        run: |
+          uv venv .venv --python 3.13
+          uv pip install --python .venv/bin/python "pyrefly==1.3.2" pytest
+
+      - name: Behaviour tests
+        run: .venv/bin/python -m pytest -q -m "not measurement"
+
+      - name: Measurements (recorded, sanity bounds only)
+        # A shared runner is not an idle machine (AGENTS.md §8): read ratios, not absolute times.
+        run: .venv/bin/python -m pytest -q -s -m measurement
+
+  sanitizers:
+    # SPEC N-8: ASan/UBSan runs are the safety net outside the proof. Every extension TypedPython
+    # builds in these tests is compiled with -fsanitize=address,undefined (TP_SANITIZE=1, see
+    # conftest.py) and the interpreter runs with the ASan runtime preloaded; any report fails the run.
+    # Linux only: macOS refuses to load the ASan runtime into the framework Python (the cgen
+    # sanitizer test has a launcher-based macOS path of its own).
+    name: TypedPython tests under ASan + UBSan (ubuntu-latest)
+    runs-on: ubuntu-latest
+    defaults:
+      run:
+        working-directory: python-multiplatform-ksp
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: astral-sh/setup-uv@v5
+
+      - name: Create the environment
+        run: |
+          uv venv .venv --python 3.13
+          uv pip install --python .venv/bin/python "pyrefly==1.3.2" pytest
+
+      - name: Relax ASLR entropy (ASan shadow mapping on newer kernels)
+        run: sudo sysctl -w vm.mmap_rnd_bits=28 || true
+
+      - name: Self-check, the sanitizers must catch planted faults
+        # Builds a deliberately faulty extension (heap out-of-bounds read, signed overflow) and
+        # REQUIRES both reports. If this step passes, the setup below can detect faults.
+        run: .venv/bin/python tools/sanitizers.py selfcheck
+
+      - name: cgen, runtime and pipeline tests, sanitized
+        # detect_leaks=0: CPython itself leaks at exit. LD_PRELOAD is applied to this one command
+        # only (tools/sanitizers.py env prints it); the gate's pyrefly runs without it.
+        run: |
+          env $(.venv/bin/python tools/sanitizers.py env) \
+            .venv/bin/python -m pytest -q -m "not measurement" \
+              src/test/python/test_cgen.py src/test/python/test_runtime.py src/test/python/test_pipeline.py

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/archive/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

@@ -317,6 +317,50 @@ All in `PM/commonTest`, so they run wherever the interpreter loads.
   `androidx.compose.runtime.mutableStateOf(x)` callable, and `.value` of the returned `MutableState`
   readable and writable on its proxy. Implemented by #38 (B-1, U-10); B-8's test now writes its root
   through `state.value = root` and the KSP-bound stand-in is gone. `Status: implemented`.
+- **N-7** 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, rebinding an unannotated name to a different type, and a list/set/dict
+  display whose inferred element type is a union) 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). Rebinding and mixed containers are found by a second Pyrefly pass over a
+  probed copy (design §6.1), which runs only when a file has a name assigned twice or a container
+  display; `for` targets and comprehension variables are not probed.
+- **N-8** TypedPython compilation to C (INTENT §1.4; design §4.3; #41). `@compiled` (a builtin name, no
+  import — #42) and a first-line `# typedpython: compiled` mark functions; the compiler lowers them
+  through the typed IR (`typedpython/ir.py`) to C against the CPython C API and builds an extension with
+  the platform C compiler. Compiled functions return what CPython returns (IR contract: checked i64
+  with deopt to the interpreted function, Python floor division/modulo, exact int/float comparison,
+  CPython's exception types and messages; tracebacks are the one accepted difference). `Status: planned`.
+- **N-9** TypedPython memory safety is proved on the IR before C is generated (#41; maintainer decision
+  2026-10-03). Each property, and what happens when it cannot be proved:
+
+  | Property proved on the IR | If not proved |
+  |---|---|
+  | No local read before assignment on every path | function not compiled; diagnostic names the local |
+  | Every node's operand types match; no implicit conversion | not compiled; diagnostic |
+  | No deopting node in an impure function | not compiled; diagnostic |
+  | Array access in bounds, or a runtime bounds check kept | the check stays (never an unchecked access) |
+  | Array parameters only indexed, stored, `len`-ed; no aliasing (entry guard) | not compiled; diagnostic |
+  | OBJ references follow one ownership rule; no IR form for free, borrowed alias or NULL read | not compiled; diagnostic |
+  | Integer overflow checked and promoted (deopt); an op marked `proven` must re-prove its interval fits i64 | not compiled; diagnostic `verify/proven-overflow` |
+  | `Call.redo` only from an impure caller to a pure, may-deopt callee returning F64/BOOL/NONE | not compiled; diagnostic `verify/redo` |
+  | `entry_globals` only in a closed function (no user code runs); a call of a function with entry globals is a deopt point in its caller unless it is a legal redo or the caller snapshots the same globals | not compiled; diagnostic `verify/entry-global-open` / `verify/deopt-impure` |
+
+  Generated C reaches memory and `PyObject`s only through the runtime helpers. ASan/UBSan CI,
+  differential tests against the interpreter and fuzzing back the proof. `Status: planned`.
+- **N-10** TypedPython incremental compilation (#41; maintainer decision 2026-10-03). The unit is a module.
+  Its cache key is the source hash, the interface hashes (typed signatures) of the modules it depends
+  on, the compiler version, the target platform and the build flags; a body-only change leaves the
+  interface hash unchanged, so dependent modules are not recompiled. C objects are cached per module.
+  The Gradle task declares exact inputs and outputs so up-to-date checks and the build cache apply.
+  Tests: changing one function body recompiles that module only; an unchanged rebuild spends ~0 s in
+  the compile step. `Status: planned`.
 
 ---