package.bend source

package.bend on the hub · documented module

# bend-u64: package entry for BendHub.# Source: https://github.com/phenomenon0/bend-u64## 64-bit unsigned integers as one Word(64n), with U64.add_comm checked at 64# by instantiating Base's own generic inductive lemma Word.add_comm(64n, ...).# Pure Bend: no FFI, no intrinsics, no unsafe, no compiler change.# Boundaries: to_nat holds while <= 2^48-1; shl.n/shr.n are O(n) folds.import Baseimport ./u64.bend as U64def zero() -> U64.U64:  U64.zero()def one() -> U64.U64:  U64.one()def max() -> U64.U64:  U64.max()def add(a: U64.U64, b: U64.U64) -> U64.U64:  U64.add(a, b)def sub(a: U64.U64, b: U64.U64) -> U64.U64:  U64.sub(a, b)def mul(a: U64.U64, b: U64.U64) -> U64.U64:  U64.mul(a, b)def inc(a: U64.U64) -> U64.U64:  U64.inc(a)def and(a: U64.U64, b: U64.U64) -> U64.U64:  U64.and(a, b)def or(a: U64.U64, b: U64.U64) -> U64.U64:  U64.or(a, b)def xor(a: U64.U64, b: U64.U64) -> U64.U64:  U64.xor(a, b)def not(a: U64.U64) -> U64.U64:  U64.not(a)def shl(a: U64.U64) -> U64.U64:  U64.shl(a)def shr(a: U64.U64) -> U64.U64:  U64.shr(a)def shl_n(a: U64.U64, n: Nat) -> U64.U64:  U64.shl.n(n, a)def shr_n(a: U64.U64, n: Nat) -> U64.U64:  U64.shr.n(n, a)def cmp(a: U64.U64, b: U64.U64) -> Cmp:  U64.cmp(a, b)def is_eq(a: U64.U64, b: U64.U64) -> Bool:  U64.is_eq(a, b)def is_lt(a: U64.U64, b: U64.U64) -> Bool:  U64.is_lt(a, b)def is_gt(a: U64.U64, b: U64.U64) -> Bool:  U64.is_gt(a, b)def to_nat(a: U64.U64) -> Nat:  U64.to_nat(a)