def o48_split

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

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/math/typed/w64div.bend as W64D
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natlight.bend as SR
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

173# g = (2^16 r2 + r1) + 2^32 h: r1, r2 the low 16-bit digits, h = g div 2^32
174def o48_split(+one: Nat, +h1: {one == 1n : Nat}, +g: Nat) -> {Nat.add(Nat.add(C.shift(16n, Nat.mod(Nat.div(g, 65536n), 65536n)), Nat.mod(g, 65536n)), C.shift(32n, Nat.div(Nat.div(g, 65536n), 65536n))) == g : Nat}:
175  +q1 = Nat.div(g, 65536n)
176  +r1 = Nat.mod(g, 65536n)
177  +h = Nat.div(q1, 65536n)
178  +r2 = Nat.mod(q1, 65536n)
179  +X1 = Nat.add(Nat.mul(Nat.add(Nat.mul(h, 65536n), r2), 65536n), r1)
180  +e1 = Equal.trans(Nat, X1, Nat.add(Nat.mul(q1, 65536n), r1), g, Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, 65536n), r1), Nat.add(Nat.mul(h, 65536n), r2), q1, SR.dmq(q1, 65536n, {==})), SR.dmq(g, 65536n, {==}))
181  +e2 = Equal.trans(Nat, Nat.add(Nat.add(WD.sc(16n, r2), r1), WD.sc(32n, h)), X1, g, Equal.sym(Nat, X1, Nat.add(Nat.add(WD.sc(16n, r2), r1), WD.sc(32n, h)), W64D.x2_eq(one, h1, h, r2, r1)), e1)
182  +e3 = Equal.trans(Nat, Nat.add(Nat.add(C.shift(16n, r2), r1), C.shift(32n, h)), Nat.add(Nat.add(WD.sc(16n, r2), r1), C.shift(32n, h)), Nat.add(Nat.add(WD.sc(16n, r2), r1), WD.sc(32n, h)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, r1), C.shift(32n, h)), C.shift(16n, r2), WD.sc(16n, r2), W64M.shift_sc(16n, r2)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(WD.sc(16n, r2), r1), z), C.shift(32n, h), WD.sc(32n, h), W64M.shift_sc(32n, h)))
183  Equal.trans(Nat, Nat.add(Nat.add(C.shift(16n, r2), r1), C.shift(32n, h)), Nat.add(Nat.add(WD.sc(16n, r2), r1), WD.sc(32n, h)), g, e3, e2)