Word.mask_split: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as Word
Lines 286-301 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&start_line=286&end_line=301

import Base
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/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A

# x == (x & mask k) + 2^k (bits above k)
def mask_split(+n: Nat, +k: Nat, +x: Word(n)) -> {uw(n, x) == Nat.add(uw(n, Word.and(n, x, mask(n, k))), sc(k, hi_part(n, k, x))) : Nat}:
  match n k x:
    case 0n _ WNil{}:
      Equal.sym(Nat, sc(k, 0n), 0n, A.sc_zero(k))
    case 1n+p 0n WCon{b, t}:
      %Equal.sym(Nat, uw(1n+p, Word.and(1n+p, WCon{b, t}, mask(1n+p, 0n))), 0n, low0(p, b, t)) : {uw(1n+p, WCon{b, t}) == Nat.add(_, uw(1n+p, WCon{b, t})) : Nat}
      {==}
    case 1n+p 1n+j WCon{b, t}:
      +at = uw(p, Word.and(p, t, mask(p, j)))
      +hs = sc(j, hi_part(p, j, t))
      %Equal.sym(Bool, Bool.and(b, True{}), b, U.and_true(b)) : {Nat.add(S.bit_value(b), Nat.double(uw(p, t))) == Nat.add(Nat.add(S.bit_value(_), Nat.double(at)), Nat.double(hs)) : Nat}
      %Equal.sym(Nat, uw(p, t), Nat.add(at, hs), mask_split(p, j, t)) : {Nat.add(S.bit_value(b), Nat.double(_)) == Nat.add(Nat.add(S.bit_value(b), Nat.double(at)), Nat.double(hs)) : Nat}
      Equal.trans(Nat, Nat.add(S.bit_value(b), Nat.double(Nat.add(at, hs))), Nat.add(S.bit_value(b), Nat.add(Nat.double(at), Nat.double(hs))), Nat.add(Nat.add(S.bit_value(b), Nat.double(at)), Nat.double(hs)),
        Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(b), z), Nat.double(Nat.add(at, hs)), Nat.add(Nat.double(at), Nat.double(hs)), Equal.sym(Nat, Nat.add(Nat.double(at), Nat.double(hs)), Nat.double(Nat.add(at, hs)), N.add_double(at, hs))),
        Equal.sym(Nat, Nat.add(Nat.add(S.bit_value(b), Nat.double(at)), Nat.double(hs)), Nat.add(S.bit_value(b), Nat.add(Nat.double(at), Nat.double(hs))), N.add_assoc(S.bit_value(b), Nat.double(at), Nat.double(hs))))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend&name=and_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend&name=sc_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=hi_part
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=low0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw