Sstable.u32_byte: def of mylsm-lsm-store@0.6.0.1
Import: import mylsm-lsm-store@0.6.0.1/src/Sstable.bend as Sstable
Lines 111-121 of mylsm-lsm-store@0.6.0.1/src/Sstable.bend: https://jend.leeeet.dev/read.txt?path=mylsm-lsm-store@0.6.0.1/src/Sstable.bend&start_line=111&end_line=121

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat