Expand description
Small, pure integer kernels of the Improv engine, with Verus specifications and machine-checked proofs.
Each kernel lives in a verus! { ... } block: a spec fn says what it
means, the executable function ensures it, and cargo-verus verify -p improv_verified (see scripts/verify.sh) checks the proof. Under plain
cargo the specs and proofs are erased and the functions are ordinary Rust,
which is what the engine calls: the proven code is the code that runs.
Floating-point arithmetic is out of scope (Verus does not reason about
f64), so every kernel takes and returns integers; the engine does the
float range checks and truncation before calling in.
Modules§
- bits
- The 48-bit operations of
BITAND,BITOR,BITXOR,BITLSHIFTandBITRSHIFT. Operands are below 2⁴⁸ (the engine checks that) and shifts are at most 53 places. - gcd
- GCD and LCM (the spreadsheet
GCD/LCMfunctions). - graph
- The dependency build order: a depth-first topological sort that rejects cycles, so building (and evaluating) the derived measures terminates.
- keys
- Coordinate-key projection and union: the key arithmetic of every dimensional join.
- radix
- Base conversion between integers and digit vectors (most significant
first):
BASE, and the 10-digit two’s complement ofDEC2BIN/BIN2DECand the rest of the radix 2 / 8 / 16 family. - take
- The index range of
TAKE/DROPover a list.