def ev

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:24

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

24def ev(xs: List<&2, U32>) -> Nat:
25  match xs:
26    case Nil{}: 0n
27    case x <> t: Nat.add(v(x), C.shift(8n, ev(t)))