@cella-lang/machine
The language-neutral execution layer for the Cella proof checker, as a
compiled module pack. Every language's semantics needs these pieces and none of them owns them: the C family
(@cella-lang/cfamily, c, cpp, arduino) and Python (@cella-lang/python) are built on it, and so can the next
language.
The package has no entry of its own; a language package exports its verdict, type query and debugger, built from these modules.
Modules
| Module | What it gives |
|---|---|
machine.bits | Fixed-width two's complement integers: wrapping into the signed or unsigned range of a width, with theorems that the result is in range; bitwise operations and shifts. Which widths a language has is the language's. |
machine.float | IEEE 754 binary floating point: add, subtract, multiply, divide and square root compute the exact rational result and round it to nearest, ties to even, so results agree bit for bit with any conforming implementation. |
machine.float.decimal | Correctly rounded decimal digits of a floating value (significant digits, or a fixed number of places). |
machine.float.functions | Correctly rounded pow, exp and log (Ziv's method). |
machine.console | Standard input and output as a state, not an effect: the input not read yet, the output written so far, and the flags a read raises. A debugger feeds input while the program waits. |
machine.checked | Computations that may stop with a reason (Checked R A). A precondition is evaluated where the operation is reached; verification and execution are the same term. |
machine.statement | A small-step machine for structured statements: sequence, conditionals, loops with break and continue, switch with fallthrough, calls, try, and cleanup on every way out. |
machine.debugger | A debugger driver for any language's machine: breakpoints, step in, over and out, fuel, waiting for input, and the kind of each stop (Stop.kind). |
machine.dap | The JSON a Debug Adapter Protocol host reads at a stop: its kind, details, call stack and variables. The shapes are the same for every language, so a host needs no change for a new one. |
Loading
The pack loads into the cella-lang build named by index.json (checkerHash, cbfVersion); the peerDependencies
entry pins that version. Load the standard modules it needs first (index.requires["cella-lang"].modules, with
load_module_pack), then its own modules in the order of index.modules.machine.deps (with load_library_pack, which
refuses a pack with a reason if the checker or format does not match). A language package lists @cella-lang/machine
in its index.requires.packages, and loads it the same way before itself.
Changes
See CHANGES.md.