def add64_exact

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64m128.bend:64

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/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

64# a 64-bit sum that fits: no wrap
65def add64_exact(+p: WU.U64, +q: WU.U64, +hf: {C.fits(64n, Nat.add(SW.value(p), SW.value(q))) == True{} : Bool}) -> {SW.value(X.add(p, q)) == Nat.add(SW.value(p), SW.value(q)) : Nat}:
66  av = WA.add_value(p, q)
67  Equal.trans(Nat, SW.value(X.add(p, q)), C.low(64n, Nat.add(SW.value(p), SW.value(q))), Nat.add(SW.value(p), SW.value(q)), av, WW.low_fit(64n, Nat.add(SW.value(p), SW.value(q)), hf))