def eb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/pow.bend:64

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

64# the exponent of x contributed by the bits
65def eb(+one: Nat, bs: List<&2, Bool>) -> Nat:
66  match bs:
67    case Nil{}:
68      0n
69    case Con{b, +bt}:
70      Nat.add(Nat.mul(bexp(b), WD.sc(blen(bt), one)), eb(one, bt))