proofs/math/typed/w64add.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as W64add

21 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../lib/word.bend as WD
import ../../lib/u32.bend as U3
import ../../lib/lemmas/spec/numeric.bend as S
import ../u64/u64.bend as P64
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./width.bend as WW
import ./u32laws.bend as LW
import ../../lib/u32half.bend as UH
import ../u64/u64div.bend as PD
import ../../lib/u32alg.bend as A
import ../natural/arith.bend as NR
import ../../lib/arith.bend as AR2

Definitions

def v source · line 31 · raw

@+x:U32 -> Nat

def val source · line 34 · raw

@+l:U32 -> @+h:U32 -> Nat

def bv source · line 37 · raw

@c:Bool -> Nat

def vb source · line 40 · raw

@+x:U32 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, v(x)) == True{} : Bool}

def acons source · line 44 · raw

@+x:U32 -> @+y:U32 -> {Nat.add(v(U32.add(x, y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, bv(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(x, y)))) == Nat.add(v(x), v(y)) : Nat}

x + y == (x + y mod 2^32) + 2^32 carry

def add_alg source · line 49 · raw

@+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> @+l:Nat -> @+c1:Nat -> @+s:Nat -> @+c2:Nat -> @+h:Nat -> @+c3:Nat -> @+e1:{Nat.add(l, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, c1)) == Nat.add(al, bl) : Nat} -> @+e2:{Nat.add(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, c2)) == Nat.add(ah, bh) : Nat} -> @+e3:{Nat.add(h, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, c3)) == Nat.add(s, c1) : Nat} -> {Nat.add(Nat.add(al, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, ah)), Nat.add(bl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, bh))) == Nat.add(Nat.add(l, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, h)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.add(c3, c2)))) : Nat}

the limb sums: al + bl == l + 2^32 c1, ah + bh == s + 2^32 c2, s + c1 == h + 2^32 c3

def true_ne_false source · line 52 · raw

@+h:{True{} == False{} : Bool} -> Empty

def add_eq source · line 56 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> {Nat.add(Nat.add(v(al), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(ah))), Nat.add(v(bl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(bh)))) == Nat.add(Nat.add(v(U32.add(al, bl)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(U32.add(U32.add(ah, bh), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(U32.is_lt(U32.add(al, bl), al)))))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, Nat.add(bv(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(U32.add(ah, bh), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(U32.is_lt(U32.add(al, bl), al)))), bv(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(ah, bh))))) : Nat}

the full sum: the two limbs of the wrapped sum plus 2^64 (c3 + c2)

def add_value source · line 74 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Add.value(a, b)

def plus1 source · line 83 · raw

@+x:Nat -> {Nat.add(x, 1n) == 1n+x : Nat}

def acons_o source · line 87 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> {Nat.add(v(U32.add(x, y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(x, y), one))) == Nat.add(v(x), v(y)) : Nat}

x + y == (x + y mod 2^32) + 2^32 carry, the carry a bit worth one

def no_carry source · line 92 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:Nat -> @+c:Bool -> @+t:Nat -> @+e:{Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(c, one))) == t : Nat} -> @+ht:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, t) == True{} : Bool} -> {c == False{} : Bool}

no carry out of a sum that fits

def c_one source · line 100 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:Nat -> @+vs:Nat -> @+vm:Nat -> @+cc:Bool -> @+e:{Nat.add(r, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(cc, one))) == Nat.add(vs, 1n) : Nat} -> @+em:{1n+vm == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, one) : Nat} -> @+hr:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, r) == True{} : Bool} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, vs) == True{} : Bool} -> {cc == Nat.is_eq(vs, vm) : Bool}

s + 1 carries exactly when s is all ones (1 + vm == 2^32)

def c3_eq source · line 116 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:U32 -> @+c:Bool -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.b32(c)) == Bool.and(c, U32.is_eq(s, m)) : Bool}

the carry of s + b32(c) is c and s all ones

def aog source · line 126 · raw

@+s:U32 -> @+ah:U32 -> @c:Bool -> @+m:U32 -> Bool

def or_bits source · line 129 · raw

@+c2:Bool -> @+c3:Bool -> {Bool.or(c2, c3) == Bool.not(Nat.is_eq(Nat.add(bv(c3), bv(c2)), 0n)) : Bool}

