cella-lang

The Cella proof checker, compiled to WebAssembly — the same build that runs the Cella Playground. Runs in browsers and in Node (≥ 18).

Cella 證明檢查器的 WebAssembly 版本，與 playground 同一份建置。瀏覽器與 Node（18 以上）都能用。

Contents

| file | what | |---|---| | cella.js, cella_bg.wasm | the checker (wasm-bindgen, ES module) | | stdlib.cell | the preloaded standard library (snapshot) | | modules/<name>.cell, modules/index.json | importable library modules, loaded on import | | corpus.json | runnable examples with this build's expected verdicts (see Corpus) |

Three modes

import { readFileSync } from 'node:fs';
import init, { check, holes, vocabulary, stdlib_mode, init_stdlib_cached, init_stdlib_explicit, load_module_pack, load_library_pack } from 'cella-lang';
import { assets } from 'cella-lang/assets';

await init({ module_or_path: readFileSync(assets.wasm) });

// 1. standalone — no stdlib: single file, no imports, nothing preloaded
stdlib_mode();            // "standalone"
vocabulary();             // JSON: every closed set a verdict can contain (switch on these, not on a copied list)
check(source);            // JSON verdict: {"ok", "verdict", "checker", "unknown", "assumptions", "errors"?}
holes(source);            // same as `cella holes --json`: {"ok", "holes": [{name, type, context, line, col, …}], "checker"}
// Provenance: write `@[origin "your-key"]` before a declaration. Cella does not interpret the key; it comes back on
// errors, unknown entries and holes inside that declaration (`"origin"`), plus `"origins": [{def, origin, verdict}]`.

// 2. preloaded — after loading the standard library (process-wide, cannot go back)
init_stdlib_cached(readFileSync(assets.stdlib));
stdlib_mode();            // "preloaded"
load_module_pack(readFileSync(assets.module('nat')));   // load `modules/index.json` deps first
check('import nat\n...');

// 3. explicit — the standard library is loaded (packs can be stacked on it), but nothing is imported implicitly:
//    a program sees only what it imports (even `prelude`). Use this instead of 2. when you need to know exactly
//    what a verdict depended on. Choose 2. or 3. once per process.
init_stdlib_explicit(readFileSync(assets.stdlib));
stdlib_mode();            // "explicit"
load_library_pack(index, 'cpp', cppPack);                // e.g. @cella-lang/cpp (load its index.requires first)
check('import cpp\ndef x : cpp.Int32 := cpp.lit (pos 5) refl');
// every verdict says what it depended on (all three modes):
//   "imports": [{"module": "cpp", "checker": "<checkerHash>"}, …]   — the modules this check could see (dependency closure)
//   "warnings": [{"message", "line", "col"}]                        — e.g. a `data` type shadowing an imported one

checker.hash in every verdict identifies the exact build; pin the package version.

When to upgrade

package.json carries two fingerprints:

• cella.checkerHash — the exact build (changes on any source change, even comments).
• cella.semanticsHash — the checker's decisions on a fixed corpus (corpus.json: 6 standalone programs plus the playground's examples and tutorials, 73 in all): definitions, verdict, unknown reasons and assumptions — not error messages. It changes when what the checker decides changes, not when only messages or comments do. Compare yours with npm view cella-lang cella.semanticsHash; if they differ, the checker's judgments moved — look before upgrading. It only sees behaviour the corpus exercises; to cover your own files, run them on both versions and compare the verdicts.

Corpus

corpus.json (import corpus from 'cella-lang/corpus.json' with { type: 'json' }, or where import attributes are not available, JSON.parse(readFileSync(require.resolve('cella-lang/corpus.json'), 'utf8'))) is the corpus behind semanticsHash, with the verdicts this build gives — generated by the same run that computes the hash, so it cannot drift from the checker. Read it to discover what the language accepts; run it to confirm what the checker does today.

{ "semanticsHash": "…",
  "entries": [ { "name", "mode": "standalone" | "preloaded",
                 "modules": [ /* packs to load first, in order */ ], "code",
                 "expected": { "verdict", "defs", "unknown": ["def:reason"], "assumptions": ["kind:name"] } } ] }

Run the standalone entries before init_stdlib_cached (mode is process-wide), then the preloaded ones in file order, loading each entry's modules that are not loaded yet. Error messages are not part of expected; they may change between builds.

Glossary

Two columns matter most: whether a thing is gone, and what it is not. Both kinds of mistake are silent. The closed sets a consumer switches on are not copied here (a copied list goes stale): call vocabulary() — it returns {verdict, unknown_reason, assumption_kind, rating_op, missing_kind}, the very names verdicts are built from.

| term | is | removed? | is not | |---|---|---|---| | verdict | accept / reject / unknown, with unknown reasons and assumptions | — | a boolean; unknown is not reject | | ok in check() | true only when the verdict is accept | — | the same ok as in holes() | | ok in holes() | the hole list is trustworthy (the file parsed and elaborated far enough to list them) | — | a verdict — ok: true with a non-empty holes is normal | | checker.covers | which sources checker.hash fingerprints (kernel, elaborator) | — | which layers checked this verdict — kernel re-checking shows up per verdict as assumptions not_rechecked_by_kernel / unknown kernel_skipped; stdlib absent means the hash does not fingerprint the library, not that the library is fine | | standalone | no stdlib preloaded: single file, import is not followed | — | a smaller stdlib — there is none | | preloaded | after init_stdlib_cached; every program implicitly imports the preloaded modules; import loads module packs | — | reversible within a process | | explicit | after init_stdlib_explicit; packs can be stacked, but a program sees only what it imports | — | standalone — the library is loaded; and not preloaded — nothing is implicit | | imports (in a verdict) | the modules this check could see (its imports' dependency closure), each with the checker fingerprint | — | the modules loaded in the process | | multiplicity 0 ((0 x : A)) | erased at run time: used only in types | — | definitional irrelevance — two values differing only at a 0 position are not equal | | definitional proof irrelevance (F171) | conv skipped 0-usage positions | ✅ 2026-09-30, unsound (Box Nat ≡ Box Empty gave a closed Empty) | — | | hole (?name) | a missing piece; holes() lists its type and context | — | an error; a file with holes checks as unknown | | @[origin "key"] | your key, returned on errors / unknowns / holes inside that declaration | — | interpreted by Cella | | @[irreducible] | the definition is not unfolded in conv; its name is kept in displays | — | display-only — refl can no longer prove a goal that needs it unfolded (corpus: standalone:irreducible-contract-blocks-refl) | | termination_by_elaborator (assumption) | a recursive function in the dependency closure whose termination was checked by the elaborator's termination checker; the second kernel re-checks the function only under the assumption that it has its declared type | — | unchecked — the elaborator did check it; what is missing is an independent (kernel) re-check of termination | | postulate | an assumed constant; shows up in assumptions | — | proved | | rule | a rewrite rule (rule r x : lhs ≡ rhs) on any visible postulate or def; both kernels check that every critical pair joins (also between rules from different modules, at import); shows up in assumptions | — | a proof — confluence is checked, the equation is assumed | | compile_wasm / wasm codegen | compiles a Cella program to WasmGC | — | the checker's own wasm (cella_bg.wasm) | | checkerHash | fingerprint of the build | — | a fingerprint of behaviour — use semanticsHash | | semanticsHash | fingerprint of the verdicts on corpus.json | — | coverage of behaviour the corpus does not exercise |

License

Apache-2.0 — see LICENSE and NOTICE. Copyright 2026 SungYu Chang.