def mul

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/ed25519.bend:101

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

101# [k] a for a scalar below 2^256: 256 bits, written 2^8 one (one == 1), so
102# the proof checker never unrolls the loop
103def mul(+one: Nat, +p: Nat, +d: Nat, +k: Nat, +a: EPt) -> EPt:
104  smul(p, d, C.shift(8n, one), k, a, identity())