What the Lean model of Python runs, measured. Everything outside the modelled tier is refused loudly (Res.unsupported, with a message naming the construct); it is never answered with a wrong value. The pass rate and the grammar table come from runs against the pinned CPython oracle; the builtin lists are the interpreter's own name tables. CI fails if this page goes stale (harness/coverage_page.py --check).
harness/diff_test.py runs every row of harness/cases.json through the model and through CPython 3.9 and compares the outcome (value, or exception class) exactly.
| rows | agree with CPython | disagree | recorded refusals |
|---|---|---|---|
| 3524 | 3193 | 0 | 331 |
Of the 3193 rows the model decides, 3193 agree with CPython (100.0%). A recorded refusal is a row kept in the suite to pin a known gap: the model must refuse it, and the suite fails if it ever answers instead.
The rows above run through the runner's interpreter (LeanModels/Python/Monadic/). Theorems are stated about a second definition, LeanModels/Python/Semantics.lean, whose tier is narrower (python-architecture.md). diff_test.py --proof-interpreter runs the same rows through it; a refusal there is allowed, a wrong answer is not.
| rows | agree with CPython | disagree | refused |
|---|---|---|---|
| 3524 | 3119 | 0 | 405 |
harness/refusal_census.py --grammar: one small witness program per production of CPython 3.9's ast grammar, plus edge rows. MATCH means the model ran the witness and agreed with CPython; it does not mean every use of the construct is in tier (2 * 3 runs, [1] * 3 refuses). REFUSE shows the model's refusal message.
144 witnesses: 126 MATCH, 18 REFUSE.
| witness | verdict | refusal message / note |
|---|---|---|
FunctionDef |
MATCH | plain positional def |
AsyncFunctionDef |
REFUSE | unsupported statement 'AsyncFunctionDef' |
ClassDef |
MATCH | H3 class tier, default protocol only |
Return |
MATCH | |
Delete |
MATCH | bare-name del at module scope |
Assign |
MATCH | |
AugAssign |
MATCH | |
AnnAssign |
MATCH | an unshadowed builtin type annotation has no effect observable in the tier, so the assignment is admitted |
AnnAssign-forward |
MATCH | A forward-reference string annotation evaluates after the value is stored; its unobservable annotation-table … |
AnnAssign-local |
MATCH | FUNCTION scope: PEP 526 never evaluates the annotation, so this is an ordinary assign — was REFUSE, landed by… |
AnnAssign-novalue |
MATCH | an unobserved value-less local annotation is erased safely |
For |
MATCH | |
AsyncFor |
REFUSE | unsupported statement 'AsyncFunctionDef' |
While |
MATCH | |
If |
MATCH | |
With |
MATCH | single synchronous context-manager item |
AsyncWith |
REFUSE | unsupported statement 'AsyncFunctionDef' |
Raise |
REFUSE | 'raise ' (anything but an admitted exception class name) is outside the tier (docs/memory-model.m… |
Raise-empty-constructor |
MATCH | a direct zero-argument exception constructor lowers to the admitted class-identity raise; payload-bearing con… |
Raise-class |
MATCH | bare admitted builtin exception class; payload construction remains unfinished |
Try |
MATCH | FLIPPED by §except-builtin: ValueError is now an admitted handler class. WHAT THIS ROW PROVES AND DOES NOT:… |
Assert |
MATCH | assertion failure uses the admitted builtin exception hierarchy |
Import |
REFUSE | unsupported statement 'Import' |
ImportFrom |
REFUSE | unsupported statement 'ImportFrom' |
Global |
REFUSE | unsupported statement 'Global' |
Nonlocal |
REFUSE | unsupported statement 'NestedDef' |
Expr |
MATCH | |
Pass |
MATCH | |
Break |
MATCH | |
Continue |
MATCH |
| witness | verdict | refusal message / note |
|---|---|---|
BoolOp |
MATCH | |
NamedExpr |
MATCH | §L14's walrus, general expression position |
BinOp |
MATCH | |
UnaryOp |
MATCH | |
Lambda |
MATCH | module-scope single-target lambda only |
IfExp |
MATCH | |
Dict |
MATCH | |
Set |
MATCH | lowered to set(list) at ingestion; order remains unobservable |
ListComp |
MATCH | desugared to list(genexp) at ingestion |
SetComp |
MATCH | lowered to set(generator) at ingestion |
DictComp |
MATCH | lowered to dict(generator) at ingestion |
GeneratorExp |
MATCH | lowered to a synthesized generator function |
Await |
REFUSE | unsupported statement 'AsyncFunctionDef' |
Yield |
MATCH | statement position only |
YieldFrom |
MATCH | inlined at ingestion |
Compare |
MATCH | |
Call |
MATCH | |
JoinedStr |
MATCH | intrinsic str/repr replacement fields; nonempty specs remain a gap |
FormattedValue |
MATCH | intrinsic conversions; !a and nonempty format specs remain gaps |
FormattedValue-repr |
MATCH | repr conversion bypasses shadowed builtin names |
FormattedValue-debug |
MATCH | CPython supplies debug text and default repr conversion |
FormattedValue-empty-spec |
MATCH | explicit empty format specification |
Constant |
MATCH | the int/str/bool/None inventory |
Attribute |
MATCH | |
Subscript |
MATCH | |
Starred |
MATCH | display position only |
Name |
MATCH | |
List |
MATCH | |
Tuple |
MATCH | |
Slice |
MATCH | str receivers; list/tuple slices allocate and refuse |
| witness | verdict | refusal message / note |
|---|---|---|
for |
MATCH | the live cursor — inch 3a. Was REFUSE/mono=MATCH while there were two interpreters; there is one now, so the … |
list |
MATCH | a DRAINING consumer: no mutation window — landed by §L53 rung 3b |
tuple |
MATCH | landed by §L53 rung 3b |
sorted |
MATCH | landed by §L53 rung 3b |
sum |
MATCH | landed by §L53 rung 3b |
max |
MATCH | landed by §L53 rung 3b |
star |
MATCH | landed by §L53 rung 3b |
for-in-function |
MATCH | the cursor at FUNCTION scope — execGen's arm, and it exercises break and continue through the new frame (… |
for-keys |
MATCH | for k in d.keys() at function scope — inch 3c-i-a |
for-values |
MATCH | for v in d.values() — the VALUES view, whose element is the value, not the key |
values |
MATCH | the VALUES view, consumed immediately — inch 3c-i-b |
items-consumed |
MATCH | the ITEMS view, consumed immediately — inch 3c-i-b |
view-escapes |
REFUSE | method call '.keys' on a dict is outside the tier (dict '.get'/'.clear' only; docs/memory-model.md) |
values-identity-eq |
REFUSE | method call '.values' on a dict is outside the tier (dict '.get'/'.clear' only; docs/memory-model.md) |
keys-set-algebra |
REFUSE | method call '.keys' on a dict is outside the tier (dict '.get'/'.clear' only; docs/memory-model.md) |
enumerate |
MATCH | the key cursor with an index — inch 3c-i-c |
enumerate-start |
MATCH | the START is an int, not a Nat: CPython counts from a negative start as readily as a positive one — inch … |
enumerate-escapes |
MATCH | THE RULED DELTA (2026-08-23-pycomplete-13 (c)): binding an enumerate and then GROWING the dict is SILENT in C… |
enumerate-resize |
MATCH | the same two statements as dict.enumerate-escapes with a different THIRD line, and that pairing is the poin… |
enumerate-of-items |
REFUSE | method call '.items' on a dict is outside the tier (dict '.get'/'.clear' only; docs/memory-model.md) |
iter-next |
MATCH | the flagship's key expression, minimal: CPython answers 2 — the FIRST key in INSERTION order, which is what m… |
iter-steps |
MATCH | ONE cursor, stepped twice. next already implemented both its forms, so the inch bought the stepping for fre… |
iter-empty |
MATCH | the 2-argument next on an EXHAUSTED-at-birth cursor: CPython answers the default, and the 1-argument form o… |
iter-escapes |
MATCH | dict.enumerate-escapes again, at a different builtin: binding an iterator and then GROWING the dict is SILE… |
iter-resize |
MATCH | the same two statements with a different THIRD line, and that pairing is the point: stepping after the growth… |
iter-exhausted |
MATCH | THE EXHAUSTION BOUNDARY, measured: an iterator STEPPED PAST the end is DEAD (CPython clears its di_dict), s… |
iter-for |
MATCH | THE WITNESS FOR THE ALLOCATOR CENSUS. iter is the THIRD expression that can allocate an Obj.generator wit… |
iter-churn |
REFUSE | the dict's KEY SET changed during iteration without changing its size — CPython's answer depends on its entri… |
iter-of-list |
MATCH | THE RECEIVER BOUNDARY, now ANSWERED. list_iterator is a PLAIN INDEX cursor — it_index against the CURRENT… |
genexp-next |
MATCH | the flagship's key expression: CPython answers 1 -- the first key in INSERTION order that passes the filter. … |
genexp-nomatch |
MATCH | no key passes the filter, so the 1-argument next is the faithful StopIteration -- and dict.genexp-default… |
genexp-default |
MATCH | the 2-argument form on the same empty filter |
genexp-drain |
MATCH | the same filter under a DRAINING consumer, which is a different lowering admission path (list is in drainin… |
genexp-bound-is-loud |
MATCH | PEP 289 calls iter() on the outermost iterable when the genexp OBJECT is made, so the cursor's size guard p… |
genfun-mutate-after-create |
MATCH | THE NEGATIVE HALF, and it is why the fix is genexp-only: calling a generator FUNCTION runs no code, so CPytho… |
keys |
MATCH | a view method in CONSUMING position — landed by inch 3c-i-b's ingestion rewrite, on a dict LITERAL receiver, … |
items |
MATCH | MEASURED CORRECTION — the live cursor is already BUILT at MODULE scope (the script executor's .items() shel… |
items-in-function |
MATCH | the SAME loop inside a function — 3a gave the bare-key form a cursor at every scope; 3c-i-a gives the VIEW fo… |
items-grow |
MATCH | MEASURED: the module-scope shell already raises CPython's RuntimeError VERBATIM ('dictionary changed size dur… |
items-update |
MATCH | the admissible regime, already exact at module scope |
update-value-during-iter |
MATCH | MEASURED admissible: updating an EXISTING key's value during iteration is fine in CPython — the regime inch 3… |
grow-during-iter |
MATCH | MEASURED: CPython raises RuntimeError('dictionary changed size during iteration') at the NEXT step — inch 3a … |
churn-during-iter |
REFUSE | the dict's KEY SET changed during iteration without changing its size — CPython's answer depends on its entri… |
| witness | verdict | refusal message / note |
|---|---|---|
dict-key |
MATCH | dict item deletion — the ingestion rewrite to <dictdel>(d, k) |
dict-missing |
MATCH | CPython raises KeyError(9) and the tier reproduces it |
dict-reinsert-order |
MATCH | deletion does NOT hold the slot: reinsertion APPENDS, so the entries array stays exactly the insertion sequen… |
dict-churn |
REFUSE | the dict's KEY SET changed during iteration without changing its size — CPython's answer depends on its entri… |
non-dict-receiver |
REFUSE | 'del o[k]' on a non-dict receiver is outside the tier (dict item deletion only; docs/memory-model.md §the del… |
dict-next-iter |
MATCH | THE FLAGSHIP LINE (sunfish.py:541 del self.tp_score[next(iter(self.tp_score))]), whole. Inch (1) landed the… |
| witness | verdict | refusal message / note |
|---|---|---|
float |
MATCH | binary64 float literal and shortest decimal rendering |
bytes |
MATCH | immutable bytes literals and sequence operations |
complex |
REFUSE | unsupported expression 'Constant:complex' |
ellipsis |
MATCH | Ellipsis is a truthy singleton, also available through the builtin name |
| witness | verdict | refusal message / note |
|---|---|---|
Add |
MATCH | |
Sub |
MATCH | |
Mult |
MATCH | int only; str/list repetition refuses |
Div |
MATCH | true division rounds directly to binary64 |
FloorDiv |
MATCH | Int.fdiv |
Mod |
MATCH | Int.fmod; bare % string formatting is a second tier |
Pow |
MATCH | MEASURED CORRECTION: ** is in tier; bounded negative integer exponents now return binary64 |
Pow-negative |
MATCH | bounded negative integer exponent returns binary64 |
LShift |
MATCH | budget-capped shift width |
RShift |
MATCH | was REFUSE; §L39 rung 1 landed it (op.RShift-budget is its edge) |
RShift-budget |
MATCH | large counts saturate by operand bit length before the shift budget |
BitOr |
MATCH | |
BitXor |
MATCH | was REFUSE — the one witness that found the whole rung; §L39 landed it |
BitAnd |
MATCH | |
MatMult |
MATCH | faithful TypeError for the admitted scalar operand tier |
UAdd |
MATCH | was REFUSE; §L39 rung 1 |
USub |
MATCH | |
Not |
MATCH | |
Invert |
MATCH | was REFUSE; §L39 rung 1 |
Eq |
MATCH | |
NotEq |
MATCH | |
Lt |
MATCH | |
LtE |
MATCH | |
Gt |
MATCH | |
GtE |
MATCH | |
Is |
MATCH | refs by address; two immediates refuse |
IsNot |
MATCH | |
In |
MATCH | |
NotIn |
MATCH | |
And |
MATCH | |
Or |
MATCH |
Read from LeanModels/Python/Ast.lean. A modelled name may still refuse some argument shapes (see the grammar and the differential suite); a refused name always refuses, and never raises a fabricated NameError.
Modelled functions (33 of 73): abs, all, any, ascii, bin, bool, chr, dict, divmod, enumerate, float, format, hex, input, int, iter, len, list, max, min, next, oct, ord, pow, print, range, repr, round, set, sorted, str, sum, tuple
Refused functions (40): breakpoint, bytearray, bytes, callable, classmethod, compile, complex, copyright, credits, delattr, dir, eval, exec, exit, filter, frozenset, getattr, globals, hasattr, hash, help, id, isinstance, issubclass, license, locals, map, memoryview, object, open, property, quit, reversed, setattr, slice, staticmethod, super, type, vars, zip
Also modelled: count (from from itertools import count).
Modelled constants: Ellipsis, False, None, True. Ellipsis and ... denote the same singleton; ordinary name shadowing still applies.
Exception classes except and bare raise can name (16): ArithmeticError, AssertionError, AttributeError, BaseException, Exception, IndexError, KeyError, LookupError, NameError, OverflowError, RecursionError, RuntimeError, StopIteration, TypeError, ValueError, ZeroDivisionError. ImportError and ModuleNotFoundError additionally work as handler names, but their bare raises remain unfinished. Other builtin exception names refuse, including OS-error ancestors such as OSError; user classes class E(Exception): pass are admitted.
Other CPython builtin names (51), refused when used: BlockingIOError, BrokenPipeError, BufferError, BytesWarning, ChildProcessError, ConnectionAbortedError, ConnectionError, ConnectionRefusedError, ConnectionResetError, DeprecationWarning, EOFError, EnvironmentError, FileExistsError, FileNotFoundError, FloatingPointError, FutureWarning, GeneratorExit, IOError, ImportError, ImportWarning, IndentationError, InterruptedError, IsADirectoryError, KeyboardInterrupt, MemoryError, ModuleNotFoundError, NotADirectoryError, NotImplemented, NotImplementedError, OSError, PendingDeprecationWarning, PermissionError, ProcessLookupError, ReferenceError, ResourceWarning, RuntimeWarning, StopAsyncIteration, SyntaxError, SyntaxWarning, SystemError, SystemExit, TabError, TimeoutError, UnboundLocalError, UnicodeDecodeError, UnicodeEncodeError, UnicodeError, UnicodeTranslateError, UnicodeWarning, UserWarning, Warning.