law mac_poly

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

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

68# Hence the tag: ((poly(blocks, r) mod p) + s) mod 2^128, as 16 little-endian
69# bytes, with r the clamped first half of the key and s the second half.
70law mac_poly:
71  for +one: Nat
72  for +h1: {one == 1n : Nat}
73  for +key: List<&2, U32>
74  for +msg: List<&2, U32>
75  {R.poly1305_mac(key, msg) == R.le_bytes(16n, Nat.add(Nat.mod(R.poly(R.blocks(List.length(&2, U32, msg), msg), R.le_num(R.clamp(R.prefix(16n, key)))), Nat.sub(C.shift(130n, one), 5n)), R.le_num(R.prefix(16n, R.suffix(16n, key))))) : List<&2, U32>}