law z_len

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V

362law z_len:
363  for +r: List<&2, U32>
364  for +h: List<&2, U32>
365  for +c: List<&2, U32>
366  for +hhl: {Nat.is_le(V.len(h), 17n) == True{} : Bool}
367  for +hcl: {Nat.is_le(V.len(c), 17n) == True{} : Bool}
368  for +hrl: {V.len(r) == 16n : Nat}
369  {Nat.is_le(V.len(zz(r, h, c)), 33n) == True{} : Bool}