@cella-lang/python
Python for the Cella proof checker, as a compiled module pack. A program
comes as its syntax tree (a subset of CPython's ast as JSON); the model runs it with CPython 3.14's semantics and gives
a verdict, a debugger that stops where CPython's tracer does, and a type query for the editor. Everything is defined in
Cella, so a verdict can be proved by both kernels.
Depends on @cella-lang/machine.
Entries
python.verdict json input fuel: runs the program on the input for at mostfuelsteps and returns{verdict, basis, exit, out, problems, assumes}(the same shape as the C family's verdicts). An uncaught exception is defined behavior (accept, exit 1, the exception as a problem). Running out of steps, a construct the model does not take (unsupported, naming it) and an empty slot of the editor (hole, at its label) areunknown, never a guess. Each problem has acategoryas the C family's do (terminationfor an uncaught exception,unsupported,incompletefor an empty slot,indeterminatefor the step limit or waiting for input,invalidfor JSON that is not a program).assumes(always there) lists the implementation's choices the run relied on, each{"implementation": "CPython", "choice": …}:random.seed(an unseededrandomstarts asseed(0)),str.hash(a set ordered by str hashes, as underPYTHONHASHSEED=0) andobject.address(an object's address shown as text, or a set ordered by objects' hashes: the model places the object at heap positionaat0x1000 + 16a, not where CPython's memory would). A verdict proved by the kernels:kernel_verdict_in("python", "python.verdict", …)incella-lang.python.types json candidates: the type query, in the same shape as the C family's:nodes(the type of each expression whose type is known before the program runs, astype(x).__name__),slots(for each hole, each candidate type isexact,nowith the reason, orunknownwhen it depends on values at run time) anderrors(operations that raiseTypeErrorwhenever they run, with CPython's message, also in code that does not run). An operation is tried on a value of each operand's type with the model's own operations; there is no second set of typing rules.python.observedTypes json input fuel: the types one run saw,{verdict, nodes, basis}.nodesmaps each expression's node (and each name an assignment,fororwithbinds, and each parameter) to its type as Python's typing writes it:int,float,str,bool,None, a class's name;list[int],set[str],dict[str, int]with the union of the items' (keys', values') types,tuple[int, str]by position;list[?],set[?],dict[?, ?],tuple[()]when empty. A node whose values had several types gets their union in the order first seen (int|str).basissaysobservedfor those, andunreached(with the empty text) for a node the run did not reach. The types hold for this input only. A run the model cannot finish (unknown) or JSON that is not a program (invalid) gives emptynodesandbasis.python.session: the debugger, forcella-lang/dap:load,run(continue, step in, step over, step out, with breakpoints),stopConf,stopKind,stopNode,stopOut,stopErr,stopDetail,feed(more input),globals,frames,setVarErr,setVarConf,env, andlineswhen the host has the line of each node (statements on one line then stop once, as CPython'slineevent). A stop is at a node; an uncaught exception stops with{"type", "what", "node"}, the node being the expression that raised it.
Modules
Each module imports the standard library, @cella-lang/machine and the modules above it.
| Module | What it is |
|---|---|
python.syntax | python.ast.Program: a subset of CPython's ast with the same constructor and field names behind a prefix (e for expressions, s for statements) and a node id n on each; deriving Json gives the JSON form, literals are text; eHole is an empty slot |
python.values | values (None, bool, int of any size, float, str as code points, tuple, range, classes, functions) and the heap (list, dict, set, views, iterators, cells, instances, classes, generators), raised exceptions, type names and truth |
python.numbers | int and float, floor division and % toward negative infinity, exact comparison of int with float, bitwise operations as infinite two's complement, CPython's hashes |
python.text | str as code points, the classes of code points the model knows, int(s) and float(s) |
python.printing | repr and str (a float's shortest round-trip form) |
python.containers, python.sets | lists, dicts in insertion order, sets in CPython's hash-table order |
python.iterators | iter, next, enumerate, zip, and the size checks of dict and set iterators |
python.operations | the operators on the built-in types, with CPython's errors |
python.objects | attributes, classes (C3 method resolution order), descriptors, closures, exception classes |
python.calls | binding arguments to parameters as CPython's initialize_locals, * and ** at a call |
python.methods, python.builtins | the methods of str, list, dict and set; the built-in functions and math |
python.random | CPython's Mersenne Twister bit for bit, and Lib/random.py's functions |
python.symbols | the symbol table, as CPython's symtable |
python.execution, python.generators | running statements on machine.statement; generators and send, throw, close |
python.dispatch | the user's special methods as statements (operators, comparisons, truth, len, iteration) |
python.flattening, python.lazy, python.sorting | a generator's body as a continuation; map, filter and the other lazy built-ins; sorting with the user's comparisons in CPython's order |
python.lowering | the syntax tree as statements, and the verdict |
python.debugging, python.variables | the debugger's machine (stops as CPython's line events); variables, calls and globals as JSON |
python.querying | the type query; the types a run observed |
python.session | the debugger's entry points |
python | the entry: python.verdict, python.types, python.observedTypes |
Assumed
A float's ** (and pow, math.pow, the math functions) gives the correctly rounded result. CPython calls the
platform's C pow, which the C standard does not require to round correctly (macOS gives 1.7976931348623157e308 ** 0.5 one unit in the last place above the correctly rounded value); as for C and C++, a verdict that depends on the
last bit holds for a libm that rounds correctly.
Not in this version
Modules other than math and random, the !a conversion, built-ins the model does not provide (hex and others),
a user's object compared inside a container comparison, and a user's function shown as text (CPython shows its
address; a function value of the model has none). A program that uses one of them is unknown with the construct
named (tests/deep_unsupported).
Loading
Load the packs into the cella-lang build named by index.json (checkerHash, cbfVersion; the peerDependencies
pin it): the standard modules in index.requires["cella-lang"].modules, the packages in index.requires.packages
(each the same way), then this package's modules in the order of index.modules.python.deps. cella-lang's README
(Official packages) has the code.