law align

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1134

import Base

1134# dst's length after the first h0 bytes is a multiple of 4.
1135law align:
1136  for +ld: U32
1137  {Nat.mul(Nat.div(Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))), 4n), 4n) == Nat.add(U32.to_nat(ld), U32.to_nat(H0(ld))) : Nat}