Mac.le_bytes_len: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as Mac
Lines 355-358 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend&start_line=355&end_line=358

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

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

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend&name=le_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=high