def msb_split

bend-osdev-crc@0.1.0.0 · PROOF.bend:47

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

47# most significant bit first: either engine splits
48def 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}:
49  match small:
50    case True{}:
51      s32_split(xs, poly, Nat.sub(width, 1n), U32.sub(U32.shln(1, width), 1), c, ys)
52    case False{}:
53      n32_split(xs, poly, Nat.sub(width, 8n), U32.shln(1, Nat.sub(width, 1n)), U32.sub(U32.shln(1, width), 1), c, ys)