@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.