def u32_byte

mylsm-lsm-store@0.6.0.1 · src/Sstable.bend:111

import Base

111# --- U32->Nat bridges that stay checker-tractable ---
112# The Bend checker does not share across sequentially-chained U32.mul terms:
113# `U32.to_nat` applied to a hash accumulated over 4+ bytes diverges in
114# `{==}` elaboration (runtime is unaffected). The bridges below therefore
115# never materialize a chained U32 as a Nat: each `to_nat` covers at most two
116# U32 ops (shift+mask on the ORIGINAL word — parallel, shared), and all
117# accumulation happens in small-Nat land. Both are EXACT (no semantic
118# change): bytes are the base-256 digits of the word (Horner), so
119# u32_to_nat_exact(w) == U32.to_nat(w) and bhash_n computes the same mod.
120def u32_byte(+word: U32, shift: Nat) -> Nat:
121  U32.to_nat(U32.and(U32.shrn(word, shift), 255))