def sj_big

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:361

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

361def sj_big(+l: U32, +h: U32, +k: Nat, +hk: {Nat.is_le(64n, k) == True{} : Bool}) -> {SW.value(WU.U64{X.b32(Bool.not(X.is_zero(WU.U64{l, h}))), 0}) == SW.jam(C.high(k, val(l, h)), C.low(k, val(l, h))) : Nat}:
362  +va = val(l, h)
363  +hf = fits_mono(64n, k, va, hk, fit64(l, h))
364  +eh = N.eq_from_is_eq(C.high(k, va), 0n, hf)
365  +el = WW.low_fit(k, va, hf)
366  +e1 = Equal.trans(Nat, SW.value(WU.U64{X.b32(Bool.not(X.is_zero(WU.U64{l, h}))), 0}), v(X.b32(Bool.not(X.is_zero(WU.U64{l, h})))), S.bit_value(Bool.not(X.is_zero(WU.U64{l, h}))), val0(X.b32(Bool.not(X.is_zero(WU.U64{l, h})))), W64M.b32_v(Bool.not(X.is_zero(WU.U64{l, h}))))
367  +e2 = Equal.cong(Bool, Nat, z => S.bit_value(Bool.not(z)), X.is_zero(WU.U64{l, h}), Nat.is_eq(va, 0n), WA.is_zero_value(WU.U64{l, h}))
368  +e3 = Equal.trans(Nat, SW.jam(0n, va), SW.jam(C.high(k, va), va), SW.jam(C.high(k, va), C.low(k, va)), Equal.cong(Nat, Nat, z => SW.jam(z, va), 0n, C.high(k, va), Equal.sym(Nat, C.high(k, va), 0n, eh)), Equal.cong(Nat, Nat, z => SW.jam(C.high(k, va), z), va, C.low(k, va), Equal.sym(Nat, C.low(k, va), va, el)))
369  Equal.trans(Nat, SW.value(WU.U64{X.b32(Bool.not(X.is_zero(WU.U64{l, h}))), 0}), S.bit_value(Bool.not(Nat.is_eq(va, 0n))), SW.jam(C.high(k, va), C.low(k, va)), Equal.trans(Nat, SW.value(WU.U64{X.b32(Bool.not(X.is_zero(WU.U64{l, h}))), 0}), S.bit_value(Bool.not(X.is_zero(WU.U64{l, h}))), S.bit_value(Bool.not(Nat.is_eq(va, 0n))), e1, e2), Equal.trans(Nat, S.bit_value(Bool.not(Nat.is_eq(va, 0n))), SW.jam(0n, va), SW.jam(C.high(k, va), C.low(k, va)), huge_n(va), e3))