law poly1305_invalid

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

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

37law poly1305_invalid:
38  for +key: List<&2, U32>
39  for +msg: List<&2, U32>
40  for +h: {Nat.is_eq(List.length(&2, U32, key), 32n) == False{} : Bool}
41  {P.poly1305(key, msg) == None{} : Maybe<&2, List<&2, U32>>}