def add_exact

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64add.bend:221

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

221# a sum that fits 32 bits: no wrap
222def add_exact(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32, +hf: {C.fits(32n, Nat.add(v(x), v(y))) == True{} : Bool}) -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}:
223  +cc = P64.carry32(x, y)
224  +e = acons_o(one, h1, x, y)
225  +nc = no_carry(one, h1, v(U32.add(x, y)), cc, Nat.add(v(x), v(y)), e, hf)
226  +e0 = L.subst(Bool, t => {Nat.add(v(U32.add(x, y)), C.shift(32n, WD.bo(t, one))) == Nat.add(v(x), v(y)) : Nat}, cc, False{}, nc, e)
227  Equal.trans(Nat, v(U32.add(x, y)), Nat.add(v(U32.add(x, y)), C.shift(32n, 0n)), Nat.add(v(x), v(y)), Equal.sym(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, 0n)), v(U32.add(x, y)), Equal.trans(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, 0n)), Nat.add(v(U32.add(x, y)), 0n), v(U32.add(x, y)), Equal.cong(Nat, Nat, t => Nat.add(v(U32.add(x, y)), t), C.shift(32n, 0n), 0n, WW.shift_zero(32n)), N.add_zero(v(U32.add(x, y))))), e0)