law add_fits

lawful-bytes@0.1.1.0 · proof_core.bend:531

import Base

531# A sum of two words that stays within 4 * 2^d does not wrap.
532law add_fits:
533  for +a: U32
534  for +b: U32
535  for +d: Nat
536  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
537  for +h: {Nat.is_le(Nat.add(U32.to_nat(a), U32.to_nat(b)), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
538  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}