def shift

bend-collections-laws-crypto@1.0.0.0 · spec/lib/common.bend:14

import Base

14# Widths without powers: x * 2^k, n div 2^k and n mod 2^k by k doublings or
15# halvings, and "n fits k bits". A literal 2^32 or 2^64 is beyond what the
16# proof checker expands, so the fixed-width specifications (spec/math/generic,
17# instances, w64) state widths through these; for a symbolic k they equal the
18# pow2 forms (proofs/math/typed/width.bend).
19def shift(k: Nat, +x: Nat) -> Nat:
20  match k:
21    case 0n:
22      x
23    case 1n+p:
24      Nat.double(shift(p, x))