~/bend-docscommunity

proofs/lib/lemmas/src/wide.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide

2 imports
import Base
import ../../../../spec/lib/numeric.bend as NM

Types

type Division source · line 58 · raw

@-n:Nat -> Data

type Parts source · line 107 · raw

@-n:Nat -> @-m:Nat -> Data

Definitions

def zero source · line 5 · raw

Word(64n)

All bits are represented explicitly: no Nat holds a full-width integer.

def inc source · line 8 · raw

@w:Word(64n) -> Word(64n)

def add source · line 11 · raw

@a:Word(64n) -> @b:Word(64n) -> Word(64n)

def neg source · line 14 · raw

@w:Word(64n) -> Word(64n)

def last source · line 17 · raw

@n:Nat -> @w:Word(n) -> Bool

def is_zero source · line 30 · raw

@n:Nat -> @w:Word(n) -> Bool

def signed_order source · line 39 · raw

@a:Word(64n) -> @b:Word(64n) -> @sa:Bool -> @sb:Bool -> Bool

def le source · line 48 · raw

@+a:Word(64n) -> @+b:Word(64n) -> Bool

def bit_u32 source · line 51 · raw

@b:Bool -> U32

def digit_result source · line 61 · raw

@p:Nat -> @q:Word(p) -> @r:U32 -> @subtract:Bool -> Division<1n+p>

def digit_compare source · line 68 · raw

@p:Nat -> @q:Word(p) -> @+r:U32 -> Division<1n+p>

def digit source · line 71 · raw

@p:Nat -> @b:Bool -> @prior:Division<p> -> Division<1n+p>

def div_million source · line 77 · raw

@+n:Nat -> @w:Word(n) -> Division<n>

Binary long division, processing the most significant bit first. The partial remainder stays below 1,000,000; the next candidate fits in U32 (<2,000,000).

def quotient source · line 86 · raw

@r:Division<64n> -> Word(64n)

def unsigned_milliseconds source · line 90 · raw

@w:Word(64n) -> Word(64n)

def signed_milliseconds source · line 93 · raw

@w:Word(64n) -> @negative:Bool -> Word(64n)

def milliseconds source · line 100 · raw

@+w:Word(64n) -> Word(64n)

def join source · line 104 · raw

@n:Nat -> @+m:Nat -> @a:Word(n) -> @b:Word(m) -> Word(Nat.add(n, m))

Exact limb boundary used by the host bridge; limbs themselves are primitive U32.

def split_cons source · line 110 · raw

@-n:Nat -> @-m:Nat -> @h:Bool -> @parts:Parts<n, m> -> Parts<1n+n, m>

def split source · line 114 · raw

@n:Nat -> @+m:Nat -> @w:Word(Nat.add(n, m)) -> Parts<n, m>

def pack source · line 123 · raw

@low:U32 -> @high:U32 -> Word(64n)

def limbs source · line 126 · raw

@parts:Parts<32n, 32n> -> Pair(U32, U32)

def unpack source · line 130 · raw

@w:Word(64n) -> Pair(U32, U32)