def ws.ov

bend-osdev-word64@0.1.1.0 · proof_shift.bend:244

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

244# the bits ws.shl(n, k, w) carries out, as a number
245def ws.ov(+n: Nat, k: Nat, +w: Word(n)) -> Nat:
246  match k:
247    case 0n:
248      0n
249    case 1n+ +p:
250      Nat.add(U.U32Nat.bit(ws.top(n, ws.shl(n, p, w))), Nat.double(ws.ov(n, p, w)))