~/bend-docscommunity

padding_proof.bend checks

raw source on the hub · import 0xda83506fb9f059ead7afcfa2f498df5f/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) == 0xda83506fb9f059ead7afcfa2f498df5f/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.