~/bend-docscommunity

proofs/crypto/sha/padding.bend checks

raw source on the hub · import 0xd9a2fae439ac7ff9e21e0853948f94fe/proofs/crypto/sha/padding.bend as Padding

2 imports
import Base
import ../../../spec/crypto/sha.bend as F

Laws

law zeros_correct provedsource · line 6 · raw

@r:Nat -> {Nat.mod(Nat.sub(119n, r), 64n) == 0xd9a2fae439ac7ff9e21e0853948f94fe/spec/crypto/sha.zero_count(r) : Nat}

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.