law le_bytes_len

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

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

355law le_bytes_len:
356  for +n: Nat
357  for +x: Nat
358  {List.length(&2, U32, R.le_bytes(n, x)) == n : Nat}