u64.bend checks
raw source on the hub · import 0x464866dd0fbd191e9b4adc04f0fb781f/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.
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 140 · raw
@a:U64 -> @b:U64 -> {add(a, b) == add(b, a) : U64}
Types
type U64 source · line 17 · raw
Data
U64@data:Word(64n) -> U64
Definitions
def zero source · line 22 · raw
U64
def one source · line 25 · raw
U64
def max source · line 28 · raw
U64
def add source · line 33 · raw
@a:U64 -> @b:U64 -> U64
def sub source · line 38 · raw
@a:U64 -> @b:U64 -> U64
def mul source · line 43 · raw
@a:U64 -> @b:U64 -> U64
def inc source · line 48 · raw
@a:U64 -> U64
def and source · line 55 · raw
@a:U64 -> @b:U64 -> U64
def or source · line 60 · raw
@a:U64 -> @b:U64 -> U64
def xor source · line 65 · raw
@a:U64 -> @b:U64 -> U64
def not source · line 70 · raw
@a:U64 -> U64
def shl source · line 77 · raw
@a:U64 -> U64
def shr source · line 82 · raw
@a:U64 -> U64
def shl.n source · line 87 · raw
@n:Nat -> @a:U64 -> U64
def shr.n source · line 92 · raw
@n:Nat -> @a:U64 -> U64
def cmp.eq source · line 99 · raw
@c:Cmp -> Bool
def cmp.lt source · line 105 · raw
@c:Cmp -> Bool
def cmp.gt source · line 111 · raw
@c:Cmp -> Bool
def cmp source · line 117 · raw
@a:U64 -> @b:U64 -> Cmp
def is_eq source · line 122 · raw
@a:U64 -> @b:U64 -> Bool
def is_lt source · line 125 · raw
@a:U64 -> @b:U64 -> Bool
def is_gt source · line 128 · raw
@a:U64 -> @b:U64 -> Bool
def to_nat source · line 133 · raw
@a:U64 -> Nat