def mul64

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/conformance.bend:606

import Base

606# Byte counts of whole blocks: 64 * k, built the way stream accumulates them.
607def mul64(k: Nat) -> Nat:
608  match k:
609    case 0n:
610      0n
611    case 1n+p:
612      Nat.add(64n, mul64(p))