Padding.zeros_correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/padding.bend as Padding
Lines 4-8 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/padding.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/padding.bend&start_line=4&end_line=8

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as F

# Universal bridge from implementation modular padding to the FIPS piecewise rule.
# Every Nat is either one of 0..119 or 120+p. Each branch closes by reduction.
law zeros_correct:
  for r: Nat
  {Nat.mod(Nat.sub(119n, r), 64n) == F.zero_count(r) : Nat}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend&name=zero_count