@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 most fuel steps 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) are unknown, never a guess. Each problem has a category as the C family's do (termination for an uncaught exception, unsupported, incomplete for an empty slot, indeterminate for the step limit or waiting for input, invalid for 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 unseeded random starts as seed(0)), str.hash (a set ordered by str hashes, as under PYTHONHASHSEED=0) and object.address (an object's address shown as text, or a set ordered by objects' hashes: the model places the object at heap position a at 0x1000 + 16a, not where CPython's memory would). A verdict proved by the kernels: kernel_verdict_in("python", "python.verdict", …) in cella-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, as type(x).__name__), slots (for each hole, each candidate type is exact, no with the reason, or unknown when it depends on values at run time) and errors (operations that raise TypeError whenever 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.session: the debugger, for cella-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, and lines when the host has the line of each node (statements on one line then stop once, as CPython's line event). 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 | | python.session | the debugger's entry points | | python | the entry: python.verdict, python.types |

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.