bendtorch

Releases (6)

• 1.3.0.0 indexed
• 1.2.0.0 unindexed
• 1.1.1.0 unindexed
• 1.1.0.0 unindexed
• 1.0.1.0 unindexed
• 1.0.0.0 unindexed

Definitions (1,049)

dtype.bend

• def u2fU32 and F32 hold the same Word(32n)
• def f2u
• def pick_u
• def bf16_rneF32 -> BF16, round to nearest even: add 0x7FFF plus the lowest kept bit, keep the top half.
• def bf16_of_bits
• def BF16.of_f32
• def BF16.to_f32BF16 -> F32 is exact: the 16 bits become the top half
• def BF16.roundx rounded to the nearest BF16 value, as an F32 (x.to(torch.bfloat16).to(torch.float32))
• def f16_normala normal F16 (|x| >= 2^-14): rebias the exponent (127 - 15 = 112), round the 23-bit mantissa to 10 bits to nearest even; past 65504 the carry reaches the infinity pattern 0x7C00 and anything above it is infinity too
• def f16_sub2a subnormal F16 (2^-25 < |x| < 2^-14): the value in units of 2^-24 is mant / 2^sh, sh = 126 - e in 14..24, rounded to nearest even; a result of 0x400 is the smallest normal, which is the right answer
• def f16_sub
• def f16_nana NaN keeps the top 9 bits of its payload and gets the quiet bit
• def f16_mag
• def f16_of_bitsF32 -> F16, round to nearest even, with the sign kept (so -0.0 and the negative tiny numbers give 0x8000)
• def F16.of_f32
• def f16_upF16 -> F32, exact.
• def F16.to_f32
• def F16.round
• def half_join
• def half_lo
• def half_hi
• type HWa pair of 16-bit values, the unit of storage
• def pairsthe values two by two; an odd last one is paired with 0
• def unpairsevery value of a list of pairs, in order
• def unpairs_nthe first n of them: the padding of an odd count is left out
• type HMat
• type UL
• def fill_u
• def read_uthe k + 1 values from index i, in order (ra holds the array and the value at i, already read)
• def ul_list
• def enc_l
• def dec_l
• def join_l
• def split_l
• def hwordsthe number of words for n halves
• def ml_l
• def Half.wordsthe values of a 16-bit list packed two per word
• def Half.valuesthe first n 16-bit values of a packed array
• def Half.packa matrix encoded by f (BF16.of_f32 or F16.of_f32) and packed
• def Half.unpacka packed matrix decoded by g (BF16.to_f32 or F16.to_f32) into F32
• def BF16.pack
• def BF16.unpack
• def F16.pack
• def F16.unpack
• def HMat.wordsthe words of a packed matrix, for printing and tests
• def unpair_pairLAW (unpair_pair): packing a list two by two and reading back as many values as it had gives the list back, in order, for any length (an odd last value is paired with a 0 that the read leaves out).
• type Q8
• def pick_f
• def rne_fv rounded to the nearest integer, ties to even (torch.round), for |v| < 2^23 (here |v| <= 127 and a bit)
• def q8_of
• def q8_bytean integer -127..127 (as an F32) to its two's complement byte, and back
• def q8_val
• def amax_l
• def q8_row
• type QR
• def qr_add
• def q8_rowsthe rows of a flat list of k rows of c, from the last one: each row's bytes and scale
• def quadsfour bytes to a word, little-endian; a short last group is padded with zeros

PROOF.bend

• def b_m0cdepth 0: the two leaves' loops, appended
• def b_m0b
• def b_m0a
• def b_m1cdepth 1 + e: each half cut in two and its b_tree (the closures run main at depth e), then the two maps appended
• def b_m1b
• def b_m1a
• def b_tree
• def b_par_finthe law: the b_tree gives what fleaf, the loop over the sequences one after another, gives
• def b_par_mid
• def b_ffmap
• type b_L1RF
• def b_lf_con
• def b_lf1
• type b_MARF
• def b_ma_conf
• def b_map_appf
• type b_MRF
• def b_fm0cdepth 0: the two leaves' loops, appended
• def b_fm0b
• def b_fm0a
• def b_fm1cdepth 1 + e: each half cut in two and its b_treef (the closures run main at depth e), then the two maps appended
• def b_fm1b
• def b_fm1a
• def b_treef
• def b_par_fin_fthe law: the b_treef gives what fleaf, the loop over the sequences one after another, gives
• def b_par_mid_f
• def div_blockone block of 1 + m numbers adds 1 to the quotient (Nat.divmod.go counts down the remainder from m)
• def div_blocksj whole blocks of 1 + s numbers add j to the quotient
• def div_restfewer than 1 + s numbers after the last whole block leave the quotient alone
• def or_comma || b == b || a, and a && b == b && a: every case computes
• def and_comm
• def and_congequal operands give equal conjunctions and disjunctions
• def or_cong
• def bc_dim_symone axis: bc_dim is written as pair(x, y) || pair(y, x), so swapping x and y only swaps the two sides of the ||
• def bc_eq_symaxis by axis: the same on each axis (bc_dim_sym), and by induction on the rest; shapes of different ranks are False either way round
• def bc_rank_symthe ranks: the same two comparisons and the same two equalities, in the other order
• def mul_swaph * (a * r) == a * (h * r): associativity, then commutativity of the first two factors, then associativity back
• def pass_pairone pass over 2k blocks of 2^p cells gives the k blocks of 2^(p+1) cells: the pass adds blocks 2j and 2j+1, the two halves bal puts under one node.
• def cnt22^(p+1) · k cells are 2^p · 2k: (a + a)·k == a·k + a·k == a·(k + k)
• def blocks_passesthe first p passes over a row of 2^p · k cells leave its k blocks, each summed as bal sums it.
• def passes_addr + p passes are p passes, then r more
• def main