@cella-lang/cpp

C++17 for the Cella proof checker, as a compiled module pack: the C++ branch of the C family's deep embedding (@cella-lang/cfamily). A program is checked by C++17's rules and run by a small-step semantics; the verdict is accept, reject or unknown, with the node and the clause of the standard.

Depends on @cella-lang/cfamily and @cella-lang/machine.

Programs

The JSON of cfamily's syntax with "lang": {"k": "langCpp"} and no board (a program for a board is @cella-lang/arduino's). The branch covers classes (inheritance, virtual functions and virtual bases, constructors, destructors and copies), templates and overloading, references and move semantics, lambdas, exceptions and the standard exceptions, iostream input and output, and std::vector, std::string and std::initializer_list, which are written in C++ and checked by the same rules as the program.

A value the standard leaves to the implementation is libc++'s, and the verdict says it assumed so (assumes). A standard function, or a member of a library class, that the model does not provide yet makes the verdict unknown with the reason, not a rejection.

Entries

• cpp.verdict src input fuel: the verdict JSON (format in @cella-lang/cfamily); input is standard input, fuel bounds the steps. A verdict proved by the kernels: kernel_verdict_in("cpp", "cpp.verdict", …) in cella-lang.
• cpp.types src candidates: the type query (format in @cella-lang/cfamily).
• The debugger, for cella-lang/dap: load, run, stopConf, stopKind, stopNode, stopOut, stopErr, stopDetail, divergences, feed, globals, frames, setVarErr, setVarConf, env; and report input fuel session, a whole run with all the input given at once.

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.cpp.deps. cella-lang's README (Official packages) has the code.

Per-definition hashes

index.json lists, for every definition, own (its own content) and merkle (its content and everything it depends on). A definition whose merkle did not change between two versions means the same; a changed one is listed in CHANGES.md.