def over_g source · line 140 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+m:U32 -> @+pm:{m == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.mask(32n, 32n)} : U32} -> {aog(U32.add(ah, bh), ah, U32.is_lt(U32.add(al, bl), al), m) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.add(Nat.add(v(al), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(ah))), Nat.add(v(bl), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(bh)))))) : Bool}

def add_over_value source · line 153 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.AddOver.value(a, b)

def iz_n source · line 160 · raw

@+x:Nat -> @+y:Nat -> {Bool.and(Nat.is_eq(x, 0n), Nat.is_eq(y, 0n)) == Nat.is_eq(Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, y)), 0n) : Bool}

def is_zero_value source · line 167 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.IsZero.value(a)

def eq_value source · line 174 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Eq.value(a, b)

def lt_value source · line 180 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Lt.value(a, b)

def nle source · line 192 · raw

@+a:Nat -> @+b:Nat -> @+c:Bool -> @+hc:{Nat.is_lt(a, b) == c : Bool} -> {Bool.not(c) == Nat.is_le(b, a) : Bool}

def le_value source · line 199 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Le.value(a, b)

def odd_value source · line 202 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Odd.value(a)

def chh source · line 209 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n) == 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/u32half.hlf(n) : Nat}

def half_div source · line 218 · raw

@+n:Nat -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.half(n) == Nat.div(n, 2n) : Nat}

def add_exact source · line 222 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, Nat.add(v(x), v(y))) == True{} : Bool} -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}

a sum that fits 32 bits: no wrap

def mul_le1 source · line 229 · raw

@+b:Nat -> @+x:Nat -> @+hb:{Nat.is_le(b, 1n) == True{} : Bool} -> {Nat.is_le(Nat.mul(b, x), x) == True{} : Bool}

def half_g source · line 238 · raw

@+l:U32 -> @+h:U32 -> @+c:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def halfval source · line 241 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+l:U32 -> @+h:U32 -> @+c:U32 -> @+pc:{c == U32{0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.pw(32n, 31n)} : U32} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(half_g(l, h, c)) == Nat.div(val(l, h), 2n) : Nat}

def half_value source · line 267 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Half.value(a)

def borrow_eq source · line 275 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+vx:Nat -> @+vs:Nat -> @+vy:Nat -> @+cc:Bool -> @+e:{Nat.add(vx, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(cc, one))) == Nat.add(vs, vy) : Nat} -> @+hs:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(32n, vs) == True{} : Bool} -> {cc == Nat.is_lt(vx, vy) : Bool}

x - y mod 2^32, plus y, is x plus 2^32 when x < y

def sub_cons source · line 287 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:U32 -> @+y:U32 -> {Nat.add(v(U32.sub(x, y)), v(y)) == Nat.add(v(x), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/lib/word.bo(U32.is_lt(x, y), one))) : Nat}

def sub_alg source · line 296 · raw

@+lo:Nat -> @+hi:Nat -> @+al:Nat -> @+ah:Nat -> @+bl:Nat -> @+bh:Nat -> @+s:Nat -> @+b1:Nat -> @+b2:Nat -> @+b3:Nat -> @+e1:{Nat.add(lo, bl) == Nat.add(al, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, b1)) : Nat} -> @+e2:{Nat.add(s, bh) == Nat.add(ah, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, b2)) : Nat} -> @+e3:{Nat.add(hi, b1) == Nat.add(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, b3)) : Nat} -> {Nat.add(Nat.add(lo, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, hi)), Nat.add(bl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, bh))) == Nat.add(Nat.add(al, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, ah)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.add(b2, b3)))) : Nat}

def sub_fin source · line 299 · raw

@+vs:Nat -> @+d:Nat -> @+q:Nat -> @+e:{vs == Nat.add(d, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(64n, q)) : Nat} -> @+hf:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, vs) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(q, 0n) == c : Bool} -> {vs == d : Nat}

def subval source · line 307 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+hle:{Nat.is_le(val(bl, bh), val(al, ah)) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.sub(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{al, ah}, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64{bl, bh})) == Nat.sub(val(al, ah), val(bl, bh)) : Nat}

def sub_value source · line 332 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:{Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(b), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(a)) == True{} : Bool} -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Sub.value(a, b, h)

