def tests_add_over

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/u32laws.bend:173

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/instances.bend as SI
import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-crypto@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as P64

173def tests_add_over(+a: U32, +b: U32) -> SI.Tests.add_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, a, b):
174  %Equal.sym(Bool, U32.is_lt(U32.add(a, b), a), P64.carry32(a, b), P64.add_lt(a, b)) : {_ == Bool.not(C.fits(32n, Nat.add(v(a), v(b)))) : Bool}
175  add_over_k(32n, {==}, a, b)