def sj_c

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

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/lemmas/proofs/nat_algebra.bend as NA
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

384def sj_c(+l: U32, +h: U32, +k: Nat, +ln: Nat, +hL: {C.low(k, val(l, h)) == ln : Nat}, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {SW.value(X.or_bit(X.shr(WU.U64{l, h}, k), Bool.not(X.eq(X.shl(X.shr(WU.U64{l, h}, k), k), WU.U64{l, h})))) == SW.jam(C.high(k, val(l, h)), C.low(k, val(l, h))) : Nat}:
385  match ln:
386    case 0n:
387      +S1 = X.shr(WU.U64{l, h}, k)
388      +q = C.high(k, val(l, h))
389      +hb = Equal.trans(Bool, Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})), Bool.not(Nat.is_eq(C.low(k, val(l, h)), 0n)), False{}, sj_bit(l, h, k, hk), Equal.cong(Nat, Bool, z => Bool.not(Nat.is_eq(z, 0n)), C.low(k, val(l, h)), 0n, hL))
390      +e1 = Equal.cong(Bool, Nat, z => SW.value(X.or_bit(S1, z)), Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})), False{}, hb)
391      +e2 = Equal.trans(Nat, SW.value(X.or_bit(S1, False{})), SW.value(WU.U64{X.lo(S1), X.hi(S1)}), q, Equal.cong(U32, Nat, z => SW.value(WU.U64{z, X.hi(S1)}), U32.or(X.lo(S1), 0), X.lo(S1), or0(X.lo(S1))), Equal.trans(Nat, SW.value(WU.U64{X.lo(S1), X.hi(S1)}), SW.value(S1), q, Equal.sym(Nat, SW.value(S1), SW.value(WU.U64{X.lo(S1), X.hi(S1)}), WA.val_eta(S1)), shr_value(WU.U64{l, h}, k)))
392      +e3 = Equal.trans(Nat, SW.jam(q, C.low(k, val(l, h))), SW.jam(q, 0n), q, Equal.cong(Nat, Nat, z => SW.jam(q, z), C.low(k, val(l, h)), 0n, hL), jam0_m(q, Nat.mod(q, 2n), {==}, mod2_lt(q)))
393      Equal.trans(Nat, SW.value(X.or_bit(S1, Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})))), q, SW.jam(q, C.low(k, val(l, h))), Equal.trans(Nat, SW.value(X.or_bit(S1, Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})))), SW.value(X.or_bit(S1, False{})), q, e1, e2), Equal.sym(Nat, SW.jam(q, C.low(k, val(l, h))), q, e3))
394    case 1n+ +lp:
395      +S1 = X.shr(WU.U64{l, h}, k)
396      +q = C.high(k, val(l, h))
397      +vl = v(X.lo(S1))
398      +vh = v(X.hi(S1))
399      +hb = Equal.trans(Bool, Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})), Bool.not(Nat.is_eq(C.low(k, val(l, h)), 0n)), True{}, sj_bit(l, h, k, hk), Equal.cong(Nat, Bool, z => Bool.not(Nat.is_eq(z, 0n)), C.low(k, val(l, h)), 1n+lp, hL))
400      +e1 = Equal.cong(Bool, Nat, z => SW.value(X.or_bit(S1, z)), Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})), True{}, hb)
401      +e2 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, vh)), v(U32.or(X.lo(S1), 1)), 1n+Nat.double(C.half(vl)), or1(X.lo(S1)))
402      +eq = Equal.trans(Nat, q, SW.value(S1), Nat.add(vl, C.shift(32n, vh)), Equal.sym(Nat, SW.value(S1), q, shr_value(WU.U64{l, h}, k)), WA.val_eta(S1))
403      +eh = Equal.trans(Nat, C.half(q), C.half(Nat.add(vl, C.shift(32n, vh))), Nat.add(C.half(vl), C.shift(31n, vh)), Equal.cong(Nat, Nat, z => C.half(z), q, Nat.add(vl, C.shift(32n, vh)), eq), WW.half_dbl(vl, C.shift(31n, vh)))
404      +e4 = Equal.trans(Nat, SW.jam(q, C.low(k, val(l, h))), SW.jam(q, 1n+lp), 1n+Nat.add(Nat.double(C.half(vl)), C.shift(32n, vh)), Equal.cong(Nat, Nat, z => SW.jam(q, z), C.low(k, val(l, h)), 1n+lp, hL), Equal.trans(Nat, SW.jam(q, 1n+lp), 1n+Nat.double(C.half(q)), 1n+Nat.add(Nat.double(C.half(vl)), C.shift(32n, vh)), jam1_m(q, lp), Equal.cong(Nat, Nat, z => 1n+z, Nat.double(C.half(q)), Nat.add(Nat.double(C.half(vl)), C.shift(32n, vh)), Equal.trans(Nat, Nat.double(C.half(q)), Nat.double(Nat.add(C.half(vl), C.shift(31n, vh))), Nat.add(Nat.double(C.half(vl)), C.shift(32n, vh)), Equal.cong(Nat, Nat, z => Nat.double(z), C.half(q), Nat.add(C.half(vl), C.shift(31n, vh)), eh), NA.double_add(C.half(vl), C.shift(31n, vh))))))
405      Equal.trans(Nat, SW.value(X.or_bit(S1, Bool.not(X.eq(X.shl(S1, k), WU.U64{l, h})))), SW.value(X.or_bit(S1, True{})), SW.jam(q, C.low(k, val(l, h))), e1, Equal.trans(Nat, SW.value(X.or_bit(S1, True{})), 1n+Nat.add(Nat.double(C.half(vl)), C.shift(32n, vh)), SW.jam(q, C.low(k, val(l, h))), e2, Equal.sym(Nat, SW.jam(q, C.low(k, val(l, h))), 1n+Nat.add(Nat.double(C.half(vl)), C.shift(32n, vh)), e4)))