def fin

bend-collections@1.0.0.0 · src/crypto/poly1305/limbs.bend:122

import Base

122# The tag bytes: the low 128 bits of (h mod p) + s. (Entered through a match
123# on s, both arms the same: while s is unknown a proof's goal stays one call
124# instead of sixteen unfolded byte steps.)
125def fin(+h: List<&2, U32>, s: List<&2, U32>) -> List<&2, U32>:
126  match s:
127    case Nil{}: bytes(16n, add(freeze(h), Nil{}), 0)
128    case y <> ys: bytes(16n, add(freeze(h), y <> ys), 0)