def wq.k

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:355

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

355def wq.k(+n: Nat, +m: Nat, +AL: Nat, +AH: Nat, +BL: Nat, +BH: Nat, +LO: Nat, +MH: Nat, +C1v: Nat, +C2v: Nat, +S1: Nat, +HI: Nat, +k1: Nat, +k2: Nat, +em: {Nat.add(n, n) == m : Nat}, +emh: {Nat.add(LO, U.U32Nat.dbl(n, MH)) == Nat.mul(AL, BL) : Nat}, +ec1: {Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH)))) == Nat.mul(AL, BH) : Nat}, +ec2: {Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))) == Nat.mul(AH, BL) : Nat}, +ea1: {Nat.add(S1, U.U32Nat.dbl(n, k1)) == Nat.add(MH, C1v) : Nat}, +ea2: {Nat.add(HI, U.U32Nat.dbl(n, k2)) == Nat.add(S1, C2v) : Nat}, +hLO: {Nat.is_lt(LO, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, +hHI: {Nat.is_lt(HI, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, U.U32Nat.high(m, Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH)))))) == Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH))) : Nat}:
356  +eE = Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.mul(AL, BH)), U.U32Nat.dbl(n, Nat.mul(AH, BL))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.mul(AL, BH)), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.mul(AL, BH)), U.U32Nat.dbl(n, Nat.mul(AH, BL))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH))))), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.mul(AL, BH)), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, MH)), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH))))), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH))))), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(MH, C1v), C2v))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, MH)), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH))))), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(S1, U.U32Nat.dbl(n, k1)), C2v))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(MH, C1v), C2v))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(S1, C2v), U.U32Nat.dbl(n, k1)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(S1, U.U32Nat.dbl(n, k1)), C2v))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(HI, U.U32Nat.dbl(n, k2)), U.U32Nat.dbl(n, k1)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(S1, C2v), U.U32Nat.dbl(n, k1)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH)))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(Nat.add(HI, U.U32Nat.dbl(n, k2)), U.U32Nat.dbl(n, k1)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), zz), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH)))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), wm.fn(n, m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))), em)), wr.m10(LO, n, HI, k1, k2, U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL)), AH, BH)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(zz, U.U32Nat.dbl(n, k1)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(HI, U.U32Nat.dbl(n, k2)), Nat.add(S1, C2v), ea2)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(LO, U.U32Nat.dbl(n, zz)), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(Nat.add(S1, C2v), U.U32Nat.dbl(n, k1)), Nat.add(Nat.add(S1, U.U32Nat.dbl(n, k1)), C2v), wr.m11(S1, C2v, n, k1))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(LO, U.U32Nat.dbl(n, Nat.add(zz, C2v))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(S1, U.U32Nat.dbl(n, k1)), Nat.add(MH, C1v), ea1)), wr.m12(LO, n, MH, C1v, C2v, U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL)), AH, BH)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH))))), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(LO, U.U32Nat.dbl(n, MH)), Nat.mul(AL, BL), emh)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, zz), U.U32Nat.dbl(n, Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))))), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(C1v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AL, BH)))), Nat.mul(AL, BH), ec1)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(AL, BL), Nat.add(Nat.add(U.U32Nat.dbl(n, Nat.mul(AL, BH)), U.U32Nat.dbl(n, zz)), U.U32Nat.dbl(n, U.U32Nat.dbl(n, Nat.mul(AH, BH))))), Nat.add(C2v, U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(AH, BL)))), Nat.mul(AH, BL), ec2)), wr.m13(AL, BL, n, BH, AH))
357  +eK = UL.high_unique(m, Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH))), Nat.add(LO, U.U32Nat.dbl(n, HI)), Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))), eE, Equal.trans(Bool, Nat.is_lt(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, 1n)), Nat.is_lt(Nat.add(LO, U.U32Nat.dbl(n, HI)), P.wv.Q(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(Nat.add(LO, U.U32Nat.dbl(n, HI)), zz), U.U32Nat.dbl(m, 1n), P.wv.Q(n, 1n), Equal.sym(Nat, P.wv.Q(n, 1n), U.U32Nat.dbl(m, 1n), Equal.sym(Nat, U.U32Nat.dbl(m, 1n), U.U32Nat.dbl(n, U.U32Nat.dbl(n, 1n)), wm.fn(n, m, 1n, em)))), P.wv.val_lt2(n, LO, HI, hLO, hHI)))
358  Equal.trans(Nat, Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, U.U32Nat.high(m, Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH)))))), Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))))), Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(LO, U.U32Nat.dbl(n, HI)), U.U32Nat.dbl(m, zz)), U.U32Nat.high(m, Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH)))), Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))), Equal.sym(Nat, Nat.add(Nat.add(k1, k2), Nat.add(Nat.add(U.U32Nat.high(n, Nat.mul(AL, BH)), U.U32Nat.high(n, Nat.mul(AH, BL))), Nat.mul(AH, BH))), U.U32Nat.high(m, Nat.mul(Nat.add(AL, U.U32Nat.dbl(n, AH)), Nat.add(BL, U.U32Nat.dbl(n, BH)))), eK)), eE)