def mac
import bend-collections@1.0.0.0/spec/crypto/poly1305.bend as Poly1305import Base
120# The same function, split on the message first so that a proof about an
121# unknown message does not unfold it.
122def mac(+key: List<&2, U32>, +msg: List<&2, U32>) -> List<&2, U32>:
123 match msg:
124 case Nil{}: poly1305_mac(key, [])
125 case b <> rest: poly1305_mac(key, b <> rest)