def sj_bit

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

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/logic.bend as L
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

371def sj_bit(+l: U32, +h: U32, +k: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> {Bool.not(X.eq(X.shl(X.shr(WU.U64{l, h}, k), k), WU.U64{l, h})) == Bool.not(Nat.is_eq(C.low(k, val(l, h)), 0n)) : Bool}:
372  +va = val(l, h)
373  +q = C.high(k, va)
374  +S1 = X.shr(WU.U64{l, h}, k)
375  +S2 = X.shl(S1, k)
376  eS1 = shr_value(WU.U64{l, h}, k)
377  +ev = Equal.sym(Nat, va, Nat.add(C.low(k, va), C.shift(k, q)), WW.low_high(k, va))
378  +hle = L.subst(Nat, z => {Nat.is_le(C.shift(k, q), z) == True{} : Bool}, Nat.add(C.shift(k, q), C.low(k, va)), va, Equal.trans(Nat, Nat.add(C.shift(k, q), C.low(k, va)), Nat.add(C.low(k, va), C.shift(k, q)), va, N.add_comm(C.shift(k, q), C.low(k, va)), ev), N.le_add_right(C.shift(k, q), C.low(k, va)))
379  sv = shl_value(S1, k, hk)
380  +eS2 = Equal.trans(Nat, SW.value(S2), C.low(64n, C.shift(k, SW.value(S1))), C.shift(k, q), sv, Equal.trans(Nat, C.low(64n, C.shift(k, SW.value(S1))), C.low(64n, C.shift(k, q)), C.shift(k, q), Equal.cong(Nat, Nat, z => C.low(64n, C.shift(k, z)), SW.value(S1), q, eS1), WW.low_fit(64n, C.shift(k, q), fits_lek(64n, C.shift(k, q), va, hle, fit64(l, h)))))
381  +eq = Equal.trans(Bool, X.eq(S2, WU.U64{l, h}), Nat.is_eq(SW.value(S2), va), Nat.is_eq(C.low(k, va), 0n), WA.eq_value(S2, WU.U64{l, h}), Equal.trans(Bool, Nat.is_eq(SW.value(S2), va), Nat.is_eq(C.shift(k, q), va), Nat.is_eq(C.low(k, va), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, va), SW.value(S2), C.shift(k, q), eS2), Equal.trans(Bool, Nat.is_eq(C.shift(k, q), va), Nat.is_eq(C.shift(k, q), Nat.add(C.low(k, va), C.shift(k, q))), Nat.is_eq(C.low(k, va), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(C.shift(k, q), z), va, Nat.add(C.low(k, va), C.shift(k, q)), Equal.sym(Nat, Nat.add(C.low(k, va), C.shift(k, q)), va, ev)), is_eq_add(C.low(k, va), C.shift(k, q)))))
382  Equal.cong(Bool, Bool, z => Bool.not(z), X.eq(S2, WU.U64{l, h}), Nat.is_eq(C.low(k, va), 0n), eq)