@cella-lang/cpp

C++ integer types for the Cella proof checker, as a compiled module pack.

C++'s int is not a mathematical integer: its width depends on the platform, signed overflow and division by zero are undefined behaviour, and division truncates toward zero. This library defines the C++ semantics directly:

• cpp.IntN bits — a value plus a proof that it lies in [−2^(bits−1), 2^(bits−1)−1];
• cpp.add / sub / mul / neg / div / rem take the "no overflow / no division by zero" precondition as an argument (for concrete values, (cpp.inRange refl) and refl); cpp.lt / le / eq have none;
• correspondence theorems with ℤ (cpp.toInt_add …, cpp.toInt_inj) proved once for every width;
• platform profiles: cpp.lp64.Int (32 bits) / cpp.lp64.Long (64), cpp.avr.Int (16) / cpp.avr.Long (32);
• cpp.Int32 is the LP64 int.

import cpp
def x : cpp.lp64.Int := cpp.add (cpp.lit (pos 30000) refl) (cpp.lit (pos 30000) refl) (cpp.inRange refl)   -- accept
def y : cpp.avr.Int  := cpp.add (cpp.lit (pos 30000) refl) (cpp.lit (pos 30000) refl) (cpp.inRange refl)   -- reject: overflows 16 bits

Loading

The pack only loads into the cella-lang build named by index.json (checkerHash, cbfVersion); the peerDependencies entry pins that version.

import init, { init_stdlib_cached, load_module_pack, load_library_pack, check } from 'cella-lang';
import assets from 'cella-lang/assets';
const index = await (await fetch(new URL('./index.json', libUrl))).text();
// 1. the standard modules it needs: index.requires["cella-lang"].modules (from cella-lang's own modules/)
for (const m of JSON.parse(index).requires['cella-lang'].modules) load_module_pack(await bytes(assets.module(m)));
// 2. the library itself — refused with a reason if the checker or format does not match
const r = JSON.parse(load_library_pack(index, 'cpp', await bytes(new URL('./cpp.cell', libUrl))));
if (!r.ok) throw new Error(r.error);

Per-definition hashes

index.json lists, for every definition, own (its own content) and merkle (its content plus everything it depends on). When you upgrade, the definitions whose merkle changed are exactly the ones whose meaning may have changed.