law poly1305_valid

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R

30# The checked API: the tag for a 32-byte key, None for any other length.
31law poly1305_valid:
32  for +key: List<&2, U32>
33  for +msg: List<&2, U32>
34  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == True{} : Bool}
35  {P.poly1305(key, msg) == Some{R.mac(key, msg)} : Maybe<&2, List<&2, U32>>}