u64.bend checks
raw source on the hub · import 0x0f1da4e80677f1d50e6f638a7d6f27ef/u64.bend as U64
bend-u64: a 64-bit unsigned integer in pure Bend, backed by one 64-bit word. Source: https://github.com/phenomenon0/bend-u64
No compiler change is involved: the runtime word is 64-bit (u64), Word(64n)
is a Base builtin, and U64 is a plain wrapper in the same shape as Base's own
F64. All operations are width-64 instantiations of Base's width-generic
Word.* layer. The commutation law is instantiated from Base's own generic
inductive lemma Word.add_comm(64n, ...) — the same theorem U32 uses at 32.
Speed: every operation walks the generic Word(64n) layer, so on hot loops expect reference-grade times (bench: ~10^2-10^3x a native 64-bit control; numbers in the repo README). A native word-64 lowering turns the SAME semantics into machine-speed ops — merged in the omen fork, proposed upstream. Intended today for cold paths: IDs, occasional math, proofs.
Boundaries, stated honestly:
- to_nat is valid while the value fits a Nat immediate (<= 2^48-1);
wider values are legal U64s and compare in word space (cmp/is_*).
- shl.n/shr.n are bit-at-a-time folds (n small); they are O(n).
- No FFI, no intrinsics, no unsafe; checked on stock Bend 2.0.17.
1 import
import Base
Laws
law add_comm provedsource · line 146 · raw
@a:U64 -> @b:U64 -> {add(a, b) == add(b, a) : U64}
Types
type U64 source · line 23 · raw
Data
U64@data:Word(64n) -> U64
Definitions
def zero source · line 28 · raw
U64
def one source · line 31 · raw
U64
def max source · line 34 · raw
U64
def add source · line 39 · raw
@a:U64 -> @b:U64 -> U64
def sub source · line 44 · raw
@a:U64 -> @b:U64 -> U64
def mul source · line 49 · raw
@a:U64 -> @b:U64 -> U64
def inc source · line 54 · raw
@a:U64 -> U64
def and source · line 61 · raw
@a:U64 -> @b:U64 -> U64
def or source · line 66 · raw
@a:U64 -> @b:U64 -> U64
def xor source · line 71 · raw
@a:U64 -> @b:U64 -> U64
def not source · line 76 · raw
@a:U64 -> U64
def shl source · line 83 · raw
@a:U64 -> U64
def shr source · line 88 · raw
@a:U64 -> U64
def shl.n source · line 93 · raw
@n:Nat -> @a:U64 -> U64
def shr.n source · line 98 · raw
@n:Nat -> @a:U64 -> U64
def cmp.eq source · line 105 · raw
@c:Cmp -> Bool
def cmp.lt source · line 111 · raw
@c:Cmp -> Bool
def cmp.gt source · line 117 · raw
@c:Cmp -> Bool
def cmp source · line 123 · raw
@a:U64 -> @b:U64 -> Cmp
def is_eq source · line 128 · raw
@a:U64 -> @b:U64 -> Bool
def is_lt source · line 131 · raw
@a:U64 -> @b:U64 -> Bool
def is_gt source · line 134 · raw
@a:U64 -> @b:U64 -> Bool
def to_nat source · line 139 · raw
@a:U64 -> Nat