~/bend-docscommunity

padding_proof.bend checks

raw source on the hub · import 0x3bdc0c9f5265bb49f7fc76b61f529f24/padding_proof.bend as Padding_proof

2 imports
import Base
import ./fips.bend as F

Laws

law zeros_correct provedsource · line 6 · raw

@r:Nat -> {Nat.mod(Nat.sub(119n, r), 64n) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.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.