def u64_add_modular

bend-collections-laws-math@1.0.0.0 · proofs/math/proof.bend:43

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
import bend-collections-laws-math@1.0.0.0/spec/math/u64.bend as SU

43def u64_add_modular(+a: U.U64, +b: U.U64) -> SU.Add.modular(a, b):
44  Equal.trans(Word(64n), P.bits(U.add(a, b)), Word.add(64n, P.bits(a), P.bits(b)), S.from_nat(64n, Nat.add(S.unsigned(64n, P.bits(a)), S.unsigned(64n, P.bits(b)))), P.add(a, b), WA.refines(64n, P.bits(a), P.bits(b)))