def blocks
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as Poly1305import Base
97# The message cut into 16-byte blocks, the last one possibly shorter; fuel
98# bounds the number of blocks (the length of the message is enough).
99def blocks(fuel: Nat, +msg: List<&2, U32>) -> List<&2, List<&2, U32>>:
100 match fuel msg:
101 case 0n _: Nil{}
102 case 1n+k Nil{}: Nil{}
103 case 1n+k b <> rest: prefix(16n, b <> rest) <> blocks(k, suffix(16n, b <> rest))
Uses (5)
Used by (5)
- bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305:poly1305_mac
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac:mac_length
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac:absorb_ok
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac:tag_main
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws:mac_poly