V0.1.0 RELEASED / RUST + LEAN 4
Small bytes.
Explicit contracts.
Varint + ZigZag, with the edge cases accounted for. One small Rust library. A corresponding Lean 4 proof package.
Watch an integer get smaller.
The published Rust codec runs right here in your browser.
Unsigned: 0 to 18,446,744,073,709,551,615.
Browser adapter · bited 0.1.0 · exact BigInt input
01 / VERIFICATION
A small library.
A traceable proof boundary.
The mathematical contract, independent reference semantics and Rust-derived model meet in explicit refinement theorems.
What is proved
ZigZag bijection, encoding and decoding correctness, canonical uniqueness, shortest base-128 length, buffer preservation, streaming equivalence and source correspondence.
Where the proof stops
The pinned extraction profile uses Apple ARM and 64-bit usize. Compiler and machine-code correctness are outside the boundary. Fresh replay uses the same Lean kernel.
02 / PERFORMANCE
Three libraries.
The same integer workloads.
full-width u64 encoder throughput
vs integer-encoding 4.1.0 on Apple M5
| Workload | bited 0.1.0 | leb128 0.2.5 | integer-encoding 4.1.0 |
|---|---|---|---|
| One-byte | 1.086 | 1.790 | 1.092 |
| Short 80 / 15 / 5 | 1.326 | 2.918 | 1.387 |
| Full-width u64 | 2.657 | 18.233 | 5.320 |
| Large full-width traversal | 3.754 | 19.049 | 6.036 |
| Workload | bited 0.1.0 | leb128 0.2.5 | integer-encoding 4.1.0 |
|---|---|---|---|
| One-byte | 1.041 | 5.570 | 1.116 |
| Short 80 / 15 / 5 | 5.011 | 5.667 | 5.057 |
| Full-width u64 | 8.159 | 7.365 | 8.246 |
| Large full-width traversal | 8.571 | 8.482 | 8.573 |
The short mixture is 80% one-byte, 15% two-byte and 5% full-width values. One-byte encoding is close to integer-encoding; the intervals overlap. leb128 is faster at full-width decoding.
These are matched native public API measurements on shared valid inputs, not identical validation work. They do not establish browser/WASM rankings, other-CPU rankings or a universal fastest implementation.
Decoding policies and error behavior.
| Input / contract | bited 0.1.0 | leb128 0.2.5 | integer-encoding 4.1.0 |
|---|---|---|---|
| Redundant zero: 80 00 | Canonical policy rejects; bounded policy accepts and flags it | Accepts 0 | Accepts 0 |
| Truncated: 80 | Truncated, consumed 1 | UnexpectedEof | None |
| Overflow on byte 10 | Overflow, consumed 10 | Overflow | None |
| 11 continuation bytes | TooLong, consumed 10 | UnexpectedEof; reader consumed 11 | None |
| Trailing bytes: 00 01 | Prefix consumes 1; exact API rejects trailing data | Prefix consumes 1 | Returns (0, 1) |
Accepting noncanonical encodings can be an intentional API policy. These observations do not imply that a peer is unsafe or defective. The Lean proof claims on this page concern bited only.
Download raw measurements ↓Read the engineering article ↗03 / THE API
Choose the contract
your caller needs.
use bited::encode_u64;
let encoded = encode_u64(300);
assert_eq!(encoded.as_bytes(), &[0xac, 0x02]);
assert_eq!(encoded.len(), 2);Caller-provided buffers are also supported. Insufficient capacity leaves the output buffer unchanged.
READY TO USE / V0.1.0
A focused primitive
for your next binary format.
Protocols, delta-coded streams, embedded firmware and WebAssembly. Consumers need Rust 1.88 or later; Lean is needed only to reproduce the proofs.