u64.bend source
u64.bend on the hub · documented module
# 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.import Basetype U64 is Data: U64{data: Word(64n)}# -- constructors ------------------------------------------------------------def zero() -> U64: U64{Word.zero(64n)}def one() -> U64: U64{Word.inc(64n, Word.zero(64n))}def max() -> U64: U64{Word.not(64n, Word.zero(64n))}# -- arithmetic --------------------------------------------------------------def add(a: U64, b: U64) -> U64: match a b: case U64{x} U64{y}: U64{Word.add(64n, x, y)}def sub(a: U64, b: U64) -> U64: match a b: case U64{x} U64{y}: U64{Word.sub(64n, x, y)}def mul(a: U64, b: U64) -> U64: match a b: case U64{x} U64{y}: U64{Word.mul(64n, x, y)}def inc(a: U64) -> U64: match a: case U64{x}: U64{Word.inc(64n, x)}# -- logic -------------------------------------------------------------------def and(a: U64, b: U64) -> U64: match a b: case U64{x} U64{y}: U64{Word.and(64n, x, y)}def or(a: U64, b: U64) -> U64: match a b: case U64{x} U64{y}: U64{Word.or(64n, x, y)}def xor(a: U64, b: U64) -> U64: match a b: case U64{x} U64{y}: U64{Word.xor(64n, x, y)}def not(a: U64) -> U64: match a: case U64{x}: U64{Word.not(64n, x)}# -- shifts (bit-at-a-time; n-fold for the .n forms) -------------------------def shl(a: U64) -> U64: match a: case U64{x}: U64{Word.shl(64n, x)}def shr(a: U64) -> U64: match a: case U64{x}: U64{Word.shr(64n, x)}def shl.n(n: Nat, a: U64) -> U64: match n: case 0n: a case 1n+p: shl.n(p, shl(a))def shr.n(n: Nat, a: U64) -> U64: match n: case 0n: a case 1n+p: shr.n(p, shr(a))# -- comparison (word space; no Nat involved) --------------------------------def cmp.eq(c: Cmp) -> Bool: match c: case EQ{}: True{} case LT{}: False{} case GT{}: False{}def cmp.lt(c: Cmp) -> Bool: match c: case LT{}: True{} case EQ{}: False{} case GT{}: False{}def cmp.gt(c: Cmp) -> Bool: match c: case GT{}: True{} case EQ{}: False{} case LT{}: False{}def cmp(a: U64, b: U64) -> Cmp: match a b: case U64{x} U64{y}: Word.cmp(64n, x, y)def is_eq(a: U64, b: U64) -> Bool: cmp.eq(cmp(a, b))def is_lt(a: U64, b: U64) -> Bool: cmp.lt(cmp(a, b))def is_gt(a: U64, b: U64) -> Bool: cmp.gt(cmp(a, b))# -- Nat interop (valid while the value fits a Nat immediate, <= 2^48-1) -----def to_nat(a: U64) -> Nat: match a: case U64{x}: Word.to_nat(64n, x)# -- the law: width-64 instantiation of Base's generic lemma -----------------law add_comm: for a: U64 for b: U64 {add(a, b) == add(b, a) : U64}def add_comm(a, b): match a b: case U64{x} U64{y}: Equal.cong(Word(64n), U64, w => U64{w}, Word.add(64n, x, y), Word.add(64n, y, x), Word.add_comm(64n, x, y))