def over_g

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

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/src/math/w64.bend as X
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

140def over_g(+one: Nat, +h1: {one == 1n : Nat}, +al: U32, +ah: U32, +bl: U32, +bh: U32, +m: U32, +pm: {m == U32{WD.mask(32n, 32n)} : U32}) -> {aog(U32.add(ah, bh), ah, U32.is_lt(U32.add(al, bl), al), m) == Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))) : Bool}:
141  +s = U32.add(ah, bh)
142  +c1b = U32.is_lt(U32.add(al, bl), al)
143  +q2 = P64.carry32(ah, bh)
144  +q3 = P64.carry32(s, X.b32(c1b))
145  +R = Nat.add(v(U32.add(al, bl)), C.shift(32n, v(U32.add(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al))))))
146  +q = Nat.add(bv(P64.carry32(U32.add(ah, bh), X.b32(U32.is_lt(U32.add(al, bl), al)))), bv(P64.carry32(ah, bh)))
147  +hR = WW.limbs_fit(32n, 32n, v(U32.add(al, bl)), v(U32.add(s, X.b32(c1b))), vb(U32.add(al, bl)), vb(U32.add(s, X.b32(c1b))))
148  +ea = Equal.trans(Bool, aog(s, ah, c1b, m), Bool.or(q2, Bool.and(c1b, U32.is_eq(s, m))), Bool.or(q2, q3), Equal.cong(Bool, Bool, t => Bool.or(t, Bool.and(c1b, U32.is_eq(s, m))), U32.is_lt(s, ah), q2, P64.add_lt(ah, bh)), Equal.cong(Bool, Bool, t => Bool.or(q2, t), Bool.and(c1b, U32.is_eq(s, m)), q3, Equal.sym(Bool, q3, Bool.and(c1b, U32.is_eq(s, m)), c3_eq(one, h1, s, c1b, m, pm))))
149  +eb = Equal.trans(Nat, C.high(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), C.high(64n, Nat.add(R, C.shift(64n, q))), q, Equal.cong(Nat, Nat, t => C.high(64n, t), Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))), Nat.add(R, C.shift(64n, q)), add_eq(al, ah, bl, bh)), WW.high_u(64n, R, q, hR))
150  +ec = Equal.cong(Nat, Bool, t => Bool.not(Nat.is_eq(t, 0n)), C.high(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh))))), q, eb)
151  Equal.trans(Bool, aog(s, ah, c1b, m), Bool.or(q2, q3), Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))), ea, Equal.trans(Bool, Bool.or(q2, q3), Bool.not(Nat.is_eq(q, 0n)), Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))), or_bits(q2, q3), Equal.sym(Bool, Bool.not(C.fits(64n, Nat.add(Nat.add(v(al), C.shift(32n, v(ah))), Nat.add(v(bl), C.shift(32n, v(bh)))))), Bool.not(Nat.is_eq(q, 0n)), ec)))