def mac

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/poly1305.bend:120

import 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)