PROOF.msb_split: def of bend-osdev-crc@0.1.0.0
Import: import bend-osdev-crc@0.1.0.0/PROOF.bend as PROOF
Lines 47-53 of bend-osdev-crc@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crc@0.1.0.0/PROOF.bend&start_line=47&end_line=53

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crc@0.1.0.0/crc.bend as C

# most significant bit first: either engine splits
def msb_split(+small: Bool, +width: Nat, +poly: U32, c: U32, xs: List<&2, U32>, ys: List<&2, U32>) -> {C.Crc32Spec.update.msb(small, width, poly, c, B.append(xs, ys)) == C.Crc32Spec.update.msb(small, width, poly, C.Crc32Spec.update.msb(small, width, poly, c, xs), ys) : U32}:
  match small:
    case True{}:
      s32_split(xs, poly, Nat.sub(width, 1n), U32.sub(U32.shln(1, width), 1), c, ys)
    case False{}:
      n32_split(xs, poly, Nat.sub(width, 8n), U32.shln(1, Nat.sub(width, 1n)), U32.sub(U32.shln(1, width), 1), c, ys)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crc@0.1.0.0/PROOF.bend&name=n32_split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crc@0.1.0.0/PROOF.bend&name=s32_split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crc@0.1.0.0/crc.bend&name=Crc32Spec.update.msb