law zeros_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/padding.bend:4

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

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