def mcons source · line 339 · raw

@+x:U32 -> @+y:U32 -> {Nat.add(v(U32.mul(x, y)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64mul.mex(x, y))) == Nat.mul(v(x), v(y)) : Nat}

def cross_eq source · line 343 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> {Nat.add(v(U32.add(U32.mul(al, bh), U32.mul(ah, bl))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, Nat.add(bv(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/u64/u64.carry32(U32.mul(al, bh), U32.mul(ah, bl))), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64mul.mex(al, bh), 0xf86f5f1d9a594d5a5cff999100e01d03/proofs/math/typed/w64mul.mex(ah, bl))))) == Nat.add(Nat.mul(v(al), v(bh)), Nat.mul(v(ah), v(bl))) : Nat}

the cross terms: al bh + ah bl == t + 2^32 kc, t their wrapped sum

def mul_value source · line 355 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.Mul.value(a, b)

def mo_alg source · line 376 · raw

@+k:Nat -> @+A:Nat -> @+t1:Nat -> @+t2:Nat -> @+hh:Nat -> @+pl:Nat -> @+ph:Nat -> @+cl:Nat -> @+ch:Nat -> @+s:Nat -> @+cr:Nat -> @+ea:{A == Nat.add(pl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, ph)) : Nat} -> @+ec:{Nat.add(t2, t1) == Nat.add(cl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, ch)) : Nat} -> @+es:{Nat.add(s, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, cr)) == Nat.add(ph, cl) : Nat} -> @+eh:{hh == 0n : Nat} -> {Nat.add(Nat.add(A, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, t1)), Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, t2), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, hh)))) == Nat.add(Nat.add(pl, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, s)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, Nat.add(cr, ch)))) : Nat}

def val_eta source · line 379 · raw

@+p:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.value(p) == Nat.add(v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.lo(p)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.hi(p)))) : Nat}

def prod_fits source · line 384 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+hx:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, x) == True{} : Bool} -> @+hy:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), Nat.mul(x, y)) == True{} : Bool}

def le_hi source · line 388 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+hy:{Nat.is_le(1n, y) == True{} : Bool} -> {Nat.is_le(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.pow2(k), Nat.add(x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y))) == True{} : Bool}

def both_hi source · line 392 · raw

@+k:Nat -> @+x1:Nat -> @+y1:Nat -> @+x2:Nat -> @+y2:Nat -> @+hy1:{Nat.is_le(1n, y1) == True{} : Bool} -> @+hy2:{Nat.is_le(1n, y2) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(Nat.add(k, k), Nat.mul(Nat.add(x1, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y1)), Nat.add(x2, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(k, y2)))) == False{} : Bool}

def pos_ne source · line 400 · raw

@+n:Nat -> @+h:{Nat.is_eq(n, 0n) == False{} : Bool} -> {Nat.is_le(1n, n) == True{} : Bool}

def or_cr source · line 407 · raw

@+x:Nat -> @+c:Bool -> {Bool.or(Bool.not(Nat.is_eq(x, 0n)), c) == Bool.not(Nat.is_eq(Nat.add(bv(c), x), 0n)) : Bool}

def mo_core source · line 419 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+eh:{Nat.mul(v(ah), v(bh)) == 0n : Nat} -> @+hT:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.add(Nat.mul(v(ah), v(bl)), Nat.mul(v(al), v(bh)))) == True{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_over_one(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(al, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(ah, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(al, bh))) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))) : Bool}

with ah bh == 0 and the cross sum fitting 64 bits: the one-limb overflow test

def mo_top source · line 445 · raw

@+al:U32 -> @+ah:U32 -> @+bl:U32 -> @+bh:U32 -> @+z1:Bool -> @+z2:Bool -> @+hz1:{U32.is_zero(ah) == z1 : Bool} -> @+hz2:{U32.is_zero(bh) == z2 : Bool} -> {Bool.or(Bool.and(Bool.not(z1), Bool.not(z2)), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul_over_one(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(al, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(ah, bl), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.mul32(al, bh)))) == Bool.not(0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.fits(64n, Nat.mul(val(al, ah), val(bl, bh)))) : Bool}

def mul_over_value source · line 465 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/w64.MulOver.value(a, b)