Repository navigation
TypedPython stage 2: typed IR → C back end, end to end on desktop - #64
Merged
Merged
Conversation
Step 1 of docs/design/typedpython.md: python -m typedpython check runs Pyrefly with its Any-leak kinds raised to errors, reports user-code expressions of type Any outside cast() (any-flow), and reports the forbidden list as warnings in checked mode and errors in compiled mode. Lives in python-multiplatform-ksp. INTENT gains TypedPython as purpose 4 (maintainer statements quoted); SPEC gains N-6 (partial: not yet run by the build). Refs #16
Pyrefly 1.3.2 reports neither and records no types for assignment targets, but it does record the type of every name load. The gate now writes a probed copy in which each candidate assignment is followed on the same line by a load of its targets (line numbers unchanged), runs Pyrefly on it, and judges the types at the probe positions. The second run happens only when a file assigns a name twice or has a container display. Refs #22
The gate's Pyrefly config lives in a temporary directory, which Pyrefly took as the import root, so relative and absolute self-imports of user packages did not resolve and every value from them failed as any-flow. Each checked file's import root (above its outermost package) now goes on the search path. Red before the fix: 3 failed in test_imports.py. Refs #16
A probed copy written alone into a temporary directory lost its package, so relative imports in it did not resolve, their values were Unknown, and rebinding went unreported in exactly the code that lives in packages. The probe pass now copies each file's package tree with the same layout. Red before the fix: test_rebinding_inside_a_package_with_relative_imports. Refs #22
A directory argument crashed with IsADirectoryError (found by the toolchain typedpythonCheck work). Directories now expand to their .py files, skipping hidden directories, __pycache__ and build. Red before the fix: test_a_directory_is_checked_file_by_file. Refs #16
The IR between the front end (AST + Pyrefly types) and the C back end, with each node specified by its CPython behaviour: checked i64 arithmetic that deopts on overflow, Python floor division and modulo, exact int/float comparison, list-semantics indexing, math errors, and native arrays for list[float]/list[int] parameters with entry guards and write-back. Also brings the TypedPython CI workflow (without Cython). Refs #41
SPEC N-7 (compile to C), N-8 (memory safety proved on the IR; a function that cannot be proved stays interpreted with a diagnostic) and N-9 (module-level incremental compilation keyed by source, dependency interfaces, compiler version, platform and flags), all planned. The IR gains 'proven' on array accesses, set only by the verifier. Refs #41
… and the compiled builtin Refs #41
New IR nodes Global, GetAttr, CallObject (vectorcall with keywords), Truth, CompareObj and ObjToFloat, with runtime helpers. A function that calls the binder becomes impure, so its unbounded ints stay CPython int objects, while floats, bounded indices and the surrounding loops stay native. PyCall is replaced by CallObject(Global(name)). Refs #41
When a file needs probing, every file of the check is mirrored and Pyrefly runs once on the copies; errors and any-flow positions are mapped back to the original columns (_Remap), and an error inside an inserted probe surfaces as internal/probe-error instead of being dropped. Red: test_pyrefly_runs_once_when_a_file_has_a_candidate (2 runs). Mutation: removing the column shift fails the remap test. Refs #21
Cache key = source hash + dependency interface hashes (typed signatures only) + compiler version + platform + flags. A body-only change leaves the interface hash unchanged, so dependents are reused. Entries are written atomically and a corrupt or missing entry is a miss. BuildReport says why each module rebuilt. Red: module missing. Green: 10/10; unchanged rebuild 1.21 ms with 0 compile calls. Mutation (deps keyed by source hash): body-change test fails. Gradle up-to-date wiring of SPEC N-9 is not part of this commit. Refs #41
verify(module) proves, per function, definite assignment, exact node typing, deopt placement (no deopting node in an impure function; pure/may_deopt/stored flags recomputed and compared), array use and bounds (proven only for range(k>=0, len(a)) indices; everything else keeps the runtime check), OBJ ownership, resolved calls and no recursion. A function it cannot prove leaves 'functions' for 'skipped' with the rule and reason. Red: 84/84 failing on import. Green: 84/84. Disabling deopt-impure, bounds, definite assignment or condition-only placement fails 10/9/6/2 tests; 200 seeded IR mutants all caught. Refs #41
CompareObj takes two OBJ operands and appears only directly as a condition; Unbox checks the exact type at run time and deopts, so it is pure-only; Global returns a new reference; call cycles are rejected (no RecursionError in C); ATAN2/HYPOT take two arguments; Function.locals excludes parameters; a value- returning function returns on every path; -2**63 % -1 handled by the runtime. Refs #41
The typedpython wheel installs a one-line .pth that sets builtins.compiled to an identity decorator unless the runtime already set it (#42 sets it in the embedded interpreter). Pyrefly 1.3.2 reads __builtins__.pyi from a search path entry as extra builtins, so the gate adds typedpython/builtin_stubs and @compiled type-checks without an import while unknown names still fail. Red: 5 of 7 failing. Green: 7/7, suite 55. Mutation (stub dir off the search path): 2 gate tests fail. Refs #41, #42
…ainst CPython Header-only helpers implementing ir.py's CPython semantics: checked i64 arithmetic, Python floor division/modulo (MIN % -1 handled), exact int/float comparison, CPython's float div/floordiv/mod, math_1/math_2 error rules, exact-type boxing/unboxing, native arrays with dirty write-back, and the opaque-object helpers (global/getattr/vectorcall/truth/compare/binop/release). Exception messages follow the running interpreter (3.13 vs 3.14 differ). Green: 140/140 (default and portable-overflow builds), also under ASan+UBSan via a sanitized launcher. Mutation (floor-mod sign fix removed): 4 fail. Refs #41
cgen generates one C file per module: multi-phase init that runs the module's original source in the extension's own namespace, then swaps each compiled function for a METH_FASTCALL wrapper with entry guards (exact types, i64 range, array enter + aliasing), deopt to __typedpython_interpreted__, and array write-back on every exit. One ownership rule, references dropped only through tp_release; FP contraction off. cbuild compiles with the host or a target CPython's headers via sysconfig, no setuptools or Cython. Green: 29/29 (incl. ASan+UBSan via a sanitized launcher and a compile against the embedded 3.14 headers). Mutation (aliasing guard off): 2 fail. Refs #41, #45
Lowers @compiled functions (or the module marker) to ir.Module: scalar and array parameters, locals from annotations/range targets/Pyrefly probes, purity and may_deopt by fixpoint, an interval proof for i64 operations that cannot overflow, OBJ paths for calls into any callable (Kotlin interop), chained comparisons via temporaries. Anything outside the IR is skipped with a line-numbered reason, never partially lowered. Green: 51/51. Mutation (impure unbounded int forced to I64): 2 fail. Refs #41
# Conflicts: # docs/design/typedpython.md
pipeline.compile_module runs the gate (compiled mode), frontend, verifier, cgen and cbuild; functions outside the IR or unproved stay interpreted with a reason, and a module with nothing left produces no C. python -m typedpython demo builds a module, runs main() both ways and fails on any difference. Red: 5/5 NotImplementedError. Green: 5/5 (incl. fact(30) promoting past i64 and demo identical output). Whole integration suite: 372 + 5. Refs #41
Found by running the pipeline on nbody/spectral-norm: the front end proves some i64 operations cannot overflow but the IR could not say so, so the verifier rejected advance/energy. New: BinOp/UnaryOp.proven (re-proved by the verifier), Call.redo (an impure caller may call a pure may_deopt callee; only the callee is redone, F64/BOOL/NONE results only), Function.entry_globals (scalar module globals read once at entry in closed functions). Also: CompareObj is RichCompare+truth without the identity shortcut; exception messages follow the running interpreter (3.14 changed some). Refs #41
Interval-proved I64 ADD/SUB/MUL/NEG carry proven=True (no deopt, allowed in impure code); an impure caller calls a pure may_deopt F64/BOOL/NONE callee with redo=True; scalar module constants read only in closed functions become entry_globals. nbody advance/energy/offset_momentum and spectral-norm eval_a/mul_av/mul_atv now lower. Red: 10 failed / 60 passed. Green: 70/70. Mutation (proven never set): 3 fail. Refs #41
Exact interval arithmetic re-proves every proven I64 op (never trusts the flag); redo is legal only from an impure caller to a pure may_deopt F64/BOOL/NONE callee; entry globals need a closed function (fixpoint over the call graph). A call of a function with entry globals counts as deopting in the caller unless it is a legal redo or the caller snapshots the same globals. Red: 42 failed. Green: 135/135; 300 seeded mutants of 16 kinds all rejected. Mutation (interval-fit check off): 12 fail. Refs #41
Proven ops keep the checked helper and raise SystemError if one overflows; a redo call reruns only the callee's interpreted function and continues the caller (result type checked exactly); entry globals are read, type-guarded and released in the wrapper before the impl runs, so a mismatch redoes the whole call before any effect. Green: 39 passed, 1 skipped (incl. ASan/UBSan). Mutation (redo the caller instead of the callee): 5 fail. Refs #41
…s (N-8) Including the rule the verifier added: a call of a function with entry globals is a deopt point in its caller (its entry guard can fail mid-call) unless it is a legal redo or the caller snapshots the same globals. Refs #41
NewArray ([fill]*n, list(range(n))), CopyArray (a[:]) and Tuple. A local array is owned by the function and never escapes, so storing into it is not an effect and its length never changes (bounds proofs against Len hold). Runtime API gains new/iota/copy/free for local arrays and tp_tuple. Leader decision: fannkuch's local list[int] and tuple return are in M2. Refs #41
…python build) compile_project runs the gate, frontend and verifier as BuildCache's lower step (so interface hashes describe what was actually compiled), cgen and cbuild as generate/compile_c. COMPILER_VERSION is a content hash of the typedpython package; platform is sysconfig platform + EXT_SUFFIX. CLI: python -m typedpython build [--cache DIR] [--out DIR] PATHS... Red: 7/7 missing compile_project. Green: 7/7 with real Pyrefly and C builds; unchanged rebuild of 3 modules 0.002 s with 0 lower/compile calls; a body-only change rebuilds that module only. Mutation (hash the unverified module): test 7 fails. Refs #41
A sanitizers job (ubuntu) builds every TypedPython extension with -fsanitize=address,undefined and runs the cgen, runtime and pipeline tests with libasan preloaded. It first runs a self-check that requires ASan to report a planted heap overflow and UBSan a planted signed overflow, so a setup that silently detects nothing cannot pass. Verified locally on macOS via the sanitized launcher: self-check OK, 185 passed. The Linux route is verified only by the first CI run. Refs #41
NewArray/CopyArray only as the value of an Assign to a matching array local; a local array never escapes (any value use is verify/array-escape); stores into local arrays are not effects; single-assignment local arrays carry a length interval for bounds proofs; Tuple elements are OBJ and it creates a reference. Red: 67 failed / 144 passed. Green: 211/211; 400 seeded mutants of 18 variants all rejected. Mutation (escape check off): 16 fail. Refs #41
list(range(n)), [v]*n and a[:] become NewArray/CopyArray of an I64/F64 array local; any other use of a local array skips the function with the statement named. Stores into local arrays are not effects, so such a function stays pure. return a, b lowers to a Tuple of boxed values (returns OBJ) when the annotation matches. fannkuch lowers: pure, may_deopt. Red: 25 failed / 71 passed. Green: 96/96. Mutation (local stores as effects): 2 fail. Refs #41
tp_*_array_new/iota/copy/free and tp_tuple per API.md: negative length is empty, size overflow or malloc failure is MemoryError with a zeroed struct, free is idempotent and never writes back, copy from a parameter array yields a local one, tp_tuple steals nothing. _exit on a local array equals _free. Red: shim build failed (helpers undeclared). Green: 264/264 (default and portable). Mutation (negative n allocates |n|): 22 fail. A standalone ASan+UBSan program over the helpers: clean. Refs #41
Local array locals are runtime structs owned by the function: Assign builds into a zeroed temporary and frees the old array on success; every exit (ok, error, deopt) frees them; no write-back or dirty bits. Stores into local arrays are not effects. Tuple builds from owned temporaries via tp_tuple. Red: 4 failed + 11 errors. Green: 58/58 incl. ASan on the new functions. Mutations: skipping frees on the deopt or error path each fail their leak test (64 MB leaked vs a 4 MB bound). Refs #41
# Conflicts: # docs/INTENT.md # docs/SPEC.md
…t head The first CI run's self-check failed: a read 56 bytes past an 8-byte block can land outside its redzone, so ASan reported something other than heap-buffer-overflow, and only the report's tail was printed. Read the first byte past the end (always in the redzone) and print the head of the output on failure. Refs #41
The second CI run showed the planted read is caught, but by UBSan's object-size check, which halts first. Build the fault-planting extension with -fno-sanitize=object-size so that case proves ASan; the signed-overflow case already proves UBSan. Refs #41
This was referenced Oct 3, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Refs #41 (stage 2: typed IR → C), #42 (the
compiledbuiltin: the typedpython side), #45 (Kotlin interop: plain-CPython tests).This does not close #41. M2 still needs the official
@compiledmeasurement, identical output on all 5 benchmarks, the incremental cache wired into the build, and ASan/UBSan in CI.Stacked on #19 → #33 → #52. It contains their commits, so merge those first.
Feature added
TypedPython stage 2, end to end on desktop: source → gate (compiled mode) →
frontend→verify→cgen→cbuild→ CPython extension.python -m typedpython demo <module> [args]builds a module, runsmain()both interpreted and compiled, and fails unless the output is identical.ir.py,runtime/API.mdruntime/tp_runtime.hfrontend.pyverify.pycgen.py,cbuild.pyincremental.pycompiledbuiltin (.pth+__builtins__.pyi)builtin_stubs/pipeline.py,__main__.pyWhole suite: 458 passed. Every component's red output, green run and mutation check are in its commit message.
Demo (single runs at load ~5–6, not official measurements)
Documentation corrected
@compiledis a builtin.proven,redoandentry_globals.Defect fixed
ir.pyfailed to import after 957315e (field order). Fixed in ac366e9.